nominal2: comparison Nominal/Parser.thy

equal deleted inserted replaced

-:d59f851926c5
+:7e28654a760a
 ||>> pair raw_binds
 ||>> pair raw_bns
 end
 *}
-ML {* add_primrec_wrapper *}
+ML {*
+fun un_raw name = unprefix "_raw" name handle Fail _ => name
+fun add_under names = hd names :: (map (prefix "_") (tl names))
+fun un_raws name = implode (map un_raw (add_under (space_explode "_" name)))
+val un_raw_names = rename_vars un_raws
+fun lift_thm ctxt thm = un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm)))
+*}
 lemma equivp_hack: "equivp x"
 sorry
 ML {*
 fun equivp_hack ctxt rel =
 in
 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
 end
 *}
-ML {* val restricted_nominal=ref 0 *}
+(* These 2 are critical, we don't know how to do it in term5 *)
-ML {* val cheat_alpha_eqvt = ref true *}
+ML {* val cheat_fv_rsp = ref true *}
+ML {* val cheat_const_rsp = ref true *} (* For alpha_bn 0 and alpha_bn_rsp *)
+(* Fixes for these 2 are known *)
+ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
+ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 let
 val thy = ProofContext.theory_of lthy
 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_ts_loc_nobn = List.take (alpha_ts_loc, length perms)
 val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
 val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc;
+val fv_ts_loc_nobn = List.take (fv_ts_loc, length perms)
+val fv_ts_nobn = List.take (fv_ts, length perms)
 val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc;
+val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts
 val alpha_induct_loc = #induct alpha
 val [alpha_induct] = ProofContext.export lthy4 lthy3 [alpha_induct_loc];
 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct
 val fv_def = ProofContext.export lthy4 lthy3 fv_def_loc;
 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4
 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
 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) lthy4 1
-val alpha_eqvt_loc = build_alpha_eqvts (List.take (alpha_ts_loc, length perms)) perms alpha_eqvt_tac' lthy4;
+val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc_nobn perms alpha_eqvt_tac' lthy4;
 val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc;
-in
+val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
-if !restricted_nominal = 0 then
+val fv_eqvt_tac =
-((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
+if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
-else
+else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5
-let
+val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5;
-val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
-val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms
-((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5;
 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 alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc
+val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc_nobn
-val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
+(*  val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
-inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;
+inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;*)
 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
 val qty_binds = map (fn (_, b, _, _) => b) dts;
 val qty_names = map Name.of_binding qty_binds;
 val qty_full_names = map (Long_Name.qualify thy_name) qty_names
 val lthy7 = define_quotient_type
-(map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts))
+(map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn))
 (ALLGOALS (resolve_tac alpha_equivp)) lthy6;
 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
 val raw_consts =
 flat (map (fn (i, (_, _, l)) =>
 map (fn (cname, dts) =>
 Const (cname, map (typ_of_dtyp descr sorts) dts --->
 typ_of_dtyp descr sorts (DtRec i))) l) descr);
 val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7;
 val (consts, const_defs) = split_list consts_defs;
-in
-if !restricted_nominal = 1 then
-((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy8)
-else
-let
 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);
-val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts
+fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
-(fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy9;
+else fvbv_rsp_tac alpha_induct fv_def 1;
-val (const_rsps, lthy11) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
+val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9
-(fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bns_rsp) alpha_equivp 1)) raw_consts lthy10
+val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms
-val (perms_rsp, lthy12) = prove_const_rsp Binding.empty perms
+(fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
-(fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy11;
+fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy
-val qfv_names = map (fn x => "fv_" ^ x) qty_names
+else constr_rsp_tac alpha_inj (fv_rsp @ bns_rsp) alpha_equivp 1
+val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
+const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11
+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 thy = Local_Theory.exit_global lthy12b;
+val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn
+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 q_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy13, induct));
+val q_induct = lift_thm lthy13 induct;
 val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13;
-val q_perm = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy14, th))) raw_perm_def;
+val q_perm = map (lift_thm lthy14) raw_perm_def;
 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14;
-val q_fv = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy15, th))) fv_def;
+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 (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy16, th))) raw_bn_eqs;
+val q_bn = map (lift_thm lthy16) raw_bn_eqs;
 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16;
 val inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj
-val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded;
+val q_inj_pre = map (lift_thm lthy17) inj_unfolded;
 val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre
 val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;
 val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
 (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))
-val q_dis = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy18, th))) rel_dists;
+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 (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy19, th))) raw_fv_bv_eqvt;
+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;
 in
 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20)
 end
-end
+*}
-end
-*}
 ML {*
 (* parsing the datatypes and declaring *)
 (* constructors in the local theory    *)
 fun prepare_dts dt_strs lthy =

changeset 1424	7e28654a760a
parent 1422	a26cb19375e8
child 1428	4029105011ca