2097 by (simp add: supp_set)

  2097 by (simp add: supp_set)

  2098 

  2098 

  2099 

  2099 

  2100 subsection {* Type @{typ "'a multiset"} is finitely supported *}

  2100 subsection {* Type @{typ "'a multiset"} is finitely supported *}

  2101 

  2101 

  2103   shows "p \<bullet> (set_of M) = set_of (p \<bullet> M)"

  2103   shows "p \<bullet> (set_of M) = set_of (p \<bullet> M)"

  2104 by (induct M) (simp_all add: insert_eqvt empty_eqvt)

  2104 by (induct M) (simp_all add: insert_eqvt empty_eqvt)

  2105 

  2105 

  2106 lemma supp_set_of:

  2106 lemma supp_set_of:

  2107   shows "supp (set_of M) \<subseteq> supp M"

  2107   shows "supp (set_of M) \<subseteq> supp M"

  2884 class at_base = pt +

  2884 class at_base = pt +

  2885   fixes atom :: "'a \<Rightarrow> atom"

  2885   fixes atom :: "'a \<Rightarrow> atom"

  2886   assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"

  2886   assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"

  2887   assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)"

  2887   assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)"

  2888 

  2888 

  2890 

  2890 

  2891 class at = at_base +

  2891 class at = at_base +

  2892   assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"

  2892   assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"

  2893 

  2893 

  2894 lemma sort_ineq [simp]:

  2894 lemma sort_ineq [simp]: