Quelle  IFOL.thy

(*  Title:      FOL/IFOL.thy
    Author:     Lawrence C Paulson and Markus Wenzel
*)

section ‹Intuitionistic first-order logic›

theory IFOL
  imports Pure
  abbrevs "?<" = "∃_\<le>₁"
begin

ML_file ‹~~/src/Tools/misc_legacy.ML›
ML_file ‹~~/src/Provers/splitter.ML›
ML_file ‹~~/src/Provers/hypsubst.ML›
ML_file ‹~~/src/Tools/IsaPlanner/zipper.ML›
ML_file ‹~~/src/Tools/IsaPlanner/isand.ML›
ML_file ‹~~/src/Tools/IsaPlanner/rw_inst.ML›
ML_file ‹~~/src/Provers/quantifier1.ML›
ML_file ‹~~/src/Tools/intuitionistic.ML›
ML_file ‹~~/src/Tools/project_rule.ML›
ML_file ‹~~/src/Tools/atomize_elim.ML›


subsection ‹Syntax and axiomatic basis›

setup Pure_Thy.old_appl_syntax_setup
setup ‹Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])›

class "term"
default_sort ‹term›

typedecl o

judgment
  Trueprop :: ‹o ==> prop›  (‹(‹notation=judgment›_)› 5)


subsubsection ‹Equality›

axiomatization
  eq :: ‹['a, 'a] ==> o›  (infixl ‹=› 50)
where
  refl: ‹a = a› and
  subst: ‹a = b ==> P(a) ==> P(b)›


subsubsection ‹Propositional logic›

axiomatization
  False :: ‹o› and
  conj :: ‹[o, o] => o›  (infixr ‹∧› 35) and
  disj :: ‹[o, o] => o›  (infixr ‹∨› 30) and
  imp :: ‹[o, o] => o›  (infixr ‹⟶› 25)
where
  conjI: ‹[P; Q] ==> P ∧ Q› and
  conjunct1: ‹P ∧ Q ==> P› and
  conjunct2: ‹P ∧ Q ==> Q› and

  disjI1: ‹P ==> P ∨ Q› and
  disjI2: ‹Q ==> P ∨ Q› and
  disjE: ‹[P ∨ Q; P ==> R; Q ==> R] ==> R› and

  impI: ‹(P ==> Q) ==> P ⟶ Q› and
  mp: ‹[P ⟶ Q; P] ==> Q› and

  FalseE: ‹False ==> P›


subsubsection ‹Quantifiers›

