--- a/Nominal/Ex/Lambda.thy	Tue Jan 18 18:04:40 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue Jan 18 19:27:30 2011 +0100
@@ -95,13 +95,70 @@
   apply(simp_all add: lam.size)
   done
 
-(* a small lemma *)
+text {* a small lemma *}
 lemma
   "supp t = set (frees_lst t)"
 apply(induct t rule: lam.induct)
 apply(simp_all add: lam.supp supp_at_base)
 done
 
+nominal_primrec
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
+where
+  "(Var x)[y ::= s] = (if x=y then s else (Var x))"
+| "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])"
+| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
+apply(case_tac x)
+apply(simp)
+apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
+apply(simp add: lam.eq_iff lam.distinct)
+apply(auto)[1]
+apply(simp add: lam.eq_iff lam.distinct)
+apply(auto)[1]
+apply(simp add: fresh_star_def lam.eq_iff lam.distinct)
+apply(simp_all add: lam.distinct)[5]
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(erule conjE)+
+apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta")
+prefer 2
+apply(rule conjI)
+apply(simp add: Abs_fresh_iff)
+apply(drule sym)
+apply(simp add: Abs_fresh_iff)
+apply(subst (asm) Abs_eq_iff2)
+apply(auto)
+apply(simp add: alphas)
+apply(simp add: atom_eqvt)
+apply(clarify)
+apply(rule trans)
+apply(rule_tac p="p" in supp_perm_eq[symmetric])
+apply(rule fresh_star_supp_conv)
+apply(drule fresh_star_perm_set_conv)
+apply(simp add: finite_supp)
+apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* ([[atom x]]lst. subst_sumC (t, ya, sa))")
+apply(auto simp add: fresh_star_def)[1]
+apply(simp (no_asm) add: fresh_star_def)
+apply(rule conjI)
+apply(simp (no_asm) add: Abs_fresh_iff)
+apply(clarify)
+apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at)
+apply(simp add: finite_supp)
+apply(simp (no_asm_use) add: fresh_Pair)
+apply(simp add: Abs_fresh_iff)
+apply(simp)
+apply(simp add: Abs_fresh_iff)
+apply(subgoal_tac "p \<bullet> ya = ya")
+apply(subgoal_tac "p \<bullet> sa = sa")
+unfolding eqvt_at_def
+apply(simp add: atom_eqvt fresh_Pair)
+apply(rule perm_supp_eq)
+apply(auto simp add: fresh_star_def fresh_Pair)[1]
+apply(rule perm_supp_eq)
+apply(auto simp add: fresh_star_def fresh_Pair)[1]
+done
+
 nominal_datatype ln = 
   LNBnd nat
 | LNVar name
@@ -137,23 +194,36 @@
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)
-apply(simp add: Abs_eq_iff)
 apply(erule conjE)
-apply(erule exE)
+apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta")
+prefer 2
+apply(rule conjI)
+apply(simp add: Abs_fresh_iff)
+apply(drule sym)
+apply(simp add: Abs_fresh_iff)
+apply(subst (asm) Abs_eq_iff2)
+apply(auto)
 apply(simp add: alphas)
 apply(simp add: atom_eqvt)
 apply(clarify)
 apply(rule trans)
 apply(rule_tac p="p" in supp_perm_eq[symmetric])
-apply(simp (no_asm) add: ln.supp)
-apply(drule supp_eqvt_at)
+apply(rule fresh_star_supp_conv)
+apply(drule fresh_star_perm_set_conv)
 apply(simp add: finite_supp)
+apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* LNLam (trans_sumC (t, x # xsa))")
+apply(auto simp add: fresh_star_def)[1]
+apply(simp (no_asm) add: fresh_star_def ln.fresh)
+apply(rule conjI)
+apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at)
+apply(simp add: finite_supp)
+apply(simp (no_asm_use) add: fresh_Pair)
+apply(simp add: Abs_fresh_iff fresh_Cons)[1]
+apply(erule disjE)
+apply(erule disjE)
+apply(simp)
 oops
 
-
-
-
-
 nominal_datatype db = 
   DBVar nat
 | DBApp db db
@@ -248,26 +318,7 @@
 | "trans (Lam x t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"
 *)
 
-nominal_primrec
-  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
-where
-  "(Var x)[y ::= s] = (if x=y then s else (Var x))"
-| "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])"
-| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
-apply(case_tac x)
-apply(simp)
-apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
-apply(simp add: lam.eq_iff lam.distinct)
-apply(auto)[1]
-apply(simp add: lam.eq_iff lam.distinct)
-apply(auto)[1]
-apply(simp add: fresh_star_def lam.eq_iff lam.distinct)
-apply(simp_all add: lam.distinct)[5]
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(erule conjE)+
-oops
+
 
 
 end

--- a/Nominal/Nominal2_Base.thy	Tue Jan 18 18:04:40 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Jan 18 19:27:30 2011 +0100
@@ -1601,6 +1601,16 @@
   shows "supp x \<sharp>* y \<Longrightarrow> supp y \<sharp>* x"
 by (auto simp add: fresh_star_def fresh_def)
 
+lemma fresh_star_perm_set_conv:
+  fixes p::"perm"
+  assumes fresh: "as \<sharp>* p"
+  and     fin: "finite as"
+  shows "supp p \<sharp>* as"
+apply(rule fresh_star_supp_conv)
+apply(simp add: supp_finite_atom_set fin fresh)
+done
+
+
 lemma fresh_star_Pair:
   shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" 
   by (auto simp add: fresh_star_def fresh_Pair)