equal
deleted
inserted
replaced
1665 lemma perm_supp_eq: |
1665 lemma perm_supp_eq: |
1666 assumes a: "(supp p) \<sharp>* x" |
1666 assumes a: "(supp p) \<sharp>* x" |
1667 shows "p \<bullet> x = x" |
1667 shows "p \<bullet> x = x" |
1668 by (rule supp_perm_eq) |
1668 by (rule supp_perm_eq) |
1669 (simp add: fresh_star_supp_conv a) |
1669 (simp add: fresh_star_supp_conv a) |
|
1670 |
|
1671 lemma supp_perm_perm_eq: |
|
1672 assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a" |
|
1673 shows "p \<bullet> x = q \<bullet> x" |
|
1674 proof - |
|
1675 from a have "\<forall>a \<in> supp x. (-q + p) \<bullet> a = a" by simp |
|
1676 then have "\<forall>a \<in> supp x. a \<notin> supp (-q + p)" |
|
1677 unfolding supp_perm by simp |
|
1678 then have "supp x \<sharp>* (-q + p)" |
|
1679 unfolding fresh_star_def fresh_def by simp |
|
1680 then have "(-q + p) \<bullet> x = x" by (simp only: supp_perm_eq) |
|
1681 then show "p \<bullet> x = q \<bullet> x" |
|
1682 by (metis permute_minus_cancel permute_plus) |
|
1683 qed |
|
1684 |
1670 |
1685 |
1671 |
1686 |
1672 section {* Avoiding of atom sets *} |
1687 section {* Avoiding of atom sets *} |
1673 |
1688 |
1674 text {* |
1689 text {* |
1791 |
1806 |
1792 |
1807 |
1793 section {* Renaming permutations *} |
1808 section {* Renaming permutations *} |
1794 |
1809 |
1795 lemma set_renaming_perm: |
1810 lemma set_renaming_perm: |
1796 assumes a: "p \<bullet> bs \<inter> bs = {}" |
1811 assumes b: "finite bs" |
1797 and b: "finite bs" |
|
1798 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" |
1812 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" |
1799 using b a |
1813 using b |
1800 proof (induct) |
1814 proof (induct) |
1801 case empty |
1815 case empty |
1802 have "0 \<bullet> {} = p \<bullet> {} \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}" |
1816 have "0 \<bullet> {} = p \<bullet> {} \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}" |
1803 by (simp add: permute_set_eq supp_perm) |
1817 by (simp add: permute_set_eq supp_perm) |
1804 then show "\<exists>q. q \<bullet> {} = p \<bullet> {} \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast |
1818 then show "\<exists>q. q \<bullet> {} = p \<bullet> {} \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast |
1825 have "q' \<bullet> insert a bs = p \<bullet> insert a bs" using 2 * unfolding q'_def |
1839 have "q' \<bullet> insert a bs = p \<bullet> insert a bs" using 2 * unfolding q'_def |
1826 by (simp add: insert_eqvt swap_set_not_in) |
1840 by (simp add: insert_eqvt swap_set_not_in) |
1827 } |
1841 } |
1828 moreover |
1842 moreover |
1829 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
1843 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
1830 using ** `a \<notin> bs` `p \<bullet> insert a bs \<inter> insert a bs = {}` |
1844 using ** |
1831 by (auto simp add: supp_perm insert_eqvt) |
1845 apply (auto simp add: supp_perm insert_eqvt) |
|
1846 apply (subgoal_tac "q \<bullet> a \<in> bs \<union> p \<bullet> bs") |
|
1847 apply(auto)[1] |
|
1848 apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}") |
|
1849 apply(blast) |
|
1850 apply(simp) |
|
1851 done |
1832 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) |
1852 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) |
1833 moreover |
1853 moreover |
1834 have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
1854 have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
1835 using ** by (auto simp add: insert_eqvt) |
1855 using ** by (auto simp add: insert_eqvt) |
1836 ultimately |
1856 ultimately |
1842 } |
1862 } |
1843 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" |
1863 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" |
1844 by blast |
1864 by blast |
1845 qed |
1865 qed |
1846 |
1866 |
1847 |
|
1848 lemma list_renaming_perm: |
1867 lemma list_renaming_perm: |
1849 fixes bs::"atom list" |
1868 fixes bs::"atom list" |
1850 assumes a: "(p \<bullet> (set bs)) \<inter> (set bs) = {}" |
|
1851 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))" |
1869 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))" |
1852 using a |
|
1853 proof (induct bs) |
1870 proof (induct bs) |
1854 case Nil |
1871 case Nil |
1855 have "0 \<bullet> [] = p \<bullet> [] \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []" |
1872 have "0 \<bullet> [] = p \<bullet> [] \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []" |
1856 by (simp add: permute_set_eq supp_perm) |
1873 by (simp add: permute_set_eq supp_perm) |
1857 then show "\<exists>q. q \<bullet> [] = p \<bullet> [] \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast |
1874 then show "\<exists>q. q \<bullet> [] = p \<bullet> [] \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast |
1880 have "q' \<bullet> (a # bs) = p \<bullet> (a # bs)" using 2 * unfolding q'_def |
1897 have "q' \<bullet> (a # bs) = p \<bullet> (a # bs)" using 2 * unfolding q'_def |
1881 by (simp add: swap_fresh_fresh) |
1898 by (simp add: swap_fresh_fresh) |
1882 } |
1899 } |
1883 moreover |
1900 moreover |
1884 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
1901 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
1885 using ** `a \<notin> set bs` `p \<bullet> (set (a # bs)) \<inter> set (a # bs) = {}` |
1902 using ** |
1886 by (auto simp add: supp_perm insert_eqvt) |
1903 apply (auto simp add: supp_perm insert_eqvt) |
|
1904 apply (subgoal_tac "q \<bullet> a \<in> set bs \<union> p \<bullet> set bs") |
|
1905 apply(auto)[1] |
|
1906 apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}") |
|
1907 apply(blast) |
|
1908 apply(simp) |
|
1909 done |
1887 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) |
1910 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) |
1888 moreover |
1911 moreover |
1889 have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
1912 have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
1890 using ** by (auto simp add: insert_eqvt) |
1913 using ** by (auto simp add: insert_eqvt) |
1891 ultimately |
1914 ultimately |