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)