equal
deleted
inserted
replaced
776 unfolding le_multiset_def by (blast intro: mult_less_trans) |
776 unfolding le_multiset_def by (blast intro: mult_less_trans) |
777 |
777 |
778 theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))" |
778 theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))" |
779 unfolding le_multiset_def by auto |
779 unfolding le_multiset_def by auto |
780 |
780 |
781 instance |
781 instance proof |
782 apply intro_classes |
782 qed (auto simp add: mult_less_le dest: mult_le_antisym elim: mult_le_trans) |
783 apply (rule mult_less_le) |
|
784 apply (rule mult_le_refl) |
|
785 apply (erule mult_le_trans, assumption) |
|
786 apply (erule mult_le_antisym, assumption) |
|
787 done |
|
788 |
783 |
789 end |
784 end |
790 |
785 |
791 |
786 |
792 subsubsection {* Monotonicity of multiset union *} |
787 subsubsection {* Monotonicity of multiset union *} |
1099 apply (simp add: nth_mem_multiset_of) |
1094 apply (simp add: nth_mem_multiset_of) |
1100 apply simp |
1095 apply simp |
1101 done |
1096 done |
1102 |
1097 |
1103 interpretation mset_order: order ["op \<le>#" "op <#"] |
1098 interpretation mset_order: order ["op \<le>#" "op <#"] |
1104 by (auto intro: order.intro mset_le_refl mset_le_antisym |
1099 proof qed (auto intro: order.intro mset_le_refl mset_le_antisym |
1105 mset_le_trans simp: mset_less_def) |
1100 mset_le_trans simp: mset_less_def) |
1106 |
1101 |
1107 interpretation mset_order_cancel_semigroup: |
1102 interpretation mset_order_cancel_semigroup: |
1108 pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"] |
1103 pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"] |
1109 by unfold_locales (erule mset_le_mono_add [OF mset_le_refl]) |
1104 proof qed (erule mset_le_mono_add [OF mset_le_refl]) |
1110 |
1105 |
1111 interpretation mset_order_semigroup_cancel: |
1106 interpretation mset_order_semigroup_cancel: |
1112 pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"] |
1107 pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"] |
1113 by (unfold_locales) simp |
1108 proof qed simp |
1114 |
1109 |
1115 |
1110 |
1116 lemma mset_lessD: "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B" |
1111 lemma mset_lessD: "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B" |
1117 apply (clarsimp simp: mset_le_def mset_less_def) |
1112 apply (clarsimp simp: mset_le_def mset_less_def) |
1118 apply (erule_tac x=x in allE) |
1113 apply (erule_tac x=x in allE) |