1 (* Title: HOLCF/Tools/Domain/domain_take_proofs.ML |
|
2 Author: Brian Huffman |
|
3 |
|
4 Defines take functions for the given domain equation |
|
5 and proves related theorems. |
|
6 *) |
|
7 |
|
8 signature DOMAIN_TAKE_PROOFS = |
|
9 sig |
|
10 type iso_info = |
|
11 { |
|
12 absT : typ, |
|
13 repT : typ, |
|
14 abs_const : term, |
|
15 rep_const : term, |
|
16 abs_inverse : thm, |
|
17 rep_inverse : thm |
|
18 } |
|
19 type take_info = |
|
20 { |
|
21 take_consts : term list, |
|
22 take_defs : thm list, |
|
23 chain_take_thms : thm list, |
|
24 take_0_thms : thm list, |
|
25 take_Suc_thms : thm list, |
|
26 deflation_take_thms : thm list, |
|
27 take_strict_thms : thm list, |
|
28 finite_consts : term list, |
|
29 finite_defs : thm list |
|
30 } |
|
31 type take_induct_info = |
|
32 { |
|
33 take_consts : term list, |
|
34 take_defs : thm list, |
|
35 chain_take_thms : thm list, |
|
36 take_0_thms : thm list, |
|
37 take_Suc_thms : thm list, |
|
38 deflation_take_thms : thm list, |
|
39 take_strict_thms : thm list, |
|
40 finite_consts : term list, |
|
41 finite_defs : thm list, |
|
42 lub_take_thms : thm list, |
|
43 reach_thms : thm list, |
|
44 take_lemma_thms : thm list, |
|
45 is_finite : bool, |
|
46 take_induct_thms : thm list |
|
47 } |
|
48 val define_take_functions : |
|
49 (binding * iso_info) list -> theory -> take_info * theory |
|
50 |
|
51 val add_lub_take_theorems : |
|
52 (binding * iso_info) list -> take_info -> thm list -> |
|
53 theory -> take_induct_info * theory |
|
54 |
|
55 val map_of_typ : |
|
56 theory -> (typ * term) list -> typ -> term |
|
57 |
|
58 val add_rec_type : (string * bool list) -> theory -> theory |
|
59 val get_rec_tab : theory -> (bool list) Symtab.table |
|
60 val add_deflation_thm : thm -> theory -> theory |
|
61 val get_deflation_thms : theory -> thm list |
|
62 val map_ID_add : attribute |
|
63 val get_map_ID_thms : theory -> thm list |
|
64 val setup : theory -> theory |
|
65 end; |
|
66 |
|
67 structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS = |
|
68 struct |
|
69 |
|
70 type iso_info = |
|
71 { |
|
72 absT : typ, |
|
73 repT : typ, |
|
74 abs_const : term, |
|
75 rep_const : term, |
|
76 abs_inverse : thm, |
|
77 rep_inverse : thm |
|
78 }; |
|
79 |
|
80 type take_info = |
|
81 { take_consts : term list, |
|
82 take_defs : thm list, |
|
83 chain_take_thms : thm list, |
|
84 take_0_thms : thm list, |
|
85 take_Suc_thms : thm list, |
|
86 deflation_take_thms : thm list, |
|
87 take_strict_thms : thm list, |
|
88 finite_consts : term list, |
|
89 finite_defs : thm list |
|
90 }; |
|
91 |
|
92 type take_induct_info = |
|
93 { |
|
94 take_consts : term list, |
|
95 take_defs : thm list, |
|
96 chain_take_thms : thm list, |
|
97 take_0_thms : thm list, |
|
98 take_Suc_thms : thm list, |
|
99 deflation_take_thms : thm list, |
|
100 take_strict_thms : thm list, |
|
101 finite_consts : term list, |
|
102 finite_defs : thm list, |
|
103 lub_take_thms : thm list, |
|
104 reach_thms : thm list, |
|
105 take_lemma_thms : thm list, |
|
106 is_finite : bool, |
|
107 take_induct_thms : thm list |
|
108 }; |
|
109 |
|
110 val beta_rules = |
|
111 @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @ |
|
112 @{thms cont2cont_fst cont2cont_snd cont2cont_Pair}; |
|
113 |
|
114 val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules); |
|
115 |
|
116 val beta_tac = simp_tac beta_ss; |
|
117 |
|
118 (******************************************************************************) |
|
119 (******************************** theory data *********************************) |
|
120 (******************************************************************************) |
|
121 |
|
122 structure Rec_Data = Theory_Data |
|
123 ( |
|
124 (* list indicates which type arguments allow indirect recursion *) |
|
125 type T = (bool list) Symtab.table; |
|
126 val empty = Symtab.empty; |
|
127 val extend = I; |
|
128 fun merge data = Symtab.merge (K true) data; |
|
129 ); |
|
130 |
|
131 structure DeflMapData = Named_Thms |
|
132 ( |
|
133 val name = "domain_deflation" |
|
134 val description = "theorems like deflation a ==> deflation (foo_map$a)" |
|
135 ); |
|
136 |
|
137 structure Map_Id_Data = Named_Thms |
|
138 ( |
|
139 val name = "domain_map_ID" |
|
140 val description = "theorems like foo_map$ID = ID" |
|
141 ); |
|
142 |
|
143 fun add_rec_type (tname, bs) = |
|
144 Rec_Data.map (Symtab.insert (K true) (tname, bs)); |
|
145 |
|
146 fun add_deflation_thm thm = |
|
147 Context.theory_map (DeflMapData.add_thm thm); |
|
148 |
|
149 val get_rec_tab = Rec_Data.get; |
|
150 fun get_deflation_thms thy = DeflMapData.get (ProofContext.init_global thy); |
|
151 |
|
152 val map_ID_add = Map_Id_Data.add; |
|
153 val get_map_ID_thms = Map_Id_Data.get o ProofContext.init_global; |
|
154 |
|
155 val setup = DeflMapData.setup #> Map_Id_Data.setup; |
|
156 |
|
157 (******************************************************************************) |
|
158 (************************** building types and terms **************************) |
|
159 (******************************************************************************) |
|
160 |
|
161 open HOLCF_Library; |
|
162 |
|
163 infixr 6 ->>; |
|
164 infix -->>; |
|
165 infix 9 `; |
|
166 |
|
167 fun mapT (T as Type (_, Ts)) = |
|
168 (map (fn T => T ->> T) Ts) -->> (T ->> T) |
|
169 | mapT T = T ->> T; |
|
170 |
|
171 fun mk_deflation t = |
|
172 Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t; |
|
173 |
|
174 fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)); |
|
175 |
|
176 (******************************************************************************) |
|
177 (****************************** isomorphism info ******************************) |
|
178 (******************************************************************************) |
|
179 |
|
180 fun deflation_abs_rep (info : iso_info) : thm = |
|
181 let |
|
182 val abs_iso = #abs_inverse info; |
|
183 val rep_iso = #rep_inverse info; |
|
184 val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso]; |
|
185 in |
|
186 Drule.zero_var_indexes thm |
|
187 end |
|
188 |
|
189 (******************************************************************************) |
|
190 (********************* building map functions over types **********************) |
|
191 (******************************************************************************) |
|
192 |
|
193 fun map_of_typ (thy : theory) (sub : (typ * term) list) (T : typ) : term = |
|
194 let |
|
195 val thms = get_map_ID_thms thy; |
|
196 val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) thms; |
|
197 val rules' = map (apfst mk_ID) sub @ map swap rules; |
|
198 in |
|
199 mk_ID T |
|
200 |> Pattern.rewrite_term thy rules' [] |
|
201 |> Pattern.rewrite_term thy rules [] |
|
202 end; |
|
203 |
|
204 (******************************************************************************) |
|
205 (********************* declaring definitions and theorems *********************) |
|
206 (******************************************************************************) |
|
207 |
|
208 fun add_qualified_def name (dbind, eqn) = |
|
209 yield_singleton (Global_Theory.add_defs false) |
|
210 ((Binding.qualified true name dbind, eqn), []); |
|
211 |
|
212 fun add_qualified_thm name (dbind, thm) = |
|
213 yield_singleton Global_Theory.add_thms |
|
214 ((Binding.qualified true name dbind, thm), []); |
|
215 |
|
216 fun add_qualified_simp_thm name (dbind, thm) = |
|
217 yield_singleton Global_Theory.add_thms |
|
218 ((Binding.qualified true name dbind, thm), [Simplifier.simp_add]); |
|
219 |
|
220 (******************************************************************************) |
|
221 (************************** defining take functions ***************************) |
|
222 (******************************************************************************) |
|
223 |
|
224 fun define_take_functions |
|
225 (spec : (binding * iso_info) list) |
|
226 (thy : theory) = |
|
227 let |
|
228 |
|
229 (* retrieve components of spec *) |
|
230 val dbinds = map fst spec; |
|
231 val iso_infos = map snd spec; |
|
232 val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos; |
|
233 val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos; |
|
234 |
|
235 fun mk_projs [] t = [] |
|
236 | mk_projs (x::[]) t = [(x, t)] |
|
237 | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t); |
|
238 |
|
239 fun mk_cfcomp2 ((rep_const, abs_const), f) = |
|
240 mk_cfcomp (abs_const, mk_cfcomp (f, rep_const)); |
|
241 |
|
242 (* define take functional *) |
|
243 val newTs : typ list = map fst dom_eqns; |
|
244 val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs); |
|
245 val copy_arg = Free ("f", copy_arg_type); |
|
246 val copy_args = map snd (mk_projs dbinds copy_arg); |
|
247 fun one_copy_rhs (rep_abs, (lhsT, rhsT)) = |
|
248 let |
|
249 val body = map_of_typ thy (newTs ~~ copy_args) rhsT; |
|
250 in |
|
251 mk_cfcomp2 (rep_abs, body) |
|
252 end; |
|
253 val take_functional = |
|
254 big_lambda copy_arg |
|
255 (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns))); |
|
256 val take_rhss = |
|
257 let |
|
258 val n = Free ("n", HOLogic.natT); |
|
259 val rhs = mk_iterate (n, take_functional); |
|
260 in |
|
261 map (lambda n o snd) (mk_projs dbinds rhs) |
|
262 end; |
|
263 |
|
264 (* define take constants *) |
|
265 fun define_take_const ((dbind, take_rhs), (lhsT, rhsT)) thy = |
|
266 let |
|
267 val take_type = HOLogic.natT --> lhsT ->> lhsT; |
|
268 val take_bind = Binding.suffix_name "_take" dbind; |
|
269 val (take_const, thy) = |
|
270 Sign.declare_const ((take_bind, take_type), NoSyn) thy; |
|
271 val take_eqn = Logic.mk_equals (take_const, take_rhs); |
|
272 val (take_def_thm, thy) = |
|
273 add_qualified_def "take_def" (dbind, take_eqn) thy; |
|
274 in ((take_const, take_def_thm), thy) end; |
|
275 val ((take_consts, take_defs), thy) = thy |
|
276 |> fold_map define_take_const (dbinds ~~ take_rhss ~~ dom_eqns) |
|
277 |>> ListPair.unzip; |
|
278 |
|
279 (* prove chain_take lemmas *) |
|
280 fun prove_chain_take (take_const, dbind) thy = |
|
281 let |
|
282 val goal = mk_trp (mk_chain take_const); |
|
283 val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd}; |
|
284 val tac = simp_tac (HOL_basic_ss addsimps rules) 1; |
|
285 val thm = Goal.prove_global thy [] [] goal (K tac); |
|
286 in |
|
287 add_qualified_simp_thm "chain_take" (dbind, thm) thy |
|
288 end; |
|
289 val (chain_take_thms, thy) = |
|
290 fold_map prove_chain_take (take_consts ~~ dbinds) thy; |
|
291 |
|
292 (* prove take_0 lemmas *) |
|
293 fun prove_take_0 ((take_const, dbind), (lhsT, rhsT)) thy = |
|
294 let |
|
295 val lhs = take_const $ @{term "0::nat"}; |
|
296 val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT)); |
|
297 val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict}; |
|
298 val tac = simp_tac (HOL_basic_ss addsimps rules) 1; |
|
299 val take_0_thm = Goal.prove_global thy [] [] goal (K tac); |
|
300 in |
|
301 add_qualified_simp_thm "take_0" (dbind, take_0_thm) thy |
|
302 end; |
|
303 val (take_0_thms, thy) = |
|
304 fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy; |
|
305 |
|
306 (* prove take_Suc lemmas *) |
|
307 val n = Free ("n", natT); |
|
308 val take_is = map (fn t => t $ n) take_consts; |
|
309 fun prove_take_Suc |
|
310 (((take_const, rep_abs), dbind), (lhsT, rhsT)) thy = |
|
311 let |
|
312 val lhs = take_const $ (@{term Suc} $ n); |
|
313 val body = map_of_typ thy (newTs ~~ take_is) rhsT; |
|
314 val rhs = mk_cfcomp2 (rep_abs, body); |
|
315 val goal = mk_eqs (lhs, rhs); |
|
316 val simps = @{thms iterate_Suc fst_conv snd_conv} |
|
317 val rules = take_defs @ simps; |
|
318 val tac = simp_tac (beta_ss addsimps rules) 1; |
|
319 val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac); |
|
320 in |
|
321 add_qualified_thm "take_Suc" (dbind, take_Suc_thm) thy |
|
322 end; |
|
323 val (take_Suc_thms, thy) = |
|
324 fold_map prove_take_Suc |
|
325 (take_consts ~~ rep_abs_consts ~~ dbinds ~~ dom_eqns) thy; |
|
326 |
|
327 (* prove deflation theorems for take functions *) |
|
328 val deflation_abs_rep_thms = map deflation_abs_rep iso_infos; |
|
329 val deflation_take_thm = |
|
330 let |
|
331 val n = Free ("n", natT); |
|
332 fun mk_goal take_const = mk_deflation (take_const $ n); |
|
333 val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts)); |
|
334 val adm_rules = |
|
335 @{thms adm_conj adm_subst [OF _ adm_deflation] |
|
336 cont2cont_fst cont2cont_snd cont_id}; |
|
337 val bottom_rules = |
|
338 take_0_thms @ @{thms deflation_UU simp_thms}; |
|
339 val deflation_rules = |
|
340 @{thms conjI deflation_ID} |
|
341 @ deflation_abs_rep_thms |
|
342 @ get_deflation_thms thy; |
|
343 in |
|
344 Goal.prove_global thy [] [] goal (fn _ => |
|
345 EVERY |
|
346 [rtac @{thm nat.induct} 1, |
|
347 simp_tac (HOL_basic_ss addsimps bottom_rules) 1, |
|
348 asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1, |
|
349 REPEAT (etac @{thm conjE} 1 |
|
350 ORELSE resolve_tac deflation_rules 1 |
|
351 ORELSE atac 1)]) |
|
352 end; |
|
353 fun conjuncts [] thm = [] |
|
354 | conjuncts (n::[]) thm = [(n, thm)] |
|
355 | conjuncts (n::ns) thm = let |
|
356 val thmL = thm RS @{thm conjunct1}; |
|
357 val thmR = thm RS @{thm conjunct2}; |
|
358 in (n, thmL):: conjuncts ns thmR end; |
|
359 val (deflation_take_thms, thy) = |
|
360 fold_map (add_qualified_thm "deflation_take") |
|
361 (map (apsnd Drule.zero_var_indexes) |
|
362 (conjuncts dbinds deflation_take_thm)) thy; |
|
363 |
|
364 (* prove strictness of take functions *) |
|
365 fun prove_take_strict (deflation_take, dbind) thy = |
|
366 let |
|
367 val take_strict_thm = |
|
368 Drule.zero_var_indexes |
|
369 (@{thm deflation_strict} OF [deflation_take]); |
|
370 in |
|
371 add_qualified_simp_thm "take_strict" (dbind, take_strict_thm) thy |
|
372 end; |
|
373 val (take_strict_thms, thy) = |
|
374 fold_map prove_take_strict |
|
375 (deflation_take_thms ~~ dbinds) thy; |
|
376 |
|
377 (* prove take/take rules *) |
|
378 fun prove_take_take ((chain_take, deflation_take), dbind) thy = |
|
379 let |
|
380 val take_take_thm = |
|
381 Drule.zero_var_indexes |
|
382 (@{thm deflation_chain_min} OF [chain_take, deflation_take]); |
|
383 in |
|
384 add_qualified_thm "take_take" (dbind, take_take_thm) thy |
|
385 end; |
|
386 val (take_take_thms, thy) = |
|
387 fold_map prove_take_take |
|
388 (chain_take_thms ~~ deflation_take_thms ~~ dbinds) thy; |
|
389 |
|
390 (* prove take_below rules *) |
|
391 fun prove_take_below (deflation_take, dbind) thy = |
|
392 let |
|
393 val take_below_thm = |
|
394 Drule.zero_var_indexes |
|
395 (@{thm deflation.below} OF [deflation_take]); |
|
396 in |
|
397 add_qualified_thm "take_below" (dbind, take_below_thm) thy |
|
398 end; |
|
399 val (take_below_thms, thy) = |
|
400 fold_map prove_take_below |
|
401 (deflation_take_thms ~~ dbinds) thy; |
|
402 |
|
403 (* define finiteness predicates *) |
|
404 fun define_finite_const ((dbind, take_const), (lhsT, rhsT)) thy = |
|
405 let |
|
406 val finite_type = lhsT --> boolT; |
|
407 val finite_bind = Binding.suffix_name "_finite" dbind; |
|
408 val (finite_const, thy) = |
|
409 Sign.declare_const ((finite_bind, finite_type), NoSyn) thy; |
|
410 val x = Free ("x", lhsT); |
|
411 val n = Free ("n", natT); |
|
412 val finite_rhs = |
|
413 lambda x (HOLogic.exists_const natT $ |
|
414 (lambda n (mk_eq (mk_capply (take_const $ n, x), x)))); |
|
415 val finite_eqn = Logic.mk_equals (finite_const, finite_rhs); |
|
416 val (finite_def_thm, thy) = |
|
417 add_qualified_def "finite_def" (dbind, finite_eqn) thy; |
|
418 in ((finite_const, finite_def_thm), thy) end; |
|
419 val ((finite_consts, finite_defs), thy) = thy |
|
420 |> fold_map define_finite_const (dbinds ~~ take_consts ~~ dom_eqns) |
|
421 |>> ListPair.unzip; |
|
422 |
|
423 val result = |
|
424 { |
|
425 take_consts = take_consts, |
|
426 take_defs = take_defs, |
|
427 chain_take_thms = chain_take_thms, |
|
428 take_0_thms = take_0_thms, |
|
429 take_Suc_thms = take_Suc_thms, |
|
430 deflation_take_thms = deflation_take_thms, |
|
431 take_strict_thms = take_strict_thms, |
|
432 finite_consts = finite_consts, |
|
433 finite_defs = finite_defs |
|
434 }; |
|
435 |
|
436 in |
|
437 (result, thy) |
|
438 end; |
|
439 |
|
440 fun prove_finite_take_induct |
|
441 (spec : (binding * iso_info) list) |
|
442 (take_info : take_info) |
|
443 (lub_take_thms : thm list) |
|
444 (thy : theory) = |
|
445 let |
|
446 val dbinds = map fst spec; |
|
447 val iso_infos = map snd spec; |
|
448 val absTs = map #absT iso_infos; |
|
449 val {take_consts, ...} = take_info; |
|
450 val {chain_take_thms, take_0_thms, take_Suc_thms, ...} = take_info; |
|
451 val {finite_consts, finite_defs, ...} = take_info; |
|
452 |
|
453 val decisive_lemma = |
|
454 let |
|
455 fun iso_locale (info : iso_info) = |
|
456 @{thm iso.intro} OF [#abs_inverse info, #rep_inverse info]; |
|
457 val iso_locale_thms = map iso_locale iso_infos; |
|
458 val decisive_abs_rep_thms = |
|
459 map (fn x => @{thm decisive_abs_rep} OF [x]) iso_locale_thms; |
|
460 val n = Free ("n", @{typ nat}); |
|
461 fun mk_decisive t = |
|
462 Const (@{const_name decisive}, fastype_of t --> boolT) $ t; |
|
463 fun f take_const = mk_decisive (take_const $ n); |
|
464 val goal = mk_trp (foldr1 mk_conj (map f take_consts)); |
|
465 val rules0 = @{thm decisive_bottom} :: take_0_thms; |
|
466 val rules1 = |
|
467 take_Suc_thms @ decisive_abs_rep_thms |
|
468 @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map}; |
|
469 val tac = EVERY [ |
|
470 rtac @{thm nat.induct} 1, |
|
471 simp_tac (HOL_ss addsimps rules0) 1, |
|
472 asm_simp_tac (HOL_ss addsimps rules1) 1]; |
|
473 in Goal.prove_global thy [] [] goal (K tac) end; |
|
474 fun conjuncts 1 thm = [thm] |
|
475 | conjuncts n thm = let |
|
476 val thmL = thm RS @{thm conjunct1}; |
|
477 val thmR = thm RS @{thm conjunct2}; |
|
478 in thmL :: conjuncts (n-1) thmR end; |
|
479 val decisive_thms = conjuncts (length spec) decisive_lemma; |
|
480 |
|
481 fun prove_finite_thm (absT, finite_const) = |
|
482 let |
|
483 val goal = mk_trp (finite_const $ Free ("x", absT)); |
|
484 val tac = |
|
485 EVERY [ |
|
486 rewrite_goals_tac finite_defs, |
|
487 rtac @{thm lub_ID_finite} 1, |
|
488 resolve_tac chain_take_thms 1, |
|
489 resolve_tac lub_take_thms 1, |
|
490 resolve_tac decisive_thms 1]; |
|
491 in |
|
492 Goal.prove_global thy [] [] goal (K tac) |
|
493 end; |
|
494 val finite_thms = |
|
495 map prove_finite_thm (absTs ~~ finite_consts); |
|
496 |
|
497 fun prove_take_induct ((ch_take, lub_take), decisive) = |
|
498 Drule.export_without_context |
|
499 (@{thm lub_ID_finite_take_induct} OF [ch_take, lub_take, decisive]); |
|
500 val take_induct_thms = |
|
501 map prove_take_induct |
|
502 (chain_take_thms ~~ lub_take_thms ~~ decisive_thms); |
|
503 |
|
504 val thy = thy |
|
505 |> fold (snd oo add_qualified_thm "finite") |
|
506 (dbinds ~~ finite_thms) |
|
507 |> fold (snd oo add_qualified_thm "take_induct") |
|
508 (dbinds ~~ take_induct_thms); |
|
509 in |
|
510 ((finite_thms, take_induct_thms), thy) |
|
511 end; |
|
512 |
|
513 fun add_lub_take_theorems |
|
514 (spec : (binding * iso_info) list) |
|
515 (take_info : take_info) |
|
516 (lub_take_thms : thm list) |
|
517 (thy : theory) = |
|
518 let |
|
519 |
|
520 (* retrieve components of spec *) |
|
521 val dbinds = map fst spec; |
|
522 val iso_infos = map snd spec; |
|
523 val absTs = map #absT iso_infos; |
|
524 val repTs = map #repT iso_infos; |
|
525 val {take_consts, take_0_thms, take_Suc_thms, ...} = take_info; |
|
526 val {chain_take_thms, deflation_take_thms, ...} = take_info; |
|
527 |
|
528 (* prove take lemmas *) |
|
529 fun prove_take_lemma ((chain_take, lub_take), dbind) thy = |
|
530 let |
|
531 val take_lemma = |
|
532 Drule.export_without_context |
|
533 (@{thm lub_ID_take_lemma} OF [chain_take, lub_take]); |
|
534 in |
|
535 add_qualified_thm "take_lemma" (dbind, take_lemma) thy |
|
536 end; |
|
537 val (take_lemma_thms, thy) = |
|
538 fold_map prove_take_lemma |
|
539 (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy; |
|
540 |
|
541 (* prove reach lemmas *) |
|
542 fun prove_reach_lemma ((chain_take, lub_take), dbind) thy = |
|
543 let |
|
544 val thm = |
|
545 Drule.zero_var_indexes |
|
546 (@{thm lub_ID_reach} OF [chain_take, lub_take]); |
|
547 in |
|
548 add_qualified_thm "reach" (dbind, thm) thy |
|
549 end; |
|
550 val (reach_thms, thy) = |
|
551 fold_map prove_reach_lemma |
|
552 (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy; |
|
553 |
|
554 (* test for finiteness of domain definitions *) |
|
555 local |
|
556 val types = [@{type_name ssum}, @{type_name sprod}]; |
|
557 fun finite d T = if member (op =) absTs T then d else finite' d T |
|
558 and finite' d (Type (c, Ts)) = |
|
559 let val d' = d andalso member (op =) types c; |
|
560 in forall (finite d') Ts end |
|
561 | finite' d _ = true; |
|
562 in |
|
563 val is_finite = forall (finite true) repTs; |
|
564 end; |
|
565 |
|
566 val ((finite_thms, take_induct_thms), thy) = |
|
567 if is_finite |
|
568 then |
|
569 let |
|
570 val ((finites, take_inducts), thy) = |
|
571 prove_finite_take_induct spec take_info lub_take_thms thy; |
|
572 in |
|
573 ((SOME finites, take_inducts), thy) |
|
574 end |
|
575 else |
|
576 let |
|
577 fun prove_take_induct (chain_take, lub_take) = |
|
578 Drule.zero_var_indexes |
|
579 (@{thm lub_ID_take_induct} OF [chain_take, lub_take]); |
|
580 val take_inducts = |
|
581 map prove_take_induct (chain_take_thms ~~ lub_take_thms); |
|
582 val thy = fold (snd oo add_qualified_thm "take_induct") |
|
583 (dbinds ~~ take_inducts) thy; |
|
584 in |
|
585 ((NONE, take_inducts), thy) |
|
586 end; |
|
587 |
|
588 val result = |
|
589 { |
|
590 take_consts = #take_consts take_info, |
|
591 take_defs = #take_defs take_info, |
|
592 chain_take_thms = #chain_take_thms take_info, |
|
593 take_0_thms = #take_0_thms take_info, |
|
594 take_Suc_thms = #take_Suc_thms take_info, |
|
595 deflation_take_thms = #deflation_take_thms take_info, |
|
596 take_strict_thms = #take_strict_thms take_info, |
|
597 finite_consts = #finite_consts take_info, |
|
598 finite_defs = #finite_defs take_info, |
|
599 lub_take_thms = lub_take_thms, |
|
600 reach_thms = reach_thms, |
|
601 take_lemma_thms = take_lemma_thms, |
|
602 is_finite = is_finite, |
|
603 take_induct_thms = take_induct_thms |
|
604 }; |
|
605 in |
|
606 (result, thy) |
|
607 end; |
|
608 |
|
609 end; |
|