1783 then have "(-q + p) \<bullet> x = x" by (simp only: supp_perm_eq) |
1783 then have "(-q + p) \<bullet> x = x" by (simp only: supp_perm_eq) |
1784 then show "p \<bullet> x = q \<bullet> x" |
1784 then show "p \<bullet> x = q \<bullet> x" |
1785 by (metis permute_minus_cancel permute_plus) |
1785 by (metis permute_minus_cancel permute_plus) |
1786 qed |
1786 qed |
1787 |
1787 |
1788 |
1788 lemma atom_set_perm_eq: |
|
1789 assumes a: "as \<sharp>* p" |
|
1790 shows "p \<bullet> as = as" |
|
1791 proof - |
|
1792 from a have "supp p \<subseteq> {a. a \<notin> as}" |
|
1793 unfolding supp_perm fresh_star_def fresh_def by auto |
|
1794 then show "p \<bullet> as = as" |
|
1795 proof (induct p rule: perm_struct_induct) |
|
1796 case zero |
|
1797 show "0 \<bullet> as = as" by simp |
|
1798 next |
|
1799 case (swap p a b) |
|
1800 then have "a \<notin> as" "b \<notin> as" "p \<bullet> as = as" by simp_all |
|
1801 then show "((a \<rightleftharpoons> b) + p) \<bullet> as = as" by (simp add: swap_set_not_in) |
|
1802 qed |
|
1803 qed |
1789 |
1804 |
1790 section {* Avoiding of atom sets *} |
1805 section {* Avoiding of atom sets *} |
1791 |
1806 |
1792 text {* |
1807 text {* |
1793 For every set of atoms, there is another set of atoms |
1808 For every set of atoms, there is another set of atoms |
1908 qed |
1923 qed |
1909 |
1924 |
1910 |
1925 |
1911 section {* Renaming permutations *} |
1926 section {* Renaming permutations *} |
1912 |
1927 |
|
1928 |
1913 lemma set_renaming_perm: |
1929 lemma set_renaming_perm: |
1914 assumes b: "finite bs" |
1930 assumes b: "finite bs" |
1915 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" |
1931 shows "\<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" |
1916 using b |
1932 using b |
1917 proof (induct) |
1933 proof (induct) |
1918 case empty |
1934 case empty |
1919 have "0 \<bullet> {} = p \<bullet> {} \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}" |
1935 have "(\<forall>b \<in> {}. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}" |
1920 by (simp add: permute_set_eq supp_perm) |
1936 by (simp add: permute_set_eq supp_perm) |
1921 then show "\<exists>q. q \<bullet> {} = p \<bullet> {} \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast |
1937 then show "\<exists>q. (\<forall>b \<in> {}. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast |
1922 next |
1938 next |
1923 case (insert a bs) |
1939 case (insert a bs) |
1924 then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> p \<bullet> bs" |
1940 then have " \<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> p \<bullet> bs" by simp |
1925 by (simp add: insert_eqvt) |
1941 then obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs" |
1926 then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs" by blast |
1942 by (metis empty_subsetI insert(3) supp_swap) |
1927 { assume 1: "q \<bullet> a = p \<bullet> a" |
1943 { assume 1: "q \<bullet> a = p \<bullet> a" |
1928 have "q \<bullet> insert a bs = p \<bullet> insert a bs" using 1 * by (simp add: insert_eqvt) |
1944 have "\<forall>b \<in> (insert a bs). q \<bullet> b = p \<bullet> b" using 1 * by simp |
1929 moreover |
1945 moreover |
1930 have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
1946 have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
1931 using ** by (auto simp add: insert_eqvt) |
1947 using ** by (auto simp add: insert_eqvt) |
1932 ultimately |
1948 ultimately |
1933 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 |
1949 have "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast |
1934 } |
1950 } |
1935 moreover |
1951 moreover |
1936 { assume 2: "q \<bullet> a \<noteq> p \<bullet> a" |
1952 { assume 2: "q \<bullet> a \<noteq> p \<bullet> a" |
1937 def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" |
1953 def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" |
1938 { have "(q \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` *[symmetric] by (simp add: mem_permute_iff) |
1954 have "\<forall>b \<in> insert a bs. q' \<bullet> b = p \<bullet> b" using 2 * `a \<notin> bs` unfolding q'_def |
1939 moreover |
1955 by (auto simp add: swap_atom) |
1940 have "(p \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` by (simp add: mem_permute_iff) |
|
1941 ultimately |
|
1942 have "q' \<bullet> insert a bs = p \<bullet> insert a bs" using 2 * unfolding q'_def |
|
1943 by (simp add: insert_eqvt swap_set_not_in) |
|
1944 } |
|
1945 moreover |
1956 moreover |
1946 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
1957 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
1947 using ** |
1958 using ** |
1948 apply (auto simp add: supp_perm insert_eqvt) |
1959 apply (auto simp add: supp_perm insert_eqvt) |
1949 apply (subgoal_tac "q \<bullet> a \<in> bs \<union> p \<bullet> bs") |
1960 apply (subgoal_tac "q \<bullet> a \<in> bs \<union> p \<bullet> bs") |
1959 ultimately |
1970 ultimately |
1960 have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
1971 have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
1961 unfolding q'_def using supp_plus_perm by blast |
1972 unfolding q'_def using supp_plus_perm by blast |
1962 } |
1973 } |
1963 ultimately |
1974 ultimately |
1964 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 |
1975 have "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast |
1965 } |
1976 } |
1966 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" |
1977 ultimately show "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
1967 by blast |
1978 by blast |
1968 qed |
1979 qed |
1969 |
1980 |
|
1981 |
1970 lemma list_renaming_perm: |
1982 lemma list_renaming_perm: |
1971 fixes bs::"atom list" |
1983 shows "\<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" |
1972 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))" |
|
1973 proof (induct bs) |
1984 proof (induct bs) |
1974 case Nil |
1985 case Nil |
1975 have "0 \<bullet> [] = p \<bullet> [] \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []" |
1986 have "(\<forall>b \<in> set []. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []" |
1976 by (simp add: permute_set_eq supp_perm) |
1987 by (simp add: supp_zero_perm) |
1977 then show "\<exists>q. q \<bullet> [] = p \<bullet> [] \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast |
1988 then show "\<exists>q. (\<forall>b \<in> set []. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast |
1978 next |
1989 next |
1979 case (Cons a bs) |
1990 case (Cons a bs) |
1980 then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" |
1991 then have " \<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" by simp |
1981 by (simp add: insert_eqvt) |
1992 then obtain q where *: "\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" |
1982 then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" by blast |
1993 by (blast) |
1983 { assume 1: "a \<in> set bs" |
1994 { assume 1: "a \<in> set bs" |
1984 have "q \<bullet> a = p \<bullet> a" using * 1 by (induct bs) (auto) |
1995 have "q \<bullet> a = p \<bullet> a" using * 1 by (induct bs) (auto) |
1985 then have "q \<bullet> (a # bs) = p \<bullet> (a # bs)" using * by simp |
1996 then have "\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b" using * by simp |
1986 moreover |
1997 moreover |
1987 have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp add: insert_eqvt) |
1998 have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp add: insert_eqvt) |
1988 ultimately |
1999 ultimately |
1989 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 |
2000 have "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast |
1990 } |
2001 } |
1991 moreover |
2002 moreover |
1992 { assume 2: "a \<notin> set bs" |
2003 { assume 2: "a \<notin> set bs" |
1993 def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" |
2004 def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" |
1994 { have "(q \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` *[symmetric] |
2005 have "\<forall>b \<in> set (a # bs). q' \<bullet> b = p \<bullet> b" |
1995 by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list) |
2006 unfolding q'_def using 2 * `a \<notin> set bs` by (auto simp add: swap_atom) |
1996 moreover |
|
1997 have "(p \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` |
|
1998 by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list) |
|
1999 ultimately |
|
2000 have "q' \<bullet> (a # bs) = p \<bullet> (a # bs)" using 2 * unfolding q'_def |
|
2001 by (simp add: swap_fresh_fresh) |
|
2002 } |
|
2003 moreover |
2007 moreover |
2004 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2008 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2005 using ** |
2009 using ** |
2006 apply (auto simp add: supp_perm insert_eqvt) |
2010 apply (auto simp add: supp_perm insert_eqvt) |
2007 apply (subgoal_tac "q \<bullet> a \<in> set bs \<union> p \<bullet> set bs") |
2011 apply (subgoal_tac "q \<bullet> a \<in> set bs \<union> p \<bullet> set bs") |