
diff -r 92dc6cfa3a95 -r 3772bb3bd7ce Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Wed Aug 25 22:55:42 2010 +0800
+++ b/Nominal/NewParser.thy	Wed Aug 25 23:16:42 2010 +0800
@@ -1,10 +1,28 @@
 theory NewParser
-imports "../Nominal-General/Nominal2_Base" 
-        "../Nominal-General/Nominal2_Eqvt" 
-        "../Nominal-General/Nominal2_Supp" 
-        "Perm" "Tacs" "Equivp"
+imports 
+  "../Nominal-General/Nominal2_Base" 
+  "../Nominal-General/Nominal2_Eqvt" 
+  "../Nominal-General/Nominal2_Supp" 
+  "Nominal2_FSet"
+  "Abs"
+uses ("nominal_dt_rawperm.ML")
+     ("nominal_dt_rawfuns.ML")
+     ("nominal_dt_alpha.ML")
+     ("nominal_dt_quot.ML")
 begin
 
+use "nominal_dt_rawperm.ML"
+ML {* open Nominal_Dt_RawPerm *}
+
+use "nominal_dt_rawfuns.ML"
+ML {* open Nominal_Dt_RawFuns *}
+
+use "nominal_dt_alpha.ML"
+ML {* open Nominal_Dt_Alpha *}
+
+use "nominal_dt_quot.ML"
+ML {* open Nominal_Dt_Quot *}
+
 
 section{* Interface for nominal_datatype *}
 
@@ -517,115 +535,8 @@
     if get_STEPS lthy > 21
     then true else raise TEST lthy9'
   
-  (* old stuff *)
-
-  val thy = ProofContext.theory_of lthy9'
-  val thy_name = Context.theory_name thy  
-  val qty_full_names = map (Long_Name.qualify thy_name) qty_names 
-
-  val _ = warning "Proving respects";
-
-  val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
-  val bns = raw_bns ~~ bn_nos;
-
-  val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_defs (map fst bns) lthy9';
-  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 lthy9';
-  val bns_rsp = flat (map snd bns_rsp_pre);
-
-  fun fv_rsp_tac _ = fvbv_rsp_tac alpha_induct raw_fv_defs lthy9' 1;
-
-  val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos
-
-  val fv_rsps = prove_fv_rsp fv_alpha_all alpha_trms 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) (raw_fvs @ raw_fv_bns) lthy9;
-  val fv_rsp = flat (map snd fv_rsp_pre);
-  val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs
-    (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
-  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;
-  val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
-    alpha_bn_rsp_tac) alpha_bn_trms lthy11
-  fun const_rsp_tac _ =
-    let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a
-      in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end
-  val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
-    const_rsp_tac) raw_constrs lthy11a
-  val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns)
-  val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns)
-  val (qfv_info, lthy12a) = define_qconsts qtys dd lthy12;
-  val qfv_ts = map #qconst qfv_info
-  val qfv_defs = map #def qfv_info
-  val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts;
-  val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
-  val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bns
-  val (qbn_info, lthy12b) = define_qconsts qtys dd lthy12a;
-  val qbn_ts = map #qconst qbn_info
-  val qbn_defs = map #def qbn_info
-  val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms
-  val dd = map2 (fn x => fn y => (x, y, NoSyn)) qalpha_bn_names alpha_bn_trms
-  val (qalpha_info, lthy12c) = define_qconsts qtys dd lthy12b;
-  val qalpha_bn_trms = map #qconst qalpha_info
-  val qalphabn_defs = map #def qalpha_info
-  
-  val _ = warning "Lifting permutations";
-  val perm_names = map (fn x => "permute_" ^ x) qty_names
-  val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs
-  val lthy13 = define_qperms qtys qty_full_names [] dd raw_perm_laws lthy12c
-  
-  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) [];
-  val q_induct = Rule_Cases.name constr_names (the_single (fst (lift_thms qtys [] [raw_induct_thm] lthy13)));
-  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 raw_fvs)) q_induct
-  val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
-  val q_perm = fst (lift_thms qtys [] raw_perm_simps lthy14);
-  val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
-  val q_fv = fst (lift_thms qtys [] raw_fv_defs lthy15);
-  val lthy16 = note_simp_suffix "fv" q_fv lthy15;
-  val q_bn = fst (lift_thms qtys [] raw_bn_defs lthy16);
-  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 alphas}) alpha_eq_iff
-  val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0
-  val q_eq_iff_pre0 = fst (lift_thms qtys [] eq_iff_unfolded1 lthy17);
-  val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms Pair_eqvt}) q_eq_iff_pre0
-  val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1
-  val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2
-  val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
-  val q_dis = fst (lift_thms qtys [] alpha_distincts lthy18);
-  val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
-  val q_eqvt = fst (lift_thms qtys [] (raw_bn_eqvt @ raw_fv_eqvt) lthy19);
-  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) [];
-  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 = Class.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_trms, qalpha_bn_trms) bn_nos;
-  val (names, supp_eq_t) = supp_eq fv_alpha_all;
-  val _ = warning "Support Equations";
-  fun supp_eq_tac' _ =  supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1;
-  val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e =>
-    let val _ = warning ("Support eqs failed") in [] end;
-  val lthy23 = note_suffix "supp" q_supp lthy22;
 in
