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 \ C2 y ...) (Proof by cases; simp) - -Tacs.thy/build_rel_inj - 6) prove alpha_eq_iff (C1 x = C2 y \ 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