1 (* Title: HOL/Tools/rewrite_hol_proof.ML
2 Author: Stefan Berghofer, TU Muenchen
4 Rewrite rules for HOL proofs
7 signature REWRITE_HOL_PROOF =
9 val rews: (Proofterm.proof * Proofterm.proof) list
10 val elim_cong: typ list -> Proofterm.proof -> Proofterm.proof option
13 structure RewriteHOLProof : REWRITE_HOL_PROOF =
18 val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) true) o
19 Logic.dest_equals o Logic.varify o ProofSyntax.read_term (the_context ()) propT)
21 (** eliminate meta-equality rules **)
23 ["(equal_elim % x1 % x2 %% \
24 \ (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %% \
25 \ (axm.reflexive % TYPE('T3) % x4) %% prf1)) == \
27 \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
29 "(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %% \
30 \ (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %% \
31 \ (axm.reflexive % TYPE('T4) % x6) %% prf1))) == \
33 \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
35 "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% \
36 \ (combination % TYPE('U) % TYPE('T) % f % g % x % y %% prf1 %% prf2)) == \
37 \ (cong % TYPE('U) % TYPE('T) % f % g % x % y %% \
38 \ (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% prf1) %% \
39 \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf2))",
41 "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% \
42 \ (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) == \
43 \ (HOL.trans % TYPE('T) % x % y % z %% \
44 \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf1) %% \
45 \ (meta_eq_to_obj_eq % TYPE('T) % y % z %% prf2))",
47 "(meta_eq_to_obj_eq % TYPE('T) % x % x %% (axm.reflexive % TYPE('T) % x)) == \
48 \ (HOL.refl % TYPE('T) % x)",
50 "(meta_eq_to_obj_eq % TYPE('T) % x % y %% \
51 \ (axm.symmetric % TYPE('T) % x % y %% prf)) == \
52 \ (sym % TYPE('T) % x % y %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf))",
54 "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% \
55 \ (abstract_rule % TYPE('U) % TYPE('T) % f % g %% prf)) == \
56 \ (ext % TYPE('U) % TYPE('T) % f % g %% \
57 \ (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% (prf % x)))",
59 "(meta_eq_to_obj_eq % TYPE('T) % x % y %% \
60 \ (eq_reflection % TYPE('T) % x % y %% prf)) == prf",
62 "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \
63 \ (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %% \
64 \ (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %% \
65 \ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) == \
66 \ (iffD1 % A = C % B = D %% \
67 \ (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %% \
68 \ (cong % TYPE('T=>bool) % TYPE('T) % \
69 \ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \
70 \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \
71 \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \
72 \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \
73 \ (meta_eq_to_obj_eq % TYPE('T) % A % C %% prf3))",
75 "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \
76 \ (axm.symmetric % TYPE('T2) % x5 % x6 %% \
77 \ (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %% \
78 \ (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %% \
79 \ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) == \
80 \ (iffD2 % A = C % B = D %% \
81 \ (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %% \
82 \ (cong % TYPE('T=>bool) % TYPE('T) % \
83 \ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \
84 \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \
85 \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \
86 \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \
87 \ (meta_eq_to_obj_eq % TYPE('T) % B % D %% prf3))",
89 (** rewriting on bool: insert proper congruence rules for logical connectives **)
93 "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \
94 \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \
95 \ (allI % TYPE('a) % Q %% \
97 \ iffD1 % P x % Q x %% (prf % x) %% \
98 \ (spec % TYPE('a) % P % x %% prf')))",
100 "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \
101 \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \
102 \ (allI % TYPE('a) % P %% \
104 \ iffD2 % P x % Q x %% (prf % x) %% \
105 \ (spec % TYPE('a) % Q % x %% prf')))",
109 "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \
110 \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \
111 \ (exE % TYPE('a) % P % EX x. Q x %% prf' %% \
113 \ exI % TYPE('a) % Q % x %% \
114 \ (iffD1 % P x % Q x %% (prf % x) %% H)))",
116 "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \
117 \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \
118 \ (exE % TYPE('a) % Q % EX x. P x %% prf' %% \
120 \ exI % TYPE('a) % P % x %% \
121 \ (iffD2 % P x % Q x %% (prf % x) %% H)))",
125 "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
126 \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% \
127 \ (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) == \
128 \ (conjI % B % D %% \
129 \ (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %% \
130 \ (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))",
132 "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
133 \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% \
134 \ (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) == \
135 \ (conjI % A % C %% \
136 \ (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %% \
137 \ (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
139 "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% \
140 \ (HOL.refl % TYPE(bool=>bool) % op & A)) == \
141 \ (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% \
142 \ (cong % TYPE(bool=>bool) % TYPE(bool) % \
143 \ (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %% \
144 \ (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %% \
145 \ (HOL.refl % TYPE(bool) % A)))",
149 "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
150 \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% \
151 \ (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) == \
152 \ (disjE % A % C % B | D %% prf3 %% \
153 \ (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %% \
154 \ (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))",
156 "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
157 \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% \
158 \ (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) == \
159 \ (disjE % B % D % A | C %% prf3 %% \
160 \ (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %% \
161 \ (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
163 "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% \
164 \ (HOL.refl % TYPE(bool=>bool) % op | A)) == \
165 \ (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% \
166 \ (cong % TYPE(bool=>bool) % TYPE(bool) % \
167 \ (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %% \
168 \ (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %% \
169 \ (HOL.refl % TYPE(bool) % A)))",
173 "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
174 \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% \
175 \ (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) == \
176 \ (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %% \
177 \ (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))",
179 "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
180 \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% \
181 \ (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) == \
182 \ (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %% \
183 \ (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
185 "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% \
186 \ (HOL.refl % TYPE(bool=>bool) % op --> A)) == \
187 \ (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% \
188 \ (cong % TYPE(bool=>bool) % TYPE(bool) % \
189 \ (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %% \
190 \ (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %% \
191 \ (HOL.refl % TYPE(bool) % A)))",
195 "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% \
196 \ (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) == \
197 \ (notI % Q %% (Lam H: Q. \
198 \ notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))",
200 "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% \
201 \ (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) == \
202 \ (notI % P %% (Lam H: P. \
203 \ notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))",
208 \ (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \
209 \ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \
210 \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
211 \ (iffD1 % C % D %% prf2 %% \
212 \ (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
215 \ (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \
216 \ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \
217 \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
218 \ (iffD1 % A % B %% prf1 %% \
219 \ (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
222 \ (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \
223 \ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \
224 \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)== \
225 \ (iffD2 % C % D %% prf2 %% \
226 \ (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
229 \ (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \
230 \ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \
231 \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
232 \ (iffD2 % A % B %% prf1 %% \
233 \ (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
235 "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \
236 \ (HOL.refl % TYPE(bool=>bool) % op = A)) == \
237 \ (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \
238 \ (cong % TYPE(bool=>bool) % TYPE(bool) % \
239 \ (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %% \
240 \ (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %% \
241 \ (HOL.refl % TYPE(bool) % A)))",
243 (** transitivity, reflexivity, and symmetry **)
245 "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) == \
246 \ (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
248 "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) == \
249 \ (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))",
251 "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
253 "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
255 "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD2 % B % A %% prf)",
257 "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD1 % B % A %% prf)",
259 (** normalization of HOL proofs **)
261 "(mp % A % B %% (impI % A % B %% prf)) == prf",
263 "(impI % A % B %% (mp % A % B %% prf)) == prf",
265 "(spec % TYPE('a) % P % x %% (allI % TYPE('a) % P %% prf)) == prf % x",
267 "(allI % TYPE('a) % P %% (Lam x::'a. spec % TYPE('a) % P % x %% prf)) == prf",
269 "(exE % TYPE('a) % P % Q %% (exI % TYPE('a) % P % x %% prf1) %% prf2) == (prf2 % x %% prf1)",
271 "(exE % TYPE('a) % P % Q %% prf %% (exI % TYPE('a) % P)) == prf",
273 "(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)",
275 "(disjE % P % Q % R %% (disjI2 % Q % P %% prf1) %% prf2 %% prf3) == (prf3 %% prf1)",
277 "(conjunct1 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf1",
279 "(conjunct2 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf2",
281 "(iffD1 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf1",
283 "(iffD2 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf2"];
286 (** Replace congruence rules by substitution rules **)
288 fun strip_cong ps (PThm (_, (("HOL.cong", _, _), _)) % _ % _ % SOME x % SOME y %%
289 prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1
290 | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f) = SOME (f, ps)
291 | strip_cong _ _ = NONE;
293 val subst_prf = fst (strip_combt (Thm.proof_of subst));
294 val sym_prf = fst (strip_combt (Thm.proof_of sym));
296 fun make_subst Ts prf xs (_, []) = prf
297 | make_subst Ts prf xs (f, ((x, y), prf') :: ps) =
298 let val T = fastype_of1 (Ts, x)
299 in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
300 else change_type (SOME [T]) subst_prf %> x %> y %>
301 Abs ("z", T, list_comb (incr_boundvars 1 f,
302 map (incr_boundvars 1) xs @ Bound 0 ::
303 map (incr_boundvars 1 o snd o fst) ps)) %% prf' %%
304 make_subst Ts prf (xs @ [x]) (f, ps)
307 fun make_sym Ts ((x, y), prf) =
308 ((y, x), change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf);
310 fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
312 fun elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) =
313 Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
314 | elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
315 Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
316 (strip_cong [] (incr_pboundvars 1 0 prf))
317 | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
318 Option.map (make_subst Ts prf2 [] o
319 apsnd (map (make_sym Ts))) (strip_cong [] prf1)
320 | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
321 Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
322 apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
323 | elim_cong _ _ = NONE;