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.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.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.36 +qed
1.37 +
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.46 +qed
1.47 +
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.51 +
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.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
```