added lemmas mult{,p}_mono_strong draft
authordesharna
Wed, 25 May 2022 13:06:29 +0200
changeset 75958 27745f72e3e1
parent 75957 8e2285baadba
added lemmas mult{,p}_mono_strong
NEWS
src/HOL/Library/Multiset.thy
--- a/NEWS	Wed May 25 10:57:07 2022 +0100
+++ b/NEWS	Wed May 25 13:06:29 2022 +0200
@@ -62,6 +62,8 @@
       filter_mset_cong
       filter_mset_cong0
       image_mset_filter_mset_swap
+      mult_mono_strong
+      multp_mono_strong
 
 * Sledgehammer:
   - Redesigned multithreading to provide more fine grained prover schedules.
--- a/src/HOL/Library/Multiset.thy	Wed May 25 10:57:07 2022 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed May 25 13:06:29 2022 +0200
@@ -3223,6 +3223,33 @@
   by (metis wfPUNIVI wfP_induct)
 
 
+subsubsection \<open>Monononicity\<close>
+
+lemma multp_mono_strong:
+  assumes "multp R M1 M2" and "transp R" and
+    S_if_R: "\<And>x y. x \<in> set_mset M1 \<Longrightarrow> y \<in> set_mset M2 \<Longrightarrow> R x y \<Longrightarrow> S x y"
+  shows "multp S M1 M2"
+proof -
+  obtain I J K where "M2 = I + J" and "M1 = I + K" and "J \<noteq> {#}" and "\<forall>k\<in>#K. \<exists>x\<in>#J. R k x"
+    using multp_implies_one_step[OF \<open>transp R\<close> \<open>multp R M1 M2\<close>] by auto
+  show ?thesis
+    unfolding \<open>M2 = I + J\<close> \<open>M1 = I + K\<close>
+  proof (rule one_step_implies_multp[OF \<open>J \<noteq> {#}\<close>])
+    show "\<forall>k\<in>#K. \<exists>j\<in>#J. S k j"
+      using S_if_R
+      by (metis \<open>M1 = I + K\<close> \<open>M2 = I + J\<close> \<open>\<forall>k\<in>#K. \<exists>x\<in>#J. R k x\<close> union_iff)
+  qed
+qed
+
+lemma mult_mono_strong:
+  assumes "(M1, M2) \<in> mult r" and "trans r" and
+    S_if_R: "\<And>x y. x \<in> set_mset M1 \<Longrightarrow> y \<in> set_mset M2 \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s"
+  shows "(M1, M2) \<in> mult s"
+  using assms multp_mono_strong[of "\<lambda>x y. (x, y) \<in> r" M1 M2 "\<lambda>x y. (x, y) \<in> s",
+      unfolded multp_def transp_trans_eq, simplified]
+  by blast
+
+
 subsection \<open>Quasi-executable version of the multiset extension\<close>
 
 text \<open>