175 val rep_strict = ax_abs_iso RS (allI RS retraction_strict); |
177 val rep_strict = ax_abs_iso RS (allI RS retraction_strict); |
176 val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict]; |
178 val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict]; |
177 |
179 |
178 (* ----- theorems concerning one induction step ----------------------------- *) |
180 (* ----- theorems concerning one induction step ----------------------------- *) |
179 |
181 |
180 val copy_strict = |
|
181 let |
|
182 val _ = trace " Proving copy_strict..."; |
|
183 val goal = mk_trp (strict (dc_copy `% "f")); |
|
184 val rules = [abs_strict, rep_strict] @ @{thms domain_map_stricts}; |
|
185 val tacs = [asm_simp_tac (HOLCF_ss addsimps rules) 1]; |
|
186 in |
|
187 SOME (pg [ax_copy_def] goal (K tacs)) |
|
188 handle |
|
189 THM (s, _, _) => (trace s; NONE) |
|
190 | ERROR s => (trace s; NONE) |
|
191 end; |
|
192 |
|
193 local |
182 local |
194 fun copy_app (con, _, args) = |
183 fun dc_take dn = %%:(dn^"_take"); |
195 let |
184 val dnames = map (fst o fst) eqs; |
196 val lhs = dc_copy`%"f"`(con_app con args); |
185 fun get_take_strict dn = PureThy.get_thm thy (dn ^ ".take_strict"); |
|
186 val axs_take_strict = map get_take_strict dnames; |
|
187 |
|
188 fun one_take_app (con, _, args) = |
|
189 let |
|
190 fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n"; |
197 fun one_rhs arg = |
191 fun one_rhs arg = |
198 if Datatype_Aux.is_rec_type (dtyp_of arg) |
192 if Datatype_Aux.is_rec_type (dtyp_of arg) |
199 then Domain_Axioms.copy_of_dtyp map_tab |
193 then Domain_Axioms.copy_of_dtyp map_tab |
200 (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg) |
194 mk_take (dtyp_of arg) ` (%# arg) |
201 else (%# arg); |
195 else (%# arg); |
|
196 val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args); |
202 val rhs = con_app2 con one_rhs args; |
197 val rhs = con_app2 con one_rhs args; |
203 fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg); |
198 fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg); |
204 fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); |
199 fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); |
205 fun nonlazy_rec args = map vname (filter is_nonlazy_rec args); |
200 fun nonlazy_rec args = map vname (filter is_nonlazy_rec args); |
206 val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); |
201 val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); |
207 val args' = filter_out (fn a => is_rec a orelse is_lazy a) args; |
202 val goal = mk_trp (lhs === rhs); |
208 val stricts = abs_strict :: rep_strict :: @{thms domain_map_stricts}; |
203 val rules = [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}]; |
209 (* FIXME! case_UU_tac *) |
204 val rules2 = @{thms take_con_rules ID1} @ axs_take_strict; |
210 fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args'; |
205 val tacs = |
211 val rules = [ax_abs_iso] @ @{thms domain_map_simps}; |
206 [simp_tac (HOL_basic_ss addsimps rules) 1, |
212 val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1]; |
207 asm_simp_tac (HOL_basic_ss addsimps rules2) 1]; |
213 in pg (ax_copy_def::con_appls) goal (fn ctxt => (tacs1 ctxt @ tacs2)) end; |
208 in pg con_appls goal (K tacs) end; |
|
209 val take_apps = map (Drule.export_without_context o one_take_app) cons; |
214 in |
210 in |
215 val _ = trace " Proving copy_apps..."; |
211 val take_rews = ax_take_0 :: ax_take_strict :: take_apps; |
216 val copy_apps = map copy_app cons; |
|
217 end; |
212 end; |
218 |
|
219 local |
|
220 fun one_strict (con, _, args) = |
|
221 let |
|
222 val goal = mk_trp (dc_copy`UU`(con_app con args) === UU); |
|
223 val rews = the_list copy_strict @ copy_apps @ con_rews; |
|
224 (* FIXME! case_UU_tac *) |
|
225 fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @ |
|
226 [asm_simp_tac (HOLCF_ss addsimps rews) 1]; |
|
227 in |
|
228 SOME (pg [] goal tacs) |
|
229 handle |
|
230 THM (s, _, _) => (trace s; NONE) |
|
231 | ERROR s => (trace s; NONE) |
|
232 end; |
|
233 |
|
234 fun has_nonlazy_rec (_, _, args) = exists is_nonlazy_rec args; |
|
235 in |
|
236 val _ = trace " Proving copy_stricts..."; |
|
237 val copy_stricts = map_filter one_strict (filter has_nonlazy_rec cons); |
|
238 end; |
|
239 |
|
240 val copy_rews = the_list copy_strict @ copy_apps @ copy_stricts; |
|
241 |
213 |
242 in |
214 in |
243 thy |
215 thy |
244 |> Sign.add_path (Long_Name.base_name dname) |
216 |> Sign.add_path (Long_Name.base_name dname) |
245 |> snd o PureThy.add_thmss [ |
217 |> snd o PureThy.add_thmss [ |
255 ((Binding.name "pat_rews" , pat_rews ), [Simplifier.simp_add]), |
227 ((Binding.name "pat_rews" , pat_rews ), [Simplifier.simp_add]), |
256 ((Binding.name "dist_les" , dist_les ), [Simplifier.simp_add]), |
228 ((Binding.name "dist_les" , dist_les ), [Simplifier.simp_add]), |
257 ((Binding.name "dist_eqs" , dist_eqs ), [Simplifier.simp_add]), |
229 ((Binding.name "dist_eqs" , dist_eqs ), [Simplifier.simp_add]), |
258 ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]), |
230 ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]), |
259 ((Binding.name "injects" , injects ), [Simplifier.simp_add]), |
231 ((Binding.name "injects" , injects ), [Simplifier.simp_add]), |
260 ((Binding.name "copy_rews" , copy_rews ), [Simplifier.simp_add]), |
232 ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]), |
261 ((Binding.name "match_rews", mat_rews ), |
233 ((Binding.name "match_rews", mat_rews ), |
262 [Simplifier.simp_add, Fixrec.fixrec_simp_add])] |
234 [Simplifier.simp_add, Fixrec.fixrec_simp_add])] |
263 |> Sign.parent_path |
235 |> Sign.parent_path |
264 |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ |
236 |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ |
265 pat_rews @ dist_les @ dist_eqs @ copy_rews) |
237 pat_rews @ dist_les @ dist_eqs) |
266 end; (* let *) |
238 end; (* let *) |
267 |
239 |
268 fun comp_theorems (comp_dnam, eqs: eq list) thy = |
240 fun comp_theorems (comp_dnam, eqs: eq list) thy = |
269 let |
241 let |
270 val global_ctxt = ProofContext.init thy; |
242 val global_ctxt = ProofContext.init thy; |
280 (* ----- getting the composite axiom and definitions ------------------------ *) |
252 (* ----- getting the composite axiom and definitions ------------------------ *) |
281 |
253 |
282 local |
254 local |
283 fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); |
255 fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); |
284 in |
256 in |
285 val axs_reach = map (ga "reach" ) dnames; |
|
286 val axs_take_def = map (ga "take_def" ) dnames; |
257 val axs_take_def = map (ga "take_def" ) dnames; |
|
258 val axs_chain_take = map (ga "chain_take") dnames; |
|
259 val axs_lub_take = map (ga "lub_take" ) dnames; |
287 val axs_finite_def = map (ga "finite_def") dnames; |
260 val axs_finite_def = map (ga "finite_def") dnames; |
288 val ax_copy2_def = ga "copy_def" comp_dnam; |
|
289 (* TEMPORARILY DISABLED |
261 (* TEMPORARILY DISABLED |
290 val ax_bisim_def = ga "bisim_def" comp_dnam; |
262 val ax_bisim_def = ga "bisim_def" comp_dnam; |
291 TEMPORARILY DISABLED *) |
263 TEMPORARILY DISABLED *) |
292 end; |
264 end; |
293 |
265 |
295 fun gt s dn = PureThy.get_thm thy (dn ^ "." ^ s); |
267 fun gt s dn = PureThy.get_thm thy (dn ^ "." ^ s); |
296 fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s); |
268 fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s); |
297 in |
269 in |
298 val cases = map (gt "casedist" ) dnames; |
270 val cases = map (gt "casedist" ) dnames; |
299 val con_rews = maps (gts "con_rews" ) dnames; |
271 val con_rews = maps (gts "con_rews" ) dnames; |
300 val copy_rews = maps (gts "copy_rews") dnames; |
|
301 end; |
272 end; |
302 |
273 |
303 fun dc_take dn = %%:(dn^"_take"); |
274 fun dc_take dn = %%:(dn^"_take"); |
304 val x_name = idx_name dnames "x"; |
275 val x_name = idx_name dnames "x"; |
305 val P_name = idx_name dnames "P"; |
276 val P_name = idx_name dnames "P"; |
306 val n_eqs = length eqs; |
277 val n_eqs = length eqs; |
307 |
278 |
308 (* ----- theorems concerning finite approximation and finite induction ------ *) |
279 (* ----- theorems concerning finite approximation and finite induction ------ *) |
309 |
280 |
310 local |
281 val take_rews = |
311 val iterate_Cprod_ss = global_simpset_of @{theory Fix}; |
282 maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames; |
312 val copy_con_rews = copy_rews @ con_rews; |
|
313 val copy_take_defs = |
|
314 (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def; |
|
315 val _ = trace " Proving take_stricts..."; |
|
316 fun one_take_strict ((dn, args), _) = |
|
317 let |
|
318 val goal = mk_trp (strict (dc_take dn $ %:"n")); |
|
319 val rules = [ |
|
320 @{thm monofun_fst [THEN monofunE]}, |
|
321 @{thm monofun_snd [THEN monofunE]}]; |
|
322 val tacs = [ |
|
323 rtac @{thm UU_I} 1, |
|
324 rtac @{thm below_eq_trans} 1, |
|
325 resolve_tac axs_reach 2, |
|
326 rtac @{thm monofun_cfun_fun} 1, |
|
327 REPEAT (resolve_tac rules 1), |
|
328 rtac @{thm iterate_below_fix} 1]; |
|
329 in pg axs_take_def goal (K tacs) end; |
|
330 val take_stricts = map one_take_strict eqs; |
|
331 fun take_0 n dn = |
|
332 let |
|
333 val goal = mk_trp ((dc_take dn $ @{term "0::nat"}) `% x_name n === UU); |
|
334 in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end; |
|
335 val take_0s = mapn take_0 1 dnames; |
|
336 val _ = trace " Proving take_apps..."; |
|
337 fun one_take_app dn (con, _, args) = |
|
338 let |
|
339 fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n"; |
|
340 fun one_rhs arg = |
|
341 if Datatype_Aux.is_rec_type (dtyp_of arg) |
|
342 then Domain_Axioms.copy_of_dtyp map_tab |
|
343 mk_take (dtyp_of arg) ` (%# arg) |
|
344 else (%# arg); |
|
345 val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args); |
|
346 val rhs = con_app2 con one_rhs args; |
|
347 fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg); |
|
348 fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); |
|
349 fun nonlazy_rec args = map vname (filter is_nonlazy_rec args); |
|
350 val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); |
|
351 val tacs = [asm_simp_tac (HOLCF_ss addsimps copy_con_rews) 1]; |
|
352 in pg copy_take_defs goal (K tacs) end; |
|
353 fun one_take_apps ((dn, _), cons) = map (one_take_app dn) cons; |
|
354 val take_apps = maps one_take_apps eqs; |
|
355 in |
|
356 val take_rews = map Drule.export_without_context |
|
357 (take_stricts @ take_0s @ take_apps); |
|
358 end; (* local *) |
|
359 |
283 |
360 local |
284 local |
361 fun one_con p (con, _, args) = |
285 fun one_con p (con, _, args) = |
362 let |
286 let |
363 val P_names = map P_name (1 upto (length dnames)); |
287 val P_names = map P_name (1 upto (length dnames)); |
373 mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl); |
297 mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl); |
374 |
298 |
375 fun ind_term concf = Library.foldr one_eq |
299 fun ind_term concf = Library.foldr one_eq |
376 (mapn (fn n => fn x => (P_name n, x)) 1 conss, |
300 (mapn (fn n => fn x => (P_name n, x)) 1 conss, |
377 mk_trp (foldr1 mk_conj (mapn concf 1 dnames))); |
301 mk_trp (foldr1 mk_conj (mapn concf 1 dnames))); |
378 val take_ss = HOL_ss addsimps take_rews; |
302 val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews); |
379 fun quant_tac ctxt i = EVERY |
303 fun quant_tac ctxt i = EVERY |
380 (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames); |
304 (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames); |
381 |
305 |
382 fun ind_prems_tac prems = EVERY |
306 fun ind_prems_tac prems = EVERY |
383 (maps (fn cons => |
307 (maps (fn cons => |
447 end; |
371 end; |
448 |
372 |
449 val _ = trace " Proving take_lemmas..."; |
373 val _ = trace " Proving take_lemmas..."; |
450 val take_lemmas = |
374 val take_lemmas = |
451 let |
375 let |
452 fun take_lemma n (dn, ax_reach) = |
376 fun take_lemma (ax_chain_take, ax_lub_take) = |
453 let |
377 @{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take]; |
454 val lhs = dc_take dn $ Bound 0 `%(x_name n); |
378 in map take_lemma (axs_chain_take ~~ axs_lub_take) end; |
455 val rhs = dc_take dn $ Bound 0 `%(x_name n^"'"); |
379 |
456 val concl = mk_trp (%:(x_name n) === %:(x_name n^"'")); |
380 val axs_reach = |
457 val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl; |
381 let |
458 val rules = [contlub_fst RS contlubE RS ssubst, |
382 fun reach (ax_chain_take, ax_lub_take) = |
459 contlub_snd RS contlubE RS ssubst]; |
383 @{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take]; |
460 fun tacf {prems, context} = [ |
384 in map reach (axs_chain_take ~~ axs_lub_take) end; |
461 res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1, |
|
462 res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1, |
|
463 stac fix_def2 1, |
|
464 REPEAT (CHANGED |
|
465 (resolve_tac rules 1 THEN chain_tac 1)), |
|
466 stac contlub_cfun_fun 1, |
|
467 stac contlub_cfun_fun 2, |
|
468 rtac lub_equal 3, |
|
469 chain_tac 1, |
|
470 rtac allI 1, |
|
471 resolve_tac prems 1]; |
|
472 in pg'' thy axs_take_def goal tacf end; |
|
473 in mapn take_lemma 1 (dnames ~~ axs_reach) end; |
|
474 |
385 |
475 (* ----- theorems concerning finiteness and induction ----------------------- *) |
386 (* ----- theorems concerning finiteness and induction ----------------------- *) |
476 |
387 |
477 val _ = trace " Proving finites, ind..."; |
388 val _ = trace " Proving finites, ind..."; |
478 val (finites, ind) = |
389 val (finites, ind) = |
578 fun concf n dn = %:(P_name n) $ %:(x_name n); |
489 fun concf n dn = %:(P_name n) $ %:(x_name n); |
579 in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end; |
490 in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end; |
580 val cont_rules = |
491 val cont_rules = |
581 [cont_id, cont_const, cont2cont_Rep_CFun, |
492 [cont_id, cont_const, cont2cont_Rep_CFun, |
582 cont2cont_fst, cont2cont_snd]; |
493 cont2cont_fst, cont2cont_snd]; |
|
494 val subgoal = |
|
495 let fun p n dn = %:(P_name n) $ (dc_take dn $ Bound 0 `%(x_name n)); |
|
496 in mk_trp (mk_all ("n", foldr1 mk_conj (mapn p 1 dnames))) end; |
|
497 val subgoal' = legacy_infer_term thy subgoal; |
583 fun tacf {prems, context} = |
498 fun tacf {prems, context} = |
584 map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [ |
499 let |
585 quant_tac context 1, |
500 val subtac = |
586 rtac (adm_impl_admw RS wfix_ind) 1, |
501 EVERY [rtac allI 1, rtac finite_ind 1, ind_prems_tac prems]; |
587 REPEAT_DETERM (rtac adm_all 1), |
502 val subthm = Goal.prove context [] [] subgoal' (K subtac); |
588 REPEAT_DETERM ( |
503 in |
589 TRY (rtac adm_conj 1) THEN |
504 map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [ |
590 rtac adm_subst 1 THEN |
505 cut_facts_tac (subthm :: take (length dnames) prems) 1, |
591 REPEAT (resolve_tac cont_rules 1) THEN |
506 REPEAT (rtac @{thm conjI} 1 ORELSE |
592 resolve_tac prems 1), |
507 EVERY [etac @{thm admD [OF _ ch2ch_Rep_CFunL]} 1, |
593 strip_tac 1, |
508 resolve_tac axs_chain_take 1, |
594 rtac (rewrite_rule axs_take_def finite_ind) 1, |
509 asm_simp_tac HOL_basic_ss 1]) |
595 ind_prems_tac prems]; |
510 ] |
|
511 end; |
596 val ind = (pg'' thy [] goal tacf |
512 val ind = (pg'' thy [] goal tacf |
597 handle ERROR _ => |
513 handle ERROR _ => |
598 (warning "Cannot prove infinite induction rule"; TrueI)); |
514 (warning "Cannot prove infinite induction rule"; TrueI) |
|
515 ); |
599 in (finites, ind) end |
516 in (finites, ind) end |
600 ) |
517 ) |
601 handle THM _ => |
518 handle THM _ => |
602 (warning "Induction proofs failed (THM raised)."; ([], TrueI)) |
519 (warning "Induction proofs failed (THM raised)."; ([], TrueI)) |
603 | ERROR _ => |
520 | ERROR _ => |
604 (warning "Cannot prove induction rule"; ([], TrueI)); |
521 (warning "Cannot prove induction rule"; ([], TrueI)); |
605 |
|
606 |
522 |
607 end; (* local *) |
523 end; (* local *) |
608 |
524 |
609 (* ----- theorem concerning coinduction ------------------------------------- *) |
525 (* ----- theorem concerning coinduction ------------------------------------- *) |
610 |
526 |
665 fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]); |
581 fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]); |
666 val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI); |
582 val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI); |
667 |
583 |
668 in thy |> Sign.add_path comp_dnam |
584 in thy |> Sign.add_path comp_dnam |
669 |> snd o PureThy.add_thmss [ |
585 |> snd o PureThy.add_thmss [ |
670 ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]), |
|
671 ((Binding.name "take_lemmas", take_lemmas ), []), |
586 ((Binding.name "take_lemmas", take_lemmas ), []), |
|
587 ((Binding.name "reach" , axs_reach ), []), |
672 ((Binding.name "finites" , finites ), []), |
588 ((Binding.name "finites" , finites ), []), |
673 ((Binding.name "finite_ind" , [finite_ind]), []), |
589 ((Binding.name "finite_ind" , [finite_ind]), []), |
674 ((Binding.name "ind" , [ind] ), [])(*, |
590 ((Binding.name "ind" , [ind] ), [])(*, |
675 ((Binding.name "coind" , [coind] ), [])*)] |
591 ((Binding.name "coind" , [coind] ), [])*)] |
676 |> (if induct_failed then I |
592 |> (if induct_failed then I |