--- a/Nominal/Fv.thy	Thu Mar 18 08:03:42 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 18 08:32:55 2010 +0100
@@ -754,16 +754,6 @@
       | SOME i => i
 *}
 
-ML {*
-fun rename_vars fnctn thm =
-let
-  val vars = Term.add_vars (prop_of thm) []
-  val nvars = map (Var o ((apfst o apfst) fnctn)) vars
-in
-  Thm.certify_instantiate ([], (vars ~~ nvars))  thm
-end
-*}
-
 lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"
 by auto
 

--- a/Nominal/LFex.thy	Thu Mar 18 08:03:42 2010 +0100
+++ b/Nominal/LFex.thy	Thu Mar 18 08:32:55 2010 +0100
@@ -37,14 +37,14 @@
 
 lemma supp_eqs:
   "supp Type = {}"
-  "supp rkind = fv_kind rkind \<Longrightarrow> supp (KPi rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)"
+  "supp kind = fv_kind kind \<Longrightarrow> supp (KPi ty name kind) = supp ty \<union> supp (Abs {atom name} kind)"
   "supp (TConst i) = {atom i}"
   "supp (TApp A M) = supp A \<union> supp M"
-  "supp rty2 = fv_ty rty2 \<Longrightarrow> supp (TPi rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)"
+  "supp ty2 = fv_ty ty2 \<Longrightarrow> supp (TPi ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)"
   "supp (Const i) = {atom i}"
   "supp (Var x) = {atom x}"
   "supp (App M N) = supp M \<union> supp N"
-  "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (Lam rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)"
+  "supp trm = fv_trm trm \<Longrightarrow> supp (Lam ty name trm) = supp ty \<union> supp (Abs {atom name} trm)"
   apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt kind_ty_trm_perm)
   apply(simp_all only: kind_ty_trm_eq_iff Abs_eq_iff alpha_gen)
   apply(simp_all only: ex_out)
@@ -64,7 +64,7 @@
   apply(simp_all add: supp_Abs)
   done
 
-lemma supp_rkind_rty_rtrm:
+lemma supp_kind_ty_trm:
   "supp Type = {}"
   "supp (KPi A x K) = supp A \<union> (supp K - {atom x})"
   "supp (TConst i) = {atom i}"

--- a/Nominal/Lift.thy	Thu Mar 18 08:03:42 2010 +0100
+++ b/Nominal/Lift.thy	Thu Mar 18 08:32:55 2010 +0100
@@ -3,14 +3,45 @@
 begin
 
 ML {*
-fun lift_thm ctxt thm =
+fun rename_vars fnctn thm =
+let
+  val vars = Term.add_vars (prop_of thm) []
+  val nvars = map (Var o ((apfst o apfst) fnctn)) vars
+in
+  Thm.certify_instantiate ([], (vars ~~ nvars))  thm
+end
+*}
+
+ML {*
+fun un_raws name =
 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)))
+in
+  implode (map un_raw (add_under (space_explode "_" name)))
+end
+*}
+
+(* Similar to Tools/IsaPlanner/rw_tools.ML *)
+ML {*
+fun rename_term_bvars (Abs(s, ty, t)) = (Abs(un_raws s, ty, rename_term_bvars t))
+  | rename_term_bvars (a $ b) = (rename_term_bvars a) $ (rename_term_bvars b)
+  | rename_term_bvars x = x;
+
+fun rename_thm_bvars th =
+let
+  val t = Thm.prop_of th
+in
+  Thm.rename_boundvars t (rename_term_bvars t) th
+end;
+*}
+
+ML {*
+fun lift_thm ctxt thm =
+let
   val un_raw_names = rename_vars un_raws
 in
-  un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm)))
+  rename_thm_bvars (un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm))))
 end
 *}
 

