--- a/Nominal/Ex/Let.thy	Wed Jul 06 15:59:11 2011 +0200
+++ b/Nominal/Ex/Let.thy	Wed Jul 06 23:11:30 2011 +0200
@@ -31,6 +31,7 @@
 thm trm_assn.bn_defs
 thm trm_assn.bn_inducts
 thm trm_assn.perm_simps
+thm trm_assn.permute_bn
 thm trm_assn.induct
 thm trm_assn.inducts
 thm trm_assn.distinct

--- a/Nominal/Ex/LetInv.thy	Wed Jul 06 15:59:11 2011 +0200
+++ b/Nominal/Ex/LetInv.thy	Wed Jul 06 23:11:30 2011 +0200
@@ -238,7 +238,12 @@
   apply (auto simp add: fresh_star_def)[3]
   apply (drule_tac x="assn" in meta_spec)
   apply (simp add: Abs1_eq_iff alpha_bn_refl)
-  apply auto
+  apply auto[7]
+  prefer 2
+  apply(simp)
+  thm subst_sumC_def
+  thm THE_default_def
+  thm theI
   apply (erule_tac c="(sa, ta)" in Abs_lst1_fcb2)
   apply (simp add: Abs_fresh_iff)
   apply (simp add: fresh_star_def)

--- a/Nominal/Ex/NBE.thy	Wed Jul 06 15:59:11 2011 +0200
+++ b/Nominal/Ex/NBE.thy	Wed Jul 06 23:11:30 2011 +0200
@@ -13,7 +13,7 @@
 
 
 nominal_datatype sem =
-  L e::"env" x::"name" l::"lam" binds "bn e" x in l
+  L e::"env" x::"name" l::"lam" binds x "bn e" in l
 | N "neu"
 and neu = 
   V "name"
@@ -25,7 +25,8 @@
   bn
 where
   "bn ENil = []"
-| "bn (ECons env x v) = atom x # bn env" 
+| "bn (ECons env x v) = (atom x) # (bn env)" 
+
 
 nominal_primrec
   evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and
@@ -121,23 +122,33 @@
 done
 
 lemma test:
+  fixes env::"env"
   shows "supp (evals env t) \<subseteq> (supp t - set (bn env)) \<union> (fv_bn env)"
-  and "supp (evals_aux s t env) \<subseteq> ((supp s) - set (bn cenv)) \<union> supp (fn cenv) \<union> supp (evals env t)"
-apply(induct rule: evals_evals_aux.induct)
+  and "supp (evals_aux s t env) \<subseteq> (supp s) \<union> (fv_bn env) \<union> (supp (t) - set (bn env))"
+apply(induct env t and s t env rule: evals_evals_aux.induct)
 apply(simp add: sem_neu_env.supp lam.supp supp_Nil sem_neu_env.bn_defs)
 apply(simp add: sem_neu_env.supp lam.supp supp_Nil supp_Cons sem_neu_env.bn_defs)
 apply(rule conjI)
 apply(auto)[1]
 apply(rule impI)
 apply(simp)
-apply (metis (no_types) at_base_infinite finite_UNIV)
+apply(simp add: supp_at_base)
+apply(blast)
 apply(simp)
 apply(subst sem_neu_env.supp)
 apply(simp add: sem_neu_env.supp lam.supp)
 apply(auto)[1]
-apply(simp)
-apply(metis)
-sorry
+apply(simp add: lam.supp sem_neu_env.supp)
+apply(blast)
+apply(simp add: sem_neu_env.supp sem_neu_env.bn_defs)
+prefer 2
+apply(simp add: sem_neu_env.supp)
+apply(rule conjI)
+apply(blast)
+apply(blast)
+apply(blast)
+done
+
 
 nominal_primrec
   reify :: "sem \<Rightarrow> lam" and
@@ -197,13 +208,13 @@
 apply(simp)
 apply(erule conjE)
 apply (simp add: meta_eq_to_obj_eq[OF reify_def, symmetric, unfolded fun_eq_iff])
-apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons enva y (N (V x))) t)")
+apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons env y (N (V x))) t)")
 apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons enva ya (N (V xa))) ta)")
-apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons enva y (N (V x))) t))")
+apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons env y (N (V x))) t))")
 apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons enva ya (N (V xa))) ta))")
 defer
 apply (simp_all add: eqvt_at_def reify_def)[2]
-apply(subgoal_tac "\<exists>c::name. atom c \<sharp> (x, xa, enva, y, ya, t, ta)")
+apply(subgoal_tac "\<exists>c::name. atom c \<sharp> (x, xa, env, enva, y, ya, t, ta)")
 prefer 2
 apply(rule obtain_fresh)
 apply(blast)
@@ -218,7 +229,7 @@
 back
 apply(assumption)
 apply(simp add: finite_supp)
-apply(rule_tac S="supp (enva, y, x, t)" in supports_fresh)
+apply(rule_tac S="supp (env, y, x, t)" in supports_fresh)
 apply(simp add: supports_def fresh_def[symmetric])
 apply(perm_simp)
 apply(simp add: swap_fresh_fresh fresh_Pair)
@@ -250,6 +261,49 @@
 apply(perm_simp)
 apply(simp add: flip_fresh_fresh)
 apply(simp (no_asm) add: Abs1_eq_iff)
+thm at_set_avoiding3
+using at_set_avoiding3
+apply -
+apply(drule_tac x="set (atom y # bn env)" in meta_spec)
+apply(drule_tac x="(env, enva)" in meta_spec)
+apply(drule_tac x="[atom y # bn env]lst. t" in meta_spec)
+apply(simp (no_asm_use) add: finite_supp)
+apply(drule meta_mp)
+apply(rule Abs_fresh_star)
+apply(auto)[1]
+apply(erule exE)
+apply(erule conjE)+
+apply(drule_tac q="(x \<leftrightarrow> c)" in eqvt_at_perm)
+apply(perm_simp)
+apply(simp add: flip_fresh_fresh fresh_Pair)
+apply(drule_tac q="(xa \<leftrightarrow> c)" in eqvt_at_perm)
+apply(perm_simp)
+apply(simp add: flip_fresh_fresh fresh_Pair)
+apply(drule sym)
+apply(rotate_tac 9)
+apply(drule trans)
+apply(rule sym)
+(* HERE *)
+
+apply(rule_tac p="p" in supp_perm_eq)
+apply(simp)
+apply(perm_simp)
+apply(simp add: Abs_eq_iff2 alphas)
+apply(clarify)
+apply(rule trans)
+apply(rule sym)
+apply(rule_tac p="pa" in perm_supp_eq)
+defer
+apply(rule sym)
+apply(rule trans)
+apply(rule sym)
+apply(rule_tac p="p" in perm_supp_eq)
+defer
+apply(simp add: atom_eqvt)
+apply(drule_tac q="(x \<leftrightarrow> c)" in eqvt_at_perm)
+apply(perm_simp)
+apply(simp add: flip_fresh_fresh fresh_Pair)
+
 apply(rule sym)
 apply(erule_tac Abs_lst1_fcb2')
 apply(rule fresh_eqvt_at)