--- a/Nominal/Ex/Lambda.thy	Sat Feb 19 09:31:22 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Wed Feb 23 11:11:02 2011 +0900
@@ -320,9 +320,9 @@
 
 lemma [eqvt]:
   shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
-apply(induct xs arbitrary: n)
-apply(simp_all add: permute_pure)
-done
+  apply(induct xs arbitrary: n)
+  apply(simp_all add: permute_pure)
+  done
 
 nominal_primrec
   trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
@@ -334,20 +334,16 @@
 apply(case_tac x)
 apply(simp)
 apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
-apply(simp_all)[3]
+apply(simp_all add: fresh_star_def)[3]
 apply(blast)
 apply(blast)
-apply(simp add: fresh_star_def)
 apply(simp_all add: lam.distinct)
 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")
+apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t")
 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)
@@ -356,22 +352,92 @@
 apply(clarify)
 apply(rule trans)
 apply(rule_tac p="p" in supp_perm_eq[symmetric])
+prefer 2
+apply (subgoal_tac "p \<bullet> xsa = xsa")
+apply (simp add: eqvt_at_def)
+apply (rule supp_perm_eq)
+apply (rule fresh_star_supp_conv)
+apply (subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* xsa")
+apply (simp add: fresh_star_def fresh_def)
+apply blast
+apply (simp add: fresh_star_def fresh_def)
+apply (simp add:  ln.supp)
 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 (subst (asm) supp_perm_pair)
+apply (elim disjE)
+apply (simp add: fresh_star_def supp_zero_perm)
+apply (simp add: flip_def[symmetric])
+apply(subgoal_tac "supp (x \<leftrightarrow> p \<bullet> x) \<sharp>* trans_sumC (t, x # xsa)")
+apply simp
+apply (subst flip_def)
+apply (simp add: supp_swap)
+apply (simp add: fresh_star_def)
+apply (rule)
+apply rule
+prefer 2
 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)
+apply (metis Rep_name_inverse atom_name_def fresh_at_base)
+apply assumption
 oops
 
+(* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)"
+  apply (case_tac "x = xa")
+  apply simp
+  apply (simp add: lam.eq_iff Abs1_eq_iff flip_def[symmetric])
+  by (metis atom_eqvt flip_at_simps(2) fresh_permute_iff)
+
+lemma supp_lookup: "supp (lookup l n name) = {atom name} - supp l"
+  apply (induct l arbitrary: n)
+  apply (simp_all add: ln.supp supp_at_base supp_Nil supp_Cons pure_supp)
+  done
+
+lemma trans_eqvt[eqvt]: "p \<bullet> (trans t l) = trans (p \<bullet> t) (p \<bullet> l)"
+  apply (induct t l rule: trans.induct)
+  apply simp_all
+  apply (simp add: eqvts permute_pure)
+  done
+
+lemma diff_un: "a - (b \<union> c) = a - b - c"
+  by blast
+
+lemma supp_trans: "supp (trans t l) = supp t - supp l"
+  apply (induct t arbitrary: l rule: lam.induct)
+  apply (simp_all add: lam.supp supp_at_base supp_lookup ln.supp)
+  apply blast
+  apply (rule_tac x="(lam, l)" and ?'a="name" in obtain_fresh)
+  apply (simp add: fresh_Pair)
+  apply clarify
+  apply (subgoal_tac "supp (Lambda.trans (Lam [a]. ((name \<leftrightarrow> a) \<bullet> lam)) l) =
+    supp lam - {atom name} - supp l")
+  using helpr
+  apply simp
+  apply (simp add: ln.supp)
+  apply (subgoal_tac "supp ((name \<leftrightarrow> a) \<bullet> (Lambda.trans lam ((name \<leftrightarrow> a) \<bullet> (a # l)))) = supp lam - {atom name} - supp l")
+  apply (simp add: trans_eqvt)
+  apply (simp add: supp_eqvt[symmetric])
+  apply (simp add: Diff_eqvt)
+  apply (simp add: supp_eqvt supp_Cons  union_eqvt)
+  apply (simp add: diff_un)
+  apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*})
+  apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*})
+  apply rule
+  prefer 2
+  apply rule
+  apply (simp add: supp_at_base)
+  apply (subgoal_tac "(name \<leftrightarrow> a) \<bullet> (supp lam - {atom name}) = supp lam - {atom name}")
+  apply (simp add: eqvts)
+  unfolding flip_def
+  apply (rule swap_fresh_fresh)
+apply (metis fresh_at_base fresh_def fresh_minus_atom_set lam.fsupp supp_at_base)
+by (metis fresh_def fresh_finite_atom_set fresh_minus_atom_set lam.fsupp)
+
+lemma "atom x \<sharp> trans_sumC (t, x # xsa)"
+  by (simp add: fresh_def meta_eq_to_obj_eq[OF trans_def, symmetric, unfolded fun_eq_iff] supp_trans supp_Cons supp_at_base)
+*)
+
 nominal_datatype db = 
   DBVar nat
 | DBApp db db