added lemmas image_mset_image_mset_mem_multI and multp_image_mset_image_msetI draft
authordesharna
Mon, 16 May 2022 11:16:48 +0200
changeset 75943 23e03451f01f
parent 75939 d1417d9c6deb
added lemmas image_mset_image_mset_mem_multI and multp_image_mset_image_msetI
NEWS
src/HOL/Library/Multiset.thy
--- a/NEWS	Fri Apr 22 16:55:48 2022 +0200
+++ b/NEWS	Mon May 16 11:16:48 2022 +0200
@@ -53,6 +53,7 @@
     used for what is now called multp_code. Minor INCOMPATIBILITY.
   - Lifted multiple lemmas from mult to multp.
   - Redefined less_multiset to be based on multp. INCOMPATIBILITY.
+  - Added lemma image_mset_image_mset_mem_multI.
 
 * Sledgehammer:
   - Redesigned multithreading to provide more fine grained prover schedules.
--- a/src/HOL/Library/Multiset.thy	Fri Apr 22 16:55:48 2022 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon May 16 11:16:48 2022 +0200
@@ -2832,6 +2832,180 @@
 lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
   by (simp add: mult1_def)
 
+lemma image_mset_image_mset_mem_mult1I:
+  assumes
+    f_mono_wrt_r: "\<And>t u. (t, u) \<in> r \<Longrightarrow> (f t, f u) \<in> r" and
+    "(M1, M2) \<in> mult1 r"
+  shows "(image_mset f M1, image_mset f M2) \<in> mult1 r"
+proof -
+  from assms(2) obtain M0 a K where
+    M2_def: "M2 = M0 + {#a#}" and M1_def: "M1 = M0 + K" and "\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r"
+    unfolding mult1_def[of r]  by auto
+
+  have "image_mset f M1 = image_mset f M0 + image_mset f K" by (simp add: M1_def)
+  moreover have "image_mset f M2 = image_mset f M0 + {# (f a) #}" by (simp add: M2_def)
+  moreover have "b \<in># image_mset f K \<Longrightarrow> (b, f a) \<in> r" if "b \<in># image_mset f K" for b
+  proof -
+    from that obtain b' where b_def: "b = (f b')" and "b' \<in># K"
+      by auto
+    with \<open>\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r\<close> have "(b',a) \<in> r"
+      by auto
+    with f_mono_wrt_r b_def show "(b, f a) \<in> r"
+      by auto
+  qed
+  ultimately show ?thesis
+    by (metis add_mset_add_single mult1I)
+qed
+
+lemma image_mset_image_mset_mem_multI:
+  assumes f_mono_wrt_r: "\<And>t u. (t, u) \<in> r \<Longrightarrow> (f t, f u) \<in> r"
+  shows "(M1, M2) \<in> mult r \<Longrightarrow> (image_mset f M1, image_mset f M2) \<in> mult r"
+  unfolding mult_def
+proof (induction M2 rule: trancl_induct)
+  case (base x)
+  with f_mono_wrt_r have "(image_mset f M1, image_mset f x) \<in> mult1 r"
+    by (simp add: image_mset_image_mset_mem_mult1I)
+  thus "(image_mset f M1, image_mset f x) \<in> (mult1 r)\<^sup>+"
+    by simp
+next
+  case (step x z)
+  with f_mono_wrt_r have "(image_mset f x, image_mset f z) \<in> mult1 r"
+    by (simp add: image_mset_image_mset_mem_mult1I)
+  thus "(image_mset f M1, image_mset f z) \<in> (mult1 r)\<^sup>+"
+    using step.IH by simp
+qed
+
+lemma multp_image_mset_image_msetI:
+  assumes "\<And>t u. R t u \<Longrightarrow> R (f t) (f u)"
+  shows "multp R M1 M2 \<Longrightarrow> multp R (image_mset f M1) (image_mset f M2)"
+    using assms image_mset_image_mset_mem_multI[of "{(x, y). r x y}" for r,
+        folded multp_def, simplified]
+    by blast
+
+text \<open>Lemmas @{thm [source] image_mset_image_mset_mem_multI} and
+  @{thm [source] image_mset_image_mset_mem_multI} are from Nicolas Peltier's AFP/SuperCalc.\<close>
+
+lemma image_mset_eq_plusD:
+  "image_mset f M1 = M2 + M3 \<Longrightarrow>
+    \<exists>M2' M3'. M1 = M2' + M3' \<and> image_mset f M2' = M2 \<and> image_mset f M3' = M3"
+proof (induction M1 arbitrary: M2 M3)
+  case empty
+  thus ?case by simp
+next
+  case (add x M1)
+  show ?case
+  proof (cases "f x \<in># M2")
+    case True
+    with add.prems have "image_mset f M1 = (M2 - {#f x#}) + M3"
+      apply simp by (metis add_mset_remove_trivial)
+    thus ?thesis
+      using add.IH add.prems by force
+  next
+    case False
+    with add.prems have "image_mset f M1 = M2 + (M3 - {#f x#})"
+      apply simp
+      by (metis add_mset_remove_trivial diff_union_single_conv union_iff union_single_eq_member)
+    then show ?thesis
+      using add.IH add.prems by force
+  qed
+qed
+
+lemma image_mset_eq_image_mset_plusD:
+  assumes inj_f: "inj_on f (set_mset M1 \<union> set_mset M2)"
+  shows "image_mset f M1 = image_mset f M2 + M3 \<Longrightarrow>
+    \<exists>M3'. M1 = M2 + M3' \<and> image_mset f M3' = M3"
+  using inj_f
+proof (induction M1 arbitrary: M2 M3)
+  case empty
+  thus ?case by simp
+next
+  case (add x M1)
+  show ?case
+  proof (cases "x \<in># M2")
+    case True
+    with add.prems have "image_mset f M1 = image_mset f (M2 - {#x#}) + M3"
+      by (smt (verit, del_insts) add.left_commute add_cancel_right_left diff_union_cancelL
+          diff_union_single_conv image_mset_union union_mset_add_mset_left
+          union_mset_add_mset_right)
+    with add.IH have "\<exists>M3'. M1 = M2 - {#x#} + M3' \<and> image_mset f M3' = M3"
+      by (smt (verit, del_insts) True Un_insert_left Un_insert_right add.prems(2) inj_on_insert
+          insert_DiffM set_mset_add_mset_insert)
+    with True show ?thesis
+      by auto
+  next
+    case False
+    with add.prems(2) have "f x \<notin># image_mset f M2"
+      by auto
+    with add.prems(1) have "image_mset f M1 = image_mset f M2 + (M3 - {#f x#})"
+      by (metis (no_types, lifting) diff_union_single_conv image_eqI image_mset_Diff
+          image_mset_single mset_subset_eq_single set_image_mset union_iff union_single_eq_diff
+          union_single_eq_member)
+    with add.prems(2) add.IH have "\<exists>M3'. M1 = M2 + M3' \<and> image_mset f M3' = M3 - {#f x#}"
+      by auto
+    then show ?thesis
+      by (metis add.prems(1) add_diff_cancel_left' image_mset_Diff mset_subset_eq_add_left
+          union_mset_add_mset_right)
+  qed
+qed
+
+lemma image_mset_eq_add_mset_image_msetD: "inj_on f (set_mset M1 \<union> set_mset M2) \<Longrightarrow>
+  image_mset f M1 = add_mset x (image_mset f M2) \<Longrightarrow>
+  \<exists>M3'. M1 = M2 + M3' \<and> image_mset f M3' = {#x#}"
+  by (rule image_mset_eq_image_mset_plusD[of f M1 M2 "{#x#}", simplified])
+
+lemma image_mset_eq_singleton_iff: "image_mset f M = {#x#} \<longleftrightarrow> (\<exists>x'. M = {#x'#} \<and> f x' = x)"
+  by (metis One_nat_def add_mset_add_single diff_add_zero image_mset_single insert_noteq_member
+      multi_drop_mem_not_eq size_1_singleton_mset size_add_mset size_empty size_image_mset)
+
+lemma image_mset_image_mset_mem_mult1D:
+  assumes
+    f_mono_wrt_r: "\<And>t u. (f t, f u) \<in> r \<Longrightarrow> (t, u) \<in> r" and
+    f_inj_on: "inj_on f (set_mset M1 \<union> set_mset M2)" and
+    "(image_mset f M1, image_mset f M2) \<in> mult1 r"
+  shows "(M1, M2) \<in> mult1 r"
+proof -
+  from assms(3) obtain M0 a K where
+    image_mset_f_M1_def: "image_mset f M1 = M0 + K" and
+    image_mset_f_M2_def: "image_mset f M2 = M0 + {#a#}" and
+    "\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r"
+    unfolding mult1_def[of r] by auto
+
+  from image_mset_f_M1_def obtain M0' K' where
+    M1_def: "M1 = M0' + K'" and M0_def: "M0 = image_mset f M0'" and K_def: "K = image_mset f K'"
+    by (auto dest: image_mset_eq_plusD)
+
+  have inj_f': "inj_on f (set_mset M2 \<union> set_mset M0')"
+  proof (rule inj_on_subset[OF f_inj_on])
+    show "set_mset M2 \<union> set_mset M0' \<subseteq> set_mset M1 \<union> set_mset M2"
+      by (auto simp: M1_def)
+  qed
+
+  from image_mset_f_M2_def obtain a' where
+    M2_def: "M2 = add_mset a' M0'" and a_def: "a = f a'"
+    by (auto simp: M0_def image_mset_eq_singleton_iff
+        dest!: image_mset_eq_add_mset_image_msetD[OF inj_f'])
+
+  show ?thesis
+  proof (rule mult1I)
+    show "M1 = M0' + K'"
+      by (rule M1_def)
+  next
+    show "M2 = add_mset a' M0'"
+      by (rule M2_def)
+  next
+    show "\<And>b. b \<in># K' \<Longrightarrow> (b, a') \<in> r"
+      using K_def \<open>\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r\<close> a_def f_mono_wrt_r by auto
+  qed
+qed
+
+lemma image_mset_image_mset_mem_multD:
+  assumes
+    f_mono_wrt_r: "\<And>t u. (f t, f u) \<in> r \<Longrightarrow> (t, u) \<in> r" and
+    f_inj_on: "inj_on f (set_mset M1 \<union> set_mset M2)" and
+    "(image_mset f M1, image_mset f M2) \<in> mult r"
+  shows "(M1, M2) \<in> mult r"
+  sorry
+
 
 subsubsection \<open>Well-foundedness\<close>