(* Title: Well-Quasi-Orders Author: Christian Sternagel <c.sternagel@gmail.com> Maintainer: Christian Sternagel License: LGPL *) section ‹Multiset Extension of Orders (as Binary Predicates)› (*TODO: move theory (and maybe rename)*) theory Multiset_Extension imports Open_Induction.Restricted_Predicates "HOL-Library.Multiset" begin definition multisets :: "'a set ⇒ 'a multiset set" where "multisets A = {M. set_mset M ⊆ A}" lemma in_multisets_iff: "M ∈ multisets A ⟷ set_mset M ⊆ A" by (simp add: multisets_def) lemma empty_multisets [simp]: "{#} ∈ multisets F" by (simp add: in_multisets_iff) lemma multisets_union [simp]: "M ∈ multisets A ⟹ N ∈ multisets A ⟹ M + N ∈ multisets A" by (auto simp add: in_multisets_iff) definition mulex1 :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where "mulex1 P = (λM N. (M, N) ∈ mult1 {(x, y). P x y})" lemma mulex1_empty [iff]: "mulex1 P M {#} ⟷ False" using not_less_empty [of M "{(x, y). P x y}"] by (auto simp: mulex1_def) lemma mulex1_add: "mulex1 P N (M0 + {#a#}) ⟹ (∃M. mulex1 P M M0 ∧ N = M + {#a#}) ∨ (∃K. (∀b. b ∈# K ⟶ P b a) ∧ N = M0 + K)" using less_add [of N a M0 "{(x, y). P x y}"] by (auto simp: mulex1_def) lemma mulex1_self_add_right [simp]: "mulex1 P A (add_mset a A)" proof - let ?R = "{(x, y). P x y}" thm mult1_def have "A + {#a#} = A + {#a#}" by simp moreover have "A = A + {#}" by simp moreover have "∀b. b ∈# {#} ⟶ (b, a) ∈ ?R" by simp ultimately have "(A, add_mset a A) ∈ mult1 ?R" unfolding mult1_def by blast then show ?thesis by (simp add: mulex1_def) qed lemma empty_mult1 [simp]: "({#}, {#a#}) ∈ mult1 R" proof - have "{#a#} = {#} + {#a#}" by simp moreover have "{#} = {#} + {#}" by simp moreover have "∀b. b ∈# {#} ⟶ (b, a) ∈ R" by simp ultimately show ?thesis unfolding mult1_def by force qed lemma empty_mulex1 [simp]: "mulex1 P {#} {#a#}" using empty_mult1 [of a "{(x, y). P x y}"] by (simp add: mulex1_def) definition mulex_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where "mulex_on P A = (restrict_to (mulex1 P) (multisets A))⇧^{+}⇧^{+}" abbreviation mulex :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where "mulex P ≡ mulex_on P UNIV" lemma mulex_on_induct [consumes 1, case_names base step, induct pred: mulex_on]: assumes "mulex_on P A M N" and "⋀M N. ⟦M ∈ multisets A; N ∈ multisets A; mulex1 P M N⟧ ⟹ Q M N" and "⋀L M N. ⟦mulex_on P A L M; Q L M; N ∈ multisets A; mulex1 P M N⟧ ⟹ Q L N" shows "Q M N" using assms unfolding mulex_on_def by (induct) blast+ lemma mulex_on_self_add_singleton_right [simp]: assumes "a ∈ A" and "M ∈ multisets A" shows "mulex_on P A M (add_mset a M)" proof - have "mulex1 P M (M + {#a#})" by simp with assms have "restrict_to (mulex1 P) (multisets A) M (add_mset a M)" by (auto simp: multisets_def) then show ?thesis unfolding mulex_on_def by blast qed lemma singleton_multisets [iff]: "{#x#} ∈ multisets A ⟷ x ∈ A" by (auto simp: multisets_def) lemma union_multisetsD: assumes "M + N ∈ multisets A" shows "M ∈ multisets A ∧ N ∈ multisets A" using assms by (auto simp: multisets_def) lemma mulex_on_multisetsD [dest]: assumes "mulex_on P F M N" shows "M ∈ multisets F" and "N ∈ multisets F" using assms by (induct) auto lemma union_multisets_iff [iff]: "M + N ∈ multisets A ⟷ M ∈ multisets A ∧ N ∈ multisets A" by (auto dest: union_multisetsD) lemma add_mset_multisets_iff [iff]: "add_mset a M ∈ multisets A ⟷ a ∈ A ∧ M ∈ multisets A" unfolding add_mset_add_single[of a M] union_multisets_iff by auto lemma mulex_on_trans: "mulex_on P A L M ⟹ mulex_on P A M N ⟹ mulex_on P A L N" by (auto simp: mulex_on_def) lemma transp_on_mulex_on: "transp_on B (mulex_on P A)" using mulex_on_trans [of P A] by (auto simp: transp_on_def) lemma mulex_on_add_right [simp]: assumes "mulex_on P A M N" and "a ∈ A" shows "mulex_on P A M (add_mset a N)" proof - from assms have "a ∈ A" and "N ∈ multisets A" by auto then have "mulex_on P A N (add_mset a N)" by simp with ‹mulex_on P A M N› show ?thesis by (rule mulex_on_trans) qed lemma empty_mulex_on [simp]: assumes "M ≠ {#}" and "M ∈ multisets A" shows "mulex_on P A {#} M" using assms proof (induct M) case (add a M) show ?case proof (cases "M = {#}") assume "M = {#}" with add show ?thesis by (auto simp: mulex_on_def) next assume "M ≠ {#}" with add show ?thesis by (auto intro: mulex_on_trans) qed qed simp lemma mulex_on_self_add_right [simp]: assumes "M ∈ multisets A" and "K ∈ multisets A" and "K ≠ {#}" shows "mulex_on P A M (M + K)" using assms proof (induct K) case empty then show ?case by (cases "K = {#}") auto next case (add a M) show ?case proof (cases "M = {#}") assume "M = {#}" with add show ?thesis by auto next assume "M ≠ {#}" with add show ?thesis by (auto dest: mulex_on_add_right simp add: ac_simps) qed qed lemma mult1_singleton [iff]: "({#x#}, {#y#}) ∈ mult1 R ⟷ (x, y) ∈ R" proof assume "(x, y) ∈ R" then have "{#y#} = {#} + {#y#}" and "{#x#} = {#} + {#x#}" and "∀b. b ∈# {#x#} ⟶ (b, y) ∈ R" by auto then show "({#x#}, {#y#}) ∈ mult1 R" unfolding mult1_def by blast next assume "({#x#}, {#y#}) ∈ mult1 R" then obtain M0 K a where "{#y#} = add_mset a M0" and "{#x#} = M0 + K" and "∀b. b ∈# K ⟶ (b, a) ∈ R" unfolding mult1_def by blast then show "(x, y) ∈ R" by (auto simp: add_eq_conv_diff) qed lemma mulex1_singleton [iff]: "mulex1 P {#x#} {#y#} ⟷ P x y" using mult1_singleton [of x y "{(x, y). P x y}"] by (simp add: mulex1_def) lemma singleton_mulex_onI: "P x y ⟹ x ∈ A ⟹ y ∈ A ⟹ mulex_on P A {#x#} {#y#}" by (auto simp: mulex_on_def) lemma reflclp_mulex_on_add_right [simp]: assumes "(mulex_on P A)⇧^{=}⇧^{=}M N" and "M ∈ multisets A" and "a ∈ A" shows "mulex_on P A M (N + {#a#})" using assms by (cases "M = N") simp_all lemma reflclp_mulex_on_add_right' [simp]: assumes "(mulex_on P A)⇧^{=}⇧^{=}M N" and "M ∈ multisets A" and "a ∈ A" shows "mulex_on P A M ({#a#} + N)" using reflclp_mulex_on_add_right [OF assms] by (simp add: ac_simps) lemma mulex_on_union_right [simp]: assumes "mulex_on P F A B" and "K ∈ multisets F" shows "mulex_on P F A (K + B)" using assms proof (induct K) case (add a K) then have "a ∈ F" and "mulex_on P F A (B + K)" by (auto simp: multisets_def ac_simps) then have "mulex_on P F A ((B + K) + {#a#})" by simp then show ?case by (simp add: ac_simps) qed simp lemma mulex_on_union_right' [simp]: assumes "mulex_on P F A B" and "K ∈ multisets F" shows "mulex_on P F A (B + K)" using mulex_on_union_right [OF assms] by (simp add: ac_simps) text ‹Adapted from @{thm all_accessible} in @{theory "HOL-Library.Multiset"}.› lemma accessible_on_mulex1_multisets: assumes wf: "wfp_on P A" shows "∀M∈multisets A. accessible_on (mulex1 P) (multisets A) M" proof let ?P = "mulex1 P" let ?A = "multisets A" let ?acc = "accessible_on ?P ?A" { fix M M0 a assume M0: "?acc M0" and "a ∈ A" and "M0 ∈ ?A" and wf_hyp: "⋀b. ⟦b ∈ A; P b a⟧ ⟹ (∀M. ?acc (M) ⟶ ?acc (M + {#b#}))" and acc_hyp: "∀M. M ∈ ?A ∧ ?P M M0 ⟶ ?acc (M + {#a#})" then have "add_mset a M0 ∈ ?A" by (auto simp: multisets_def) then have "?acc (add_mset a M0)" proof (rule accessible_onI [of "add_mset a M0"]) fix N assume "N ∈ ?A" and "?P N (add_mset a M0)" then have "((∃M. M ∈ ?A ∧ ?P M M0 ∧ N = M + {#a#}) ∨ (∃K. (∀b. b ∈# K ⟶ P b a) ∧ N = M0 + K))" using mulex1_add [of P N M0 a] by (auto simp: multisets_def) then show "?acc (N)" proof (elim exE disjE conjE) fix M assume "M ∈ ?A" and "?P M M0" and N: "N = M + {#a#}" from acc_hyp have "M ∈ ?A ∧ ?P M M0 ⟶ ?acc (M + {#a#})" .. with ‹M ∈ ?A› and ‹?P M M0› have "?acc (M + {#a#})" by blast then show "?acc (N)" by (simp only: N) next fix K assume N: "N = M0 + K" assume "∀b. b ∈# K ⟶ P b a" moreover from N and ‹N ∈ ?A› have "K ∈ ?A" by (auto simp: multisets_def) ultimately have "?acc (M0 + K)" proof (induct K) case empty from M0 show "?acc (M0 + {#})" by simp next case (add x K) from add.prems have "x ∈ A" and "P x a" by (auto simp: multisets_def) with wf_hyp have "∀M. ?acc M ⟶ ?acc (M + {#x#})" by blast moreover from add have "?acc (M0 + K)" by (auto simp: multisets_def) ultimately show "?acc (M0 + (add_mset x K))" by simp qed then show "?acc N" by (simp only: N) qed qed } note tedious_reasoning = this fix M assume "M ∈ ?A" then show "?acc M" proof (induct M) show "?acc {#}" proof (rule accessible_onI) show "{#} ∈ ?A" by (auto simp: multisets_def) next fix b assume "?P b {#}" then show "?acc b" by simp qed next case (add a M) then have "?acc M" by (auto simp: multisets_def) from add have "a ∈ A" by (auto simp: multisets_def) with wf have "∀M. ?acc M ⟶ ?acc (add_mset a M)" proof (induct) case (less a) then have r: "⋀b. ⟦b ∈ A; P b a⟧ ⟹ (∀M. ?acc M ⟶ ?acc (M + {#b#}))" by auto show "∀M. ?acc M ⟶ ?acc (add_mset a M)" proof (intro allI impI) fix M' assume "?acc M'" moreover then have "M' ∈ ?A" by (blast dest: accessible_on_imp_mem) ultimately show "?acc (add_mset a M')" by (induct) (rule tedious_reasoning [OF _ ‹a ∈ A› _ r], auto) qed qed with ‹?acc (M)› show "?acc (add_mset a M)" by blast qed qed lemmas wfp_on_mulex1_multisets = accessible_on_mulex1_multisets [THEN accessible_on_imp_wfp_on] lemmas irreflp_on_mulex1 = wfp_on_mulex1_multisets [THEN wfp_on_imp_irreflp_on] lemma wfp_on_mulex_on_multisets: assumes "wfp_on P A" shows "wfp_on (mulex_on P A) (multisets A)" using wfp_on_mulex1_multisets [OF assms] by (simp only: mulex_on_def wfp_on_restrict_to_tranclp_wfp_on_conv) lemmas irreflp_on_mulex_on = wfp_on_mulex_on_multisets [THEN wfp_on_imp_irreflp_on] lemma mulex1_union: "mulex1 P M N ⟹ mulex1 P (K + M) (K + N)" by (auto simp: mulex1_def mult1_union) lemma mulex_on_union: assumes "mulex_on P A M N" and "K ∈ multisets A" shows "mulex_on P A (K + M) (K + N)" using assms proof (induct) case (base M N) then have "mulex1 P (K + M) (K + N)" by (blast dest: mulex1_union) moreover from base have "(K + M) ∈ multisets A" and "(K + N) ∈ multisets A" by (auto simp: multisets_def) ultimately have "restrict_to (mulex1 P) (multisets A) (K + M) (K + N)" by auto then show ?case by (auto simp: mulex_on_def) next case (step L M N) then have "mulex1 P (K + M) (K + N)" by (blast dest: mulex1_union) moreover from step have "(K + M) ∈ multisets A" and "(K + N) ∈ multisets A" by blast+ ultimately have "(restrict_to (mulex1 P) (multisets A))⇧^{+}⇧^{+}(K + M) (K + N)" by auto moreover have "mulex_on P A (K + L) (K + M)" using step by blast ultimately show ?case by (auto simp: mulex_on_def) qed lemma mulex_on_union': assumes "mulex_on P A M N" and "K ∈ multisets A" shows "mulex_on P A (M + K) (N + K)" using mulex_on_union [OF assms] by (simp add: ac_simps) lemma mulex_on_add_mset: assumes "mulex_on P A M N" and "m ∈ A" shows "mulex_on P A (add_mset m M) (add_mset m N)" unfolding add_mset_add_single[of m M] add_mset_add_single[of m N] apply (rule mulex_on_union') using assms by auto lemma union_mulex_on_mono: "mulex_on P F A C ⟹ mulex_on P F B D ⟹ mulex_on P F (A + B) (C + D)" by (metis mulex_on_multisetsD mulex_on_trans mulex_on_union mulex_on_union') lemma mulex_on_add_mset': assumes "P m n" and "m ∈ A" and "n ∈ A" and "M ∈ multisets A" shows "mulex_on P A (add_mset m M) (add_mset n M)" unfolding add_mset_add_single[of m M] add_mset_add_single[of n M] apply (rule mulex_on_union) using assms by (auto simp: mulex_on_def) lemma mulex_on_add_mset_mono: assumes "P m n" and "m ∈ A" and "n ∈ A" and "mulex_on P A M N" shows "mulex_on P A (add_mset m M) (add_mset n N)" unfolding add_mset_add_single[of m M] add_mset_add_single[of n N] apply (rule union_mulex_on_mono) using assms by (auto simp: mulex_on_def) lemma union_mulex_on_mono1: "A ∈ multisets F ⟹ (mulex_on P F)⇧^{=}⇧^{=}A C ⟹ mulex_on P F B D ⟹ mulex_on P F (A + B) (C + D)" by (auto intro: union_mulex_on_mono mulex_on_union) lemma union_mulex_on_mono2: "B ∈ multisets F ⟹ mulex_on P F A C ⟹ (mulex_on P F)⇧^{=}⇧^{=}B D ⟹ mulex_on P F (A + B) (C + D)" by (auto intro: union_mulex_on_mono mulex_on_union') lemma mult1_mono: assumes "⋀x y. ⟦x ∈ A; y ∈ A; (x, y) ∈ R⟧ ⟹ (x, y) ∈ S" and "M ∈ multisets A" and "N ∈ multisets A" and "(M, N) ∈ mult1 R" shows "(M, N) ∈ mult1 S" using assms unfolding mult1_def multisets_def by auto (metis (full_types) subsetD) lemma mulex1_mono: assumes "⋀x y. ⟦x ∈ A; y ∈ A; P x y⟧ ⟹ Q x y" and "M ∈ multisets A" and "N ∈ multisets A" and "mulex1 P M N" shows "mulex1 Q M N" using mult1_mono [of A "{(x, y). P x y}" "{(x, y). Q x y}" M N] and assms unfolding mulex1_def by blast lemma mulex_on_mono: assumes *: "⋀x y. ⟦x ∈ A; y ∈ A; P x y⟧ ⟹ Q x y" and "mulex_on P A M N" shows "mulex_on Q A M N" proof - let ?rel = "λP. (restrict_to (mulex1 P) (multisets A))" from ‹mulex_on P A M N› have "(?rel P)⇧^{+}⇧^{+}M N" by (simp add: mulex_on_def) then have "(?rel Q)⇧^{+}⇧^{+}M N" proof (induct rule: tranclp.induct) case (r_into_trancl M N) then have "M ∈ multisets A" and "N ∈ multisets A" by auto from mulex1_mono [OF * this] and r_into_trancl show ?case by auto next case (trancl_into_trancl L M N) then have "M ∈ multisets A" and "N ∈ multisets A" by auto from mulex1_mono [OF * this] and trancl_into_trancl have "?rel Q M N" by auto with ‹(?rel Q)⇧^{+}⇧^{+}L M› show ?case by (rule tranclp.trancl_into_trancl) qed then show ?thesis by (simp add: mulex_on_def) qed lemma mult1_reflcl: assumes "(M, N) ∈ mult1 R" shows "(M, N) ∈ mult1 (R⇧^{=})" using assms by (auto simp: mult1_def) lemma mulex1_reflclp: assumes "mulex1 P M N" shows "mulex1 (P⇧^{=}⇧^{=}) M N" using mulex1_mono [of UNIV P "P⇧^{=}⇧^{=}" M N, OF _ _ _ assms] by (auto simp: multisets_def) lemma mulex_on_reflclp: assumes "mulex_on P A M N" shows "mulex_on (P⇧^{=}⇧^{=}) A M N" using mulex_on_mono [OF _ assms, of "P⇧^{=}⇧^{=}"] by auto lemma surj_on_multisets_mset: "∀M∈multisets A. ∃xs∈lists A. M = mset xs" proof fix M assume "M ∈ multisets A" then show "∃xs∈lists A. M = mset xs" proof (induct M) case empty show ?case by simp next case (add a M) then obtain xs where "xs ∈ lists A" and "M = mset xs" by auto then have "add_mset a M = mset (a # xs)" by simp moreover have "a # xs ∈ lists A" using ‹xs ∈ lists A› and add by auto ultimately show ?case by blast qed qed lemma image_mset_lists [simp]: "mset ` lists A = multisets A" using surj_on_multisets_mset [of A] by auto (metis mem_Collect_eq multisets_def set_mset_mset subsetI) lemma multisets_UNIV [simp]: "multisets UNIV = UNIV" by (metis image_mset_lists lists_UNIV surj_mset) lemma non_empty_multiset_induct [consumes 1, case_names singleton add]: assumes "M ≠ {#}" and "⋀x. P {#x#}" and "⋀x M. P M ⟹ P (add_mset x M)" shows "P M" using assms by (induct M) auto lemma mulex_on_all_strict: assumes "X ≠ {#}" assumes "X ∈ multisets A" and "Y ∈ multisets A" and *: "∀y. y ∈# Y ⟶ (∃x. x ∈# X ∧ P y x)" shows "mulex_on P A Y X" using assms proof (induction X arbitrary: Y rule: non_empty_multiset_induct) case (singleton x) then have "mulex1 P Y {#x#}" unfolding mulex1_def mult1_def by auto with singleton show ?case by (auto simp: mulex_on_def) next case (add x M) let ?Y = "{# y ∈# Y. ∃x. x ∈# M ∧ P y x #}" let ?Z = "Y - ?Y" have Y: "Y = ?Z + ?Y" by (subst multiset_eq_iff) auto from ‹Y ∈ multisets A› have "?Y ∈ multisets A" by (metis multiset_partition union_multisets_iff) moreover have "∀y. y ∈# ?Y ⟶ (∃x. x ∈# M ∧ P y x)" by auto moreover have "M ∈ multisets A" using add by auto ultimately have "mulex_on P A ?Y M" using add by blast moreover have "mulex_on P A ?Z {#x#}" proof - have "{#x#} = {#} + {#x#}" by simp moreover have "?Z = {#} + ?Z" by simp moreover have "∀y. y ∈# ?Z ⟶ P y x" using add.prems by (auto simp add: in_diff_count split: if_splits) ultimately have "mulex1 P ?Z {#x#}" unfolding mulex1_def mult1_def by blast moreover have "{#x#} ∈ multisets A" using add.prems by auto moreover have "?Z ∈ multisets A" using ‹Y ∈ multisets A› by (metis diff_union_cancelL multiset_partition union_multisetsD) ultimately show ?thesis by (auto simp: mulex_on_def) qed ultimately have "mulex_on P A (?Y + ?Z) (M + {#x#})" by (rule union_mulex_on_mono) then show ?case using Y by (simp add: ac_simps) qed text ‹The following lemma shows that the textbook definition (e.g., ``Term Rewriting and All That'') is the same as the one used below.› lemma diff_set_Ex_iff: "X ≠ {#} ∧ X ⊆# M ∧ N = (M - X) + Y ⟷ X ≠ {#} ∧ (∃Z. M = Z + X ∧ N = Z + Y)" by (auto) (metis add_diff_cancel_left' multiset_diff_union_assoc union_commute) text ‹Show that @{const mulex_on} is equivalent to the textbook definition of multiset-extension for transitive base orders.› lemma mulex_on_alt_def: assumes trans: "transp_on A P" shows "mulex_on P A M N ⟷ M ∈ multisets A ∧ N ∈ multisets A ∧ (∃X Y Z. X ≠ {#} ∧ N = Z + X ∧ M = Z + Y ∧ (∀y. y ∈# Y ⟶ (∃x. x ∈# X ∧ P y x)))" (is "?P M N ⟷ ?Q M N") proof assume "?P M N" then show "?Q M N" proof (induct M N) case (base M N) then obtain a M0 K where N: "N = M0 + {#a#}" and M: "M = M0 + K" and *: "∀b. b ∈# K ⟶ P b a" and "M ∈ multisets A" and "N ∈ multisets A" by (auto simp: mulex1_def mult1_def) moreover then have "{#a#} ∈ multisets A" and "K ∈ multisets A" by auto moreover have "{#a#} ≠ {#}" by auto moreover have "N = M0 + {#a#}" by fact moreover have "M = M0 + K" by fact moreover have "∀y. y ∈# K ⟶ (∃x. x ∈# {#a#} ∧ P y x)" using * by auto ultimately show ?case by blast next case (step L M N) then obtain X Y Z where "L ∈ multisets A" and "M ∈ multisets A" and "N ∈ multisets A" and "X ∈ multisets A" and "Y ∈ multisets A" and M: "M = Z + X" and L: "L = Z + Y" and "X ≠ {#}" and Y: "∀y. y ∈# Y ⟶ (∃x. x ∈# X ∧ P y x)" and "mulex1 P M N" by blast from ‹mulex1 P M N› obtain a M0 K where N: "N = add_mset a M0" and M': "M = M0 + K" and *: "∀b. b ∈# K ⟶ P b a" unfolding mulex1_def mult1_def by blast have L': "L = (M - X) + Y" by (simp add: L M) have K: "∀y. y ∈# K ⟶ (∃x. x ∈# {#a#} ∧ P y x)" using * by auto txt ‹The remainder of the proof is adapted from the proof of Lemma 2.5.4. of the book ``Term Rewriting and All That.''› let ?X = "add_mset a (X - K)" let ?Y = "(K - X) + Y" have "L ∈ multisets A" and "N ∈ multisets A" by fact+ moreover have "?X ≠ {#} ∧ (∃Z. N = Z + ?X ∧ L = Z + ?Y)" proof - have "?X ≠ {#}" by auto moreover have "?X ⊆# N" using M N M' by (simp add: add.commute [of "{#a#}"]) (metis Multiset.diff_subset_eq_self add.commute add_diff_cancel_right) moreover have "L = (N - ?X) + ?Y" proof (rule multiset_eqI) fix x :: 'a let ?c = "λM. count M x" let ?ic = "λx. int (?c x)" from ‹?X ⊆# N› have *: "?c {#a#} + ?c (X - K) ≤ ?c N" by (auto simp add: subseteq_mset_def split: if_splits) from * have **: "?c (X - K) ≤ ?c M0" unfolding N by (auto split: if_splits) have "?ic (N - ?X + ?Y) = int (?c N - ?c ?X) + ?ic ?Y" by simp also have "… = int (?c N - (?c {#a#} + ?c (X - K))) + ?ic (K - X) + ?ic Y" by simp also have "… = ?ic N - (?ic {#a#} + ?ic (X - K)) + ?ic (K - X) + ?ic Y" using of_nat_diff [OF *] by simp also have "… = (?ic N - ?ic {#a#}) - ?ic (X - K) + ?ic (K - X) + ?ic Y" by simp also have "… = (?ic N - ?ic {#a#}) + (?ic (K - X) - ?ic (X - K)) + ?ic Y" by simp also have "… = (?ic N - ?ic {#a#}) + (?ic K - ?ic X) + ?ic Y" by simp also have "… = (?ic N - ?ic ?X) + ?ic ?Y" by (simp add: N) also have "… = ?ic L" unfolding L' M' N using ** by (simp add: algebra_simps) finally show "?c L = ?c (N - ?X + ?Y)" by simp qed ultimately show ?thesis by (metis diff_set_Ex_iff) qed moreover have "∀y. y ∈# ?Y ⟶ (∃x. x ∈# ?X ∧ P y x)" proof (intro allI impI) fix y assume "y ∈# ?Y" then have "y ∈# K - X ∨ y ∈# Y" by auto then show "∃x. x ∈# ?X ∧ P y x" proof assume "y ∈# K - X" then have "y ∈# K" by (rule in_diffD) with K show ?thesis by auto next assume "y ∈# Y" with Y obtain x where "x ∈# X" and "P y x" by blast { assume "x ∈# X - K" with ‹P y x› have ?thesis by auto } moreover { assume "x ∈# K" with * have "P x a" by auto moreover have "y ∈ A" using ‹Y ∈ multisets A› and ‹y ∈# Y› by (auto simp: multisets_def) moreover have "a ∈ A" using ‹N ∈ multisets A› by (auto simp: N) moreover have "x ∈ A" using ‹M ∈ multisets A› and ‹x ∈# K› by (auto simp: M' multisets_def) ultimately have "P y a" using ‹P y x› and trans unfolding transp_on_def by blast then have ?thesis by force } moreover from ‹x ∈# X› have "x ∈# X - K ∨ x ∈# K" by (auto simp add: in_diff_count not_in_iff) ultimately show ?thesis by auto qed qed ultimately show ?case by blast qed next assume "?Q M N" then obtain X Y Z where "M ∈ multisets A" and "N ∈ multisets A" and "X ≠ {#}" and N: "N = Z + X" and M: "M = Z + Y" and *: "∀y. y ∈# Y ⟶ (∃x. x ∈# X ∧ P y x)" by blast with mulex_on_all_strict [of X A Y] have "mulex_on P A Y X" by auto moreover from ‹N ∈ multisets A› have "Z ∈ multisets A" by (auto simp: N) ultimately show "?P M N" unfolding M N by (metis mulex_on_union) qed end