File ‹Tools/rewrite_hol_proof.ML›
signature REWRITE_HOL_PROOF =
sig
val rews: (Proofterm.proof * Proofterm.proof) list
val elim_cong: typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
end;
structure Rewrite_HOL_Proof : REWRITE_HOL_PROOF =
struct
val rews =
map (apply2 (Proof_Syntax.proof_of_term \<^theory> true) o Logic.dest_equals o
Logic.varify_global o Proof_Syntax.read_term \<^theory> true propT o Syntax.implode_input)
[‹(equal_elim ⋅ x1 ⋅ x2 ∙
(combination ⋅ TYPE('T1) ⋅ TYPE('T2) ⋅ Trueprop ⋅ x3 ⋅ A ⋅ B ∙
(axm.reflexive ⋅ TYPE('T3) ⋅ x4) ∙ prf1)) ≡
(iffD1 ⋅ A ⋅ B ∙
(meta_eq_to_obj_eq ⋅ TYPE(bool) ⋅ A ⋅ B ∙ arity_type_bool ∙ prf1))›,
‹(equal_elim ⋅ x1 ⋅ x2 ∙ (axm.symmetric ⋅ TYPE('T1) ⋅ x3 ⋅ x4 ∙
(combination ⋅ TYPE('T2) ⋅ TYPE('T3) ⋅ Trueprop ⋅ x5 ⋅ A ⋅ B ∙
(axm.reflexive ⋅ TYPE('T4) ⋅ x6) ∙ prf1))) ≡
(iffD2 ⋅ A ⋅ B ∙
(meta_eq_to_obj_eq ⋅ TYPE(bool) ⋅ A ⋅ B ∙ arity_type_bool ∙ prf1))›,
‹(meta_eq_to_obj_eq ⋅ TYPE('U) ⋅ x1 ⋅ x2 ∙ prfU ∙
(combination ⋅ TYPE('T) ⋅ TYPE('U) ⋅ f ⋅ g ⋅ x ⋅ y ∙ prf1 ∙ prf2)) ≡
(cong ⋅ TYPE('T) ⋅ TYPE('U) ⋅ f ⋅ g ⋅ x ⋅ y ∙
(Pure.PClass type_class ⋅ TYPE('T)) ∙ prfU ∙
(meta_eq_to_obj_eq ⋅ TYPE('T ⇒ 'U) ⋅ f ⋅ g ∙ (Pure.PClass type_class ⋅ TYPE('T ⇒ 'U)) ∙ prf1) ∙
(meta_eq_to_obj_eq ⋅ TYPE('T) ⋅ x ⋅ y ∙ (Pure.PClass type_class ⋅ TYPE('T)) ∙ prf2))›,
‹(meta_eq_to_obj_eq ⋅ TYPE('T) ⋅ x1 ⋅ x2 ∙ prfT ∙
(axm.transitive ⋅ TYPE('T) ⋅ x ⋅ y ⋅ z ∙ prf1 ∙ prf2)) ≡
(HOL.trans ⋅ TYPE('T) ⋅ x ⋅ y ⋅ z ∙ prfT ∙
(meta_eq_to_obj_eq ⋅ TYPE('T) ⋅ x ⋅ y ∙ prfT ∙ prf1) ∙
(meta_eq_to_obj_eq ⋅ TYPE('T) ⋅ y ⋅ z ∙ prfT ∙ prf2))›,
‹(meta_eq_to_obj_eq ⋅ TYPE('T) ⋅ x ⋅ x ∙ prfT ∙ (axm.reflexive ⋅ TYPE('T) ⋅ x)) ≡
(HOL.refl ⋅ TYPE('T) ⋅ x ∙ prfT)›,
‹(meta_eq_to_obj_eq ⋅ TYPE('T) ⋅ x ⋅ y ∙ prfT ∙
(axm.symmetric ⋅ TYPE('T) ⋅ x ⋅ y ∙ prf)) ≡
(sym ⋅ TYPE('T) ⋅ x ⋅ y ∙ prfT ∙ (meta_eq_to_obj_eq ⋅ TYPE('T) ⋅ x ⋅ y ∙ prfT ∙ prf))›,
‹(meta_eq_to_obj_eq ⋅ TYPE('T ⇒ 'U) ⋅ x1 ⋅ x2 ∙ prfTU ∙
(abstract_rule ⋅ TYPE('T) ⋅ TYPE('U) ⋅ f ⋅ g ∙ prf)) ≡
(ext ⋅ TYPE('T) ⋅ TYPE('U) ⋅ f ⋅ g ∙
(Pure.PClass type_class ⋅ TYPE('T)) ∙ (Pure.PClass type_class ⋅ TYPE('U)) ∙
(❙λ(x::'T). meta_eq_to_obj_eq ⋅ TYPE('U) ⋅ f x ⋅ g x ∙
(Pure.PClass type_class ⋅ TYPE('U)) ∙ (prf ⋅ x)))›,
‹(meta_eq_to_obj_eq ⋅ TYPE('T) ⋅ x ⋅ y ∙ prfT ∙
(eq_reflection ⋅ TYPE('T) ⋅ x ⋅ y ∙ prfT ∙ prf)) ≡ prf›,
‹(meta_eq_to_obj_eq ⋅ TYPE('T) ⋅ x1 ⋅ x2 ∙ prfT ∙ (equal_elim ⋅ x3 ⋅ x4 ∙
(combination ⋅ TYPE('T) ⋅ TYPE(prop) ⋅ x7 ⋅ x8 ⋅ C ⋅ D ∙
(combination ⋅ TYPE('T) ⋅ TYPE('T3) ⋅ (≡) ⋅ (≡) ⋅ A ⋅ B ∙
(axm.reflexive ⋅ TYPE('T4) ⋅ (≡)) ∙ prf1) ∙ prf2) ∙ prf3)) ≡
(iffD1 ⋅ A = C ⋅ B = D ∙
(cong ⋅ TYPE('T) ⋅ TYPE(bool) ⋅ (=) A ⋅ (=) B ⋅ C ⋅ D ∙
prfT ∙ arity_type_bool ∙
(cong ⋅ TYPE('T) ⋅ TYPE('T⇒bool) ⋅
((=) :: 'T⇒'T⇒bool) ⋅ ((=) :: 'T⇒'T⇒bool) ⋅ A ⋅ B ∙
prfT ∙ (Pure.PClass type_class ⋅ TYPE('T⇒bool)) ∙
(HOL.refl ⋅ TYPE('T⇒'T⇒bool) ⋅ ((=) :: 'T⇒'T⇒bool) ∙
(Pure.PClass type_class ⋅ TYPE('T⇒'T⇒bool))) ∙
(meta_eq_to_obj_eq ⋅ TYPE('T) ⋅ A ⋅ B ∙ prfT ∙ prf1)) ∙
(meta_eq_to_obj_eq ⋅ TYPE('T) ⋅ C ⋅ D ∙ prfT ∙ prf2)) ∙
(meta_eq_to_obj_eq ⋅ TYPE('T) ⋅ A ⋅ C ∙ prfT ∙ prf3))›,
‹(meta_eq_to_obj_eq ⋅ TYPE('T) ⋅ x1 ⋅ x2 ∙ prfT ∙ (equal_elim ⋅ x3 ⋅ x4 ∙
(axm.symmetric ⋅ TYPE('T2) ⋅ x5 ⋅ x6 ∙
(combination ⋅ TYPE('T) ⋅ TYPE(prop) ⋅ x7 ⋅ x8 ⋅ C ⋅ D ∙
(combination ⋅ TYPE('T) ⋅ TYPE('T3) ⋅ (≡) ⋅ (≡) ⋅ A ⋅ B ∙
(axm.reflexive ⋅ TYPE('T4) ⋅ (≡)) ∙ prf1) ∙ prf2)) ∙ prf3)) ≡
(iffD2 ⋅ A = C ⋅ B = D ∙
(cong ⋅ TYPE('T) ⋅ TYPE(bool) ⋅ (=) A ⋅ (=) B ⋅ C ⋅ D ∙
prfT ∙ arity_type_bool ∙
(cong ⋅ TYPE('T) ⋅ TYPE('T⇒bool) ⋅
((=) :: 'T⇒'T⇒bool) ⋅ ((=) :: 'T⇒'T⇒bool) ⋅ A ⋅ B ∙
prfT ∙ (Pure.PClass type_class ⋅ TYPE('T⇒bool)) ∙
(HOL.refl ⋅ TYPE('T⇒'T⇒bool) ⋅ ((=) :: 'T⇒'T⇒bool) ∙
(Pure.PClass type_class ⋅ TYPE('T⇒'T⇒bool))) ∙
(meta_eq_to_obj_eq ⋅ TYPE('T) ⋅ A ⋅ B ∙ prfT ∙ prf1)) ∙
(meta_eq_to_obj_eq ⋅ TYPE('T) ⋅ C ⋅ D ∙ prfT ∙ prf2)) ∙
(meta_eq_to_obj_eq ⋅ TYPE('T) ⋅ B ⋅ D ∙ prfT ∙ prf3))›,
‹(iffD1 ⋅ All P ⋅ All Q ∙ (cong ⋅ TYPE('T1) ⋅ TYPE('T2) ⋅ All ⋅ All ⋅ P ⋅ Q ∙ prfT1 ∙ prfT2 ∙
(HOL.refl ⋅ TYPE('T3) ⋅ x1 ∙ prfT3) ∙
(ext ⋅ TYPE('a) ⋅ TYPE(bool) ⋅ x2 ⋅ x3 ∙ prfa ∙ prfb ∙ prf)) ∙ prf') ≡
(allI ⋅ TYPE('a) ⋅ Q ∙ prfa ∙
(❙λx.
iffD1 ⋅ P x ⋅ Q x ∙ (prf ⋅ x) ∙
(spec ⋅ TYPE('a) ⋅ P ⋅ x ∙ prfa ∙ prf')))›,
‹(iffD2 ⋅ All P ⋅ All Q ∙ (cong ⋅ TYPE('T1) ⋅ TYPE('T2) ⋅ All ⋅ All ⋅ P ⋅ Q ∙ prfT1 ∙ prfT2 ∙
(HOL.refl ⋅ TYPE('T3) ⋅ x1 ∙ prfT3) ∙
(ext ⋅ TYPE('a) ⋅ TYPE(bool) ⋅ x2 ⋅ x3 ∙ prfa ∙ prfb ∙ prf)) ∙ prf') ≡
(allI ⋅ TYPE('a) ⋅ P ∙ prfa ∙
(❙λx.
iffD2 ⋅ P x ⋅ Q x ∙ (prf ⋅ x) ∙
(spec ⋅ TYPE('a) ⋅ Q ⋅ x ∙ prfa ∙ prf')))›,
‹(iffD1 ⋅ Ex P ⋅ Ex Q ∙ (cong ⋅ TYPE('T1) ⋅ TYPE('T2) ⋅ Ex ⋅ Ex ⋅ P ⋅ Q ∙ prfT1 ∙ prfT2 ∙
(HOL.refl ⋅ TYPE('T3) ⋅ x1 ∙ prfT3) ∙
(ext ⋅ TYPE('a) ⋅ TYPE(bool) ⋅ x2 ⋅ x3 ∙ prfa ∙ prfb ∙ prf)) ∙ prf') ≡
(exE ⋅ TYPE('a) ⋅ P ⋅ ∃x. Q x ∙ prfa ∙ prf' ∙
(❙λx H : P x.
exI ⋅ TYPE('a) ⋅ Q ⋅ x ∙ prfa ∙
(iffD1 ⋅ P x ⋅ Q x ∙ (prf ⋅ x) ∙ H)))›,
‹(iffD2 ⋅ Ex P ⋅ Ex Q ∙ (cong ⋅ TYPE('T1) ⋅ TYPE('T2) ⋅ Ex ⋅ Ex ⋅ P ⋅ Q ∙ prfT1 ∙ prfT2 ∙
(HOL.refl ⋅ TYPE('T3) ⋅ x1 ∙ prfT3) ∙
(ext ⋅ TYPE('a) ⋅ TYPE(bool) ⋅ x2 ⋅ x3 ∙ prfa ∙ prfb ∙ prf)) ∙ prf') ≡
(exE ⋅ TYPE('a) ⋅ Q ⋅ ∃x. P x ∙ prfa ∙ prf' ∙
(❙λx H : Q x.
exI ⋅ TYPE('a) ⋅ P ⋅ x ∙ prfa ∙
(iffD2 ⋅ P x ⋅ Q x ∙ (prf ⋅ x) ∙ H)))›,
‹(iffD1 ⋅ A ∧ C ⋅ B ∧ D ∙ (cong ⋅ TYPE('T1) ⋅ TYPE('T2) ⋅ x1 ⋅ x2 ⋅ C ⋅ D ∙ prfT1 ∙ prfT2 ∙
(cong ⋅ TYPE('T3) ⋅ TYPE('T4) ⋅ (∧) ⋅ (∧) ⋅ A ⋅ B ∙ prfT3 ∙ prfT4 ∙
(HOL.refl ⋅ TYPE('T5) ⋅ (∧) ∙ prfT5) ∙ prf1) ∙ prf2) ∙ prf3) ≡
(conjI ⋅ B ⋅ D ∙
(iffD1 ⋅ A ⋅ B ∙ prf1 ∙ (conjunct1 ⋅ A ⋅ C ∙ prf3)) ∙
(iffD1 ⋅ C ⋅ D ∙ prf2 ∙ (conjunct2 ⋅ A ⋅ C ∙ prf3)))›,
‹(iffD2 ⋅ A ∧ C ⋅ B ∧ D ∙ (cong ⋅ TYPE('T1) ⋅ TYPE('T2) ⋅ x1 ⋅ x2 ⋅ C ⋅ D ∙ prfT1 ∙ prfT2 ∙
(cong ⋅ TYPE('T3) ⋅ TYPE('T4) ⋅ (∧) ⋅ (∧) ⋅ A ⋅ B ∙ prfT3 ∙ prfT4 ∙
(HOL.refl ⋅ TYPE('T5) ⋅ (∧) ∙ prfT5) ∙ prf1) ∙ prf2) ∙ prf3) ≡
(conjI ⋅ A ⋅ C ∙
(iffD2 ⋅ A ⋅ B ∙ prf1 ∙ (conjunct1 ⋅ B ⋅ D ∙ prf3)) ∙
(iffD2 ⋅ C ⋅ D ∙ prf2 ∙ (conjunct2 ⋅ B ⋅ D ∙ prf3)))›,
‹(cong ⋅ TYPE(bool) ⋅ TYPE(bool) ⋅ (∧) A ⋅ (∧) A ⋅ B ⋅ C ∙ prfb ∙ prfb ∙
(HOL.refl ⋅ TYPE(bool⇒bool) ⋅ (∧) A ∙ prfbb)) ≡
(cong ⋅ TYPE(bool) ⋅ TYPE(bool) ⋅ (∧) A ⋅ (∧) A ⋅ B ⋅ C ∙ prfb ∙ prfb ∙
(cong ⋅ TYPE(bool) ⋅ TYPE(bool⇒bool) ⋅
((∧) :: bool⇒bool⇒bool) ⋅ ((∧) :: bool⇒bool⇒bool) ⋅ A ⋅ A ∙
prfb ∙ prfbb ∙
(HOL.refl ⋅ TYPE(bool⇒bool⇒bool) ⋅ ((∧) :: bool⇒bool⇒bool) ∙
(Pure.PClass type_class ⋅ TYPE(bool⇒bool⇒bool))) ∙
(HOL.refl ⋅ TYPE(bool) ⋅ A ∙ prfb)))›,
‹(iffD1 ⋅ A ∨ C ⋅ B ∨ D ∙ (cong ⋅ TYPE('T1) ⋅ TYPE('T2) ⋅ x1 ⋅ x2 ⋅ C ⋅ D ∙ prfT1 ∙ prfT2 ∙
(cong ⋅ TYPE('T3) ⋅ TYPE('T4) ⋅ (∨) ⋅ (∨) ⋅ A ⋅ B ∙ prfT3 ∙ prfT4 ∙
(HOL.refl ⋅ TYPE('T5) ⋅ (∨) ∙ prfT5) ∙ prf1) ∙ prf2) ∙ prf3) ≡
(disjE ⋅ A ⋅ C ⋅ B ∨ D ∙ prf3 ∙
(❙λH : A. disjI1 ⋅ B ⋅ D ∙ (iffD1 ⋅ A ⋅ B ∙ prf1 ∙ H)) ∙
(❙λH : C. disjI2 ⋅ D ⋅ B ∙ (iffD1 ⋅ C ⋅ D ∙ prf2 ∙ H)))›,
‹(iffD2 ⋅ A ∨ C ⋅ B ∨ D ∙ (cong ⋅ TYPE('T1) ⋅ TYPE('T2) ⋅ x1 ⋅ x2 ⋅ C ⋅ D ∙ prfT1 ∙ prfT2 ∙
(cong ⋅ TYPE('T3) ⋅ TYPE('T4) ⋅ (∨) ⋅ (∨) ⋅ A ⋅ B ∙ prfT3 ∙ prfT4 ∙
(HOL.refl ⋅ TYPE('T5) ⋅ (∨) ∙ prfT5) ∙ prf1) ∙ prf2) ∙ prf3) ≡
(disjE ⋅ B ⋅ D ⋅ A ∨ C ∙ prf3 ∙
(❙λH : B. disjI1 ⋅ A ⋅ C ∙ (iffD2 ⋅ A ⋅ B ∙ prf1 ∙ H)) ∙
(❙λH : D. disjI2 ⋅ C ⋅ A ∙ (iffD2 ⋅ C ⋅ D ∙ prf2 ∙ H)))›,
‹(cong ⋅ TYPE(bool) ⋅ TYPE(bool) ⋅ (∨) A ⋅ (∨) A ⋅ B ⋅ C ∙ prfb ∙ prfb ∙
(HOL.refl ⋅ TYPE(bool⇒bool) ⋅ (∨) A ∙ prfbb)) ≡
(cong ⋅ TYPE(bool) ⋅ TYPE(bool) ⋅ (∨) A ⋅ (∨) A ⋅ B ⋅ C ∙ prfb ∙ prfb ∙
(cong ⋅ TYPE(bool) ⋅ TYPE(bool⇒bool) ⋅
((∨) :: bool⇒bool⇒bool) ⋅ ((∨) :: bool⇒bool⇒bool) ⋅ A ⋅ A ∙
prfb ∙ prfbb ∙
(HOL.refl ⋅ TYPE(bool⇒bool⇒bool) ⋅ ((∨) :: bool⇒bool⇒bool) ∙
(Pure.PClass type_class ⋅ TYPE(bool⇒bool⇒bool))) ∙
(HOL.refl ⋅ TYPE(bool) ⋅ A ∙ prfb)))›,
‹(iffD1 ⋅ A ⟶ C ⋅ B ⟶ D ∙ (cong ⋅ TYPE('T1) ⋅ TYPE('T2) ⋅ x1 ⋅ x2 ⋅ C ⋅ D ∙ prfT1 ∙ prfT2 ∙
(cong ⋅ TYPE('T3) ⋅ TYPE('T4) ⋅ (⟶) ⋅ (⟶) ⋅ A ⋅ B ∙ prfT3 ∙ prfT4 ∙
(HOL.refl ⋅ TYPE('T5) ⋅ (⟶) ∙ prfT5) ∙ prf1) ∙ prf2) ∙ prf3) ≡
(impI ⋅ B ⋅ D ∙ (❙λH: B. iffD1 ⋅ C ⋅ D ∙ prf2 ∙
(mp ⋅ A ⋅ C ∙ prf3 ∙ (iffD2 ⋅ A ⋅ B ∙ prf1 ∙ H))))›,
‹(iffD2 ⋅ A ⟶ C ⋅ B ⟶ D ∙ (cong ⋅ TYPE('T1) ⋅ TYPE('T2) ⋅ x1 ⋅ x2 ⋅ C ⋅ D ∙ prfT1 ∙ prfT2 ∙
(cong ⋅ TYPE('T3) ⋅ TYPE('T4) ⋅ (⟶) ⋅ (⟶) ⋅ A ⋅ B ∙ prfT3 ∙ prfT4 ∙
(HOL.refl ⋅ TYPE('T5) ⋅ (⟶) ∙ prfT5) ∙ prf1) ∙ prf2) ∙ prf3) ≡
(impI ⋅ A ⋅ C ∙ (❙λH: A. iffD2 ⋅ C ⋅ D ∙ prf2 ∙
(mp ⋅ B ⋅ D ∙ prf3 ∙ (iffD1 ⋅ A ⋅ B ∙ prf1 ∙ H))))›,
‹(cong ⋅ TYPE(bool) ⋅ TYPE(bool) ⋅ (⟶) A ⋅ (⟶) A ⋅ B ⋅ C ∙ prfb ∙ prfb ∙
(HOL.refl ⋅ TYPE(bool⇒bool) ⋅ (⟶) A ∙ prfbb)) ≡
(cong ⋅ TYPE(bool) ⋅ TYPE(bool) ⋅ (⟶) A ⋅ (⟶) A ⋅ B ⋅ C ∙ prfb ∙ prfb ∙
(cong ⋅ TYPE(bool) ⋅ TYPE(bool⇒bool) ⋅
((⟶) :: bool⇒bool⇒bool) ⋅ ((⟶) :: bool⇒bool⇒bool) ⋅ A ⋅ A ∙
prfb ∙ prfbb ∙
(HOL.refl ⋅ TYPE(bool⇒bool⇒bool) ⋅ ((⟶) :: bool⇒bool⇒bool) ∙
(Pure.PClass type_class ⋅ TYPE(bool⇒bool⇒bool))) ∙
(HOL.refl ⋅ TYPE(bool) ⋅ A ∙ prfb)))›,
‹(iffD1 ⋅ ¬ P ⋅ ¬ Q ∙ (cong ⋅ TYPE('T1) ⋅ TYPE('T2) ⋅ Not ⋅ Not ⋅ P ⋅ Q ∙ prfT1 ∙ prfT2 ∙
(HOL.refl ⋅ TYPE('T3) ⋅ Not ∙ prfT3) ∙ prf1) ∙ prf2) ≡
(notI ⋅ Q ∙ (❙λH: Q.
notE ⋅ P ⋅ False ∙ prf2 ∙ (iffD2 ⋅ P ⋅ Q ∙ prf1 ∙ H)))›,
‹(iffD2 ⋅ ¬ P ⋅ ¬ Q ∙ (cong ⋅ TYPE('T1) ⋅ TYPE('T2) ⋅ Not ⋅ Not ⋅ P ⋅ Q ∙ prfT1 ∙ prfT2 ∙
(HOL.refl ⋅ TYPE('T3) ⋅ Not ∙ prfT3) ∙ prf1) ∙ prf2) ≡
(notI ⋅ P ∙ (❙λH: P.
notE ⋅ Q ⋅ False ∙ prf2 ∙ (iffD1 ⋅ P ⋅ Q ∙ prf1 ∙ H)))›,
‹(iffD1 ⋅ B ⋅ D ∙
(iffD1 ⋅ A = C ⋅ B = D ∙ (cong ⋅ TYPE(bool) ⋅ TYPE('T1) ⋅ x1 ⋅ x2 ⋅ C ⋅ D ∙ prfb ∙ prfT1 ∙
(cong ⋅ TYPE(bool) ⋅ TYPE('T2) ⋅ (=) ⋅ (=) ⋅ A ⋅ B ∙ prfb ∙ prfT2 ∙
(HOL.refl ⋅ TYPE('T3) ⋅ (=) ∙ prfT3) ∙ prf1) ∙ prf2) ∙ prf3) ∙ prf4) ≡
(iffD1 ⋅ C ⋅ D ∙ prf2 ∙
(iffD1 ⋅ A ⋅ C ∙ prf3 ∙ (iffD2 ⋅ A ⋅ B ∙ prf1 ∙ prf4)))›,
‹(iffD2 ⋅ B ⋅ D ∙
(iffD1 ⋅ A = C ⋅ B = D ∙ (cong ⋅ TYPE(bool) ⋅ TYPE('T1) ⋅ x1 ⋅ x2 ⋅ C ⋅ D ∙ prfb ∙ prfT1 ∙
(cong ⋅ TYPE(bool) ⋅ TYPE('T2) ⋅ (=) ⋅ (=) ⋅ A ⋅ B ∙ prfb ∙ prfT2 ∙
(HOL.refl ⋅ TYPE('T3) ⋅ (=) ∙ prfT3) ∙ prf1) ∙ prf2) ∙ prf3) ∙ prf4) ≡
(iffD1 ⋅ A ⋅ B ∙ prf1 ∙
(iffD2 ⋅ A ⋅ C ∙ prf3 ∙ (iffD2 ⋅ C ⋅ D ∙ prf2 ∙ prf4)))›,
‹(iffD1 ⋅ A ⋅ C ∙
(iffD2 ⋅ A = C ⋅ B = D ∙ (cong ⋅ TYPE(bool) ⋅ TYPE('T1) ⋅ x1 ⋅ x2 ⋅ C ⋅ D ∙ prfb ∙ prfT1 ∙
(cong ⋅ TYPE(bool) ⋅ TYPE('T2) ⋅ (=) ⋅ (=) ⋅ A ⋅ B ∙ prfb ∙ prfT2 ∙
(HOL.refl ⋅ TYPE('T3) ⋅ (=) ∙ prfT3) ∙ prf1) ∙ prf2) ∙ prf3) ∙ prf4)≡
(iffD2 ⋅ C ⋅ D ∙ prf2 ∙
(iffD1 ⋅ B ⋅ D ∙ prf3 ∙ (iffD1 ⋅ A ⋅ B ∙ prf1 ∙ prf4)))›,
‹(iffD2 ⋅ A ⋅ C ∙
(iffD2 ⋅ A = C ⋅ B = D ∙ (cong ⋅ TYPE(bool) ⋅ TYPE('T1) ⋅ x1 ⋅ x2 ⋅ C ⋅ D ∙ prfb ∙ prfT1 ∙
(cong ⋅ TYPE(bool) ⋅ TYPE('T2) ⋅ (=) ⋅ (=) ⋅ A ⋅ B ∙ prfb ∙ prfT2 ∙
(HOL.refl ⋅ TYPE('T3) ⋅ (=) ∙ prfT3) ∙ prf1) ∙ prf2) ∙ prf3) ∙ prf4) ≡
(iffD2 ⋅ A ⋅ B ∙ prf1 ∙
(iffD2 ⋅ B ⋅ D ∙ prf3 ∙ (iffD1 ⋅ C ⋅ D ∙ prf2 ∙ prf4)))›,
‹(cong ⋅ TYPE(bool) ⋅ TYPE(bool) ⋅ (=) A ⋅ (=) A ⋅ B ⋅ C ∙ prfb ∙ prfb ∙
(HOL.refl ⋅ TYPE(bool⇒bool) ⋅ (=) A ∙ prfbb)) ≡
(cong ⋅ TYPE(bool) ⋅ TYPE(bool) ⋅ (=) A ⋅ (=) A ⋅ B ⋅ C ∙ prfb ∙ prfb ∙
(cong ⋅ TYPE(bool) ⋅ TYPE(bool⇒bool) ⋅
((=) :: bool⇒bool⇒bool) ⋅ ((=) :: bool⇒bool⇒bool) ⋅ A ⋅ A ∙
prfb ∙ prfbb ∙
(HOL.refl ⋅ TYPE(bool⇒bool⇒bool) ⋅ ((=) :: bool⇒bool⇒bool) ∙
(Pure.PClass type_class ⋅ TYPE(bool⇒bool⇒bool))) ∙
(HOL.refl ⋅ TYPE(bool) ⋅ A ∙ prfb)))›,
‹(iffD1 ⋅ A ⋅ C ∙ (HOL.trans ⋅ TYPE(bool) ⋅ A ⋅ B ⋅ C ∙ prfb ∙ prf1 ∙ prf2) ∙ prf3) ≡
(iffD1 ⋅ B ⋅ C ∙ prf2 ∙ (iffD1 ⋅ A ⋅ B ∙ prf1 ∙ prf3))›,
‹(iffD2 ⋅ A ⋅ C ∙ (HOL.trans ⋅ TYPE(bool) ⋅ A ⋅ B ⋅ C ∙ prfb ∙ prf1 ∙ prf2) ∙ prf3) ≡
(iffD2 ⋅ A ⋅ B ∙ prf1 ∙ (iffD2 ⋅ B ⋅ C ∙ prf2 ∙ prf3))›,
‹(iffD1 ⋅ A ⋅ A ∙ (HOL.refl ⋅ TYPE(bool) ⋅ A ∙ prfb) ∙ prf) ≡ prf›,
‹(iffD2 ⋅ A ⋅ A ∙ (HOL.refl ⋅ TYPE(bool) ⋅ A ∙ prfb) ∙ prf) ≡ prf›,
‹(iffD1 ⋅ A ⋅ B ∙ (sym ⋅ TYPE(bool) ⋅ B ⋅ A ∙ prfb ∙ prf)) ≡ (iffD2 ⋅ B ⋅ A ∙ prf)›,
‹(iffD2 ⋅ A ⋅ B ∙ (sym ⋅ TYPE(bool) ⋅ B ⋅ A ∙ prfb ∙ prf)) ≡ (iffD1 ⋅ B ⋅ A ∙ prf)›,
‹(mp ⋅ A ⋅ B ∙ (impI ⋅ A ⋅ B ∙ prf)) ≡ prf›,
‹(impI ⋅ A ⋅ B ∙ (mp ⋅ A ⋅ B ∙ prf)) ≡ prf›,
‹(spec ⋅ TYPE('a) ⋅ P ⋅ x ∙ prfa ∙ (allI ⋅ TYPE('a) ⋅ P ∙ prfa ∙ prf)) ≡ prf ⋅ x›,
‹(allI ⋅ TYPE('a) ⋅ P ∙ prfa ∙ (❙λx::'a. spec ⋅ TYPE('a) ⋅ P ⋅ x ∙ prfa ∙ prf)) ≡ prf›,
‹(exE ⋅ TYPE('a) ⋅ P ⋅ Q ∙ prfa ∙ (exI ⋅ TYPE('a) ⋅ P ⋅ x ∙ prfa ∙ prf1) ∙ prf2) ≡ (prf2 ⋅ x ∙ prf1)›,
‹(exE ⋅ TYPE('a) ⋅ P ⋅ Q ∙ prfa ∙ prf ∙ (exI ⋅ TYPE('a) ⋅ P ∙ prfa)) ≡ prf›,
‹(disjE ⋅ P ⋅ Q ⋅ R ∙ (disjI1 ⋅ P ⋅ Q ∙ prf1) ∙ prf2 ∙ prf3) ≡ (prf2 ∙ prf1)›,
‹(disjE ⋅ P ⋅ Q ⋅ R ∙ (disjI2 ⋅ Q ⋅ P ∙ prf1) ∙ prf2 ∙ prf3) ≡ (prf3 ∙ prf1)›,
‹(conjunct1 ⋅ P ⋅ Q ∙ (conjI ⋅ P ⋅ Q ∙ prf1 ∙ prf2)) ≡ prf1›,
‹(conjunct2 ⋅ P ⋅ Q ∙ (conjI ⋅ P ⋅ Q ∙ prf1 ∙ prf2)) ≡ prf2›,
‹(iffD1 ⋅ A ⋅ B ∙ (iffI ⋅ A ⋅ B ∙ prf1 ∙ prf2)) ≡ prf1›,
‹(iffD2 ⋅ A ⋅ B ∙ (iffI ⋅ A ⋅ B ∙ prf1 ∙ prf2)) ≡ prf2›];
fun strip_cong ps (PThm ({thm_name = (("HOL.cong", 0), _), ...}, _) % _ % _ % SOME x % SOME y %%
prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1
| strip_cong ps (PThm ({thm_name = (("HOL.refl", 0), _), ...}, _) % SOME f %% _) = SOME (f, ps)
| strip_cong _ _ = NONE;
val subst_prf = Proofterm.any_head_of (Thm.proof_of @{thm subst});
val sym_prf = Proofterm.any_head_of (Thm.proof_of @{thm sym});
fun make_subst Ts prf xs (_, []) = prf
| make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) =
let val T = fastype_of1 (Ts, x)
in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
else Proofterm.change_types (SOME [T]) subst_prf %> x %> y %>
Abs ("z", T, list_comb (incr_boundvars 1 f,
map (incr_boundvars 1) xs @ Bound 0 ::
map (incr_boundvars 1 o snd o fst) ps)) %% clprf %% prf' %%
make_subst Ts prf (xs @ [x]) (f, ps)
end;
fun make_sym Ts ((x, y), (prf, clprf)) =
((y, x),
(Proofterm.change_types (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
fun elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD1", 0), _), ...}, _) % _ % _ %% prf1 %% prf2) =
Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
| elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD1", 0), _), ...}, _) % P % _ %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
(strip_cong [] (Proofterm.incr_boundvars 1 0 prf))
| elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD2", 0), _), ...}, _) % _ % _ %% prf1 %% prf2) =
Option.map (make_subst Ts prf2 [] o
apsnd (map (make_sym Ts))) (strip_cong [] prf1)
| elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD2", 0), _), ...}, _) % _ % P %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_boundvars 1 0 prf))
| elim_cong_aux _ _ = NONE;
fun elim_cong Ts hs prf = Option.map (rpair Proofterm.no_skel) (elim_cong_aux Ts prf);
end;