
diff -r 52f68b524fd2 -r 923413256cbb Nominal/Lift.thy
--- 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
 




