author | wenzelm |
Sat, 04 Oct 2008 16:05:09 +0200 | |
changeset 28500 | 4b79e5d3d0aa |
parent 27982 | 2aaa4a5569a6 |
child 28797 | 9dcd32ee5dbe |
permissions | -rw-r--r-- |
13403 | 1 |
(* Title: HOL/Extraction.thy |
2 |
ID: $Id$ |
|
3 |
Author: Stefan Berghofer, TU Muenchen |
|
4 |
*) |
|
5 |
||
6 |
header {* Program extraction for HOL *} |
|
7 |
||
15131 | 8 |
theory Extraction |
24194 | 9 |
imports Datatype |
16417 | 10 |
uses "Tools/rewrite_hol_proof.ML" |
15131 | 11 |
begin |
13403 | 12 |
|
13 |
subsection {* Setup *} |
|
14 |
||
16121 | 15 |
setup {* |
16 |
let |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
17 |
fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $ |
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
18 |
(Const ("op :", _) $ x $ S)) = (case strip_comb S of |
15531 | 19 |
(Var (ixn, U), ts) => SOME (list_comb (Var (ixn, binder_types U @ |
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
20 |
[HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), ts @ [x])) |
15531 | 21 |
| (Free (s, U), ts) => SOME (list_comb (Free (s, binder_types U @ |
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
22 |
[HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), ts @ [x])) |
15531 | 23 |
| _ => NONE) |
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
24 |
| realizes_set_proc (Const ("realizes", Type ("fun", [T, _])) $ r $ |
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
25 |
(Const ("op :", _) $ x $ S)) = (case strip_comb S of |
15531 | 26 |
(Var (ixn, U), ts) => SOME (list_comb (Var (ixn, T :: binder_types U @ |
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
27 |
[HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), r :: ts @ [x])) |
15531 | 28 |
| (Free (s, U), ts) => SOME (list_comb (Free (s, T :: binder_types U @ |
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
29 |
[HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), r :: ts @ [x])) |
15531 | 30 |
| _ => NONE) |
31 |
| realizes_set_proc _ = NONE; |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
32 |
|
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
33 |
fun mk_realizes_set r rT s (setT as Type ("set", [elT])) = |
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
34 |
Abs ("x", elT, Const ("realizes", rT --> HOLogic.boolT --> HOLogic.boolT) $ |
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
35 |
incr_boundvars 1 r $ (Const ("op :", elT --> setT --> HOLogic.boolT) $ |
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
36 |
Bound 0 $ incr_boundvars 1 s)); |
16121 | 37 |
in |
18708 | 38 |
Extraction.add_types |
15531 | 39 |
[("bool", ([], NONE)), |
18708 | 40 |
("set", ([realizes_set_proc], SOME mk_realizes_set))] #> |
41 |
Extraction.set_preprocessor (fn thy => |
|
13403 | 42 |
Proofterm.rewrite_proof_notypes |
43 |
([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) :: |
|
44 |
ProofRewriteRules.rprocs true) o |
|
17203 | 45 |
Proofterm.rewrite_proof thy |
13599 | 46 |
(RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o |
27982 | 47 |
ProofRewriteRules.elim_vars (curry Const @{const_name default})) |
16121 | 48 |
end |
13403 | 49 |
*} |
50 |
||
51 |
lemmas [extraction_expand] = |
|
22281 | 52 |
meta_spec atomize_eq atomize_all atomize_imp atomize_conj |
13403 | 53 |
allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2 |
20941
beedcae49096
added eq_True eq_False True_implies_equals to extraction_expand
haftmann
parents:
18708
diff
changeset
|
54 |
notE' impE' impE iffE imp_cong simp_thms eq_True eq_False |
18456 | 55 |
induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq |
56 |
induct_forall_def induct_implies_def induct_equal_def induct_conj_def |
|
18511 | 57 |
induct_atomize induct_rulify induct_rulify_fallback |
25424 | 58 |
True_implies_equals TrueE |
13403 | 59 |
|
60 |
datatype sumbool = Left | Right |
|
61 |
||
62 |
subsection {* Type of extracted program *} |
|
63 |
||
64 |
extract_type |
|
65 |
"typeof (Trueprop P) \<equiv> typeof P" |
|
66 |
||
67 |
"typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> |
|
68 |
typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE('Q))" |
|
69 |
||
70 |
"typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE(Null))" |
|
71 |
||
72 |
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> |
|
73 |
typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE('P \<Rightarrow> 'Q))" |
|
74 |
||
75 |
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow> |
|
76 |
typeof (\<forall>x. P x) \<equiv> Type (TYPE(Null))" |
|
77 |
||
78 |
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE('P))) \<Longrightarrow> |
|
79 |
typeof (\<forall>x::'a. P x) \<equiv> Type (TYPE('a \<Rightarrow> 'P))" |
|
80 |
||
81 |
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow> |
|
82 |
typeof (\<exists>x::'a. P x) \<equiv> Type (TYPE('a))" |
|
83 |
||
84 |
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE('P))) \<Longrightarrow> |
|
85 |
typeof (\<exists>x::'a. P x) \<equiv> Type (TYPE('a \<times> 'P))" |
|
86 |
||
87 |
"typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> |
|
88 |
typeof (P \<or> Q) \<equiv> Type (TYPE(sumbool))" |
|
89 |
||
90 |
"typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> |
|
91 |
typeof (P \<or> Q) \<equiv> Type (TYPE('Q option))" |
|
92 |
||
93 |
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> |
|
94 |
typeof (P \<or> Q) \<equiv> Type (TYPE('P option))" |
|
95 |
||
96 |
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> |
|
97 |
typeof (P \<or> Q) \<equiv> Type (TYPE('P + 'Q))" |
|
98 |
||
99 |
"typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> |
|
100 |
typeof (P \<and> Q) \<equiv> Type (TYPE('Q))" |
|
101 |
||
102 |
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> |
|
103 |
typeof (P \<and> Q) \<equiv> Type (TYPE('P))" |
|
104 |
||
105 |
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> |
|
106 |
typeof (P \<and> Q) \<equiv> Type (TYPE('P \<times> 'Q))" |
|
107 |
||
108 |
"typeof (P = Q) \<equiv> typeof ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P))" |
|
109 |
||
110 |
"typeof (x \<in> P) \<equiv> typeof P" |
|
111 |
||
112 |
subsection {* Realizability *} |
|
113 |
||
114 |
realizability |
|
115 |
"(realizes t (Trueprop P)) \<equiv> (Trueprop (realizes t P))" |
|
116 |
||
117 |
"(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> |
|
118 |
(realizes t (P \<longrightarrow> Q)) \<equiv> (realizes Null P \<longrightarrow> realizes t Q)" |
|
119 |
||
120 |
"(typeof P) \<equiv> (Type (TYPE('P))) \<Longrightarrow> |
|
121 |
(typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> |
|
122 |
(realizes t (P \<longrightarrow> Q)) \<equiv> (\<forall>x::'P. realizes x P \<longrightarrow> realizes Null Q)" |
|
123 |
||
124 |
"(realizes t (P \<longrightarrow> Q)) \<equiv> (\<forall>x. realizes x P \<longrightarrow> realizes (t x) Q)" |
|
125 |
||
126 |
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow> |
|
127 |
(realizes t (\<forall>x. P x)) \<equiv> (\<forall>x. realizes Null (P x))" |
|
128 |
||
129 |
"(realizes t (\<forall>x. P x)) \<equiv> (\<forall>x. realizes (t x) (P x))" |
|
130 |
||
131 |
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow> |
|
132 |
(realizes t (\<exists>x. P x)) \<equiv> (realizes Null (P t))" |
|
133 |
||
134 |
"(realizes t (\<exists>x. P x)) \<equiv> (realizes (snd t) (P (fst t)))" |
|
135 |
||
136 |
"(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> |
|
137 |
(typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> |
|
138 |
(realizes t (P \<or> Q)) \<equiv> |
|
139 |
(case t of Left \<Rightarrow> realizes Null P | Right \<Rightarrow> realizes Null Q)" |
|
140 |
||
141 |
"(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> |
|
142 |
(realizes t (P \<or> Q)) \<equiv> |
|
143 |
(case t of None \<Rightarrow> realizes Null P | Some q \<Rightarrow> realizes q Q)" |
|
144 |
||
145 |
"(typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> |
|
146 |
(realizes t (P \<or> Q)) \<equiv> |
|
147 |
(case t of None \<Rightarrow> realizes Null Q | Some p \<Rightarrow> realizes p P)" |
|
148 |
||
149 |
"(realizes t (P \<or> Q)) \<equiv> |
|
150 |
(case t of Inl p \<Rightarrow> realizes p P | Inr q \<Rightarrow> realizes q Q)" |
|
151 |
||
152 |
"(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> |
|
153 |
(realizes t (P \<and> Q)) \<equiv> (realizes Null P \<and> realizes t Q)" |
|
154 |
||
155 |
"(typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> |
|
156 |
(realizes t (P \<and> Q)) \<equiv> (realizes t P \<and> realizes Null Q)" |
|
157 |
||
158 |
"(realizes t (P \<and> Q)) \<equiv> (realizes (fst t) P \<and> realizes (snd t) Q)" |
|
159 |
||
160 |
"typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> |
|
161 |
realizes t (\<not> P) \<equiv> \<not> realizes Null P" |
|
162 |
||
163 |
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> |
|
164 |
realizes t (\<not> P) \<equiv> (\<forall>x::'P. \<not> realizes x P)" |
|
165 |
||
166 |
"typeof (P::bool) \<equiv> Type (TYPE(Null)) \<Longrightarrow> |
|
167 |
typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> |
|
168 |
realizes t (P = Q) \<equiv> realizes Null P = realizes Null Q" |
|
169 |
||
170 |
"(realizes t (P = Q)) \<equiv> (realizes t ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)))" |
|
171 |
||
172 |
subsection {* Computational content of basic inference rules *} |
|
173 |
||
174 |
theorem disjE_realizer: |
|
175 |
assumes r: "case x of Inl p \<Rightarrow> P p | Inr q \<Rightarrow> Q q" |
|
176 |
and r1: "\<And>p. P p \<Longrightarrow> R (f p)" and r2: "\<And>q. Q q \<Longrightarrow> R (g q)" |
|
177 |
shows "R (case x of Inl p \<Rightarrow> f p | Inr q \<Rightarrow> g q)" |
|
178 |
proof (cases x) |
|
179 |
case Inl |
|
180 |
with r show ?thesis by simp (rule r1) |
|
181 |
next |
|
182 |
case Inr |
|
183 |
with r show ?thesis by simp (rule r2) |
|
184 |
qed |
|
185 |
||
186 |
theorem disjE_realizer2: |
|
187 |
assumes r: "case x of None \<Rightarrow> P | Some q \<Rightarrow> Q q" |
|
188 |
and r1: "P \<Longrightarrow> R f" and r2: "\<And>q. Q q \<Longrightarrow> R (g q)" |
|
189 |
shows "R (case x of None \<Rightarrow> f | Some q \<Rightarrow> g q)" |
|
190 |
proof (cases x) |
|
191 |
case None |
|
192 |
with r show ?thesis by simp (rule r1) |
|
193 |
next |
|
194 |
case Some |
|
195 |
with r show ?thesis by simp (rule r2) |
|
196 |
qed |
|
197 |
||
198 |
theorem disjE_realizer3: |
|
199 |
assumes r: "case x of Left \<Rightarrow> P | Right \<Rightarrow> Q" |
|
200 |
and r1: "P \<Longrightarrow> R f" and r2: "Q \<Longrightarrow> R g" |
|
201 |
shows "R (case x of Left \<Rightarrow> f | Right \<Rightarrow> g)" |
|
202 |
proof (cases x) |
|
203 |
case Left |
|
204 |
with r show ?thesis by simp (rule r1) |
|
205 |
next |
|
206 |
case Right |
|
207 |
with r show ?thesis by simp (rule r2) |
|
208 |
qed |
|
209 |
||
210 |
theorem conjI_realizer: |
|
211 |
"P p \<Longrightarrow> Q q \<Longrightarrow> P (fst (p, q)) \<and> Q (snd (p, q))" |
|
212 |
by simp |
|
213 |
||
214 |
theorem exI_realizer: |
|
13918
2134ed516b1b
Tuned realizer for exE rule, to avoid blowup of extracted program.
berghofe
parents:
13725
diff
changeset
|
215 |
"P y x \<Longrightarrow> P (snd (x, y)) (fst (x, y))" by simp |
2134ed516b1b
Tuned realizer for exE rule, to avoid blowup of extracted program.
berghofe
parents:
13725
diff
changeset
|
216 |
|
2134ed516b1b
Tuned realizer for exE rule, to avoid blowup of extracted program.
berghofe
parents:
13725
diff
changeset
|
217 |
theorem exE_realizer: "P (snd p) (fst p) \<Longrightarrow> |
15393 | 218 |
(\<And>x y. P y x \<Longrightarrow> Q (f x y)) \<Longrightarrow> Q (let (x, y) = p in f x y)" |
219 |
by (cases p) (simp add: Let_def) |
|
13918
2134ed516b1b
Tuned realizer for exE rule, to avoid blowup of extracted program.
berghofe
parents:
13725
diff
changeset
|
220 |
|
2134ed516b1b
Tuned realizer for exE rule, to avoid blowup of extracted program.
berghofe
parents:
13725
diff
changeset
|
221 |
theorem exE_realizer': "P (snd p) (fst p) \<Longrightarrow> |
2134ed516b1b
Tuned realizer for exE rule, to avoid blowup of extracted program.
berghofe
parents:
13725
diff
changeset
|
222 |
(\<And>x y. P y x \<Longrightarrow> Q) \<Longrightarrow> Q" by (cases p) simp |
13403 | 223 |
|
27982 | 224 |
setup {* |
225 |
Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::type"}) |
|
226 |
*} |
|
227 |
||
13403 | 228 |
realizers |
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
229 |
impI (P, Q): "\<lambda>pq. pq" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
230 |
"\<Lambda> P Q pq (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" |
13403 | 231 |
|
232 |
impI (P): "Null" |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
233 |
"\<Lambda> P Q (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" |
13403 | 234 |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
235 |
impI (Q): "\<lambda>q. q" "\<Lambda> P Q q. impI \<cdot> _ \<cdot> _" |
13403 | 236 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
237 |
impI: "Null" "impI" |
13403 | 238 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
239 |
mp (P, Q): "\<lambda>pq. pq" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
240 |
"\<Lambda> P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
13403 | 241 |
|
242 |
mp (P): "Null" |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
243 |
"\<Lambda> P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
13403 | 244 |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
245 |
mp (Q): "\<lambda>q. q" "\<Lambda> P Q q. mp \<cdot> _ \<cdot> _" |
13403 | 246 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
247 |
mp: "Null" "mp" |
13403 | 248 |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
249 |
allI (P): "\<lambda>p. p" "\<Lambda> P p. allI \<cdot> _" |
13403 | 250 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
251 |
allI: "Null" "allI" |
13403 | 252 |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
253 |
spec (P): "\<lambda>x p. p x" "\<Lambda> P x p. spec \<cdot> _ \<cdot> x" |
13403 | 254 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
255 |
spec: "Null" "spec" |
13403 | 256 |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
257 |
exI (P): "\<lambda>x p. (x, p)" "\<Lambda> P x p. exI_realizer \<cdot> P \<cdot> p \<cdot> x" |
13403 | 258 |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
259 |
exI: "\<lambda>x. x" "\<Lambda> P x (h: _). h" |
13403 | 260 |
|
15393 | 261 |
exE (P, Q): "\<lambda>p pq. let (x, y) = p in pq x y" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
262 |
"\<Lambda> P Q p (h: _) pq. exE_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> pq \<bullet> h" |
13403 | 263 |
|
264 |
exE (P): "Null" |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
265 |
"\<Lambda> P Q p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _" |
13403 | 266 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
267 |
exE (Q): "\<lambda>x pq. pq x" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
268 |
"\<Lambda> P Q x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1" |
13403 | 269 |
|
270 |
exE: "Null" |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
271 |
"\<Lambda> P Q x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1" |
13403 | 272 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
273 |
conjI (P, Q): "Pair" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
274 |
"\<Lambda> P Q p (h: _) q. conjI_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> q \<bullet> h" |
13403 | 275 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
276 |
conjI (P): "\<lambda>p. p" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
277 |
"\<Lambda> P Q p. conjI \<cdot> _ \<cdot> _" |
13403 | 278 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
279 |
conjI (Q): "\<lambda>q. q" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
280 |
"\<Lambda> P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h" |
13403 | 281 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
282 |
conjI: "Null" "conjI" |
13403 | 283 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
284 |
conjunct1 (P, Q): "fst" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
285 |
"\<Lambda> P Q pq. conjunct1 \<cdot> _ \<cdot> _" |
13403 | 286 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
287 |
conjunct1 (P): "\<lambda>p. p" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
288 |
"\<Lambda> P Q p. conjunct1 \<cdot> _ \<cdot> _" |
13403 | 289 |
|
290 |
conjunct1 (Q): "Null" |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
291 |
"\<Lambda> P Q q. conjunct1 \<cdot> _ \<cdot> _" |
13403 | 292 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
293 |
conjunct1: "Null" "conjunct1" |
13403 | 294 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
295 |
conjunct2 (P, Q): "snd" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
296 |
"\<Lambda> P Q pq. conjunct2 \<cdot> _ \<cdot> _" |
13403 | 297 |
|
298 |
conjunct2 (P): "Null" |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
299 |
"\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _" |
13403 | 300 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
301 |
conjunct2 (Q): "\<lambda>p. p" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
302 |
"\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _" |
13403 | 303 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
304 |
conjunct2: "Null" "conjunct2" |
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
305 |
|
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
306 |
disjI1 (P, Q): "Inl" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
307 |
"\<Lambda> P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> P \<cdot> _ \<cdot> p)" |
13403 | 308 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
309 |
disjI1 (P): "Some" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
310 |
"\<Lambda> P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p)" |
13403 | 311 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
312 |
disjI1 (Q): "None" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
313 |
"\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)" |
13403 | 314 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
315 |
disjI1: "Left" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
316 |
"\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _)" |
13403 | 317 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
318 |
disjI2 (P, Q): "Inr" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
319 |
"\<Lambda> Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)" |
13403 | 320 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
321 |
disjI2 (P): "None" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
322 |
"\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)" |
13403 | 323 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
324 |
disjI2 (Q): "Some" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
325 |
"\<Lambda> Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)" |
13403 | 326 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
327 |
disjI2: "Right" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
328 |
"\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _)" |
13403 | 329 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
330 |
disjE (P, Q, R): "\<lambda>pq pr qr. |
13403 | 331 |
(case pq of Inl p \<Rightarrow> pr p | Inr q \<Rightarrow> qr q)" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
332 |
"\<Lambda> P Q R pq (h1: _) pr (h2: _) qr. |
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
333 |
disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" |
13403 | 334 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
335 |
disjE (Q, R): "\<lambda>pq pr qr. |
13403 | 336 |
(case pq of None \<Rightarrow> pr | Some q \<Rightarrow> qr q)" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
337 |
"\<Lambda> P Q R pq (h1: _) pr (h2: _) qr. |
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
338 |
disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" |
13403 | 339 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
340 |
disjE (P, R): "\<lambda>pq pr qr. |
13403 | 341 |
(case pq of None \<Rightarrow> qr | Some p \<Rightarrow> pr p)" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
342 |
"\<Lambda> P Q R pq (h1: _) pr (h2: _) qr (h3: _). |
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
343 |
disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> qr \<cdot> pr \<bullet> h1 \<bullet> h3 \<bullet> h2" |
13403 | 344 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
345 |
disjE (R): "\<lambda>pq pr qr. |
13403 | 346 |
(case pq of Left \<Rightarrow> pr | Right \<Rightarrow> qr)" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
347 |
"\<Lambda> P Q R pq (h1: _) pr (h2: _) qr. |
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
348 |
disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" |
13403 | 349 |
|
350 |
disjE (P, Q): "Null" |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
351 |
"\<Lambda> P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _" |
13403 | 352 |
|
353 |
disjE (Q): "Null" |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
354 |
"\<Lambda> P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _" |
13403 | 355 |
|
356 |
disjE (P): "Null" |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
357 |
"\<Lambda> P Q R pq (h1: _) (h2: _) (h3: _). |
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
358 |
disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> h1 \<bullet> h3 \<bullet> h2" |
13403 | 359 |
|
360 |
disjE: "Null" |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
361 |
"\<Lambda> P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _" |
13403 | 362 |
|
27982 | 363 |
FalseE (P): "default" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
364 |
"\<Lambda> P. FalseE \<cdot> _" |
13403 | 365 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
366 |
FalseE: "Null" "FalseE" |
13403 | 367 |
|
368 |
notI (P): "Null" |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
369 |
"\<Lambda> P (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. notI \<cdot> _ \<bullet> (h \<cdot> x))" |
13403 | 370 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
371 |
notI: "Null" "notI" |
13403 | 372 |
|
27982 | 373 |
notE (P, R): "\<lambda>p. default" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
374 |
"\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
13403 | 375 |
|
376 |
notE (P): "Null" |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
377 |
"\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
13403 | 378 |
|
27982 | 379 |
notE (R): "default" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
380 |
"\<Lambda> P R. notE \<cdot> _ \<cdot> _" |
13403 | 381 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
382 |
notE: "Null" "notE" |
13403 | 383 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
384 |
subst (P): "\<lambda>s t ps. ps" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
385 |
"\<Lambda> s t P (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> P ps \<bullet> h" |
13403 | 386 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
387 |
subst: "Null" "subst" |
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
388 |
|
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
389 |
iffD1 (P, Q): "fst" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
390 |
"\<Lambda> Q P pq (h: _) p. |
13403 | 391 |
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" |
392 |
||
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
393 |
iffD1 (P): "\<lambda>p. p" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
394 |
"\<Lambda> Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)" |
13403 | 395 |
|
396 |
iffD1 (Q): "Null" |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
397 |
"\<Lambda> Q P q1 (h: _) q2. |
13403 | 398 |
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" |
399 |
||
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
400 |
iffD1: "Null" "iffD1" |
13403 | 401 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
402 |
iffD2 (P, Q): "snd" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
403 |
"\<Lambda> P Q pq (h: _) q. |
13403 | 404 |
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" |
405 |
||
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
406 |
iffD2 (P): "\<lambda>p. p" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
407 |
"\<Lambda> P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)" |
13403 | 408 |
|
409 |
iffD2 (Q): "Null" |
|
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
410 |
"\<Lambda> P Q q1 (h: _) q2. |
13403 | 411 |
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" |
412 |
||
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
413 |
iffD2: "Null" "iffD2" |
13403 | 414 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
415 |
iffI (P, Q): "Pair" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
416 |
"\<Lambda> P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot> |
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
417 |
(\<lambda>pq. \<forall>x. P x \<longrightarrow> Q (pq x)) \<cdot> pq \<cdot> |
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
418 |
(\<lambda>qp. \<forall>x. Q x \<longrightarrow> P (qp x)) \<cdot> qp \<bullet> |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
419 |
(allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> |
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
420 |
(allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" |
13403 | 421 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
422 |
iffI (P): "\<lambda>p. p" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
423 |
"\<Lambda> P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> |
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
424 |
(allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> |
13403 | 425 |
(impI \<cdot> _ \<cdot> _ \<bullet> h2)" |
426 |
||
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
427 |
iffI (Q): "\<lambda>q. q" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
428 |
"\<Lambda> P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> |
13403 | 429 |
(impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet> |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
430 |
(allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" |
13403 | 431 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
432 |
iffI: "Null" "iffI" |
13403 | 433 |
|
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
434 |
(* |
13403 | 435 |
classical: "Null" |
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset
|
436 |
"\<Lambda> P. classical \<cdot> _" |
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset
|
437 |
*) |
13403 | 438 |
|
27982 | 439 |
setup {* |
440 |
Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::default"}) |
|
441 |
*} |
|
442 |
||
13403 | 443 |
end |