1408 lemma fresh_star_set:

  1408 lemma fresh_star_set:

  1409   fixes xs::"('a::fs) list"

  1409   fixes xs::"('a::fs) list"

  1410   shows "as \<sharp>* set xs \<longleftrightarrow> as \<sharp>* xs"

  1410   shows "as \<sharp>* set xs \<longleftrightarrow> as \<sharp>* xs"

  1411 unfolding fresh_star_def

  1411 unfolding fresh_star_def

  1412 by (simp add: fresh_set)

  1412 by (simp add: fresh_set)

  1413 

  1423 

  1414 lemma fresh_star_Un:

  1424 lemma fresh_star_Un:

  1415   shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"

  1425   shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"

  1416   by (auto simp add: fresh_star_def)

  1426   by (auto simp add: fresh_star_def)

  1417 

  1427 

  1698   hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast

  1708   hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast

  1699   then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast

  1709   then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast

  1700 qed

  1710 qed

  1701 

  1711 

  1702 section {* Renaming permutations *}

  1712 section {* Renaming permutations *}

  1704 

  1713 

  1705 lemma set_renaming_perm:

  1714 lemma set_renaming_perm:

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

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

  1707   and     b: "finite bs"

  1716   and     b: "finite bs"

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

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

  1838 lemma fresh_atom_at_base: 

  1847 lemma fresh_atom_at_base: 

  1839   fixes b::"'a::at_base"

  1848   fixes b::"'a::at_base"

  1840   shows "a \<sharp> atom b \<longleftrightarrow> a \<sharp> b"

  1849   shows "a \<sharp> atom b \<longleftrightarrow> a \<sharp> b"

  1841   by (simp add: fresh_def supp_at_base supp_atom)

  1850   by (simp add: fresh_def supp_at_base supp_atom)

  1842 

  1851 

  1843 

  1856 

  1844 instance at_base < fs

  1857 instance at_base < fs

  1845 proof qed (simp add: supp_at_base)

  1858 proof qed (simp add: supp_at_base)

  1846 

  1859 

  1847 lemma at_base_infinite [simp]:

  1860 lemma at_base_infinite [simp]: