Theory Crush.Base

(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
   SPDX-License-Identifier: MIT *)

(*<*)
theory Base
  imports Main
  keywords
    "enable_print_timings" "disable_print_timings" "enable_timings" "disable_timings"
    "reset_timelogs" "show_timelogs" "applyτ" "step" :: prf_script % "proof"
begin

subsection ‹Configuration›

ML_file "config.ML"

subsection ‹Base material›

ML_file "base.ML"
ML‹open Crush_Base›

subsection‹Parsers›

ML_file "parsers.ML"

subsection ‹Tactic profiling›

ML_file "time.ML"
ML‹open Crush_Time›


subsection‹Meng-Paulson filter for premises›

definition IGNORE :: ‹prop ⇒ prop› where
  ‹IGNORE (PROP x) ≡ (PROP x)›

lemma IGNORE_splitE:
  assumes ‹PROP IGNORE (PROP P &&& PROP Q)›
     and ‹PROP IGNORE P ⟹ PROP IGNORE Q ⟹ PROP R›
   shows ‹PROP R›
  using assms apply -
  apply (simp add: IGNORE_def conjunction_imp)
  apply (rule revcut_rl; assumption)
  done

definition IGNORE_imp :: ‹prop ⇒ prop ⇒ prop› where
  ‹IGNORE_imp (PROP P) (PROP Q) ≡ (PROP (IGNORE (PROP P)) ⟹ (PROP Q))›
notation IGNORE_imp ("_ ⟹'' _")

lemma IGNORE_imp_mergeI:
  assumes ‹(PROP P &&& PROP Q) ⟹' PROP R›
  shows ‹PROP P ⟹' (PROP Q ⟹' PROP R)›
  using assms apply -
  apply (simp add: IGNORE_def IGNORE_imp_def conjunction_imp)
  apply (rule revcut_rl; assumption)
  done

lemma IGNORE_imp_cong [cong]:
  assumes ‹PROP Q0 ≡ PROP Q1›
  shows ‹PROP IGNORE_imp (PROP P) (PROP Q0) ≡ PROP IGNORE_imp (PROP P) (PROP Q1)›
  using assms unfolding IGNORE_imp_def by simp

lemma IGNORE_imp_ignoreE:
  assumes ‹PROP P›
  and ‹PROP P ⟹' PROP R›
  shows ‹PROP R›
  using assms unfolding IGNORE_def IGNORE_imp_def apply -
  apply (rule revcut_rl; assumption)
  done

lemma IGNORE_imp_unwrapI:
  assumes ‹PROP IGNORE (PROP P) ⟹ PROP R›
  shows ‹PROP P ⟹' PROP R›
  using assms unfolding IGNORE_imp_def apply -
  apply (rule revcut_rl; assumption)
  done

lemma IGNORE_unwrapE:
  assumes ‹PROP IGNORE (PROP P)›
  and ‹PROP P ⟹ PROP R›
  shows ‹PROP R›
  using assms unfolding IGNORE_def apply -
  apply (rule revcut_rl; assumption)
  done

lemma IGNORE_cong [cong]:
  shows ‹PROP (IGNORE P) ≡ PROP (IGNORE P)›
  unfolding IGNORE_def by simp

syntax (output) "_premise_elided" :: ‹prop ⇒ prop› ("…'(ignored')… ⟹ _")
translations
  "_premise_elided z" ↽ "CONST Pure.imp (CONST IGNORE y) z"
  "_premise_elided z" ↽ "_premise_elided (_premise_elided z)"

ML_file "mepo_prem.ML"

subsection ‹Various tacticals›

ML_file "tacticals.ML"
ML‹open Crush_Tacticals›

end
(*>*)