author | wenzelm |
Wed, 15 Jul 2009 23:48:21 +0200 | |
changeset 32010 | cb1a1c94b4cd |
parent 30850 | 5e20f9c20086 |
child 33388 | d64545e6cba5 |
permissions | -rw-r--r-- |
13404 | 1 |
(* Title: HOL/Tools/rewrite_hol_proof.ML |
2 |
Author: Stefan Berghofer, TU Muenchen |
|
3 |
||
4 |
Rewrite rules for HOL proofs |
|
5 |
*) |
|
6 |
||
7 |
signature REWRITE_HOL_PROOF = |
|
8 |
sig |
|
9 |
val rews: (Proofterm.proof * Proofterm.proof) list |
|
10 |
val elim_cong: typ list -> Proofterm.proof -> Proofterm.proof option |
|
11 |
end; |
|
12 |
||
13 |
structure RewriteHOLProof : REWRITE_HOL_PROOF = |
|
14 |
struct |
|
15 |
||
16 |
open Proofterm; |
|
17 |
||
32010 | 18 |
val rews = map (pairself (ProofSyntax.proof_of_term @{theory} true) o |
19 |
Logic.dest_equals o Logic.varify o ProofSyntax.read_term @{theory} propT) |
|
13404 | 20 |
|
21 |
(** eliminate meta-equality rules **) |
|
22 |
||
23 |
["(equal_elim % x1 % x2 %% \ |
|
24 |
\ (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %% \ |
|
28712
4f2954d995f0
Removed argument prf2 in rewrite rules for equal_elim to make them applicable
berghofe
parents:
28262
diff
changeset
|
25 |
\ (axm.reflexive % TYPE('T3) % x4) %% prf1)) == \ |
13404 | 26 |
\ (iffD1 % A % B %% \ |
28712
4f2954d995f0
Removed argument prf2 in rewrite rules for equal_elim to make them applicable
berghofe
parents:
28262
diff
changeset
|
27 |
\ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))", |
13404 | 28 |
|
29 |
"(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %% \ |
|
30 |
\ (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %% \ |
|
28712
4f2954d995f0
Removed argument prf2 in rewrite rules for equal_elim to make them applicable
berghofe
parents:
28262
diff
changeset
|
31 |
\ (axm.reflexive % TYPE('T4) % x6) %% prf1))) == \ |
13404 | 32 |
\ (iffD2 % A % B %% \ |
28712
4f2954d995f0
Removed argument prf2 in rewrite rules for equal_elim to make them applicable
berghofe
parents:
28262
diff
changeset
|
33 |
\ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))", |
13404 | 34 |
|
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))", |
|
40 |
||
41 |
"(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% \ |
|
42 |
\ (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) == \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
43 |
\ (HOL.trans % TYPE('T) % x % y % z %% \ |
13404 | 44 |
\ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf1) %% \ |
45 |
\ (meta_eq_to_obj_eq % TYPE('T) % y % z %% prf2))", |
|
46 |
||
47 |
"(meta_eq_to_obj_eq % TYPE('T) % x % x %% (axm.reflexive % TYPE('T) % x)) == \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
48 |
\ (HOL.refl % TYPE('T) % x)", |
13404 | 49 |
|
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))", |
|
53 |
||
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)))", |
|
58 |
||
59 |
"(meta_eq_to_obj_eq % TYPE('T) % x % y %% \ |
|
60 |
\ (eq_reflection % TYPE('T) % x % y %% prf)) == prf", |
|
61 |
||
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 %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
70 |
\ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \ |
13404 | 71 |
\ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \ |
72 |
\ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \ |
|
30850
5e20f9c20086
Fixed bug in transformation of congruence rule for ==
berghofe
parents:
28814
diff
changeset
|
73 |
\ (meta_eq_to_obj_eq % TYPE('T) % A % C %% prf3))", |
13404 | 74 |
|
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 %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
84 |
\ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \ |
13404 | 85 |
\ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \ |
86 |
\ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \ |
|
30850
5e20f9c20086
Fixed bug in transformation of congruence rule for ==
berghofe
parents:
28814
diff
changeset
|
87 |
\ (meta_eq_to_obj_eq % TYPE('T) % B % D %% prf3))", |
13404 | 88 |
|
89 |
(** rewriting on bool: insert proper congruence rules for logical connectives **) |
|
90 |
||
91 |
(* All *) |
|
92 |
||
93 |
"(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
94 |
\ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \ |
13404 | 95 |
\ (allI % TYPE('a) % Q %% \ |
96 |
\ (Lam x. \ |
|
97 |
\ iffD1 % P x % Q x %% (prf % x) %% \ |
|
98 |
\ (spec % TYPE('a) % P % x %% prf')))", |
|
99 |
||
100 |
"(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
101 |
\ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \ |
13404 | 102 |
\ (allI % TYPE('a) % P %% \ |
103 |
\ (Lam x. \ |
|
104 |
\ iffD2 % P x % Q x %% (prf % x) %% \ |
|
19798 | 105 |
\ (spec % TYPE('a) % Q % x %% prf')))", |
13404 | 106 |
|
107 |
(* Ex *) |
|
108 |
||
109 |
"(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
110 |
\ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \ |
13404 | 111 |
\ (exE % TYPE('a) % P % EX x. Q x %% prf' %% \ |
112 |
\ (Lam x H : P x. \ |
|
113 |
\ exI % TYPE('a) % Q % x %% \ |
|
114 |
\ (iffD1 % P x % Q x %% (prf % x) %% H)))", |
|
115 |
||
116 |
"(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
117 |
\ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \ |
13404 | 118 |
\ (exE % TYPE('a) % Q % EX x. P x %% prf' %% \ |
119 |
\ (Lam x H : Q x. \ |
|
120 |
\ exI % TYPE('a) % P % x %% \ |
|
121 |
\ (iffD2 % P x % Q x %% (prf % x) %% H)))", |
|
122 |
||
123 |
(* & *) |
|
124 |
||
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 %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
127 |
\ (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) == \ |
13404 | 128 |
\ (conjI % B % D %% \ |
129 |
\ (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %% \ |
|
130 |
\ (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))", |
|
131 |
||
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 %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
134 |
\ (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) == \ |
13404 | 135 |
\ (conjI % A % C %% \ |
136 |
\ (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %% \ |
|
137 |
\ (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))", |
|
138 |
||
13602
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
139 |
"(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% \ |
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
140 |
\ (HOL.refl % TYPE(bool=>bool) % op & A)) == \ |
13602
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
141 |
\ (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% \ |
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
142 |
\ (cong % TYPE(bool=>bool) % TYPE(bool) % \ |
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
143 |
\ (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %% \ |
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
144 |
\ (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %% \ |
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
145 |
\ (HOL.refl % TYPE(bool) % A)))", |
13602
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
146 |
|
13404 | 147 |
(* | *) |
148 |
||
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 %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
151 |
\ (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) == \ |
13404 | 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)))", |
|
155 |
||
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 %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
158 |
\ (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) == \ |
13404 | 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)))", |
|
162 |
||
13602
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
163 |
"(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% \ |
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
164 |
\ (HOL.refl % TYPE(bool=>bool) % op | A)) == \ |
13602
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
165 |
\ (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% \ |
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
166 |
\ (cong % TYPE(bool=>bool) % TYPE(bool) % \ |
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
167 |
\ (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %% \ |
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
168 |
\ (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %% \ |
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
169 |
\ (HOL.refl % TYPE(bool) % A)))", |
13602
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
170 |
|
13404 | 171 |
(* --> *) |
172 |
||
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 %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
175 |
\ (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) == \ |
13404 | 176 |
\ (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %% \ |
177 |
\ (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))", |
|
178 |
||
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 %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
181 |
\ (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) == \ |
13404 | 182 |
\ (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %% \ |
183 |
\ (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))", |
|
184 |
||
13602
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
185 |
"(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% \ |
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
186 |
\ (HOL.refl % TYPE(bool=>bool) % op --> A)) == \ |
13602
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
187 |
\ (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% \ |
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
188 |
\ (cong % TYPE(bool=>bool) % TYPE(bool) % \ |
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
189 |
\ (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %% \ |
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
190 |
\ (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %% \ |
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
191 |
\ (HOL.refl % TYPE(bool) % A)))", |
13602
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
192 |
|
13404 | 193 |
(* ~ *) |
194 |
||
195 |
"(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
196 |
\ (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) == \ |
13404 | 197 |
\ (notI % Q %% (Lam H: Q. \ |
198 |
\ notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))", |
|
199 |
||
200 |
"(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
201 |
\ (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) == \ |
13404 | 202 |
\ (notI % P %% (Lam H: P. \ |
203 |
\ notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))", |
|
204 |
||
205 |
(* = *) |
|
206 |
||
207 |
"(iffD1 % B % D %% \ |
|
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 %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
210 |
\ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \ |
13404 | 211 |
\ (iffD1 % C % D %% prf2 %% \ |
212 |
\ (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))", |
|
213 |
||
214 |
"(iffD2 % B % D %% \ |
|
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 %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
217 |
\ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \ |
13404 | 218 |
\ (iffD1 % A % B %% prf1 %% \ |
219 |
\ (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))", |
|
220 |
||
221 |
"(iffD1 % A % C %% \ |
|
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 %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
224 |
\ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)== \ |
13404 | 225 |
\ (iffD2 % C % D %% prf2 %% \ |
226 |
\ (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))", |
|
227 |
||
228 |
"(iffD2 % A % C %% \ |
|
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 %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
231 |
\ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \ |
13404 | 232 |
\ (iffD2 % A % B %% prf1 %% \ |
233 |
\ (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))", |
|
234 |
||
235 |
"(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
236 |
\ (HOL.refl % TYPE(bool=>bool) % op = A)) == \ |
13404 | 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 %% \ |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
240 |
\ (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %% \ |
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
241 |
\ (HOL.refl % TYPE(bool) % A)))", |
13404 | 242 |
|
13916
f078a758e5d8
elim_cong now eta-expands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset
|
243 |
(** transitivity, reflexivity, and symmetry **) |
f078a758e5d8
elim_cong now eta-expands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset
|
244 |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
245 |
"(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) == \ |
13404 | 246 |
\ (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))", |
247 |
||
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
248 |
"(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) == \ |
13404 | 249 |
\ (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))", |
250 |
||
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
251 |
"(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf", |
13404 | 252 |
|
15530
6f43714517ee
Fully qualified refl and trans to avoid confusion with theorems
berghofe
parents:
14981
diff
changeset
|
253 |
"(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf", |
13404 | 254 |
|
13602
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
255 |
"(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD2 % B % A %% prf)", |
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
256 |
|
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
257 |
"(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD1 % B % A %% prf)", |
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
258 |
|
13404 | 259 |
(** normalization of HOL proofs **) |
260 |
||
261 |
"(mp % A % B %% (impI % A % B %% prf)) == prf", |
|
262 |
||
263 |
"(impI % A % B %% (mp % A % B %% prf)) == prf", |
|
264 |
||
265 |
"(spec % TYPE('a) % P % x %% (allI % TYPE('a) % P %% prf)) == prf % x", |
|
266 |
||
267 |
"(allI % TYPE('a) % P %% (Lam x::'a. spec % TYPE('a) % P % x %% prf)) == prf", |
|
268 |
||
13602
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
269 |
"(exE % TYPE('a) % P % Q %% (exI % TYPE('a) % P % x %% prf1) %% prf2) == (prf2 % x %% prf1)", |
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
270 |
|
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
271 |
"(exE % TYPE('a) % P % Q %% prf %% (exI % TYPE('a) % P)) == prf", |
4cecd1e0f4a9
- additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset
|
272 |
|
13404 | 273 |
"(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)", |
274 |
||
275 |
"(disjE % P % Q % R %% (disjI2 % Q % P %% prf1) %% prf2 %% prf3) == (prf3 %% prf1)", |
|
276 |
||
277 |
"(conjunct1 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf1", |
|
278 |
||
279 |
"(conjunct2 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf2", |
|
280 |
||
281 |
"(iffD1 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf1", |
|
282 |
||
283 |
"(iffD2 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf2"]; |
|
284 |
||
285 |
||
286 |
(** Replace congruence rules by substitution rules **) |
|
287 |
||
28801
fc45401bdf6f
ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28712
diff
changeset
|
288 |
fun strip_cong ps (PThm (_, (("HOL.cong", _, _), _)) % _ % _ % SOME x % SOME y %% |
13404 | 289 |
prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1 |
28801
fc45401bdf6f
ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28712
diff
changeset
|
290 |
| strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f) = SOME (f, ps) |
15531 | 291 |
| strip_cong _ _ = NONE; |
13404 | 292 |
|
28814 | 293 |
val subst_prf = fst (strip_combt (Thm.proof_of subst)); |
294 |
val sym_prf = fst (strip_combt (Thm.proof_of sym)); |
|
13404 | 295 |
|
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) |
|
15531 | 300 |
else change_type (SOME [T]) subst_prf %> x %> y %> |
13404 | 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) |
|
305 |
end; |
|
306 |
||
307 |
fun make_sym Ts ((x, y), prf) = |
|
15531 | 308 |
((y, x), change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf); |
13404 | 309 |
|
22277 | 310 |
fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t); |
13916
f078a758e5d8
elim_cong now eta-expands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset
|
311 |
|
28801
fc45401bdf6f
ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28712
diff
changeset
|
312 |
fun elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) = |
15570 | 313 |
Option.map (make_subst Ts prf2 []) (strip_cong [] prf1) |
28801
fc45401bdf6f
ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28712
diff
changeset
|
314 |
| elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) = |
15570 | 315 |
Option.map (mk_AbsP P o make_subst Ts (PBound 0) []) |
13916
f078a758e5d8
elim_cong now eta-expands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset
|
316 |
(strip_cong [] (incr_pboundvars 1 0 prf)) |
28801
fc45401bdf6f
ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28712
diff
changeset
|
317 |
| elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) = |
15570 | 318 |
Option.map (make_subst Ts prf2 [] o |
13404 | 319 |
apsnd (map (make_sym Ts))) (strip_cong [] prf1) |
28801
fc45401bdf6f
ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28712
diff
changeset
|
320 |
| elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) = |
15570 | 321 |
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o |
13916
f078a758e5d8
elim_cong now eta-expands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset
|
322 |
apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf)) |
15531 | 323 |
| elim_cong _ _ = NONE; |
13404 | 324 |
|
325 |
end; |