1702 section {* Renaming permutations *}

  1703 

  1704 

  1705 lemma set_renaming_perm:

  1706   assumes a: "p \<bullet> bs \<inter> bs = {}" 

  1707   and     b: "finite bs"

  1708   shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"

  1709 using b a

  1710 proof (induct)

  1711   case empty

  1712   have "0 \<bullet> {} = p \<bullet> {} \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"

  1713     by (simp add: permute_set_eq supp_perm)

  1714   then show "\<exists>q. q \<bullet> {} = p \<bullet> {} \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast

  1715 next

  1716   case (insert a bs)

  1717   then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> p \<bullet> bs" 

  1718     by (simp add: insert_eqvt) 

  1719   then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs" by blast 

  1720   { assume 1: "q \<bullet> a = p \<bullet> a"

  1721     have "q \<bullet> insert a bs = p \<bullet> insert a bs" using 1 * by (simp add: insert_eqvt)

  1722     moreover 

  1723     have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 

  1724       using ** by (auto simp add: insert_eqvt)

  1725     ultimately 

  1726     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

  1727   }

  1728   moreover

  1729   { assume 2: "q \<bullet> a \<noteq> p \<bullet> a"

  1730     def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"

  1731     { have "(q \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` *[symmetric] by (simp add: mem_permute_iff)

  1732       moreover 

  1733       have "(p \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` by (simp add: mem_permute_iff)

  1734       ultimately 

  1735       have "q' \<bullet> insert a bs = p \<bullet> insert a bs" using 2 * unfolding q'_def 

  1736         by (simp add: insert_eqvt  swap_set_not_in) 

  1737     }

  1738     moreover 

  1739     { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs"

  1740 	using ** `a \<notin> bs` `p \<bullet> insert a bs \<inter> insert a bs = {}`

  1741 	by (auto simp add: supp_perm insert_eqvt)

  1742       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)

  1743       moreover

  1744       have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 

  1745 	using ** by (auto simp add: insert_eqvt)

  1746       ultimately 

  1747       have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 

  1748         unfolding q'_def using supp_plus_perm by blast

  1749     }

  1750     ultimately 

  1751     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

  1752   }

  1753   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"

  1754     by blast

  1755 qed

  1756 

  1757 

  1758 lemma list_renaming_perm:

  1759   fixes bs::"atom list"

  1760   assumes a: "(p \<bullet> (set bs)) \<inter> (set bs) = {}"

  1761   shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))"

  1762 using a

  1763 proof (induct bs)

  1764   case Nil

  1765   have "0 \<bullet> [] = p \<bullet> [] \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []"

  1766     by (simp add: permute_set_eq supp_perm)

  1767   then show "\<exists>q. q \<bullet> [] = p \<bullet> [] \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast

  1768 next

  1769   case (Cons a bs)

  1770   then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" 

  1771     by (simp add: insert_eqvt) 

  1772   then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" by blast 

  1773   { assume 1: "a \<in> set bs"

  1774     have "q \<bullet> a = p \<bullet> a" using * 1 by (induct bs) (auto)

  1775     then have "q \<bullet> (a # bs) = p \<bullet> (a # bs)" using * by simp 

  1776     moreover 

  1777     have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp add: insert_eqvt)

  1778     ultimately 

  1779     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

  1780   }

  1781   moreover

  1782   { assume 2: "a \<notin> set bs"

  1783     def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"

  1784     { have "(q \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` *[symmetric] 

  1785 	by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)

  1786       moreover 

  1787       have "(p \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` 

  1788 	by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)

  1789       ultimately 

  1790       have "q' \<bullet> (a # bs) = p \<bullet> (a # bs)" using 2 * unfolding q'_def 

  1791         by (simp add: swap_fresh_fresh) 

  1792     }

  1793     moreover 

  1794     { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"

  1795 	using ** `a \<notin> set bs` `p \<bullet> (set (a # bs)) \<inter> set (a # bs) = {}`

  1796 	by (auto simp add: supp_perm insert_eqvt)

  1797       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)

  1798       moreover

  1799       have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" 

  1800 	using ** by (auto simp add: insert_eqvt)

  1801       ultimately 

  1802       have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" 

  1803         unfolding q'_def using supp_plus_perm by blast

  1804     }

  1805     ultimately 

  1806     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

  1807   }

  1808   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))"

  1809     by blast

  1810 qed

  1811 

  1812