--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Lift.thy	Thu Feb 25 15:40:09 2010 +0100
@@ -0,0 +1,89 @@
+theory Lift
+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 {*
+fun build_eqvts_ funs perms simps induct ctxt =
+let
+  val pi = Free ("pi", @{typ perm});
+  val types = map (domain_type o fastype_of) funs;
+  val fv_indnames = Datatype_Prop.make_tnames (map body_type types);
+  val args = map Free (fv_indnames ~~ types);
+  val perm_at = Const (@{const_name permute}, @{typ "perm \<Rightarrow> atom set \<Rightarrow> atom set"})
+  fun eqvtc (fv, (arg, perm)) =
+    HOLogic.mk_eq ((perm_at $ pi $ (fv $ arg)), (fv $ (perm $ pi $ arg)))
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))
+  fun tac _ = (indtac induct fv_indnames THEN_ALL_NEW
+    (asm_full_simp_tac (HOL_ss addsimps 
+      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1
+in
+  Goal.prove ctxt ("pi" :: fv_indnames) [] gl tac
+end
+*}
+
+
+ML {*
+print_depth 500;
+val thy1 = @{theory};
+val tnames = ["rtrm2", "ras"];
+val ftname = "Lift.rtrm2"
+val binds = [[[[]], [[], []], [[], [(SOME @{term rbv2}, 0)]]], 
+             [[[], []]]  (*, [[], [[], []]] *) ];
+val bv_simps = @{thms rbv2.simps}
+val info = Datatype.the_info @{theory} ftname;
+val descr = #descr info;
+val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
+val full_tnames = List.take (all_full_tnames, length tnames);
+val induct = #induct info;
+val inducts = #inducts info;
+val infos = map (Datatype.the_info @{theory}) all_full_tnames;
+val inject = flat (map #inject infos);
+val distinct = flat (map #distinct infos);
+val ((raw_perm_def, raw_perm_simps, perms), thy2) = define_raw_perms tnames full_tnames thy1;
+val lthy1 = Theory_Target.init NONE thy2
+val (((fv_ts_loc, fv_def_loc), alpha), lthy2) = define_fv_alpha ftname binds lthy1;
+val alpha_ts = #preds alpha
+val alpha_intros = #intrs alpha
+val alpha_cases = #elims alpha
+val alpha_induct = #induct alpha
+val alpha_inj = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy2
+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 (bv_eqvts, lthy3) = build_eqvts @{binding bv_eqvts} [@{term rbv2}] [hd (tl perms)] 
+  (bv_simps @ raw_perm_def) @{thm rtrm2_ras.inducts(2)} lthy2;
+val (fv_eqvts, lthy4) = build_eqvts @{binding fv_eqvts} fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3;
+val alpha_eqvt = build_alpha_eqvts alpha_ts perms (raw_perm_def @ alpha_inj) alpha_induct lthy4;
+val alpha_equivp = build_equivps alpha_ts induct alpha_induct inject alpha_inj distinct alpha_cases alpha_eqvt lthy4
+
+*}
+
+
+
+ML {*
+  val thyf = Local_Theory.exit_global lthy4
+*}
+setup {* fn _ => thyf *}
+print_theorems
+
+ML {*
+(*val thyn = @{theory}
+val lthy3 = Theory_Target.init NONE thyn;*)
+build_equivps alpha_ts induct alpha_induct inject alpha_inj distinct alpha_cases @{thms alpha2_eqvt} lthy2
+
+*}
+
+

--- a/Nominal/Term1.thy	Thu Feb 25 14:14:40 2010 +0100
+++ b/Nominal/Term1.thy	Thu Feb 25 15:40:09 2010 +0100
@@ -74,6 +74,7 @@
   apply (subst permute_minus_cancel(2)[symmetric,of "b" "pi"])
   apply (simp_all only: alpha1_eqvt)
 done
+thm eqvts_raw(1)
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []),
   (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *}