diff -r 2ceec1b4b015 -r 7ee9a2fefc77 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Sat May 01 09:14:25 2010 +0100
+++ b/Nominal/NewParser.thy	Sat May 01 09:15:46 2010 +0100
@@ -2,7 +2,7 @@
 imports "../Nominal-General/Nominal2_Base" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
-        "Perm" "NewFv" "NewAlpha"
+        "Perm" "NewFv" "NewAlpha" "Tacs" "Equivp" "Lift"
 begin
 
 section{* Interface for nominal_datatype *}
@@ -266,6 +266,18 @@
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
   val {descr, sorts, ...} = dtinfo;
+  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+  val raw_tys = map (fn (i, _) => nth_dtyp i) descr;
+  val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
+
+  val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
+  val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames;
+  val inject = flat (map #inject dtinfos);
+  val distincts = flat (map #distinct dtinfos);
+  val rel_dtinfos = List.take (dtinfos, (length dts));
+  val rel_distinct = map #distinct rel_dtinfos;
+  val induct = #induct dtinfo;
+  val exhausts = map #exhaust dtinfos;
 
   val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1;
@@ -274,14 +286,130 @@
   fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
   val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
   val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
+  val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc
   val thy = Local_Theory.exit_global lthy2;
+  val thy_name = Context.theory_name thy
   val lthy3 = Theory_Target.init NONE thy;
+  val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls;
 
-  val ((fv, fvbn), fvsimps, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
-  val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy5) =
-    define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy4;
+  val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
+  val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
+    define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a;
+  val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
+  val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
+  val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
+  val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
+  val bns = raw_bn_funs ~~ bn_nos;
+  val rel_dists = flat (map (distinct_rel lthy4 alpha_cases)
+    (rel_distinct ~~ alpha_ts_nobn));
+  val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
+    ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
+  val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4
+  val _ = warning "Proving equivariance";
+  val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
+  val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
+  fun alpha_eqvt_tac' _ = Skip_Proof.cheat_tac thy
+  val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
+  val _ = warning "Proving equivalence";
+  val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
+  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6;
+  val alpha_equivp =
+    build_equivps alpha_ts reflps alpha_induct
+      inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6;
+  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 (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn 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, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
+  val _ = warning "Proving respects";
+  val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
+  val (bns_rsp_pre, lthy9) = fold_map (
+    fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
+       resolve_tac bns_rsp_pre' 1)) bns lthy8;
+  val bns_rsp = flat (map snd bns_rsp_pre);
+  (*val _ = map tracing (map PolyML.makestring fv_alpha_all);*)
+  fun fv_rsp_tac _ = Skip_Proof.cheat_tac thy
+  val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
+  val (fv_rsp_pre, lthy10) = fold_map
+    (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
+    (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9;
+  val fv_rsp = flat (map snd fv_rsp_pre);
+  val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms
+    (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
+  val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
+        (fn _ => Skip_Proof.cheat_tac thy)) alpha_ts_bn lthy11
+  fun const_rsp_tac _ =
+    let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a
+      in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
+  val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
+    const_rsp_tac) raw_consts lthy11a
+    val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn)
+  val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12;
+  val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;
+  val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
+  val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (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 (qalpha_ts_bn, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
+  val _ = warning "Lifting permutations";
+  val thy = Local_Theory.exit_global lthy12c;
+  val perm_names = map (fn x => "permute_" ^ x) qty_names
+  val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
+  val lthy13 = Theory_Target.init NONE thy';
+  val q_name = space_implode "_" qty_names;
+  fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
+  val _ = warning "Lifting induction";
+  val constr_names = map (Long_Name.base_name o fst o dest_Const) consts;
+  val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct);
+  fun note_suffix s th ctxt =
+    snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
+  fun note_simp_suffix s th ctxt =
+    snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
+  val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",
+    [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13;
+  val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct
+  val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
+  val q_perm = map (lift_thm qtys lthy14) raw_perm_def;
+  val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
+  val q_fv = map (lift_thm qtys lthy15) fv_def;
+  val lthy16 = note_simp_suffix "fv" q_fv lthy15;
+  val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs;
+  val lthy17 = note_simp_suffix "bn" q_bn lthy16;
+  val _ = warning "Lifting eq-iff";
+  (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
+  val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff
+  val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0
+  val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1
+  val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2;
+  val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0
+  val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1
+  val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2
+  val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
+  val q_dis = map (lift_thm qtys lthy18) rel_dists;
+  val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
+  val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt);
+  val (_, lthy20) = Local_Theory.note ((Binding.empty,
+    [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
+  val _ = warning "Supports";
+  val supports = map (prove_supports lthy20 q_perm) consts;
+  val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys);
+  val thy3 = Local_Theory.exit_global lthy20;
+  val _ = warning "Instantiating FS";
+  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
+  val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos;
+  val (names, supp_eq_t) = supp_eq fv_alpha_all;
+  val _ = warning "Support Equations";
+  val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => [];
+  val lthy23 = note_suffix "supp" q_supp lthy22;
 in
-  ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy5)
+  (0, lthy23)
 end
 *}
 
@@ -467,8 +595,11 @@
   "bn (P1 x) = {atom x}"
 | "bn (P2 p1 p2) = bn p1 \<union> bn p2"
 
-thm fv_lam_raw.simps fv_pt_raw.simps fv_bn_raw.simps
-thm alpha_lam_raw_alpha_pt_raw_alpha_bn_raw.intros
+thm lam_pt.bn
+thm lam_pt.fv[simplified lam_pt.supp(1-2)]
+thm lam_pt.eq_iff
+thm lam_pt.induct
+thm lam_pt.perm
 
 nominal_datatype exp =
   EVar name
@@ -513,24 +644,29 @@
 | "b_lrb (Clause fcs) = (b_fnclauses fcs)"
 | "b_fnclause (K x pat exp) = [atom x]"
 
-typ exp_raw
-typ pat_raw
-thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars]
-thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars]
-thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars]
-thm fv_exp_raw.simps fv_fnclause_raw.simps fv_fnclauses_raw.simps fv_lrb_raw.simps fv_lrbs_raw.simps fv_pat_raw.simps fv_b_lrbs_raw.simps fv_b_pat_raw.simps fv_b_fnclauses_raw.simps fv_b_lrb_raw.simps fv_b_fnclause_raw.simps
-thm alpha_exp_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb_raw_alpha_lrbs_raw_alpha_pat_raw_alpha_b_lrbs_raw_alpha_b_pat_raw_alpha_b_fnclauses_raw_alpha_b_lrb_raw_alpha_b_fnclause_raw.intros[no_vars]
+thm exp_fnclause_fnclauses_lrb_lrbs_pat.bn
+thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv
+thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff
+thm exp_fnclause_fnclauses_lrb_lrbs_pat.induct
+thm exp_fnclause_fnclauses_lrb_lrbs_pat.perm
 
 nominal_datatype ty =
-  Var "name"
-| Fun "ty" "ty"
+  Vr "name"
+| Fn "ty" "ty"
+and tys =
+  Al xs::"name fset" t::"ty" bind_res xs in t
+
+thm ty_tys.fv[simplified ty_tys.supp]
+thm ty_tys.eq_iff
+
+(* some further tests *)
+
+nominal_datatype ty =
+  Vr "name"
+| Fn "ty" "ty"
 
 nominal_datatype tys =
   All xs::"name fset" ty::"ty_raw" bind_res xs in ty
-thm fv_tys_raw.simps
-thm alpha_tys_raw.intros
-
-(* some further tests *)
 
 nominal_datatype lam2 =
   Var2 "name"