--- 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>