--- a/Nominal/Lift.thy Thu Mar 18 00:17:21 2010 +0100
+++ b/Nominal/Lift.thy Thu Mar 18 07:26:36 2010 +0100
@@ -1,156 +1,31 @@
theory Lift
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp"
begin
-atom_decl name
-atom_decl ident
-
-(* datatype rtrm2 =
- rVr2 "name"
-| rAp2 "rtrm2" "rtrm2"
-| rLt2 "ras" "rtrm2" --"bind (bv2 l) in (r)"
-and ras =
- rAs "name" "rtrm2"
-
-primrec rbv2 where "rbv2 (rAs x t) = {atom x}"
-ML {*
-val thy1 = @{theory};
-val info = Datatype.the_info @{theory} "Lift.rtrm2"
-val number = 2; (* Number of defined types, rest are unfoldings *)
-val binds = [[[[]], [[], []], [[], [(SOME @{term rbv2}, 0)]]],
- [[[], []]] (*, [[], [[], []]] *) ];
-val bvs = [(@{term rbv2}, 1)] (* Which type it operates on *)
-val bv_simps = @{thms rbv2.simps}
-
-val ntnames = [@{binding trm2}, @{binding as}]
-val ncnames = ["Vr2", "Ap2", "Lt2", "As"] *} *)
-
-(*datatype rkind =
- Type
- | KPi "rty" "name" "rkind"
-and rty =
- TConst "ident"
- | TApp "rty" "rtrm"
- | TPi "rty" "name" "rty"
-and rtrm =
- Const "ident"
- | Var "name"
- | App "rtrm" "rtrm"
- | Lam "rty" "name" "rtrm"
-ML {*
-val thy1 = @{theory};
-val info = Datatype.the_info @{theory} "Lift.rkind"
-val number = 3;
-val binds = [[ [], [(NONE, 1, 2)]],
- [ [], [], [(NONE, 1, 2)] ],
- [ [], [], [], [(NONE, 1, 2)]]];
-val bvs = []
-val bv_simps = []
-
-val ntnames = [@{binding kind}, @{binding ty}, @{binding trm}]
-val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"]*}*)
-
-datatype rtrm5 =
- rVr5 "name"
-| rAp5 "rtrm5" "rtrm5"
-| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
-and rlts =
- rLnil
-| rLcons "name" "rtrm5" "rlts"
-
-primrec
- rbv5
-where
- "rbv5 rLnil = {}"
-| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
-
-
-
ML {*
-val thy1 = @{theory};
-val info = Datatype.the_info @{theory} "Lift.rtrm5"
-val number = 2;
-val binds = [ [[], [], [(SOME @{term rbv5}, 0, 1)]], [[], []] ]
-val bvs = [(@{term rbv5}, 1)]
-val bv_simps = @{thms rbv5.simps}
-
-val ntnames = [@{binding trm5}, @{binding lts}]
-val ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"]
-
-
-val descr = #descr info;
-val sorts = #sorts info;
-val nos = map fst descr
-val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) nos
-val typs = List.take (all_typs, number)
-val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
-val induct = #induct info;
-val inducts = #inducts info;
-val infos = map (Datatype.the_info thy1) all_full_tnames;
-val rel_infos = List.take (infos, number);
-val inject = flat (map #inject infos);
-val distinct = flat (map #distinct infos);
-val rel_distinct = map #distinct rel_infos;
-val ((raw_perm_def, raw_perm_simps, perms), thy2) = define_raw_perms info number thy1;
-val lthy1 = Theory_Target.init NONE thy2
-val (((fv_ts_loc, fv_def_loc), alpha), lthy2) = define_fv_alpha info binds lthy1;
-val alpha_ts_loc = #preds alpha
-val alpha_intros = #intrs alpha
-val alpha_cases_loc = #elims alpha
-val alpha_induct_loc = #induct alpha
-val alpha_cases = ProofContext.export lthy2 lthy1 alpha_cases_loc
-val [alpha_induct] = ProofContext.export lthy2 lthy1 [alpha_induct_loc]
-(* TODO replace when inducts is provided by the 2 lines below: *)
-val alpha_inducts = Project_Rule.projects lthy2 (1 upto number) alpha_induct
-(*val alpha_inducts_loc = #inducts alpha
-val alpha_inducts = ProofContext.export lthy2 lthy1 alpha_inducts_loc*)
-val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy2
-val alpha_inj = ProofContext.export lthy2 lthy1 alpha_inj_loc
-val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc
-val morphism = ProofContext.export_morphism lthy2 lthy1
-val fv_ts = map (Morphism.term morphism) fv_ts_loc
-val alpha_ts = map (Morphism.term morphism) alpha_ts_loc
-val (bv_eqvts, lthy3) = fold_map (build_bv_eqvt perms (bv_simps @ raw_perm_def) inducts) bvs lthy2;
-val (fv_eqvts, lthy4) = build_eqvts Binding.empty fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3;
-val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy4;
-val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_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 lthy4;
-val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc
-val lthy5 = define_quotient_type
- (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((ntnames ~~ typs) ~~ alpha_ts))
- (ALLGOALS (resolve_tac alpha_equivp)) lthy4;
-val 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 (csdefl, lthy6) = fold_map Quotient_Def.quotient_lift_const (ncnames ~~ consts) lthy5;
-val (cs, def) = split_list csdefl;
-val (bvs_rsp', lthy7) = fold_map (
- fn (bv_t, i) => prove_const_rsp Binding.empty [bv_t]
- (fn _ => fvbv_rsp_tac (nth alpha_inducts i) bv_simps 1)) bvs lthy6;
-val ((_, fv_rsp), lthy8) = prove_const_rsp Binding.empty fv_ts
- (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy7;
-val bvs_rsp = flat (map snd bvs_rsp');
-val (const_rsps, lthy9) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
- (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bvs_rsp) alpha_equivp 1)) consts lthy8
-val (perms_rsp, lthy10) = prove_const_rsp Binding.empty perms
- (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy9;
-val thy3 = Local_Theory.exit_global lthy10;
-(* TODO: fix this hack... *)
-(*val tinfo = #abs_type (Typedef.the_info thy3 "Lift.trm5");*)
-(*val thy4 = define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})]
- @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append}*)
-val lthy11 = Theory_Target.init NONE thy3;
-val lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy11, induct));
-val lthy12 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy11);
-val rel_dists = flat (map (distinct_rel lthy12 alpha_cases) (rel_distinct ~~ (List.take (alpha_ts, number))))
-
+fun lift_thm ctxt thm =
+let
+ 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
+in
+ un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm)))
+end
*}
-setup {* fn _ => Local_Theory.exit_global lthy12 *}
-thm lift_induct
-
+ML {*
+fun quotient_lift_consts_export spec ctxt =
+let
+ val (result, ctxt') = fold_map Quotient_Def.quotient_lift_const spec ctxt;
+ val (ts_loc, defs_loc) = split_list result;
+ val morphism = ProofContext.export_morphism ctxt' ctxt;
+ val ts = map (Morphism.term morphism) ts_loc
+ val defs = Morphism.fact morphism defs_loc
+in
+ (ts, defs, ctxt')
+end
+*}
end
--- a/Nominal/Parser.thy Thu Mar 18 00:17:21 2010 +0100
+++ b/Nominal/Parser.thy Thu Mar 18 07:26:36 2010 +0100
@@ -1,5 +1,5 @@
theory Parser
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Perm" "Fv" "Rsp"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Perm" "Fv" "Rsp" "Lift"
begin
atom_decl name
@@ -253,14 +253,6 @@
end
*}
-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
ML {*
@@ -333,10 +325,11 @@
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 alpha_intros = #intrs alpha;
+ val alpha_intros_loc = #intrs alpha;
val alpha_cases_loc = #elims alpha
+ val alpha_intros = ProofContext.export lthy4 lthy3 alpha_intros_loc
val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
- val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4
+ val alpha_inj_loc = build_alpha_inj alpha_intros_loc (inject @ distincts) alpha_cases_loc lthy4
val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
val _ = tracing "Proving equivariance";
val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
@@ -350,18 +343,16 @@
(fv_ts_loc_bn ~~ (map snd bns)) lthy6;
val lthy6 = lthy6a;
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 raw_fv_bv_eqvt = ProofContext.export lthy6 lthy2 raw_fv_bv_eqvt_loc;
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 @ raw_fv_bv_eqvt_loc) lthy6 1
- val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy6;
- val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
+ else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_inj @ raw_fv_bv_eqvt) lthy6 1
+ val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
val _ = tracing "Proving equivalence";
- val alpha_equivp_loc =
- if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_loc_nobn
- else build_equivps alpha_ts_loc induct alpha_induct_loc
- inject alpha_inj_loc distincts alpha_cases_loc alpha_eqvt_loc lthy6;
- val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
+ val alpha_equivp =
+ if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn
+ else build_equivps alpha_ts induct alpha_induct
+ inject alpha_inj 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
@@ -374,10 +365,7 @@
map (fn (cname, dts) =>
Const (cname, map (typ_of_dtyp descr sorts) dts --->
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_loc, const_defs) = split_list consts_defs;
- val morphism_8_7 = ProofContext.export_morphism lthy8 lthy7;
- val consts = map (Morphism.term morphism_8_7) consts_loc;
+ val (consts, const_defs, lthy8) = quotient_lift_consts_export (const_names ~~ raw_consts) lthy7;
(* Could be done nicer *)
val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts);
val _ = tracing "Proving respects";