190 show "\<forall>k\<in>#K. \<exists>x\<in>#J. R k x" |
190 show "\<forall>k\<in>#K. \<exists>x\<in>#J. R k x" |
191 using \<open>multp\<^sub>H\<^sub>O R A B\<close> |
191 using \<open>multp\<^sub>H\<^sub>O R A B\<close> |
192 by (metis J_def K_def in_diff_count multp\<^sub>H\<^sub>O_def) |
192 by (metis J_def K_def in_diff_count multp\<^sub>H\<^sub>O_def) |
193 qed |
193 qed |
194 |
194 |
|
195 lemma multp\<^sub>H\<^sub>O_minus_inter_minus_inter_iff: |
|
196 fixes M1 M2 :: "_ multiset" |
|
197 shows "multp\<^sub>H\<^sub>O R (M1 - M2) (M2 - M1) \<longleftrightarrow> multp\<^sub>H\<^sub>O R M1 M2" |
|
198 by (metis diff_intersect_left_idem multiset_inter_commute multp\<^sub>H\<^sub>O_plus_plus |
|
199 subset_mset.add_diff_inverse subset_mset.inf.cobounded1) |
|
200 |
|
201 lemma multp\<^sub>H\<^sub>O_iff_set_mset_less\<^sub>H\<^sub>O_set_mset: |
|
202 "multp\<^sub>H\<^sub>O R M1 M2 \<longleftrightarrow> (set_mset (M1 - M2) \<noteq> set_mset (M2 - M1) \<and> |
|
203 (\<forall>y \<in># M1 - M2. (\<exists>x \<in># M2 - M1. R y x)))" |
|
204 unfolding multp\<^sub>H\<^sub>O_minus_inter_minus_inter_iff[of R M1 M2, symmetric] |
|
205 unfolding multp\<^sub>H\<^sub>O_def |
|
206 unfolding count_minus_inter_lt_count_minus_inter_iff |
|
207 unfolding minus_inter_eq_minus_inter_iff |
|
208 by auto |
|
209 |
195 |
210 |
196 subsubsection \<open>Monotonicity\<close> |
211 subsubsection \<open>Monotonicity\<close> |
197 |
212 |
198 lemma multp\<^sub>D\<^sub>M_mono_strong: |
213 lemma multp\<^sub>D\<^sub>M_mono_strong: |
199 "multp\<^sub>D\<^sub>M R M1 M2 \<Longrightarrow> (\<And>x y. x \<in># M1 \<Longrightarrow> y \<in># M2 \<Longrightarrow> R x y \<Longrightarrow> S x y) \<Longrightarrow> multp\<^sub>D\<^sub>M S M1 M2" |
214 "multp\<^sub>D\<^sub>M R M1 M2 \<Longrightarrow> (\<And>x y. x \<in># M1 \<Longrightarrow> y \<in># M2 \<Longrightarrow> R x y \<Longrightarrow> S x y) \<Longrightarrow> multp\<^sub>D\<^sub>M S M1 M2" |