--- a/Nominal/Nominal2_Base.thy Tue Dec 07 14:27:39 2010 +0000
+++ b/Nominal/Nominal2_Base.thy Tue Dec 07 19:16:09 2010 +0000
@@ -1699,6 +1699,117 @@
then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast
qed
+section {* Renaming permutations *}
+
+
+lemma set_renaming_perm:
+ assumes a: "p \<bullet> bs \<inter> bs = {}"
+ and b: "finite bs"
+ shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
+using b a
+proof (induct)
+ case empty
+ have "0 \<bullet> {} = p \<bullet> {} \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
+ by (simp add: permute_set_eq supp_perm)
+ then show "\<exists>q. q \<bullet> {} = p \<bullet> {} \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast
+next
+ case (insert a bs)
+ then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> p \<bullet> bs"
+ by (simp add: insert_eqvt)
+ then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs" by blast
+ { assume 1: "q \<bullet> a = p \<bullet> a"
+ have "q \<bullet> insert a bs = p \<bullet> insert a bs" using 1 * by (simp add: insert_eqvt)
+ moreover
+ have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
+ using ** by (auto simp add: insert_eqvt)
+ ultimately
+ have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
+ }
+ moreover
+ { assume 2: "q \<bullet> a \<noteq> p \<bullet> a"
+ def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"
+ { have "(q \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` *[symmetric] by (simp add: mem_permute_iff)
+ moreover
+ have "(p \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` by (simp add: mem_permute_iff)
+ ultimately
+ have "q' \<bullet> insert a bs = p \<bullet> insert a bs" using 2 * unfolding q'_def
+ by (simp add: insert_eqvt swap_set_not_in)
+ }
+ 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)
+ 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"
+ using ** by (auto simp add: insert_eqvt)
+ ultimately
+ have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
+ unfolding q'_def using supp_plus_perm by blast
+ }
+ ultimately
+ have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
+ }
+ ultimately show "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
+ 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 []"
+ by (simp add: permute_set_eq supp_perm)
+ then show "\<exists>q. q \<bullet> [] = p \<bullet> [] \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast
+next
+ case (Cons a bs)
+ then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)"
+ by (simp add: insert_eqvt)
+ then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" by blast
+ { assume 1: "a \<in> set bs"
+ have "q \<bullet> a = p \<bullet> a" using * 1 by (induct bs) (auto)
+ then have "q \<bullet> (a # bs) = p \<bullet> (a # bs)" using * by simp
+ moreover
+ have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp add: insert_eqvt)
+ ultimately
+ have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
+ }
+ moreover
+ { assume 2: "a \<notin> set bs"
+ def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"
+ { have "(q \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` *[symmetric]
+ by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)
+ moreover
+ have "(p \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs`
+ by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)
+ ultimately
+ have "q' \<bullet> (a # bs) = p \<bullet> (a # bs)" using 2 * unfolding q'_def
+ by (simp add: swap_fresh_fresh)
+ }
+ 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)
+ 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))"
+ using ** by (auto simp add: insert_eqvt)
+ ultimately
+ have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
+ unfolding q'_def using supp_plus_perm by blast
+ }
+ ultimately
+ have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
+ }
+ ultimately show "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
+ by blast
+qed
+
+
section {* Concrete Atoms Types *}