515 |
533 |
516 val _ = |
534 val _ = |
517 if get_STEPS lthy > 21 |
535 if get_STEPS lthy > 21 |
518 then true else raise TEST lthy9' |
536 then true else raise TEST lthy9' |
519 |
537 |
520 (* old stuff *) |
538 in |
521 |
539 (0, lthy9') |
522 val thy = ProofContext.theory_of lthy9' |
|
523 val thy_name = Context.theory_name thy |
|
524 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
|
525 |
|
526 val _ = warning "Proving respects"; |
|
527 |
|
528 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
|
529 val bns = raw_bns ~~ bn_nos; |
|
530 |
|
531 val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_defs (map fst bns) lthy9'; |
|
532 val (bns_rsp_pre, lthy9) = fold_map ( |
|
533 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
|
534 resolve_tac bns_rsp_pre' 1)) bns lthy9'; |
|
535 val bns_rsp = flat (map snd bns_rsp_pre); |
|
536 |
|
537 fun fv_rsp_tac _ = fvbv_rsp_tac alpha_induct raw_fv_defs lthy9' 1; |
|
538 |
|
539 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos |
|
540 |
|
541 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_trms fv_rsp_tac lthy9; |
|
542 val (fv_rsp_pre, lthy10) = fold_map |
|
543 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
|
544 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (raw_fvs @ raw_fv_bns) lthy9; |
|
545 val fv_rsp = flat (map snd fv_rsp_pre); |
|
546 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs |
|
547 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
|
548 fun alpha_bn_rsp_tac _ = let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts) alpha_equivp_thms raw_exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; |
|
549 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
|
550 alpha_bn_rsp_tac) alpha_bn_trms lthy11 |
|
551 fun const_rsp_tac _ = |
|
552 let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a |
|
553 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end |
|
554 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
|
555 const_rsp_tac) raw_constrs lthy11a |
|
556 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) |
|
557 val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns) |
|
558 val (qfv_info, lthy12a) = define_qconsts qtys dd lthy12; |
|
559 val qfv_ts = map #qconst qfv_info |
|
560 val qfv_defs = map #def qfv_info |
|
561 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; |
|
562 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
|
563 val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bns |
|
564 val (qbn_info, lthy12b) = define_qconsts qtys dd lthy12a; |
|
565 val qbn_ts = map #qconst qbn_info |
|
566 val qbn_defs = map #def qbn_info |
|
567 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms |
|
568 val dd = map2 (fn x => fn y => (x, y, NoSyn)) qalpha_bn_names alpha_bn_trms |
|
569 val (qalpha_info, lthy12c) = define_qconsts qtys dd lthy12b; |
|
570 val qalpha_bn_trms = map #qconst qalpha_info |
|
571 val qalphabn_defs = map #def qalpha_info |
|
572 |
|
573 val _ = warning "Lifting permutations"; |
|
574 val perm_names = map (fn x => "permute_" ^ x) qty_names |
|
575 val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs |
|
576 val lthy13 = define_qperms qtys qty_full_names [] dd raw_perm_laws lthy12c |
|
577 |
|
578 val q_name = space_implode "_" qty_names; |
|
579 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
|
580 val _ = warning "Lifting induction"; |
|
581 val constr_names = map (Long_Name.base_name o fst o dest_Const) []; |
|
582 val q_induct = Rule_Cases.name constr_names (the_single (fst (lift_thms qtys [] [raw_induct_thm] lthy13))); |
|
583 fun note_suffix s th ctxt = |
|
584 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
|
585 fun note_simp_suffix s th ctxt = |
|
586 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
|
587 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
|
588 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), |
|
589 [Rule_Cases.name constr_names q_induct]) lthy13; |
|
590 val q_inducts = Project_Rule.projects lthy13 (1 upto (length raw_fvs)) q_induct |
|
591 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
|
592 val q_perm = fst (lift_thms qtys [] raw_perm_simps lthy14); |
|
593 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
|
594 val q_fv = fst (lift_thms qtys [] raw_fv_defs lthy15); |
|
595 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
|
596 val q_bn = fst (lift_thms qtys [] raw_bn_defs lthy16); |
|
597 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
|
598 val _ = warning "Lifting eq-iff"; |
|
599 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) |
|
600 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff |
|
601 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0 |
|
602 val q_eq_iff_pre0 = fst (lift_thms qtys [] eq_iff_unfolded1 lthy17); |
|
603 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms Pair_eqvt}) q_eq_iff_pre0 |
|
604 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1 |
|
605 val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2 |
|
606 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
|
607 val q_dis = fst (lift_thms qtys [] alpha_distincts lthy18); |
|
608 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
|
609 val q_eqvt = fst (lift_thms qtys [] (raw_bn_eqvt @ raw_fv_eqvt) lthy19); |
|
610 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
|
611 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
|
612 val _ = warning "Supports"; |
|
613 val supports = map (prove_supports lthy20 q_perm) []; |
|
614 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); |
|
615 val thy3 = Local_Theory.exit_global lthy20; |
|
616 val _ = warning "Instantiating FS"; |
|
617 val lthy21 = Class.instantiation (qty_full_names, [], @{sort fs}) thy3; |
|
618 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
|
619 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
|
620 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_trms, qalpha_bn_trms) bn_nos; |
|
621 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
|
622 val _ = warning "Support Equations"; |
|
623 fun supp_eq_tac' _ = supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1; |
|
624 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e => |
|
625 let val _ = warning ("Support eqs failed") in [] end; |
|
626 val lthy23 = note_suffix "supp" q_supp lthy22; |
|
627 in |
|
628 (0, lthy23) |
|
629 end handle TEST ctxt => (0, ctxt) |
540 end handle TEST ctxt => (0, ctxt) |
630 *} |
541 *} |
631 |
542 |
632 section {* Preparing and parsing of the specification *} |
543 section {* Preparing and parsing of the specification *} |
633 |
544 |
853 val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl |
764 val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl |
854 (main_parser >> nominal_datatype2_cmd) |
765 (main_parser >> nominal_datatype2_cmd) |
855 *} |
766 *} |
856 |
767 |
857 |
768 |
858 text {* |
769 end |
859 nominal_datatype2 does the following things in order: |
770 |
860 |
771 |
861 Parser.thy/raw_nominal_decls |
772 |
862 1) define the raw datatype |
|
863 2) define the raw binding functions |
|
864 |
|
865 Perm.thy/define_raw_perms |
|
866 3) define permutations of the raw datatype and show that the raw type is |
|
867 in the pt typeclass |
|
868 |
|
869 Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha |
|
870 4) define fv and fv_bn |
|
871 5) define alpha and alpha_bn |
|
872 |
|
873 Perm.thy/distinct_rel |
|
874 6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...) (Proof by cases; simp) |
|
875 |
|
876 Tacs.thy/build_rel_inj |
|
877 6) prove alpha_eq_iff (C1 x = C2 y \<leftrightarrow> P x y ...) |
|
878 (left-to-right by intro rule, right-to-left by cases; simp) |
|
879 Equivp.thy/prove_eqvt |
|
880 7) prove bn_eqvt (common induction on the raw datatype) |
|
881 8) prove fv_eqvt (common induction on the raw datatype with help of above) |
|
882 Rsp.thy/build_alpha_eqvts |
|
883 9) prove alpha_eqvt and alpha_bn_eqvt |
|
884 (common alpha-induction, unfolding alpha_gen, permute of #* and =) |
|
885 Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps |
|
886 10) prove that alpha and alpha_bn are equivalence relations |
|
887 (common induction and application of 'compose' lemmas) |
|
888 Lift.thy/define_quotient_types |
|
889 11) define quotient types |
|
890 Rsp.thy/build_fvbv_rsps |
|
891 12) prove bn respects (common induction and simp with alpha_gen) |
|
892 Rsp.thy/prove_const_rsp |
|
893 13) prove fv respects (common induction and simp with alpha_gen) |
|
894 14) prove permute respects (unfolds to alpha_eqvt) |
|
895 Rsp.thy/prove_alpha_bn_rsp |
|
896 15) prove alpha_bn respects |
|
897 (alpha_induct then cases then sym and trans of the relations) |
|
898 Rsp.thy/prove_alpha_alphabn |
|
899 16) show that alpha implies alpha_bn (by unduction, needed in following step) |
|
900 Rsp.thy/prove_const_rsp |
|
901 17) prove respects for all datatype constructors |
|
902 (unfold eq_iff and alpha_gen; introduce zero permutations; simp) |
|
903 Perm.thy/quotient_lift_consts_export |
|
904 18) define lifted constructors, fv, bn, alpha_bn, permutations |
|
905 Perm.thy/define_lifted_perms |
|
906 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass |
|
907 Lift.thy/lift_thm |
|
908 20) lift permutation simplifications |
|
909 21) lift induction |
|
910 22) lift fv |
|
911 23) lift bn |
|
912 24) lift eq_iff |
|
913 25) lift alpha_distincts |
|
914 26) lift fv and bn eqvts |
|
915 Equivp.thy/prove_supports |
|
916 27) prove that union of arguments supports constructors |
|
917 Equivp.thy/prove_fs |
|
918 28) show that the lifted type is in fs typeclass (* by q_induct, supports *) |
|
919 Equivp.thy/supp_eq |
|
920 29) prove supp = fv |
|
921 *} |
|
922 |
|
923 |
|
924 |
|
925 end |
|
926 |
|
927 |
|
928 |
|