--- a/Nominal/Ex/NBE.thy	Wed Jul 06 01:04:09 2011 +0200
+++ b/Nominal/Ex/NBE.thy	Wed Jul 06 15:59:11 2011 +0200
@@ -13,7 +13,7 @@
 
 
 nominal_datatype sem =
-  L "env" x::"name" l::"lam" binds x in l
+  L e::"env" x::"name" l::"lam" binds "bn e" x in l
 | N "neu"
 and neu = 
   V "name"
@@ -21,6 +21,11 @@
 and env =
   ENil
 | ECons "env" "name" "sem"
+binder
+  bn
+where
+  "bn ENil = []"
+| "bn (ECons env x v) = atom x # bn env" 
 
 nominal_primrec
   evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and
@@ -32,7 +37,37 @@
 | "evals env (App t1 t2) = evals_aux (evals env t1) t2 env"
 | "evals_aux (L cenv x t) t2 env = evals (ECons cenv x (evals env t2)) t"
 | "evals_aux (N n) t2 env = N (A n (evals env t2))"
-defer
+apply(subgoal_tac "\<And>p x y. evals_evals_aux_graph x y \<Longrightarrow> evals_evals_aux_graph (p \<bullet> x) (p \<bullet> y)")
+apply(simp add: eqvt_def)
+apply(simp add: permute_fun_def)
+apply(rule allI)
+apply(rule ext)
+apply(rule ext)
+apply(rule iffI)
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="- p \<bullet> x" in meta_spec)
+apply(drule_tac x="- p \<bullet> xa" in meta_spec)
+apply(simp add: permute_bool_def)
+apply(simp add: permute_bool_def)
+apply(erule evals_evals_aux_graph.induct)
+apply(perm_simp)
+apply(rule evals_evals_aux_graph.intros)
+apply(perm_simp)
+apply(rule evals_evals_aux_graph.intros)
+apply(simp)
+apply(perm_simp)
+apply(rule evals_evals_aux_graph.intros)
+apply(perm_simp)
+apply(rule evals_evals_aux_graph.intros)
+apply(simp)
+apply(simp)
+apply(perm_simp)
+apply(rule evals_evals_aux_graph.intros)
+apply(simp)
+apply(simp)
+apply(perm_simp)
+apply(rule evals_evals_aux_graph.intros)
+apply(simp)
 apply (rule TrueI)
 --"completeness"
 apply(case_tac x)
@@ -54,44 +89,102 @@
 apply(all_trivials)
 apply(simp)
 apply(simp)
+defer
 apply(simp)
 apply(simp)
 apply (simp add: meta_eq_to_obj_eq[OF evals_def, symmetric, unfolded fun_eq_iff])
-apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva x (evals enva t2a), t)")
+apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenv x (evals enva t2a), t)")
 apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (enva, t2a)")
 apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva xa (evals enva t2a), ta)")
-apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva x (evals enva t2a), t))")
+apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenv x (evals enva t2a), t))")
 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (enva, t2a))")
 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa (evals enva t2a), ta))")
 apply(erule conjE)+
 defer
 apply (simp_all add: eqvt_at_def evals_def)[3]
 apply(simp)
-defer
-apply(erule_tac c="(cenv, env)" in  Abs_lst1_fcb2')
-apply(rule fresh_eqvt_at)
-back
-apply(simp add: eqvt_at_def)
 sorry
 
 (* can probably not proved by a trivial size argument *)
 termination sorry
 
+lemma [eqvt]:
+  shows "(p \<bullet> evals env t) = evals (p \<bullet> env) (p \<bullet> t)"
+  and "(p \<bullet> evals_aux v t env) = evals_aux (p \<bullet> v) (p \<bullet> t) (p \<bullet> env)"
+sorry
+
+(* fixme: should be a provided lemma *)
+lemma fv_bn_finite:
+  shows "finite (fv_bn env)"
+apply(induct env rule: sem_neu_env.inducts(3))
+apply(auto simp add: sem_neu_env.supp finite_supp)
+done
+
+lemma test:
+  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)
+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)
+apply(subst sem_neu_env.supp)
+apply(simp add: sem_neu_env.supp lam.supp)
+apply(auto)[1]
+apply(simp)
+apply(metis)
+sorry
+
 nominal_primrec
   reify :: "sem \<Rightarrow> lam" and
   reifyn :: "neu \<Rightarrow> lam"
 where
-  "reify (L env y t) = (fresh_fun (\<lambda>x::name. Lam [x]. (reify (evals (ECons env y (N (V x))) t))))"
+  "atom x \<sharp> (env, y, t) \<Longrightarrow> reify (L env y t) = Lam [x]. (reify (evals (ECons env y (N (V x))) t))"
 | "reify (N n) = reifyn n"
 | "reifyn (V x) = Var x"
 | "reifyn (A n d) = App (reifyn n) (reify d)"
