Theory IFOL

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

section ‹Intuitionistic first-order logic›

theory IFOL
  imports Pure
  abbrevs "?<" = "∃≤1"
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 ∃≤1››∃≤1 _./ _)› [0, 10] 10)
syntax_consts "_Uniq" ⇌ Uniq
translations "∃≤1x. P" ⇌ "CONST Uniq (λx. P)"
typed_print_translation ‹
  [(const_syntax‹Uniq›, Syntax_Trans.preserve_binder_abs_tr' syntax_const‹_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 ML‹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 ML‹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 ‹
structure 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 ‹
structure Hypsubst = Hypsubst
(
  val dest_eq = FOLogic.dest_eq
  val dest_Trueprop = dest_judgment
  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}
);
open Hypsubst;
›

ML_file ‹intprover.ML›


subsection ‹Intuitionistic Reasoning›

setup ‹Intuitionistic.method_setup binding‹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 ML‹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