diff --git a/thys/Nested_Multisets_Ordinals/Signed_Multiset.thy b/thys/Nested_Multisets_Ordinals/Signed_Multiset.thy --- a/thys/Nested_Multisets_Ordinals/Signed_Multiset.thy +++ b/thys/Nested_Multisets_Ordinals/Signed_Multiset.thy @@ -1,878 +1,883 @@ (* Title: Signed (Finite) Multisets Author: Jasmin Blanchette , 2016 Maintainer: Jasmin Blanchette *) section \Signed (Finite) Multisets\ theory Signed_Multiset imports Multiset_More abbrevs "!z" = "\<^sub>z" begin +unbundle multiset.lifting + subsection \Definition of Signed Multisets\ definition equiv_zmset :: "'a multiset \ 'a multiset \ 'a multiset \ 'a multiset \ bool" where "equiv_zmset = (\(Mp, Mn) (Np, Nn). Mp + Nn = Np + Mn)" quotient_type 'a zmultiset = "'a multiset \ 'a multiset" / equiv_zmset by (rule equivpI, simp_all add: equiv_zmset_def reflp_def symp_def transp_def) (metis multi_union_self_other_eq union_lcomm) subsection \Basic Operations on Signed Multisets\ instantiation zmultiset :: (type) cancel_comm_monoid_add begin lift_definition zero_zmultiset :: "'a zmultiset" is "({#}, {#})" . abbreviation empty_zmset :: "'a zmultiset" ("{#}\<^sub>z") where "empty_zmset \ 0" lift_definition minus_zmultiset :: "'a zmultiset \ 'a zmultiset \ 'a zmultiset" is "\(Mp, Mn) (Np, Nn). (Mp + Nn, Mn + Np)" by (auto simp: equiv_zmset_def union_commute union_lcomm) lift_definition plus_zmultiset :: "'a zmultiset \ 'a zmultiset \ 'a zmultiset" is "\(Mp, Mn) (Np, Nn). (Mp + Np, Mn + Nn)" by (auto simp: equiv_zmset_def union_commute union_lcomm) instance by (intro_classes; transfer) (auto simp: equiv_zmset_def) end instantiation zmultiset :: (type) group_add begin lift_definition uminus_zmultiset :: "'a zmultiset \ 'a zmultiset" is "\(Mp, Mn). (Mn, Mp)" by (auto simp: equiv_zmset_def add.commute) instance by (intro_classes; transfer) (auto simp: equiv_zmset_def) end lift_definition zcount :: "'a zmultiset \ 'a \ int" is "\(Mp, Mn) x. int (count Mp x) - int (count Mn x)" by (auto simp del: of_nat_add simp: equiv_zmset_def fun_eq_iff multiset_eq_iff diff_eq_eq diff_add_eq eq_diff_eq of_nat_add[symmetric]) lemma zcount_inject: "zcount M = zcount N \ M = N" by transfer (auto simp del: of_nat_add simp: equiv_zmset_def fun_eq_iff multiset_eq_iff diff_eq_eq diff_add_eq eq_diff_eq of_nat_add[symmetric]) lemma zmultiset_eq_iff: "M = N \ (\a. zcount M a = zcount N a)" by (simp only: zcount_inject[symmetric] fun_eq_iff) lemma zmultiset_eqI: "(\x. zcount A x = zcount B x) \ A = B" using zmultiset_eq_iff by auto lemma zcount_uminus[simp]: "zcount (- A) x = - zcount A x" by transfer auto lift_definition add_zmset :: "'a \ 'a zmultiset \ 'a zmultiset" is "\x (Mp, Mn). (add_mset x Mp, Mn)" by (auto simp: equiv_zmset_def) syntax "_zmultiset" :: "args \ 'a zmultiset" ("{#(_)#}\<^sub>z") translations "{#x, xs#}\<^sub>z" == "CONST add_zmset x {#xs#}\<^sub>z" "{#x#}\<^sub>z" == "CONST add_zmset x {#}\<^sub>z" lemma zcount_empty[simp]: "zcount {#}\<^sub>z a = 0" by transfer auto lemma zcount_add_zmset[simp]: "zcount (add_zmset b A) a = (if b = a then zcount A a + 1 else zcount A a)" by transfer auto lemma zcount_single: "zcount {#b#}\<^sub>z a = (if b = a then 1 else 0)" by simp lemma add_add_same_iff_zmset[simp]: "add_zmset a A = add_zmset a B \ A = B" by (auto simp: zmultiset_eq_iff) lemma add_zmset_commute: "add_zmset x (add_zmset y M) = add_zmset y (add_zmset x M)" by (auto simp: zmultiset_eq_iff) lemma singleton_ne_empty_zmset[simp]: "{#x#}\<^sub>z \ {#}\<^sub>z" and empty_ne_singleton_zmset[simp]: "{#}\<^sub>z \ {#x#}\<^sub>z" by (auto dest!: arg_cong2[of _ _ x _ zcount]) lemma singleton_ne_uminus_singleton_zmset[simp]: "{#x#}\<^sub>z \ - {#y#}\<^sub>z" and uminus_singleton_ne_singleton_zmset[simp]: "- {#x#}\<^sub>z \ {#y#}\<^sub>z" by (auto dest!: arg_cong2[of _ _ x x zcount] split: if_splits) subsubsection \Conversion to Set and Membership\ definition set_zmset :: "'a zmultiset \ 'a set" where "set_zmset M = {x. zcount M x \ 0}" abbreviation elem_zmset :: "'a \ 'a zmultiset \ bool" where "elem_zmset a M \ a \ set_zmset M" notation elem_zmset ("'(\#\<^sub>z')") and elem_zmset ("(_/ \#\<^sub>z _)" [51, 51] 50) notation (ASCII) elem_zmset ("'(:#z')") and elem_zmset ("(_/ :#z _)" [51, 51] 50) abbreviation not_elem_zmset :: "'a \ 'a zmultiset \ bool" where "not_elem_zmset a M \ a \ set_zmset M" notation not_elem_zmset ("'(\#\<^sub>z')") and not_elem_zmset ("(_/ \#\<^sub>z _)" [51, 51] 50) notation (ASCII) not_elem_zmset ("'(~:#z')") and not_elem_zmset ("(_/ ~:#z _)" [51, 51] 50) context begin qualified abbreviation Ball :: "'a zmultiset \ ('a \ bool) \ bool" where "Ball M \ Set.Ball (set_zmset M)" qualified abbreviation Bex :: "'a zmultiset \ ('a \ bool) \ bool" where "Bex M \ Set.Bex (set_zmset M)" end syntax "_ZMBall" :: "pttrn \ 'a set \ bool \ bool" ("(3\_\#\<^sub>z_./ _)" [0, 0, 10] 10) "_ZMBex" :: "pttrn \ 'a set \ bool \ bool" ("(3\_\#\<^sub>z_./ _)" [0, 0, 10] 10) syntax (ASCII) "_ZMBall" :: "pttrn \ 'a set \ bool \ bool" ("(3\_:#\<^sub>z_./ _)" [0, 0, 10] 10) "_ZMBex" :: "pttrn \ 'a set \ bool \ bool" ("(3\_:#\<^sub>z_./ _)" [0, 0, 10] 10) translations "\x\#\<^sub>zA. P" \ "CONST Signed_Multiset.Ball A (\x. P)" "\x\#\<^sub>zA. P" \ "CONST Signed_Multiset.Bex A (\x. P)" lemma zcount_eq_zero_iff: "zcount M x = 0 \ x \#\<^sub>z M" by (auto simp add: set_zmset_def) lemma not_in_iff_zmset: "x \#\<^sub>z M \ zcount M x = 0" by (auto simp add: zcount_eq_zero_iff) lemma zcount_ne_zero_iff[simp]: "zcount M x \ 0 \ x \#\<^sub>z M" by (auto simp add: set_zmset_def) lemma zcount_inI: assumes "zcount M x = 0 \ False" shows "x \#\<^sub>z M" proof (rule ccontr) assume "x \#\<^sub>z M" with assms show False by (simp add: not_in_iff_zmset) qed lemma set_zmset_empty[simp]: "set_zmset {#}\<^sub>z = {}" by (simp add: set_zmset_def) lemma set_zmset_single: "set_zmset {#b#}\<^sub>z = {b}" by (simp add: set_zmset_def) lemma set_zmset_eq_empty_iff[simp]: "set_zmset M = {} \ M = {#}\<^sub>z" by (auto simp add: zmultiset_eq_iff zcount_eq_zero_iff) lemma finite_count_ne: "finite {x. count M x \ count N x}" proof - have "{x. count M x \ count N x} \ set_mset M \ set_mset N" by (auto simp: not_in_iff) moreover have "finite (set_mset M \ set_mset N)" by (rule finite_UnI[OF finite_set_mset finite_set_mset]) ultimately show ?thesis by (rule finite_subset) qed lemma finite_set_zmset[iff]: "finite (set_zmset M)" unfolding set_zmset_def by transfer (auto intro: finite_count_ne) lemma zmultiset_nonemptyE[elim]: assumes "A \ {#}\<^sub>z" obtains x where "x \#\<^sub>z A" proof - have "\x. x \#\<^sub>z A" by (rule ccontr) (insert assms, auto) with that show ?thesis by blast qed subsubsection \Union\ lemma zcount_union[simp]: "zcount (M + N) a = zcount M a + zcount N a" by transfer auto lemma union_add_left_zmset[simp]: "add_zmset a A + B = add_zmset a (A + B)" by (auto simp: zmultiset_eq_iff) lemma union_zmset_add_zmset_right[simp]: "A + add_zmset a B = add_zmset a (A + B)" by (auto simp: zmultiset_eq_iff) lemma add_zmset_add_single: \add_zmset a A = A + {#a#}\<^sub>z\ by (subst union_zmset_add_zmset_right, subst add.comm_neutral) (rule refl) subsubsection \Difference\ lemma zcount_diff[simp]: "zcount (M - N) a = zcount M a - zcount N a" by transfer auto lemma add_zmset_diff_bothsides: \add_zmset a M - add_zmset a A = M - A\ by (auto simp: zmultiset_eq_iff) lemma in_diff_zcount: "a \#\<^sub>z M - N \ zcount N a \ zcount M a" by (fastforce simp: set_zmset_def) lemma diff_add_zmset: fixes M N Q :: "'a zmultiset" shows "M - (N + Q) = M - N - Q" by (rule sym) (fact diff_diff_add) lemma insert_Diff_zmset[simp]: "add_zmset x (M - {#x#}\<^sub>z) = M" by (clarsimp simp: zmultiset_eq_iff) lemma diff_union_swap_zmset: "add_zmset b (M - {#a#}\<^sub>z) = add_zmset b M - {#a#}\<^sub>z" by (auto simp add: zmultiset_eq_iff) lemma diff_add_zmset_swap[simp]: "add_zmset b M - A = add_zmset b (M - A)" by (auto simp add: zmultiset_eq_iff) lemma diff_diff_add_zmset[simp]: "(M :: 'a zmultiset) - N - P = M - (N + P)" by (rule diff_diff_add) lemma zmset_add[elim?]: obtains B where "A = add_zmset a B" proof - have "A = add_zmset a (A - {#a#}\<^sub>z)" by simp with that show thesis . qed subsubsection \Equality of Signed Multisets\ lemma single_eq_single_zmset[simp]: "{#a#}\<^sub>z = {#b#}\<^sub>z \ a = b" by (auto simp add: zmultiset_eq_iff) lemma multi_self_add_other_not_self_zmset[simp]: "M = add_zmset x M \ False" by (auto simp add: zmultiset_eq_iff) lemma add_zmset_remove_trivial: \add_zmset x M - {#x#}\<^sub>z = M\ by simp lemma diff_single_eq_union_zmset: "M - {#x#}\<^sub>z = N \ M = add_zmset x N" by auto lemma union_single_eq_diff_zmset: "add_zmset x M = N \ M = N - {#x#}\<^sub>z" unfolding add_zmset_add_single[of _ M] by (fact add_implies_diff) lemma add_zmset_eq_conv_diff: "add_zmset a M = add_zmset b N \ M = N \ a = b \ M = add_zmset b (N - {#a#}\<^sub>z) \ N = add_zmset a (M - {#b#}\<^sub>z)" by (simp add: zmultiset_eq_iff) fastforce lemma add_zmset_eq_conv_ex: "(add_zmset a M = add_zmset b N) = (M = N \ a = b \ (\K. M = add_zmset b K \ N = add_zmset a K))" by (auto simp add: add_zmset_eq_conv_diff) lemma multi_member_split: "\A. M = add_zmset x A" by (rule exI[where x = "M - {#x#}\<^sub>z"]) simp subsection \Conversions from and to Multisets\ lift_definition zmset_of :: "'a multiset \ 'a zmultiset" is "\f. (Abs_multiset f, {#})" . lemma zmset_of_inject[simp]: "zmset_of M = zmset_of N \ M = N" - by (simp add: zmset_of_def, transfer, auto simp: equiv_zmset_def) + by (simp add: zmset_of_def, transfer', auto simp: equiv_zmset_def) lemma zmset_of_empty[simp]: "zmset_of {#} = {#}\<^sub>z" by (simp add: zmset_of_def zero_zmultiset_def) lemma zmset_of_add_mset[simp]: "zmset_of (add_mset x M) = add_zmset x (zmset_of M)" by transfer (auto simp: equiv_zmset_def add_mset_def cong: if_cong) lemma zcount_of_mset[simp]: "zcount (zmset_of M) x = int (count M x)" by (induct M) auto lemma zmset_of_plus: "zmset_of (M + N) = zmset_of M + zmset_of N" by (transfer, auto simp: equiv_zmset_def eq_onp_same_args plus_multiset.abs_eq)+ lift_definition mset_pos :: "'a zmultiset \ 'a multiset" is "\(Mp, Mn). count (Mp - Mn)" by (auto simp add: equiv_zmset_def simp flip: set_mset_diff) (metis add.commute add_diff_cancel_right) lift_definition mset_neg :: "'a zmultiset \ 'a multiset" is "\(Mp, Mn). count (Mn - Mp)" by (auto simp add: equiv_zmset_def simp flip: set_mset_diff) (metis add.commute add_diff_cancel_right) lemma zmset_of_inverse[simp]: "mset_pos (zmset_of M) = M" and minus_zmset_of_inverse[simp]: "mset_neg (- zmset_of M) = M" by (transfer, simp)+ lemma neg_zmset_pos[simp]: "mset_neg (zmset_of M) = {#}" by (rule zmset_of_inject[THEN iffD1], simp, transfer, auto simp: equiv_zmset_def)+ lemma count_mset_pos[simp]: "count (mset_pos M) x = nat (zcount M x)" and count_mset_neg[simp]: "count (mset_neg M) x = nat (- zcount M x)" by (transfer; auto)+ lemma mset_pos_empty[simp]: "mset_pos {#}\<^sub>z = {#}" and mset_neg_empty[simp]: "mset_neg {#}\<^sub>z = {#}" by (rule multiset_eqI, simp)+ lemma mset_pos_singleton[simp]: "mset_pos {#x#}\<^sub>z = {#x#}" and mset_neg_singleton[simp]: "mset_neg {#x#}\<^sub>z = {#}" by (rule multiset_eqI, simp)+ lemma mset_pos_neg_partition: "M = zmset_of (mset_pos M) - zmset_of (mset_neg M)" and mset_pos_as_neg: "zmset_of (mset_pos M) = zmset_of (mset_neg M) + M" and mset_neg_as_pos: "zmset_of (mset_neg M) = zmset_of (mset_pos M) - M" by (rule zmultiset_eqI, simp)+ lemma mset_pos_uminus[simp]: "mset_pos (- A) = mset_neg A" by (rule multiset_eqI) simp lemma mset_neg_uminus[simp]: "mset_neg (- A) = mset_pos A" by (rule multiset_eqI) simp lemma mset_pos_plus[simp]: "mset_pos (A + B) = (mset_pos A - mset_neg B) + (mset_pos B - mset_neg A)" by (rule multiset_eqI) simp lemma mset_neg_plus[simp]: "mset_neg (A + B) = (mset_neg A - mset_pos B) + (mset_neg B - mset_pos A)" by (rule multiset_eqI) simp lemma mset_pos_diff[simp]: "mset_pos (A - B) = (mset_pos A - mset_pos B) + (mset_neg B - mset_neg A)" by (rule mset_pos_plus[of A "- B", simplified]) lemma mset_neg_diff[simp]: "mset_neg (A - B) = (mset_neg A - mset_neg B) + (mset_pos B - mset_pos A)" by (rule mset_neg_plus[of A "- B", simplified]) lemma mset_pos_neg_dual: "mset_pos a + mset_pos b + (mset_neg a - mset_pos b) + (mset_neg b - mset_pos a) = mset_neg a + mset_neg b + (mset_pos a - mset_neg b) + (mset_pos b - mset_neg a)" using [[linarith_split_limit = 20]] by (rule multiset_eqI) simp lemma decompose_zmset_of2: obtains A B C where "M = zmset_of A + C" and "N = zmset_of B + C" proof let ?A = "zmset_of (mset_pos M + mset_neg N)" let ?B = "zmset_of (mset_pos N + mset_neg M)" let ?C = "- (zmset_of (mset_neg M) + zmset_of (mset_neg N))" show "M = ?A + ?C" by (simp add: zmset_of_plus mset_pos_neg_partition) show "N = ?B + ?C" by (simp add: zmset_of_plus diff_add_zmset mset_pos_neg_partition) qed subsubsection \Pointwise Ordering Induced by @{const zcount}\ definition subseteq_zmset :: "'a zmultiset \ 'a zmultiset \ bool" (infix "\#\<^sub>z" 50) where "A \#\<^sub>z B \ (\a. zcount A a \ zcount B a)" definition subset_zmset :: "'a zmultiset \ 'a zmultiset \ bool" (infix "\#\<^sub>z" 50) where "A \#\<^sub>z B \ A \#\<^sub>z B \ A \ B" abbreviation (input) supseteq_zmset :: "'a zmultiset \ 'a zmultiset \ bool" (infix "\#\<^sub>z" 50) where "supseteq_zmset A B \ B \#\<^sub>z A" abbreviation (input) supset_zmset :: "'a zmultiset \ 'a zmultiset \ bool" (infix "\#\<^sub>z" 50) where "supset_zmset A B \ B \#\<^sub>z A" notation (input) subseteq_zmset (infix "\#\<^sub>z" 50) and supseteq_zmset (infix "\#\<^sub>z" 50) notation (ASCII) subseteq_zmset (infix "\#\<^sub>z" 50) and subset_zmset (infix "\#\<^sub>z" 50) and supseteq_zmset (infix "\#\<^sub>z" 50) and supset_zmset (infix ">#\<^sub>z" 50) interpretation subset_zmset: ordered_ab_semigroup_add_imp_le "(+)" "(-)" "(\#\<^sub>z)" "(\#\<^sub>z)" by unfold_locales (auto simp add: subset_zmset_def subseteq_zmset_def zmultiset_eq_iff intro: order_trans antisym) interpretation subset_zmset: ordered_ab_semigroup_monoid_add_imp_le "(+)" 0 "(-)" "(\#\<^sub>z)" "(\#\<^sub>z)" by unfold_locales lemma zmset_subset_eqI: "(\a. zcount A a \ zcount B a) \ A \#\<^sub>z B" by (simp add: subseteq_zmset_def) lemma zmset_subset_eq_zcount: "A \#\<^sub>z B \ zcount A a \ zcount B a" by (simp add: subseteq_zmset_def) lemma zmset_subset_eq_add_zmset_cancel: \add_zmset a A \#\<^sub>z add_zmset a B \ A \#\<^sub>z B\ unfolding add_zmset_add_single[of _ A] add_zmset_add_single[of _ B] by (rule subset_zmset.add_le_cancel_right) lemma zmset_subset_eq_zmultiset_union_diff_commute: "A - B + C = A + C - B" for A B C :: "'a zmultiset" by (simp add: add.commute add_diff_eq) lemma zmset_subset_eq_insertD: "add_zmset x A \#\<^sub>z B \ A \#\<^sub>z B" unfolding subset_zmset_def subseteq_zmset_def by (metis (no_types) add.commute add_le_same_cancel2 zcount_add_zmset dual_order.trans le_cases le_numeral_extra(2)) lemma zmset_subset_insertD: "add_zmset x A \#\<^sub>z B \ A \#\<^sub>z B" by (rule zmset_subset_eq_insertD) (rule subset_zmset.less_imp_le) lemma subset_eq_diff_conv_zmset: "A - C \#\<^sub>z B \ A \#\<^sub>z B + C" by (simp add: subseteq_zmset_def ordered_ab_group_add_class.diff_le_eq) lemma multi_psub_of_add_self_zmset[simp]: "A \#\<^sub>z add_zmset x A" by (auto simp: subset_zmset_def subseteq_zmset_def) lemma multi_psub_self_zmset: "A \#\<^sub>z A = False" by simp lemma zmset_subset_add_zmset[simp]: "add_zmset x N \#\<^sub>z add_zmset x M \ N \#\<^sub>z M" unfolding add_zmset_add_single[of _ N] add_zmset_add_single[of _ M] by (fact subset_zmset.add_less_cancel_right) lemma zmset_of_subseteq_iff[simp]: "zmset_of M \#\<^sub>z zmset_of N \ M \# N" by (simp add: subseteq_zmset_def subseteq_mset_def) lemma zmset_of_subset_iff[simp]: "zmset_of M \#\<^sub>z zmset_of N \ M \# N" by (simp add: subset_zmset_def subset_mset_def) lemma mset_pos_supset: "A \#\<^sub>z zmset_of (mset_pos A)" and mset_neg_supset: "- A \#\<^sub>z zmset_of (mset_neg A)" by (auto intro: zmset_subset_eqI) lemma subset_mset_zmsetE: assumes "M \#\<^sub>z N" obtains A B C where "M = zmset_of A + C" and "N = zmset_of B + C" and "A \# B" by (metis assms decompose_zmset_of2 subset_zmset.add_less_cancel_right zmset_of_subset_iff) lemma subseteq_mset_zmsetE: assumes "M \#\<^sub>z N" obtains A B C where "M = zmset_of A + C" and "N = zmset_of B + C" and "A \# B" by (metis assms add.commute add.right_neutral subset_mset.order_refl subset_mset_def subset_mset_zmsetE subset_zmset_def zmset_of_empty) subsubsection \Subset is an Order\ interpretation subset_zmset: order "(\#\<^sub>z)" "(\#\<^sub>z)" by unfold_locales subsection \Replicate and Repeat Operations\ definition replicate_zmset :: "nat \ 'a \ 'a zmultiset" where "replicate_zmset n x = (add_zmset x ^^ n) {#}\<^sub>z" lemma replicate_zmset_0[simp]: "replicate_zmset 0 x = {#}\<^sub>z" unfolding replicate_zmset_def by simp lemma replicate_zmset_Suc[simp]: "replicate_zmset (Suc n) x = add_zmset x (replicate_zmset n x)" unfolding replicate_zmset_def by (induct n) (auto intro: add.commute) lemma count_replicate_zmset[simp]: "zcount (replicate_zmset n x) y = (if y = x then of_nat n else 0)" unfolding replicate_zmset_def by (induct n) auto fun repeat_zmset :: "nat \ 'a zmultiset \ 'a zmultiset" where "repeat_zmset 0 _ = {#}\<^sub>z" | "repeat_zmset (Suc n) A = A + repeat_zmset n A" lemma count_repeat_zmset[simp]: "zcount (repeat_zmset i A) a = of_nat i * zcount A a" by (induct i) (auto simp: semiring_normalization_rules(3)) lemma repeat_zmset_right[simp]: "repeat_zmset a (repeat_zmset b A) = repeat_zmset (a * b) A" by (auto simp: zmultiset_eq_iff left_diff_distrib') lemma left_diff_repeat_zmset_distrib': \i \ j \ repeat_zmset (i - j) u = repeat_zmset i u - repeat_zmset j u\ by (auto simp: zmultiset_eq_iff int_distrib(3) of_nat_diff) lemma left_add_mult_distrib_zmset: "repeat_zmset i u + (repeat_zmset j u + k) = repeat_zmset (i+j) u + k" by (auto simp: zmultiset_eq_iff add_mult_distrib int_distrib(1)) lemma repeat_zmset_distrib: "repeat_zmset (m + n) A = repeat_zmset m A + repeat_zmset n A" by (auto simp: zmultiset_eq_iff Nat.add_mult_distrib int_distrib(1)) lemma repeat_zmset_distrib2[simp]: "repeat_zmset n (A + B) = repeat_zmset n A + repeat_zmset n B" by (auto simp: zmultiset_eq_iff add_mult_distrib2 int_distrib(2)) lemma repeat_zmset_replicate_zmset[simp]: "repeat_zmset n {#a#}\<^sub>z = replicate_zmset n a" by (auto simp: zmultiset_eq_iff) lemma repeat_zmset_distrib_add_zmset[simp]: "repeat_zmset n (add_zmset a A) = replicate_zmset n a + repeat_zmset n A" by (auto simp: zmultiset_eq_iff int_distrib(2)) lemma repeat_zmset_empty[simp]: "repeat_zmset n {#}\<^sub>z = {#}\<^sub>z" by (induct n) simp_all subsubsection \Filter (with Comprehension Syntax)\ lift_definition filter_zmset :: "('a \ bool) \ 'a zmultiset \ 'a zmultiset" is "\P (Mp, Mn). (filter_mset P Mp, filter_mset P Mn)" by (auto simp del: filter_union_mset simp: equiv_zmset_def filter_union_mset[symmetric]) syntax (ASCII) "_ZMCollect" :: "pttrn \ 'a zmultiset \ bool \ 'a zmultiset" ("(1{#_ :#z _./ _#})") syntax "_ZMCollect" :: "pttrn \ 'a zmultiset \ bool \ 'a zmultiset" ("(1{#_ \#\<^sub>z _./ _#})") translations "{#x \#\<^sub>z M. P#}" == "CONST filter_zmset (\x. P) M" lemma count_filter_zmset[simp]: "zcount (filter_zmset P M) a = (if P a then zcount M a else 0)" by transfer auto lemma filter_empty_zmset[simp]: "filter_zmset P {#}\<^sub>z = {#}\<^sub>z" by (rule zmultiset_eqI) simp lemma filter_single_zmset: "filter_zmset P {#x#}\<^sub>z = (if P x then {#x#}\<^sub>z else {#}\<^sub>z)" by (rule zmultiset_eqI) simp lemma filter_union_zmset[simp]: "filter_zmset P (M + N) = filter_zmset P M + filter_zmset P N" by (rule zmultiset_eqI) simp lemma filter_diff_zmset[simp]: "filter_zmset P (M - N) = filter_zmset P M - filter_zmset P N" by (rule zmultiset_eqI) simp lemma filter_add_zmset[simp]: "filter_zmset P (add_zmset x A) = (if P x then add_zmset x (filter_zmset P A) else filter_zmset P A)" by (auto simp: zmultiset_eq_iff) lemma zmultiset_filter_mono: assumes "A \#\<^sub>z B" shows "filter_zmset f A \#\<^sub>z filter_zmset f B" using assms by (simp add: subseteq_zmset_def) lemma filter_filter_zmset: "filter_zmset P (filter_zmset Q M) = {#x \#\<^sub>z M. Q x \ P x#}" by (auto simp: zmultiset_eq_iff) lemma filter_zmset_True[simp]: "{#y \#\<^sub>z M. True#} = M" and filter_zmset_False[simp]: "{#y \#\<^sub>z M. False#} = {#}\<^sub>z" by (auto simp: zmultiset_eq_iff) subsection \Uncategorized\ lemma multi_drop_mem_not_eq_zmset: "B - {#c#}\<^sub>z \ B" by (simp add: diff_single_eq_union_zmset) lemma zmultiset_partition: "M = {#x \#\<^sub>z M. P x #} + {#x \#\<^sub>z M. \ P x#}" by (subst zmultiset_eq_iff) auto subsection \Image\ definition image_zmset :: "('a \ 'b) \ 'a zmultiset \ 'b zmultiset" where "image_zmset f M = zmset_of (fold_mset (add_mset \ f) {#} (mset_pos M)) - zmset_of (fold_mset (add_mset \ f) {#} (mset_neg M))" subsection \Multiset Order\ instantiation zmultiset :: (preorder) order begin lift_definition less_zmultiset :: "'a zmultiset \ 'a zmultiset \ bool" is "\(Mp, Mn) (Np, Nn). Mp + Nn < Mn + Np" proof (clarsimp simp: equiv_zmset_def) fix A1 B2 B1 A2 C1 D2 D1 C2 :: "'a multiset" assume ab: "A1 + A2 = B1 + B2" and cd: "C1 + C2 = D1 + D2" have "A1 + D2 < B2 + C1 \ A1 + A2 + D2 < A2 + B2 + C1" by simp also have "\ \ B1 + B2 + D2 < A2 + B2 + C1" unfolding ab by (rule refl) also have "\ \ B1 + D2 < A2 + C1" by simp also have "\ \ B1 + D1 + D2 < A2 + C1 + D1" by simp also have "\ \ B1 + C1 + C2 < A2 + C1 + D1" using cd by (simp add: add.assoc) also have "\ \ B1 + C2 < A2 + D1" by simp finally show "A1 + D2 < B2 + C1 \ B1 + C2 < A2 + D1" by assumption qed definition less_eq_zmultiset :: "'a zmultiset \ 'a zmultiset \ bool" where "less_eq_zmultiset M' M \ M' < M \ M' = M" instance proof ((intro_classes; unfold less_eq_zmultiset_def; transfer), auto simp: equiv_zmset_def union_commute) fix A1 B1 D C B2 A2 :: "'a multiset" assume ab: "A1 + A2 \ B1 + B2" { assume ab1: "A1 + C < B1 + D" { assume ab2: "D + A2 < C + B2" show "A1 + A2 < B1 + B2" proof - have f1: "\m. D + A2 + m < C + B2 + m" using ab2 add_less_cancel_right by blast have "\m. C + (A1 + m) < D + (B1 + m)" by (simp add: ab1 add.commute) then have "D + (A2 + A1) < D + (B1 + B2)" using f1 by (metis add.assoc add.commute mset_le_trans) then show ?thesis by (simp add: add.commute) qed } { assume ab2: "D + A2 = C + B2" show "A1 + A2 < B1 + B2" proof - have "\m. C + A1 + m < D + B1 + m" by (simp add: ab1 add.commute) then have "D + (A2 + A1) < D + (B1 + B2)" by (metis (no_types) ab2 add.assoc add.commute) then show ?thesis by (simp add: add.commute) qed } } { assume ab1: "A1 + C = B1 + D" { assume ab2: "D + A2 < C + B2" show "A1 + A2 < B1 + B2" proof - have "A1 + (D + A2) < B1 + (D + B2)" by (metis (no_types) ab1 ab2 add.assoc add_less_cancel_left) then show ?thesis by simp qed } { assume ab2: "D + A2 = C + B2" have False by (metis (no_types) ab ab1 ab2 add.assoc add.commute add_diff_cancel_right') thus "A1 + A2 < B1 + B2" by sat } } qed end instance zmultiset :: (preorder) ordered_cancel_comm_monoid_add by (intro_classes, unfold less_eq_zmultiset_def, transfer, auto simp: equiv_zmset_def) instance zmultiset :: (preorder) ordered_ab_group_add by (intro_classes; transfer; auto simp: equiv_zmset_def) instantiation zmultiset :: (linorder) distrib_lattice begin definition inf_zmultiset :: "'a zmultiset \ 'a zmultiset \ 'a zmultiset" where "inf_zmultiset A B = (if A < B then A else B)" definition sup_zmultiset :: "'a zmultiset \ 'a zmultiset \ 'a zmultiset" where "sup_zmultiset A B = (if B > A then B else A)" lemma not_lt_iff_ge_zmset: "\ x < y \ x \ y" for x y :: "'a zmultiset" by (unfold less_eq_zmultiset_def, transfer, auto simp: equiv_zmset_def algebra_simps) instance by intro_classes (auto simp: less_eq_zmultiset_def inf_zmultiset_def sup_zmultiset_def dest!: not_lt_iff_ge_zmset[THEN iffD1]) end lemma zmset_of_less: "zmset_of M < zmset_of N \ M < N" - by (clarsimp simp: zmset_of_def, transfer, simp)+ + by (clarsimp simp: zmset_of_def, transfer', simp)+ lemma zmset_of_le: "zmset_of M \ zmset_of N \ M \ N" - by (simp_all add: less_eq_zmultiset_def zmset_of_def; transfer; auto simp: equiv_zmset_def) + by (simp_all add: less_eq_zmultiset_def zmset_of_def; transfer'; auto simp: equiv_zmset_def) instance zmultiset :: (preorder) ordered_ab_semigroup_add by (intro_classes, unfold less_eq_zmultiset_def, transfer, auto simp: equiv_zmset_def) lemma uminus_add_conv_diff_mset[cancelation_simproc_pre]: \-a + b = b - a\ for a :: \'a zmultiset\ by (simp add: add.commute) lemma uminus_add_add_uminus[cancelation_simproc_pre]: \b -a + c = b + c - a\ for a :: \'a zmultiset\ by (simp add: uminus_add_conv_diff_mset zmset_subset_eq_zmultiset_union_diff_commute) lemma add_zmset_eq_add_NO_MATCH[cancelation_simproc_pre]: \NO_MATCH {#}\<^sub>z H \ add_zmset a H = {#a#}\<^sub>z + H\ by auto lemma repeat_zmset_iterate_add: \repeat_zmset n M = iterate_add n M\ unfolding iterate_add_def by (induction n) auto declare repeat_zmset_iterate_add[cancelation_simproc_pre] declare repeat_zmset_iterate_add[symmetric, cancelation_simproc_post] simproc_setup zmseteq_cancel_numerals ("(l::'a zmultiset) + m = n" | "(l::'a zmultiset) = m + n" | "add_zmset a m = n" | "m = add_zmset a n" | "replicate_zmset p a = n" | "m = replicate_zmset p a" | "repeat_zmset p m = n" | "m = repeat_zmset p m") = \fn phi => Cancel_Simprocs.eq_cancel\ lemma zmset_subseteq_add_iff1: \j \ i \ (repeat_zmset i u + m \#\<^sub>z repeat_zmset j u + n) = (repeat_zmset (i - j) u + m \#\<^sub>z n)\ by (simp add: add.commute add_diff_eq left_diff_repeat_zmset_distrib' subset_eq_diff_conv_zmset) lemma zmset_subseteq_add_iff2: \i \ j \ (repeat_zmset i u + m \#\<^sub>z repeat_zmset j u + n) = (m \#\<^sub>z repeat_zmset (j - i) u + n)\ proof - assume "i \ j" then have "\z. repeat_zmset j (z::'a zmultiset) - repeat_zmset i z = repeat_zmset (j - i) z" by (simp add: left_diff_repeat_zmset_distrib') then show ?thesis by (metis add.commute diff_diff_eq2 subset_eq_diff_conv_zmset) qed lemma zmset_subset_add_iff1: \j \ i \ (repeat_zmset i u + m \#\<^sub>z repeat_zmset j u + n) = (repeat_zmset (i - j) u + m \#\<^sub>z n)\ by (simp add: subset_zmset.less_le_not_le zmset_subseteq_add_iff1 zmset_subseteq_add_iff2) lemma zmset_subset_add_iff2: \i \ j \ (repeat_zmset i u + m \#\<^sub>z repeat_zmset j u + n) = (m \#\<^sub>z repeat_zmset (j - i) u + n)\ by (simp add: subset_zmset.less_le_not_le zmset_subseteq_add_iff1 zmset_subseteq_add_iff2) ML_file \zmultiset_simprocs.ML\ simproc_setup zmsetsubset_cancel ("(l::'a zmultiset) + m \#\<^sub>z n" | "(l::'a zmultiset) \#\<^sub>z m + n" | "add_zmset a m \#\<^sub>z n" | "m \#\<^sub>z add_zmset a n" | "replicate_zmset p a \#\<^sub>z n" | "m \#\<^sub>z replicate_zmset p a" | "repeat_zmset p m \#\<^sub>z n" | "m \#\<^sub>z repeat_zmset p m") = \fn phi => ZMultiset_Simprocs.subset_cancel_zmsets\ simproc_setup zmsetsubseteq_cancel ("(l::'a zmultiset) + m \#\<^sub>z n" | "(l::'a zmultiset) \#\<^sub>z m + n" | "add_zmset a m \#\<^sub>z n" | "m \#\<^sub>z add_zmset a n" | "replicate_zmset p a \#\<^sub>z n" | "m \#\<^sub>z replicate_zmset p a" | "repeat_zmset p m \#\<^sub>z n" | "m \#\<^sub>z repeat_zmset p m") = \fn phi => ZMultiset_Simprocs.subseteq_cancel_zmsets\ instance zmultiset :: (preorder) ordered_ab_semigroup_add_imp_le by (intro_classes; unfold less_eq_zmultiset_def; transfer; auto) simproc_setup zmsetless_cancel ("(l::'a::preorder zmultiset) + m < n" | "(l::'a zmultiset) < m + n" | "add_zmset a m < n" | "m < add_zmset a n" | "replicate_zmset p a < n" | "m < replicate_zmset p a" | "repeat_zmset p m < n" | "m < repeat_zmset p m") = \fn phi => Cancel_Simprocs.less_cancel\ simproc_setup zmsetless_eq_cancel ("(l::'a::preorder zmultiset) + m \ n" | "(l::'a zmultiset) \ m + n" | "add_zmset a m \ n" | "m \ add_zmset a n" | "replicate_zmset p a \ n" | "m \ replicate_zmset p a" | "repeat_zmset p m \ n" | "m \ repeat_zmset p m") = \fn phi => Cancel_Simprocs.less_eq_cancel\ simproc_setup zmsetdiff_cancel ("n + (l::'a zmultiset)" | "(l::'a zmultiset) - m" | "add_zmset a m - n" | "m - add_zmset a n" | "replicate_zmset p r - n" | "m - replicate_zmset p r" | "repeat_zmset p m - n" | "m - repeat_zmset p m") = \fn phi => Cancel_Simprocs.diff_cancel\ instance zmultiset :: (linorder) linordered_cancel_ab_semigroup_add by (intro_classes, unfold less_eq_zmultiset_def, transfer, auto simp: equiv_zmset_def add.commute) lemma less_mset_zmsetE: assumes "M < N" obtains A B C where "M = zmset_of A + C" and "N = zmset_of B + C" and "A < B" by (metis add_less_imp_less_right assms decompose_zmset_of2 zmset_of_less) lemma less_eq_mset_zmsetE: assumes "M \ N" obtains A B C where "M = zmset_of A + C" and "N = zmset_of B + C" and "A \ B" by (metis add.commute add.right_neutral assms le_neq_trans less_imp_le less_mset_zmsetE order_refl zmset_of_empty) lemma subset_eq_imp_le_zmset: "M \#\<^sub>z N \ M \ N" by (metis (no_types) add_mono_thms_linordered_semiring(3) subset_eq_imp_le_multiset subseteq_mset_zmsetE zmset_of_le) lemma subset_imp_less_zmset: "M \#\<^sub>z N \ M < N" by (metis le_neq_trans subset_eq_imp_le_zmset subset_zmset_def) lemma lt_imp_ex_zcount_lt: assumes m_lt_n: "M < N" shows "\y. zcount M y < zcount N y" proof (rule ccontr, clarsimp) assume "\y. \ zcount M y < zcount N y" hence "\y. zcount M y \ zcount N y" by (simp add: leI) hence "M \#\<^sub>z N" by (simp add: zmset_subset_eqI) hence "M \ N" by (simp add: subset_eq_imp_le_zmset) thus False using m_lt_n by simp qed instance zmultiset :: (preorder) no_top proof fix M :: \'a zmultiset\ obtain a :: 'a where True by fast let ?M = \zmset_of (mset_pos M) + zmset_of (mset_neg M)\ have \M < add_zmset a ?M + ?M\ by (subst mset_pos_neg_partition) (auto simp: subset_zmset_def subseteq_zmset_def zmultiset_eq_iff intro!: subset_imp_less_zmset) then show \\N. M < N\ by blast qed +lifting_update multiset.lifting +lifting_forget multiset.lifting + end diff --git a/thys/Pi_Transcendental/Pi_Transcendental_Polynomial_Library.thy b/thys/Pi_Transcendental/Pi_Transcendental_Polynomial_Library.thy --- a/thys/Pi_Transcendental/Pi_Transcendental_Polynomial_Library.thy +++ b/thys/Pi_Transcendental/Pi_Transcendental_Polynomial_Library.thy @@ -1,381 +1,386 @@ (* File: Pi_Transcendental_Polynomial_Library Author: Manuel Eberl, TU München Various facts about univariate polynomials and some other things that probably belong in the distribution. *) section \Preliminary facts\ theory Pi_Transcendental_Polynomial_Library imports "HOL-Computational_Algebra.Computational_Algebra" begin +unbundle multiset.lifting + (* TODO: Move all this *) lemma Ints_sum: "(\x. x \ A \ f x \ \) \ sum f A \ \" by (induction A rule: infinite_finite_induct) auto lemma Ints_prod: "(\x. x \ A \ f x \ \) \ prod f A \ \" by (induction A rule: infinite_finite_induct) auto lemma sum_in_Rats [intro]: "(\x. x \ A \ f x \ \) \ sum f A \ \" by (induction A rule: infinite_finite_induct) auto lemma prod_in_Rats [intro]: "(\x. x \ A \ f x \ \) \ prod f A \ \" by (induction A rule: infinite_finite_induct) auto lemma poly_cnj: "cnj (poly p z) = poly (map_poly cnj p) (cnj z)" by (simp add: poly_altdef degree_map_poly coeff_map_poly) lemma poly_cnj_real: assumes "\n. poly.coeff p n \ \" shows "cnj (poly p z) = poly p (cnj z)" proof - from assms have "map_poly cnj p = p" by (intro poly_eqI) (auto simp: coeff_map_poly Reals_cnj_iff) with poly_cnj[of p z] show ?thesis by simp qed lemma real_poly_cnj_root_iff: assumes "\n. poly.coeff p n \ \" shows "poly p (cnj z) = 0 \ poly p z = 0" proof - have "poly p (cnj z) = cnj (poly p z)" by (simp add: poly_cnj_real assms) also have "\ = 0 \ poly p z = 0" by simp finally show ?thesis . qed lemma coeff_pcompose_linear: fixes p :: "'a :: comm_semiring_1 poly" shows "coeff (pcompose p [:0, c:]) i = c ^ i * coeff p i" by (induction p arbitrary: i) (auto simp: pcompose_pCons coeff_pCons mult_ac split: nat.splits) lemma coeff_pCons': "poly.coeff (pCons c p) n = (if n = 0 then c else poly.coeff p (n - 1))" by transfer'(auto split: nat.splits) lemma prod_smult: "(\x\A. Polynomial.smult (c x) (p x)) = Polynomial.smult (prod c A) (prod p A)" by (induction A rule: infinite_finite_induct) (auto simp: mult_ac) lemma degree_higher_pderiv: "Polynomial.degree ((pderiv ^^ n) p) = Polynomial.degree p - n" for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly" by (induction n) (auto simp: degree_pderiv) lemma sum_to_poly: "(\x\A. [:f x:]) = [:\x\A. f x:]" by (induction A rule: infinite_finite_induct) auto lemma diff_to_poly: "[:c:] - [:d:] = [:c - d:]" by (simp add: poly_eq_iff mult_ac) lemma mult_to_poly: "[:c:] * [:d:] = [:c * d:]" by (simp add: poly_eq_iff mult_ac) lemma prod_to_poly: "(\x\A. [:f x:]) = [:\x\A. f x:]" by (induction A rule: infinite_finite_induct) (auto simp: mult_to_poly mult_ac) lemma coeff_mult_0: "poly.coeff (p * q) 0 = poly.coeff p 0 * poly.coeff q 0" by (simp add: coeff_mult) lemma card_poly_roots_bound: fixes p :: "'a::{comm_ring_1,ring_no_zero_divisors} poly" assumes "p \ 0" shows "card {x. poly p x = 0} \ degree p" using assms proof (induction "degree p" arbitrary: p rule: less_induct) case (less p) show ?case proof (cases "\x. poly p x = 0") case False hence "{x. poly p x = 0} = {}" by blast thus ?thesis by simp next case True then obtain x where x: "poly p x = 0" by blast hence "[:-x, 1:] dvd p" by (subst (asm) poly_eq_0_iff_dvd) then obtain q where q: "p = [:-x, 1:] * q" by (auto simp: dvd_def) with \p \ 0\ have [simp]: "q \ 0" by auto have deg: "degree p = Suc (degree q)" by (subst q, subst degree_mult_eq) auto have "card {x. poly p x = 0} \ card (insert x {x. poly q x = 0})" by (intro card_mono) (auto intro: poly_roots_finite simp: q) also have "\ \ Suc (card {x. poly q x = 0})" by (rule card_insert_le_m1) auto also from deg have "card {x. poly q x = 0} \ degree q" using \p \ 0\ and q by (intro less) auto also have "Suc \ = degree p" by (simp add: deg) finally show ?thesis by - simp_all qed qed lemma poly_eqI_degree: fixes p q :: "'a :: {comm_ring_1, ring_no_zero_divisors} poly" assumes "\x. x \ A \ poly p x = poly q x" assumes "card A > degree p" "card A > degree q" shows "p = q" proof (rule ccontr) assume neq: "p \ q" have "degree (p - q) \ max (degree p) (degree q)" by (rule degree_diff_le_max) also from assms have "\ < card A" by linarith also have "\ \ card {x. poly (p - q) x = 0}" using neq and assms by (intro card_mono poly_roots_finite) auto finally have "degree (p - q) < card {x. poly (p - q) x = 0}" . moreover have "degree (p - q) \ card {x. poly (p - q) x = 0}" using neq by (intro card_poly_roots_bound) auto ultimately show False by linarith qed lemma poly_root_order_induct [case_names 0 no_roots root]: fixes p :: "'a :: idom poly" assumes "P 0" "\p. (\x. poly p x \ 0) \ P p" "\p x n. n > 0 \ poly p x \ 0 \ P p \ P ([:-x, 1:] ^ n * p)" shows "P p" proof (induction "degree p" arbitrary: p rule: less_induct) case (less p) consider "p = 0" | "p \ 0" "\x. poly p x = 0" | "\x. poly p x \ 0" by blast thus ?case proof cases case 3 with assms(2)[of p] show ?thesis by simp next case 2 then obtain x where x: "poly p x = 0" by auto have "[:-x, 1:] ^ order x p dvd p" by (intro order_1) then obtain q where q: "p = [:-x, 1:] ^ order x p * q" by (auto simp: dvd_def) with 2 have [simp]: "q \ 0" by auto have order_pos: "order x p > 0" using \p \ 0\ and x by (auto simp: order_root) have "order x p = order x p + order x q" by (subst q, subst order_mult) (auto simp: order_power_n_n) hence [simp]: "order x q = 0" by simp have deg: "degree p = order x p + degree q" by (subst q, subst degree_mult_eq) (auto simp: degree_power_eq) with order_pos have "degree q < degree p" by simp hence "P q" by (rule less) with order_pos have "P ([:-x, 1:] ^ order x p * q)" by (intro assms(3)) (auto simp: order_root) with q show ?thesis by simp qed (simp_all add: assms(1)) qed lemma complex_poly_decompose: "smult (lead_coeff p) (\z|poly p z = 0. [:-z, 1:] ^ order z p) = (p :: complex poly)" proof (induction p rule: poly_root_order_induct) case (no_roots p) show ?case proof (cases "degree p = 0") case False hence "\constant (poly p)" by (subst constant_degree) with fundamental_theorem_of_algebra and no_roots show ?thesis by blast qed (auto elim!: degree_eq_zeroE) next case (root p x n) from root have *: "{z. poly ([:- x, 1:] ^ n * p) z = 0} = insert x {z. poly p z = 0}" by auto have "smult (lead_coeff ([:-x, 1:] ^ n * p)) (\z|poly ([:-x,1:] ^ n * p) z = 0. [:-z, 1:] ^ order z ([:- x, 1:] ^ n * p)) = [:- x, 1:] ^ order x ([:- x, 1:] ^ n * p) * smult (lead_coeff p) (\z\{z. poly p z = 0}. [:- z, 1:] ^ order z ([:- x, 1:] ^ n * p))" by (subst *, subst prod.insert) (insert root, auto intro: poly_roots_finite simp: mult_ac lead_coeff_mult lead_coeff_power) also have "order x ([:- x, 1:] ^ n * p) = n" using root by (subst order_mult) (auto simp: order_power_n_n order_0I) also have "(\z\{z. poly p z = 0}. [:- z, 1:] ^ order z ([:- x, 1:] ^ n * p)) = (\z\{z. poly p z = 0}. [:- z, 1:] ^ order z p)" proof (intro prod.cong refl, goal_cases) case (1 y) with root have "order y ([:-x,1:] ^ n) = 0" by (intro order_0I) auto thus ?case using root by (subst order_mult) auto qed also note root.IH finally show ?case . qed simp_all lemma order_pos_iff: "p \ 0 \ order a p > 0 \ poly p a = 0" using order_root[of p a] by auto lift_definition poly_roots_mset :: "('a :: idom) poly \ 'a multiset" is "\p x. if p = 0 then 0 else Polynomial.order x p" proof - fix p :: "'a poly" show "finite {x. 0 < (if p = 0 then 0 else order x p)}" by (cases "p = 0") (auto simp: order_pos_iff intro: finite_subset[OF _ poly_roots_finite[of p]]) qed lemma poly_roots_mset_0 [simp]: "poly_roots_mset 0 = {#}" by transfer' auto lemma count_poly_roots_mset [simp]: "p \ 0 \ count (poly_roots_mset p) a = order a p" by transfer' auto lemma set_count_poly_roots_mset [simp]: "p \ 0 \ set_mset (poly_roots_mset p) = {x. poly p x = 0}" by (auto simp: set_mset_def order_pos_iff) lemma image_prod_mset_multiplicity: "prod_mset (image_mset f M) = prod (\x. f x ^ count M x) (set_mset M)" proof (induction M) case (add x M) show ?case proof (cases "x \ set_mset M") case True have "(\y\set_mset (add_mset x M). f y ^ count (add_mset x M) y) = (\y\set_mset M. (if y = x then f x else 1) * f y ^ count M y)" using True add by (intro prod.cong) auto also have "\ = f x * (\y\set_mset M. f y ^ count M y)" using True by (subst prod.distrib) auto also note add.IH [symmetric] finally show ?thesis using True by simp next case False hence "(\y\set_mset (add_mset x M). f y ^ count (add_mset x M) y) = f x * (\y\set_mset M. f y ^ count (add_mset x M) y)" by (auto simp: not_in_iff) also have "(\y\set_mset M. f y ^ count (add_mset x M) y) = (\y\set_mset M. f y ^ count M y)" using False by (intro prod.cong) auto also note add.IH [symmetric] finally show ?thesis by simp qed qed auto lemma complex_poly_decompose_multiset: "smult (lead_coeff p) (\x\#poly_roots_mset p. [:-x, 1:]) = (p :: complex poly)" proof (cases "p = 0") case False hence "(\x\#poly_roots_mset p. [:-x, 1:]) = (\x | poly p x = 0. [:-x, 1:] ^ order x p)" by (subst image_prod_mset_multiplicity) simp_all also have "smult (lead_coeff p) \ = p" by (rule complex_poly_decompose) finally show ?thesis . qed auto lemma (in monoid_add) prod_list_prod_nth: "prod_list xs = (\i=0..i. xs ! i) [0.. = (\i=0.. prod f A = 0 \ (\x\A. f x = 0)" for f :: "'a \ 'b :: {comm_semiring_1, semiring_no_zero_divisors}" by (induction A rule: infinite_finite_induct) auto lemma degree_prod_eq: "(\x. x \ A \ f x \ 0) \ degree (prod f A) = (\x\A. degree (f x))" for f :: "'a \ 'b::{comm_semiring_1, semiring_no_zero_divisors} poly" by (induction A rule: infinite_finite_induct) (auto simp: degree_mult_eq prod_zero_iff') lemma lead_coeff_prod: "(\x. x \ A \ f x \ 0) \ lead_coeff (prod f A) = (\x\A. lead_coeff (f x))" for f :: "'a \ 'b :: {comm_semiring_1, semiring_no_zero_divisors} poly" by (induction A rule: infinite_finite_induct) (auto simp: lead_coeff_mult prod_zero_iff') lemma complex_poly_decompose': obtains root where "smult (lead_coeff p) (\ix\#poly_roots_mset p. [:-x, 1:])" by (rule complex_poly_decompose_multiset [symmetric]) also have "(\x\#poly_roots_mset p. [:-x, 1:]) = (\x\roots. [:-x, 1:])" by (subst prod_mset_prod_list [symmetric]) (simp add: roots) also have "\ = (\iii. roots ! i"]) auto qed lemma rsquarefree_root_order: assumes "rsquarefree p" "poly p z = 0" "p \ 0" shows "order z p = 1" proof - from assms have "order z p \ {0, 1}" by (auto simp: rsquarefree_def) moreover from assms have "order z p > 0" by (auto simp: order_root) ultimately show "order z p = 1" by auto qed lemma complex_poly_decompose_rsquarefree: assumes "rsquarefree p" shows "smult (lead_coeff p) (\z|poly p z = 0. [:-z, 1:]) = (p :: complex poly)" proof (cases "p = 0") case False have "(\z|poly p z = 0. [:-z, 1:]) = (\z|poly p z = 0. [:-z, 1:] ^ order z p)" using assms False by (intro prod.cong) (auto simp: rsquarefree_root_order) also have "smult (lead_coeff p) \ = p" by (rule complex_poly_decompose) finally show ?thesis . qed auto lemma pcompose_conjugates_integer: assumes "\i. poly.coeff p i \ \" shows "poly.coeff (pcompose p [:0, \:] * pcompose p [:0, -\:]) i \ \" proof - let ?c = "\i. poly.coeff p i :: complex" have "poly.coeff (pcompose p [:0, \:] * pcompose p [:0, -\:]) i = \ ^ i * (\k\i. (-1) ^ (i - k) * ?c k * ?c (i - k))" unfolding coeff_mult sum_distrib_left by (intro sum.cong) (auto simp: coeff_mult coeff_pcompose_linear power_minus' power_diff field_simps intro!: Ints_sum) also have "(\k\i. (-1) ^ (i - k) * ?c k * ?c (i - k)) = (\k\i. (-1) ^ k * ?c k * ?c (i - k))" (is "?S1 = ?S2") by (intro sum.reindex_bij_witness[of _ "\k. i - k" "\k. i - k"]) (auto simp: mult_ac) hence "?S1 = (?S1 + ?S2) / 2" by simp also have "\ = (\k\i. ((-1) ^ k + (-1) ^ (i - k)) / 2 * ?c k * ?c (i - k))" by (simp add: ring_distribs sum.distrib sum_divide_distrib [symmetric]) also have "\ = (\k\i. (1 + (-1) ^ i) / 2 * (-1) ^ k * ?c k * ?c (i - k))" by (intro sum.cong) (auto simp: power_add power_diff field_simps) also have "\ ^ i * \ \ \" proof (cases "even i") case True thus ?thesis by (intro Ints_mult Ints_sum assms) (auto elim!: evenE simp: power_mult) next case False hence "1 + (-1) ^ i = (0 :: complex)" by (auto elim!: oddE simp: power_mult) thus ?thesis by simp qed finally show ?thesis . qed lemma algebraic_times_i: assumes "algebraic x" shows "algebraic (\ * x)" "algebraic (-\ * x)" proof - from assms obtain p where p: "poly p x = 0" "\i. coeff p i \ \" "p \ 0" by (auto elim!: algebraicE) define p' where "p' = pcompose p [:0, \:] * pcompose p [:0, -\:]" have p': "poly p' (\ * x) = 0" "poly p' (-\ * x) = 0" "p' \ 0" by (auto simp: p'_def poly_pcompose algebra_simps p dest: pcompose_eq_0) moreover have "\i. poly.coeff p' i \ \" using p unfolding p'_def by (intro allI pcompose_conjugates_integer) auto ultimately show "algebraic (\ * x)" "algebraic (-\ * x)" by (intro algebraicI[of p']; simp)+ qed lemma algebraic_times_i_iff: "algebraic (\ * x) \ algebraic x" using algebraic_times_i[of x] algebraic_times_i[of "\ * x"] by auto lemma ratpolyE: assumes "\i. poly.coeff p i \ \" obtains q where "p = map_poly of_rat q" proof - have "\i\{..Polynomial.degree p}. \x. poly.coeff p i = of_rat x" using assms by (auto simp: Rats_def) from bchoice[OF this] obtain f where f: "\i. i \ Polynomial.degree p \ poly.coeff p i = of_rat (f i)" by blast define q where "q = Poly (map f [0..Auxiliary material\ theory Power_Sum_Polynomials_Library imports "Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized" "Symmetric_Polynomials.Symmetric_Polynomials" "HOL-Computational_Algebra.Computational_Algebra" begin +unbundle multiset.lifting + subsection \Miscellaneous\ lemma atLeastAtMost_nat_numeral: "atLeastAtMost m (numeral k :: nat) = (if m \ numeral k then insert (numeral k) (atLeastAtMost m (pred_numeral k)) else {})" by (simp add: numeral_eq_Suc atLeastAtMostSuc_conv) lemma sum_in_Rats [intro]: "(\x. x \ A \ f x \ \) \ sum f A \ \" by (induction A rule: infinite_finite_induct) auto (* TODO Move *) lemma (in monoid_mult) prod_list_distinct_conv_prod_set: "distinct xs \ prod_list (map f xs) = prod f (set xs)" by (induct xs) simp_all lemma (in monoid_mult) interv_prod_list_conv_prod_set_nat: "prod_list (map f [m..i = 0..< length xs. xs ! i)" using interv_prod_list_conv_prod_set_nat [of "(!) xs" 0 "length xs"] by (simp add: map_nth) lemma gcd_poly_code_aux_reduce: "gcd_poly_code_aux p 0 = normalize p" "q \ 0 \ gcd_poly_code_aux p q = gcd_poly_code_aux q (primitive_part (pseudo_mod p q))" by (subst gcd_poly_code_aux.simps; simp)+ lemma coprimeI_primes: fixes a b :: "'a :: factorial_semiring" assumes "a \ 0 \ b \ 0" assumes "\p. prime p \ p dvd a \ p dvd b \ False" shows "coprime a b" proof (rule coprimeI) fix d assume d: "d dvd a" "d dvd b" with assms(1) have [simp]: "d \ 0" by auto show "is_unit d" proof (rule ccontr) assume "\is_unit d" then obtain p where p: "prime p" "p dvd d" using prime_divisor_exists[of d] by auto from assms(2)[of p] and p and d show False using dvd_trans by auto qed qed lemma coprime_pderiv_imp_squarefree: assumes "coprime p (pderiv p)" shows "squarefree p" proof (rule squarefreeI) fix d assume d: "d ^ 2 dvd p" then obtain q where q: "p = d ^ 2 * q" by (elim dvdE) hence "d dvd p" "d dvd pderiv p" by (auto simp: pderiv_mult pderiv_power_Suc numeral_2_eq_2) with assms show "is_unit d" using not_coprimeI by blast qed lemma squarefree_field_poly_iff: fixes p :: "'a :: {field_char_0,euclidean_ring_gcd,semiring_gcd_mult_normalize} poly" assumes [simp]: "p \ 0" shows "squarefree p \ coprime p (pderiv p)" proof assume "squarefree p" show "coprime p (pderiv p)" proof (rule coprimeI_primes) fix d assume d: "d dvd p" "d dvd pderiv p" "prime d" from d(1) obtain q where q: "p = d * q" by (elim dvdE) from d(2) and q have "d dvd q * pderiv d" by (simp add: pderiv_mult dvd_add_right_iff) with \prime d\ have "d dvd q \ d dvd pderiv d" using prime_dvd_mult_iff by blast thus False proof assume "d dvd q" hence "d ^ 2 dvd p" by (auto simp: q power2_eq_square) with \squarefree p\ show False using d(3) not_prime_unit squarefreeD by blast next assume "d dvd pderiv d" hence "Polynomial.degree d = 0" by simp moreover have "d \ 0" using d by auto ultimately show False using d(3) is_unit_iff_degree not_prime_unit by blast qed qed auto qed (use coprime_pderiv_imp_squarefree[of p] in auto) lemma coprime_pderiv_imp_rsquarefree: assumes "coprime (p :: 'a :: field_char_0 poly) (pderiv p)" shows "rsquarefree p" unfolding rsquarefree_roots proof safe fix x assume "poly p x = 0" "poly (pderiv p) x = 0" hence "[:-x, 1:] dvd p" "[:-x, 1:] dvd pderiv p" by (auto simp: poly_eq_0_iff_dvd) with assms have "is_unit [:-x, 1:]" using not_coprimeI by blast thus False by auto qed lemma poly_of_nat [simp]: "poly (of_nat n) x = of_nat n" by (induction n) auto lemma poly_of_int [simp]: "poly (of_int n) x = of_int n" by (cases n) auto lemma order_eq_0_iff: "p \ 0 \ order x p = 0 \ poly p x \ 0" by (auto simp: order_root) lemma order_pos_iff: "p \ 0 \ order x p > 0 \ poly p x = 0" by (auto simp: order_root) lemma order_prod: assumes "\x. x \ A \ f x \ 0" shows "order x (\y\A. f y) = (\y\A. order x (f y))" using assms by (induction A rule: infinite_finite_induct) (auto simp: order_mult) lemma order_prod_mset: assumes "0 \# A" shows "order x (prod_mset A) = sum_mset (image_mset (order x) A)" using assms by (induction A) (auto simp: order_mult) lemma order_prod_list: assumes "0 \ set xs" shows "order x (prod_list xs) = sum_list (map (order x) xs)" using assms by (induction xs) (auto simp: order_mult) lemma order_power: "p \ 0 \ order x (p ^ n) = n * order x p" by (induction n) (auto simp: order_mult) lemma smult_0_right [simp]: "MPoly_Type.smult p 0 = 0" by (transfer, transfer) auto lemma mult_smult_right [simp]: fixes c :: "'a :: comm_semiring_0" shows "p * MPoly_Type.smult c q = MPoly_Type.smult c (p * q)" by (simp add: smult_conv_mult mult_ac) lemma mapping_single_eq_iff [simp]: "Poly_Mapping.single a b = Poly_Mapping.single c d \ b = 0 \ d = 0 \ a = c \ b = d" by transfer (unfold fun_eq_iff when_def, metis) lemma monom_of_set_plus_monom_of_set: assumes "A \ B = {}" "finite A" "finite B" shows "monom_of_set A + monom_of_set B = monom_of_set (A \ B)" using assms by transfer (auto simp: fun_eq_iff) lemma mpoly_monom_0_eq_Const: "monom 0 c = Const c" by (intro mpoly_eqI) (auto simp: coeff_monom when_def mpoly_coeff_Const) lemma mpoly_Const_0 [simp]: "Const 0 = 0" by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const mpoly_coeff_0) lemma mpoly_Const_1 [simp]: "Const 1 = 1" by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const mpoly_coeff_1) lemma mpoly_Const_uminus: "Const (-a) = -Const a" by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const) lemma mpoly_Const_add: "Const (a + b) = Const a + Const b" by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const) lemma mpoly_Const_mult: "Const (a * b) = Const a * Const b" unfolding mpoly_monom_0_eq_Const [symmetric] mult_monom by simp lemma mpoly_Const_power: "Const (a ^ n) = Const a ^ n" by (induction n) (auto simp: mpoly_Const_mult) lemma of_nat_mpoly_eq: "of_nat n = Const (of_nat n)" proof (induction n) case 0 have "0 = (Const 0 :: 'a mpoly)" by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const) thus ?case by simp next case (Suc n) have "1 + Const (of_nat n) = Const (1 + of_nat n)" by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const mpoly_coeff_1) thus ?case using Suc by auto qed lemma insertion_of_nat [simp]: "insertion f (of_nat n) = of_nat n" by (simp add: of_nat_mpoly_eq) lemma insertion_monom_of_set [simp]: "insertion f (monom (monom_of_set X) c) = c * (\i\X. f i)" proof (cases "finite X") case [simp]: True have "insertion f (monom (monom_of_set X) c) = c * (\a. f a ^ (if a \ X then 1 else 0))" by (auto simp: lookup_monom_of_set) also have "(\a. f a ^ (if a \ X then 1 else 0)) = (\i\X. f i ^ (if i \ X then 1 else 0))" by (intro Prod_any.expand_superset) auto also have "\ = (\i\X. f i)" by (intro prod.cong) auto finally show ?thesis . qed (auto simp: lookup_monom_of_set) (* TODO: Move! Version in AFP is too weak! *) lemma symmetric_mpoly_symmetric_sum: assumes "\\. \ permutes A \ g \ permutes X" assumes "\x \. x \ X \ \ permutes A \ mpoly_map_vars \ (f x) = f (g \ x)" shows "symmetric_mpoly A (\x\X. f x)" unfolding symmetric_mpoly_def proof safe fix \ assume \: "\ permutes A" have "mpoly_map_vars \ (sum f X) = (\x\X. mpoly_map_vars \ (f x))" by simp also have "\ = (\x\X. f (g \ x))" by (intro sum.cong assms \ refl) also have "\ = (\x\g \`X. f x)" using assms(1)[OF \] by (subst sum.reindex) (auto simp: permutes_inj_on) also have "g \ ` X = X" using assms(1)[OF \] by (simp add: permutes_image) finally show "mpoly_map_vars \ (sum f X) = sum f X" . qed lemma sym_mpoly_0 [simp]: assumes "finite A" shows "sym_mpoly A 0 = 1" using assms by (transfer, transfer) (auto simp: fun_eq_iff when_def) lemma sym_mpoly_eq_0 [simp]: assumes "k > card A" shows "sym_mpoly A k = 0" proof (transfer fixing: A k, transfer fixing: A k, intro ext) fix mon have "\(finite A \ (\Y\A. card Y = k \ mon = monom_of_set Y))" proof safe fix Y assume Y: "finite A" "Y \ A" "k = card Y" "mon = monom_of_set Y" hence "card Y \ card A" by (intro card_mono) auto with Y and assms show False by simp qed thus "(if finite A \ (\Y\A. card Y = k \ mon = monom_of_set Y) then 1 else 0) = 0" by auto qed lemma coeff_sym_mpoly_monom_of_set_eq_0: assumes "finite X" "Y \ X" "card Y \ k" shows "MPoly_Type.coeff (sym_mpoly X k) (monom_of_set Y) = 0" using assms finite_subset[of _ X] by (auto simp: coeff_sym_mpoly) lemma coeff_sym_mpoly_monom_of_set_eq_0': assumes "finite X" "\Y \ X" "finite Y" shows "MPoly_Type.coeff (sym_mpoly X k) (monom_of_set Y) = 0" using assms finite_subset[of _ X] by (auto simp: coeff_sym_mpoly) subsection \The set of roots of a univariate polynomial\ lift_definition poly_roots :: "'a :: idom poly \ 'a multiset" is "\p x. if p = 0 then 0 else order x p" proof - fix p :: "'a poly" show "finite {x. 0 < (if p = 0 then 0 else order x p)}" by (cases "p = 0") (auto simp: order_pos_iff poly_roots_finite) qed lemma poly_roots_0 [simp]: "poly_roots 0 = {#}" by transfer auto lemma poly_roots_1 [simp]: "poly_roots 1 = {#}" by transfer auto lemma count_poly_roots [simp]: assumes "p \ 0" shows "count (poly_roots p) x = order x p" using assms by transfer auto lemma in_poly_roots_iff [simp]: "p \ 0 \ x \# poly_roots p \ poly p x = 0" by (subst count_greater_zero_iff [symmetric], subst count_poly_roots) (auto simp: order_pos_iff) lemma set_mset_poly_roots: "p \ 0 \ set_mset (poly_roots p) = {x. poly p x = 0}" using in_poly_roots_iff[of p] by blast lemma count_poly_roots': "count (poly_roots p) x = (if p = 0 then 0 else order x p)" by transfer' auto lemma poly_roots_const [simp]: "poly_roots [:c:] = {#}" by (intro multiset_eqI) (auto simp: count_poly_roots' order_eq_0_iff) lemma poly_roots_linear [simp]: "poly_roots [:-x, 1:] = {#x#}" by (intro multiset_eqI) (auto simp: count_poly_roots' order_eq_0_iff) lemma poly_roots_monom [simp]: "c \ 0 \ poly_roots (Polynomial.monom c n) = replicate_mset n 0" by (intro multiset_eqI) (auto simp: count_poly_roots' order_eq_0_iff poly_monom) lemma poly_roots_smult [simp]: "c \ 0 \ poly_roots (Polynomial.smult c p) = poly_roots p" by (intro multiset_eqI) (auto simp: count_poly_roots' order_smult) lemma poly_roots_mult: "p \ 0 \ q \ 0 \ poly_roots (p * q) = poly_roots p + poly_roots q" by (intro multiset_eqI) (auto simp: count_poly_roots' order_mult) lemma poly_roots_prod: assumes "\x. x \ A \ f x \ 0" shows "poly_roots (prod f A) = (\x\A. poly_roots (f x))" using assms by (induction A rule: infinite_finite_induct) (auto simp: poly_roots_mult) lemma poly_roots_prod_mset: assumes "0 \# A" shows "poly_roots (prod_mset A) = sum_mset (image_mset poly_roots A)" using assms by (induction A) (auto simp: poly_roots_mult) lemma poly_roots_prod_list: assumes "0 \ set xs" shows "poly_roots (prod_list xs) = sum_list (map poly_roots xs)" using assms by (induction xs) (auto simp: poly_roots_mult) lemma poly_roots_power: "p \ 0 \ poly_roots (p ^ n) = repeat_mset n (poly_roots p)" by (induction n) (auto simp: poly_roots_mult) lemma rsquarefree_poly_roots_eq: assumes "rsquarefree p" shows "poly_roots p = mset_set {x. poly p x = 0}" proof (rule multiset_eqI) fix x :: 'a from assms show "count (poly_roots p) x = count (mset_set {x. poly p x = 0}) x" by (cases "poly p x = 0") (auto simp: poly_roots_finite order_eq_0_iff rsquarefree_def) qed lemma rsquarefree_imp_distinct_roots: assumes "rsquarefree p" and "mset xs = poly_roots p" shows "distinct xs" proof (cases "p = 0") case [simp]: False have *: "mset xs = mset_set {x. poly p x = 0}" using assms by (simp add: rsquarefree_poly_roots_eq) hence "set_mset (mset xs) = set_mset (mset_set {x. poly p x = 0})" by (simp only: ) hence [simp]: "set xs = {x. poly p x = 0}" by (simp add: poly_roots_finite) from * show ?thesis by (subst distinct_count_atmost_1) (auto simp: poly_roots_finite) qed (use assms in auto) lemma poly_roots_factorization: fixes p c A assumes [simp]: "c \ 0" defines "p \ Polynomial.smult c (prod_mset (image_mset (\x. [:-x, 1:]) A))" shows "poly_roots p = A" proof - have "poly_roots p = poly_roots (\x\#A. [:-x, 1:])" by (auto simp: p_def) also have "\ = A" by (subst poly_roots_prod_mset) (auto simp: image_mset.compositionality o_def) finally show ?thesis . qed lemma fundamental_theorem_algebra_factorized': fixes p :: "complex poly" shows "p = Polynomial.smult (Polynomial.lead_coeff p) (prod_mset (image_mset (\x. [:-x, 1:]) (poly_roots p)))" proof (cases "p = 0") case [simp]: False obtain xs where xs: "Polynomial.smult (Polynomial.lead_coeff p) (\x\xs. [:-x, 1:]) = p" "length xs = Polynomial.degree p" using fundamental_theorem_algebra_factorized[of p] by auto define A where "A = mset xs" note xs(1) also have "(\x\xs. [:-x, 1:]) = prod_mset (image_mset (\x. [:-x, 1:]) A)" unfolding A_def by (induction xs) auto finally have *: "Polynomial.smult (Polynomial.lead_coeff p) (\x\#A. [:- x, 1:]) = p" . also have "A = poly_roots p" using poly_roots_factorization[of "Polynomial.lead_coeff p" A] by (subst * [symmetric]) auto finally show ?thesis .. qed auto lemma poly_roots_eq_imp_eq: fixes p q :: "complex poly" assumes "Polynomial.lead_coeff p = Polynomial.lead_coeff q" assumes "poly_roots p = poly_roots q" shows "p = q" proof (cases "p = 0 \ q = 0") case False hence [simp]: "p \ 0" "q \ 0" by auto have "p = Polynomial.smult (Polynomial.lead_coeff p) (prod_mset (image_mset (\x. [:-x, 1:]) (poly_roots p)))" by (rule fundamental_theorem_algebra_factorized') also have "\ = Polynomial.smult (Polynomial.lead_coeff q) (prod_mset (image_mset (\x. [:-x, 1:]) (poly_roots q)))" by (simp add: assms) also have "\ = q" by (rule fundamental_theorem_algebra_factorized' [symmetric]) finally show ?thesis . qed (use assms in auto) lemma Sum_any_zeroI': "(\x. P x \ f x = 0) \ Sum_any (\x. f x when P x) = 0" by (auto simp: Sum_any.expand_set) (* TODO: This was not really needed here, but it is important nonetheless. It should go in the Symmetric_Polynomials entry. *) lemma sym_mpoly_insert: assumes "finite X" "x \ X" shows "(sym_mpoly (insert x X) (Suc k) :: 'a :: semiring_1 mpoly) = monom (monom_of_set {x}) 1 * sym_mpoly X k + sym_mpoly X (Suc k)" (is "?lhs = ?A + ?B") proof (rule mpoly_eqI) fix mon show "coeff ?lhs mon = coeff (?A + ?B) mon" proof (cases "\i. lookup mon i \ 1 \ (i \ insert x X \ lookup mon i = 0)") case False then obtain i where i: "lookup mon i > 1 \ i \ insert x X \ lookup mon i > 0" by (auto simp: not_le) have "coeff ?A mon = prod_fun (coeff (monom (monom_of_set {x}) 1)) (coeff (sym_mpoly X k)) mon" by (simp add: coeff_mpoly_times) also have "\ = (\l. \q. coeff (monom (monom_of_set {x}) 1) l * coeff (sym_mpoly X k) q when mon = l + q)" unfolding prod_fun_def by (intro Sum_any.cong, subst Sum_any_right_distrib, force) (auto simp: Sum_any_right_distrib when_def intro!: Sum_any.cong) also have "\ = 0" proof (rule Sum_any_zeroI, rule Sum_any_zeroI') fix ma mb assume *: "mon = ma + mb" show "coeff (monom (monom_of_set {x}) (1::'a)) ma * coeff (sym_mpoly X k) mb = 0" proof (cases "i = x") case [simp]: True show ?thesis proof (cases "lookup mb i > 0") case True hence "coeff (sym_mpoly X k) mb = 0" using \x \ X\ by (auto simp: coeff_sym_mpoly lookup_monom_of_set split: if_splits) thus ?thesis using mult_not_zero by blast next case False hence "coeff (monom (monom_of_set {x}) 1) ma = 0" using i by (auto simp: coeff_monom when_def * lookup_add) thus ?thesis using mult_not_zero by blast qed next case [simp]: False show ?thesis proof (cases "lookup ma i > 0") case False hence "lookup mb i = lookup mon i" using * by (auto simp: lookup_add) hence "coeff (sym_mpoly X k) mb = 0" using i by (auto simp: coeff_sym_mpoly lookup_monom_of_set split: if_splits) thus ?thesis using mult_not_zero by blast next case True hence "coeff (monom (monom_of_set {x}) 1) ma = 0" using i by (auto simp: coeff_monom when_def * lookup_add) thus ?thesis using mult_not_zero by blast qed qed qed finally have "coeff ?A mon = 0" . moreover from False have "coeff ?lhs mon = 0" by (subst coeff_sym_mpoly) (auto simp: lookup_monom_of_set split: if_splits) moreover from False have "coeff (sym_mpoly X (Suc k)) mon = 0" by (subst coeff_sym_mpoly) (auto simp: lookup_monom_of_set split: if_splits) ultimately show ?thesis by auto next case True define A where "A = keys mon" have A: "A \ insert x X" using True by (auto simp: A_def) have [simp]: "mon = monom_of_set A" unfolding A_def using True by transfer (force simp: fun_eq_iff le_Suc_eq) have "finite A" using finite_subset A assms by blast show ?thesis proof (cases "x \ A") case False have "coeff ?A mon = prod_fun (coeff (monom (monom_of_set {x}) 1)) (coeff (sym_mpoly X k)) (monom_of_set A)" by (simp add: coeff_mpoly_times) also have "\ = (\l. \q. coeff (monom (monom_of_set {x}) 1) l * coeff (sym_mpoly X k) q when monom_of_set A = l + q)" unfolding prod_fun_def by (intro Sum_any.cong, subst Sum_any_right_distrib, force) (auto simp: Sum_any_right_distrib when_def intro!: Sum_any.cong) also have "\ = 0" proof (rule Sum_any_zeroI, rule Sum_any_zeroI') fix ma mb assume *: "monom_of_set A = ma + mb" hence "keys ma \ A" using \finite A\ by transfer (auto simp: fun_eq_iff split: if_splits) thus "coeff (monom (monom_of_set {x}) (1::'a)) ma * coeff (sym_mpoly X k) mb = 0" using \x \ A\ by (auto simp: coeff_monom when_def) qed finally show ?thesis using False A assms finite_subset[of _ "insert x X"] finite_subset[of _ X] by (auto simp: coeff_sym_mpoly) next case True have "mon = monom_of_set {x} + monom_of_set (A - {x})" using \x \ A\ \finite A\ by (auto simp: monom_of_set_plus_monom_of_set) also have "coeff ?A \ = coeff (sym_mpoly X k) (monom_of_set (A - {x}))" by (subst coeff_monom_mult) auto also have "\ = (if card A = Suc k then 1 else 0)" proof (cases "card A = Suc k") case True thus ?thesis using assms \finite A\ \x \ A\ A by (subst coeff_sym_mpoly_monom_of_set) auto next case False thus ?thesis using assms \x \ A\ A \finite A\ card_Suc_Diff1[of A x] by (subst coeff_sym_mpoly_monom_of_set_eq_0) auto qed moreover have "coeff ?B (monom_of_set A) = 0" using assms \x \ A\ \finite A\ by (subst coeff_sym_mpoly_monom_of_set_eq_0') auto moreover have "coeff ?lhs (monom_of_set A) = (if card A = Suc k then 1 else 0)" using assms A \finite A\ finite_subset[of _ "insert x X"] by (auto simp: coeff_sym_mpoly) ultimately show ?thesis by simp qed qed qed +lifting_update multiset.lifting +lifting_forget multiset.lifting end \ No newline at end of file diff --git a/thys/Progress_Tracking/Auxiliary.thy b/thys/Progress_Tracking/Auxiliary.thy --- a/thys/Progress_Tracking/Auxiliary.thy +++ b/thys/Progress_Tracking/Auxiliary.thy @@ -1,406 +1,411 @@ section \Auxiliary Lemmas\ (*<*) theory Auxiliary imports "HOL-Library.Multiset" "Nested_Multisets_Ordinals.Signed_Multiset" "HOL-Library.Linear_Temporal_Logic_on_Streams" begin (*>*) +unbundle multiset.lifting + subsection\General\ lemma sum_list_hd_tl: fixes xs :: "(_ :: group_add) list" shows "xs \ [] \ sum_list (tl xs) = (- hd xs) + sum_list xs" by (cases xs) simp_all lemma finite_distinct_bounded: "finite A \ finite {xs. distinct xs \ set xs \ A}" apply (rule finite_subset[of _ "\n \ {0 .. card A}. {xs. length xs = n \ distinct xs \ set xs \ A}"]) subgoal by clarsimp (metis card_mono distinct_card) subgoal by auto done subsection\Sums\ lemma Sum_eq_pick_changed_elem: assumes "finite M" and "m \ M" "f m = g m + \" and "\n. n \ m \ n \ M \ f n = g n" shows "(\x\M. f x) = (\x\M. g x) + \" using assms proof (induct M arbitrary: m rule: finite_induct) case empty then show ?case by simp next case (insert x F) then show ?case proof (cases "x=m") case True with insert have "sum f F = sum g F" by (intro sum.cong[OF refl]) force with insert True show ?thesis by (auto simp: add.commute add.left_commute) next case False with insert show ?thesis by (auto simp: add.assoc) qed qed lemma sum_pos_ex_elem_pos: "(0::int) < (\m\M. f m) \ \m\M. 0 < f m" by (meson not_le sum_nonpos) lemma sum_if_distrib_add: "finite A \ b \ A \ (\a\A. if a=b then X b + Y a else X a) = (\a\A. X a) + Y b" by (simp add: Sum_eq_pick_changed_elem) subsection\Partial Orders\ lemma (in order) order_finite_set_exists_foundation: fixes t :: 'a assumes "finite M" and "t \ M" shows "\s\M. s \ t \ (\u\M. \ u < s)" using assms by (simp add: dual_order.strict_iff_order finite_has_minimal2) lemma order_finite_set_obtain_foundation: fixes t :: "_ :: order" assumes "finite M" and "t \ M" obtains s where "s \ M" "s \ t" "\u\M. \ u < s" using assms order_finite_set_exists_foundation by blast subsection\Multisets\ lemma finite_nonzero_count: "finite {t. count M t > 0}" using count by auto lemma finite_count[simp]: "finite {t. count M t > i}" by (rule finite_subset[OF _ finite_nonzero_count[of M]]) (auto simp only: set_mset_def) subsection\Signed Multisets\ lemma zcount_zmset_of_nonneg[simp]: "0 \ zcount (zmset_of M) t" by simp lemma finite_zcount_pos[simp]: "finite {t. zcount M t > 0}" apply transfer subgoal for M apply (rule finite_subset[OF _ finite_Un[THEN iffD2, OF conjI[OF finite_nonzero_count finite_nonzero_count]], of _ "fst M" "snd M"]) apply (auto simp only: set_mset_def fst_conv snd_conv split: prod.splits) done done lemma finite_zcount_neg[simp]: "finite {t. zcount M t < 0}" apply transfer subgoal for M apply (rule finite_subset[OF _ finite_Un[THEN iffD2, OF conjI[OF finite_nonzero_count finite_nonzero_count]], of _ "fst M" "snd M"]) apply (auto simp only: set_mset_def fst_conv snd_conv split: prod.splits) done done lemma pos_zcount_in_zmset: "0 < zcount M x \ x \#\<^sub>z M" by (simp add: zcount_inI) lemma zmset_elem_nonneg: "x \#\<^sub>z M \ (\x. x \#\<^sub>z M \ 0 \ zcount M x) \ 0 < zcount M x" by (simp add: order.order_iff_strict zcount_eq_zero_iff) lemma zero_le_sum_single: "0 \ zcount (\x\M. {#f x#}\<^sub>z) t" by (induct M rule: infinite_finite_induct) auto lemma mem_zmset_of[simp]: "x \#\<^sub>z zmset_of M \ x \# M" by (simp add: set_zmset_def) lemma mset_neg_minus: "mset_neg (abs_zmultiset (Mp,Mn)) = Mn-Mp" by (simp add: mset_neg.abs_eq) lemma mset_pos_minus: "mset_pos (abs_zmultiset (Mp,Mn)) = Mp-Mn" by (simp add: mset_pos.abs_eq) lemma mset_neg_sum_set: "(\m. m \ M \ mset_neg (f m) = {#}) \ mset_neg (\m\M. f m) = {#}" by (induct M rule: infinite_finite_induct) auto lemma mset_neg_empty_iff: "mset_neg M = {#} \ (\t. 0 \ zcount M t)" apply rule subgoal by (metis add.commute add.right_neutral mset_pos_as_neg zcount_zmset_of_nonneg zmset_of_empty) subgoal apply (induct rule: zmultiset.abs_induct) subgoal for y apply (induct y) apply (subst mset_neg_minus) - apply transfer + apply transfer' apply (simp add: Diff_eq_empty_iff_mset mset_subset_eqI) done done done lemma mset_neg_zcount_nonneg: "mset_neg M = {#} \ 0 \ zcount M t" by (subst (asm) mset_neg_empty_iff) simp lemma in_zmset_conv_pos_neg_disj: "x \#\<^sub>z M \ x \# mset_pos M \ x \# mset_neg M" by (metis count_mset_pos in_diff_zcount mem_zmset_of mset_pos_neg_partition nat_code(2) not_in_iff zcount_ne_zero_iff) lemma in_zmset_notin_mset_pos[simp]: "x \#\<^sub>z M \ x \# mset_pos M \ x \# mset_neg M" by (auto simp: in_zmset_conv_pos_neg_disj) lemma in_zmset_notin_mset_neg[simp]: "x \#\<^sub>z M \ x \# mset_neg M \ x \# mset_pos M" by (auto simp: in_zmset_conv_pos_neg_disj) lemma in_mset_pos_in_zmset: "x \# mset_pos M \ x \#\<^sub>z M" by (auto intro: iffD2[OF in_zmset_conv_pos_neg_disj]) lemma in_mset_neg_in_zmset: "x \# mset_neg M \ x \#\<^sub>z M" by (auto intro: iffD2[OF in_zmset_conv_pos_neg_disj]) lemma set_zmset_eq_set_mset_union: "set_zmset M = set_mset (mset_pos M) \ set_mset (mset_neg M)" by (auto dest: in_mset_pos_in_zmset in_mset_neg_in_zmset) lemma member_mset_pos_iff_zcount: "x \# mset_pos M \ 0 < zcount M x" using not_in_iff pos_zcount_in_zmset by force lemma member_mset_neg_iff_zcount: "x \# mset_neg M \ zcount M x < 0" by (metis member_mset_pos_iff_zcount mset_pos_uminus neg_le_0_iff_le not_le zcount_uminus) lemma mset_pos_mset_neg_disjoint[simp]: "set_mset (mset_pos \) \ set_mset (mset_neg \) = {}" by (auto simp: member_mset_pos_iff_zcount member_mset_neg_iff_zcount) lemma zcount_sum: "zcount (\M\MM. f M) t = (\M\MM. zcount (f M) t)" by (induct MM rule: infinite_finite_induct) auto lemma zcount_filter_invariant: "zcount {# t'\#\<^sub>zM. t'=t #} t = zcount M t" by auto lemma in_filter_zmset_in_zmset[simp]: "x \#\<^sub>z filter_zmset P M \ x \#\<^sub>z M" by (metis count_filter_zmset zcount_ne_zero_iff) lemma pos_filter_zmset_pos_zmset[simp]: "0 < zcount (filter_zmset P M) x \ 0 < zcount M x" by (metis (full_types) count_filter_zmset less_irrefl) lemma neg_filter_zmset_neg_zmset[simp]: "0 > zcount (filter_zmset P M) x \ 0 > zcount M x" by (metis (full_types) count_filter_zmset less_irrefl) lift_definition update_zmultiset :: "'t zmultiset \ 't \ int \ 't zmultiset" is "\(A,B) T D.(if D>0 then (A + replicate_mset (nat D) T, B) else (A,B + replicate_mset (nat (-D)) T))" by (auto simp: equiv_zmset_def if_split) lemma zcount_update_zmultiset: "zcount (update_zmultiset M t n) t' = zcount M t' + (if t = t' then n else 0)" by transfer auto lemma (in order) order_zmset_exists_foundation: fixes t :: 'a assumes "0 < zcount M t" shows "\s. s \ t \ 0 < zcount M s \ (\u. 0 < zcount M u \ \ u < s)" using assms proof - let ?M = "{t. 0 < zcount M t}" from assms have "t \ ?M" by simp then have "\s\?M. s \ t \ (\u\?M. \ u < s)" by - (drule order_finite_set_exists_foundation[rotated 1], auto) then show ?thesis by auto qed lemma (in order) order_zmset_exists_foundation': fixes t :: 'a assumes "0 < zcount M t" shows "\s. s \ t \ 0 < zcount M s \ (\u 0)" using assms order_zmset_exists_foundation by (meson le_less_linear) lemma (in order) order_zmset_exists_foundation_neg: fixes t :: 'a assumes "zcount M t < 0" shows "\s. s \ t \ zcount M s < 0 \ (\u. zcount M u < 0 \ \ u < s)" using assms proof - let ?M = "{t. zcount M t < 0}" from assms have "t \ ?M" by simp then have "\s\?M. s \ t \ (\u\?M. \ u < s)" by - (drule order_finite_set_exists_foundation[rotated 1], auto) then show ?thesis by auto qed lemma (in order) order_zmset_exists_foundation_neg': fixes t :: 'a assumes "zcount M t < 0" shows "\s. s \ t \ zcount M s < 0 \ (\u zcount M u)" using assms order_zmset_exists_foundation_neg by (meson le_less_linear) lemma (in order) elem_order_zmset_exists_foundation: fixes x :: 'a assumes "x \#\<^sub>z M" shows "\s\#\<^sub>zM. s \ x \ (\u\#\<^sub>zM. \ u < s)" by (rule order_finite_set_exists_foundation[OF finite_set_zmset, OF assms(1)]) subsubsection\Image of a Signed Multiset\ lift_definition image_zmset :: "('a \ 'b) \ 'a zmultiset \ 'b zmultiset" is "\f (M, N). (image_mset f M, image_mset f N)" by (auto simp: equiv_zmset_def simp flip: image_mset_union) syntax (ASCII) "_comprehension_zmset" :: "'a \ 'b \ 'b zmultiset \ 'a zmultiset" ("({#_/. _ :#z _#})") syntax "_comprehension_zmset" :: "'a \ 'b \ 'b zmultiset \ 'a zmultiset" ("({#_/. _ \#\<^sub>z _#})") translations "{#e. x \#\<^sub>z M#}" \ "CONST image_zmset (\x. e) M" lemma image_zmset_empty[simp]: "image_zmset f {#}\<^sub>z = {#}\<^sub>z" by transfer (auto simp: equiv_zmset_def) lemma image_zmset_single[simp]: "image_zmset f {#x#}\<^sub>z = {#f x#}\<^sub>z" by transfer (simp add: equiv_zmset_def) lemma image_zmset_union[simp]: "image_zmset f (M + N) = image_zmset f M + image_zmset f N" by transfer (auto simp: equiv_zmset_def) lemma image_zmset_Diff[simp]: "image_zmset f (A - B) = image_zmset f A - image_zmset f B" proof - have "image_zmset f (A - B + B) = image_zmset f (A - B) + image_zmset f B" using image_zmset_union by blast then show ?thesis by simp qed lemma mset_neg_image_zmset: "mset_neg M = {#} \ mset_neg (image_zmset f M) = {#}" unfolding multiset_eq_iff count_empty by transfer (auto simp add: image_mset_subseteq_mono mset_subset_eqI mset_subset_eq_count) lemma nonneg_zcount_image_zmset[simp]: "(\t. 0 \ zcount M t) \ 0 \ zcount (image_zmset f M) t" by (meson mset_neg_empty_iff mset_neg_image_zmset) lemma image_zmset_add_zmset[simp]: "image_zmset f (add_zmset t M) = add_zmset (f t) (image_zmset f M)" by transfer (auto simp: equiv_zmset_def) lemma pos_zcount_image_zmset[simp]: "(\t. 0 \ zcount M t) \ 0 < zcount M t \ 0 < zcount (image_zmset f M) (f t)" apply transfer subgoal for M t f apply (induct M) subgoal for Mp Mn apply simp apply (metis count_diff count_image_mset_ge_count image_mset_Diff less_le_trans subseteq_mset_def zero_less_diff) done done done lemma set_zmset_transfer[transfer_rule]: "(rel_fun (pcr_zmultiset (=)) (rel_set (=))) (\(Mp, Mn). set_mset Mp \ set_mset Mn - {x. count Mp x = count Mn x}) set_zmset" by (auto simp: rel_fun_def pcr_zmultiset_def cr_zmultiset_def rel_set_eq multiset.rel_eq set_zmset_def zcount.abs_eq count_eq_zero_iff[symmetric] simp del: zcount_ne_zero_iff) lemma zcount_image_zmset: "zcount (image_zmset f M) x = (\y \ f -` {x} \ set_zmset M. zcount M y)" apply (transfer fixing: f x) subgoal for M apply (cases M; clarify) subgoal for Mp Mn unfolding count_image_mset int_sum proof - have "(\x\f -` {x} \ set_mset Mp. int (count Mp x)) = (\x\f -` {x} \ (set_mset Mp \ set_mset Mn). int (count Mp x))" (is "?S1 = _") by (subst sum.same_carrier[where C="f -` {x} \ (set_mset Mp \ set_mset Mn)"]) (auto simp: count_eq_zero_iff) moreover have "(\x\f -` {x} \ set_mset Mn. int (count Mn x)) = (\x\f -` {x} \ (set_mset Mp \ set_mset Mn). int (count Mn x))"(is "?S2 = _") by (subst sum.same_carrier[where C="f -` {x} \ (set_mset Mp \ set_mset Mn)"]) (auto simp: count_eq_zero_iff) moreover have "(\x\f -` {x} \ (set_mset Mp \ set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x)) = (\x\f -` {x} \ (set_mset Mp \ set_mset Mn). int (count Mp x) - int (count Mn x))" (is "?S = _") by (subst sum.same_carrier[where C="f -` {x} \ (set_mset Mp \ set_mset Mn)"]) auto ultimately show "?S1 - ?S2 = ?S" by (auto simp: sum_subtractf) qed done done lemma zmset_empty_image_zmset_empty: "(\t. zcount M t = 0) \ zcount (image_zmset f M) t = 0" by (auto simp: zcount_image_zmset) lemma in_image_zmset_in_zmset: "t \#\<^sub>z image_zmset f M \ \t. t \#\<^sub>z M" by (rule ccontr) simp lemma zcount_image_zmset_zero: "(\m. m \#\<^sub>z M \ f m \ x) \ x \#\<^sub>z image_zmset f M" unfolding set_zmset_def by (simp add: zcount_image_zmset) (metis Int_emptyI sum.empty vimage_singleton_eq) lemma image_zmset_pre: "t \#\<^sub>z image_zmset f M \ \m. m \#\<^sub>z M \ f m = t" proof (rule ccontr) assume t: "t \#\<^sub>z image_zmset f M" assume "\m. m \#\<^sub>z M \ f m = t" then have "m \#\<^sub>z M \ \ f m = t" for m by blast then have "zcount (image_zmset f M) t = 0" by (meson t zcount_image_zmset_zero) with t show False by (meson zcount_ne_zero_iff) qed lemma pos_image_zmset_obtain_pre: "(\t. 0 \ zcount M t) \ 0 < zcount (image_zmset f M) t \ \m. 0 < zcount M m \ f m = t" proof - assume nonneg: "0 \ zcount M t" for t assume "0 < zcount (image_zmset f M) t" then have "t \#\<^sub>z image_zmset f M" by (simp add: pos_zcount_in_zmset) then obtain x where x: "x \#\<^sub>z M" "f x = t" by (auto dest: image_zmset_pre) with nonneg have "0 < zcount M x" by (meson zmset_elem_nonneg) with x show ?thesis by auto qed subsection\Streams\ definition relates :: "('a \ 'a \ bool) \ 'a stream \ bool" where "relates \ s = \ (shd s) (shd (stl s))" lemma relatesD[dest]: "relates P s \ P (shd s) (shd (stl s))" unfolding relates_def by simp lemma alw_relatesD[dest]: "alw (relates P) s \ P (shd s) (shd (stl s))" by auto lemma relatesI[intro]: "P (shd s) (shd (stl s)) \ relates P s" by (auto simp: relates_def) lemma alw_holds_smap_conv_comp: "alw (holds P) (smap f s) = alw (\s. (P o f) (shd s)) s" apply (rule iffI) apply (coinduction arbitrary: s) apply auto [] apply (coinduction arbitrary: s) apply auto done lemma alw_relates: "alw (relates P) s \ P (shd s) (shd (stl s)) \ alw (relates P) (stl s)" apply (rule iffI) apply (auto simp: relates_def dest: alwD) [] apply (coinduction arbitrary: s) apply (auto simp: relates_def) done subsection\Notation\ no_notation AND (infix "aand" 60) no_notation OR (infix "or" 60) no_notation IMPL (infix "imp" 60) notation AND (infixr "aand" 70) notation OR (infixr "or" 65) notation IMPL (infixr "imp" 60) +lifting_update multiset.lifting +lifting_forget multiset.lifting + (*<*) end (*>*) \ No newline at end of file