--- a/Nominal/Ex/Lambda.thy	Thu Jun 09 15:34:51 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Fri Jun 10 15:30:09 2011 +0900
@@ -25,28 +25,6 @@
 abbreviation
   "FCB f \<equiv> \<forall>x t r. atom x \<sharp> f x t r" 
 
-lemma Abs1_eq_fdest:
-  fixes x y :: "'a :: at_base"
-    and S T :: "'b :: fs"
-  assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)"
-  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom x \<sharp> f x T"
-  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom y \<sharp> f x T"
-  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> T = S \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S"
-  and "sort_of (atom x) = sort_of (atom y)"
-  shows "f x T = f y S"
-using assms apply -
-thm Abs1_eq_iff'
-apply (subst (asm) Abs1_eq_iff')
-apply simp_all
-apply (elim conjE disjE)
-apply simp
-apply(rule trans)
-apply (rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric])
-apply(rule fresh_star_supp_conv)
-apply(simp add: supp_swap fresh_star_def)
-apply(simp add: swap_commute)
-done
-
 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y")
   frees_set :: "lam \<Rightarrow> atom set"
 where
@@ -64,7 +42,7 @@
 apply(simp)
 apply(simp)
 apply(simp)
-apply (erule Abs1_eq_fdest)
+apply (erule Abs_lst1_fcb)
 apply(simp add: fresh_def)
 apply(subst supp_of_finite_sets)
 apply(simp)
@@ -123,7 +101,7 @@
   apply(rule TrueI)
   apply(rule_tac y="x" in lam.exhaust)
   apply(auto simp add: fresh_star_def)
-  apply(erule Abs1_eq_fdest)
+  apply(erule Abs_lst1_fcb)
   apply simp_all
   apply(simp add: fcb)
   apply (rule fresh_fun_eqvt_app3[OF eq(3)])
@@ -211,7 +189,7 @@
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto simp add: lam.distinct lam.eq_iff)
-apply (erule Abs1_eq_fdest)
+apply (erule Abs_lst1_fcb)
 apply(simp_all add: fresh_def pure_supp eqvt_at_def)
 done
 
@@ -234,7 +212,7 @@
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)
-apply (erule Abs1_eq_fdest)
+apply (erule Abs_lst1_fcb)
 apply(simp add: supp_removeAll fresh_def)
 apply(drule supp_eqvt_at)
 apply(simp add: finite_supp)
@@ -266,7 +244,7 @@
 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
 apply(blast)+
 apply(simp_all add: fresh_star_def fresh_Pair_elim)
-apply (erule Abs1_eq_fdest)
+apply (erule Abs_lst1_fcb)
 apply(simp_all add: Abs_fresh_iff)
 apply(drule_tac a="atom (xa)" in fresh_eqvt_at)
 apply(simp_all add: finite_supp fresh_Pair)
@@ -455,7 +433,7 @@
   apply (simp add: ln.fresh fresh_star_def)
   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply (auto simp add: fresh_star_def)[3]
-  apply (erule Abs1_eq_fdest)
+  apply (erule Abs_lst1_fcb)
   apply (simp_all add: fresh_star_def)
   apply (drule supp_eqvt_at)
   apply (rule finite_supp)
@@ -479,7 +457,7 @@
   apply(case_tac x)
   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply(auto simp add: fresh_star_def)
-  apply(erule Abs1_eq_fdest)
+  apply(erule Abs_lst1_fcb)
   apply(simp_all add: pure_fresh)
   apply (simp add: eqvt_at_def swap_fresh_fresh)
   done
@@ -549,7 +527,7 @@
   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply (auto simp add: fresh_star_def fresh_at_list)
   apply (rule_tac f="dblam_in" in arg_cong)
-  apply (erule Abs1_eq_fdest)
+  apply (erule Abs_lst1_fcb)
   apply (simp_all add: pure_fresh)
   apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa")
   apply (simp add: eqvt_at_def)
@@ -651,7 +629,7 @@
 apply blast
 apply (simp add: Abs1_eq_iff fresh_star_def)
 apply(simp_all)
-apply(erule Abs1_eq_fdest)
+apply(erule Abs_lst1_fcb)
 apply (simp add: Abs_fresh_iff)
 apply (simp add: Abs_fresh_iff)
 apply (erule fresh_eqvt_at)
@@ -661,7 +639,7 @@
 apply simp
 defer
 apply clarify
-apply(erule Abs1_eq_fdest)
+apply(erule Abs_lst1_fcb)
 apply (erule fresh_eqvt_at)
 apply (simp add: finite_supp)
 apply (simp add: fresh_Inl var_fresh_subst)
@@ -671,7 +649,7 @@
 apply (simp add: fresh_def)
 using supp_subst apply blast
 apply (simp add: eqvt_at_def subst_eqvt)
-apply (subst swap_fresh_fresh)
+apply (subst (2) swap_fresh_fresh)
 apply assumption+
 apply rule
 apply simp
@@ -709,7 +687,7 @@
   apply(rule TrueI)
   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
   apply auto
-  apply (erule Abs1_eq_fdest)
+  apply (erule Abs_lst1_fcb)
   apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
   apply (simp add: eqvt_def permute_fun_app_eq)
   done