-defer
-defer
+apply(subgoal_tac "\<And>p x y. reify_reifyn_graph x y \<Longrightarrow> reify_reifyn_graph (p \<bullet> x) (p \<bullet> y)")
+apply(simp add: eqvt_def)
+apply(simp add: permute_fun_def)
+apply(rule allI)
+apply(rule ext)
+apply(rule ext)
+apply(rule iffI)
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="- p \<bullet> x" in meta_spec)
+apply(drule_tac x="- p \<bullet> xa" in meta_spec)
+apply(simp add: permute_bool_def)
+apply(simp add: permute_bool_def)
+apply(erule reify_reifyn_graph.induct)
+apply(perm_simp)
+apply(rule reify_reifyn_graph.intros)
+apply(rule_tac p="-p" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel)
+apply(simp)
+apply(simp)
+apply(perm_simp)
+apply(rule reify_reifyn_graph.intros)
+apply(simp)
+apply(perm_simp)
+apply(rule reify_reifyn_graph.intros)
+apply(perm_simp)
+apply(rule reify_reifyn_graph.intros)
+apply(simp)
+apply(simp)
+apply(rule TrueI)
 --"completeness"
 apply(case_tac x)
 apply(simp)
 apply(case_tac a rule: sem_neu_env.exhaust(1))
-apply(metis)+
+apply(subgoal_tac "\<exists>x::name. atom x \<sharp> (env, name, lam)")
+apply(metis)
+apply(rule obtain_fresh)
+apply(blast)
+apply(blast)
 apply(case_tac b rule: sem_neu_env.exhaust(2))
 apply(simp)
 apply(simp)
@@ -101,6 +194,87 @@
 defer
 apply(simp)
 apply(simp)
+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 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 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)")
+prefer 2
+apply(rule obtain_fresh)
+apply(blast)
+apply(erule exE)
+apply(rule 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)
+apply(auto)[1]
+apply(rule fresh_eqvt_at)
+back
+apply(assumption)
+apply(simp add: finite_supp)
+apply(rule_tac S="supp (enva, 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)
+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)
+apply(auto)[1]
+apply(rule fresh_eqvt_at)
+back
+apply(assumption)
+apply(simp add: finite_supp)
+apply(rule_tac S="supp (enva, ya, xa, ta)" 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(simp (no_asm) add: Abs1_eq_iff)
+apply(rule sym)
+apply(erule_tac Abs_lst1_fcb2')
+apply(rule fresh_eqvt_at)
+back
+apply(drule_tac q="(c \<leftrightarrow> x)" in eqvt_at_perm)
+apply(perm_simp)
+apply(simp add: flip_fresh_fresh)
+apply(simp add: finite_supp)
+apply(rule supports_fresh)
+apply(rule_tac S="supp (enva, ya, xa, ta)" 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(rule fresh_eqvt_at)
+back
+apply(drule_tac q="(c \<leftrightarrow> x)" in eqvt_at_perm)
+apply(perm_simp)
+apply(simp add: flip_fresh_fresh)
+apply(assumption)
+apply(simp add: finite_supp)
 sorry
 
 termination sorry

--- a/Nominal/Nominal2_Base.thy	Wed Jul 06 01:04:09 2011 +0200
+++ b/Nominal/Nominal2_Base.thy	Wed Jul 06 15:59:11 2011 +0200
@@ -1238,6 +1238,18 @@
   then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)
 qed
 
+lemma supports_fresh:
+  fixes x :: "'a::pt"
+  assumes a1: "S supports x"
+  and     a2: "finite S"
+  and     a3: "a \<notin> S"
+  shows "a \<sharp> x"
+unfolding fresh_def
+proof -
+  have "(supp x) \<subseteq> S" using a1 a2 by (rule supp_is_subset)
+  then show "a \<notin> (supp x)" using a3 by auto
+qed
+
 lemma supp_is_least_supports:
   fixes S :: "atom set"
   and   x :: "'a::pt"
@@ -1252,6 +1264,7 @@
   with fin a3 show "S \<subseteq> supp x" by blast
 qed
 
+
 lemma subsetCI: 
   shows "(\<And>x. x \<in> A \<Longrightarrow> x \<notin> B \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> B"
   by auto
@@ -1642,6 +1655,21 @@
 unfolding eqvt_def
 by simp
 
+lemma eqvt_at_perm:
+  assumes "eqvt_at f x"
+  shows "eqvt_at f (q \<bullet> x)"
+proof -
+  { fix p::"perm"
+    have "p \<bullet> (f (q \<bullet> x)) = p \<bullet> q \<bullet> (f x)"
+      using assms by (simp add: eqvt_at_def)
+    also have "\<dots> = (p + q) \<bullet> (f x)" by simp
+    also have "\<dots> = f ((p + q) \<bullet> x)"
+      using assms by (simp add: eqvt_at_def)
+    finally have "p \<bullet> (f (q \<bullet> x)) = f (p \<bullet> q \<bullet> x)" by simp } 
+  then show "eqvt_at f (q \<bullet> x)" unfolding eqvt_at_def
+    by simp
+qed
+
 lemma supp_fun_eqvt:
   assumes a: "eqvt f"
   shows "supp f = {}"