nominal2: comparison Nominal/Parser.thy

equal deleted inserted replaced

-:c004e7448dca
+:f86710d35146
 val raw_binds = rawify_binds dts_env cnstrs_env bn_fun_full_env binds
 val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs)
-val _ = tracing (cat_lines (map PolyML.makestring raw_bns))
+(*val _ = tracing (cat_lines (map PolyML.makestring raw_bns))*)
 in
 lthy
 |> add_datatype_wrapper raw_dt_names raw_dts
 ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs
 ||>> pair raw_binds
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 let
+val _ = tracing "Raw declarations";
 val thy = ProofContext.theory_of lthy
 val thy_name = Context.theory_name thy
 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) =
 raw_nominal_decls dts bn_funs bn_eqs binds lthy
 val morphism_2_1 = ProofContext.export_morphism lthy2 lthy
 val inject = flat (map #inject dtinfos);
 val distincts = flat (map #distinct dtinfos);
 val rel_distinct = map #distinct rel_dtinfos;
 val induct = #induct dtinfo;
 val inducts = #inducts dtinfo;
+val _ = tracing "Defining permutations, fv and alpha";
 val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
 val raw_binds_flat = map (map flat) raw_binds;
 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3;
 val alpha_ts_loc = #preds alpha
 val alpha_intros = #intrs alpha;
 val alpha_cases_loc = #elims alpha
 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4
 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
+val _ = tracing "Proving equivariance";
 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
-val _ = tracing "3";
 val fv_eqvt_tac =
 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5
-val _ = tracing "4";
 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc_nobn fv_eqvt_tac lthy5;
-val _ = tracing "4a";
 val (fv_bn_eqvts, lthy6a) =
 if fv_ts_loc_bn = [] then ([], lthy6) else
 fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts)
 (fv_ts_loc_bn ~~ (map snd bns)) lthy6;
-val _ = tracing "4b";
 val lthy6 = lthy6a;
 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
-val _ = tracing "5";
 fun alpha_eqvt_tac' _ =
 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
 else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc @ raw_fv_bv_eqvt_loc) lthy6 1
 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy6;
 val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
-val _ = map tracing (map PolyML.makestring alpha_eqvt)
+val _ = tracing "Proving equivalence";
 val alpha_equivp_loc =
 if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_loc_nobn
 else build_equivps alpha_ts_loc induct alpha_induct_loc
 inject alpha_inj_loc distincts alpha_cases_loc alpha_eqvt_loc lthy6;
 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
 val (consts_loc, const_defs) = split_list consts_defs;
 val morphism_8_7 = ProofContext.export_morphism lthy8 lthy7;
 val consts = map (Morphism.term morphism_8_7) consts_loc;
 (* Could be done nicer *)
 val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts);
+val _ = tracing "Proving respects";
 val (bns_rsp_pre, lthy9) = fold_map (
 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t]
 (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8;
 val bns_rsp = flat (map snd bns_rsp_pre);
 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts
 val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12;
 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a;
 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn
+val _ = tracing "Lifting permutations";
 val (qbn_defs, lthy12c) = fold_map Quotient_Def.quotient_lift_const (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
 val thy = Local_Theory.exit_global lthy12c;
 val perm_names = map (fn x => "permute_" ^ x) qty_names
 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
 val lthy13 = Theory_Target.init NONE thy';
 val q_name = space_implode "_" qty_names;
+val _ = tracing "Lifting induction";
 val q_induct = lift_thm lthy13 induct;
 val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13;
 val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct
 val (_, lthy14a) = Local_Theory.note ((Binding.name (q_name ^ "_inducts"), []), q_inducts) lthy14;
 val q_perm = map (lift_thm lthy14) raw_perm_def;
 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14a;
 val q_fv = map (lift_thm lthy15) fv_def;
 val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
 val q_bn = map (lift_thm lthy16) raw_bn_eqs;
 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16;
+val _ = tracing "Lifting pseudo-injectivity";
 val inj_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_inj
 val inj_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) inj_unfolded1
 val q_inj_pre1 = map (lift_thm lthy17) inj_unfolded2;
 val q_inj_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_inj_pre1
 val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre2
 val q_dis = map (lift_thm lthy18) rel_dists;
 val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18;
 val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt;
 val (_, lthy20) = Local_Theory.note ((Binding.empty,
 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
+val _ = tracing "Finite Support";
 val supports = map (prove_supports lthy20 q_perm) consts
-val _ = map tracing (map PolyML.makestring supports);
 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys) handle _ => []
 val thy3 = Local_Theory.exit_global lthy20;
 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3;
 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp))
 val lthy22 = Class.prove_instantiation_instance tac lthy21 handle _ => lthy20

changeset 1486	f86710d35146
parent 1484	dc7b049d9072
parent 1480	21cbb5b0e321
child 1494	923413256cbb