equal
deleted
inserted
replaced
413 interpretation mset_order: order "op \<le>#" "op <#" |
413 interpretation mset_order: order "op \<le>#" "op <#" |
414 proof qed (auto intro: order.intro mset_le_refl mset_le_antisym |
414 proof qed (auto intro: order.intro mset_le_refl mset_le_antisym |
415 mset_le_trans simp: mset_less_def) |
415 mset_le_trans simp: mset_less_def) |
416 |
416 |
417 interpretation mset_order_cancel_semigroup: |
417 interpretation mset_order_cancel_semigroup: |
418 pordered_cancel_ab_semigroup_add "op +" "op \<le>#" "op <#" |
418 ordered_cancel_ab_semigroup_add "op +" "op \<le>#" "op <#" |
419 proof qed (erule mset_le_mono_add [OF mset_le_refl]) |
419 proof qed (erule mset_le_mono_add [OF mset_le_refl]) |
420 |
420 |
421 interpretation mset_order_semigroup_cancel: |
421 interpretation mset_order_semigroup_cancel: |
422 pordered_ab_semigroup_add_imp_le "op +" "op \<le>#" "op <#" |
422 ordered_ab_semigroup_add_imp_le "op +" "op \<le>#" "op <#" |
423 proof qed simp |
423 proof qed simp |
424 |
424 |
425 lemma mset_lessD: "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B" |
425 lemma mset_lessD: "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B" |
426 apply (clarsimp simp: mset_le_def mset_less_def) |
426 apply (clarsimp simp: mset_le_def mset_less_def) |
427 apply (erule_tac x=x in allE) |
427 apply (erule_tac x=x in allE) |
1346 qed |
1346 qed |
1347 |
1347 |
1348 lemma union_upper2: "B <= A + (B::'a::order multiset)" |
1348 lemma union_upper2: "B <= A + (B::'a::order multiset)" |
1349 by (subst add_commute) (rule union_upper1) |
1349 by (subst add_commute) (rule union_upper1) |
1350 |
1350 |
1351 instance multiset :: (order) pordered_ab_semigroup_add |
1351 instance multiset :: (order) ordered_ab_semigroup_add |
1352 apply intro_classes |
1352 apply intro_classes |
1353 apply (erule union_le_mono[OF mult_le_refl]) |
1353 apply (erule union_le_mono[OF mult_le_refl]) |
1354 done |
1354 done |
1355 |
1355 |
1356 |
1356 |