--- a/Nominal/Ex/NBE.thy	Fri Jul 15 22:48:37 2011 +0100
+++ b/Nominal/Ex/NBE.thy	Sat Jul 16 21:36:43 2011 +0100
@@ -27,8 +27,8 @@
   "bn ENil = []"
 | "bn (ECons env x v) = (atom x) # (bn env)" 
 
-
-nominal_primrec
+nominal_primrec  (invariant "\<lambda>x y. case x of Inl (x1, y1) \<Rightarrow> 
+  supp y \<subseteq> (supp y1 - set (bn x1)) \<union> (fv_bn x1) | Inr (x2, y2) \<Rightarrow> supp y \<subseteq> supp x2 \<union> supp y2")
   evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and
   evals_aux :: "sem \<Rightarrow> sem \<Rightarrow> sem"
 where
@@ -41,7 +41,22 @@
 apply(simp add: eqvt_def  evals_evals_aux_graph_def)
 apply(perm_simp)
 apply(simp)
-apply (rule TrueI)
+apply(erule evals_evals_aux_graph.induct)
+apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
+apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
+apply(rule conjI)
+apply(rule impI)
+apply(blast)
+apply(rule impI)
+apply(simp add: supp_at_base)
+apply(blast)
+apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
+apply(blast)
+apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
+apply(blast)
+apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
+apply(blast)
+apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
 --"completeness"
 apply(case_tac x)
 apply(simp)
@@ -88,11 +103,67 @@
 apply(simp add: fresh_star_Pair perm_supp_eq)
 apply(perm_simp)
 apply(simp add: fresh_star_Pair perm_supp_eq)
-thm Abs_lst1_fcb2'
+apply(simp add: sem_neu_env.bn_defs sem_neu_env.supp)
+using at_set_avoiding3
+apply -
+apply(drule_tac x="set (atom x # bn cenv)" in meta_spec)
+apply(drule_tac x="(cenv, cenva, x, xa, t, ta, t'a)" in meta_spec)
+apply(drule_tac x="[atom x # bn cenv]lst. t" in meta_spec)
+apply(simp (no_asm_use) add: finite_supp Abs_fresh_star_iff)
+apply(drule meta_mp)
+apply(simp add: fresh_star_def)
+apply(erule exE)
+apply(erule conjE)+
+thm Abs_fresh_star_iff
+
+
+apply(subgoal_tac "\<exists>c::name. atom c \<sharp> (x, xa, cenv, cenva, t, ta, t'a)")
+prefer 2
+apply(rule obtain_fresh)
+apply(blast)
+apply(erule exE)
+apply(drule trans)
+apply(rule sym)
+apply(rule_tac a="xa" and b="c" in flip_fresh_fresh)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: Abs_fresh_iff fresh_Pair fresh_at_base)
+apply(perm_simp)
+apply(simp)
+apply(rotate_tac 4)
+apply(drule sym)
+apply(rotate_tac 5)
+apply(drule trans)
+apply(rule sym)
+apply(rule_tac a="x" and b="c" in flip_fresh_fresh)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: Abs_fresh_iff fresh_Pair fresh_at_base)
+apply(perm_simp)
+apply(simp)
+(* HERE *)
+apply(auto)[1]
+apply(rule fresh_eqvt_at)
+back
+apply(assumption)
+apply(simp add: finite_supp)
+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)
+apply(simp add: finite_supp)
+apply(simp add: fresh_def[symmetric])
+apply(simp add: eqvt_at_def)
+apply(simp add: eqvt_at_def[symmetric])
+apply(perm_simp)
+apply(simp add: flip_fresh_fresh)
+apply(rule sym)
+apply(rule trans)
+
 sorry
 
 (* can probably not proved by a trivial size argument *)
-termination sorry
+termination apply(lexicographic_order)
+
+sorry
 
 lemma [eqvt]:
   shows "(p \<bullet> evals env t) = evals (p \<bullet> env) (p \<bullet> t)"