13404
|
1 |
(* Title: HOL/Tools/rewrite_hol_proof.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Stefan Berghofer, TU Muenchen
|
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
|
5 |
|
|
6 |
Rewrite rules for HOL proofs
|
|
7 |
*)
|
|
8 |
|
|
9 |
signature REWRITE_HOL_PROOF =
|
|
10 |
sig
|
|
11 |
val rews: (Proofterm.proof * Proofterm.proof) list
|
|
12 |
val elim_cong: typ list -> Proofterm.proof -> Proofterm.proof option
|
|
13 |
end;
|
|
14 |
|
|
15 |
structure RewriteHOLProof : REWRITE_HOL_PROOF =
|
|
16 |
struct
|
|
17 |
|
|
18 |
open Proofterm;
|
|
19 |
|
|
20 |
val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) Symtab.empty true) o
|
|
21 |
Logic.dest_equals o Logic.varify o ProofSyntax.read_term (the_context ()) propT)
|
|
22 |
|
|
23 |
(** eliminate meta-equality rules **)
|
|
24 |
|
|
25 |
["(equal_elim % x1 % x2 %% \
|
|
26 |
\ (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %% \
|
|
27 |
\ (axm.reflexive % TYPE('T3) % x4) %% prf1) %% prf2) == \
|
|
28 |
\ (iffD1 % A % B %% \
|
|
29 |
\ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1) %% prf2)",
|
|
30 |
|
|
31 |
"(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %% \
|
|
32 |
\ (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %% \
|
|
33 |
\ (axm.reflexive % TYPE('T4) % x6) %% prf1)) %% prf2) == \
|
|
34 |
\ (iffD2 % A % B %% \
|
|
35 |
\ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1) %% prf2)",
|
|
36 |
|
|
37 |
"(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% \
|
|
38 |
\ (combination % TYPE('U) % TYPE('T) % f % g % x % y %% prf1 %% prf2)) == \
|
|
39 |
\ (cong % TYPE('U) % TYPE('T) % f % g % x % y %% \
|
|
40 |
\ (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% prf1) %% \
|
|
41 |
\ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf2))",
|
|
42 |
|
|
43 |
"(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% \
|
|
44 |
\ (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) == \
|
|
45 |
\ (trans % TYPE('T) % x % y % z %% \
|
|
46 |
\ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf1) %% \
|
|
47 |
\ (meta_eq_to_obj_eq % TYPE('T) % y % z %% prf2))",
|
|
48 |
|
|
49 |
"(meta_eq_to_obj_eq % TYPE('T) % x % x %% (axm.reflexive % TYPE('T) % x)) == \
|
|
50 |
\ (refl % TYPE('T) % x)",
|
|
51 |
|
|
52 |
"(meta_eq_to_obj_eq % TYPE('T) % x % y %% \
|
|
53 |
\ (axm.symmetric % TYPE('T) % x % y %% prf)) == \
|
|
54 |
\ (sym % TYPE('T) % x % y %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf))",
|
|
55 |
|
|
56 |
"(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% \
|
|
57 |
\ (abstract_rule % TYPE('U) % TYPE('T) % f % g %% prf)) == \
|
|
58 |
\ (ext % TYPE('U) % TYPE('T) % f % g %% \
|
|
59 |
\ (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% (prf % x)))",
|
|
60 |
|
|
61 |
"(meta_eq_to_obj_eq % TYPE('T) % x % y %% \
|
|
62 |
\ (eq_reflection % TYPE('T) % x % y %% prf)) == prf",
|
|
63 |
|
|
64 |
"(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \
|
|
65 |
\ (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %% \
|
|
66 |
\ (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %% \
|
|
67 |
\ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) == \
|
|
68 |
\ (iffD1 % A = C % B = D %% \
|
|
69 |
\ (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %% \
|
|
70 |
\ (cong % TYPE('T=>bool) % TYPE('T) % \
|
|
71 |
\ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \
|
|
72 |
\ (refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \
|
|
73 |
\ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \
|
|
74 |
\ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \
|
|
75 |
\ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))",
|
|
76 |
|
|
77 |
"(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \
|
|
78 |
\ (axm.symmetric % TYPE('T2) % x5 % x6 %% \
|
|
79 |
\ (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %% \
|
|
80 |
\ (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %% \
|
|
81 |
\ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) == \
|
|
82 |
\ (iffD2 % A = C % B = D %% \
|
|
83 |
\ (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %% \
|
|
84 |
\ (cong % TYPE('T=>bool) % TYPE('T) % \
|
|
85 |
\ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \
|
|
86 |
\ (refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \
|
|
87 |
\ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \
|
|
88 |
\ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \
|
|
89 |
\ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))",
|
|
90 |
|
|
91 |
(** rewriting on bool: insert proper congruence rules for logical connectives **)
|
|
92 |
|
|
93 |
(* All *)
|
|
94 |
|
|
95 |
"(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \
|
|
96 |
\ (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \
|
|
97 |
\ (allI % TYPE('a) % Q %% \
|
|
98 |
\ (Lam x. \
|
|
99 |
\ iffD1 % P x % Q x %% (prf % x) %% \
|
|
100 |
\ (spec % TYPE('a) % P % x %% prf')))",
|
|
101 |
|
|
102 |
"(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \
|
|
103 |
\ (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \
|
|
104 |
\ (allI % TYPE('a) % P %% \
|
|
105 |
\ (Lam x. \
|
|
106 |
\ iffD2 % P x % Q x %% (prf % x) %% \
|
|
107 |
\ (spec % TYPE('a) % ?Q % x %% prf')))",
|
|
108 |
|
|
109 |
(* Ex *)
|
|
110 |
|
|
111 |
"(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \
|
|
112 |
\ (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \
|
|
113 |
\ (exE % TYPE('a) % P % EX x. Q x %% prf' %% \
|
|
114 |
\ (Lam x H : P x. \
|
|
115 |
\ exI % TYPE('a) % Q % x %% \
|
|
116 |
\ (iffD1 % P x % Q x %% (prf % x) %% H)))",
|
|
117 |
|
|
118 |
"(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \
|
|
119 |
\ (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \
|
|
120 |
\ (exE % TYPE('a) % Q % EX x. P x %% prf' %% \
|
|
121 |
\ (Lam x H : Q x. \
|
|
122 |
\ exI % TYPE('a) % P % x %% \
|
|
123 |
\ (iffD2 % P x % Q x %% (prf % x) %% H)))",
|
|
124 |
|
|
125 |
(* & *)
|
|
126 |
|
|
127 |
"(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
|
|
128 |
\ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% \
|
|
129 |
\ (refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) == \
|
|
130 |
\ (conjI % B % D %% \
|
|
131 |
\ (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %% \
|
|
132 |
\ (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))",
|
|
133 |
|
|
134 |
"(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
|
|
135 |
\ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% \
|
|
136 |
\ (refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) == \
|
|
137 |
\ (conjI % A % C %% \
|
|
138 |
\ (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %% \
|
|
139 |
\ (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
|
|
140 |
|
|
141 |
(* | *)
|
|
142 |
|
|
143 |
"(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
|
|
144 |
\ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% \
|
|
145 |
\ (refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) == \
|
|
146 |
\ (disjE % A % C % B | D %% prf3 %% \
|
|
147 |
\ (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %% \
|
|
148 |
\ (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))",
|
|
149 |
|
|
150 |
"(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
|
|
151 |
\ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% \
|
|
152 |
\ (refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) == \
|
|
153 |
\ (disjE % B % D % A | C %% prf3 %% \
|
|
154 |
\ (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %% \
|
|
155 |
\ (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
|
|
156 |
|
|
157 |
(* --> *)
|
|
158 |
|
|
159 |
"(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
|
|
160 |
\ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% \
|
|
161 |
\ (refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) == \
|
|
162 |
\ (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %% \
|
|
163 |
\ (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))",
|
|
164 |
|
|
165 |
"(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
|
|
166 |
\ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% \
|
|
167 |
\ (refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) == \
|
|
168 |
\ (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %% \
|
|
169 |
\ (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
|
|
170 |
|
|
171 |
(* ~ *)
|
|
172 |
|
|
173 |
"(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% \
|
|
174 |
\ (refl % TYPE('T3) % Not) %% prf1) %% prf2) == \
|
|
175 |
\ (notI % Q %% (Lam H: Q. \
|
|
176 |
\ notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))",
|
|
177 |
|
|
178 |
"(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% \
|
|
179 |
\ (refl % TYPE('T3) % Not) %% prf1) %% prf2) == \
|
|
180 |
\ (notI % P %% (Lam H: P. \
|
|
181 |
\ notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))",
|
|
182 |
|
|
183 |
(* = *)
|
|
184 |
|
|
185 |
"(iffD1 % B % D %% \
|
|
186 |
\ (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \
|
|
187 |
\ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \
|
|
188 |
\ (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
|
|
189 |
\ (iffD1 % C % D %% prf2 %% \
|
|
190 |
\ (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
|
|
191 |
|
|
192 |
"(iffD2 % B % D %% \
|
|
193 |
\ (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \
|
|
194 |
\ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \
|
|
195 |
\ (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
|
|
196 |
\ (iffD1 % A % B %% prf1 %% \
|
|
197 |
\ (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
|
|
198 |
|
|
199 |
"(iffD1 % A % C %% \
|
|
200 |
\ (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \
|
|
201 |
\ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \
|
|
202 |
\ (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)== \
|
|
203 |
\ (iffD2 % C % D %% prf2 %% \
|
|
204 |
\ (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
|
|
205 |
|
|
206 |
"(iffD2 % A % C %% \
|
|
207 |
\ (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \
|
|
208 |
\ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \
|
|
209 |
\ (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
|
|
210 |
\ (iffD2 % A % B %% prf1 %% \
|
|
211 |
\ (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
|
|
212 |
|
|
213 |
"(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \
|
|
214 |
\ (refl % TYPE(bool) % op = A)) == \
|
|
215 |
\ (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \
|
|
216 |
\ (cong % TYPE(bool=>bool) % TYPE(bool) % \
|
|
217 |
\ (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %% \
|
|
218 |
\ (refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %% \
|
|
219 |
\ (refl % TYPE(bool) % A % A)))",
|
|
220 |
|
|
221 |
"(iffD1 % A % C %% (trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) == \
|
|
222 |
\ (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
|
|
223 |
|
|
224 |
"(iffD2 % A % C %% (trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) == \
|
|
225 |
\ (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))",
|
|
226 |
|
|
227 |
"(iffD1 % A % A %% (refl % TYPE(bool) % A) %% prf) == prf",
|
|
228 |
|
|
229 |
"(iffD2 % A % A %% (refl % TYPE(bool) % A) %% prf) == prf",
|
|
230 |
|
|
231 |
(** normalization of HOL proofs **)
|
|
232 |
|
|
233 |
"(mp % A % B %% (impI % A % B %% prf)) == prf",
|
|
234 |
|
|
235 |
"(impI % A % B %% (mp % A % B %% prf)) == prf",
|
|
236 |
|
|
237 |
"(spec % TYPE('a) % P % x %% (allI % TYPE('a) % P %% prf)) == prf % x",
|
|
238 |
|
|
239 |
"(allI % TYPE('a) % P %% (Lam x::'a. spec % TYPE('a) % P % x %% prf)) == prf",
|
|
240 |
|
|
241 |
"(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)",
|
|
242 |
|
|
243 |
"(disjE % P % Q % R %% (disjI2 % Q % P %% prf1) %% prf2 %% prf3) == (prf3 %% prf1)",
|
|
244 |
|
|
245 |
"(conjunct1 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf1",
|
|
246 |
|
|
247 |
"(conjunct2 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf2",
|
|
248 |
|
|
249 |
"(iffD1 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf1",
|
|
250 |
|
|
251 |
"(iffD2 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf2"];
|
|
252 |
|
|
253 |
|
|
254 |
(** Replace congruence rules by substitution rules **)
|
|
255 |
|
|
256 |
fun strip_cong ps (PThm (("HOL.cong", _), _, _, _) % _ % _ % Some x % Some y %%
|
|
257 |
prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1
|
|
258 |
| strip_cong ps (PThm (("HOL.refl", _), _, _, _) % Some f) = Some (f, ps)
|
|
259 |
| strip_cong _ _ = None;
|
|
260 |
|
|
261 |
val subst_prf = fst (strip_combt (#2 (#der (rep_thm subst))));
|
|
262 |
val sym_prf = fst (strip_combt (#2 (#der (rep_thm sym))));
|
|
263 |
|
|
264 |
fun make_subst Ts prf xs (_, []) = prf
|
|
265 |
| make_subst Ts prf xs (f, ((x, y), prf') :: ps) =
|
|
266 |
let val T = fastype_of1 (Ts, x)
|
|
267 |
in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
|
|
268 |
else change_type (Some [T]) subst_prf %> x %> y %>
|
|
269 |
Abs ("z", T, list_comb (incr_boundvars 1 f,
|
|
270 |
map (incr_boundvars 1) xs @ Bound 0 ::
|
|
271 |
map (incr_boundvars 1 o snd o fst) ps)) %% prf' %%
|
|
272 |
make_subst Ts prf (xs @ [x]) (f, ps)
|
|
273 |
end;
|
|
274 |
|
|
275 |
fun make_sym Ts ((x, y), prf) =
|
|
276 |
((y, x), change_type (Some [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf);
|
|
277 |
|
|
278 |
fun elim_cong Ts (PThm (("HOL.iffD1", _), _, _, _) % _ % _ %% prf1 %% prf2) =
|
|
279 |
apsome (make_subst Ts prf2 []) (strip_cong [] prf1)
|
|
280 |
| elim_cong Ts (PThm (("HOL.iffD2", _), _, _, _) % _ % _ %% prf1 %% prf2) =
|
|
281 |
apsome (make_subst Ts prf2 [] o
|
|
282 |
apsnd (map (make_sym Ts))) (strip_cong [] prf1)
|
|
283 |
| elim_cong _ _ = None;
|
|
284 |
|
|
285 |
end;
|