1(*  Title:      HOL/Tools/rewrite_hol_proof.ML
2    Author:     Stefan Berghofer, TU Muenchen
3
4Rewrite rules for HOL proofs.
5*)
6
7signature REWRITE_HOL_PROOF =
8sig
9  val rews: (Proofterm.proof * Proofterm.proof) list
10  val elim_cong: typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
11end;
12
13structure Rewrite_HOL_Proof : REWRITE_HOL_PROOF =
14struct
15
16val rews =
17  map (apply2 (Proof_Syntax.proof_of_term \<^theory> true) o Logic.dest_equals o
18    Logic.varify_global o Proof_Syntax.read_term \<^theory> true propT o Syntax.implode_input)
19
20  (** eliminate meta-equality rules **)
21
22  [\<open>(equal_elim \<cdot> x1 \<cdot> x2 \<bullet>
23      (combination \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> Trueprop \<cdot> x3 \<cdot> A \<cdot> B \<bullet>
24        (axm.reflexive \<cdot> TYPE('T3) \<cdot> x4) \<bullet> prf1)) \<equiv>
25    (iffD1 \<cdot> A \<cdot> B \<bullet>
26      (meta_eq_to_obj_eq \<cdot> TYPE(bool) \<cdot> A \<cdot> B \<bullet> arity_type_bool \<bullet> prf1))\<close>,
27
28   \<open>(equal_elim \<cdot> x1 \<cdot> x2 \<bullet> (axm.symmetric \<cdot> TYPE('T1) \<cdot> x3 \<cdot> x4 \<bullet>
29      (combination \<cdot> TYPE('T2) \<cdot> TYPE('T3) \<cdot> Trueprop \<cdot> x5 \<cdot> A \<cdot> B \<bullet>
30        (axm.reflexive \<cdot> TYPE('T4) \<cdot> x6) \<bullet> prf1))) \<equiv>
31    (iffD2 \<cdot> A \<cdot> B \<bullet>
32      (meta_eq_to_obj_eq \<cdot> TYPE(bool) \<cdot> A \<cdot> B \<bullet> arity_type_bool \<bullet> prf1))\<close>,
33
34   \<open>(meta_eq_to_obj_eq \<cdot> TYPE('U) \<cdot> x1 \<cdot> x2 \<bullet> prfU \<bullet>
35      (combination \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<cdot> x \<cdot> y \<bullet> prf1 \<bullet> prf2)) \<equiv>
36    (cong \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<cdot> x \<cdot> y \<bullet>
37      (Pure.OfClass type_class \<cdot> TYPE('T)) \<bullet> prfU \<bullet>
38      (meta_eq_to_obj_eq \<cdot> TYPE('T \<Rightarrow> 'U) \<cdot> f \<cdot> g \<bullet> (Pure.OfClass type_class \<cdot> TYPE('T \<Rightarrow> 'U)) \<bullet> prf1) \<bullet>
39      (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> (Pure.OfClass type_class \<cdot> TYPE('T)) \<bullet> prf2))\<close>,
40
41   \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x1 \<cdot> x2 \<bullet> prfT \<bullet>
42      (axm.transitive \<cdot> TYPE('T) \<cdot> x \<cdot> y \<cdot> z \<bullet> prf1 \<bullet> prf2)) \<equiv>
43    (HOL.trans \<cdot> TYPE('T) \<cdot> x \<cdot> y \<cdot> z \<bullet> prfT \<bullet>
44      (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet> prf1) \<bullet>
45      (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> y \<cdot> z \<bullet> prfT \<bullet> prf2))\<close>,
46
47   \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> x \<bullet> prfT \<bullet> (axm.reflexive \<cdot> TYPE('T) \<cdot> x)) \<equiv>
48    (HOL.refl \<cdot> TYPE('T) \<cdot> x \<bullet> prfT)\<close>,
49
50   \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet>
51      (axm.symmetric \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prf)) \<equiv>
52    (sym \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet> (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet> prf))\<close>,
53
54   \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T \<Rightarrow> 'U) \<cdot> x1 \<cdot> x2 \<bullet> prfTU \<bullet>
55      (abstract_rule \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<bullet> prf)) \<equiv>
56    (ext \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<bullet>
57      (Pure.OfClass type_class \<cdot> TYPE('T)) \<bullet> (Pure.OfClass type_class \<cdot> TYPE('U)) \<bullet>
58      (\<^bold>\<lambda>(x::'T). meta_eq_to_obj_eq \<cdot> TYPE('U) \<cdot> f x \<cdot> g x \<bullet>
59         (Pure.OfClass type_class \<cdot> TYPE('U)) \<bullet> (prf \<cdot> x)))\<close>,
60
61   \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet>
62      (eq_reflection \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet> prf)) \<equiv> prf\<close>,
63
64   \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x1 \<cdot> x2 \<bullet> prfT \<bullet> (equal_elim \<cdot> x3 \<cdot> x4 \<bullet>
65      (combination \<cdot> TYPE('T) \<cdot> TYPE(prop) \<cdot> x7 \<cdot> x8 \<cdot> C \<cdot> D \<bullet>
66        (combination \<cdot> TYPE('T) \<cdot> TYPE('T3) \<cdot> (\<equiv>) \<cdot> (\<equiv>) \<cdot> A \<cdot> B \<bullet>
67          (axm.reflexive \<cdot> TYPE('T4) \<cdot> (\<equiv>)) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3)) \<equiv>
68    (iffD1 \<cdot> A = C \<cdot> B = D \<bullet>
69      (cong \<cdot> TYPE('T) \<cdot> TYPE(bool) \<cdot> (=) A \<cdot> (=) B \<cdot> C \<cdot> D \<bullet>
70        prfT \<bullet> arity_type_bool \<bullet>
71        (cong \<cdot> TYPE('T) \<cdot> TYPE('T\<Rightarrow>bool) \<cdot>
72          ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> A \<cdot> B \<bullet>
73          prfT \<bullet> (Pure.OfClass type_class \<cdot> TYPE('T\<Rightarrow>bool)) \<bullet>
74          (HOL.refl \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<bullet>
75             (Pure.OfClass type_class \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool))) \<bullet>
76          (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> A \<cdot> B \<bullet> prfT \<bullet> prf1)) \<bullet>
77        (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> C \<cdot> D \<bullet> prfT \<bullet> prf2)) \<bullet>
78      (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> A \<cdot> C \<bullet> prfT \<bullet> prf3))\<close>,
79
80   \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x1 \<cdot> x2 \<bullet> prfT \<bullet> (equal_elim \<cdot> x3 \<cdot> x4 \<bullet>
81      (axm.symmetric \<cdot> TYPE('T2) \<cdot> x5 \<cdot> x6 \<bullet>
82        (combination \<cdot> TYPE('T) \<cdot> TYPE(prop) \<cdot> x7 \<cdot> x8 \<cdot> C \<cdot> D \<bullet>
83          (combination \<cdot> TYPE('T) \<cdot> TYPE('T3) \<cdot> (\<equiv>) \<cdot> (\<equiv>) \<cdot> A \<cdot> B \<bullet>
84            (axm.reflexive \<cdot> TYPE('T4) \<cdot> (\<equiv>)) \<bullet> prf1) \<bullet> prf2)) \<bullet> prf3)) \<equiv>
85    (iffD2 \<cdot> A = C \<cdot> B = D \<bullet>
86      (cong \<cdot> TYPE('T) \<cdot> TYPE(bool) \<cdot> (=) A \<cdot> (=) B \<cdot> C \<cdot> D \<bullet>
87        prfT \<bullet> arity_type_bool \<bullet>
88        (cong \<cdot> TYPE('T) \<cdot> TYPE('T\<Rightarrow>bool) \<cdot>
89          ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> A \<cdot> B \<bullet>
90          prfT \<bullet> (Pure.OfClass type_class \<cdot> TYPE('T\<Rightarrow>bool)) \<bullet>
91          (HOL.refl \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<bullet>
92             (Pure.OfClass type_class \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool))) \<bullet>
93          (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> A \<cdot> B \<bullet> prfT \<bullet> prf1)) \<bullet>
94        (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> C \<cdot> D \<bullet> prfT \<bullet> prf2)) \<bullet>
95      (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> B \<cdot> D \<bullet> prfT \<bullet> prf3))\<close>,
96
97   (** rewriting on bool: insert proper congruence rules for logical connectives **)
98
99   (* All *)
100
101   \<open>(iffD1 \<cdot> All P \<cdot> All Q \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> All \<cdot> All \<cdot> P \<cdot> Q \<bullet> prfT1 \<bullet> prfT2 \<bullet>
102      (HOL.refl \<cdot> TYPE('T3) \<cdot> x1 \<bullet> prfT3) \<bullet>
103      (ext \<cdot> TYPE('a) \<cdot> TYPE(bool) \<cdot> x2 \<cdot> x3 \<bullet> prfa \<bullet> prfb \<bullet> prf)) \<bullet> prf') \<equiv>
104    (allI \<cdot> TYPE('a) \<cdot> Q \<bullet> prfa \<bullet>
105      (\<^bold>\<lambda>x.
106          iffD1 \<cdot> P x \<cdot> Q x \<bullet> (prf \<cdot> x) \<bullet>
107           (spec \<cdot> TYPE('a) \<cdot> P \<cdot> x \<bullet> prfa \<bullet> prf')))\<close>,
108
109   \<open>(iffD2 \<cdot> All P \<cdot> All Q \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> All \<cdot> All \<cdot> P \<cdot> Q \<bullet> prfT1 \<bullet> prfT2 \<bullet>
110      (HOL.refl \<cdot> TYPE('T3) \<cdot> x1 \<bullet> prfT3) \<bullet>
111      (ext \<cdot> TYPE('a) \<cdot> TYPE(bool) \<cdot> x2 \<cdot> x3 \<bullet> prfa \<bullet> prfb \<bullet> prf)) \<bullet> prf') \<equiv>
112    (allI \<cdot> TYPE('a) \<cdot> P \<bullet> prfa \<bullet>
113      (\<^bold>\<lambda>x.
114          iffD2 \<cdot> P x \<cdot> Q x \<bullet> (prf \<cdot> x) \<bullet>
115           (spec \<cdot> TYPE('a) \<cdot> Q \<cdot> x \<bullet> prfa \<bullet> prf')))\<close>,
116
117   (* Ex *)
118
119   \<open>(iffD1 \<cdot> Ex P \<cdot> Ex Q \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> Ex \<cdot> Ex \<cdot> P \<cdot> Q \<bullet> prfT1 \<bullet> prfT2 \<bullet>
120      (HOL.refl \<cdot> TYPE('T3) \<cdot> x1 \<bullet> prfT3) \<bullet>
121      (ext \<cdot> TYPE('a) \<cdot> TYPE(bool) \<cdot> x2 \<cdot> x3 \<bullet> prfa \<bullet> prfb \<bullet> prf)) \<bullet> prf') \<equiv>
122    (exE \<cdot> TYPE('a) \<cdot> P \<cdot> \<exists>x. Q x \<bullet> prfa \<bullet> prf' \<bullet>
123      (\<^bold>\<lambda>x H : P x.
124          exI \<cdot> TYPE('a) \<cdot> Q \<cdot> x \<bullet> prfa \<bullet>
125           (iffD1 \<cdot> P x \<cdot> Q x \<bullet> (prf \<cdot> x) \<bullet> H)))\<close>,
126
127   \<open>(iffD2 \<cdot> Ex P \<cdot> Ex Q \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> Ex \<cdot> Ex \<cdot> P \<cdot> Q \<bullet> prfT1 \<bullet> prfT2 \<bullet>
128      (HOL.refl \<cdot> TYPE('T3) \<cdot> x1 \<bullet> prfT3) \<bullet>
129      (ext \<cdot> TYPE('a) \<cdot> TYPE(bool) \<cdot> x2 \<cdot> x3 \<bullet> prfa \<bullet> prfb \<bullet> prf)) \<bullet> prf') \<equiv>
130    (exE \<cdot> TYPE('a) \<cdot> Q \<cdot> \<exists>x. P x \<bullet> prfa \<bullet> prf' \<bullet>
131      (\<^bold>\<lambda>x H : Q x.
132          exI \<cdot> TYPE('a) \<cdot> P \<cdot> x \<bullet> prfa \<bullet>
133           (iffD2 \<cdot> P x \<cdot> Q x \<bullet> (prf \<cdot> x) \<bullet> H)))\<close>,
134
135   (* \<and> *)
136
137   \<open>(iffD1 \<cdot> A \<and> C \<cdot> B \<and> D \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfT1 \<bullet> prfT2 \<bullet>
138      (cong \<cdot> TYPE('T3) \<cdot> TYPE('T4) \<cdot> (\<and>) \<cdot> (\<and>) \<cdot> A \<cdot> B \<bullet> prfT3 \<bullet> prfT4 \<bullet>
139        (HOL.refl \<cdot> TYPE('T5) \<cdot> (\<and>) \<bullet> prfT5) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<equiv>
140    (conjI \<cdot> B \<cdot> D \<bullet>
141      (iffD1 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> (conjunct1 \<cdot> A \<cdot> C \<bullet> prf3)) \<bullet>
142      (iffD1 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet> (conjunct2 \<cdot> A \<cdot> C \<bullet> prf3)))\<close>,
143
144   \<open>(iffD2 \<cdot> A \<and> C \<cdot> B \<and> D \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfT1 \<bullet> prfT2 \<bullet>
145      (cong \<cdot> TYPE('T3) \<cdot> TYPE('T4) \<cdot> (\<and>) \<cdot> (\<and>) \<cdot> A \<cdot> B \<bullet> prfT3 \<bullet> prfT4 \<bullet>
146        (HOL.refl \<cdot> TYPE('T5) \<cdot> (\<and>) \<bullet> prfT5) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<equiv>
147    (conjI \<cdot> A \<cdot> C \<bullet>
148      (iffD2 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> (conjunct1 \<cdot> B \<cdot> D \<bullet> prf3)) \<bullet>
149      (iffD2 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet> (conjunct2 \<cdot> B \<cdot> D \<bullet> prf3)))\<close>,
150
151   \<open>(cong \<cdot> TYPE(bool) \<cdot> TYPE(bool) \<cdot> (\<and>) A \<cdot> (\<and>) A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prfb \<bullet>
152      (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool) \<cdot> (\<and>) A \<bullet> prfbb)) \<equiv>
153    (cong \<cdot> TYPE(bool) \<cdot> TYPE(bool) \<cdot> (\<and>) A \<cdot> (\<and>) A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prfb \<bullet>
154      (cong \<cdot> TYPE(bool) \<cdot> TYPE(bool\<Rightarrow>bool) \<cdot>
155        ((\<and>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<and>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
156          prfb \<bullet> prfbb \<bullet>
157          (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<and>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
158             (Pure.OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
159          (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
160
161   (* \<or> *)
162
163   \<open>(iffD1 \<cdot> A \<or> C \<cdot> B \<or> D \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfT1 \<bullet> prfT2 \<bullet>
164      (cong \<cdot> TYPE('T3) \<cdot> TYPE('T4) \<cdot> (\<or>) \<cdot> (\<or>) \<cdot> A \<cdot> B \<bullet> prfT3 \<bullet> prfT4 \<bullet>
165        (HOL.refl \<cdot> TYPE('T5) \<cdot> (\<or>) \<bullet> prfT5) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<equiv>
166    (disjE \<cdot> A \<cdot> C \<cdot> B \<or> D \<bullet> prf3 \<bullet>
167      (\<^bold>\<lambda>H : A. disjI1 \<cdot> B \<cdot> D \<bullet> (iffD1 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> H)) \<bullet>
168      (\<^bold>\<lambda>H : C. disjI2 \<cdot> D \<cdot> B \<bullet> (iffD1 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet> H)))\<close>,
169
170   \<open>(iffD2 \<cdot> A \<or> C \<cdot> B \<or> D \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfT1 \<bullet> prfT2 \<bullet>
171      (cong \<cdot> TYPE('T3) \<cdot> TYPE('T4) \<cdot> (\<or>) \<cdot> (\<or>) \<cdot> A \<cdot> B \<bullet> prfT3 \<bullet> prfT4 \<bullet>
172        (HOL.refl \<cdot> TYPE('T5) \<cdot> (\<or>) \<bullet> prfT5) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<equiv>
173    (disjE \<cdot> B \<cdot> D \<cdot> A \<or> C \<bullet> prf3 \<bullet>
174      (\<^bold>\<lambda>H : B. disjI1 \<cdot> A \<cdot> C \<bullet> (iffD2 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> H)) \<bullet>
175      (\<^bold>\<lambda>H : D. disjI2 \<cdot> C \<cdot> A \<bullet> (iffD2 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet> H)))\<close>,
176
177   \<open>(cong \<cdot> TYPE(bool) \<cdot> TYPE(bool) \<cdot> (\<or>) A \<cdot> (\<or>) A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prfb \<bullet>
178      (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool) \<cdot> (\<or>) A \<bullet> prfbb)) \<equiv>
179    (cong \<cdot> TYPE(bool) \<cdot> TYPE(bool) \<cdot> (\<or>) A \<cdot> (\<or>) A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prfb \<bullet>
180      (cong \<cdot> TYPE(bool) \<cdot> TYPE(bool\<Rightarrow>bool) \<cdot>
181        ((\<or>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<or>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
182          prfb \<bullet> prfbb \<bullet>
183          (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<or>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
184             (Pure.OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
185          (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
186
187   (* \<longrightarrow> *)
188
189   \<open>(iffD1 \<cdot> A \<longrightarrow> C \<cdot> B \<longrightarrow> D \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfT1 \<bullet> prfT2 \<bullet>
190      (cong \<cdot> TYPE('T3) \<cdot> TYPE('T4) \<cdot> (\<longrightarrow>) \<cdot> (\<longrightarrow>) \<cdot> A \<cdot> B \<bullet> prfT3 \<bullet> prfT4 \<bullet>
191        (HOL.refl \<cdot> TYPE('T5) \<cdot> (\<longrightarrow>) \<bullet> prfT5) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<equiv>
192    (impI \<cdot> B \<cdot> D \<bullet> (\<^bold>\<lambda>H: B. iffD1 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet>
193      (mp \<cdot> A \<cdot> C \<bullet> prf3 \<bullet> (iffD2 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> H))))\<close>,
194
195   \<open>(iffD2 \<cdot> A \<longrightarrow> C \<cdot> B \<longrightarrow> D \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfT1 \<bullet> prfT2 \<bullet>
196      (cong \<cdot> TYPE('T3) \<cdot> TYPE('T4) \<cdot> (\<longrightarrow>) \<cdot> (\<longrightarrow>) \<cdot> A \<cdot> B \<bullet> prfT3 \<bullet> prfT4 \<bullet>
197        (HOL.refl \<cdot> TYPE('T5) \<cdot> (\<longrightarrow>) \<bullet> prfT5) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<equiv>
198    (impI \<cdot> A \<cdot> C \<bullet> (\<^bold>\<lambda>H: A. iffD2 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet>
199      (mp \<cdot> B \<cdot> D \<bullet> prf3 \<bullet> (iffD1 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> H))))\<close>,
200
201   \<open>(cong \<cdot> TYPE(bool) \<cdot> TYPE(bool) \<cdot> (\<longrightarrow>) A \<cdot> (\<longrightarrow>) A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prfb \<bullet>
202      (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool) \<cdot> (\<longrightarrow>) A \<bullet> prfbb)) \<equiv>
203    (cong \<cdot> TYPE(bool) \<cdot> TYPE(bool) \<cdot> (\<longrightarrow>) A \<cdot> (\<longrightarrow>) A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prfb \<bullet>
204      (cong \<cdot> TYPE(bool) \<cdot> TYPE(bool\<Rightarrow>bool) \<cdot>
205        ((\<longrightarrow>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<longrightarrow>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
206          prfb \<bullet> prfbb \<bullet>
207          (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<longrightarrow>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
208             (Pure.OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
209          (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
210
211   (* \<not> *)
212
213   \<open>(iffD1 \<cdot> \<not> P \<cdot> \<not> Q \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> Not \<cdot> Not \<cdot> P \<cdot> Q \<bullet> prfT1 \<bullet> prfT2 \<bullet>
214      (HOL.refl \<cdot> TYPE('T3) \<cdot> Not \<bullet> prfT3) \<bullet> prf1) \<bullet> prf2) \<equiv>
215    (notI \<cdot> Q \<bullet> (\<^bold>\<lambda>H: Q.
216      notE \<cdot> P \<cdot> False \<bullet> prf2 \<bullet> (iffD2 \<cdot> P \<cdot> Q \<bullet> prf1 \<bullet> H)))\<close>,
217
218   \<open>(iffD2 \<cdot> \<not> P \<cdot> \<not> Q \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> Not \<cdot> Not \<cdot> P \<cdot> Q \<bullet> prfT1 \<bullet> prfT2 \<bullet>
219      (HOL.refl \<cdot> TYPE('T3) \<cdot> Not \<bullet> prfT3) \<bullet> prf1) \<bullet> prf2) \<equiv>
220    (notI \<cdot> P \<bullet> (\<^bold>\<lambda>H: P.
221      notE \<cdot> Q \<cdot> False \<bullet> prf2 \<bullet> (iffD1 \<cdot> P \<cdot> Q \<bullet> prf1 \<bullet> H)))\<close>,
222
223   (* = *)
224
225   \<open>(iffD1 \<cdot> B \<cdot> D \<bullet>
226      (iffD1 \<cdot> A = C \<cdot> B = D \<bullet> (cong \<cdot> TYPE(bool) \<cdot> TYPE('T1) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfb \<bullet> prfT1 \<bullet>
227        (cong \<cdot> TYPE(bool) \<cdot> TYPE('T2) \<cdot> (=) \<cdot> (=) \<cdot> A \<cdot> B \<bullet> prfb \<bullet> prfT2 \<bullet>
228          (HOL.refl \<cdot> TYPE('T3) \<cdot> (=) \<bullet> prfT3) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<bullet> prf4) \<equiv>
229    (iffD1 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet>
230      (iffD1 \<cdot> A \<cdot> C \<bullet> prf3 \<bullet> (iffD2 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> prf4)))\<close>,
231
232   \<open>(iffD2 \<cdot> B \<cdot> D \<bullet>
233      (iffD1 \<cdot> A = C \<cdot> B = D \<bullet> (cong \<cdot> TYPE(bool) \<cdot> TYPE('T1) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfb \<bullet> prfT1 \<bullet>
234        (cong \<cdot> TYPE(bool) \<cdot> TYPE('T2) \<cdot> (=) \<cdot> (=) \<cdot> A \<cdot> B \<bullet> prfb \<bullet> prfT2 \<bullet>
235          (HOL.refl \<cdot> TYPE('T3) \<cdot> (=) \<bullet> prfT3) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<bullet> prf4) \<equiv>
236    (iffD1 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet>
237      (iffD2 \<cdot> A \<cdot> C \<bullet> prf3 \<bullet> (iffD2 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet> prf4)))\<close>,
238
239   \<open>(iffD1 \<cdot> A \<cdot> C \<bullet>
240      (iffD2 \<cdot> A = C \<cdot> B = D \<bullet> (cong \<cdot> TYPE(bool) \<cdot> TYPE('T1) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfb \<bullet> prfT1 \<bullet>
241        (cong \<cdot> TYPE(bool) \<cdot> TYPE('T2) \<cdot> (=) \<cdot> (=) \<cdot> A \<cdot> B \<bullet> prfb \<bullet> prfT2 \<bullet>
242          (HOL.refl \<cdot> TYPE('T3) \<cdot> (=) \<bullet> prfT3) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<bullet> prf4)\<equiv>
243    (iffD2 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet>
244      (iffD1 \<cdot> B \<cdot> D \<bullet> prf3 \<bullet> (iffD1 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> prf4)))\<close>,
245
246   \<open>(iffD2 \<cdot> A \<cdot> C \<bullet>
247      (iffD2 \<cdot> A = C \<cdot> B = D \<bullet> (cong \<cdot> TYPE(bool) \<cdot> TYPE('T1) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfb \<bullet> prfT1 \<bullet>
248        (cong \<cdot> TYPE(bool) \<cdot> TYPE('T2) \<cdot> (=) \<cdot> (=) \<cdot> A \<cdot> B \<bullet> prfb \<bullet> prfT2 \<bullet>
249          (HOL.refl \<cdot> TYPE('T3) \<cdot> (=) \<bullet> prfT3) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<bullet> prf4) \<equiv>
250    (iffD2 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet>
251      (iffD2 \<cdot> B \<cdot> D \<bullet> prf3 \<bullet> (iffD1 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet> prf4)))\<close>,
252
253   \<open>(cong \<cdot> TYPE(bool) \<cdot> TYPE(bool) \<cdot> (=) A \<cdot> (=) A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prfb \<bullet>
254      (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool) \<cdot> (=) A \<bullet> prfbb)) \<equiv>
255    (cong \<cdot> TYPE(bool) \<cdot> TYPE(bool) \<cdot> (=) A \<cdot> (=) A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prfb \<bullet>
256      (cong \<cdot> TYPE(bool) \<cdot> TYPE(bool\<Rightarrow>bool) \<cdot>
257        ((=) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((=) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
258          prfb \<bullet> prfbb \<bullet>
259          (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((=) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
260             (Pure.OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
261          (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
262
263   (** transitivity, reflexivity, and symmetry **)
264
265   \<open>(iffD1 \<cdot> A \<cdot> C \<bullet> (HOL.trans \<cdot> TYPE(bool) \<cdot> A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prf1 \<bullet> prf2) \<bullet> prf3) \<equiv>
266    (iffD1 \<cdot> B \<cdot> C \<bullet> prf2 \<bullet> (iffD1 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> prf3))\<close>,
267
268   \<open>(iffD2 \<cdot> A \<cdot> C \<bullet> (HOL.trans \<cdot> TYPE(bool) \<cdot> A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prf1 \<bullet> prf2) \<bullet> prf3) \<equiv>
269    (iffD2 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> (iffD2 \<cdot> B \<cdot> C \<bullet> prf2 \<bullet> prf3))\<close>,
270
271   \<open>(iffD1 \<cdot> A \<cdot> A \<bullet> (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb) \<bullet> prf) \<equiv> prf\<close>,
272
273   \<open>(iffD2 \<cdot> A \<cdot> A \<bullet> (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb) \<bullet> prf) \<equiv> prf\<close>,
274
275   \<open>(iffD1 \<cdot> A \<cdot> B \<bullet> (sym \<cdot> TYPE(bool) \<cdot> B \<cdot> A \<bullet> prfb \<bullet> prf)) \<equiv> (iffD2 \<cdot> B \<cdot> A \<bullet> prf)\<close>,
276
277   \<open>(iffD2 \<cdot> A \<cdot> B \<bullet> (sym \<cdot> TYPE(bool) \<cdot> B \<cdot> A \<bullet> prfb \<bullet> prf)) \<equiv> (iffD1 \<cdot> B \<cdot> A \<bullet> prf)\<close>,
278
279   (** normalization of HOL proofs **)
280
281   \<open>(mp \<cdot> A \<cdot> B \<bullet> (impI \<cdot> A \<cdot> B \<bullet> prf)) \<equiv> prf\<close>,
282
283   \<open>(impI \<cdot> A \<cdot> B \<bullet> (mp \<cdot> A \<cdot> B \<bullet> prf)) \<equiv> prf\<close>,
284
285   \<open>(spec \<cdot> TYPE('a) \<cdot> P \<cdot> x \<bullet> prfa \<bullet> (allI \<cdot> TYPE('a) \<cdot> P \<bullet> prfa \<bullet> prf)) \<equiv> prf \<cdot> x\<close>,
286
287   \<open>(allI \<cdot> TYPE('a) \<cdot> P \<bullet> prfa \<bullet> (\<^bold>\<lambda>x::'a. spec \<cdot> TYPE('a) \<cdot> P \<cdot> x \<bullet> prfa \<bullet> prf)) \<equiv> prf\<close>,
288
289   \<open>(exE \<cdot> TYPE('a) \<cdot> P \<cdot> Q \<bullet> prfa \<bullet> (exI \<cdot> TYPE('a) \<cdot> P \<cdot> x \<bullet> prfa \<bullet> prf1) \<bullet> prf2) \<equiv> (prf2 \<cdot> x \<bullet> prf1)\<close>,
290
291   \<open>(exE \<cdot> TYPE('a) \<cdot> P \<cdot> Q \<bullet> prfa \<bullet> prf \<bullet> (exI \<cdot> TYPE('a) \<cdot> P \<bullet> prfa)) \<equiv> prf\<close>,
292
293   \<open>(disjE \<cdot> P \<cdot> Q \<cdot> R \<bullet> (disjI1 \<cdot> P \<cdot> Q \<bullet> prf1) \<bullet> prf2 \<bullet> prf3) \<equiv> (prf2 \<bullet> prf1)\<close>,
294
295   \<open>(disjE \<cdot> P \<cdot> Q \<cdot> R \<bullet> (disjI2 \<cdot> Q \<cdot> P \<bullet> prf1) \<bullet> prf2 \<bullet> prf3) \<equiv> (prf3 \<bullet> prf1)\<close>,
296
297   \<open>(conjunct1 \<cdot> P \<cdot> Q \<bullet> (conjI \<cdot> P \<cdot> Q \<bullet> prf1 \<bullet> prf2)) \<equiv> prf1\<close>,
298
299   \<open>(conjunct2 \<cdot> P \<cdot> Q \<bullet> (conjI \<cdot> P \<cdot> Q \<bullet> prf1 \<bullet> prf2)) \<equiv> prf2\<close>,
300
301   \<open>(iffD1 \<cdot> A \<cdot> B \<bullet> (iffI \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> prf2)) \<equiv> prf1\<close>,
302
303   \<open>(iffD2 \<cdot> A \<cdot> B \<bullet> (iffI \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> prf2)) \<equiv> prf2\<close>];
304
305
306(** Replace congruence rules by substitution rules **)
307
308fun strip_cong ps (PThm ({name = "HOL.cong", ...}, _) % _ % _ % SOME x % SOME y %%
309      prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1
310  | strip_cong ps (PThm ({name = "HOL.refl", ...}, _) % SOME f %% _) = SOME (f, ps)
311  | strip_cong _ _ = NONE;
312
313val subst_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of @{thm subst}))));
314val sym_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of@{thm sym}))));
315
316fun make_subst Ts prf xs (_, []) = prf
317  | make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) =
318      let val T = fastype_of1 (Ts, x)
319      in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
320        else Proofterm.change_types (SOME [T]) subst_prf %> x %> y %>
321          Abs ("z", T, list_comb (incr_boundvars 1 f,
322            map (incr_boundvars 1) xs @ Bound 0 ::
323            map (incr_boundvars 1 o snd o fst) ps)) %% clprf %% prf' %%
324          make_subst Ts prf (xs @ [x]) (f, ps)
325      end;
326
327fun make_sym Ts ((x, y), (prf, clprf)) =
328  ((y, x),
329    (Proofterm.change_types (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
330
331fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
332
333fun elim_cong_aux Ts (PThm ({name = "HOL.iffD1", ...}, _) % _ % _ %% prf1 %% prf2) =
334      Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
335  | elim_cong_aux Ts (PThm ({name = "HOL.iffD1", ...}, _) % P % _ %% prf) =
336      Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
337        (strip_cong [] (Proofterm.incr_pboundvars 1 0 prf))
338  | elim_cong_aux Ts (PThm ({name = "HOL.iffD2", ...}, _) % _ % _ %% prf1 %% prf2) =
339      Option.map (make_subst Ts prf2 [] o
340        apsnd (map (make_sym Ts))) (strip_cong [] prf1)
341  | elim_cong_aux Ts (PThm ({name = "HOL.iffD2", ...}, _) % _ % P %% prf) =
342      Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
343        apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_pboundvars 1 0 prf))
344  | elim_cong_aux _ _ = NONE;
345
346fun elim_cong Ts hs prf = Option.map (rpair Proofterm.no_skel) (elim_cong_aux Ts prf);
347
348end;
349