--- a/Nominal/Ex/TypeSchemes.thy	Tue Feb 01 08:48:14 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Tue Feb 01 08:57:50 2011 +0900
@@ -15,7 +15,6 @@
 apply(subst permute_fun_def)
 sorry
 
-
 nominal_primrec
     even :: "nat \<Rightarrow> A"
 and odd  :: "nat \<Rightarrow> B"
@@ -48,7 +47,7 @@
   Var "name"
 | Fun "ty" "ty"
 and tys =
-  All xs::"name fset" ty::"ty" bind (set) xs in ty
+  All xs::"name fset" ty::"ty" bind (set+) xs in ty
 
 thm ty_tys.distinct
 thm ty_tys.induct
@@ -258,8 +257,10 @@
 --"This is exactly the assumption for the properly defined function"
 defer
 apply (simp add: ty_tys.eq_iff)
-apply (subgoal_tac "(atom ` fset xsa - atom ` fset xs) \<sharp>* ([atom ` fset xs]set. T)")
+apply (simp only: Abs_eq_res_set)
+apply (subgoal_tac "(atom ` fset xsa \<inter> supp T - atom ` fset xs \<inter> supp Ta) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)")
 apply (subst (asm) Abs_eq_iff2)
+apply (clarify)
 apply (simp add: alphas)
 apply (clarify)
 apply (rule trans)
@@ -269,32 +270,48 @@
 apply(drule fresh_star_perm_set_conv)
 apply (rule finite_Diff)
 apply (rule finite_supp)
-apply (subgoal_tac "(atom ` fset xs \<union> atom ` fset xsa) \<sharp>* ([atom ` fset xs]set. subst \<theta>' T)")
+apply (subgoal_tac "(atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. subst \<theta>' T)")
 apply (metis Un_absorb2 fresh_star_Un)
 apply (simp add: fresh_star_Un)
 apply (rule conjI)
-apply (simp add: fresh_star_def)
-apply rule
-apply(simp (no_asm) only: Abs_fresh_iff)
-apply(clarify)
-apply simp
-apply (simp add: fresh_star_def)
+apply (simp (no_asm) add: fresh_star_def)
+
 apply rule
 apply(simp (no_asm) only: Abs_fresh_iff)
 apply(clarify)
-apply(drule_tac a="atom a" in fresh_eqvt_at)
+apply auto[1]
+apply (simp add: fresh_star_def fresh_def)
+--"HERE"
+apply (simp (no_asm) add: fresh_star_def)
+apply rule
+apply auto[1]
+apply(simp (no_asm) only: Abs_fresh_iff)
+apply(clarify)
+apply auto[1]
+prefer 2
+apply (simp add: fresh_def)
+apply(drule_tac a="atom x" in fresh_eqvt_at)
 apply (simp add: supp_Pair finite_supp)
 apply (simp add: fresh_Pair)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: Abs_fresh_iff)
+apply(auto simp add: Abs_fresh_iff fresh_star_def)[1]
+prefer 2
+apply auto[1]
+apply (erule_tac x="atom x" in ballE)
+apply auto[1]
+apply (auto simp add: fresh_def)[1]
+
 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
 prefer 2
 apply (rule perm_supp_eq)
-apply (metis Un_absorb2 fresh_star_Un)
-apply (simp add: eqvt_at_def)
-apply (simp add: fresh_star_def)
-apply rule
-apply(simp add: Abs_fresh_iff)
+apply (subgoal_tac "(atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* \<theta>'")
+apply (auto simp add: fresh_star_def)[1]
+apply (simp add: fresh_star_Un fresh_star_def)
+apply blast
+apply(simp add: eqvt_at_def inter_eqvt supp_eqvt)
+apply (simp only: Abs_eq_res_set[symmetric])
+
+apply (rule_tac s="[p \<bullet> atom ` fset xs \<inter> supp (\<theta>', p \<bullet> T)]res. subst \<theta>' (p \<bullet> T)" in trans)
+--"What if (p \<bullet> xs) is not fresh for \<theta>' ?"
 oops