src/HOL/Library/Multiset.thy
changeset 35308 359e0fd38a92
parent 35273 51692ec1b220
child 35352 fa051b504c3f
equal deleted inserted replaced
35307:8ee07543409f 35308:359e0fd38a92
  1210   "M' <# M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
  1210   "M' <# M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
  1211 
  1211 
  1212 definition le_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
  1212 definition le_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
  1213   "M' <=# M \<longleftrightarrow> M' <# M \<or> M' = M"
  1213   "M' <=# M \<longleftrightarrow> M' <# M \<or> M' = M"
  1214 
  1214 
  1215 notation (xsymbol) less_multiset (infix "\<subset>#" 50)
  1215 notation (xsymbols) less_multiset (infix "\<subset>#" 50)
  1216 notation (xsymbol) le_multiset (infix "\<subseteq>#" 50)
  1216 notation (xsymbols) le_multiset (infix "\<subseteq>#" 50)
  1217 
  1217 
  1218 interpretation multiset_order: order le_multiset less_multiset
  1218 interpretation multiset_order: order le_multiset less_multiset
  1219 proof -
  1219 proof -
  1220   have irrefl: "\<And>M :: 'a multiset. \<not> M \<subset># M"
  1220   have irrefl: "\<And>M :: 'a multiset. \<not> M \<subset># M"
  1221   proof
  1221   proof