--- a/Nominal/Ex/NBE.thy	Sat Jul 16 21:36:43 2011 +0100
+++ b/Nominal/Ex/NBE.thy	Sun Jul 17 04:04:17 2011 +0100
@@ -11,7 +11,6 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
-
 nominal_datatype sem =
   L e::"env" x::"name" l::"lam" binds x "bn e" in l
 | N "neu"
@@ -25,7 +24,69 @@
   bn
 where
   "bn ENil = []"
-| "bn (ECons env x v) = (atom x) # (bn env)" 
+| "bn (ECons env x v) = (atom x) # (bn env)"
+
+thm sem_neu_env.supp
+
+lemma [simp]:
+  shows "finite (fv_bn env)"
+apply(induct env rule: sem_neu_env.inducts(3))
+apply(rule TrueI)+
+apply(auto simp add: sem_neu_env.supp finite_supp)
+done
+
+lemma test1:
+  shows "supp p \<sharp>* (fv_bn env) \<Longrightarrow> (p \<bullet> env) = permute_bn p env"
+apply(induct env rule: sem_neu_env.inducts(3))
+apply(rule TrueI)+
+apply(auto simp add: sem_neu_env.perm_bn_simps sem_neu_env.supp)
+apply(drule meta_mp)
+apply(drule fresh_star_supp_conv)
+apply(subst (asm) supp_finite_atom_set)
+apply(simp add: finite_supp)
+apply(simp add: fresh_star_Un)
+apply(rule fresh_star_supp_conv)
+apply(subst supp_finite_atom_set)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(rule perm_supp_eq)
+apply(drule fresh_star_supp_conv)
+apply(subst (asm) supp_finite_atom_set)
+apply(simp add: finite_supp)
+apply(simp add: fresh_star_Un)
+apply(rule fresh_star_supp_conv)
+apply(simp)
+done
+
+thm alpha_sem_raw_alpha_neu_raw_alpha_env_raw_alpha_bn_raw.inducts(4)[no_vars]
+
+lemma alpha_bn_inducts_raw[consumes 1]:
+  "\<lbrakk>alpha_bn_raw x7 x8;
+  P4 ENil_raw ENil_raw;
+ \<And>env_raw env_rawa sem_raw sem_rawa name namea.
+    \<lbrakk>alpha_bn_raw env_raw env_rawa; P4 env_raw env_rawa; alpha_sem_raw sem_raw sem_rawa\<rbrakk>
+    \<Longrightarrow> P4 (ECons_raw env_raw name sem_raw) (ECons_raw env_rawa namea sem_rawa)\<rbrakk>
+\<Longrightarrow> P4 x7 x8"
+apply(induct rule: alpha_sem_raw_alpha_neu_raw_alpha_env_raw_alpha_bn_raw.inducts(4))
+apply(rule TrueI)+
+apply(auto)
+done
+
+lemmas alpha_bn_inducts[consumes 1] = alpha_bn_inducts_raw[quot_lifted]
+
+lemma test2:
+  shows "alpha_bn env1 env2 \<Longrightarrow> p \<bullet> (bn env1) = q \<bullet> (bn env2) \<Longrightarrow> permute_bn p env1 = permute_bn q env2"
+apply(induct rule: alpha_bn_inducts)
+apply(auto simp add: sem_neu_env.perm_bn_simps sem_neu_env.bn_defs)
+apply(simp add: atom_eqvt)
+done
+
+lemma fresh_star_Union:
+  assumes "as \<subseteq> bs" "bs \<sharp>* x"
+  shows "as \<sharp>* x"
+using assms by (auto simp add: fresh_star_def)
+  
 
 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")
@@ -36,7 +97,7 @@
 | "evals (ECons tail y v) (Var x) = (if x = y then v else evals tail (Var x))" 
 | "atom x \<sharp> env \<Longrightarrow> evals env (Lam [x]. t) = L env x t"
 | "evals env (App t1 t2) = evals_aux (evals env t1) (evals env t2)"
-| "evals_aux (L cenv x t) t' = evals (ECons cenv x t') t"
+| "set (atom x # bn env) \<sharp>* (fv_bn env, t') \<Longrightarrow> evals_aux (L env x t) t' = evals (ECons env x t') t"
 | "evals_aux (N n) t' = N (A n t')"
 apply(simp add: eqvt_def  evals_evals_aux_graph_def)
 apply(perm_simp)
@@ -77,7 +138,24 @@
 apply(simp)
 apply(case_tac b)
 apply(simp)
-apply(case_tac a rule: sem_neu_env.exhaust(1))
+apply(rule_tac y="a" and c="(a, ba)" in sem_neu_env.strong_exhaust(1))
+apply(simp)
+apply(rotate_tac 4)
+apply(drule_tac x="name" in meta_spec)
+apply(drule_tac x="env" in meta_spec)
+apply(drule_tac x="ba" in meta_spec)
+apply(drule_tac x="lam" in meta_spec)
+apply(simp add:  sem_neu_env.alpha_refl)
+apply(rotate_tac 9)
+apply(drule_tac meta_mp)
+apply(simp (no_asm_use) add: fresh_star_def sem_neu_env.fresh fresh_Pair)
+apply(simp)
+apply(subst fresh_finite_atom_set)
+defer
+apply(simp)
+apply(subst fresh_finite_atom_set)
+defer
+apply(simp)
 apply(metis)+
 --"compatibility"
 apply(all_trivials)
@@ -87,13 +165,15 @@
 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 cenv x t'a, t)")
-apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva xa t'a, ta)")
-apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenv x t'a, t))")
-apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa t'a, ta))")
+apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons env x t'a, t)")
+apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons enva xa t'a, ta)")
+apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons env x t'a, t))")
+apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons enva xa t'a, ta))")
 apply(erule conjE)+
 defer
 apply (simp_all add: eqvt_at_def evals_def)[3]