-  (0, lthy23)
+  (0, lthy9')
 end handle TEST ctxt => (0, ctxt)
 *}
 
@@ -855,73 +766,6 @@
 *}
 
 
-text {* 
-  nominal_datatype2 does the following things in order:
-
-Parser.thy/raw_nominal_decls
-  1) define the raw datatype
-  2) define the raw binding functions 
-
-Perm.thy/define_raw_perms
-  3) define permutations of the raw datatype and show that the raw type is 
-     in the pt typeclass
-      
-Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha
-  4) define fv and fv_bn
-  5) define alpha and alpha_bn
-
-Perm.thy/distinct_rel
-  6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...)             (Proof by cases; simp)
-
-Tacs.thy/build_rel_inj
-  6) prove alpha_eq_iff    (C1 x = C2 y \<leftrightarrow> P x y ...)
-     (left-to-right by intro rule, right-to-left by cases; simp)
-Equivp.thy/prove_eqvt
-  7) prove bn_eqvt (common induction on the raw datatype)
-  8) prove fv_eqvt (common induction on the raw datatype with help of above)
-Rsp.thy/build_alpha_eqvts
-  9) prove alpha_eqvt and alpha_bn_eqvt
-     (common alpha-induction, unfolding alpha_gen, permute of #* and =)
-Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps
- 10) prove that alpha and alpha_bn are equivalence relations
-     (common induction and application of 'compose' lemmas)
-Lift.thy/define_quotient_types
- 11) define quotient types
-Rsp.thy/build_fvbv_rsps
- 12) prove bn respects     (common induction and simp with alpha_gen)
-Rsp.thy/prove_const_rsp
- 13) prove fv respects     (common induction and simp with alpha_gen)
- 14) prove permute respects    (unfolds to alpha_eqvt)
-Rsp.thy/prove_alpha_bn_rsp
- 15) prove alpha_bn respects
-     (alpha_induct then cases then sym and trans of the relations)
-Rsp.thy/prove_alpha_alphabn
- 16) show that alpha implies alpha_bn (by unduction, needed in following step)
-Rsp.thy/prove_const_rsp
- 17) prove respects for all datatype constructors
-     (unfold eq_iff and alpha_gen; introduce zero permutations; simp)
-Perm.thy/quotient_lift_consts_export
- 18) define lifted constructors, fv, bn, alpha_bn, permutations
-Perm.thy/define_lifted_perms
- 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass
-Lift.thy/lift_thm
- 20) lift permutation simplifications
- 21) lift induction
- 22) lift fv
- 23) lift bn
- 24) lift eq_iff
- 25) lift alpha_distincts
- 26) lift fv and bn eqvts
-Equivp.thy/prove_supports
- 27) prove that union of arguments supports constructors
-Equivp.thy/prove_fs
- 28) show that the lifted type is in fs typeclass     (* by q_induct, supports *)
-Equivp.thy/supp_eq
- 29) prove supp = fv
-*}
-
-
-
 end
 
 




