src/HOL/Library/Multiset_Order.thy
changeset 63525 f01d1e393f3f
parent 63410 9789ccc2a477
child 63793 e68a0b651eb5
     1.1 --- a/src/HOL/Library/Multiset_Order.thy	Wed Jul 20 13:51:38 2016 +0200
     1.2 +++ b/src/HOL/Library/Multiset_Order.thy	Wed Jul 20 14:52:09 2016 +0200
     1.3 @@ -187,9 +187,6 @@
     1.4    shows "{#} \<le> M"
     1.5    by (simp add: subset_eq_imp_le_multiset)
     1.6  
     1.7 -lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
     1.8 -  by (rule cancel_comm_monoid_add_class.add_cancel_left_right)
     1.9 -
    1.10  lemma ex_gt_imp_less_multiset: "(\<exists>y. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M < N"
    1.11    unfolding less_multiset\<^sub>H\<^sub>O
    1.12    by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
    1.13 @@ -207,7 +204,7 @@
    1.14  lemma union_le_diff_plus: "P \<le># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
    1.15    by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)
    1.16  
    1.17 -instantiation multiset :: (preorder) ordered_ab_semigroup_add_imp_le
    1.18 +instantiation multiset :: (preorder) ordered_ab_semigroup_monoid_add_imp_le
    1.19  begin
    1.20  
    1.21  lemma less_eq_multiset\<^sub>H\<^sub>O:
    1.22 @@ -219,24 +216,16 @@
    1.23  lemma
    1.24    fixes M N :: "'a multiset"
    1.25    shows
    1.26 -    less_eq_multiset_plus_left[simp]: "N \<le> (M + N)" and
    1.27 -    less_eq_multiset_plus_right[simp]: "M \<le> (M + N)"
    1.28 -  using add_le_cancel_left[of N 0] add_le_cancel_left[of M 0 N] by (simp_all add: add.commute)
    1.29 -
    1.30 -lemma
    1.31 -  fixes M N :: "'a multiset"
    1.32 -  shows
    1.33 -    le_multiset_plus_plus_left_iff: "M + N < M' + N \<longleftrightarrow> M < M'" and
    1.34 -    le_multiset_plus_plus_right_iff: "M + N < M + N' \<longleftrightarrow> N < N'"
    1.35 +    less_eq_multiset_plus_left: "N \<le> (M + N)" and
    1.36 +    less_eq_multiset_plus_right: "M \<le> (M + N)"
    1.37    by simp_all
    1.38  
    1.39  lemma
    1.40    fixes M N :: "'a multiset"
    1.41    shows
    1.42 -    le_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N < M + N" and
    1.43 -    le_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M < M + N"
    1.44 -  using [[metis_verbose = false]]
    1.45 -  by (metis add.right_neutral le_multiset_empty_left le_multiset_plus_plus_right_iff add.commute)+
    1.46 +    le_multiset_plus_left_nonempty: "M \<noteq> {#} \<Longrightarrow> N < M + N" and
    1.47 +    le_multiset_plus_right_nonempty: "N \<noteq> {#} \<Longrightarrow> M < M + N"
    1.48 +    by simp_all
    1.49  
    1.50  end
    1.51