--- a/Nominal/Test.thy	Thu Mar 18 08:03:42 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 18 08:32:55 2010 +0100
@@ -43,7 +43,7 @@
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 apply(simp only: supp_def[symmetric])
-apply(rule_tac t="supp (Lm name lm_raw)" and s="supp (Abs {atom name} lm_raw)" in subst)
+apply(rule_tac t="supp (Lm name lm)" and s="supp (Abs {atom name} lm)" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lm_perm)
 apply(simp only: permute_ABS)
@@ -68,8 +68,8 @@
 lemma
   assumes a0: "finite (supp c)"
   and     a1: "\<And>name c. P c (Vr name)"
-  and     a2: "\<And>lm_raw1 lm_raw2 c. \<lbrakk>\<And>d. P d lm_raw1; \<And>d. P d lm_raw2\<rbrakk> \<Longrightarrow> P c (Ap lm_raw1 lm_raw2)"
-  and     a3: "\<And>name lm_raw c. \<lbrakk>\<And>d. P d lm_raw\<rbrakk> \<Longrightarrow> P c (Lm name lm_raw)"
+  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
+  and     a3: "\<And>name lm c. \<lbrakk>\<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
   shows "P c lm"
 proof -
   have "\<And>p c. P c (p \<bullet> lm)"
@@ -80,11 +80,11 @@
     apply(rule a2)
     apply(assumption)
     apply(assumption)
-    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm_raw)) 
+    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm)) 
                           \<and> sort_of (atom new) = sort_of (atom name)")
     apply(erule exE)
-    apply(rule_tac t="(p \<bullet> Lm name lm_raw)" and 
-                   s="((((atom (p \<bullet> name)) \<rightleftharpoons> (atom new)) + p) \<bullet> Lm name lm_raw)" in subst)
+    apply(rule_tac t="(p \<bullet> Lm name lm)" and 
+                   s="((((atom (p \<bullet> name)) \<rightleftharpoons> (atom new)) + p) \<bullet> Lm name lm)" in subst)
     apply(simp)
     apply(subst lm_perm)
     apply(subst (2) lm_perm)
@@ -150,7 +150,7 @@
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 (* LAM case *)
-apply(rule_tac t="supp (LAM name lam_raw)" and s="supp (Abs {atom name} lam_raw)" in subst)
+apply(rule_tac t="supp (LAM name lam)" and s="supp (Abs {atom name} lam)" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam_bp_perm)
 apply(simp only: permute_ABS)
@@ -162,7 +162,7 @@
 apply(simp only: eqvts)
 apply(simp only: supp_Abs)
 (* LET case *)
-apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs (bi bp_raw) lam_raw) \<union> fv_bi bp_raw" in subst)
+apply(rule_tac t="supp (LET bp lam)" and s="supp (Abs (bi bp) lam) \<union> fv_bi bp" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam_bp_perm)
 apply(simp only: permute_ABS)
@@ -239,7 +239,7 @@
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 (* LAM case *)
-apply(rule_tac t="supp (LAM' name lam'_raw)" and s="supp (Abs {atom name} lam'_raw)" in subst)
+apply(rule_tac t="supp (LAM' name lam')" and s="supp (Abs {atom name} lam')" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam'_bp'_perm)
 apply(simp only: permute_ABS)
@@ -251,8 +251,8 @@
 apply(simp only: eqvts)
 apply(simp only: supp_Abs)
 (* LET case *)
-apply(rule_tac t="supp (LET' bp'_raw lam'_raw)" and 
-               s="supp (Abs (bi' bp'_raw) (bp'_raw, lam'_raw))" in subst)
+apply(rule_tac t="supp (LET' bp' lam')" and 
+               s="supp (Abs (bi' bp') (bp', lam'))" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam'_bp'_perm)
 apply(simp only: permute_ABS)
@@ -325,7 +325,7 @@
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 (* LAM case *)
-apply(rule_tac t="supp (Lam name trm'_raw)" and s="supp (Abs {atom name} trm'_raw)" in subst)
+apply(rule_tac t="supp (Lam name trm')" and s="supp (Abs {atom name} trm')" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: trm'_pat'_perm)
 apply(simp only: permute_ABS)
