author | berghofe |
Wed, 07 Aug 2002 16:47:36 +0200 | |
changeset 13468 | 71118807d303 |
parent 13452 | 278f2cba42ab |
child 13599 | cfdf7e4cd0d2 |
permissions | -rw-r--r-- |
13403 | 1 |
(* Title: HOL/Extraction.thy |
2 |
ID: $Id$ |
|
3 |
Author: Stefan Berghofer, TU Muenchen |
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
*) |
|
6 |
||
7 |
header {* Program extraction for HOL *} |
|
8 |
||
9 |
theory Extraction = Datatype |
|
10 |
files |
|
11 |
"Tools/rewrite_hol_proof.ML": |
|
12 |
||
13 |
subsection {* Setup *} |
|
14 |
||
15 |
ML_setup {* |
|
16 |
Context.>> (fn thy => thy |> |
|
17 |
Extraction.set_preprocessor (fn sg => |
|
18 |
Proofterm.rewrite_proof_notypes |
|
19 |
([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) :: |
|
20 |
ProofRewriteRules.rprocs true) o |
|
21 |
Proofterm.rewrite_proof (Sign.tsig_of sg) |
|
22 |
(RewriteHOLProof.rews, ProofRewriteRules.rprocs true))) |
|
23 |
*} |
|
24 |
||
25 |
lemmas [extraction_expand] = |
|
13468
71118807d303
Removed (now unneeded) declaration of realizers for induction on natural numbers.
berghofe
parents:
13452
diff
changeset
|
26 |
atomize_eq atomize_all atomize_imp |
13403 | 27 |
allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2 |
28 |
notE' impE' impE iffE imp_cong simp_thms |
|
29 |
induct_forall_eq induct_implies_eq induct_equal_eq |
|
30 |
induct_forall_def induct_implies_def |
|
31 |
induct_atomize induct_rulify1 induct_rulify2 |
|
32 |
||
33 |
datatype sumbool = Left | Right |
|
34 |
||
35 |
subsection {* Type of extracted program *} |
|
36 |
||
37 |
extract_type |
|
38 |
"typeof (Trueprop P) \<equiv> typeof P" |
|
39 |
||
40 |
"typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> |
|
41 |
typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE('Q))" |
|
42 |
||
43 |
"typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE(Null))" |
|
44 |
||
45 |
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> |
|
46 |
typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE('P \<Rightarrow> 'Q))" |
|
47 |
||
48 |
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow> |
|
49 |
typeof (\<forall>x. P x) \<equiv> Type (TYPE(Null))" |
|
50 |
||
51 |
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE('P))) \<Longrightarrow> |
|
52 |
typeof (\<forall>x::'a. P x) \<equiv> Type (TYPE('a \<Rightarrow> 'P))" |
|
53 |
||
54 |
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow> |
|
55 |
typeof (\<exists>x::'a. P x) \<equiv> Type (TYPE('a))" |
|
56 |
||
57 |
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE('P))) \<Longrightarrow> |
|
58 |
typeof (\<exists>x::'a. P x) \<equiv> Type (TYPE('a \<times> 'P))" |
|
59 |
||
60 |
"typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> |
|
61 |
typeof (P \<or> Q) \<equiv> Type (TYPE(sumbool))" |
|
62 |
||
63 |
"typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> |
|
64 |
typeof (P \<or> Q) \<equiv> Type (TYPE('Q option))" |
|
65 |
||
66 |
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> |
|
67 |
typeof (P \<or> Q) \<equiv> Type (TYPE('P option))" |
|
68 |
||
69 |
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> |
|
70 |
typeof (P \<or> Q) \<equiv> Type (TYPE('P + 'Q))" |
|
71 |
||
72 |
"typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> |
|
73 |
typeof (P \<and> Q) \<equiv> Type (TYPE('Q))" |
|
74 |
||
75 |
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> |
|
76 |
typeof (P \<and> Q) \<equiv> Type (TYPE('P))" |
|
77 |
||
78 |
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> |
|
79 |
typeof (P \<and> Q) \<equiv> Type (TYPE('P \<times> 'Q))" |
|
80 |
||
81 |
"typeof (P = Q) \<equiv> typeof ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P))" |
|
82 |
||
83 |
"typeof (x \<in> P) \<equiv> typeof P" |
|
84 |
||
85 |
subsection {* Realizability *} |
|
86 |
||
87 |
realizability |
|
88 |
"(realizes t (Trueprop P)) \<equiv> (Trueprop (realizes t P))" |
|
89 |
||
90 |
"(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> |
|
91 |
(realizes t (P \<longrightarrow> Q)) \<equiv> (realizes Null P \<longrightarrow> realizes t Q)" |
|
92 |
||
93 |
"(typeof P) \<equiv> (Type (TYPE('P))) \<Longrightarrow> |
|
94 |
(typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> |
|
95 |
(realizes t (P \<longrightarrow> Q)) \<equiv> (\<forall>x::'P. realizes x P \<longrightarrow> realizes Null Q)" |
|
96 |
||
97 |
"(realizes t (P \<longrightarrow> Q)) \<equiv> (\<forall>x. realizes x P \<longrightarrow> realizes (t x) Q)" |
|
98 |
||
99 |
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow> |
|
100 |
(realizes t (\<forall>x. P x)) \<equiv> (\<forall>x. realizes Null (P x))" |
|
101 |
||
102 |
"(realizes t (\<forall>x. P x)) \<equiv> (\<forall>x. realizes (t x) (P x))" |
|
103 |
||
104 |
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow> |
|
105 |
(realizes t (\<exists>x. P x)) \<equiv> (realizes Null (P t))" |
|
106 |
||
107 |
"(realizes t (\<exists>x. P x)) \<equiv> (realizes (snd t) (P (fst t)))" |
|
108 |
||
109 |
"(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> |
|
110 |
(typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> |
|
111 |
(realizes t (P \<or> Q)) \<equiv> |
|
112 |
(case t of Left \<Rightarrow> realizes Null P | Right \<Rightarrow> realizes Null Q)" |
|
113 |
||
114 |
"(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> |
|
115 |
(realizes t (P \<or> Q)) \<equiv> |
|
116 |
(case t of None \<Rightarrow> realizes Null P | Some q \<Rightarrow> realizes q Q)" |
|
117 |
||
118 |
"(typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> |
|
119 |
(realizes t (P \<or> Q)) \<equiv> |
|
120 |
(case t of None \<Rightarrow> realizes Null Q | Some p \<Rightarrow> realizes p P)" |
|
121 |
||
122 |
"(realizes t (P \<or> Q)) \<equiv> |
|
123 |
(case t of Inl p \<Rightarrow> realizes p P | Inr q \<Rightarrow> realizes q Q)" |
|
124 |
||
125 |
"(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> |
|
126 |
(realizes t (P \<and> Q)) \<equiv> (realizes Null P \<and> realizes t Q)" |
|
127 |
||
128 |
"(typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> |
|
129 |
(realizes t (P \<and> Q)) \<equiv> (realizes t P \<and> realizes Null Q)" |
|
130 |
||
131 |
"(realizes t (P \<and> Q)) \<equiv> (realizes (fst t) P \<and> realizes (snd t) Q)" |
|
132 |
||
133 |
"typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> |
|
134 |
realizes t (\<not> P) \<equiv> \<not> realizes Null P" |
|
135 |
||
136 |
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> |
|
137 |
realizes t (\<not> P) \<equiv> (\<forall>x::'P. \<not> realizes x P)" |
|
138 |
||
139 |
"typeof (P::bool) \<equiv> Type (TYPE(Null)) \<Longrightarrow> |
|
140 |
typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> |
|
141 |
realizes t (P = Q) \<equiv> realizes Null P = realizes Null Q" |
|
142 |
||
143 |
"(realizes t (P = Q)) \<equiv> (realizes t ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)))" |
|
144 |
||
145 |
subsection {* Computational content of basic inference rules *} |
|
146 |
||
147 |
theorem disjE_realizer: |
|
148 |
assumes r: "case x of Inl p \<Rightarrow> P p | Inr q \<Rightarrow> Q q" |
|
149 |
and r1: "\<And>p. P p \<Longrightarrow> R (f p)" and r2: "\<And>q. Q q \<Longrightarrow> R (g q)" |
|
150 |
shows "R (case x of Inl p \<Rightarrow> f p | Inr q \<Rightarrow> g q)" |
|
151 |
proof (cases x) |
|
152 |
case Inl |
|
153 |
with r show ?thesis by simp (rule r1) |
|
154 |
next |
|
155 |
case Inr |
|
156 |
with r show ?thesis by simp (rule r2) |
|
157 |
qed |
|
158 |
||
159 |
theorem disjE_realizer2: |
|
160 |
assumes r: "case x of None \<Rightarrow> P | Some q \<Rightarrow> Q q" |
|
161 |
and r1: "P \<Longrightarrow> R f" and r2: "\<And>q. Q q \<Longrightarrow> R (g q)" |
|
162 |
shows "R (case x of None \<Rightarrow> f | Some q \<Rightarrow> g q)" |
|
163 |
proof (cases x) |
|
164 |
case None |
|
165 |
with r show ?thesis by simp (rule r1) |
|
166 |
next |
|
167 |
case Some |
|
168 |
with r show ?thesis by simp (rule r2) |
|
169 |
qed |
|
170 |
||
171 |
theorem disjE_realizer3: |
|
172 |
assumes r: "case x of Left \<Rightarrow> P | Right \<Rightarrow> Q" |
|
173 |
and r1: "P \<Longrightarrow> R f" and r2: "Q \<Longrightarrow> R g" |
|
174 |
shows "R (case x of Left \<Rightarrow> f | Right \<Rightarrow> g)" |
|
175 |
proof (cases x) |
|
176 |
case Left |
|
177 |
with r show ?thesis by simp (rule r1) |
|
178 |
next |
|
179 |
case Right |
|
180 |
with r show ?thesis by simp (rule r2) |
|
181 |
qed |
|
182 |
||
183 |
theorem conjI_realizer: |
|
184 |
"P p \<Longrightarrow> Q q \<Longrightarrow> P (fst (p, q)) \<and> Q (snd (p, q))" |
|
185 |
by simp |
|
186 |
||
187 |
theorem exI_realizer: |
|
188 |
"P x y \<Longrightarrow> P (fst (x, y)) (snd (x, y))" by simp |
|
189 |
||
190 |
realizers |
|
191 |
impI (P, Q): "\<lambda>P Q pq. pq" |
|
192 |
"\<Lambda>P Q pq (h: _). allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" |
|
193 |
||
194 |
impI (P): "Null" |
|
195 |
"\<Lambda>P Q (h: _). allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" |
|
196 |
||
197 |
impI (Q): "\<lambda>P Q q. q" "\<Lambda>P Q q. impI \<cdot> _ \<cdot> _" |
|
198 |
||
199 |
impI: "Null" "\<Lambda>P Q. impI \<cdot> _ \<cdot> _" |
|
200 |
||
201 |
mp (P, Q): "\<lambda>P Q pq. pq" |
|
202 |
"\<Lambda>P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
|
203 |
||
204 |
mp (P): "Null" |
|
205 |
"\<Lambda>P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
|
206 |
||
207 |
mp (Q): "\<lambda>P Q q. q" "\<Lambda>P Q q. mp \<cdot> _ \<cdot> _" |
|
208 |
||
209 |
mp: "Null" "\<Lambda>P Q. mp \<cdot> _ \<cdot> _" |
|
210 |
||
211 |
allI (P): "\<lambda>P p. p" "\<Lambda>P p. allI \<cdot> _" |
|
212 |
||
213 |
allI: "Null" "\<Lambda>P. allI \<cdot> _" |
|
214 |
||
215 |
spec (P): "\<lambda>P x p. p x" "\<Lambda>P x p. spec \<cdot> _ \<cdot> x" |
|
216 |
||
217 |
spec: "Null" "\<Lambda>P x. spec \<cdot> _ \<cdot> x" |
|
218 |
||
219 |
exI (P): "\<lambda>P x p. (x, p)" "\<Lambda>P. exI_realizer \<cdot> _" |
|
220 |
||
221 |
exI: "\<lambda>P x. x" "\<Lambda>P x (h: _). h" |
|
222 |
||
223 |
exE (P, Q): "\<lambda>P Q p pq. pq (fst p) (snd p)" |
|
224 |
"\<Lambda>P Q p (h1: _) pq (h2: _). h2 \<cdot> (fst p) \<cdot> (snd p) \<bullet> h1" |
|
225 |
||
226 |
exE (P): "Null" |
|
227 |
"\<Lambda>P Q p (h1: _) (h2: _). h2 \<cdot> (fst p) \<cdot> (snd p) \<bullet> h1" |
|
228 |
||
229 |
exE (Q): "\<lambda>P Q x pq. pq x" |
|
230 |
"\<Lambda>P Q x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1" |
|
231 |
||
232 |
exE: "Null" |
|
233 |
"\<Lambda>P Q x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1" |
|
234 |
||
235 |
conjI (P, Q): "\<lambda>P Q p q. (p, q)" |
|
236 |
"\<Lambda>P Q p (h: _) q. conjI_realizer \<cdot> |
|
237 |
(\<lambda>p. realizes p P) \<cdot> p \<cdot> (\<lambda>q. realizes q Q) \<cdot> q \<bullet> h" |
|
238 |
||
239 |
conjI (P): "\<lambda>P Q p. p" |
|
240 |
"\<Lambda>P Q p. conjI \<cdot> _ \<cdot> _" |
|
241 |
||
242 |
conjI (Q): "\<lambda>P Q q. q" |
|
243 |
"\<Lambda>P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h" |
|
244 |
||
245 |
conjI: "Null" |
|
246 |
"\<Lambda>P Q. conjI \<cdot> _ \<cdot> _" |
|
247 |
||
248 |
conjunct1 (P, Q): "\<lambda>P Q. fst" |
|
249 |
"\<Lambda>P Q pq. conjunct1 \<cdot> _ \<cdot> _" |
|
250 |
||
251 |
conjunct1 (P): "\<lambda>P Q p. p" |
|
252 |
"\<Lambda>P Q p. conjunct1 \<cdot> _ \<cdot> _" |
|
253 |
||
254 |
conjunct1 (Q): "Null" |
|
255 |
"\<Lambda>P Q q. conjunct1 \<cdot> _ \<cdot> _" |
|
256 |
||
257 |
conjunct1: "Null" |
|
258 |
"\<Lambda>P Q. conjunct1 \<cdot> _ \<cdot> _" |
|
259 |
||
260 |
conjunct2 (P, Q): "\<lambda>P Q. snd" |
|
261 |
"\<Lambda>P Q pq. conjunct2 \<cdot> _ \<cdot> _" |
|
262 |
||
263 |
conjunct2 (P): "Null" |
|
264 |
"\<Lambda>P Q p. conjunct2 \<cdot> _ \<cdot> _" |
|
265 |
||
266 |
conjunct2 (Q): "\<lambda>P Q p. p" |
|
267 |
"\<Lambda>P Q p. conjunct2 \<cdot> _ \<cdot> _" |
|
268 |
||
269 |
conjunct2: "Null" |
|
270 |
"\<Lambda>P Q. conjunct2 \<cdot> _ \<cdot> _" |
|
271 |
||
272 |
disjI1 (P, Q): "\<lambda>P Q. Inl" |
|
273 |
"\<Lambda>P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> (\<lambda>p. realizes p P) \<cdot> _ \<cdot> p)" |
|
274 |
||
275 |
disjI1 (P): "\<lambda>P Q. Some" |
|
276 |
"\<Lambda>P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> (\<lambda>p. realizes p P) \<cdot> p)" |
|
277 |
||
278 |
disjI1 (Q): "\<lambda>P Q. None" |
|
279 |
"\<Lambda>P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)" |
|
280 |
||
281 |
disjI1: "\<lambda>P Q. Left" |
|
282 |
"\<Lambda>P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _)" |
|
283 |
||
284 |
disjI2 (P, Q): "\<lambda>Q P. Inr" |
|
285 |
"\<Lambda>Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> (\<lambda>q. realizes q Q) \<cdot> q)" |
|
286 |
||
287 |
disjI2 (P): "\<lambda>Q P. None" |
|
288 |
"\<Lambda>Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)" |
|
289 |
||
290 |
disjI2 (Q): "\<lambda>Q P. Some" |
|
291 |
"\<Lambda>Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> (\<lambda>q. realizes q Q) \<cdot> q)" |
|
292 |
||
293 |
disjI2: "\<lambda>Q P. Right" |
|
294 |
"\<Lambda>Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _)" |
|
295 |
||
296 |
disjE (P, Q, R): "\<lambda>P Q R pq pr qr. |
|
297 |
(case pq of Inl p \<Rightarrow> pr p | Inr q \<Rightarrow> qr q)" |
|
298 |
"\<Lambda>P Q R pq (h1: _) pr (h2: _) qr. |
|
299 |
disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes r R) \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" |
|
300 |
||
301 |
disjE (Q, R): "\<lambda>P Q R pq pr qr. |
|
302 |
(case pq of None \<Rightarrow> pr | Some q \<Rightarrow> qr q)" |
|
303 |
"\<Lambda>P Q R pq (h1: _) pr (h2: _) qr. |
|
304 |
disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes r R) \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" |
|
305 |
||
306 |
disjE (P, R): "\<lambda>P Q R pq pr qr. |
|
307 |
(case pq of None \<Rightarrow> qr | Some p \<Rightarrow> pr p)" |
|
308 |
"\<Lambda>P Q R pq (h1: _) pr (h2: _) qr (h3: _). |
|
309 |
disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes r R) \<cdot> qr \<cdot> pr \<bullet> h1 \<bullet> h3 \<bullet> h2" |
|
310 |
||
311 |
disjE (R): "\<lambda>P Q R pq pr qr. |
|
312 |
(case pq of Left \<Rightarrow> pr | Right \<Rightarrow> qr)" |
|
313 |
"\<Lambda>P Q R pq (h1: _) pr (h2: _) qr. |
|
314 |
disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes r R) \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" |
|
315 |
||
316 |
disjE (P, Q): "Null" |
|
317 |
"\<Lambda>P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes Null R) \<cdot> _ \<cdot> _" |
|
318 |
||
319 |
disjE (Q): "Null" |
|
320 |
"\<Lambda>P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes Null R) \<cdot> _ \<cdot> _" |
|
321 |
||
322 |
disjE (P): "Null" |
|
323 |
"\<Lambda>P Q R pq (h1: _) (h2: _) (h3: _). |
|
324 |
disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes Null R) \<cdot> _ \<cdot> _ \<bullet> h1 \<bullet> h3 \<bullet> h2" |
|
325 |
||
326 |
disjE: "Null" |
|
327 |
"\<Lambda>P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes Null R) \<cdot> _ \<cdot> _" |
|
328 |
||
329 |
FalseE (P): "\<lambda>P. arbitrary" |
|
330 |
"\<Lambda>P. FalseE \<cdot> _" |
|
331 |
||
332 |
FalseE: "Null" |
|
333 |
"\<Lambda>P. FalseE \<cdot> _" |
|
334 |
||
335 |
notI (P): "Null" |
|
336 |
"\<Lambda>P (h: _). allI \<cdot> _ \<bullet> (\<Lambda>x. notI \<cdot> _ \<bullet> (h \<cdot> x))" |
|
337 |
||
338 |
notI: "Null" |
|
339 |
"\<Lambda>P. notI \<cdot> _" |
|
340 |
||
341 |
notE (P, R): "\<lambda>P R p. arbitrary" |
|
342 |
"\<Lambda>P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
|
343 |
||
344 |
notE (P): "Null" |
|
345 |
"\<Lambda>P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
|
346 |
||
347 |
notE (R): "\<lambda>P R. arbitrary" |
|
348 |
"\<Lambda>P R. notE \<cdot> _ \<cdot> _" |
|
349 |
||
350 |
notE: "Null" |
|
351 |
"\<Lambda>P R. notE \<cdot> _ \<cdot> _" |
|
352 |
||
353 |
subst (P): "\<lambda>s t P ps. ps" |
|
354 |
"\<Lambda>s t P (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> (\<lambda>x. realizes ps (P x)) \<bullet> h" |
|
355 |
||
356 |
subst: "Null" |
|
357 |
"\<Lambda>s t P. subst \<cdot> s \<cdot> t \<cdot> (\<lambda>x. realizes Null (P x))" |
|
358 |
||
359 |
iffD1 (P, Q): "\<lambda>Q P. fst" |
|
360 |
"\<Lambda>Q P pq (h: _) p. |
|
361 |
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" |
|
362 |
||
363 |
iffD1 (P): "\<lambda>Q P p. p" |
|
364 |
"\<Lambda>Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)" |
|
365 |
||
366 |
iffD1 (Q): "Null" |
|
367 |
"\<Lambda>Q P q1 (h: _) q2. |
|
368 |
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" |
|
369 |
||
370 |
iffD1: "Null" |
|
371 |
"\<Lambda>Q P. iffD1 \<cdot> _ \<cdot> _" |
|
372 |
||
373 |
iffD2 (P, Q): "\<lambda>P Q. snd" |
|
374 |
"\<Lambda>P Q pq (h: _) q. |
|
375 |
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" |
|
376 |
||
377 |
iffD2 (P): "\<lambda>P Q p. p" |
|
378 |
"\<Lambda>P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)" |
|
379 |
||
380 |
iffD2 (Q): "Null" |
|
381 |
"\<Lambda>P Q q1 (h: _) q2. |
|
382 |
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" |
|
383 |
||
384 |
iffD2: "Null" |
|
385 |
"\<Lambda>P Q. iffD2 \<cdot> _ \<cdot> _" |
|
386 |
||
387 |
iffI (P, Q): "\<lambda>P Q pq qp. (pq, qp)" |
|
388 |
"\<Lambda>P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot> |
|
389 |
(\<lambda>pq. \<forall>x. realizes x P \<longrightarrow> realizes (pq x) Q) \<cdot> pq \<cdot> |
|
390 |
(\<lambda>qp. \<forall>x. realizes x Q \<longrightarrow> realizes (qp x) P) \<cdot> qp \<bullet> |
|
391 |
(allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> |
|
392 |
(allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" |
|
393 |
||
394 |
iffI (P): "\<lambda>P Q p. p" |
|
395 |
"\<Lambda>P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> |
|
396 |
(allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> |
|
397 |
(impI \<cdot> _ \<cdot> _ \<bullet> h2)" |
|
398 |
||
399 |
iffI (Q): "\<lambda>P Q q. q" |
|
400 |
"\<Lambda>P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> |
|
401 |
(impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet> |
|
402 |
(allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" |
|
403 |
||
404 |
iffI: "Null" |
|
405 |
"\<Lambda>P Q. iffI \<cdot> _ \<cdot> _" |
|
406 |
||
407 |
classical: "Null" |
|
408 |
"\<Lambda>P. classical \<cdot> _" |
|
409 |
||
410 |
end |