# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295014945 0
# Node ID 619ecb57db389193ed52bf5875d31dc68ab394fe
# Parent  b4472ebd7fadab0123d48d411c938bc48a04c585
strengthened renaming lemmas

diff -r b4472ebd7fad -r 619ecb57db38 Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Thu Jan 13 12:12:47 2011 +0000
+++ b/Nominal/Nominal2_Abs.thy	Fri Jan 14 14:22:25 2011 +0000
@@ -545,17 +545,15 @@
 
 lemma Abs_rename_set:
   fixes x::"'a::fs"
-  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
+  assumes a: "(p \<bullet> bs) \<sharp>* x" 
   and     b: "finite bs"
   shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 proof -
-  from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair)   
-  with set_renaming_perm 
-  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
+  from b set_renaming_perm 
+  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
   have "[bs]set. x =  q \<bullet> ([bs]set. x)"
     apply(rule perm_supp_eq[symmetric])
     using a **
-    unfolding fresh_star_Pair
     unfolding Abs_fresh_star_iff
     unfolding fresh_star_def
     by auto
@@ -566,17 +564,15 @@
 
 lemma Abs_rename_res:
   fixes x::"'a::fs"
-  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
+  assumes a: "(p \<bullet> bs) \<sharp>* x" 
   and     b: "finite bs"
   shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 proof -
-  from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair) 
-  with set_renaming_perm 
-  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
+  from b set_renaming_perm 
+  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
   have "[bs]res. x =  q \<bullet> ([bs]res. x)"
     apply(rule perm_supp_eq[symmetric])
     using a **
-    unfolding fresh_star_Pair
     unfolding Abs_fresh_star_iff
     unfolding fresh_star_def
     by auto
@@ -587,17 +583,14 @@
 
 lemma Abs_rename_lst:
   fixes x::"'a::fs"
-  assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" 
+  assumes a: "(p \<bullet> (set bs)) \<sharp>* x" 
   shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 proof -
-  from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter 
-    by (simp add: fresh_star_Pair fresh_star_set)
-  with list_renaming_perm 
-  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis 
+  from a list_renaming_perm 
+  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by blast
   have "[bs]lst. x =  q \<bullet> ([bs]lst. x)"
     apply(rule perm_supp_eq[symmetric])
     using a **
-    unfolding fresh_star_Pair
     unfolding Abs_fresh_star_iff
     unfolding fresh_star_def
     by auto
@@ -611,21 +604,21 @@
 
 lemma Abs_rename_set':
   fixes x::"'a::fs"
-  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
+  assumes a: "(p \<bullet> bs) \<sharp>* x" 
   and     b: "finite bs"
   shows "\<exists>q. [bs]set. x = [q \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 using Abs_rename_set[OF a b] by metis
 
 lemma Abs_rename_res':
   fixes x::"'a::fs"
-  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
+  assumes a: "(p \<bullet> bs) \<sharp>* x" 
   and     b: "finite bs"
   shows "\<exists>q. [bs]res. x = [q \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 using Abs_rename_res[OF a b] by metis
 
 lemma Abs_rename_lst':
   fixes x::"'a::fs"
-  assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" 
+  assumes a: "(p \<bullet> (set bs)) \<sharp>* x" 
   shows "\<exists>q. [bs]lst. x = [q \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 using Abs_rename_lst[OF a] by metis
 
diff -r b4472ebd7fad -r 619ecb57db38 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Thu Jan 13 12:12:47 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Fri Jan 14 14:22:25 2011 +0000
@@ -1668,6 +1668,21 @@
 by (rule supp_perm_eq)
    (simp add: fresh_star_supp_conv a)
 
+lemma supp_perm_perm_eq:
+  assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a"
+  shows "p \<bullet> x = q \<bullet> x"
+proof -
+  from a have "\<forall>a \<in> supp x. (-q + p) \<bullet> a = a" by simp
+  then have "\<forall>a \<in> supp x. a \<notin> supp (-q + p)" 
+    unfolding supp_perm by simp
+  then have "supp x \<sharp>* (-q + p)"
+    unfolding fresh_star_def fresh_def by simp
+  then have "(-q + p) \<bullet> x = x" by (simp only: supp_perm_eq)
+  then show "p \<bullet> x = q \<bullet> x"
+    by (metis permute_minus_cancel permute_plus)
+qed
+    
+
 
 section {* Avoiding of atom sets *}
 
@@ -1793,10 +1808,9 @@
 section {* Renaming permutations *}
 
 lemma set_renaming_perm:
-  assumes a: "p \<bullet> bs \<inter> bs = {}" 
-  and     b: "finite bs"
+  assumes b: "finite bs"
   shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
-using b a
+using b
 proof (induct)
   case empty
   have "0 \<bullet> {} = p \<bullet> {} \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
@@ -1827,8 +1841,14 @@
     }
     moreover 
     { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
-	using ** `a \<notin> bs` `p \<bullet> insert a bs \<inter> insert a bs = {}`
-	by (auto simp add: supp_perm insert_eqvt)
+	using ** 
+	apply (auto simp add: supp_perm insert_eqvt)
+	apply (subgoal_tac "q \<bullet> a \<in> bs \<union> p \<bullet> bs")
+	apply(auto)[1]
+	apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}")
+	apply(blast)
+	apply(simp)
+	done
       then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by (simp add: supp_swap)
       moreover
       have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
@@ -1844,12 +1864,9 @@
     by blast
 qed
 
-
 lemma list_renaming_perm:
   fixes bs::"atom list"
-  assumes a: "(p \<bullet> (set bs)) \<inter> (set bs) = {}"
   shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))"
-using a
 proof (induct bs)
   case Nil
   have "0 \<bullet> [] = p \<bullet> [] \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []"
@@ -1882,8 +1899,14 @@
     }
     moreover 
     { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
-	using ** `a \<notin> set bs` `p \<bullet> (set (a # bs)) \<inter> set (a # bs) = {}`
-	by (auto simp add: supp_perm insert_eqvt)
+	using **
+	apply (auto simp add: supp_perm insert_eqvt)
+	apply (subgoal_tac "q \<bullet> a \<in> set bs \<union> p \<bullet> set bs")
+	apply(auto)[1]
+	apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}")
+	apply(blast)
+	apply(simp)
+	done
       then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" by (simp add: supp_swap)
       moreover
       have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"