src/HOL/Library/Multiset_Order.thy
 changeset 62430 9527ff088c15 parent 61424 c3658c18b7bc child 63040 eb4ddd18d635
```     1.1 --- a/src/HOL/Library/Multiset_Order.thy	Fri Feb 26 22:15:09 2016 +0100
1.2 +++ b/src/HOL/Library/Multiset_Order.thy	Fri Feb 26 22:44:11 2016 +0100
1.3 @@ -77,22 +77,29 @@
1.4  definition less_multiset\<^sub>H\<^sub>O where
1.5    "less_multiset\<^sub>H\<^sub>O M N \<longleftrightarrow> M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
1.6
1.7 -lemma mult_imp_less_multiset\<^sub>H\<^sub>O: "(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N"
1.8 -proof (unfold mult_def less_multiset\<^sub>H\<^sub>O_def, induct rule: trancl_induct)
1.9 +lemma mult_imp_less_multiset\<^sub>H\<^sub>O:
1.10 +  "(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N"
1.11 +proof (unfold mult_def, induct rule: trancl_induct)
1.12    case (base P)
1.13 -  then show ?case unfolding mult1_def by force
1.14 +  then show ?case
1.15 +    by (auto elim!: mult1_lessE simp add: count_eq_zero_iff less_multiset\<^sub>H\<^sub>O_def split: if_splits dest!: Suc_lessD)
1.16  next
1.17    case (step N P)
1.18 +  from step(3) have "M \<noteq> N" and
1.19 +    **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x>y. count M x < count N x)"
1.20 +    by (simp_all add: less_multiset\<^sub>H\<^sub>O_def)
1.21    from step(2) obtain M0 a K where
1.22 -    *: "P = M0 + {#a#}" "N = M0 + K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
1.23 -    unfolding mult1_def by blast
1.24 -  then have count_K_a: "count K a = 0" by auto
1.25 -  with step(3) *(1,2) have "M \<noteq> P" by (force dest: *(3) split: if_splits)
1.26 +    *: "P = M0 + {#a#}" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
1.27 +    by (blast elim: mult1_lessE)
1.28 +  from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) split: if_splits)
1.29    moreover
1.30    { assume "count P a \<le> count M a"
1.31 -    with count_K_a have "count N a < count M a" unfolding *(1,2) by auto
1.32 -      with step(3) obtain z where z: "z > a" "count M z < count N z" by blast
1.33 -      with * have "count N z \<le> count P z" by force
1.34 +    with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
1.35 +      by (auto simp add: not_in_iff)
1.36 +      with ** obtain z where z: "z > a" "count M z < count N z"
1.37 +        by blast
1.38 +      with * have "count N z \<le> count P z"
1.39 +        by (force simp add: not_in_iff)
1.40        with z have "\<exists>z > a. count M z < count P z" by auto
1.41    } note count_a = this
1.42    { fix y
1.43 @@ -106,27 +113,29 @@
1.44        show ?thesis
1.45        proof (cases "y \<in># K")
1.46          case True
1.47 -        with *(3) have "y < a" by simp
1.48 +        with *(4) have "y < a" by simp
1.49          then show ?thesis by (cases "count P a \<le> count M a") (auto dest: count_a intro: less_trans)
1.50        next
1.51          case False
1.52 -        with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2) by simp
1.53 -        with count_y step(3) obtain z where z: "z > y" "count M z < count N z" by auto
1.54 +        with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2)
1.55 +          by (simp add: not_in_iff)
1.56 +        with count_y ** obtain z where z: "z > y" "count M z < count N z" by auto
1.57          show ?thesis
1.58          proof (cases "z \<in># K")
1.59            case True
1.60 -          with *(3) have "z < a" by simp
1.61 +          with *(4) have "z < a" by simp
1.62            with z(1) show ?thesis
1.63              by (cases "count P a \<le> count M a") (auto dest!: count_a intro: less_trans)
1.64          next
1.65            case False
1.66 -          with count_K_a have "count N z \<le> count P z" unfolding * by auto
1.67 +          with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding *
1.68 +            by (auto simp add: not_in_iff)
1.69            with z show ?thesis by auto
1.70          qed
1.71        qed
1.72      qed
1.73    }
1.74 -  ultimately show ?case by blast
1.75 +  ultimately show ?case unfolding less_multiset\<^sub>H\<^sub>O_def by blast
1.76  qed
1.77
1.78  lemma less_multiset\<^sub>D\<^sub>M_imp_mult:
1.79 @@ -157,10 +166,12 @@
1.80    proof (intro allI impI)
1.81      fix k
1.82      assume "k \<in># Y"
1.83 -    then have "count N k < count M k" unfolding Y_def by auto
1.84 +    then have "count N k < count M k" unfolding Y_def
1.85 +      by (auto simp add: in_diff_count)
1.86      with \<open>less_multiset\<^sub>H\<^sub>O M N\<close> obtain a where "k < a" and "count M a < count N a"
1.87        unfolding less_multiset\<^sub>H\<^sub>O_def by blast
1.88 -    then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def by auto
1.89 +    then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def
1.90 +      by (auto simp add: in_diff_count)
1.91    qed
1.92  qed
1.93
1.94 @@ -295,12 +306,13 @@
1.95      add.commute)+
1.96
1.97  lemma ex_gt_imp_less_multiset: "(\<exists>y :: 'a :: linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M #\<subset># N"
1.98 -  unfolding less_multiset\<^sub>H\<^sub>O by (metis less_irrefl less_nat_zero_code not_gr0)
1.99 -
1.100 +  unfolding less_multiset\<^sub>H\<^sub>O
1.101 +  by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
1.102 +
1.103  lemma ex_gt_count_imp_less_multiset:
1.104    "(\<forall>y :: 'a :: linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M #\<subset># N"
1.105 -  unfolding less_multiset\<^sub>H\<^sub>O by (metis add.left_neutral add_lessD1 dual_order.strict_iff_order
1.106 -    less_not_sym mset_leD mset_le_add_left)
1.107 +  unfolding less_multiset\<^sub>H\<^sub>O
1.108 +  by (metis add_gr_0 count_union mem_Collect_eq not_gr0 not_le not_less_iff_gr_or_eq set_mset_def)
1.109
1.110  lemma union_less_diff_plus: "P \<le># M \<Longrightarrow> N #\<subset># P \<Longrightarrow> M - P + N #\<subset># M"
1.111    by (drule subset_mset.diff_add[symmetric]) (metis union_less_mono2)
```