--- 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