src/HOL/Library/Multiset_Order.thy
changeset 63793 e68a0b651eb5
parent 63525 f01d1e393f3f
child 64076 9f089287687b
     1.1 --- a/src/HOL/Library/Multiset_Order.thy	Mon Sep 05 15:00:37 2016 +0200
     1.2 +++ b/src/HOL/Library/Multiset_Order.thy	Mon Sep 05 15:47:50 2016 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4      **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x>y. count M x < count N x)"
     1.5      by (simp_all add: less_multiset\<^sub>H\<^sub>O_def)
     1.6    from step(2) obtain M0 a K where
     1.7 -    *: "P = M0 + {#a#}" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
     1.8 +    *: "P = add_mset a M0" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
     1.9      by (blast elim: mult1_lessE)
    1.10    from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) elim!: less_asym split: if_splits )
    1.11    moreover
    1.12 @@ -180,7 +180,7 @@
    1.13    by (simp add: less_le_not_le subseteq_mset_def)
    1.14  
    1.15  lemma le_multiset_right_total:
    1.16 -  shows "M < M + {#x#}"
    1.17 +  shows "M < add_mset x M"
    1.18    unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp
    1.19  
    1.20  lemma less_eq_multiset_empty_left[simp]:
    1.21 @@ -229,6 +229,52 @@
    1.22  
    1.23  end
    1.24  
    1.25 +
    1.26 +subsection \<open>Simprocs\<close>
    1.27 +
    1.28 +lemma mset_le_add_iff1:
    1.29 +  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (repeat_mset (i-j) u + m \<le> n)"
    1.30 +proof -
    1.31 +  assume "j \<le> i"
    1.32 +  then have "j + (i - j) = i"
    1.33 +    using le_add_diff_inverse by blast
    1.34 +  then show ?thesis
    1.35 +    by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
    1.36 +qed
    1.37 +
    1.38 +lemma mset_le_add_iff2:
    1.39 +  "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (m \<le> repeat_mset (j-i) u + n)"
    1.40 +proof -
    1.41 +  assume "i \<le> j"
    1.42 +  then have "i + (j - i) = j"
    1.43 +    using le_add_diff_inverse by blast
    1.44 +  then show ?thesis
    1.45 +    by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
    1.46 +qed
    1.47 +
    1.48 +lemma mset_less_add_iff1:
    1.49 +  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m < repeat_mset j u + n) = (repeat_mset (i-j) u + m < n)"
    1.50 +  by (simp add: less_le_not_le mset_le_add_iff1 mset_le_add_iff2)
    1.51 +
    1.52 +lemma mset_less_add_iff2:
    1.53 +     "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m < repeat_mset j u + n) = (m < repeat_mset (j-i) u + n)"
    1.54 +  by (simp add: less_le_not_le mset_le_add_iff1 mset_le_add_iff2)
    1.55 +
    1.56 +ML_file "multiset_order_simprocs.ML"
    1.57 +
    1.58 +simproc_setup msetless_cancel_numerals
    1.59 +  ("(l::'a::preorder multiset) + m < n" | "(l::'a multiset) < m + n" |
    1.60 +   "add_mset a m < n" | "m < add_mset a n") =
    1.61 +  \<open>fn phi => Multiset_Order_Simprocs.less_cancel_msets\<close>
    1.62 +
    1.63 +simproc_setup msetle_cancel_numerals
    1.64 +  ("(l::'a::preorder multiset) + m \<le> n" | "(l::'a multiset) \<le> m + n" |
    1.65 +   "add_mset a m \<le> n" | "m \<le> add_mset a n") =
    1.66 +  \<open>fn phi => Multiset_Order_Simprocs.le_cancel_msets\<close>
    1.67 +
    1.68 +
    1.69 +subsection \<open>Additional facts and instantiations\<close>
    1.70 +
    1.71  lemma ex_gt_count_imp_le_multiset:
    1.72    "(\<forall>y :: 'a :: order. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M < N"
    1.73    unfolding less_multiset\<^sub>H\<^sub>O