245 val lhs = Term.list_comb (mapBsCs, all_gs) $ |
245 val lhs = Term.list_comb (mapBsCs, all_gs) $ |
246 (Term.list_comb (mapAsBs, passive_ids @ fs) $ x); |
246 (Term.list_comb (mapAsBs, passive_ids @ fs) $ x); |
247 val rhs = |
247 val rhs = |
248 Term.list_comb (mapAsCs, take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x; |
248 Term.list_comb (mapAsCs, take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x; |
249 in |
249 in |
250 Skip_Proof.prove lthy [] [] |
250 Goal.prove_sorry lthy [] [] |
251 (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs))) |
251 (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs))) |
252 (K (mk_map_comp_id_tac map_comp)) |
252 (K (mk_map_comp_id_tac map_comp)) |
253 |> Thm.close_derivation |
253 |> Thm.close_derivation |
254 end; |
254 end; |
255 |
255 |
263 HOLogic.mk_Trueprop |
263 HOLogic.mk_Trueprop |
264 (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z)))); |
264 (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z)))); |
265 val prems = map4 mk_prem (drop m sets) self_fs zs zs'; |
265 val prems = map4 mk_prem (drop m sets) self_fs zs zs'; |
266 val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x); |
266 val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x); |
267 in |
267 in |
268 Skip_Proof.prove lthy [] [] |
268 Goal.prove_sorry lthy [] [] |
269 (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal))) |
269 (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal))) |
270 (K (mk_map_congL_tac m map_cong map_id')) |
270 (K (mk_map_congL_tac m map_cong map_id')) |
271 |> Thm.close_derivation |
271 |> Thm.close_derivation |
272 end; |
272 end; |
273 |
273 |
284 val goals = |
284 val goals = |
285 map4 (fn prem => fn concl => fn x => fn y => |
285 map4 (fn prem => fn concl => fn x => fn y => |
286 fold_rev Logic.all (x :: y :: all_fs) (Logic.mk_implies (prem, concl))) |
286 fold_rev Logic.all (x :: y :: all_fs) (Logic.mk_implies (prem, concl))) |
287 prems concls xFs xFs_copy; |
287 prems concls xFs xFs_copy; |
288 in |
288 in |
289 map (fn goal => Skip_Proof.prove lthy [] [] goal |
289 map (fn goal => Goal.prove_sorry lthy [] [] goal |
290 (K ((hyp_subst_tac THEN' rtac refl) 1)) |> Thm.close_derivation) goals |
290 (K ((hyp_subst_tac THEN' rtac refl) 1)) |> Thm.close_derivation) goals |
291 end; |
291 end; |
292 |
292 |
293 val timer = time (timer "Derived simple theorems"); |
293 val timer = time (timer "Derived simple theorems"); |
294 |
294 |
346 ss zs setssAs; |
346 ss zs setssAs; |
347 val goalss = map3 (fn x => fn prem => fn concls => map (fn concl => |
347 val goalss = map3 (fn x => fn prem => fn concls => map (fn concl => |
348 fold_rev Logic.all (x :: As @ Bs @ ss) |
348 fold_rev Logic.all (x :: As @ Bs @ ss) |
349 (Logic.list_implies (coalg_prem :: [prem], concl))) concls) zs prems conclss; |
349 (Logic.list_implies (coalg_prem :: [prem], concl))) concls) zs prems conclss; |
350 in |
350 in |
351 map (fn goals => map (fn goal => Skip_Proof.prove lthy [] [] goal |
351 map (fn goals => map (fn goal => Goal.prove_sorry lthy [] [] goal |
352 (K (mk_coalg_set_tac coalg_def)) |> Thm.close_derivation) goals) goalss |
352 (K (mk_coalg_set_tac coalg_def)) |> Thm.close_derivation) goals) goalss |
353 end; |
353 end; |
354 |
354 |
355 val coalg_set_thmss' = transpose coalg_set_thmss; |
355 val coalg_set_thmss' = transpose coalg_set_thmss; |
356 |
356 |
359 val tcoalg_thm = |
359 val tcoalg_thm = |
360 let |
360 let |
361 val goal = fold_rev Logic.all ss |
361 val goal = fold_rev Logic.all ss |
362 (HOLogic.mk_Trueprop (mk_tcoalg passiveAs activeAs ss)) |
362 (HOLogic.mk_Trueprop (mk_tcoalg passiveAs activeAs ss)) |
363 in |
363 in |
364 Skip_Proof.prove lthy [] [] goal |
364 Goal.prove_sorry lthy [] [] goal |
365 (K (stac coalg_def 1 THEN CONJ_WRAP |
365 (K (stac coalg_def 1 THEN CONJ_WRAP |
366 (K (EVERY' [rtac ballI, rtac CollectI, |
366 (K (EVERY' [rtac ballI, rtac CollectI, |
367 CONJ_WRAP' (K (EVERY' [rtac @{thm subset_UNIV}])) allAs] 1)) ss)) |
367 CONJ_WRAP' (K (EVERY' [rtac @{thm subset_UNIV}])) allAs] 1)) ss)) |
368 |> Thm.close_derivation |
368 |> Thm.close_derivation |
369 end; |
369 end; |
426 fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs) |
426 fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs) |
427 (Logic.list_implies ([prem, HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B))], |
427 (Logic.list_implies ([prem, HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B))], |
428 mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x)))); |
428 mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x)))); |
429 val elim_goals = map6 mk_elim_goal Bs mapsAsBs fs ss s's zs; |
429 val elim_goals = map6 mk_elim_goal Bs mapsAsBs fs ss s's zs; |
430 fun prove goal = |
430 fun prove goal = |
431 Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |
431 Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |
432 |> Thm.close_derivation; |
432 |> Thm.close_derivation; |
433 in |
433 in |
434 (map prove image_goals, map prove elim_goals) |
434 (map prove image_goals, map prove elim_goals) |
435 end; |
435 end; |
436 |
436 |
439 val mor_incl_thm = |
439 val mor_incl_thm = |
440 let |
440 let |
441 val prems = map2 (HOLogic.mk_Trueprop oo mk_subset) Bs Bs_copy; |
441 val prems = map2 (HOLogic.mk_Trueprop oo mk_subset) Bs Bs_copy; |
442 val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids); |
442 val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids); |
443 in |
443 in |
444 Skip_Proof.prove lthy [] [] |
444 Goal.prove_sorry lthy [] [] |
445 (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl))) |
445 (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl))) |
446 (K (mk_mor_incl_tac mor_def map_id's)) |
446 (K (mk_mor_incl_tac mor_def map_id's)) |
447 |> Thm.close_derivation |
447 |> Thm.close_derivation |
448 end; |
448 end; |
449 |
449 |
455 [HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs), |
455 [HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs), |
456 HOLogic.mk_Trueprop (mk_mor B's s's B''s s''s gs)]; |
456 HOLogic.mk_Trueprop (mk_mor B's s's B''s s''s gs)]; |
457 val concl = |
457 val concl = |
458 HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs)); |
458 HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs)); |
459 in |
459 in |
460 Skip_Proof.prove lthy [] [] |
460 Goal.prove_sorry lthy [] [] |
461 (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ fs @ gs) |
461 (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ fs @ gs) |
462 (Logic.list_implies (prems, concl))) |
462 (Logic.list_implies (prems, concl))) |
463 (K (mk_mor_comp_tac mor_def mor_image'_thms morE_thms map_comp_id_thms)) |
463 (K (mk_mor_comp_tac mor_def mor_image'_thms morE_thms map_comp_id_thms)) |
464 |> Thm.close_derivation |
464 |> Thm.close_derivation |
465 end; |
465 end; |
468 let |
468 let |
469 val prems = map HOLogic.mk_Trueprop |
469 val prems = map HOLogic.mk_Trueprop |
470 (map2 (curry HOLogic.mk_eq) fs_copy fs @ [mk_mor Bs ss B's s's fs]) |
470 (map2 (curry HOLogic.mk_eq) fs_copy fs @ [mk_mor Bs ss B's s's fs]) |
471 val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy); |
471 val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy); |
472 in |
472 in |
473 Skip_Proof.prove lthy [] [] |
473 Goal.prove_sorry lthy [] [] |
474 (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy) |
474 (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy) |
475 (Logic.list_implies (prems, concl))) |
475 (Logic.list_implies (prems, concl))) |
476 (K ((hyp_subst_tac THEN' atac) 1)) |
476 (K ((hyp_subst_tac THEN' atac) 1)) |
477 |> Thm.close_derivation |
477 |> Thm.close_derivation |
478 end; |
478 end; |
483 (HOLogic.mk_comp (Term.list_comb (mapAsBs, passive_ids @ fs), s), |
483 (HOLogic.mk_comp (Term.list_comb (mapAsBs, passive_ids @ fs), s), |
484 HOLogic.mk_comp (s', f)); |
484 HOLogic.mk_comp (s', f)); |
485 val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs; |
485 val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs; |
486 val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's); |
486 val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's); |
487 in |
487 in |
488 Skip_Proof.prove lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs))) |
488 Goal.prove_sorry lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs))) |
489 (K (mk_mor_UNIV_tac morE_thms mor_def)) |
489 (K (mk_mor_UNIV_tac morE_thms mor_def)) |
490 |> Thm.close_derivation |
490 |> Thm.close_derivation |
491 end; |
491 end; |
492 |
492 |
493 val mor_str_thm = |
493 val mor_str_thm = |
494 let |
494 let |
495 val maps = map2 (fn Ds => fn bnf => Term.list_comb |
495 val maps = map2 (fn Ds => fn bnf => Term.list_comb |
496 (mk_map_of_bnf Ds allAs (passiveAs @ FTsAs) bnf, passive_ids @ ss)) Dss bnfs; |
496 (mk_map_of_bnf Ds allAs (passiveAs @ FTsAs) bnf, passive_ids @ ss)) Dss bnfs; |
497 in |
497 in |
498 Skip_Proof.prove lthy [] [] |
498 Goal.prove_sorry lthy [] [] |
499 (fold_rev Logic.all ss (HOLogic.mk_Trueprop |
499 (fold_rev Logic.all ss (HOLogic.mk_Trueprop |
500 (mk_mor active_UNIVs ss (map HOLogic.mk_UNIV FTsAs) maps ss))) |
500 (mk_mor active_UNIVs ss (map HOLogic.mk_UNIV FTsAs) maps ss))) |
501 (K (mk_mor_str_tac ks mor_UNIV_thm)) |
501 (K (mk_mor_str_tac ks mor_UNIV_thm)) |
502 |> Thm.close_derivation |
502 |> Thm.close_derivation |
503 end; |
503 end; |
506 let |
506 let |
507 val maps = map3 (fn s => fn sum_s => fn mapx => |
507 val maps = map3 (fn s => fn sum_s => fn mapx => |
508 mk_sum_case (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ Inls), s), sum_s)) |
508 mk_sum_case (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ Inls), s), sum_s)) |
509 s's sum_ss map_Inls; |
509 s's sum_ss map_Inls; |
510 in |
510 in |
511 Skip_Proof.prove lthy [] [] |
511 Goal.prove_sorry lthy [] [] |
512 (fold_rev Logic.all (s's @ sum_ss) (HOLogic.mk_Trueprop |
512 (fold_rev Logic.all (s's @ sum_ss) (HOLogic.mk_Trueprop |
513 (mk_mor (map HOLogic.mk_UNIV activeBs) s's sum_UNIVs maps Inls))) |
513 (mk_mor (map HOLogic.mk_UNIV activeBs) s's sum_UNIVs maps Inls))) |
514 (K (mk_mor_sum_case_tac ks mor_UNIV_thm)) |
514 (K (mk_mor_sum_case_tac ks mor_UNIV_thm)) |
515 |> Thm.close_derivation |
515 |> Thm.close_derivation |
516 end; |
516 end; |
640 zs_copy (drop m sets) hsetssAs) |
640 zs_copy (drop m sets) hsetssAs) |
641 ss zs setssAs hsetssAs; |
641 ss zs setssAs hsetssAs; |
642 in |
642 in |
643 (map3 (fn goals => fn defs => fn rec_Sucs => |
643 (map3 (fn goals => fn defs => fn rec_Sucs => |
644 map3 (fn goal => fn def => fn rec_Suc => |
644 map3 (fn goal => fn def => fn rec_Suc => |
645 Skip_Proof.prove lthy [] [] goal (K (mk_set_incl_hset_tac def rec_Suc)) |
645 Goal.prove_sorry lthy [] [] goal (K (mk_set_incl_hset_tac def rec_Suc)) |
646 |> Thm.close_derivation) |
646 |> Thm.close_derivation) |
647 goals defs rec_Sucs) |
647 goals defs rec_Sucs) |
648 set_incl_hset_goalss hset_defss hset_rec_Sucss, |
648 set_incl_hset_goalss hset_defss hset_rec_Sucss, |
649 map3 (fn goalss => fn defsi => fn rec_Sucs => |
649 map3 (fn goalss => fn defsi => fn rec_Sucs => |
650 map3 (fn k => fn goals => fn defsk => |
650 map3 (fn k => fn goals => fn defsk => |
651 map4 (fn goal => fn defk => fn defi => fn rec_Suc => |
651 map4 (fn goal => fn defk => fn defi => fn rec_Suc => |
652 Skip_Proof.prove lthy [] [] goal |
652 Goal.prove_sorry lthy [] [] goal |
653 (K (mk_set_hset_incl_hset_tac n [defk, defi] rec_Suc k)) |
653 (K (mk_set_hset_incl_hset_tac n [defk, defi] rec_Suc k)) |
654 |> Thm.close_derivation) |
654 |> Thm.close_derivation) |
655 goals defsk defsi rec_Sucs) |
655 goals defsk defsi rec_Sucs) |
656 ks goalss hset_defss) |
656 ks goalss hset_defss) |
657 set_hset_incl_hset_goalsss hset_defss hset_rec_Sucss) |
657 set_hset_incl_hset_goalsss hset_defss hset_rec_Sucss) |
678 map4 (fn s => fn x => fn sets => fn hsets => |
678 map4 (fn s => fn x => fn sets => fn hsets => |
679 map3 (mk_set_incl_hin s x hsets) (drop m sets) hsetssAs activeAs) |
679 map3 (mk_set_incl_hin s x hsets) (drop m sets) hsetssAs activeAs) |
680 ss zs setssAs hsetssAs; |
680 ss zs setssAs hsetssAs; |
681 in |
681 in |
682 map2 (map2 (fn goal => fn thms => |
682 map2 (map2 (fn goal => fn thms => |
683 Skip_Proof.prove lthy [] [] goal (K (mk_set_incl_hin_tac thms)) |
683 Goal.prove_sorry lthy [] [] goal (K (mk_set_incl_hin_tac thms)) |
684 |> Thm.close_derivation)) |
684 |> Thm.close_derivation)) |
685 set_incl_hin_goalss set_hset_incl_hset_thmsss |
685 set_incl_hin_goalss set_hset_incl_hset_thmsss |
686 end; |
686 end; |
687 |
687 |
688 val hset_minimal_thms = |
688 val hset_minimal_thms = |
714 val ctss = |
714 val ctss = |
715 map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls; |
715 map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls; |
716 in |
716 in |
717 map4 (fn goal => fn cts => fn hset_rec_0s => fn hset_rec_Sucs => |
717 map4 (fn goal => fn cts => fn hset_rec_0s => fn hset_rec_Sucs => |
718 singleton (Proof_Context.export names_lthy lthy) |
718 singleton (Proof_Context.export names_lthy lthy) |
719 (Skip_Proof.prove lthy [] [] goal |
719 (Goal.prove_sorry lthy [] [] goal |
720 (mk_hset_rec_minimal_tac m cts hset_rec_0s hset_rec_Sucs)) |
720 (mk_hset_rec_minimal_tac m cts hset_rec_0s hset_rec_Sucs)) |
721 |> Thm.close_derivation) |
721 |> Thm.close_derivation) |
722 goals ctss hset_rec_0ss' hset_rec_Sucss' |
722 goals ctss hset_rec_0ss' hset_rec_Sucss' |
723 end; |
723 end; |
724 |
724 |
729 val goals = map3 (fn Ks => fn prems => fn concl => |
729 val goals = map3 (fn Ks => fn prems => fn concl => |
730 fold_rev Logic.all (Ks @ ss @ zs) |
730 fold_rev Logic.all (Ks @ ss @ zs) |
731 (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))) Kss premss concls; |
731 (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))) Kss premss concls; |
732 in |
732 in |
733 map3 (fn goal => fn hset_defs => fn hset_rec_minimal => |
733 map3 (fn goal => fn hset_defs => fn hset_rec_minimal => |
734 Skip_Proof.prove lthy [] [] goal |
734 Goal.prove_sorry lthy [] [] goal |
735 (mk_hset_minimal_tac n hset_defs hset_rec_minimal) |
735 (mk_hset_minimal_tac n hset_defs hset_rec_minimal) |
736 |> Thm.close_derivation) |
736 |> Thm.close_derivation) |
737 goals hset_defss' hset_rec_minimal_thms |
737 goals hset_defss' hset_rec_minimal_thms |
738 end; |
738 end; |
739 |
739 |
755 val goals = map (fn concl => |
755 val goals = map (fn concl => |
756 Logic.list_implies ([coalg_prem, mor_prem], HOLogic.mk_Trueprop concl)) concls; |
756 Logic.list_implies ([coalg_prem, mor_prem], HOLogic.mk_Trueprop concl)) concls; |
757 in |
757 in |
758 map5 (fn j => fn goal => fn cts => fn hset_rec_0s => fn hset_rec_Sucs => |
758 map5 (fn j => fn goal => fn cts => fn hset_rec_0s => fn hset_rec_Sucs => |
759 singleton (Proof_Context.export names_lthy lthy) |
759 singleton (Proof_Context.export names_lthy lthy) |
760 (Skip_Proof.prove lthy [] [] goal |
760 (Goal.prove_sorry lthy [] [] goal |
761 (K (mk_mor_hset_rec_tac m n cts j hset_rec_0s hset_rec_Sucs |
761 (K (mk_mor_hset_rec_tac m n cts j hset_rec_0s hset_rec_Sucs |
762 morE_thms set_natural'ss coalg_set_thmss))) |
762 morE_thms set_natural'ss coalg_set_thmss))) |
763 |> Thm.close_derivation) |
763 |> Thm.close_derivation) |
764 ls goals ctss hset_rec_0ss' hset_rec_Sucss' |
764 ls goals ctss hset_rec_0ss' hset_rec_Sucss' |
765 end; |
765 end; |
776 fold_rev Logic.all (x :: As @ Bs @ ss @ B's @ s's @ fs) |
776 fold_rev Logic.all (x :: As @ Bs @ ss @ B's @ s's @ fs) |
777 (Logic.list_implies ([coalg_prem, mor_prem, |
777 (Logic.list_implies ([coalg_prem, mor_prem, |
778 mk_prem x B], mk_concl j T i f x))) ks fs zs Bs) ls passiveAs; |
778 mk_prem x B], mk_concl j T i f x))) ks fs zs Bs) ls passiveAs; |
779 in |
779 in |
780 map3 (map3 (fn goal => fn hset_def => fn mor_hset_rec => |
780 map3 (map3 (fn goal => fn hset_def => fn mor_hset_rec => |
781 Skip_Proof.prove lthy [] [] goal |
781 Goal.prove_sorry lthy [] [] goal |
782 (K (mk_mor_hset_tac hset_def mor_hset_rec)) |
782 (K (mk_mor_hset_tac hset_def mor_hset_rec)) |
783 |> Thm.close_derivation)) |
783 |> Thm.close_derivation)) |
784 goalss hset_defss' mor_hset_rec_thmss |
784 goalss hset_defss' mor_hset_rec_thmss |
785 end; |
785 end; |
786 |
786 |
839 let |
839 let |
840 val prems = map HOLogic.mk_Trueprop |
840 val prems = map HOLogic.mk_Trueprop |
841 (mk_bis As Bs ss B's s's Rs :: map2 (curry HOLogic.mk_eq) Rs_copy Rs) |
841 (mk_bis As Bs ss B's s's Rs :: map2 (curry HOLogic.mk_eq) Rs_copy Rs) |
842 val concl = HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs_copy); |
842 val concl = HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs_copy); |
843 in |
843 in |
844 Skip_Proof.prove lthy [] [] |
844 Goal.prove_sorry lthy [] [] |
845 (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs @ Rs_copy) |
845 (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs @ Rs_copy) |
846 (Logic.list_implies (prems, concl))) |
846 (Logic.list_implies (prems, concl))) |
847 (K ((hyp_subst_tac THEN' atac) 1)) |
847 (K ((hyp_subst_tac THEN' atac) 1)) |
848 |> Thm.close_derivation |
848 |> Thm.close_derivation |
849 end; |
849 end; |
858 |
858 |
859 val rhs = HOLogic.mk_conj |
859 val rhs = HOLogic.mk_conj |
860 (bis_le, Library.foldr1 HOLogic.mk_conj |
860 (bis_le, Library.foldr1 HOLogic.mk_conj |
861 (map6 mk_conjunct Rs ss s's zs z's relsAsBs)) |
861 (map6 mk_conjunct Rs ss s's zs z's relsAsBs)) |
862 in |
862 in |
863 Skip_Proof.prove lthy [] [] |
863 Goal.prove_sorry lthy [] [] |
864 (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs) |
864 (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs) |
865 (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs))) |
865 (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs))) |
866 (K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_congs set_natural'ss)) |
866 (K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_congs set_natural'ss)) |
867 |> Thm.close_derivation |
867 |> Thm.close_derivation |
868 end; |
868 end; |
869 |
869 |
870 val bis_converse_thm = |
870 val bis_converse_thm = |
871 Skip_Proof.prove lthy [] [] |
871 Goal.prove_sorry lthy [] [] |
872 (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs) |
872 (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs) |
873 (Logic.mk_implies |
873 (Logic.mk_implies |
874 (HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs), |
874 (HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs), |
875 HOLogic.mk_Trueprop (mk_bis As B's s's Bs ss (map mk_converse Rs))))) |
875 HOLogic.mk_Trueprop (mk_bis As B's s's Bs ss (map mk_converse Rs))))) |
876 (K (mk_bis_converse_tac m bis_srel_thm srel_congs srel_converses)) |
876 (K (mk_bis_converse_tac m bis_srel_thm srel_congs srel_converses)) |
882 [HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs), |
882 [HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs), |
883 HOLogic.mk_Trueprop (mk_bis As B's s's B''s s''s R's)]; |
883 HOLogic.mk_Trueprop (mk_bis As B's s's B''s s''s R's)]; |
884 val concl = |
884 val concl = |
885 HOLogic.mk_Trueprop (mk_bis As Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's)); |
885 HOLogic.mk_Trueprop (mk_bis As Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's)); |
886 in |
886 in |
887 Skip_Proof.prove lthy [] [] |
887 Goal.prove_sorry lthy [] [] |
888 (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's) |
888 (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's) |
889 (Logic.list_implies (prems, concl))) |
889 (Logic.list_implies (prems, concl))) |
890 (K (mk_bis_O_tac m bis_srel_thm srel_congs srel_Os)) |
890 (K (mk_bis_O_tac m bis_srel_thm srel_congs srel_Os)) |
891 |> Thm.close_derivation |
891 |> Thm.close_derivation |
892 end; |
892 end; |
894 val bis_Gr_thm = |
894 val bis_Gr_thm = |
895 let |
895 let |
896 val concl = |
896 val concl = |
897 HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's (map2 mk_Gr Bs fs)); |
897 HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's (map2 mk_Gr Bs fs)); |
898 in |
898 in |
899 Skip_Proof.prove lthy [] [] |
899 Goal.prove_sorry lthy [] [] |
900 (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ fs) |
900 (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ fs) |
901 (Logic.list_implies ([coalg_prem, mor_prem], concl))) |
901 (Logic.list_implies ([coalg_prem, mor_prem], concl))) |
902 (mk_bis_Gr_tac bis_srel_thm srel_Grs mor_image_thms morE_thms coalg_in_thms) |
902 (mk_bis_Gr_tac bis_srel_thm srel_Grs mor_image_thms morE_thms coalg_in_thms) |
903 |> Thm.close_derivation |
903 |> Thm.close_derivation |
904 end; |
904 end; |
916 HOLogic.mk_Trueprop (mk_Ball Idx |
916 HOLogic.mk_Trueprop (mk_Ball Idx |
917 (Term.absfree idx' (mk_bis As Bs ss B's s's (map (fn R => R $ idx) Ris)))); |
917 (Term.absfree idx' (mk_bis As Bs ss B's s's (map (fn R => R $ idx) Ris)))); |
918 val concl = |
918 val concl = |
919 HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's (map (mk_UNION Idx) Ris)); |
919 HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's (map (mk_UNION Idx) Ris)); |
920 in |
920 in |
921 Skip_Proof.prove lthy [] [] |
921 Goal.prove_sorry lthy [] [] |
922 (fold_rev Logic.all (Idx :: As @ Bs @ ss @ B's @ s's @ Ris) |
922 (fold_rev Logic.all (Idx :: As @ Bs @ ss @ B's @ s's @ Ris) |
923 (Logic.mk_implies (prem, concl))) |
923 (Logic.mk_implies (prem, concl))) |
924 (mk_bis_Union_tac bis_def in_mono'_thms) |
924 (mk_bis_Union_tac bis_def in_mono'_thms) |
925 |> Thm.close_derivation |
925 |> Thm.close_derivation |
926 end; |
926 end; |
972 in |
972 in |
973 Term.list_comb (Const (nth lsbiss (i - 1), lsbisT), args) |
973 Term.list_comb (Const (nth lsbiss (i - 1), lsbisT), args) |
974 end; |
974 end; |
975 |
975 |
976 val sbis_lsbis_thm = |
976 val sbis_lsbis_thm = |
977 Skip_Proof.prove lthy [] [] |
977 Goal.prove_sorry lthy [] [] |
978 (fold_rev Logic.all (As @ Bs @ ss) |
978 (fold_rev Logic.all (As @ Bs @ ss) |
979 (HOLogic.mk_Trueprop (mk_sbis As Bs ss (map (mk_lsbis As Bs ss) ks)))) |
979 (HOLogic.mk_Trueprop (mk_sbis As Bs ss (map (mk_lsbis As Bs ss) ks)))) |
980 (K (mk_sbis_lsbis_tac lsbis_defs bis_Union_thm bis_cong_thm)) |
980 (K (mk_sbis_lsbis_tac lsbis_defs bis_Union_thm bis_cong_thm)) |
981 |> Thm.close_derivation; |
981 |> Thm.close_derivation; |
982 |
982 |
989 let |
989 let |
990 fun mk_concl i R = HOLogic.mk_Trueprop (mk_subset R (mk_lsbis As Bs ss i)); |
990 fun mk_concl i R = HOLogic.mk_Trueprop (mk_subset R (mk_lsbis As Bs ss i)); |
991 val goals = map2 (fn i => fn R => fold_rev Logic.all (As @ Bs @ ss @ sRs) |
991 val goals = map2 (fn i => fn R => fold_rev Logic.all (As @ Bs @ ss @ sRs) |
992 (Logic.mk_implies (sbis_prem, mk_concl i R))) ks sRs; |
992 (Logic.mk_implies (sbis_prem, mk_concl i R))) ks sRs; |
993 in |
993 in |
994 map3 (fn goal => fn i => fn def => Skip_Proof.prove lthy [] [] goal |
994 map3 (fn goal => fn i => fn def => Goal.prove_sorry lthy [] [] goal |
995 (K (mk_incl_lsbis_tac n i def)) |> Thm.close_derivation) goals ks lsbis_defs |
995 (K (mk_incl_lsbis_tac n i def)) |> Thm.close_derivation) goals ks lsbis_defs |
996 end; |
996 end; |
997 |
997 |
998 val equiv_lsbis_thms = |
998 val equiv_lsbis_thms = |
999 let |
999 let |
1000 fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis As Bs ss i)); |
1000 fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis As Bs ss i)); |
1001 val goals = map2 (fn i => fn B => fold_rev Logic.all (As @ Bs @ ss) |
1001 val goals = map2 (fn i => fn B => fold_rev Logic.all (As @ Bs @ ss) |
1002 (Logic.mk_implies (coalg_prem, mk_concl i B))) ks Bs; |
1002 (Logic.mk_implies (coalg_prem, mk_concl i B))) ks Bs; |
1003 in |
1003 in |
1004 map3 (fn goal => fn l_incl => fn incl_l => |
1004 map3 (fn goal => fn l_incl => fn incl_l => |
1005 Skip_Proof.prove lthy [] [] goal |
1005 Goal.prove_sorry lthy [] [] goal |
1006 (K (mk_equiv_lsbis_tac sbis_lsbis_thm l_incl incl_l |
1006 (K (mk_equiv_lsbis_tac sbis_lsbis_thm l_incl incl_l |
1007 bis_Id_on_thm bis_converse_thm bis_O_thm)) |
1007 bis_Id_on_thm bis_converse_thm bis_O_thm)) |
1008 |> Thm.close_derivation) |
1008 |> Thm.close_derivation) |
1009 goals lsbis_incl_thms incl_lsbis_thms |
1009 goals lsbis_incl_thms incl_lsbis_thms |
1010 end; |
1010 end; |
1277 val carTAs_copy = map (mk_carT As_copy) ks; |
1277 val carTAs_copy = map (mk_carT As_copy) ks; |
1278 val strTAs = map2 mk_strT treeFTs ks; |
1278 val strTAs = map2 mk_strT treeFTs ks; |
1279 val hset_strTss = map (fn i => map2 (mk_hset strTAs i) ls passiveAs) ks; |
1279 val hset_strTss = map (fn i => map2 (mk_hset strTAs i) ls passiveAs) ks; |
1280 |
1280 |
1281 val coalgT_thm = |
1281 val coalgT_thm = |
1282 Skip_Proof.prove lthy [] [] |
1282 Goal.prove_sorry lthy [] [] |
1283 (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_coalg As carTAs strTAs))) |
1283 (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_coalg As carTAs strTAs))) |
1284 (mk_coalgT_tac m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_natural'ss) |
1284 (mk_coalgT_tac m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_natural'ss) |
1285 |> Thm.close_derivation; |
1285 |> Thm.close_derivation; |
1286 |
1286 |
1287 val card_of_carT_thms = |
1287 val card_of_carT_thms = |
1292 val rhs = mk_cexp |
1292 val rhs = mk_cexp |
1293 (if m = 0 then ctwo else |
1293 (if m = 0 then ctwo else |
1294 (mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo)) |
1294 (mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo)) |
1295 (mk_cexp sbd sbd); |
1295 (mk_cexp sbd sbd); |
1296 val card_of_carT = |
1296 val card_of_carT = |
1297 Skip_Proof.prove lthy [] [] |
1297 Goal.prove_sorry lthy [] [] |
1298 (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_ordLeq lhs rhs))) |
1298 (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_ordLeq lhs rhs))) |
1299 (K (mk_card_of_carT_tac m isNode_defs sbd_sbd_thm |
1299 (K (mk_card_of_carT_tac m isNode_defs sbd_sbd_thm |
1300 sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds)) |
1300 sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds)) |
1301 |> Thm.close_derivation |
1301 |> Thm.close_derivation |
1302 in |
1302 in |
1321 map3 (mk_goal carT strT) (drop m sets) kks ks) carTAs strTAs tree_setss; |
1321 map3 (mk_goal carT strT) (drop m sets) kks ks) carTAs strTAs tree_setss; |
1322 in |
1322 in |
1323 map6 (fn i => fn goals => |
1323 map6 (fn i => fn goals => |
1324 fn carT_def => fn strT_def => fn isNode_def => fn set_naturals => |
1324 fn carT_def => fn strT_def => fn isNode_def => fn set_naturals => |
1325 map2 (fn goal => fn set_natural => |
1325 map2 (fn goal => fn set_natural => |
1326 Skip_Proof.prove lthy [] [] goal |
1326 Goal.prove_sorry lthy [] [] goal |
1327 (mk_carT_set_tac n i carT_def strT_def isNode_def set_natural) |
1327 (mk_carT_set_tac n i carT_def strT_def isNode_def set_natural) |
1328 |> Thm.close_derivation) |
1328 |> Thm.close_derivation) |
1329 goals (drop m set_naturals)) |
1329 goals (drop m set_naturals)) |
1330 ks goalss carT_defs strT_defs isNode_defs set_natural'ss |
1330 ks goalss carT_defs strT_defs isNode_defs set_natural'ss |
1331 end; |
1331 end; |
1363 |
1363 |
1364 val goals = map HOLogic.mk_Trueprop concls; |
1364 val goals = map HOLogic.mk_Trueprop concls; |
1365 in |
1365 in |
1366 map5 (fn j => fn goal => fn cts => fn set_incl_hsets => fn set_hset_incl_hsetss => |
1366 map5 (fn j => fn goal => fn cts => fn set_incl_hsets => fn set_hset_incl_hsetss => |
1367 singleton (Proof_Context.export names_lthy lthy) |
1367 singleton (Proof_Context.export names_lthy lthy) |
1368 (Skip_Proof.prove lthy [] [] goal |
1368 (Goal.prove_sorry lthy [] [] goal |
1369 (K (mk_strT_hset_tac n m j arg_cong_cTs cTs cts |
1369 (K (mk_strT_hset_tac n m j arg_cong_cTs cTs cts |
1370 carT_defs strT_defs isNode_defs |
1370 carT_defs strT_defs isNode_defs |
1371 set_incl_hsets set_hset_incl_hsetss coalg_set_thmss' carT_set_thmss' |
1371 set_incl_hsets set_hset_incl_hsetss coalg_set_thmss' carT_set_thmss' |
1372 coalgT_thm set_natural'ss))) |
1372 coalgT_thm set_natural'ss))) |
1373 |> Thm.close_derivation) |
1373 |> Thm.close_derivation) |
1388 val isNode_premss = replicate n (map (HOLogic.mk_Trueprop o mk_isNode As_copy kl) ks); |
1388 val isNode_premss = replicate n (map (HOLogic.mk_Trueprop o mk_isNode As_copy kl) ks); |
1389 val conclss = replicate n (map (HOLogic.mk_Trueprop o mk_isNode As kl) ks); |
1389 val conclss = replicate n (map (HOLogic.mk_Trueprop o mk_isNode As kl) ks); |
1390 in |
1390 in |
1391 map5 (fn carT_prem => fn isNode_prems => fn in_prem => fn concls => fn strT_hset_thmss => |
1391 map5 (fn carT_prem => fn isNode_prems => fn in_prem => fn concls => fn strT_hset_thmss => |
1392 map4 (fn isNode_prem => fn concl => fn isNode_def => fn strT_hset_thms => |
1392 map4 (fn isNode_prem => fn concl => fn isNode_def => fn strT_hset_thms => |
1393 Skip_Proof.prove lthy [] [] |
1393 Goal.prove_sorry lthy [] [] |
1394 (fold_rev Logic.all (Kl :: lab :: kl :: As @ As_copy) |
1394 (fold_rev Logic.all (Kl :: lab :: kl :: As @ As_copy) |
1395 (Logic.list_implies ([carT_prem, prem, isNode_prem, in_prem], concl))) |
1395 (Logic.list_implies ([carT_prem, prem, isNode_prem, in_prem], concl))) |
1396 (mk_isNode_hset_tac n isNode_def strT_hset_thms) |
1396 (mk_isNode_hset_tac n isNode_def strT_hset_thms) |
1397 |> Thm.close_derivation) |
1397 |> Thm.close_derivation) |
1398 isNode_prems concls isNode_defs |
1398 isNode_prems concls isNode_defs |
1567 (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs)); |
1567 (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs)); |
1568 |
1568 |
1569 val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat]; |
1569 val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat]; |
1570 |
1570 |
1571 val Lev_sbd = singleton (Proof_Context.export names_lthy lthy) |
1571 val Lev_sbd = singleton (Proof_Context.export names_lthy lthy) |
1572 (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal) |
1572 (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) |
1573 (K (mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbd_thmss)) |
1573 (K (mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbd_thmss)) |
1574 |> Thm.close_derivation); |
1574 |> Thm.close_derivation); |
1575 |
1575 |
1576 val Lev_sbd' = mk_specN n Lev_sbd; |
1576 val Lev_sbd' = mk_specN n Lev_sbd; |
1577 in |
1577 in |
1586 (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs)); |
1586 (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs)); |
1587 |
1587 |
1588 val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat]; |
1588 val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat]; |
1589 |
1589 |
1590 val length_Lev = singleton (Proof_Context.export names_lthy lthy) |
1590 val length_Lev = singleton (Proof_Context.export names_lthy lthy) |
1591 (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal) |
1591 (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) |
1592 (K (mk_length_Lev_tac cts Lev_0s Lev_Sucs)) |
1592 (K (mk_length_Lev_tac cts Lev_0s Lev_Sucs)) |
1593 |> Thm.close_derivation); |
1593 |> Thm.close_derivation); |
1594 |
1594 |
1595 val length_Lev' = mk_specN (n + 1) length_Lev; |
1595 val length_Lev' = mk_specN (n + 1) length_Lev; |
1596 val length_Levs = map (fn i => length_Lev' RS mk_conjunctN n i RS mp) ks; |
1596 val length_Levs = map (fn i => length_Lev' RS mk_conjunctN n i RS mp) ks; |
1599 (HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z)), |
1599 (HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z)), |
1600 HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, mk_Lev ss (mk_size kl) i $ z)))); |
1600 HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, mk_Lev ss (mk_size kl) i $ z)))); |
1601 val goals = map2 mk_goal ks zs; |
1601 val goals = map2 mk_goal ks zs; |
1602 |
1602 |
1603 val length_Levs' = map2 (fn goal => fn length_Lev => |
1603 val length_Levs' = map2 (fn goal => fn length_Lev => |
1604 Skip_Proof.prove lthy [] [] goal (K (mk_length_Lev'_tac length_Lev)) |
1604 Goal.prove_sorry lthy [] [] goal (K (mk_length_Lev'_tac length_Lev)) |
1605 |> Thm.close_derivation) goals length_Levs; |
1605 |> Thm.close_derivation) goals length_Levs; |
1606 in |
1606 in |
1607 (length_Levs, length_Levs') |
1607 (length_Levs, length_Levs') |
1608 end; |
1608 end; |
1609 |
1609 |
1616 (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs)); |
1616 (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs)); |
1617 |
1617 |
1618 val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat]; |
1618 val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat]; |
1619 |
1619 |
1620 val prefCl_Lev = singleton (Proof_Context.export names_lthy lthy) |
1620 val prefCl_Lev = singleton (Proof_Context.export names_lthy lthy) |
1621 (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal) |
1621 (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) |
1622 (K (mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs))) |
1622 (K (mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs))) |
1623 |> Thm.close_derivation; |
1623 |> Thm.close_derivation; |
1624 |
1624 |
1625 val prefCl_Lev' = mk_specN (n + 2) prefCl_Lev; |
1625 val prefCl_Lev' = mk_specN (n + 2) prefCl_Lev; |
1626 in |
1626 in |
1640 |
1640 |
1641 val cTs = [SOME (certifyT lthy sum_sbdT)]; |
1641 val cTs = [SOME (certifyT lthy sum_sbdT)]; |
1642 val cts = map (SOME o certify lthy) [Term.absfree kl' goal, kl]; |
1642 val cts = map (SOME o certify lthy) [Term.absfree kl' goal, kl]; |
1643 |
1643 |
1644 val rv_last = singleton (Proof_Context.export names_lthy lthy) |
1644 val rv_last = singleton (Proof_Context.export names_lthy lthy) |
1645 (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal) |
1645 (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) |
1646 (K (mk_rv_last_tac cTs cts rv_Nils rv_Conss))) |
1646 (K (mk_rv_last_tac cTs cts rv_Nils rv_Conss))) |
1647 |> Thm.close_derivation; |
1647 |> Thm.close_derivation; |
1648 |
1648 |
1649 val rv_last' = mk_specN (n + 1) rv_last; |
1649 val rv_last' = mk_specN (n + 1) rv_last; |
1650 in |
1650 in |
1664 (Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct ks zs Bs)); |
1664 (Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct ks zs Bs)); |
1665 |
1665 |
1666 val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat]; |
1666 val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat]; |
1667 |
1667 |
1668 val set_rv_Lev = singleton (Proof_Context.export names_lthy lthy) |
1668 val set_rv_Lev = singleton (Proof_Context.export names_lthy lthy) |
1669 (Skip_Proof.prove lthy [] [] |
1669 (Goal.prove_sorry lthy [] [] |
1670 (Logic.mk_implies (coalg_prem, HOLogic.mk_Trueprop goal)) |
1670 (Logic.mk_implies (coalg_prem, HOLogic.mk_Trueprop goal)) |
1671 (K (mk_set_rv_Lev_tac m cts Lev_0s Lev_Sucs rv_Nils rv_Conss |
1671 (K (mk_set_rv_Lev_tac m cts Lev_0s Lev_Sucs rv_Nils rv_Conss |
1672 coalg_set_thmss from_to_sbd_thmss))) |
1672 coalg_set_thmss from_to_sbd_thmss))) |
1673 |> Thm.close_derivation; |
1673 |> Thm.close_derivation; |
1674 |
1674 |
1705 (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs)); |
1705 (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs)); |
1706 |
1706 |
1707 val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat]; |
1707 val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat]; |
1708 |
1708 |
1709 val set_Lev = singleton (Proof_Context.export names_lthy lthy) |
1709 val set_Lev = singleton (Proof_Context.export names_lthy lthy) |
1710 (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal) |
1710 (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) |
1711 (K (mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss))) |
1711 (K (mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss))) |
1712 |> Thm.close_derivation; |
1712 |> Thm.close_derivation; |
1713 |
1713 |
1714 val set_Lev' = mk_specN (3 * n + 1) set_Lev; |
1714 val set_Lev' = mk_specN (3 * n + 1) set_Lev; |
1715 in |
1715 in |
1743 (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs)); |
1743 (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs)); |
1744 |
1744 |
1745 val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat]; |
1745 val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat]; |
1746 |
1746 |
1747 val set_image_Lev = singleton (Proof_Context.export names_lthy lthy) |
1747 val set_image_Lev = singleton (Proof_Context.export names_lthy lthy) |
1748 (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal) |
1748 (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) |
1749 (K (mk_set_image_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss |
1749 (K (mk_set_image_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss |
1750 from_to_sbd_thmss to_sbd_inj_thmss))) |
1750 from_to_sbd_thmss to_sbd_inj_thmss))) |
1751 |> Thm.close_derivation; |
1751 |> Thm.close_derivation; |
1752 |
1752 |
1753 val set_image_Lev' = mk_specN (2 * n + 2) set_image_Lev; |
1753 val set_image_Lev' = mk_specN (2 * n + 2) set_image_Lev; |
1757 mk_conjunctN n i'' RS mp RS |
1757 mk_conjunctN n i'' RS mp RS |
1758 mk_conjunctN n i' RS mp) ks) ks) ks |
1758 mk_conjunctN n i' RS mp) ks) ks) ks |
1759 end; |
1759 end; |
1760 |
1760 |
1761 val mor_beh_thm = |
1761 val mor_beh_thm = |
1762 Skip_Proof.prove lthy [] [] |
1762 Goal.prove_sorry lthy [] [] |
1763 (fold_rev Logic.all (As @ Bs @ ss) (Logic.mk_implies (coalg_prem, |
1763 (fold_rev Logic.all (As @ Bs @ ss) (Logic.mk_implies (coalg_prem, |
1764 HOLogic.mk_Trueprop (mk_mor Bs ss carTAs strTAs (map (mk_beh ss) ks))))) |
1764 HOLogic.mk_Trueprop (mk_mor Bs ss carTAs strTAs (map (mk_beh ss) ks))))) |
1765 (mk_mor_beh_tac m mor_def mor_cong_thm |
1765 (mk_mor_beh_tac m mor_def mor_cong_thm |
1766 beh_defs carT_defs strT_defs isNode_defs |
1766 beh_defs carT_defs strT_defs isNode_defs |
1767 to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms |
1767 to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms |
1795 (Term.list_comb (final_map, passive_ids @ map (mk_proj o mk_LSBIS As) ks), strT)))); |
1795 (Term.list_comb (final_map, passive_ids @ map (mk_proj o mk_LSBIS As) ks), strT)))); |
1796 |
1796 |
1797 val goals = map3 mk_goal (map (mk_LSBIS As) ks) final_maps strTAs; |
1797 val goals = map3 mk_goal (map (mk_LSBIS As) ks) final_maps strTAs; |
1798 in |
1798 in |
1799 map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong => |
1799 map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong => |
1800 Skip_Proof.prove lthy [] [] goal |
1800 Goal.prove_sorry lthy [] [] goal |
1801 (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong equiv_LSBIS_thms)) |
1801 (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong equiv_LSBIS_thms)) |
1802 |> Thm.close_derivation) |
1802 |> Thm.close_derivation) |
1803 goals lsbisE_thms map_comp_id_thms map_congs |
1803 goals lsbisE_thms map_comp_id_thms map_congs |
1804 end; |
1804 end; |
1805 |
1805 |
1806 val coalg_final_thm = Skip_Proof.prove lthy [] [] (fold_rev Logic.all As |
1806 val coalg_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As |
1807 (HOLogic.mk_Trueprop (mk_coalg As car_finalAs str_finalAs))) |
1807 (HOLogic.mk_Trueprop (mk_coalg As car_finalAs str_finalAs))) |
1808 (K (mk_coalg_final_tac m coalg_def congruent_str_final_thms equiv_LSBIS_thms |
1808 (K (mk_coalg_final_tac m coalg_def congruent_str_final_thms equiv_LSBIS_thms |
1809 set_natural'ss coalgT_set_thmss)) |
1809 set_natural'ss coalgT_set_thmss)) |
1810 |> Thm.close_derivation; |
1810 |> Thm.close_derivation; |
1811 |
1811 |
1812 val mor_T_final_thm = Skip_Proof.prove lthy [] [] (fold_rev Logic.all As |
1812 val mor_T_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As |
1813 (HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finalAs str_finalAs |
1813 (HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finalAs str_finalAs |
1814 (map (mk_proj o mk_LSBIS As) ks)))) |
1814 (map (mk_proj o mk_LSBIS As) ks)))) |
1815 (K (mk_mor_T_final_tac mor_def congruent_str_final_thms equiv_LSBIS_thms)) |
1815 (K (mk_mor_T_final_tac mor_def congruent_str_final_thms equiv_LSBIS_thms)) |
1816 |> Thm.close_derivation; |
1816 |> Thm.close_derivation; |
1817 |
1817 |
1910 |
1910 |
1911 val coalg_final_set_thmss = map (map (fn thm => coalg_final_thm RS thm)) coalg_set_thmss; |
1911 val coalg_final_set_thmss = map (map (fn thm => coalg_final_thm RS thm)) coalg_set_thmss; |
1912 val (mor_Rep_thm, mor_Abs_thm) = |
1912 val (mor_Rep_thm, mor_Abs_thm) = |
1913 let |
1913 let |
1914 val mor_Rep = |
1914 val mor_Rep = |
1915 Skip_Proof.prove lthy [] [] |
1915 Goal.prove_sorry lthy [] [] |
1916 (HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts)) |
1916 (HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts)) |
1917 (mk_mor_Rep_tac m (mor_def :: dtor_defs) Reps Abs_inverses coalg_final_set_thmss |
1917 (mk_mor_Rep_tac m (mor_def :: dtor_defs) Reps Abs_inverses coalg_final_set_thmss |
1918 map_comp_id_thms map_congL_thms) |
1918 map_comp_id_thms map_congL_thms) |
1919 |> Thm.close_derivation; |
1919 |> Thm.close_derivation; |
1920 |
1920 |
1921 val mor_Abs = |
1921 val mor_Abs = |
1922 Skip_Proof.prove lthy [] [] |
1922 Goal.prove_sorry lthy [] [] |
1923 (HOLogic.mk_Trueprop (mk_mor car_finals str_finals UNIVs dtors Abs_Ts)) |
1923 (HOLogic.mk_Trueprop (mk_mor car_finals str_finals UNIVs dtors Abs_Ts)) |
1924 (mk_mor_Abs_tac (mor_def :: dtor_defs) Abs_inverses) |
1924 (mk_mor_Abs_tac (mor_def :: dtor_defs) Abs_inverses) |
1925 |> Thm.close_derivation; |
1925 |> Thm.close_derivation; |
1926 in |
1926 in |
1927 (mor_Rep, mor_Abs) |
1927 (mor_Rep, mor_Abs) |
1964 let |
1964 let |
1965 val Abs_inverses' = map2 (curry op RS) in_car_final_thms Abs_inverses; |
1965 val Abs_inverses' = map2 (curry op RS) in_car_final_thms Abs_inverses; |
1966 val morEs' = map (fn thm => |
1966 val morEs' = map (fn thm => |
1967 (thm OF [tcoalg_thm RS mor_final_thm, UNIV_I]) RS sym) morE_thms; |
1967 (thm OF [tcoalg_thm RS mor_final_thm, UNIV_I]) RS sym) morE_thms; |
1968 in |
1968 in |
1969 Skip_Proof.prove lthy [] [] |
1969 Goal.prove_sorry lthy [] [] |
1970 (fold_rev Logic.all ss |
1970 (fold_rev Logic.all ss |
1971 (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks)))) |
1971 (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks)))) |
1972 (K (mk_mor_unfold_tac m mor_UNIV_thm dtor_defs unfold_defs Abs_inverses' morEs' |
1972 (K (mk_mor_unfold_tac m mor_UNIV_thm dtor_defs unfold_defs Abs_inverses' morEs' |
1973 map_comp_id_thms map_congs)) |
1973 map_comp_id_thms map_congs)) |
1974 |> Thm.close_derivation |
1974 |> Thm.close_derivation |
1980 val prem = HOLogic.mk_Trueprop (mk_sbis passive_UNIVs UNIVs dtors TRs); |
1980 val prem = HOLogic.mk_Trueprop (mk_sbis passive_UNIVs UNIVs dtors TRs); |
1981 val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
1981 val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
1982 (map2 (fn R => fn T => mk_subset R (Id_const T)) TRs Ts)); |
1982 (map2 (fn R => fn T => mk_subset R (Id_const T)) TRs Ts)); |
1983 val goal = fold_rev Logic.all TRs (Logic.mk_implies (prem, concl)); |
1983 val goal = fold_rev Logic.all TRs (Logic.mk_implies (prem, concl)); |
1984 in |
1984 in |
1985 `split_conj_thm (Skip_Proof.prove lthy [] [] goal |
1985 `split_conj_thm (Goal.prove_sorry lthy [] [] goal |
1986 (K (mk_raw_coind_tac bis_def bis_cong_thm bis_O_thm bis_converse_thm bis_Gr_thm |
1986 (K (mk_raw_coind_tac bis_def bis_cong_thm bis_O_thm bis_converse_thm bis_Gr_thm |
1987 tcoalg_thm coalgT_thm mor_T_final_thm sbis_lsbis_thm |
1987 tcoalg_thm coalgT_thm mor_T_final_thm sbis_lsbis_thm |
1988 lsbis_incl_thms incl_lsbis_thms equiv_LSBIS_thms mor_Rep_thm Rep_injects)) |
1988 lsbis_incl_thms incl_lsbis_thms equiv_LSBIS_thms mor_Rep_thm Rep_injects)) |
1989 |> Thm.close_derivation) |
1989 |> Thm.close_derivation) |
1990 end; |
1990 end; |
1997 fun mk_fun_eq B f g z = HOLogic.mk_imp |
1997 fun mk_fun_eq B f g z = HOLogic.mk_imp |
1998 (HOLogic.mk_mem (z, B), HOLogic.mk_eq (f $ z, g $ z)); |
1998 (HOLogic.mk_mem (z, B), HOLogic.mk_eq (f $ z, g $ z)); |
1999 val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
1999 val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
2000 (map4 mk_fun_eq Bs unfold_fs unfold_fs_copy zs)); |
2000 (map4 mk_fun_eq Bs unfold_fs unfold_fs_copy zs)); |
2001 |
2001 |
2002 val unique_mor = Skip_Proof.prove lthy [] [] |
2002 val unique_mor = Goal.prove_sorry lthy [] [] |
2003 (fold_rev Logic.all (Bs @ ss @ unfold_fs @ unfold_fs_copy @ zs) |
2003 (fold_rev Logic.all (Bs @ ss @ unfold_fs @ unfold_fs_copy @ zs) |
2004 (Logic.list_implies (prems, unique))) |
2004 (Logic.list_implies (prems, unique))) |
2005 (K (mk_unique_mor_tac raw_coind_thms bis_image2_thm)) |
2005 (K (mk_unique_mor_tac raw_coind_thms bis_image2_thm)) |
2006 |> Thm.close_derivation; |
2006 |> Thm.close_derivation; |
2007 in |
2007 in |
2016 (map2 mk_fun_eq unfold_fs ks)); |
2016 (map2 mk_fun_eq unfold_fs ks)); |
2017 |
2017 |
2018 val bis_thm = tcoalg_thm RSN (2, tcoalg_thm RS bis_image2_thm); |
2018 val bis_thm = tcoalg_thm RSN (2, tcoalg_thm RS bis_image2_thm); |
2019 val mor_thm = mor_comp_thm OF [tcoalg_thm RS mor_final_thm, mor_Abs_thm]; |
2019 val mor_thm = mor_comp_thm OF [tcoalg_thm RS mor_final_thm, mor_Abs_thm]; |
2020 |
2020 |
2021 val unique_mor = Skip_Proof.prove lthy [] [] |
2021 val unique_mor = Goal.prove_sorry lthy [] [] |
2022 (fold_rev Logic.all (ss @ unfold_fs) (Logic.mk_implies (prem, unique))) |
2022 (fold_rev Logic.all (ss @ unfold_fs) (Logic.mk_implies (prem, unique))) |
2023 (K (mk_unfold_unique_mor_tac raw_coind_thms bis_thm mor_thm unfold_defs)) |
2023 (K (mk_unfold_unique_mor_tac raw_coind_thms bis_thm mor_thm unfold_defs)) |
2024 |> Thm.close_derivation; |
2024 |> Thm.close_derivation; |
2025 in |
2025 in |
2026 `split_conj_thm unique_mor |
2026 `split_conj_thm unique_mor |
2079 fun mk_goal dtor ctor FT = |
2079 fun mk_goal dtor ctor FT = |
2080 mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT); |
2080 mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT); |
2081 val goals = map3 mk_goal dtors ctors FTs; |
2081 val goals = map3 mk_goal dtors ctors FTs; |
2082 in |
2082 in |
2083 map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_congL => |
2083 map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_congL => |
2084 Skip_Proof.prove lthy [] [] goal |
2084 Goal.prove_sorry lthy [] [] goal |
2085 (mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtor_thms) |
2085 (mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtor_thms) |
2086 |> Thm.close_derivation) |
2086 |> Thm.close_derivation) |
2087 goals ctor_defs dtor_unfold_thms map_comp_id_thms map_congL_thms |
2087 goals ctor_defs dtor_unfold_thms map_comp_id_thms map_congL_thms |
2088 end; |
2088 end; |
2089 |
2089 |
2167 fold_rev Logic.all (z :: corec_ss) (mk_Trueprop_eq (lhs, rhs)) |
2167 fold_rev Logic.all (z :: corec_ss) (mk_Trueprop_eq (lhs, rhs)) |
2168 end; |
2168 end; |
2169 val goals = map5 mk_goal ks corec_ss corec_maps_rev dtors zs; |
2169 val goals = map5 mk_goal ks corec_ss corec_maps_rev dtors zs; |
2170 in |
2170 in |
2171 map3 (fn goal => fn unfold => fn map_cong => |
2171 map3 (fn goal => fn unfold => fn map_cong => |
2172 Skip_Proof.prove lthy [] [] goal |
2172 Goal.prove_sorry lthy [] [] goal |
2173 (mk_corec_tac m corec_defs unfold map_cong corec_Inl_sum_thms) |
2173 (mk_corec_tac m corec_defs unfold map_cong corec_Inl_sum_thms) |
2174 |> Thm.close_derivation) |
2174 |> Thm.close_derivation) |
2175 goals dtor_unfold_thms map_congs |
2175 goals dtor_unfold_thms map_congs |
2176 end; |
2176 end; |
2177 |
2177 |
2219 val dtor_srel_coinduct_goal = |
2219 val dtor_srel_coinduct_goal = |
2220 fold_rev Logic.all frees (Logic.list_implies (srel_prems, concl)); |
2220 fold_rev Logic.all frees (Logic.list_implies (srel_prems, concl)); |
2221 val coinduct_params = rev (Term.add_tfrees dtor_srel_coinduct_goal []); |
2221 val coinduct_params = rev (Term.add_tfrees dtor_srel_coinduct_goal []); |
2222 |
2222 |
2223 val dtor_srel_coinduct = unfold_thms lthy @{thms Id_on_UNIV} |
2223 val dtor_srel_coinduct = unfold_thms lthy @{thms Id_on_UNIV} |
2224 (Skip_Proof.prove lthy [] [] dtor_srel_coinduct_goal |
2224 (Goal.prove_sorry lthy [] [] dtor_srel_coinduct_goal |
2225 (K (mk_dtor_srel_coinduct_tac ks raw_coind_thm bis_srel_thm)) |
2225 (K (mk_dtor_srel_coinduct_tac ks raw_coind_thm bis_srel_thm)) |
2226 |> Thm.close_derivation); |
2226 |> Thm.close_derivation); |
2227 |
2227 |
2228 fun mk_prem strong_eq phi dtor map_nth sets Jz Jz_copy FJz = |
2228 fun mk_prem strong_eq phi dtor map_nth sets Jz Jz_copy FJz = |
2229 let |
2229 let |
2251 |
2251 |
2252 val prems = mk_prems false; |
2252 val prems = mk_prems false; |
2253 val strong_prems = mk_prems true; |
2253 val strong_prems = mk_prems true; |
2254 |
2254 |
2255 val dtor_map_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (prems, concl)); |
2255 val dtor_map_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (prems, concl)); |
2256 val dtor_map_coinduct = Skip_Proof.prove lthy [] [] dtor_map_coinduct_goal |
2256 val dtor_map_coinduct = Goal.prove_sorry lthy [] [] dtor_map_coinduct_goal |
2257 (K (mk_dtor_map_coinduct_tac m ks raw_coind_thm bis_def)) |
2257 (K (mk_dtor_map_coinduct_tac m ks raw_coind_thm bis_def)) |
2258 |> Thm.close_derivation; |
2258 |> Thm.close_derivation; |
2259 |
2259 |
2260 val cTs = map (SOME o certifyT lthy o TFree) coinduct_params; |
2260 val cTs = map (SOME o certifyT lthy o TFree) coinduct_params; |
2261 val cts = map3 (SOME o certify lthy ooo mk_phi true) phis Jzs1 Jzs2; |
2261 val cts = map3 (SOME o certify lthy ooo mk_phi true) phis Jzs1 Jzs2; |
2262 |
2262 |
2263 val dtor_srel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy) |
2263 val dtor_srel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy) |
2264 (Skip_Proof.prove lthy [] [] |
2264 (Goal.prove_sorry lthy [] [] |
2265 (fold_rev Logic.all zs (Logic.list_implies (srel_strong_prems, concl))) |
2265 (fold_rev Logic.all zs (Logic.list_implies (srel_strong_prems, concl))) |
2266 (K (mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids))) |
2266 (K (mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids))) |
2267 |> Thm.close_derivation; |
2267 |> Thm.close_derivation; |
2268 |
2268 |
2269 val dtor_map_strong_coinduct = singleton (Proof_Context.export names_lthy lthy) |
2269 val dtor_map_strong_coinduct = singleton (Proof_Context.export names_lthy lthy) |
2270 (Skip_Proof.prove lthy [] [] |
2270 (Goal.prove_sorry lthy [] [] |
2271 (fold_rev Logic.all zs (Logic.list_implies (strong_prems, concl))) |
2271 (fold_rev Logic.all zs (Logic.list_implies (strong_prems, concl))) |
2272 (K (mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def |
2272 (K (mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def |
2273 (tcoalg_thm RS bis_Id_on_thm)))) |
2273 (tcoalg_thm RS bis_Id_on_thm)))) |
2274 |> Thm.close_derivation; |
2274 |> Thm.close_derivation; |
2275 |
2275 |
2381 HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), dtor))); |
2381 HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), dtor))); |
2382 val goals = map4 mk_goal fs_maps map_FTFT's dtors dtor's; |
2382 val goals = map4 mk_goal fs_maps map_FTFT's dtors dtor's; |
2383 val cTs = map (SOME o certifyT lthy) FTs'; |
2383 val cTs = map (SOME o certifyT lthy) FTs'; |
2384 val maps = |
2384 val maps = |
2385 map5 (fn goal => fn cT => fn unfold => fn map_comp' => fn map_cong => |
2385 map5 (fn goal => fn cT => fn unfold => fn map_comp' => fn map_cong => |
2386 Skip_Proof.prove lthy [] [] goal |
2386 Goal.prove_sorry lthy [] [] goal |
2387 (K (mk_map_tac m n cT unfold map_comp' map_cong)) |
2387 (K (mk_map_tac m n cT unfold map_comp' map_cong)) |
2388 |> Thm.close_derivation) |
2388 |> Thm.close_derivation) |
2389 goals cTs dtor_unfold_thms map_comp's map_congs; |
2389 goals cTs dtor_unfold_thms map_comp's map_congs; |
2390 in |
2390 in |
2391 map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps |
2391 map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps |
2397 (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
2397 (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
2398 (map3 (fn fmap => fn gmap => fn fgmap => |
2398 (map3 (fn fmap => fn gmap => fn fgmap => |
2399 HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap)) |
2399 HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap)) |
2400 fs_maps gs_maps fgs_maps))) |
2400 fs_maps gs_maps fgs_maps))) |
2401 in |
2401 in |
2402 split_conj_thm (Skip_Proof.prove lthy [] [] goal |
2402 split_conj_thm (Goal.prove_sorry lthy [] [] goal |
2403 (K (mk_map_comp_tac m n map_thms map_comps map_congs dtor_unfold_unique_thm)) |
2403 (K (mk_map_comp_tac m n map_thms map_comps map_congs dtor_unfold_unique_thm)) |
2404 |> Thm.close_derivation) |
2404 |> Thm.close_derivation) |
2405 end; |
2405 end; |
2406 |
2406 |
2407 val dtor_map_unique_thm = |
2407 val dtor_map_unique_thm = |
2412 val prems = map4 mk_prem us map_FTFT's dtors dtor's; |
2412 val prems = map4 mk_prem us map_FTFT's dtors dtor's; |
2413 val goal = |
2413 val goal = |
2414 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
2414 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
2415 (map2 (curry HOLogic.mk_eq) us fs_maps)); |
2415 (map2 (curry HOLogic.mk_eq) us fs_maps)); |
2416 in |
2416 in |
2417 Skip_Proof.prove lthy [] [] |
2417 Goal.prove_sorry lthy [] [] |
2418 (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal))) |
2418 (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal))) |
2419 (mk_dtor_map_unique_tac dtor_unfold_unique_thm map_comps) |
2419 (mk_dtor_map_unique_tac dtor_unfold_unique_thm map_comps) |
2420 |> Thm.close_derivation |
2420 |> Thm.close_derivation |
2421 end; |
2421 end; |
2422 |
2422 |
2446 val le_goals = map |
2446 val le_goals = map |
2447 (fold_rev Logic.all Jzs o HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj) |
2447 (fold_rev Logic.all Jzs o HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj) |
2448 (mk_goals (uncurry mk_subset)); |
2448 (mk_goals (uncurry mk_subset)); |
2449 val set_le_thmss = map split_conj_thm |
2449 val set_le_thmss = map split_conj_thm |
2450 (map4 (fn goal => fn hset_minimal => fn set_hsets => fn set_hset_hsetss => |
2450 (map4 (fn goal => fn hset_minimal => fn set_hsets => fn set_hset_hsetss => |
2451 Skip_Proof.prove lthy [] [] goal |
2451 Goal.prove_sorry lthy [] [] goal |
2452 (K (mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss)) |
2452 (K (mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss)) |
2453 |> Thm.close_derivation) |
2453 |> Thm.close_derivation) |
2454 le_goals hset_minimal_thms set_hset_thmss' set_hset_hset_thmsss'); |
2454 le_goals hset_minimal_thms set_hset_thmss' set_hset_hset_thmsss'); |
2455 |
2455 |
2456 val simp_goalss = map (map2 (fn z => fn goal => |
2456 val simp_goalss = map (map2 (fn z => fn goal => |
2457 Logic.all z (HOLogic.mk_Trueprop goal)) Jzs) |
2457 Logic.all z (HOLogic.mk_Trueprop goal)) Jzs) |
2458 (mk_goals HOLogic.mk_eq); |
2458 (mk_goals HOLogic.mk_eq); |
2459 in |
2459 in |
2460 map4 (map4 (fn goal => fn set_le => fn set_incl_hset => fn set_hset_incl_hsets => |
2460 map4 (map4 (fn goal => fn set_le => fn set_incl_hset => fn set_hset_incl_hsets => |
2461 Skip_Proof.prove lthy [] [] goal |
2461 Goal.prove_sorry lthy [] [] goal |
2462 (K (mk_dtor_set_tac n set_le set_incl_hset set_hset_incl_hsets)) |
2462 (K (mk_dtor_set_tac n set_le set_incl_hset set_hset_incl_hsets)) |
2463 |> Thm.close_derivation)) |
2463 |> Thm.close_derivation)) |
2464 simp_goalss set_le_thmss set_incl_hset_thmss' set_hset_incl_hset_thmsss' |
2464 simp_goalss set_le_thmss set_incl_hset_thmss' set_hset_incl_hset_thmsss' |
2465 end; |
2465 end; |
2466 |
2466 |
2487 map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals; |
2487 map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals; |
2488 |
2488 |
2489 val thms = |
2489 val thms = |
2490 map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs => |
2490 map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs => |
2491 singleton (Proof_Context.export names_lthy lthy) |
2491 singleton (Proof_Context.export names_lthy lthy) |
2492 (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal) |
2492 (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) |
2493 (mk_col_natural_tac cts rec_0s rec_Sucs dtor_map_thms set_natural'ss)) |
2493 (mk_col_natural_tac cts rec_0s rec_Sucs dtor_map_thms set_natural'ss)) |
2494 |> Thm.close_derivation) |
2494 |> Thm.close_derivation) |
2495 goals ctss hset_rec_0ss' hset_rec_Sucss'; |
2495 goals ctss hset_rec_0ss' hset_rec_Sucss'; |
2496 in |
2496 in |
2497 map (split_conj_thm o mk_specN n) thms |
2497 map (split_conj_thm o mk_specN n) thms |
2510 map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals; |
2510 map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals; |
2511 |
2511 |
2512 val thms = |
2512 val thms = |
2513 map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs => |
2513 map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs => |
2514 singleton (Proof_Context.export names_lthy lthy) |
2514 singleton (Proof_Context.export names_lthy lthy) |
2515 (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal) |
2515 (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) |
2516 (K (mk_col_bd_tac m j cts rec_0s rec_Sucs |
2516 (K (mk_col_bd_tac m j cts rec_0s rec_Sucs |
2517 sbd_Card_order sbd_Cinfinite set_sbdss))) |
2517 sbd_Card_order sbd_Cinfinite set_sbdss))) |
2518 |> Thm.close_derivation) |
2518 |> Thm.close_derivation) |
2519 ls goals ctss hset_rec_0ss' hset_rec_Sucss'; |
2519 ls goals ctss hset_rec_0ss' hset_rec_Sucss'; |
2520 in |
2520 in |
2555 val goal = |
2555 val goal = |
2556 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
2556 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
2557 (map4 mk_map_cong setss_by_bnf Jzs fs_maps fs_copy_maps)); |
2557 (map4 mk_map_cong setss_by_bnf Jzs fs_maps fs_copy_maps)); |
2558 |
2558 |
2559 val thm = singleton (Proof_Context.export names_lthy lthy) |
2559 val thm = singleton (Proof_Context.export names_lthy lthy) |
2560 (Skip_Proof.prove lthy [] [] goal |
2560 (Goal.prove_sorry lthy [] [] goal |
2561 (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_congs set_natural'ss |
2561 (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_congs set_natural'ss |
2562 set_hset_thmss set_hset_hset_thmsss))) |
2562 set_hset_thmss set_hset_hset_thmsss))) |
2563 |> Thm.close_derivation |
2563 |> Thm.close_derivation |
2564 in |
2564 in |
2565 split_conj_thm thm |
2565 split_conj_thm thm |
2591 val coalg = HOLogic.mk_Trueprop |
2591 val coalg = HOLogic.mk_Trueprop |
2592 (mk_coalg CUNIVs thePulls (map2 (curry HOLogic.mk_comp) pid_Fmaps pickF_ss)); |
2592 (mk_coalg CUNIVs thePulls (map2 (curry HOLogic.mk_comp) pid_Fmaps pickF_ss)); |
2593 val goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s @ ps) |
2593 val goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s @ ps) |
2594 (Logic.mk_implies (wpull_prem, coalg)); |
2594 (Logic.mk_implies (wpull_prem, coalg)); |
2595 in |
2595 in |
2596 Skip_Proof.prove lthy [] [] goal (mk_coalg_thePull_tac m coalg_def map_wpull_thms |
2596 Goal.prove_sorry lthy [] [] goal (mk_coalg_thePull_tac m coalg_def map_wpull_thms |
2597 set_natural'ss pickWP_assms_tacs) |
2597 set_natural'ss pickWP_assms_tacs) |
2598 |> Thm.close_derivation |
2598 |> Thm.close_derivation |
2599 end; |
2599 end; |
2600 |
2600 |
2601 val (mor_thePull_fst_thm, mor_thePull_snd_thm, mor_thePull_pick_thm) = |
2601 val (mor_thePull_fst_thm, mor_thePull_snd_thm, mor_thePull_pick_thm) = |
2615 val snd_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s) |
2615 val snd_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s) |
2616 (Logic.mk_implies (wpull_prem, mor_snd)); |
2616 (Logic.mk_implies (wpull_prem, mor_snd)); |
2617 val pick_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s @ ps) |
2617 val pick_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s @ ps) |
2618 (Logic.mk_implies (wpull_prem, mor_pick)); |
2618 (Logic.mk_implies (wpull_prem, mor_pick)); |
2619 in |
2619 in |
2620 (Skip_Proof.prove lthy [] [] fst_goal (mk_mor_thePull_fst_tac m mor_def map_wpull_thms |
2620 (Goal.prove_sorry lthy [] [] fst_goal (mk_mor_thePull_fst_tac m mor_def map_wpull_thms |
2621 map_comp's pickWP_assms_tacs) |> Thm.close_derivation, |
2621 map_comp's pickWP_assms_tacs) |> Thm.close_derivation, |
2622 Skip_Proof.prove lthy [] [] snd_goal (mk_mor_thePull_snd_tac m mor_def map_wpull_thms |
2622 Goal.prove_sorry lthy [] [] snd_goal (mk_mor_thePull_snd_tac m mor_def map_wpull_thms |
2623 map_comp's pickWP_assms_tacs) |> Thm.close_derivation, |
2623 map_comp's pickWP_assms_tacs) |> Thm.close_derivation, |
2624 Skip_Proof.prove lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def dtor_unfold_thms |
2624 Goal.prove_sorry lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def dtor_unfold_thms |
2625 map_comp's) |> Thm.close_derivation) |
2625 map_comp's) |> Thm.close_derivation) |
2626 end; |
2626 end; |
2627 |
2627 |
2628 val pick_col_thmss = |
2628 val pick_col_thmss = |
2629 let |
2629 let |
2642 val goals = |
2642 val goals = |
2643 map (fn concl => Logic.mk_implies (wpull_prem, HOLogic.mk_Trueprop concl)) concls; |
2643 map (fn concl => Logic.mk_implies (wpull_prem, HOLogic.mk_Trueprop concl)) concls; |
2644 |
2644 |
2645 val thms = |
2645 val thms = |
2646 map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs => |
2646 map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs => |
2647 singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] goal |
2647 singleton (Proof_Context.export names_lthy lthy) (Goal.prove_sorry lthy [] [] goal |
2648 (mk_pick_col_tac m j cts rec_0s rec_Sucs dtor_unfold_thms set_natural'ss |
2648 (mk_pick_col_tac m j cts rec_0s rec_Sucs dtor_unfold_thms set_natural'ss |
2649 map_wpull_thms pickWP_assms_tacs)) |
2649 map_wpull_thms pickWP_assms_tacs)) |
2650 |> Thm.close_derivation) |
2650 |> Thm.close_derivation) |
2651 ls goals ctss hset_rec_0ss' hset_rec_Sucss'; |
2651 ls goals ctss hset_rec_0ss' hset_rec_Sucss'; |
2652 in |
2652 in |
2836 (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct sets Jzs dummys wits))) |
2836 (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct sets Jzs dummys wits))) |
2837 end; |
2837 end; |
2838 val goals = map5 mk_goal setss_by_range ys ys_copy ys'_copy ls; |
2838 val goals = map5 mk_goal setss_by_range ys ys_copy ys'_copy ls; |
2839 in |
2839 in |
2840 map2 (fn goal => fn induct => |
2840 map2 (fn goal => fn induct => |
2841 Skip_Proof.prove lthy [] [] goal |
2841 Goal.prove_sorry lthy [] [] goal |
2842 (mk_coind_wit_tac induct dtor_unfold_thms (flat set_natural'ss) wit_thms) |
2842 (mk_coind_wit_tac induct dtor_unfold_thms (flat set_natural'ss) wit_thms) |
2843 |> Thm.close_derivation) |
2843 |> Thm.close_derivation) |
2844 goals dtor_hset_induct_thms |
2844 goals dtor_hset_induct_thms |
2845 |> map split_conj_thm |
2845 |> map split_conj_thm |
2846 |> transpose |
2846 |> transpose |
2913 val goals = map6 mk_goal Jzs Jz's dtors dtor's JsrelRs srelRs; |
2913 val goals = map6 mk_goal Jzs Jz's dtors dtor's JsrelRs srelRs; |
2914 in |
2914 in |
2915 map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong => |
2915 map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong => |
2916 fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor => |
2916 fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor => |
2917 fn set_naturals => fn dtor_set_incls => fn dtor_set_set_inclss => |
2917 fn set_naturals => fn dtor_set_incls => fn dtor_set_set_inclss => |
2918 Skip_Proof.prove lthy [] [] goal |
2918 Goal.prove_sorry lthy [] [] goal |
2919 (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets |
2919 (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets |
2920 dtor_inject dtor_ctor set_naturals dtor_set_incls dtor_set_set_inclss)) |
2920 dtor_inject dtor_ctor set_naturals dtor_set_incls dtor_set_set_inclss)) |
2921 |> Thm.close_derivation) |
2921 |> Thm.close_derivation) |
2922 ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_dtor_set_thmss' |
2922 ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_dtor_set_thmss' |
2923 dtor_inject_thms dtor_ctor_thms set_natural'ss dtor_set_incl_thmss |
2923 dtor_inject_thms dtor_ctor_thms set_natural'ss dtor_set_incl_thmss |
2929 fun mk_goal Jz Jz' dtor dtor' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis) |
2929 fun mk_goal Jz Jz' dtor dtor' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis) |
2930 (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (dtor $ Jz) $ (dtor' $ Jz'))); |
2930 (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (dtor $ Jz) $ (dtor' $ Jz'))); |
2931 val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis; |
2931 val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis; |
2932 in |
2932 in |
2933 map3 (fn goal => fn srel_def => fn dtor_Jsrel => |
2933 map3 (fn goal => fn srel_def => fn dtor_Jsrel => |
2934 Skip_Proof.prove lthy [] [] goal |
2934 Goal.prove_sorry lthy [] [] goal |
2935 (mk_ctor_or_dtor_rel_tac srel_def Jrel_defs Jsrel_defs dtor_Jsrel) |
2935 (mk_ctor_or_dtor_rel_tac srel_def Jrel_defs Jsrel_defs dtor_Jsrel) |
2936 |> Thm.close_derivation) |
2936 |> Thm.close_derivation) |
2937 goals srel_defs dtor_Jsrel_thms |
2937 goals srel_defs dtor_Jsrel_thms |
2938 end; |
2938 end; |
2939 |
2939 |