249 using le_add_diff_inverse by blast |
249 using le_add_diff_inverse by blast |
250 then show ?thesis |
250 then show ?thesis |
251 by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset) |
251 by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset) |
252 qed |
252 qed |
253 |
253 |
254 lemma mset_less_add_iff1: |
|
255 "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m < repeat_mset j u + n) = (repeat_mset (i-j) u + m < n)" |
|
256 by (simp add: less_le_not_le mset_le_add_iff1 mset_le_add_iff2) |
|
257 |
|
258 lemma mset_less_add_iff2: |
|
259 "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m < repeat_mset j u + n) = (m < repeat_mset (j-i) u + n)" |
|
260 by (simp add: less_le_not_le mset_le_add_iff1 mset_le_add_iff2) |
|
261 |
|
262 ML_file "multiset_order_simprocs.ML" |
|
263 |
|
264 simproc_setup msetless_cancel |
254 simproc_setup msetless_cancel |
265 ("(l::'a::preorder multiset) + m < n" | "(l::'a multiset) < m + n" | |
255 ("(l::'a::preorder multiset) + m < n" | "(l::'a multiset) < m + n" | |
266 "add_mset a m < n" | "m < add_mset a n" | |
256 "add_mset a m < n" | "m < add_mset a n" | |
267 "replicate_mset p a < n" | "m < replicate_mset p a" | |
257 "replicate_mset p a < n" | "m < replicate_mset p a" | |
268 "repeat_mset p m < n" | "m < repeat_mset p n") = |
258 "repeat_mset p m < n" | "m < repeat_mset p n") = |
269 \<open>fn phi => Multiset_Order_Simprocs.less_cancel_msets\<close> |
259 \<open>fn phi => Cancel_Simprocs.less_cancel\<close> |
270 |
260 |
271 simproc_setup msetle_cancel |
261 simproc_setup msetle_cancel |
272 ("(l::'a::preorder multiset) + m \<le> n" | "(l::'a multiset) \<le> m + n" | |
262 ("(l::'a::preorder multiset) + m \<le> n" | "(l::'a multiset) \<le> m + n" | |
273 "add_mset a m \<le> n" | "m \<le> add_mset a n" | |
263 "add_mset a m \<le> n" | "m \<le> add_mset a n" | |
274 "replicate_mset p a \<le> n" | "m \<le> replicate_mset p a" | |
264 "replicate_mset p a \<le> n" | "m \<le> replicate_mset p a" | |
275 "repeat_mset p m \<le> n" | "m \<le> repeat_mset p n") = |
265 "repeat_mset p m \<le> n" | "m \<le> repeat_mset p n") = |
276 \<open>fn phi => Multiset_Order_Simprocs.le_cancel_msets\<close> |
266 \<open>fn phi => Cancel_Simprocs.less_eq_cancel\<close> |
277 |
267 |
278 |
268 |
279 subsection \<open>Additional facts and instantiations\<close> |
269 subsection \<open>Additional facts and instantiations\<close> |
280 |
270 |
281 lemma ex_gt_count_imp_le_multiset: |
271 lemma ex_gt_count_imp_le_multiset: |