# 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›  (‹(_)› 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 (‹¬ _›  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)›

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"  ("(2∃⇩≤⇩1 _./ _)" [0, 10] 10)
translations "∃⇩≤⇩1x. P" ⇌ "CONST Uniq (λx. P)"

print_translation ‹
[Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>‹Uniq› \<^syntax_const>‹_Uniq›]
› ― ‹to avoid eta-contraction of body›

subsubsection ‹Old-style ASCII syntax›

notation (ASCII)
not_equal  (infixl ‹~=› 50) and
Not  (‹~ _›  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  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 ‹
(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›           (‹(2_ =/ _)› 10)
""            :: ‹letbind => letbinds›              (‹_›)
"_binds"      :: ‹[letbind, letbinds] => letbinds›  (‹_;/ _›)
"_Let"        :: ‹[letbinds, 'a] => 'a›             (‹(let (_)/ in (_))› 10)

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
```