equal
deleted
inserted
replaced
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 |