--- a/Nominal/Lift.thy Tue Mar 02 13:28:54 2010 +0100
+++ b/Nominal/Lift.thy Tue Mar 02 14:24:57 2010 +0100
@@ -25,7 +25,7 @@
val ntnames = [@{binding trm2}, @{binding as}]
val ncnames = ["Vr2", "Ap2", "Lt2", "As"] *} *)
-(* datatype rkind =
+datatype rkind =
Type
| KPi "rty" "name" "rkind"
and rty =
@@ -41,16 +41,16 @@
val thy1 = @{theory};
val info = Datatype.the_info @{theory} "Lift.rkind"
val number = 3;
-val binds = [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
- [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
- [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]];
+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"]*} *)
+val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"]
-datatype rtrm5 =
+(*datatype rtrm5 =
rVr5 "name"
| rAp5 "rtrm5" "rtrm5"
| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
@@ -64,18 +64,17 @@
"rbv5 rLnil = {}"
| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
-ML Typedef.add_typedef
-
-ML {*
+ML
val thy1 = @{theory};
val info = Datatype.the_info @{theory} "Lift.rtrm5"
val number = 2;
-val binds = [ [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ]
+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 ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"]*)
+
val descr = #descr info;
val sorts = #sorts info;
@@ -113,7 +112,7 @@
val (bv_eqvts, lthy3) = fold_map build_bv_eqvt 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_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 alpha_eqvt_loc lthy4;
val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc
val lthy5 = define_quotient_type
@@ -126,19 +125,19 @@
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 ((_, fv_rsp), lthy7) = prove_const_rsp Binding.empty fv_ts
- (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy6
-val (bvs_rsp', lthy8) = fold_map (
+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 lthy7
-val bvs_rsp = flat (map snd bvs_rsp')
+ (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 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;