+defer
+defer
 apply(simp add: sem_neu_env.alpha_refl)
 apply(erule conjE)+
 apply(erule_tac c="(env, enva)" in Abs_lst1_fcb2)
@@ -106,63 +186,127 @@
 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(drule_tac x="set (atom x # bn env)" in meta_spec)
+apply(drule_tac x="(fv_bn env, fv_bn enva, env, enva, x, xa, t, ta, t'a)" in meta_spec)
+apply(drule_tac x="[atom x # bn env]lst. t" in meta_spec)
 apply(simp (no_asm_use) add: finite_supp Abs_fresh_star_iff)
 apply(drule meta_mp)
+apply(simp add: supp_Pair finite_supp supp_finite_atom_set)
+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(rule trans)
+apply(rule sym)
+apply(rule_tac p="p" in perm_supp_eq)
+apply(simp)
+apply(perm_simp)
+apply(simp add: fresh_star_Un fresh_star_insert)
+apply(rule conjI)
+apply(simp (no_asm_use) add: fresh_star_def fresh_Pair)
+apply(simp add: fresh_def)
+apply(simp add: supp_finite_atom_set)
+apply(blast)
+apply(rule conjI)
+apply(simp (no_asm_use) add: fresh_star_def fresh_Pair)
+apply(simp add: fresh_def)
+apply(simp add: supp_finite_atom_set)
 apply(blast)
-apply(erule exE)
+apply(rule conjI)
+apply(simp (no_asm_use) add: fresh_star_def fresh_Pair)
+apply(simp add: fresh_def)
+apply(simp add: supp_finite_atom_set)
+apply(blast)
+apply(simp (no_asm_use) add: fresh_star_def fresh_Pair)
+apply(simp add: fresh_def)
+apply(simp add: supp_finite_atom_set)
+apply(blast)
+apply(simp add: eqvt_at_def perm_supp_eq)
+apply(subst (3) perm_supp_eq)
+apply(simp)
+apply(simp add: fresh_star_def fresh_Pair)
+apply(auto)[1]
+apply(rotate_tac 6)
+apply(drule sym)
+apply(simp)
+apply(rotate_tac 11)
 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(rule_tac p="p" in supp_perm_eq)
+apply(assumption)
+apply(rotate_tac 11)
+apply(rule sym)
+apply(simp add: atom_eqvt)
+apply(simp (no_asm_use) add: Abs_eq_iff2 alphas)
+apply(erule conjE | erule exE)+
+apply(rule trans)
+apply(rule sym)
+apply(rule_tac p="pa" in perm_supp_eq)
+apply(erule fresh_star_Union)
+apply(simp (no_asm_use) add: fresh_star_insert fresh_star_Un)
+apply(rule conjI)
 apply(perm_simp)
+apply(simp add: fresh_star_insert fresh_star_Un)
+apply(simp add: fresh_Pair)
+apply(simp add: fresh_def)
+apply(simp add: supp_finite_atom_set)
+apply(blast)
+apply(rule conjI)
+apply(perm_simp)
+apply(simp add: fresh_star_insert fresh_star_Un)
+apply(simp add: fresh_Pair)
+apply(simp add: fresh_def)
+apply(simp add: supp_finite_atom_set)
+apply(blast)
+apply(rule conjI)
+apply(perm_simp)
+defer
+apply(perm_simp)
+apply(simp add: fresh_star_insert fresh_star_Un)
+apply(simp add: fresh_star_Pair)
+apply(simp add: fresh_star_def fresh_def)
+apply(simp add: supp_finite_atom_set)
+apply(blast)
 apply(simp)
-apply(rotate_tac 4)
-apply(drule sym)
-apply(rotate_tac 5)
-apply(drule trans)
+apply(perm_simp)
+apply(subst (3) perm_supp_eq)
+apply(erule fresh_star_Union)
+apply(simp add: fresh_star_insert fresh_star_Un)
+apply(simp add: fresh_star_def fresh_Pair)
+apply(subgoal_tac "pa \<bullet> enva = p \<bullet> env")
+apply(simp)
+defer
+apply(simp (no_asm_use) add: fresh_star_insert fresh_star_Un)
+apply(simp (no_asm_use) add: fresh_star_def)
+apply(rule ballI)
+apply(subgoal_tac "a \<notin> supp ta - insert (atom xa) (set (bn enva)) \<union> (fv_bn enva \<union> supp t'a)")
+apply(simp only: fresh_def)
+apply(blast)
+apply(simp (no_asm_use))
+apply(rule conjI)
+apply(blast)
+apply(simp add: fresh_Pair)
+apply(simp add: fresh_star_def fresh_def)
+apply(simp add: supp_finite_atom_set)
+apply(subst test1)
+apply(erule fresh_star_Union)
+apply(simp add: fresh_star_insert fresh_star_Un)
+apply(simp add: fresh_star_def fresh_Pair)
+apply(subst test1)
+apply(simp)
+apply(simp add: fresh_star_insert fresh_star_Un)
+apply(simp add: fresh_star_def fresh_Pair)
 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(erule test2)
 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)
+done
+
+
 
-sorry
 
-(* can probably not proved by a trivial size argument *)
-termination apply(lexicographic_order)
-
+text {* can probably not proved by a trivial size argument *}
+termination (* apply(lexicographic_order) *)
 sorry
 
 lemma [eqvt]:
@@ -313,6 +457,7 @@
 apply(perm_simp)
 apply(simp add: flip_fresh_fresh)
 apply(simp (no_asm) add: Abs1_eq_iff)
+(* HERE *)
 thm at_set_avoiding3
 using at_set_avoiding3
 apply -