axiomatization
  All :: ‹('a ==> o) ==> o›  (binder ‹∀› 10) and
  Ex :: ‹('a ==> o) ==> o›  (binder ‹∃› 10)
where
  allI: ‹(∧x. P(x)) ==> (∀x. P(x))› and
  spec: ‹(∀x. P(x)) ==> P(x)› and
  exI: ‹P(x) ==> (∃x. P(x))› and
  exE: ‹[∃x. P(x); ∧x. P(x) ==> R] ==> R›


subsubsection ‹Definitions›

definition ‹True ≡ False ⟶ False›

definition Not (‹(‹open_block notation=‹prefix ¬››¬ _)› [40] 40)
  where not_def: ‹¬ P ≡ P ⟶ False›

definition iff  (infixr ‹⟷› 25)
  where ‹P ⟷ Q ≡ (P ⟶ Q) ∧ (Q ⟶ P)›

definition Uniq :: "('a ==> o) ==> o"
  where ‹Uniq(P) ≡ (∀x y. P(x) ⟶ P(y) ⟶ y = x)›

definition Ex1 :: ‹('a ==> o) ==> o›  (binder ‹∃!› 10)
  where ex1_def: ‹∃!x. P(x) ≡ ∃x. P(x) ∧ (∀y. P(y) ⟶ y = x)›

axiomatization where  ― ‹Reflection, admissible›
  eq_reflection: ‹(x = y) ==> (x ≡ y)› and
  iff_reflection: ‹(P ⟷ Q) ==> (P ≡ Q)›

abbreviation not_equal :: ‹['a, 'a] ==> o›  (infixl ‹≠› 50)
  where ‹x ≠ y ≡ ¬ (x = y)›

syntax "_Uniq" :: "pttrn ==> o ==> o"  (‹(‹indent=2 notation=‹binder ∃_\≤₁››∃_\≤₁ _./ _)› [0, 10] 10)
syntax_consts "_Uniq" ⇌ Uniq
translations "∃_\<le>₁x. P" ⇌ "CONST Uniq (λx. P)"
typed_print_translation ‹
 [(🍋‹Uniq›, Syntax_Trans.preserve_binder_abs_tr' 🍋‹_Uniq›)]
 › ― ‹to avoid eta-contraction of body›


subsubsection ‹Old-style ASCII syntax›

notation (ASCII)
  not_equal  (infixl ‹~=› 50) and
  Not  (‹(‹open_block notation=‹prefix ~››~ _)› [40] 40) and
  conj  (infixr ‹&› 35) and
  disj  (infixr ‹|› 30) and
  All  (binder ‹ALL › 10) and
  Ex  (binder ‹EX › 10) and
  Ex1  (binder ‹EX! › 10) and
  imp  (infixr ‹-->› 25) and
  iff  (infixr ‹🪙› 25)


subsection ‹Lemmas and proof tools›

lemmas strip = impI allI

lemma TrueI: ‹True›
  unfolding True_def by (rule impI)


subsubsection ‹Sequent-style elimination rules for ‹∧› ‹⟶› and ‹∀››

lemma conjE:
  assumes major: ‹P ∧ Q›
    and r: ‹[P; Q] ==> R›
  shows ‹R›
proof (rule r)
  show "P"
    by (rule major [THEN conjunct1])
  show "Q"
    by (rule major [THEN conjunct2])
qed

lemma impE:
  assumes major: ‹P ⟶ Q›
    and ‹P›
  and r: ‹Q ==> R›
  shows ‹R›
proof (rule r)
  show "Q"
    by (rule mp [OF major ‹P›])
qed

lemma allE:
  assumes major: ‹∀x. P(x)›
    and r: ‹P(x) ==> R›
  shows ‹R›
proof (rule r)
  show "P(x)"
    by (rule major [THEN spec])
qed

text ‹Duplicates the quantifier; for use with 🪙‹eresolve_tac›.›
lemma all_dupE:
  assumes major: ‹∀x. P(x)›
    and r: ‹[P(x); ∀x. P(x)] ==> R›
  shows ‹R›
proof (rule r)
  show "P(x)"
    by (rule major [THEN spec])
qed (rule major)



subsubsection ‹Negation rules, which translate between ‹¬ P› and ‹P ⟶ False››

lemma notI: ‹(P ==> False) ==> ¬ P›
  unfolding not_def by (erule impI)

lemma notE: ‹[¬ P; P] ==> R›
  unfolding not_def by (erule mp [THEN FalseE])

lemma rev_notE: ‹[P; ¬ P] ==> R›
  by (erule notE)

text ‹This is useful with the special implication rules for each kind of ‹P›.›
lemma not_to_imp:
  assumes ‹¬ P›
    and r: ‹P ⟶ False ==> Q›
  shows ‹Q›
  apply (rule r)
  apply (rule impI)
  apply (erule notE [OF ‹¬ P›])
  done

text ‹
 For substitution into an assumption ‹P›, reduce ‹Q› to ‹P ⟶ Q›, substitute into this implication, then apply ‹impI› to
 move ‹P› back into the assumptions.
 ›
lemma rev_mp: ‹[P; P ⟶ Q] ==> Q›
  by (erule mp)

text ‹Contrapositive of an inference rule.›
lemma contrapos:
  assumes major: ‹¬ Q›
    and minor: ‹P ==> Q›
  shows ‹¬ P›
  apply (rule major [THEN notE, THEN notI])
  apply (erule minor)
  done


subsubsection ‹Modus Ponens Tactics›

text ‹
 Finds ‹P ⟶ Q› and P in the assumptions, replaces implication by
 ‹Q›.
 ›
ML ‹
 fun mp_tac ctxt i =
 eresolve_tac ctxt @{thms notE impE} i THEN assume_tac ctxt i;
 fun eq_mp_tac ctxt i =
 eresolve_tac ctxt @{thms notE impE} i THEN eq_assume_tac i;
 ›


subsection ‹If-and-only-if›

lemma iffI: ‹[P ==> Q; Q ==> P] ==> P ⟷ Q›
  unfolding iff_def
  by (rule conjI; erule impI)

lemma iffE:
  assumes major: ‹P ⟷ Q›
    and r: ‹[P ⟶ Q; Q ⟶ P] ==> R›
  shows ‹R›
  using major
  unfolding iff_def
  apply (rule conjE)
  apply (erule r)
  apply assumption
  done


subsubsection ‹Destruct rules for ‹⟷› similar to Modus Ponens›

lemma iffD1: ‹[P ⟷ Q; P] ==> Q›
  unfolding iff_def
  apply (erule conjunct1 [THEN mp])
  apply assumption
  done

lemma iffD2: ‹[P ⟷ Q; Q] ==> P›
  unfolding iff_def
  apply (erule conjunct2 [THEN mp])
  apply assumption
  done

lemma rev_iffD1: ‹[P; P ⟷ Q] ==> Q›
  apply (erule iffD1)
  apply assumption
  done

lemma rev_iffD2: ‹[Q; P ⟷ Q] ==> P›
  apply (erule iffD2)
  apply assumption
  done

lemma iff_refl: ‹P ⟷ P›
  by (rule iffI)

lemma iff_sym: ‹Q ⟷ P ==> P ⟷ Q›
  apply (erule iffE)
  apply (rule iffI)
  apply (assumption | erule mp)+
  done

lemma iff_trans: ‹[P ⟷ Q; Q ⟷ R] ==> P ⟷ R›
  apply (rule iffI)
  apply (assumption | erule iffE | erule (1) notE impE)+
  done


subsection ‹Unique existence›

text ‹
 NOTE THAT the following 2 quantifications:

 ▪ ‹∃!x› such that [‹∃!y› such that P(x,y)] (sequential)
 ▪ ‹∃!x,y› such that P(x,y) (simultaneous)

 do NOT mean the same thing. The parser treats ‹∃!x y.P(x,y)› as sequential.
 ›

lemma ex1I: ‹P(a) ==> (∧x. P(x) ==> x = a) ==> ∃!x. P(x)›
  unfolding ex1_def
  apply (assumption | rule exI conjI allI impI)+
  done

text ‹Sometimes easier to use: the premises have no shared variables. Safe!›
lemma ex_ex1I: ‹∃x. P(x) ==> (∧x y. [P(x); P(y)] ==> x = y) ==> ∃!x. P(x)›
  apply (erule exE)
  apply (rule ex1I)
   apply assumption
  apply assumption
  done

lemma ex1E: ‹∃! x. P(x) ==> (∧x. [P(x); ∀y. P(y) ⟶ y = x] ==> R) ==> R›
  unfolding ex1_def
  apply (assumption | erule exE conjE)+
  done


subsubsection ‹‹⟷› congruence rules for simplification›

text ‹Use ‹iffE› on a premise. For ‹conj_cong›, ‹imp_cong›, ‹all_cong›, ‹ex_cong›.›
ML ‹
 fun iff_tac ctxt prems i =
 resolve_tac ctxt (prems RL @{thms iffE}) i THEN
 REPEAT1 (eresolve_tac ctxt @{thms asm_rl mp} i);
 ›

method_setup iff =
  ‹Attrib.thms >>
 (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))›

lemma conj_cong:
  assumes ‹P ⟷ P'›
    and ‹P' ==> Q ⟷ Q'›
  shows ‹(P ∧ Q) ⟷ (P' ∧ Q')›
  apply (insert assms)
  apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
  done

text ‹Reversed congruence rule! Used in ZF/Order.›
lemma conj_cong2:
  assumes ‹P ⟷ P'›
    and ‹P' ==> Q ⟷ Q'›
  shows ‹(Q ∧ P) ⟷ (Q' ∧ P')›
  apply (insert assms)
  apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
  done

lemma disj_cong:
  assumes ‹P ⟷ P'› and ‹Q ⟷ Q'›
  shows ‹(P ∨ Q) ⟷ (P' ∨ Q')›
  apply (insert assms)
  apply (erule iffE disjE disjI1 disjI2 |
    assumption | rule iffI | erule (1) notE impE)+
  done

lemma imp_cong:
  assumes ‹P ⟷ P'›
    and ‹P' ==> Q ⟷ Q'›
  shows ‹(P ⟶ Q) ⟷ (P' ⟶ Q')›
  apply (insert assms)
  apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE | iff assms)+
  done

lemma iff_cong: ‹[P ⟷ P'; Q ⟷ Q'] ==> (P ⟷ Q) ⟷ (P' ⟷ Q')›
  apply (erule iffE | assumption | rule iffI | erule (1) notE impE)+
  done

lemma not_cong: ‹P ⟷ P' ==> ¬ P ⟷ ¬ P'›
  apply (assumption | rule iffI notI | erule (1) notE impE | erule iffE notE)+
  done

lemma all_cong:
  assumes ‹∧x. P(x) ⟷ Q(x)›
  shows ‹(∀x. P(x)) ⟷ (∀x. Q(x))›
  apply (assumption | rule iffI allI | erule (1) notE impE | erule allE | iff assms)+
  done

lemma ex_cong:
  assumes ‹∧x. P(x) ⟷ Q(x)›
  shows ‹(∃x. P(x)) ⟷ (∃x. Q(x))›
  apply (erule exE | assumption | rule iffI exI | erule (1) notE impE | iff assms)+
  done

lemma ex1_cong:
  assumes ‹∧x. P(x) ⟷ Q(x)›
  shows ‹(∃!x. P(x)) ⟷ (∃!x. Q(x))›
  apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE | iff assms)+
  done


subsection ‹Equality rules›

lemma sym: ‹a = b ==> b = a›
  apply (erule subst)
  apply (rule refl)
  done

lemma trans: ‹[a = b; b = c] ==> a = c›
  apply (erule subst, assumption)
  done

lemma not_sym: ‹b ≠ a ==> a ≠ b›
  apply (erule contrapos)
  apply (erule sym)
  done

text ‹
 Two theorems for rewriting only one instance of a definition:
 the first for definitions of formulae and the second for terms.
 ›

lemma def_imp_iff: ‹(A ≡ B) ==> A ⟷ B›
  apply unfold
  apply (rule iff_refl)
  done

lemma meta_eq_to_obj_eq: ‹(A ≡ B) ==> A = B›
  apply unfold
  apply (rule refl)
  done

lemma meta_eq_to_iff: ‹x ≡ y ==> x ⟷ y›
  by unfold (rule iff_refl)

text ‹Substitution.›
lemma ssubst: ‹[b = a; P(a)] ==> P(b)›
  apply (drule sym)
  apply (erule (1) subst)
  done

text ‹A special case of ‹ex1E› that would otherwise need quantifier
 expansion.›
lemma ex1_equalsE: ‹[∃!x. P(x); P(a); P(b)] ==> a = b›
  apply (erule ex1E)
  apply (rule trans)
   apply (rule_tac [2] sym)
   apply (assumption | erule spec [THEN mp])+
  done


subsection ‹Simplifications of assumed implications›

text ‹
 Roy Dyckhoff has proved that ‹conj_impE›, ‹disj_impE›, and
 ‹imp_impE› used with 🪙‹mp_tac› (restricted to atomic formulae) is
 COMPLETE for intuitionistic propositional logic.

 See R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
 (preprint, University of St Andrews, 1991).
 ›

lemma conj_impE:
  assumes major: ‹(P ∧ Q) ⟶ S›
    and r: ‹P ⟶ (Q ⟶ S) ==> R›
  shows ‹R›
  by (assumption | rule conjI impI major [THEN mp] r)+

lemma disj_impE:
  assumes major: ‹(P ∨ Q) ⟶ S›
    and r: ‹[P ⟶ S; Q ⟶ S] ==> R›
  shows ‹R›
  by (assumption | rule disjI1 disjI2 impI major [THEN mp] r)+

text ‹Simplifies the implication. Classical version is stronger.
 Still UNSAFE since Q must be provable -- backtracking needed.›
lemma imp_impE:
  assumes major: ‹(P ⟶ Q) ⟶ S›
    and r1: ‹[P; Q ⟶ S] ==> Q›
    and r2: ‹S ==> R›
  shows ‹R›
  by (assumption | rule impI major [THEN mp] r1 r2)+

text ‹Simplifies the implication. Classical version is stronger.
 Still UNSAFE since ~P must be provable -- backtracking needed.›
lemma not_impE: ‹¬ P ⟶ S ==> (P ==> False) ==> (S ==> R) ==> R›
  apply (drule mp)
   apply (rule notI | assumption)+
  done

text ‹Simplifies the implication. UNSAFE.›
lemma iff_impE:
  assumes major: ‹(P ⟷ Q) ⟶ S›
    and r1: ‹[P; Q ⟶ S] ==> Q›
    and r2: ‹[Q; P ⟶ S] ==> P›
    and r3: ‹S ==> R›
  shows ‹R›
  by (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+

text ‹What if ‹(∀x. ¬ ¬ P(x)) ⟶ ¬ ¬ (∀x. P(x))› is an assumption?
 UNSAFE.›
lemma all_impE:
  assumes major: ‹(∀x. P(x)) ⟶ S›
    and r1: ‹∧x. P(x)›
    and r2: ‹S ==> R›
  shows ‹R›
  by (rule allI impI major [THEN mp] r1 r2)+

text ‹
 Unsafe: ‹∃x. P(x)) ⟶ S› is equivalent
 to ‹∀x. P(x) ⟶ S›.›
lemma ex_impE:
  assumes major: ‹(∃x. P(x)) ⟶ S›
    and r: ‹P(x) ⟶ S ==> R›
  shows ‹R›
  by (assumption | rule exI impI major [THEN mp] r)+

text ‹Courtesy of Krzysztof Grabczewski.›
lemma disj_imp_disj: ‹P ∨ Q ==> (P ==> R) ==> (Q ==> S) ==> R ∨ S›
  apply (erule disjE)
  apply (rule disjI1) apply assumption
  apply (rule disjI2) apply assumption
  done

ML ‹
  Project_Rule = Project_Rule
 
 val conjunct1 = @{thm conjunct1}
 val conjunct2 = @{thm conjunct2}
 val mp = @{thm mp}
 
 ›

ML_file ‹fologic.ML›

lemma thin_refl: ‹[x = x; PROP W] ==> PROP W› .

ML ‹
  Hypsubst = Hypsubst
 
 val dest_eq = FOLogic.dest_eq
 val dest_Trueprop = 🍋
 val dest_imp = FOLogic.dest_imp
 val eq_reflection = @{thm eq_reflection}
 val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
 val imp_intr = @{thm impI}
 val rev_mp = @{thm rev_mp}
 val subst = @{thm subst}
 val sym = @{thm sym}
 val thin_refl = @{thm thin_refl}
 ;
  Hypsubst;
 ›

ML_file ‹intprover.ML›


subsection ‹Intuitionistic Reasoning›

setup ‹Intuitionistic.method_setup 🍋‹iprover››

lemma impE':
  assumes 1: ‹P ⟶ Q›
    and 2: ‹Q ==> R›
    and 3: ‹P ⟶ Q ==> P›
  shows ‹R›
proof -
  from 3 and 1 have ‹P› .
  with 1 have ‹Q› by (rule impE)
  with 2 show ‹R› .
qed

lemma allE':
  assumes 1: ‹∀x. P(x)›
    and 2: ‹P(x) ==> ∀x. P(x) ==> Q›
  shows ‹Q›
proof -
  from 1 have ‹P(x)› by (rule spec)
  from this and 1 show ‹Q› by (rule 2)
qed

lemma notE':
  assumes 1: ‹¬ P›
    and 2: ‹¬ P ==> P›
  shows ‹R›
proof -
  from 2 and 1 have ‹P› .
  with 1 show ‹R› by (rule notE)
qed

lemmas [Pure.elim!] = disjE iffE FalseE conjE exE
  and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
  and [Pure.elim 2] = allE notE' impE'
  and [Pure.intro] = exI disjI2 disjI1

setup ‹
 Context_Rules.addSWrapper
 (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac)
 ›


lemma iff_not_sym: ‹¬ (Q ⟷ P) ==> ¬ (P ⟷ Q)›
  by iprover

lemmas [sym] = sym iff_sym not_sym iff_not_sym
  and [Pure.elim?] = iffD1 iffD2 impE


lemma eq_commute: ‹a = b ⟷ b = a›
  by iprover


subsection ‹Polymorphic congruence rules›

lemma subst_context: ‹a = b ==> t(a) = t(b)›
  by iprover

lemma subst_context2: ‹[a = b; c = d] ==> t(a,c) = t(b,d)›
  by iprover

lemma subst_context3: ‹[a = b; c = d; e = f] ==> t(a,c,e) = t(b,d,f)›
  by iprover

text ‹
 Useful with 🪙‹eresolve_tac› for proving equalities from known
 equalities.

 a = b
 | |
 c = d
 ›
lemma box_equals: ‹[a = b; a = c; b = d] ==> c = d›
  by iprover

text ‹Dual of ‹box_equals›: for proving equalities backwards.›
lemma simp_equals: ‹[a = c; b = d; c = d] ==> a = b›
  by iprover


subsubsection ‹Congruence rules for predicate letters›

lemma pred1_cong: ‹a = a' ==> P(a) ⟷ P(a')›
  by iprover

lemma pred2_cong: ‹[a = a'; b = b'] ==> P(a,b) ⟷ P(a',b')›
  by iprover

lemma pred3_cong: ‹[a = a'; b = b'; c = c'] ==> P(a,b,c) ⟷ P(a',b',c')›
  by iprover

text ‹Special case for the equality predicate!›
lemma eq_cong: ‹[a = a'; b = b'] ==> a = b ⟷ a' = b'›
  by iprover


subsection ‹Atomizing meta-level rules›

lemma atomize_all [atomize]: ‹(∧x. P(x)) ≡ Trueprop (∀x. P(x))›
proof
  assume ‹∧x. P(x)›
  then show ‹∀x. P(x)› ..
next
  assume ‹∀x. P(x)›
  then show ‹∧x. P(x)› ..
qed

lemma atomize_imp [atomize]: ‹(A ==> B) ≡ Trueprop (A ⟶ B)›
proof
  assume ‹A ==> B›
  then show ‹A ⟶ B› ..
next
  assume ‹A ⟶ B› and ‹A›
  then show ‹B› by (rule mp)
qed

lemma atomize_eq [atomize]: ‹(x ≡ y) ≡ Trueprop (x = y)›
proof
  assume ‹x ≡ y›
  show ‹x = y› unfolding ‹x ≡ y› by (rule refl)
next
  assume ‹x = y›
  then show ‹x ≡ y› by (rule eq_reflection)
qed

lemma atomize_iff [atomize]: ‹(A ≡ B) ≡ Trueprop (A ⟷ B)›
proof
  assume ‹A ≡ B›
  show ‹A ⟷ B› unfolding ‹A ≡ B› by (rule iff_refl)
next
  assume ‹A ⟷ B›
  then show ‹A ≡ B› by (rule iff_reflection)
qed

lemma atomize_conj [atomize]: ‹(A &&& B) ≡ Trueprop (A ∧ B)›
proof
  assume conj: ‹A &&& B›
  show ‹A ∧ B›
  proof (rule conjI)
    from conj show ‹A› by (rule conjunctionD1)
    from conj show ‹B› by (rule conjunctionD2)
  qed
next
  assume conj: ‹A ∧ B›
  show ‹A &&& B›
  proof -
    from conj show ‹A› ..
    from conj show ‹B› ..
  qed
qed

lemmas [symmetric, rulify] = atomize_all atomize_imp
  and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff


subsection ‹Atomizing elimination rules›

lemma atomize_exL[atomize_elim]: ‹(∧x. P(x) ==> Q) ≡ ((∃x. P(x)) ==> Q)›
  by rule iprover+

lemma atomize_conjL[atomize_elim]: ‹(A ==> B ==> C) ≡ (A ∧ B ==> C)›
  by rule iprover+

lemma atomize_disjL[atomize_elim]: ‹((A ==> C) ==> (B ==> C) ==> C) ≡ ((A ∨ B ==> C) ==> C)›
  by rule iprover+

lemma atomize_elimL[atomize_elim]: ‹(∧B. (A ==> B) ==> B) ≡ Trueprop(A)› ..


subsection ‹Calculational rules›

lemma forw_subst: ‹a = b ==> P(b) ==> P(a)›
  by (rule ssubst)

lemma back_subst: ‹P(a) ==> a = b ==> P(b)›
  by (rule subst)

text ‹
 Note that this list of rules is in reverse order of priorities.
 ›

lemmas basic_trans_rules [trans] =
  forw_subst
  back_subst
  rev_mp
  mp
  trans


subsection ‹``Let'' declarations›

nonterminal letbinds and letbind

definition Let :: ‹['a::{}, 'a => 'b] ==> ('b::{})›
  where ‹Let(s, f) ≡ f(s)›

syntax
  "_bind"       :: ‹[pttrn, 'a] => letbind›  (‹(‹indent=2 notation=‹infix let binding››_ =/ _)› 10)
  ""            :: ‹letbind => letbinds›              (‹_›)
  "_binds"      :: ‹[letbind, letbinds] => letbinds›  (‹_;/ _›)
  "_Let"        :: ‹[letbinds, 'a] => 'a›  (‹(‹notation=‹mixfix let expression››let (_)/ in (_))› 10)
syntax_consts
  "_Let" ⇌ Let
translations
  "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
  "let x = a in e"          == "CONST Let(a, λx. e)"

lemma LetI:
  assumes ‹∧x. x = t ==> P(u(x))›
  shows ‹P(let x = t in u(x))›
  unfolding Let_def
  apply (rule refl [THEN assms])
  done


subsection ‹Intuitionistic simplification rules›

lemma conj_simps:
  ‹P ∧ True ⟷ P›
  ‹True ∧ P ⟷ P›
  ‹P ∧ False ⟷ False›
  ‹False ∧ P ⟷ False›
  ‹P ∧ P ⟷ P›
  ‹P ∧ P ∧ Q ⟷ P ∧ Q›
  ‹P ∧ ¬ P ⟷ False›
  ‹¬ P ∧ P ⟷ False›
  ‹(P ∧ Q) ∧ R ⟷ P ∧ (Q ∧ R)›
  by iprover+

lemma disj_simps:
  ‹P ∨ True ⟷ True›
  ‹True ∨ P ⟷ True›
  ‹P ∨ False ⟷ P›
  ‹False ∨ P ⟷ P›
  ‹P ∨ P ⟷ P›
  ‹P ∨ P ∨ Q ⟷ P ∨ Q›
  ‹(P ∨ Q) ∨ R ⟷ P ∨ (Q ∨ R)›
  by iprover+

lemma not_simps:
  ‹¬ (P ∨ Q) ⟷ ¬ P ∧ ¬ Q›
  ‹¬ False ⟷ True›
  ‹¬ True ⟷ False›
  by iprover+

lemma imp_simps:
  ‹(P ⟶ False) ⟷ ¬ P›
  ‹(P ⟶ True) ⟷ True›
  ‹(False ⟶ P) ⟷ True›
  ‹(True ⟶ P) ⟷ P›
  ‹(P ⟶ P) ⟷ True›
  ‹(P ⟶ ¬ P) ⟷ ¬ P›
  by iprover+

lemma iff_simps:
  ‹(True ⟷ P) ⟷ P›
  ‹(P ⟷ True) ⟷ P›
  ‹(P ⟷ P) ⟷ True›
  ‹(False ⟷ P) ⟷ ¬ P›
  ‹(P ⟷ False) ⟷ ¬ P›
  by iprover+

text ‹The ‹x = t› versions are needed for the simplification
 procedures.›
lemma quant_simps:
  ‹∧P. (∀x. P) ⟷ P›
  ‹(∀x. x = t ⟶ P(x)) ⟷ P(t)›
  ‹(∀x. t = x ⟶ P(x)) ⟷ P(t)›
  ‹∧P. (∃x. P) ⟷ P›
  ‹∃x. x = t›
  ‹∃x. t = x›
  ‹(∃x. x = t ∧ P(x)) ⟷ P(t)›
  ‹(∃x. t = x ∧ P(x)) ⟷ P(t)›
  by iprover+

text ‹These are NOT supplied by default!›
lemma distrib_simps:
  ‹P ∧ (Q ∨ R) ⟷ P ∧ Q ∨ P ∧ R›
  ‹(Q ∨ R) ∧ P ⟷ Q ∧ P ∨ R ∧ P›
  ‹(P ∨ Q ⟶ R) ⟷ (P ⟶ R) ∧ (Q ⟶ R)›
  by iprover+

lemma subst_all:
  ‹(∧x. x = a ==> PROP P(x)) ≡ PROP P(a)›
  ‹(∧x. a = x ==> PROP P(x)) ≡ PROP P(a)›
proof -
  show ‹(∧x. x = a ==> PROP P(x)) ≡ PROP P(a)›
  proof (rule equal_intr_rule)
    assume *: ‹∧x. x = a ==> PROP P(x)›
    show ‹PROP P(a)›
      by (rule *) (rule refl)
  next
    fix x
    assume ‹PROP P(a)› and ‹x = a›
    from ‹x = a› have ‹x ≡ a›
      by (rule eq_reflection)
    with ‹PROP P(a)› show ‹PROP P(x)›
      by simp
  qed
  show ‹(∧x. a = x ==> PROP P(x)) ≡ PROP P(a)›
  proof (rule equal_intr_rule)
    assume *: ‹∧x. a = x ==> PROP P(x)›
    show ‹PROP P(a)›
      by (rule *) (rule refl)
  next
    fix x
    assume ‹PROP P(a)› and ‹a = x›
    from ‹a = x› have ‹a ≡ x›
      by (rule eq_reflection)
    with ‹PROP P(a)› show ‹PROP P(x)›
      by simp
  qed
qed


subsubsection ‹Conversion into rewrite rules›

lemma P_iff_F: ‹¬ P ==> (P ⟷ False)›
  by iprover
lemma iff_reflection_F: ‹¬ P ==> (P ≡ False)›
  by (rule P_iff_F [THEN iff_reflection])

lemma P_iff_T: ‹P ==> (P ⟷ True)›
  by iprover
lemma iff_reflection_T: ‹P ==> (P ≡ True)›
  by (rule P_iff_T [THEN iff_reflection])


subsubsection ‹More rewrite rules›

lemma conj_commute: ‹P ∧ Q ⟷ Q ∧ P› by iprover
lemma conj_left_commute: ‹P ∧ (Q ∧ R) ⟷ Q ∧ (P ∧ R)› by iprover
lemmas conj_comms = conj_commute conj_left_commute

lemma disj_commute: ‹P ∨ Q ⟷ Q ∨ P› by iprover
lemma disj_left_commute: ‹P ∨ (Q ∨ R) ⟷ Q ∨ (P ∨ R)› by iprover
lemmas disj_comms = disj_commute disj_left_commute

lemma conj_disj_distribL: ‹P ∧ (Q ∨ R) ⟷ (P ∧ Q ∨ P ∧ R)› by iprover
lemma conj_disj_distribR: ‹(P ∨ Q) ∧ R ⟷ (P ∧ R ∨ Q ∧ R)› by iprover

lemma disj_conj_distribL: ‹P ∨ (Q ∧ R) ⟷ (P ∨ Q) ∧ (P ∨ R)› by iprover
lemma disj_conj_distribR: ‹(P ∧ Q) ∨ R ⟷ (P ∨ R) ∧ (Q ∨ R)› by iprover

lemma imp_conj_distrib: ‹(P ⟶ (Q ∧ R)) ⟷ (P ⟶ Q) ∧ (P ⟶ R)› by iprover
lemma imp_conj: ‹((P ∧ Q) ⟶ R) ⟷ (P ⟶ (Q ⟶ R))› by iprover
lemma imp_disj: ‹(P ∨ Q ⟶ R) ⟷ (P ⟶ R) ∧ (Q ⟶ R)› by iprover

lemma de_Morgan_disj: ‹(¬ (P ∨ Q)) ⟷ (¬ P ∧ ¬ Q)› by iprover

lemma not_ex: ‹(¬ (∃x. P(x))) ⟷ (∀x. ¬ P(x))› by iprover
lemma imp_ex: ‹((∃x. P(x)) ⟶ Q) ⟷ (∀x. P(x) ⟶ Q)› by iprover

lemma ex_disj_distrib: ‹(∃x. P(x) ∨ Q(x)) ⟷ ((∃x. P(x)) ∨ (∃x. Q(x)))›
  by iprover

lemma all_conj_distrib: ‹(∀x. P(x) ∧ Q(x)) ⟷ ((∀x. P(x)) ∧ (∀x. Q(x)))›
  by iprover

end