--- a/Nominal/Ex/Lambda.thy	Thu Feb 03 02:51:57 2011 +0000
+++ b/Nominal/Ex/Lambda.thy	Thu Feb 03 02:57:04 2011 +0000
@@ -140,7 +140,7 @@
 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
 apply(blast)+
 apply(simp add: fresh_star_def)
-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")
 apply(subst (asm) Abs_eq_iff2)
 apply(simp add: alphas atom_eqvt)
 apply(clarify)
@@ -168,9 +168,6 @@
 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]
-apply(rule conjI)
-apply(simp add: Abs_fresh_iff)
-apply(drule sym)
 apply(simp add: Abs_fresh_iff)
 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") 
 unfolding eqvt_def

--- a/Nominal/Ex/TypeSchemes.thy	Thu Feb 03 02:51:57 2011 +0000
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Feb 03 02:57:04 2011 +0000
@@ -15,7 +15,6 @@
 apply(subst permute_fun_def)
 sorry
 
-
 nominal_primrec
     even :: "nat \<Rightarrow> A"
 and odd  :: "nat \<Rightarrow> B"
@@ -258,8 +257,11 @@
 --"This is exactly the assumption for the properly defined function"
 defer
 apply (simp add: ty_tys.eq_iff)
+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 (simp add: alpha_res.simps)
+apply (clarify)
+apply (simp add: alphas)
 apply (clarify)
 apply (rule trans)
 apply(rule_tac p="p" in supp_perm_eq[symmetric])
@@ -268,22 +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]res. 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 (simp (no_asm) add: fresh_star_def)
+
 apply rule
 apply(simp (no_asm) only: Abs_fresh_iff)
 apply(clarify)
-apply blast
-defer
+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(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
---"Would work for 'set' and 'list' bindings, not sure how to do 'set+'."
+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
 
 

--- a/Nominal/Nominal2_Abs.thy	Thu Feb 03 02:51:57 2011 +0000
+++ b/Nominal/Nominal2_Abs.thy	Thu Feb 03 02:57:04 2011 +0000
@@ -285,7 +285,7 @@
   then have "(supp x' - as') \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using a by (simp add: alphas)
   ultimately show "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'"
     by (auto dest: disjoint_right_eq)
-qed 
+qed
 
 lemma alpha_abs_res_stronger1_aux:
   assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')"
@@ -320,6 +320,31 @@
   show "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" by blast
 qed
 
+lemma alpha_abs_res_minimal:
+  assumes asm: "(as, x) \<approx>res (op =) supp p (as', x')"
+  shows "(as \<inter> supp x, x) \<approx>res (op =) supp p (as' \<inter> supp x', x')"
+  using asm unfolding alpha_res by (auto simp add: Diff_Int)
+
+lemma alpha_abs_res_abs_set:
+  assumes asm: "(as, x) \<approx>res (op =) supp p (as', x')"
+  shows "(as \<inter> supp x, x) \<approx>set (op =) supp p (as' \<inter> supp x', x')"
+proof -
+  have c: "p \<bullet> x = x'"
+    using alpha_abs_res_minimal[OF asm] unfolding alpha_res by clarify
+  then have a: "supp x - as \<inter> supp x = supp (p \<bullet> x) - as' \<inter> supp (p \<bullet> x)"
+    using alpha_abs_res_minimal[OF asm] by (simp add: alpha_res)
+  have b: "(supp x - as \<inter> supp x) \<sharp>* p"
+    using alpha_abs_res_minimal[OF asm] unfolding alpha_res by clarify
+  have "p \<bullet> (as \<inter> supp x) = as' \<inter> supp (p \<bullet> x)"
+    by (metis Int_commute asm c supp_property_res)
+  then show ?thesis using a b c unfolding alpha_set by simp
+qed
+
+lemma alpha_abs_set_abs_res:
+  assumes asm: "(as \<inter> supp x, x) \<approx>set (op =) supp p (as' \<inter> supp x', x')"
+  shows "(as, x) \<approx>res (op =) supp p (as', x')"
+  using asm unfolding alphas by (auto simp add: Diff_Int)
+
 lemma alpha_abs_res_stronger1:
   assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')"
   shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'"
@@ -483,6 +508,25 @@
     (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y) \<and> supp p \<subseteq> set bsl \<union> set csl)"
   by (lifting alphas_abs_stronger)
 
+lemma Abs_eq_res_set:
+  "(([bs]res. x) = ([cs]res. y)) = (([(bs \<inter> supp x)]set. x) = ([(cs \<inter> supp y)]set. y))"
+  unfolding Abs_eq_iff
+  using alpha_abs_set_abs_res alpha_abs_res_abs_set
+  apply auto
+  apply (rule_tac x="p" in exI)
+  apply assumption
+  apply (rule_tac x="p" in exI)
+  apply assumption
+  done
+
+lemma Abs_eq_res_supp:
+  assumes asm: "supp x \<subseteq> bs"
+  shows "([as]res. x) = ([as \<inter> bs]res. x)"
+  unfolding Abs_eq_iff alphas
+  apply (rule_tac x="0::perm" in exI)
+  apply (simp add: fresh_star_zero)
+  using asm by blast
+
 lemma Abs_exhausts:
   shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1"
   and   "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2"