--- a/Nominal/Parser.thy	Thu Mar 11 15:10:07 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 16:12:15 2010 +0100
@@ -253,7 +253,13 @@
 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
@@ -269,8 +275,13 @@
 end
 *}
 
-ML {* val restricted_nominal=ref 0 *}
-ML {* val cheat_alpha_eqvt = ref true *}
+(* These 2 are critical, we don't know how to do it in term5 *)
+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 =
@@ -302,9 +313,13 @@
   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
@@ -321,27 +336,24 @@
   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
-if !restricted_nominal = 0 then
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
-else
-let
-  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 (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
+  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 (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac 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 = build_equivps alpha_ts_loc induct alpha_induct_loc
-    inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;
+  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
+    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 =
@@ -351,56 +363,55 @@
           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
-    (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy9;
-  val (const_rsps, lthy11) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
-    (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bns_rsp) alpha_equivp 1)) raw_consts lthy10
-  val (perms_rsp, lthy12) = prove_const_rsp Binding.empty perms
-    (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy11;
-  val qfv_names = map (fn x => "fv_" ^ x) qty_names
+  fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
+    else fvbv_rsp_tac alpha_induct fv_def 1;
+  val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9
+  val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms
+    (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
+  fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy
+    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    *)