@@ -337,8 +337,8 @@
 apply(simp only: eqvts)
 apply(simp only: supp_Abs)
 (* LET case *)
-apply(rule_tac t="supp (Let pat'_raw trm'_raw1 trm'_raw2)" 
-           and s="supp (Abs (f pat'_raw) trm'_raw2) \<union> supp trm'_raw1 \<union> fv_f pat'_raw" in subst)
+apply(rule_tac t="supp (Let pat' trm'1 trm'2)" 
+           and s="supp (Abs (f pat') trm'2) \<union> supp trm'1 \<union> fv_f pat'" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: trm'_pat'_perm)
 apply(simp only: permute_ABS)
@@ -460,7 +460,7 @@
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 (* All case *)
-apply(rule_tac t="supp (All fun t_raw)" and s="supp (Abs (atom ` fun) t_raw)" in subst)
+apply(rule_tac t="supp (All fun t)" and s="supp (Abs (atom ` fun) t)" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: t_tyS_perm)
 apply(simp only: permute_ABS)

--- a/Nominal/TySch.thy	Thu Mar 18 08:03:42 2010 +0100
+++ b/Nominal/TySch.thy	Thu Mar 18 08:32:55 2010 +0100
@@ -9,7 +9,6 @@
 ML {* val _ = cheat_equivp := false *}
 ML {* val _ = cheat_fv_eqvt := false *}
 ML {* val _ = cheat_alpha_eqvt := false *}
-ML {* val _ = recursive := false  *}
 
 nominal_datatype t =
   Var "name"
@@ -24,68 +23,6 @@
 thm t_tyS_induct
 thm t_tyS_distinct
 
-lemma supports:
-  "(supp (atom i)) supports (Var i)"
-  "(supp A \<union> supp M) supports (Fun A M)"
-apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh t_tyS_perm)
-apply clarify
-apply(simp_all add: fresh_atom)
-done
-
-lemma fs:
-  "finite (supp (x\<Colon>t)) \<and> finite (supp (z\<Colon>tyS))"
-apply(induct rule: t_tyS_induct)
-apply(rule supports_finite)
-apply(rule supports)
-apply(simp add: supp_atom)
-apply(rule supports_finite)
-apply(rule supports)
-apply(simp add: supp_atom)
-sorry
-
-instance t and tyS :: fs
-apply default
-apply (simp_all add: fs)
-sorry
-
-(* Should be moved to a proper place *)
-lemma infinite_Un:
-  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
-  by simp
-
-lemma supp_fv_t_tyS:
-  shows "supp T = fv_t T" 
-  and   "supp S = fv_tyS S"
-apply(induct T and S rule: t_tyS_inducts)
-apply(simp_all add: t_tyS_fv)
-(* VarTS case *)
-apply(simp only: supp_def)
-apply(simp only: t_tyS_perm)
-apply(simp only: t_tyS_eq_iff)
-apply(simp only: supp_def[symmetric])
-apply(simp only: supp_at_base)
-(* FunTS case *)
-apply(simp only: supp_def)
-apply(simp only: t_tyS_perm)
-apply(simp only: t_tyS_eq_iff)
-apply(simp only: de_Morgan_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-(* All case *)
-apply(rule_tac t="supp (All fun t_raw)" and s="supp (Abs (atom ` fun) t_raw)" in subst)
-apply(simp (no_asm) only: supp_def)
-apply(simp only: t_tyS_perm)
-apply(simp only: permute_ABS)
-apply(simp only: t_tyS_eq_iff)
-apply(simp only: Abs_eq_iff)
-apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw)
-apply(simp only: alpha_gen)
-apply(simp only: supp_eqvt[symmetric])
-apply(simp only: eqvts)
-apply(simp only: supp_Abs)
-done
-
 lemma
   shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))"
   apply(simp add: t_tyS_eq_iff)
@@ -120,5 +57,4 @@
   apply auto
   done
 
-
 end