# HG changeset patch # User wenzelm # Date 1491077759 -7200 # Node ID 673a7b3379ec2e581b9cff89af156822b6d4ba1b # Parent 2fdd4431b30ecec508ee398a6a952fd9cfd363aa misc tuning and modernization; diff -r 2fdd4431b30e -r 673a7b3379ec src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Sat Apr 01 22:03:24 2017 +0200 +++ b/src/HOL/Library/Polynomial.thy Sat Apr 01 22:15:59 2017 +0200 @@ -8,50 +8,51 @@ section \Polynomials as type over a ring structure\ theory Polynomial -imports Main "~~/src/HOL/Deriv" "~~/src/HOL/Library/More_List" - "~~/src/HOL/Library/Infinite_Set" + imports + "~~/src/HOL/Deriv" + "~~/src/HOL/Library/More_List" + "~~/src/HOL/Library/Infinite_Set" begin subsection \Auxiliary: operations for lists (later) representing coefficients\ definition cCons :: "'a::zero \ 'a list \ 'a list" (infixr "##" 65) -where - "x ## xs = (if xs = [] \ x = 0 then [] else x # xs)" - -lemma cCons_0_Nil_eq [simp]: - "0 ## [] = []" + where "x ## xs = (if xs = [] \ x = 0 then [] else x # xs)" + +lemma cCons_0_Nil_eq [simp]: "0 ## [] = []" by (simp add: cCons_def) -lemma cCons_Cons_eq [simp]: - "x ## y # ys = x # y # ys" +lemma cCons_Cons_eq [simp]: "x ## y # ys = x # y # ys" by (simp add: cCons_def) -lemma cCons_append_Cons_eq [simp]: - "x ## xs @ y # ys = x # xs @ y # ys" +lemma cCons_append_Cons_eq [simp]: "x ## xs @ y # ys = x # xs @ y # ys" by (simp add: cCons_def) -lemma cCons_not_0_eq [simp]: - "x \ 0 \ x ## xs = x # xs" +lemma cCons_not_0_eq [simp]: "x \ 0 \ x ## xs = x # xs" by (simp add: cCons_def) lemma strip_while_not_0_Cons_eq [simp]: "strip_while (\x. x = 0) (x # xs) = x ## strip_while (\x. x = 0) xs" proof (cases "x = 0") - case False then show ?thesis by simp + case False + then show ?thesis by simp next - case True show ?thesis + case True + show ?thesis proof (induct xs rule: rev_induct) - case Nil with True show ?case by simp + case Nil + with True show ?case by simp next - case (snoc y ys) then show ?case + case (snoc y ys) + then show ?case by (cases "y = 0") (simp_all add: append_Cons [symmetric] del: append_Cons) qed qed -lemma tl_cCons [simp]: - "tl (x ## xs) = xs" +lemma tl_cCons [simp]: "tl (x ## xs) = xs" by (simp add: cCons_def) + subsection \Definition of type \poly\\ typedef (overloaded) 'a poly = "{f :: nat \ 'a::zero. \\<^sub>\ n. f n = 0}" @@ -73,8 +74,7 @@ subsection \Degree of a polynomial\ definition degree :: "'a::zero poly \ nat" -where - "degree p = (LEAST n. \i>n. coeff p i = 0)" + where "degree p = (LEAST n. \i>n. coeff p i = 0)" lemma coeff_eq_0: assumes "degree p < n" @@ -109,12 +109,10 @@ end -lemma coeff_0 [simp]: - "coeff 0 n = 0" +lemma coeff_0 [simp]: "coeff 0 n = 0" by transfer rule -lemma degree_0 [simp]: - "degree 0 = 0" +lemma degree_0 [simp]: "degree 0 = 0" by (rule order_antisym [OF degree_le le0]) simp lemma leading_coeff_neq_0: @@ -122,48 +120,52 @@ shows "coeff p (degree p) \ 0" proof (cases "degree p") case 0 - from \p \ 0\ have "\n. coeff p n \ 0" - by (simp add: poly_eq_iff) - then obtain n where "coeff p n \ 0" .. - hence "n \ degree p" by (rule le_degree) - with \coeff p n \ 0\ and \degree p = 0\ - show "coeff p (degree p) \ 0" by simp + from \p \ 0\ obtain n where "coeff p n \ 0" + by (auto simp add: poly_eq_iff) + then have "n \ degree p" + by (rule le_degree) + with \coeff p n \ 0\ and \degree p = 0\ show "coeff p (degree p) \ 0" + by simp next case (Suc n) - from \degree p = Suc n\ have "n < degree p" by simp - hence "\i>n. coeff p i \ 0" by (rule less_degree_imp) - then obtain i where "n < i" and "coeff p i \ 0" by fast - from \degree p = Suc n\ and \n < i\ have "degree p \ i" by simp - also from \coeff p i \ 0\ have "i \ degree p" by (rule le_degree) + from \degree p = Suc n\ have "n < degree p" + by simp + then have "\i>n. coeff p i \ 0" + by (rule less_degree_imp) + then obtain i where "n < i" and "coeff p i \ 0" + by blast + from \degree p = Suc n\ and \n < i\ have "degree p \ i" + by simp + also from \coeff p i \ 0\ have "i \ degree p" + by (rule le_degree) finally have "degree p = i" . with \coeff p i \ 0\ show "coeff p (degree p) \ 0" by simp qed -lemma leading_coeff_0_iff [simp]: - "coeff p (degree p) = 0 \ p = 0" - by (cases "p = 0", simp, simp add: leading_coeff_neq_0) +lemma leading_coeff_0_iff [simp]: "coeff p (degree p) = 0 \ p = 0" + by (cases "p = 0") (simp_all add: leading_coeff_neq_0) lemma eq_zero_or_degree_less: assumes "degree p \ n" and "coeff p n = 0" shows "p = 0 \ degree p < n" proof (cases n) case 0 - with \degree p \ n\ and \coeff p n = 0\ - have "coeff p (degree p) = 0" by simp + with \degree p \ n\ and \coeff p n = 0\ have "coeff p (degree p) = 0" + by simp then have "p = 0" by simp then show ?thesis .. next case (Suc m) - have "\i>n. coeff p i = 0" - using \degree p \ n\ by (simp add: coeff_eq_0) - then have "\i\n. coeff p i = 0" - using \coeff p n = 0\ by (simp add: le_less) - then have "\i>m. coeff p i = 0" - using \n = Suc m\ by (simp add: less_eq_Suc_le) + from \degree p \ n\ have "\i>n. coeff p i = 0" + by (simp add: coeff_eq_0) + with \coeff p n = 0\ have "\i\n. coeff p i = 0" + by (simp add: le_less) + with \n = Suc m\ have "\i>m. coeff p i = 0" + by (simp add: less_eq_Suc_le) then have "degree p \ m" by (rule degree_le) - then have "degree p < n" - using \n = Suc m\ by (simp add: less_Suc_eq_le) + with \n = Suc m\ have "degree p < n" + by (simp add: less_Suc_eq_le) then show ?thesis .. qed @@ -179,32 +181,26 @@ lemmas coeff_pCons = pCons.rep_eq -lemma coeff_pCons_0 [simp]: - "coeff (pCons a p) 0 = a" +lemma coeff_pCons_0 [simp]: "coeff (pCons a p) 0 = a" by transfer simp -lemma coeff_pCons_Suc [simp]: - "coeff (pCons a p) (Suc n) = coeff p n" +lemma coeff_pCons_Suc [simp]: "coeff (pCons a p) (Suc n) = coeff p n" by (simp add: coeff_pCons) -lemma degree_pCons_le: - "degree (pCons a p) \ Suc (degree p)" +lemma degree_pCons_le: "degree (pCons a p) \ Suc (degree p)" by (rule degree_le) (simp add: coeff_eq_0 coeff_pCons split: nat.split) -lemma degree_pCons_eq: - "p \ 0 \ degree (pCons a p) = Suc (degree p)" +lemma degree_pCons_eq: "p \ 0 \ degree (pCons a p) = Suc (degree p)" apply (rule order_antisym [OF degree_pCons_le]) apply (rule le_degree, simp) done -lemma degree_pCons_0: - "degree (pCons a 0) = 0" +lemma degree_pCons_0: "degree (pCons a 0) = 0" apply (rule order_antisym [OF _ le0]) apply (rule degree_le, simp add: coeff_pCons split: nat.split) done -lemma degree_pCons_eq_if [simp]: - "degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))" +lemma degree_pCons_eq_if [simp]: "degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))" apply (cases "p = 0", simp_all) apply (rule order_antisym [OF _ le0]) apply (rule degree_le, simp add: coeff_pCons split: nat.split) @@ -212,25 +208,25 @@ apply (rule le_degree, simp) done -lemma pCons_0_0 [simp]: - "pCons 0 0 = 0" +lemma pCons_0_0 [simp]: "pCons 0 0 = 0" by (rule poly_eqI) (simp add: coeff_pCons split: nat.split) -lemma pCons_eq_iff [simp]: - "pCons a p = pCons b q \ a = b \ p = q" +lemma pCons_eq_iff [simp]: "pCons a p = pCons b q \ a = b \ p = q" proof safe assume "pCons a p = pCons b q" - then have "coeff (pCons a p) 0 = coeff (pCons b q) 0" by simp - then show "a = b" by simp + then have "coeff (pCons a p) 0 = coeff (pCons b q) 0" + by simp + then show "a = b" + by simp next assume "pCons a p = pCons b q" - then have "\n. coeff (pCons a p) (Suc n) = - coeff (pCons b q) (Suc n)" by simp - then show "p = q" by (simp add: poly_eq_iff) + then have "coeff (pCons a p) (Suc n) = coeff (pCons b q) (Suc n)" for n + by simp + then show "p = q" + by (simp add: poly_eq_iff) qed -lemma pCons_eq_0_iff [simp]: - "pCons a p = 0 \ a = 0 \ p = 0" +lemma pCons_eq_0_iff [simp]: "pCons a p = 0 \ a = 0 \ p = 0" using pCons_eq_iff [of a p 0 0] by simp lemma pCons_cases [cases type: poly]: @@ -238,8 +234,8 @@ proof show "p = pCons (coeff p 0) (Abs_poly (\n. coeff p (Suc n)))" by transfer - (simp_all add: MOST_inj[where f=Suc and P="\n. p n = 0" for p] fun_eq_iff Abs_poly_inverse - split: nat.split) + (simp_all add: MOST_inj[where f=Suc and P="\n. p n = 0" for p] fun_eq_iff Abs_poly_inverse + split: nat.split) qed lemma pCons_induct [case_names 0 pCons, induct type: poly]: @@ -257,8 +253,8 @@ case False then have "degree (pCons a q) = Suc (degree q)" by (rule degree_pCons_eq) - then have "degree q < degree p" - using \p = pCons a q\ by simp + with \p = pCons a q\ have "degree q < degree p" + by simp then show "P q" by (rule less.hyps) qed @@ -270,8 +266,8 @@ case False with zero show ?thesis by simp qed - then show ?case - using \p = pCons a q\ by simp + with \p = pCons a q\ show ?case + by simp qed lemma degree_eq_zeroE: @@ -279,10 +275,13 @@ assumes "degree p = 0" obtains a where "p = pCons a 0" proof - - obtain a q where p: "p = pCons a q" by (cases p) - with assms have "q = 0" by (cases "q = 0") simp_all - with p have "p = pCons a 0" by simp - with that show thesis . + obtain a q where p: "p = pCons a q" + by (cases p) + with assms have "q = 0" + by (cases "q = 0") simp_all + with p have "p = pCons a 0" + by simp + then show thesis .. qed @@ -293,139 +292,112 @@ subsection \List-style syntax for polynomials\ -syntax - "_poly" :: "args \ 'a poly" ("[:(_):]") - +syntax "_poly" :: "args \ 'a poly" ("[:(_):]") translations - "[:x, xs:]" == "CONST pCons x [:xs:]" - "[:x:]" == "CONST pCons x 0" - "[:x:]" <= "CONST pCons x (_constrain 0 t)" + "[:x, xs:]" \ "CONST pCons x [:xs:]" + "[:x:]" \ "CONST pCons x 0" + "[:x:]" \ "CONST pCons x (_constrain 0 t)" subsection \Representation of polynomials by lists of coefficients\ primrec Poly :: "'a::zero list \ 'a poly" -where - [code_post]: "Poly [] = 0" -| [code_post]: "Poly (a # as) = pCons a (Poly as)" - -lemma Poly_replicate_0 [simp]: - "Poly (replicate n 0) = 0" + where + [code_post]: "Poly [] = 0" + | [code_post]: "Poly (a # as) = pCons a (Poly as)" + +lemma Poly_replicate_0 [simp]: "Poly (replicate n 0) = 0" by (induct n) simp_all -lemma Poly_eq_0: - "Poly as = 0 \ (\n. as = replicate n 0)" +lemma Poly_eq_0: "Poly as = 0 \ (\n. as = replicate n 0)" by (induct as) (auto simp add: Cons_replicate_eq) -lemma Poly_append_replicate_zero [simp]: - "Poly (as @ replicate n 0) = Poly as" +lemma Poly_append_replicate_zero [simp]: "Poly (as @ replicate n 0) = Poly as" by (induct as) simp_all -lemma Poly_snoc_zero [simp]: - "Poly (as @ [0]) = Poly as" +lemma Poly_snoc_zero [simp]: "Poly (as @ [0]) = Poly as" using Poly_append_replicate_zero [of as 1] by simp -lemma Poly_cCons_eq_pCons_Poly [simp]: - "Poly (a ## p) = pCons a (Poly p)" +lemma Poly_cCons_eq_pCons_Poly [simp]: "Poly (a ## p) = pCons a (Poly p)" by (simp add: cCons_def) -lemma Poly_on_rev_starting_with_0 [simp]: - assumes "hd as = 0" - shows "Poly (rev (tl as)) = Poly (rev as)" - using assms by (cases as) simp_all +lemma Poly_on_rev_starting_with_0 [simp]: "hd as = 0 \ Poly (rev (tl as)) = Poly (rev as)" + by (cases as) simp_all lemma degree_Poly: "degree (Poly xs) \ length xs" - by (induction xs) simp_all - -lemma coeff_Poly_eq [simp]: - "coeff (Poly xs) = nth_default 0 xs" + by (induct xs) simp_all + +lemma coeff_Poly_eq [simp]: "coeff (Poly xs) = nth_default 0 xs" by (induct xs) (simp_all add: fun_eq_iff coeff_pCons split: nat.splits) definition coeffs :: "'a poly \ 'a::zero list" -where - "coeffs p = (if p = 0 then [] else map (\i. coeff p i) [0 ..< Suc (degree p)])" - -lemma coeffs_eq_Nil [simp]: - "coeffs p = [] \ p = 0" + where "coeffs p = (if p = 0 then [] else map (\i. coeff p i) [0 ..< Suc (degree p)])" + +lemma coeffs_eq_Nil [simp]: "coeffs p = [] \ p = 0" by (simp add: coeffs_def) -lemma not_0_coeffs_not_Nil: - "p \ 0 \ coeffs p \ []" +lemma not_0_coeffs_not_Nil: "p \ 0 \ coeffs p \ []" by simp -lemma coeffs_0_eq_Nil [simp]: - "coeffs 0 = []" +lemma coeffs_0_eq_Nil [simp]: "coeffs 0 = []" by simp -lemma coeffs_pCons_eq_cCons [simp]: - "coeffs (pCons a p) = a ## coeffs p" +lemma coeffs_pCons_eq_cCons [simp]: "coeffs (pCons a p) = a ## coeffs p" proof - - { fix ms :: "nat list" and f :: "nat \ 'a" and x :: "'a" - assume "\m\set ms. m > 0" - then have "map (case_nat x f) ms = map f (map (\n. n - 1) ms)" - by (induct ms) (auto split: nat.split) - } - note * = this + have *: "\m\set ms. m > 0 \ map (case_nat x f) ms = map f (map (\n. n - 1) ms)" + for ms :: "nat list" and f :: "nat \ 'a" and x :: "'a" + by (induct ms) (auto split: nat.split) show ?thesis - by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt del: upt_Suc) + by (simp add: * coeffs_def upt_conv_Cons coeff_pCons map_decr_upt del: upt_Suc) qed lemma length_coeffs: "p \ 0 \ length (coeffs p) = degree p + 1" by (simp add: coeffs_def) -lemma coeffs_nth: - assumes "p \ 0" "n \ degree p" - shows "coeffs p ! n = coeff p n" - using assms unfolding coeffs_def by (auto simp del: upt_Suc) - -lemma coeff_in_coeffs: - "p \ 0 \ n \ degree p \ coeff p n \ set (coeffs p)" - using coeffs_nth [of p n, symmetric] - by (simp add: length_coeffs) - -lemma not_0_cCons_eq [simp]: - "p \ 0 \ a ## coeffs p = a # coeffs p" +lemma coeffs_nth: "p \ 0 \ n \ degree p \ coeffs p ! n = coeff p n" + by (auto simp: coeffs_def simp del: upt_Suc) + +lemma coeff_in_coeffs: "p \ 0 \ n \ degree p \ coeff p n \ set (coeffs p)" + using coeffs_nth [of p n, symmetric] by (simp add: length_coeffs) + +lemma not_0_cCons_eq [simp]: "p \ 0 \ a ## coeffs p = a # coeffs p" by (simp add: cCons_def) -lemma Poly_coeffs [simp, code abstype]: - "Poly (coeffs p) = p" +lemma Poly_coeffs [simp, code abstype]: "Poly (coeffs p) = p" by (induct p) auto -lemma coeffs_Poly [simp]: - "coeffs (Poly as) = strip_while (HOL.eq 0) as" +lemma coeffs_Poly [simp]: "coeffs (Poly as) = strip_while (HOL.eq 0) as" proof (induct as) - case Nil then show ?case by simp + case Nil + then show ?case by simp next case (Cons a as) - have "(\n. as \ replicate n 0) \ (\a\set as. a \ 0)" - using replicate_length_same [of as 0] by (auto dest: sym [of _ as]) + from replicate_length_same [of as 0] have "(\n. as \ replicate n 0) \ (\a\set as. a \ 0)" + by (auto dest: sym [of _ as]) with Cons show ?case by auto qed -lemma last_coeffs_not_0: - "p \ 0 \ last (coeffs p) \ 0" +lemma last_coeffs_not_0: "p \ 0 \ last (coeffs p) \ 0" by (induct p) (auto simp add: cCons_def) -lemma strip_while_coeffs [simp]: - "strip_while (HOL.eq 0) (coeffs p) = coeffs p" +lemma strip_while_coeffs [simp]: "strip_while (HOL.eq 0) (coeffs p) = coeffs p" by (cases "p = 0") (auto dest: last_coeffs_not_0 intro: strip_while_not_last) -lemma coeffs_eq_iff: - "p = q \ coeffs p = coeffs q" (is "?P \ ?Q") +lemma coeffs_eq_iff: "p = q \ coeffs p = coeffs q" + (is "?P \ ?Q") proof - assume ?P then show ?Q by simp + assume ?P + then show ?Q by simp next assume ?Q then have "Poly (coeffs p) = Poly (coeffs q)" by simp then show ?P by simp qed -lemma nth_default_coeffs_eq: - "nth_default 0 (coeffs p) = coeff p" +lemma nth_default_coeffs_eq: "nth_default 0 (coeffs p) = coeff p" by (simp add: fun_eq_iff coeff_Poly_eq [symmetric]) -lemma [code]: - "coeff p = nth_default 0 (coeffs p)" +lemma [code]: "coeff p = nth_default 0 (coeffs p)" by (simp add: nth_default_coeffs_eq) lemma coeffs_eqI: @@ -434,30 +406,25 @@ shows "coeffs p = xs" proof - from coeff have "p = Poly xs" by (simp add: poly_eq_iff) - with zero show ?thesis by simp (cases xs, simp_all) + with zero show ?thesis by simp (cases xs; simp) qed -lemma degree_eq_length_coeffs [code]: - "degree p = length (coeffs p) - 1" +lemma degree_eq_length_coeffs [code]: "degree p = length (coeffs p) - 1" by (simp add: coeffs_def) -lemma length_coeffs_degree: - "p \ 0 \ length (coeffs p) = Suc (degree p)" - by (induct p) (auto simp add: cCons_def) - -lemma [code abstract]: - "coeffs 0 = []" +lemma length_coeffs_degree: "p \ 0 \ length (coeffs p) = Suc (degree p)" + by (induct p) (auto simp: cCons_def) + +lemma [code abstract]: "coeffs 0 = []" by (fact coeffs_0_eq_Nil) -lemma [code abstract]: - "coeffs (pCons a p) = a ## coeffs p" +lemma [code abstract]: "coeffs (pCons a p) = a ## coeffs p" by (fact coeffs_pCons_eq_cCons) instantiation poly :: ("{zero, equal}") equal begin -definition - [code]: "HOL.equal (p::'a poly) q \ HOL.equal (coeffs p) (coeffs q)" +definition [code]: "HOL.equal (p::'a poly) q \ HOL.equal (coeffs p) (coeffs q)" instance by standard (simp add: equal equal_poly_def coeffs_eq_iff) @@ -468,41 +435,34 @@ by (fact equal_refl) definition is_zero :: "'a::zero poly \ bool" -where - [code]: "is_zero p \ List.null (coeffs p)" - -lemma is_zero_null [code_abbrev]: - "is_zero p \ p = 0" + where [code]: "is_zero p \ List.null (coeffs p)" + +lemma is_zero_null [code_abbrev]: "is_zero p \ p = 0" by (simp add: is_zero_def null_def) + subsubsection \Reconstructing the polynomial from the list\ \ \contributed by Sebastiaan J.C. Joosten and René Thiemann\ definition poly_of_list :: "'a::comm_monoid_add list \ 'a poly" -where - [simp]: "poly_of_list = Poly" - -lemma poly_of_list_impl [code abstract]: - "coeffs (poly_of_list as) = strip_while (HOL.eq 0) as" + where [simp]: "poly_of_list = Poly" + +lemma poly_of_list_impl [code abstract]: "coeffs (poly_of_list as) = strip_while (HOL.eq 0) as" by simp subsection \Fold combinator for polynomials\ definition fold_coeffs :: "('a::zero \ 'b \ 'b) \ 'a poly \ 'b \ 'b" -where - "fold_coeffs f p = foldr f (coeffs p)" - -lemma fold_coeffs_0_eq [simp]: - "fold_coeffs f 0 = id" + where "fold_coeffs f p = foldr f (coeffs p)" + +lemma fold_coeffs_0_eq [simp]: "fold_coeffs f 0 = id" by (simp add: fold_coeffs_def) -lemma fold_coeffs_pCons_eq [simp]: - "f 0 = id \ fold_coeffs f (pCons a p) = f a \ fold_coeffs f p" +lemma fold_coeffs_pCons_eq [simp]: "f 0 = id \ fold_coeffs f (pCons a p) = f a \ fold_coeffs f p" by (simp add: fold_coeffs_def cCons_def fun_eq_iff) -lemma fold_coeffs_pCons_0_0_eq [simp]: - "fold_coeffs f (pCons 0 0) = id" +lemma fold_coeffs_pCons_0_0_eq [simp]: "fold_coeffs f (pCons 0 0) = id" by (simp add: fold_coeffs_def) lemma fold_coeffs_pCons_coeff_not_0_eq [simp]: @@ -517,35 +477,39 @@ subsection \Canonical morphism on polynomials -- evaluation\ definition poly :: "'a::comm_semiring_0 poly \ 'a \ 'a" -where - "poly p = fold_coeffs (\a f x. a + x * f x) p (\x. 0)" \ \The Horner Schema\ - -lemma poly_0 [simp]: - "poly 0 x = 0" + where "poly p = fold_coeffs (\a f x. a + x * f x) p (\x. 0)" \ \The Horner Schema\ + +lemma poly_0 [simp]: "poly 0 x = 0" by (simp add: poly_def) - -lemma poly_pCons [simp]: - "poly (pCons a p) x = a + x * poly p x" + +lemma poly_pCons [simp]: "poly (pCons a p) x = a + x * poly p x" by (cases "p = 0 \ a = 0") (auto simp add: poly_def) -lemma poly_altdef: - "poly p (x :: 'a :: {comm_semiring_0, semiring_1}) = (\i\degree p. coeff p i * x ^ i)" +lemma poly_altdef: "poly p x = (\i\degree p. coeff p i * x ^ i)" + for x :: "'a::{comm_semiring_0,semiring_1}" proof (induction p rule: pCons_induct) + case 0 + then show ?case + by simp +next case (pCons a p) - show ?case - proof (cases "p = 0") - case False - let ?p' = "pCons a p" - note poly_pCons[of a p x] - also note pCons.IH - also have "a + x * (\i\degree p. coeff p i * x ^ i) = - coeff ?p' 0 * x^0 + (\i\degree p. coeff ?p' (Suc i) * x^Suc i)" - by (simp add: field_simps sum_distrib_left coeff_pCons) - also note sum_atMost_Suc_shift[symmetric] - also note degree_pCons_eq[OF \p \ 0\, of a, symmetric] - finally show ?thesis . - qed simp -qed simp + show ?case + proof (cases "p = 0") + case True + then show ?thesis by simp + next + case False + let ?p' = "pCons a p" + note poly_pCons[of a p x] + also note pCons.IH + also have "a + x * (\i\degree p. coeff p i * x ^ i) = + coeff ?p' 0 * x^0 + (\i\degree p. coeff ?p' (Suc i) * x^Suc i)" + by (simp add: field_simps sum_distrib_left coeff_pCons) + also note sum_atMost_Suc_shift[symmetric] + also note degree_pCons_eq[OF \p \ 0\, of a, symmetric] + finally show ?thesis . + qed +qed lemma poly_0_coeff_0: "poly p 0 = coeff p 0" by (cases p) (auto simp: poly_altdef) @@ -557,16 +521,13 @@ is "\a m n. if m = n then a else 0" by (simp add: MOST_iff_cofinite) -lemma coeff_monom [simp]: - "coeff (monom a m) n = (if m = n then a else 0)" +lemma coeff_monom [simp]: "coeff (monom a m) n = (if m = n then a else 0)" by transfer rule -lemma monom_0: - "monom a 0 = pCons a 0" +lemma monom_0: "monom a 0 = pCons a 0" by (rule poly_eqI) (simp add: coeff_pCons split: nat.split) -lemma monom_Suc: - "monom a (Suc n) = pCons 0 (monom a n)" +lemma monom_Suc: "monom a (Suc n) = pCons 0 (monom a n)" by (rule poly_eqI) (simp add: coeff_pCons split: nat.split) lemma monom_eq_0 [simp]: "monom 0 n = 0" @@ -583,26 +544,24 @@ lemma degree_monom_eq: "a \ 0 \ degree (monom a n) = n" apply (rule order_antisym [OF degree_monom_le]) - apply (rule le_degree, simp) + apply (rule le_degree) + apply simp done lemma coeffs_monom [code abstract]: "coeffs (monom a n) = (if a = 0 then [] else replicate n 0 @ [a])" by (induct n) (simp_all add: monom_0 monom_Suc) -lemma fold_coeffs_monom [simp]: - "a \ 0 \ fold_coeffs f (monom a n) = f 0 ^^ n \ f a" +lemma fold_coeffs_monom [simp]: "a \ 0 \ fold_coeffs f (monom a n) = f 0 ^^ n \ f a" by (simp add: fold_coeffs_def coeffs_monom fun_eq_iff) -lemma poly_monom: - fixes a x :: "'a::{comm_semiring_1}" - shows "poly (monom a n) x = a * x ^ n" - by (cases "a = 0", simp_all) - (induct n, simp_all add: mult.left_commute poly_def) +lemma poly_monom: "poly (monom a n) x = a * x ^ n" + for a x :: "'a::comm_semiring_1" + by (cases "a = 0", simp_all) (induct n, simp_all add: mult.left_commute poly_def) lemma monom_eq_iff': "monom c n = monom d m \ c = d \ (c = 0 \ n = m)" by (auto simp: poly_eq_iff) - + lemma monom_eq_const_iff: "monom c n = [:d:] \ c = d \ (c = 0 \ n = 0)" using monom_eq_iff'[of c n d 0] by (simp add: monom_0) @@ -700,74 +659,56 @@ end -lemma add_pCons [simp]: - "pCons a p + pCons b q = pCons (a + b) (p + q)" - by (rule poly_eqI, simp add: coeff_pCons split: nat.split) - -lemma minus_pCons [simp]: - "- pCons a p = pCons (- a) (- p)" - by (rule poly_eqI, simp add: coeff_pCons split: nat.split) - -lemma diff_pCons [simp]: - "pCons a p - pCons b q = pCons (a - b) (p - q)" - by (rule poly_eqI, simp add: coeff_pCons split: nat.split) +lemma add_pCons [simp]: "pCons a p + pCons b q = pCons (a + b) (p + q)" + by (rule poly_eqI) (simp add: coeff_pCons split: nat.split) + +lemma minus_pCons [simp]: "- pCons a p = pCons (- a) (- p)" + by (rule poly_eqI) (simp add: coeff_pCons split: nat.split) + +lemma diff_pCons [simp]: "pCons a p - pCons b q = pCons (a - b) (p - q)" + by (rule poly_eqI) (simp add: coeff_pCons split: nat.split) lemma degree_add_le_max: "degree (p + q) \ max (degree p) (degree q)" - by (rule degree_le, auto simp add: coeff_eq_0) - -lemma degree_add_le: - "\degree p \ n; degree q \ n\ \ degree (p + q) \ n" + by (rule degree_le) (auto simp add: coeff_eq_0) + +lemma degree_add_le: "degree p \ n \ degree q \ n \ degree (p + q) \ n" by (auto intro: order_trans degree_add_le_max) -lemma degree_add_less: - "\degree p < n; degree q < n\ \ degree (p + q) < n" +lemma degree_add_less: "degree p < n \ degree q < n \ degree (p + q) < n" by (auto intro: le_less_trans degree_add_le_max) -lemma degree_add_eq_right: - "degree p < degree q \ degree (p + q) = degree q" - apply (cases "q = 0", simp) +lemma degree_add_eq_right: "degree p < degree q \ degree (p + q) = degree q" + apply (cases "q = 0") + apply simp apply (rule order_antisym) - apply (simp add: degree_add_le) + apply (simp add: degree_add_le) apply (rule le_degree) apply (simp add: coeff_eq_0) done -lemma degree_add_eq_left: - "degree q < degree p \ degree (p + q) = degree p" - using degree_add_eq_right [of q p] - by (simp add: add.commute) - -lemma degree_minus [simp]: - "degree (- p) = degree p" - unfolding degree_def by simp - -lemma lead_coeff_add_le: - assumes "degree p < degree q" - shows "lead_coeff (p + q) = lead_coeff q" - using assms +lemma degree_add_eq_left: "degree q < degree p \ degree (p + q) = degree p" + using degree_add_eq_right [of q p] by (simp add: add.commute) + +lemma degree_minus [simp]: "degree (- p) = degree p" + by (simp add: degree_def) + +lemma lead_coeff_add_le: "degree p < degree q \ lead_coeff (p + q) = lead_coeff q" by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right) -lemma lead_coeff_minus: - "lead_coeff (- p) = - lead_coeff p" +lemma lead_coeff_minus: "lead_coeff (- p) = - lead_coeff p" by (metis coeff_minus degree_minus) -lemma degree_diff_le_max: - fixes p q :: "'a :: ab_group_add poly" - shows "degree (p - q) \ max (degree p) (degree q)" - using degree_add_le [where p=p and q="-q"] - by simp - -lemma degree_diff_le: - fixes p q :: "'a :: ab_group_add poly" - assumes "degree p \ n" and "degree q \ n" - shows "degree (p - q) \ n" - using assms degree_add_le [of p n "- q"] by simp - -lemma degree_diff_less: - fixes p q :: "'a :: ab_group_add poly" - assumes "degree p < n" and "degree q < n" - shows "degree (p - q) < n" - using assms degree_add_less [of p n "- q"] by simp +lemma degree_diff_le_max: "degree (p - q) \ max (degree p) (degree q)" + for p q :: "'a::ab_group_add poly" + using degree_add_le [where p=p and q="-q"] by simp + +lemma degree_diff_le: "degree p \ n \ degree q \ n \ degree (p - q) \ n" + for p q :: "'a::ab_group_add poly" + using degree_add_le [of p n "- q"] by simp + +lemma degree_diff_less: "degree p < n \ degree q < n \ degree (p - q) < n" + for p q :: "'a::ab_group_add poly" + using degree_add_less [of p n "- q"] by simp lemma add_monom: "monom a n + monom b n = monom (a + b) n" by (rule poly_eqI) simp @@ -775,99 +716,99 @@ lemma diff_monom: "monom a n - monom b n = monom (a - b) n" by (rule poly_eqI) simp -lemma minus_monom: "- monom a n = monom (-a) n" +lemma minus_monom: "- monom a n = monom (- a) n" by (rule poly_eqI) simp lemma coeff_sum: "coeff (\x\A. p x) i = (\x\A. coeff (p x) i)" - by (cases "finite A", induct set: finite, simp_all) + by (induct A rule: infinite_finite_induct) simp_all lemma monom_sum: "monom (\x\A. a x) n = (\x\A. monom (a x) n)" by (rule poly_eqI) (simp add: coeff_sum) fun plus_coeffs :: "'a::comm_monoid_add list \ 'a list \ 'a list" -where - "plus_coeffs xs [] = xs" -| "plus_coeffs [] ys = ys" -| "plus_coeffs (x # xs) (y # ys) = (x + y) ## plus_coeffs xs ys" + where + "plus_coeffs xs [] = xs" + | "plus_coeffs [] ys = ys" + | "plus_coeffs (x # xs) (y # ys) = (x + y) ## plus_coeffs xs ys" lemma coeffs_plus_eq_plus_coeffs [code abstract]: "coeffs (p + q) = plus_coeffs (coeffs p) (coeffs q)" proof - - { fix xs ys :: "'a list" and n - have "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n" - proof (induct xs ys arbitrary: n rule: plus_coeffs.induct) - case (3 x xs y ys n) - then show ?case by (cases n) (auto simp add: cCons_def) - qed simp_all } - note * = this - { fix xs ys :: "'a list" - assume "xs \ [] \ last xs \ 0" and "ys \ [] \ last ys \ 0" - moreover assume "plus_coeffs xs ys \ []" - ultimately have "last (plus_coeffs xs ys) \ 0" - proof (induct xs ys rule: plus_coeffs.induct) - case (3 x xs y ys) then show ?case by (auto simp add: cCons_def) metis - qed simp_all } - note ** = this + have *: "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n" + for xs ys :: "'a list" and n + proof (induct xs ys arbitrary: n rule: plus_coeffs.induct) + case 3 + then show ?case by (cases n) (auto simp: cCons_def) + qed simp_all + have **: "last (plus_coeffs xs ys) \ 0" + if "xs \ [] \ last xs \ 0" and "ys \ [] \ last ys \ 0" and "plus_coeffs xs ys \ []" + for xs ys :: "'a list" + using that + proof (induct xs ys rule: plus_coeffs.induct) + case 3 + then show ?case by (auto simp add: cCons_def) metis + qed simp_all show ?thesis apply (rule coeffs_eqI) - apply (simp add: * nth_default_coeffs_eq) + apply (simp add: * nth_default_coeffs_eq) apply (rule **) - apply (auto dest: last_coeffs_not_0) + apply (auto dest: last_coeffs_not_0) done qed -lemma coeffs_uminus [code abstract]: - "coeffs (- p) = map (\a. - a) (coeffs p)" +lemma coeffs_uminus [code abstract]: "coeffs (- p) = map (\a. - a) (coeffs p)" by (rule coeffs_eqI) (simp_all add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq) -lemma [code]: - fixes p q :: "'a::ab_group_add poly" - shows "p - q = p + - q" +lemma [code]: "p - q = p + - q" + for p q :: "'a::ab_group_add poly" by (fact diff_conv_add_uminus) lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x" - apply (induct p arbitrary: q, simp) + apply (induct p arbitrary: q) + apply simp apply (case_tac q, simp, simp add: algebra_simps) done -lemma poly_minus [simp]: - fixes x :: "'a::comm_ring" - shows "poly (- p) x = - poly p x" +lemma poly_minus [simp]: "poly (- p) x = - poly p x" + for x :: "'a::comm_ring" by (induct p) simp_all -lemma poly_diff [simp]: - fixes x :: "'a::comm_ring" - shows "poly (p - q) x = poly p x - poly q x" +lemma poly_diff [simp]: "poly (p - q) x = poly p x - poly q x" + for x :: "'a::comm_ring" using poly_add [of p "- q" x] by simp lemma poly_sum: "poly (\k\A. p k) x = (\k\A. poly (p k) x)" by (induct A rule: infinite_finite_induct) simp_all -lemma degree_sum_le: "finite S \ (\ p . p \ S \ degree (f p) \ n) - \ degree (sum f S) \ n" +lemma degree_sum_le: "finite S \ (\p. p \ S \ degree (f p) \ n) \ degree (sum f S) \ n" proof (induct S rule: finite_induct) + case empty + then show ?case by simp +next case (insert p S) - hence "degree (sum f S) \ n" "degree (f p) \ n" by auto - thus ?case unfolding sum.insert[OF insert(1-2)] by (metis degree_add_le) -qed simp - -lemma poly_as_sum_of_monoms': - assumes n: "degree p \ n" + then have "degree (sum f S) \ n" "degree (f p) \ n" + by auto + then show ?case + unfolding sum.insert[OF insert(1-2)] by (metis degree_add_le) +qed + +lemma poly_as_sum_of_monoms': + assumes "degree p \ n" shows "(\i\n. monom (coeff p i) i) = p" proof - have eq: "\i. {..n} \ {i} = (if i \ n then {i} else {})" by auto - show ?thesis - using n by (simp add: poly_eq_iff coeff_sum coeff_eq_0 sum.If_cases eq - if_distrib[where f="\x. x * a" for a]) + from assms show ?thesis + by (simp add: poly_eq_iff coeff_sum coeff_eq_0 sum.If_cases eq + if_distrib[where f="\x. x * a" for a]) qed lemma poly_as_sum_of_monoms: "(\i\degree p. monom (coeff p i) i) = p" by (intro poly_as_sum_of_monoms' order_refl) lemma Poly_snoc: "Poly (xs @ [x]) = Poly xs + monom x (length xs)" - by (induction xs) (simp_all add: monom_0 monom_Suc) + by (induct xs) (simp_all add: monom_0 monom_Suc) subsection \Multiplication by a constant, polynomial multiplication and the unit polynomial\ @@ -875,126 +816,123 @@ lift_definition smult :: "'a::comm_semiring_0 \ 'a poly \ 'a poly" is "\a p n. a * coeff p n" proof - - fix a :: 'a and p :: "'a poly" show "\\<^sub>\ i. a * coeff p i = 0" + fix a :: 'a and p :: "'a poly" + show "\\<^sub>\ i. a * coeff p i = 0" using MOST_coeff_eq_0[of p] by eventually_elim simp qed -lemma coeff_smult [simp]: - "coeff (smult a p) n = a * coeff p n" +lemma coeff_smult [simp]: "coeff (smult a p) n = a * coeff p n" by (simp add: smult.rep_eq) lemma degree_smult_le: "degree (smult a p) \ degree p" - by (rule degree_le, simp add: coeff_eq_0) + by (rule degree_le) (simp add: coeff_eq_0) lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p" - by (rule poly_eqI, simp add: mult.assoc) + by (rule poly_eqI) (simp add: mult.assoc) lemma smult_0_right [simp]: "smult a 0 = 0" - by (rule poly_eqI, simp) + by (rule poly_eqI) simp lemma smult_0_left [simp]: "smult 0 p = 0" - by (rule poly_eqI, simp) + by (rule poly_eqI) simp lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p" - by (rule poly_eqI, simp) - -lemma smult_add_right: - "smult a (p + q) = smult a p + smult a q" - by (rule poly_eqI, simp add: algebra_simps) - -lemma smult_add_left: - "smult (a + b) p = smult a p + smult b p" - by (rule poly_eqI, simp add: algebra_simps) - -lemma smult_minus_right [simp]: - "smult (a::'a::comm_ring) (- p) = - smult a p" - by (rule poly_eqI, simp) - -lemma smult_minus_left [simp]: - "smult (- a::'a::comm_ring) p = - smult a p" - by (rule poly_eqI, simp) - -lemma smult_diff_right: - "smult (a::'a::comm_ring) (p - q) = smult a p - smult a q" - by (rule poly_eqI, simp add: algebra_simps) - -lemma smult_diff_left: - "smult (a - b::'a::comm_ring) p = smult a p - smult b p" - by (rule poly_eqI, simp add: algebra_simps) + by (rule poly_eqI) simp + +lemma smult_add_right: "smult a (p + q) = smult a p + smult a q" + by (rule poly_eqI) (simp add: algebra_simps) + +lemma smult_add_left: "smult (a + b) p = smult a p + smult b p" + by (rule poly_eqI) (simp add: algebra_simps) + +lemma smult_minus_right [simp]: "smult a (- p) = - smult a p" + for a :: "'a::comm_ring" + by (rule poly_eqI) simp + +lemma smult_minus_left [simp]: "smult (- a) p = - smult a p" + for a :: "'a::comm_ring" + by (rule poly_eqI) simp + +lemma smult_diff_right: "smult a (p - q) = smult a p - smult a q" + for a :: "'a::comm_ring" + by (rule poly_eqI) (simp add: algebra_simps) + +lemma smult_diff_left: "smult (a - b) p = smult a p - smult b p" + for a b :: "'a::comm_ring" + by (rule poly_eqI) (simp add: algebra_simps) lemmas smult_distribs = smult_add_left smult_add_right smult_diff_left smult_diff_right -lemma smult_pCons [simp]: - "smult a (pCons b p) = pCons (a * b) (smult a p)" - by (rule poly_eqI, simp add: coeff_pCons split: nat.split) +lemma smult_pCons [simp]: "smult a (pCons b p) = pCons (a * b) (smult a p)" + by (rule poly_eqI) (simp add: coeff_pCons split: nat.split) lemma smult_monom: "smult a (monom b n) = monom (a * b) n" - by (induct n, simp add: monom_0, simp add: monom_Suc) + by (induct n) (simp_all add: monom_0 monom_Suc) lemma smult_Poly: "smult c (Poly xs) = Poly (map (op * c) xs)" - by (auto simp add: poly_eq_iff nth_default_def) - -lemma degree_smult_eq [simp]: - fixes a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}" - shows "degree (smult a p) = (if a = 0 then 0 else degree p)" - by (cases "a = 0", simp, simp add: degree_def) - -lemma smult_eq_0_iff [simp]: - fixes a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}" - shows "smult a p = 0 \ a = 0 \ p = 0" + by (auto simp: poly_eq_iff nth_default_def) + +lemma degree_smult_eq [simp]: "degree (smult a p) = (if a = 0 then 0 else degree p)" + for a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}" + by (cases "a = 0") (simp_all add: degree_def) + +lemma smult_eq_0_iff [simp]: "smult a p = 0 \ a = 0 \ p = 0" + for a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}" by (simp add: poly_eq_iff) - + lemma coeffs_smult [code abstract]: - fixes p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" - shows "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))" + "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))" + for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" by (rule coeffs_eqI) - (auto simp add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq) + (auto simp add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 + nth_default_map_eq nth_default_coeffs_eq) lemma smult_eq_iff: - assumes "(b :: 'a :: field) \ 0" - shows "smult a p = smult b q \ smult (a / b) p = q" + fixes b :: "'a :: field" + assumes "b \ 0" + shows "smult a p = smult b q \ smult (a / b) p = q" + (is "?lhs \ ?rhs") proof - assume "smult a p = smult b q" - also from assms have "smult (inverse b) \ = q" by simp - finally show "smult (a / b) p = q" by (simp add: field_simps) -qed (insert assms, auto) + assume ?lhs + also from assms have "smult (inverse b) \ = q" + by simp + finally show ?rhs + by (simp add: field_simps) +next + assume ?rhs + with assms show ?lhs by auto +qed instantiation poly :: (comm_semiring_0) comm_semiring_0 begin -definition - "p * q = fold_coeffs (\a p. smult a q + pCons 0 p) p 0" +definition "p * q = fold_coeffs (\a p. smult a q + pCons 0 p) p 0" lemma mult_poly_0_left: "(0::'a poly) * q = 0" by (simp add: times_poly_def) -lemma mult_pCons_left [simp]: - "pCons a p * q = smult a q + pCons 0 (p * q)" +lemma mult_pCons_left [simp]: "pCons a p * q = smult a q + pCons 0 (p * q)" by (cases "p = 0 \ a = 0") (auto simp add: times_poly_def) lemma mult_poly_0_right: "p * (0::'a poly) = 0" - by (induct p) (simp add: mult_poly_0_left, simp) - -lemma mult_pCons_right [simp]: - "p * pCons a q = smult a p + pCons 0 (p * q)" - by (induct p) (simp add: mult_poly_0_left, simp add: algebra_simps) + by (induct p) (simp_all add: mult_poly_0_left) + +lemma mult_pCons_right [simp]: "p * pCons a q = smult a p + pCons 0 (p * q)" + by (induct p) (simp_all add: mult_poly_0_left algebra_simps) lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right -lemma mult_smult_left [simp]: - "smult a p * q = smult a (p * q)" - by (induct p) (simp add: mult_poly_0, simp add: smult_add_right) - -lemma mult_smult_right [simp]: - "p * smult a q = smult a (p * q)" - by (induct q) (simp add: mult_poly_0, simp add: smult_add_right) - -lemma mult_poly_add_left: - fixes p q r :: "'a poly" - shows "(p + q) * r = p * r + q * r" - by (induct r) (simp add: mult_poly_0, simp add: smult_distribs algebra_simps) +lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)" + by (induct p) (simp_all add: mult_poly_0 smult_add_right) + +lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)" + by (induct q) (simp_all add: mult_poly_0 smult_add_right) + +lemma mult_poly_add_left: "(p + q) * r = p * r + q * r" + for p q r :: "'a poly" + by (induct r) (simp_all add: mult_poly_0 smult_distribs algebra_simps) instance proof @@ -1006,49 +944,48 @@ show "(p + q) * r = p * r + q * r" by (rule mult_poly_add_left) show "(p * q) * r = p * (q * r)" - by (induct p, simp add: mult_poly_0, simp add: mult_poly_add_left) + by (induct p) (simp_all add: mult_poly_0 mult_poly_add_left) show "p * q = q * p" - by (induct p, simp add: mult_poly_0, simp) + by (induct p) (simp_all add: mult_poly_0) qed end lemma coeff_mult_degree_sum: - "coeff (p * q) (degree p + degree q) = - coeff p (degree p) * coeff q (degree q)" - by (induct p, simp, simp add: coeff_eq_0) + "coeff (p * q) (degree p + degree q) = coeff p (degree p) * coeff q (degree q)" + by (induct p) (simp_all add: coeff_eq_0) instance poly :: ("{comm_semiring_0,semiring_no_zero_divisors}") semiring_no_zero_divisors proof fix p q :: "'a poly" assume "p \ 0" and "q \ 0" - have "coeff (p * q) (degree p + degree q) = - coeff p (degree p) * coeff q (degree q)" + have "coeff (p * q) (degree p + degree q) = coeff p (degree p) * coeff q (degree q)" by (rule coeff_mult_degree_sum) - also have "coeff p (degree p) * coeff q (degree q) \ 0" - using \p \ 0\ and \q \ 0\ by simp + also from \p \ 0\ \q \ 0\ have "coeff p (degree p) * coeff q (degree q) \ 0" + by simp finally have "\n. coeff (p * q) n \ 0" .. - thus "p * q \ 0" by (simp add: poly_eq_iff) + then show "p * q \ 0" + by (simp add: poly_eq_iff) qed instance poly :: (comm_semiring_0_cancel) comm_semiring_0_cancel .. -lemma coeff_mult: - "coeff (p * q) n = (\i\n. coeff p i * coeff q (n-i))" +lemma coeff_mult: "coeff (p * q) n = (\i\n. coeff p i * coeff q (n-i))" proof (induct p arbitrary: n) - case 0 show ?case by simp + case 0 + show ?case by simp next - case (pCons a p n) thus ?case - by (cases n, simp, simp add: sum_atMost_Suc_shift - del: sum_atMost_Suc) + case (pCons a p n) + then show ?case + by (cases n) (simp_all add: sum_atMost_Suc_shift del: sum_atMost_Suc) qed lemma degree_mult_le: "degree (p * q) \ degree p + degree q" -apply (rule degree_le) -apply (induct p) -apply simp -apply (simp add: coeff_eq_0 coeff_pCons split: nat.split) -done + apply (rule degree_le) + apply (induct p) + apply simp + apply (simp add: coeff_eq_0 coeff_pCons split: nat.split) + done lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)" by (induct m) (simp add: monom_0 smult_monom, simp add: monom_Suc) @@ -1061,67 +998,53 @@ instance proof show "1 * p = p" for p :: "'a poly" - unfolding one_poly_def by simp + by (simp add: one_poly_def) show "0 \ (1::'a poly)" - unfolding one_poly_def by simp + by (simp add: one_poly_def) qed end instance poly :: ("{comm_semiring_1,semiring_1_no_zero_divisors}") semiring_1_no_zero_divisors .. - instance poly :: (comm_ring) comm_ring .. - instance poly :: (comm_ring_1) comm_ring_1 .. - instance poly :: (comm_ring_1) comm_semiring_1_cancel .. lemma coeff_1 [simp]: "coeff 1 n = (if n = 0 then 1 else 0)" - unfolding one_poly_def - by (simp add: coeff_pCons split: nat.split) - -lemma monom_eq_1 [simp]: - "monom 1 0 = 1" + by (simp add: one_poly_def coeff_pCons split: nat.split) + +lemma monom_eq_1 [simp]: "monom 1 0 = 1" by (simp add: monom_0 one_poly_def) lemma monom_eq_1_iff: "monom c n = 1 \ c = 1 \ n = 0" using monom_eq_const_iff[of c n 1] by (auto simp: one_poly_def) -lemma monom_altdef: - "monom c n = smult c ([:0, 1:]^n)" - by (induction n) (simp_all add: monom_0 monom_Suc one_poly_def) - +lemma monom_altdef: "monom c n = smult c ([:0, 1:]^n)" + by (induct n) (simp_all add: monom_0 monom_Suc one_poly_def) + lemma degree_1 [simp]: "degree 1 = 0" - unfolding one_poly_def - by (rule degree_pCons_0) - -lemma coeffs_1_eq [simp, code abstract]: - "coeffs 1 = [1]" + unfolding one_poly_def by (rule degree_pCons_0) + +lemma coeffs_1_eq [simp, code abstract]: "coeffs 1 = [1]" by (simp add: one_poly_def) -lemma degree_power_le: - "degree (p ^ n) \ degree p * n" +lemma degree_power_le: "degree (p ^ n) \ degree p * n" by (induct n) (auto intro: order_trans degree_mult_le) -lemma coeff_0_power: - "coeff (p ^ n) 0 = coeff p 0 ^ n" - by (induction n) (simp_all add: coeff_mult) - -lemma poly_smult [simp]: - "poly (smult a p) x = a * poly p x" - by (induct p, simp, simp add: algebra_simps) - -lemma poly_mult [simp]: - "poly (p * q) x = poly p x * poly q x" - by (induct p, simp_all, simp add: algebra_simps) - -lemma poly_1 [simp]: - "poly 1 x = 1" +lemma coeff_0_power: "coeff (p ^ n) 0 = coeff p 0 ^ n" + by (induct n) (simp_all add: coeff_mult) + +lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x" + by (induct p) (simp_all add: algebra_simps) + +lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x" + by (induct p) (simp_all add: algebra_simps) + +lemma poly_1 [simp]: "poly 1 x = 1" by (simp add: one_poly_def) -lemma poly_power [simp]: - fixes p :: "'a::{comm_semiring_1} poly" - shows "poly (p ^ n) x = poly p x ^ n" +lemma poly_power [simp]: "poly (p ^ n) x = poly p x ^ n" + for p :: "'a::comm_semiring_1 poly" by (induct n) simp_all lemma poly_prod: "poly (\k\A. p k) x = (\k\A. poly (p k) x)" @@ -1129,51 +1052,54 @@ lemma degree_prod_sum_le: "finite S \ degree (prod f S) \ sum (degree o f) S" proof (induct S rule: finite_induct) + case empty + then show ?case by simp +next case (insert a S) - show ?case unfolding prod.insert[OF insert(1-2)] sum.insert[OF insert(1-2)] - by (rule le_trans[OF degree_mult_le], insert insert, auto) -qed simp - -lemma coeff_0_prod_list: - "coeff (prod_list xs) 0 = prod_list (map (\p. coeff p 0) xs)" - by (induction xs) (simp_all add: coeff_mult) - -lemma coeff_monom_mult: - "coeff (monom c n * p) k = (if k < n then 0 else c * coeff p (k - n))" + show ?case + unfolding prod.insert[OF insert(1-2)] sum.insert[OF insert(1-2)] + by (rule le_trans[OF degree_mult_le]) (use insert in auto) +qed + +lemma coeff_0_prod_list: "coeff (prod_list xs) 0 = prod_list (map (\p. coeff p 0) xs)" + by (induct xs) (simp_all add: coeff_mult) + +lemma coeff_monom_mult: "coeff (monom c n * p) k = (if k < n then 0 else c * coeff p (k - n))" proof - have "coeff (monom c n * p) k = (\i\k. (if n = i then c else 0) * coeff p (k - i))" by (simp add: coeff_mult) also have "\ = (\i\k. (if n = i then c * coeff p (k - i) else 0))" by (intro sum.cong) simp_all - also have "\ = (if k < n then 0 else c * coeff p (k - n))" by (simp add: sum.delta') + also have "\ = (if k < n then 0 else c * coeff p (k - n))" + by (simp add: sum.delta') finally show ?thesis . qed -lemma monom_1_dvd_iff': - "monom 1 n dvd p \ (\k (\kkkkk. coeff p (k + n))" have "\\<^sub>\k. coeff p (k + n) = 0" - by (subst cofinite_eq_sequentially, subst eventually_sequentially_seg, + by (subst cofinite_eq_sequentially, subst eventually_sequentially_seg, subst cofinite_eq_sequentially [symmetric]) transfer - hence coeff_r [simp]: "coeff r k = coeff p (k + n)" for k unfolding r_def - by (subst poly.Abs_poly_inverse) simp_all + then have coeff_r [simp]: "coeff r k = coeff p (k + n)" for k + unfolding r_def by (subst poly.Abs_poly_inverse) simp_all have "p = monom 1 n * r" - by (intro poly_eqI, subst coeff_monom_mult) (insert zero, simp_all) - thus "monom 1 n dvd p" by simp + by (rule poly_eqI, subst coeff_monom_mult) (simp_all add: zero) + then show "monom 1 n dvd p" by simp qed subsection \Mapping polynomials\ -definition map_poly - :: "('a :: zero \ 'b :: zero) \ 'a poly \ 'b poly" where - "map_poly f p = Poly (map f (coeffs p))" +definition map_poly :: "('a :: zero \ 'b :: zero) \ 'a poly \ 'b poly" + where "map_poly f p = Poly (map f (coeffs p))" lemma map_poly_0 [simp]: "map_poly f 0 = 0" by (simp add: map_poly_def) @@ -1186,60 +1112,68 @@ lemma coeff_map_poly: assumes "f 0 = 0" - shows "coeff (map_poly f p) n = f (coeff p n)" - by (auto simp: map_poly_def nth_default_def coeffs_def assms - not_less Suc_le_eq coeff_eq_0 simp del: upt_Suc) - -lemma coeffs_map_poly [code abstract]: - "coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))" + shows "coeff (map_poly f p) n = f (coeff p n)" + by (auto simp: assms map_poly_def nth_default_def coeffs_def not_less Suc_le_eq coeff_eq_0 + simp del: upt_Suc) + +lemma coeffs_map_poly [code abstract]: + "coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))" by (simp add: map_poly_def) lemma set_coeffs_map_poly: "(\x. f x = 0 \ x = 0) \ set (coeffs (map_poly f p)) = f ` set (coeffs p)" by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0) -lemma coeffs_map_poly': - assumes "(\x. x \ 0 \ f x \ 0)" - shows "coeffs (map_poly f p) = map f (coeffs p)" - by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0 assms - intro!: strip_while_not_last split: if_splits) +lemma coeffs_map_poly': + assumes "\x. x \ 0 \ f x \ 0" + shows "coeffs (map_poly f p) = map f (coeffs p)" + by (cases "p = 0") + (auto simp: assms coeffs_map_poly last_map last_coeffs_not_0 + intro!: strip_while_not_last split: if_splits) lemma degree_map_poly: assumes "\x. x \ 0 \ f x \ 0" - shows "degree (map_poly f p) = degree p" + shows "degree (map_poly f p) = degree p" by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms) lemma map_poly_eq_0_iff: assumes "f 0 = 0" "\x. x \ set (coeffs p) \ x \ 0 \ f x \ 0" - shows "map_poly f p = 0 \ p = 0" + shows "map_poly f p = 0 \ p = 0" proof - - { - fix n :: nat - have "coeff (map_poly f p) n = f (coeff p n)" by (simp add: coeff_map_poly assms) + have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" for n + proof - + have "coeff (map_poly f p) n = f (coeff p n)" + by (simp add: coeff_map_poly assms) also have "\ = 0 \ coeff p n = 0" proof (cases "n < length (coeffs p)") case True - hence "coeff p n \ set (coeffs p)" by (auto simp: coeffs_def simp del: upt_Suc) - with assms show "f (coeff p n) = 0 \ coeff p n = 0" by auto - qed (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def) - finally have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" . - } - thus ?thesis by (auto simp: poly_eq_iff) + then have "coeff p n \ set (coeffs p)" + by (auto simp: coeffs_def simp del: upt_Suc) + with assms show "f (coeff p n) = 0 \ coeff p n = 0" + by auto + next + case False + then show ?thesis + by (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def) + qed + finally show ?thesis . + qed + then show ?thesis by (auto simp: poly_eq_iff) qed lemma map_poly_smult: assumes "f 0 = 0""\c x. f (c * x) = f c * f x" - shows "map_poly f (smult c p) = smult (f c) (map_poly f p)" + shows "map_poly f (smult c p) = smult (f c) (map_poly f p)" by (intro poly_eqI) (simp_all add: assms coeff_map_poly) lemma map_poly_pCons: assumes "f 0 = 0" - shows "map_poly f (pCons c p) = pCons (f c) (map_poly f p)" + shows "map_poly f (pCons c p) = pCons (f c) (map_poly f p)" by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits) lemma map_poly_map_poly: assumes "f 0 = 0" "g 0 = 0" - shows "map_poly f (map_poly g p) = map_poly (f \ g) p" + shows "map_poly f (map_poly g p) = map_poly (f \ g) p" by (intro poly_eqI) (simp add: coeff_map_poly assms) lemma map_poly_id [simp]: "map_poly id p = p" @@ -1248,12 +1182,14 @@ lemma map_poly_id' [simp]: "map_poly (\x. x) p = p" by (simp add: map_poly_def) -lemma map_poly_cong: +lemma map_poly_cong: assumes "(\x. x \ set (coeffs p) \ f x = g x)" - shows "map_poly f p = map_poly g p" + shows "map_poly f p = map_poly g p" proof - - from assms have "map f (coeffs p) = map g (coeffs p)" by (intro map_cong) simp_all - thus ?thesis by (simp only: coeffs_eq_iff coeffs_map_poly) + from assms have "map f (coeffs p) = map g (coeffs p)" + by (intro map_cong) simp_all + then show ?thesis + by (simp only: coeffs_eq_iff coeffs_map_poly) qed lemma map_poly_monom: "f 0 = 0 \ map_poly f (monom c n) = monom (f c) n" @@ -1261,12 +1197,12 @@ lemma map_poly_idI: assumes "\x. x \ set (coeffs p) \ f x = x" - shows "map_poly f p = p" + shows "map_poly f p = p" using map_poly_cong[OF assms, of _ id] by simp lemma map_poly_idI': assumes "\x. x \ set (coeffs p) \ f x = x" - shows "p = map_poly f p" + shows "p = map_poly f p" using map_poly_cong[OF assms, of _ id] by simp lemma smult_conv_map_poly: "smult c p = map_poly (\x. c * x) p" @@ -1276,21 +1212,26 @@ subsection \Conversions from @{typ nat} and @{typ int} numbers\ lemma of_nat_poly: "of_nat n = [:of_nat n :: 'a :: comm_semiring_1:]" -proof (induction n) +proof (induct n) + case 0 + then show ?case by simp +next case (Suc n) - hence "of_nat (Suc n) = 1 + (of_nat n :: 'a poly)" + then have "of_nat (Suc n) = 1 + (of_nat n :: 'a poly)" by simp - also have "(of_nat n :: 'a poly) = [: of_nat n :]" + also have "(of_nat n :: 'a poly) = [: of_nat n :]" by (subst Suc) (rule refl) - also have "1 = [:1:]" by (simp add: one_poly_def) - finally show ?case by (subst (asm) add_pCons) simp -qed simp + also have "1 = [:1:]" + by (simp add: one_poly_def) + finally show ?case + by (subst (asm) add_pCons) simp +qed lemma degree_of_nat [simp]: "degree (of_nat n) = 0" by (simp add: of_nat_poly) lemma lead_coeff_of_nat [simp]: - "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})" + "lead_coeff (of_nat n) = (of_nat n :: 'a::{comm_semiring_1,semiring_char_0})" by (simp add: of_nat_poly) lemma of_int_poly: "of_int k = [:of_int k :: 'a :: comm_ring_1:]" @@ -1300,57 +1241,54 @@ by (simp add: of_int_poly) lemma lead_coeff_of_int [simp]: - "lead_coeff (of_int k) = (of_int k :: 'a :: {comm_ring_1,ring_char_0})" + "lead_coeff (of_int k) = (of_int k :: 'a::{comm_ring_1,ring_char_0})" by (simp add: of_int_poly) lemma numeral_poly: "numeral n = [:numeral n:]" by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp - + lemma degree_numeral [simp]: "degree (numeral n) = 0" by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp -lemma lead_coeff_numeral [simp]: +lemma lead_coeff_numeral [simp]: "lead_coeff (numeral n) = numeral n" by (simp add: numeral_poly) subsection \Lemmas about divisibility\ -lemma dvd_smult: "p dvd q \ p dvd smult a q" +lemma dvd_smult: + assumes "p dvd q" + shows "p dvd smult a q" proof - - assume "p dvd q" - then obtain k where "q = p * k" .. + from assms obtain k where "q = p * k" .. then have "smult a q = p * smult a k" by simp then show "p dvd smult a q" .. qed -lemma dvd_smult_cancel: - fixes a :: "'a :: field" - shows "p dvd smult a q \ a \ 0 \ p dvd q" +lemma dvd_smult_cancel: "p dvd smult a q \ a \ 0 \ p dvd q" + for a :: "'a::field" by (drule dvd_smult [where a="inverse a"]) simp -lemma dvd_smult_iff: - fixes a :: "'a::field" - shows "a \ 0 \ p dvd smult a q \ p dvd q" +lemma dvd_smult_iff: "a \ 0 \ p dvd smult a q \ p dvd q" + for a :: "'a::field" by (safe elim!: dvd_smult dvd_smult_cancel) lemma smult_dvd_cancel: - "smult a p dvd q \ p dvd q" + assumes "smult a p dvd q" + shows "p dvd q" proof - - assume "smult a p dvd q" - then obtain k where "q = smult a p * k" .. + from assms obtain k where "q = smult a p * k" .. then have "q = p * smult a k" by simp then show "p dvd q" .. qed -lemma smult_dvd: - fixes a :: "'a::field" - shows "p dvd q \ a \ 0 \ smult a p dvd q" +lemma smult_dvd: "p dvd q \ a \ 0 \ smult a p dvd q" + for a :: "'a::field" by (rule smult_dvd_cancel [where a="inverse a"]) simp -lemma smult_dvd_iff: - fixes a :: "'a::field" - shows "smult a p dvd q \ (if a = 0 then q = 0 else p dvd q)" +lemma smult_dvd_iff: "smult a p dvd q \ (if a = 0 then q = 0 else p dvd q)" + for a :: "'a::field" by (auto elim: smult_dvd smult_dvd_cancel) lemma is_unit_smult_iff: "smult c p dvd 1 \ c dvd 1 \ p dvd 1" @@ -1358,19 +1296,28 @@ have "smult c p = [:c:] * p" by simp also have "\ dvd 1 \ c dvd 1 \ p dvd 1" proof safe - assume A: "[:c:] * p dvd 1" - thus "p dvd 1" by (rule dvd_mult_right) - from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE) - have "c dvd c * (coeff p 0 * coeff q 0)" by simp - also have "\ = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult) - also note B [symmetric] - finally show "c dvd 1" by simp + assume *: "[:c:] * p dvd 1" + then show "p dvd 1" + by (rule dvd_mult_right) + from * obtain q where q: "1 = [:c:] * p * q" + by (rule dvdE) + have "c dvd c * (coeff p 0 * coeff q 0)" + by simp + also have "\ = coeff ([:c:] * p * q) 0" + by (simp add: mult.assoc coeff_mult) + also note q [symmetric] + finally have "c dvd coeff 1 0" . + then show "c dvd 1" by simp next assume "c dvd 1" "p dvd 1" - from \c dvd 1\ obtain d where "1 = c * d" by (erule dvdE) - hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac) - hence "[:c:] dvd 1" by (rule dvdI) - from mult_dvd_mono[OF this \p dvd 1\] show "[:c:] * p dvd 1" by simp + from this(1) obtain d where "1 = c * d" + by (rule dvdE) + then have "1 = [:c:] * [:d:]" + by (simp add: one_poly_def mult_ac) + then have "[:c:] dvd 1" + by (rule dvdI) + from mult_dvd_mono[OF this \p dvd 1\] show "[:c:] * p dvd 1" + by simp qed finally show ?thesis . qed @@ -1380,17 +1327,14 @@ instance poly :: (idom) idom .. -lemma degree_mult_eq: - fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" - shows "\p \ 0; q \ 0\ \ degree (p * q) = degree p + degree q" -apply (rule order_antisym [OF degree_mult_le le_degree]) -apply (simp add: coeff_mult_degree_sum) -done +lemma degree_mult_eq: "p \ 0 \ q \ 0 \ degree (p * q) = degree p + degree q" + for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" + by (rule order_antisym [OF degree_mult_le le_degree]) (simp add: coeff_mult_degree_sum) lemma degree_mult_eq_0: - fixes p q:: "'a :: {comm_semiring_0,semiring_no_zero_divisors} poly" - shows "degree (p * q) = 0 \ p = 0 \ q = 0 \ (p \ 0 \ q \ 0 \ degree p = 0 \ degree q = 0)" - by (auto simp add: degree_mult_eq) + "degree (p * q) = 0 \ p = 0 \ q = 0 \ (p \ 0 \ q \ 0 \ degree p = 0 \ degree q = 0)" + for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" + by (auto simp: degree_mult_eq) lemma degree_mult_right_le: fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" @@ -1398,55 +1342,59 @@ shows "degree p \ degree (p * q)" using assms by (cases "p = 0") (simp_all add: degree_mult_eq) -lemma coeff_degree_mult: - fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" - shows "coeff (p * q) (degree (p * q)) = - coeff q (degree q) * coeff p (degree p)" - by (cases "p = 0 \ q = 0") (auto simp add: degree_mult_eq coeff_mult_degree_sum mult_ac) - -lemma dvd_imp_degree_le: - fixes p q :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" - shows "\p dvd q; q \ 0\ \ degree p \ degree q" +lemma coeff_degree_mult: "coeff (p * q) (degree (p * q)) = coeff q (degree q) * coeff p (degree p)" + for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" + by (cases "p = 0 \ q = 0") (auto simp: degree_mult_eq coeff_mult_degree_sum mult_ac) + +lemma dvd_imp_degree_le: "p dvd q \ q \ 0 \ degree p \ degree q" + for p q :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" by (erule dvdE, hypsubst, subst degree_mult_eq) auto lemma divides_degree: - assumes pq: "p dvd (q :: 'a ::{comm_semiring_1,semiring_no_zero_divisors} poly)" + fixes p q :: "'a ::{comm_semiring_1,semiring_no_zero_divisors} poly" + assumes "p dvd q" shows "degree p \ degree q \ q = 0" - by (metis dvd_imp_degree_le pq) - + by (metis dvd_imp_degree_le assms) + lemma const_poly_dvd_iff: - fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}" + fixes c :: "'a::{comm_semiring_1,semiring_no_zero_divisors}" shows "[:c:] dvd p \ (\n. c dvd coeff p n)" proof (cases "c = 0 \ p = 0") + case True + then show ?thesis + by (auto intro!: poly_eqI) +next case False show ?thesis proof assume "[:c:] dvd p" - thus "\n. c dvd coeff p n" by (auto elim!: dvdE simp: coeffs_def) + then show "\n. c dvd coeff p n" + by (auto elim!: dvdE simp: coeffs_def) next assume *: "\n. c dvd coeff p n" - define mydiv where "mydiv = (\x y :: 'a. SOME z. x = y * z)" + define mydiv where "mydiv x y = (SOME z. x = y * z)" for x y :: 'a have mydiv: "x = y * mydiv x y" if "y dvd x" for x y using that unfolding mydiv_def dvd_def by (rule someI_ex) define q where "q = Poly (map (\a. mydiv a c) (coeffs p))" from False * have "p = q * [:c:]" - by (intro poly_eqI) (auto simp: q_def nth_default_def not_less length_coeffs_degree - coeffs_nth intro!: coeff_eq_0 mydiv) - thus "[:c:] dvd p" by (simp only: dvd_triv_right) + by (intro poly_eqI) + (auto simp: q_def nth_default_def not_less length_coeffs_degree coeffs_nth + intro!: coeff_eq_0 mydiv) + then show "[:c:] dvd p" + by (simp only: dvd_triv_right) qed -qed (auto intro!: poly_eqI) - -lemma const_poly_dvd_const_poly_iff [simp]: - "[:a::'a::{comm_semiring_1,semiring_no_zero_divisors}:] dvd [:b:] \ a dvd b" +qed + +lemma const_poly_dvd_const_poly_iff [simp]: "[:a:] dvd [:b:] \ a dvd b" + for a b :: "'a::{comm_semiring_1,semiring_no_zero_divisors}" by (subst const_poly_dvd_iff) (auto simp: coeff_pCons split: nat.splits) -lemma lead_coeff_mult: - fixes p q :: "'a :: {comm_semiring_0, semiring_no_zero_divisors} poly" - shows "lead_coeff (p * q) = lead_coeff p * lead_coeff q" - by (cases "p=0 \ q=0", auto simp add:coeff_mult_degree_sum degree_mult_eq) - -lemma lead_coeff_smult: - "lead_coeff (smult c p :: 'a :: {comm_semiring_0,semiring_no_zero_divisors} poly) = c * lead_coeff p" +lemma lead_coeff_mult: "lead_coeff (p * q) = lead_coeff p * lead_coeff q" + for p q :: "'a::{comm_semiring_0, semiring_no_zero_divisors} poly" + by (cases "p = 0 \ q = 0") (auto simp: coeff_mult_degree_sum degree_mult_eq) + +lemma lead_coeff_smult: "lead_coeff (smult c p) = c * lead_coeff p" + for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" proof - have "smult c p = [:c:] * p" by simp also have "lead_coeff \ = c * lead_coeff p" @@ -1457,67 +1405,69 @@ lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1" by simp -lemma lead_coeff_power: - "lead_coeff (p ^ n :: 'a :: {comm_semiring_1,semiring_no_zero_divisors} poly) = lead_coeff p ^ n" - by (induction n) (simp_all add: lead_coeff_mult) +lemma lead_coeff_power: "lead_coeff (p ^ n) = lead_coeff p ^ n" + for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" + by (induct n) (simp_all add: lead_coeff_mult) subsection \Polynomials form an ordered integral domain\ definition pos_poly :: "'a::linordered_semidom poly \ bool" -where - "pos_poly p \ 0 < coeff p (degree p)" - -lemma pos_poly_pCons: - "pos_poly (pCons a p) \ pos_poly p \ (p = 0 \ 0 < a)" - unfolding pos_poly_def by simp + where "pos_poly p \ 0 < coeff p (degree p)" + +lemma pos_poly_pCons: "pos_poly (pCons a p) \ pos_poly p \ (p = 0 \ 0 < a)" + by (simp add: pos_poly_def) lemma not_pos_poly_0 [simp]: "\ pos_poly 0" - unfolding pos_poly_def by simp - -lemma pos_poly_add: "\pos_poly p; pos_poly q\ \ pos_poly (p + q)" - apply (induct p arbitrary: q, simp) - apply (case_tac q, force simp add: pos_poly_pCons add_pos_pos) + by (simp add: pos_poly_def) + +lemma pos_poly_add: "pos_poly p \ pos_poly q \ pos_poly (p + q)" + apply (induct p arbitrary: q) + apply simp + apply (case_tac q) + apply (force simp add: pos_poly_pCons add_pos_pos) done -lemma pos_poly_mult: "\pos_poly p; pos_poly q\ \ pos_poly (p * q)" +lemma pos_poly_mult: "pos_poly p \ pos_poly q \ pos_poly (p * q)" unfolding pos_poly_def apply (subgoal_tac "p \ 0 \ q \ 0") - apply (simp add: degree_mult_eq coeff_mult_degree_sum) + apply (simp add: degree_mult_eq coeff_mult_degree_sum) apply auto done -lemma pos_poly_total: "(p :: 'a :: linordered_idom poly) = 0 \ pos_poly p \ pos_poly (- p)" -by (induct p) (auto simp add: pos_poly_pCons) - -lemma last_coeffs_eq_coeff_degree: - "p \ 0 \ last (coeffs p) = coeff p (degree p)" +lemma pos_poly_total: "p = 0 \ pos_poly p \ pos_poly (- p)" + for p :: "'a::linordered_idom poly" + by (induct p) (auto simp: pos_poly_pCons) + +lemma last_coeffs_eq_coeff_degree: "p \ 0 \ last (coeffs p) = coeff p (degree p)" by (simp add: coeffs_def) -lemma pos_poly_coeffs [code]: - "pos_poly p \ (let as = coeffs p in as \ [] \ last as > 0)" (is "?P \ ?Q") +lemma pos_poly_coeffs [code]: "pos_poly p \ (let as = coeffs p in as \ [] \ last as > 0)" + (is "?lhs \ ?rhs") proof - assume ?Q then show ?P by (auto simp add: pos_poly_def last_coeffs_eq_coeff_degree) + assume ?rhs + then show ?lhs + by (auto simp add: pos_poly_def last_coeffs_eq_coeff_degree) next - assume ?P then have *: "0 < coeff p (degree p)" by (simp add: pos_poly_def) - then have "p \ 0" by auto - with * show ?Q by (simp add: last_coeffs_eq_coeff_degree) + assume ?lhs + then have *: "0 < coeff p (degree p)" + by (simp add: pos_poly_def) + then have "p \ 0" + by auto + with * show ?rhs + by (simp add: last_coeffs_eq_coeff_degree) qed instantiation poly :: (linordered_idom) linordered_idom begin -definition - "x < y \ pos_poly (y - x)" - -definition - "x \ y \ x = y \ pos_poly (y - x)" - -definition - "\x::'a poly\ = (if x < 0 then - x else x)" - -definition - "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)" +definition "x < y \ pos_poly (y - x)" + +definition "x \ y \ x = y \ pos_poly (y - x)" + +definition "\x::'a poly\ = (if x < 0 then - x else x)" + +definition "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)" instance proof @@ -1525,12 +1475,12 @@ show "x < y \ x \ y \ \ y \ x" unfolding less_eq_poly_def less_poly_def apply safe - apply simp + apply simp apply (drule (1) pos_poly_add) apply simp done show "x \ x" - unfolding less_eq_poly_def by simp + by (simp add: less_eq_poly_def) show "x \ y \ y \ z \ x \ z" unfolding less_eq_poly_def apply safe @@ -1553,8 +1503,7 @@ using pos_poly_total [of "x - y"] by auto show "x < y \ 0 < z \ z * x < z * y" - unfolding less_poly_def - by (simp add: right_diff_distrib [symmetric] pos_poly_mult) + by (simp add: less_poly_def right_diff_distrib [symmetric] pos_poly_mult) show "\x\ = (if x < 0 then - x else x)" by (rule abs_poly_def) show "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)" @@ -1568,46 +1517,37 @@ subsection \Synthetic division and polynomial roots\ -subsubsection \Synthetic division\ - -text \ - Synthetic division is simply division by the linear polynomial @{term "x - c"}. -\ +subsubsection \Synthetic division\ + +text \Synthetic division is simply division by the linear polynomial @{term "x - c"}.\ definition synthetic_divmod :: "'a::comm_semiring_0 poly \ 'a \ 'a poly \ 'a" -where - "synthetic_divmod p c = fold_coeffs (\a (q, r). (pCons r q, a + c * r)) p (0, 0)" + where "synthetic_divmod p c = fold_coeffs (\a (q, r). (pCons r q, a + c * r)) p (0, 0)" definition synthetic_div :: "'a::comm_semiring_0 poly \ 'a \ 'a poly" -where - "synthetic_div p c = fst (synthetic_divmod p c)" - -lemma synthetic_divmod_0 [simp]: - "synthetic_divmod 0 c = (0, 0)" + where "synthetic_div p c = fst (synthetic_divmod p c)" + +lemma synthetic_divmod_0 [simp]: "synthetic_divmod 0 c = (0, 0)" by (simp add: synthetic_divmod_def) lemma synthetic_divmod_pCons [simp]: "synthetic_divmod (pCons a p) c = (\(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)" by (cases "p = 0 \ a = 0") (auto simp add: synthetic_divmod_def) -lemma synthetic_div_0 [simp]: - "synthetic_div 0 c = 0" - unfolding synthetic_div_def by simp +lemma synthetic_div_0 [simp]: "synthetic_div 0 c = 0" + by (simp add: synthetic_div_def) lemma synthetic_div_unique_lemma: "smult c p = pCons a p \ p = 0" -by (induct p arbitrary: a) simp_all - -lemma snd_synthetic_divmod: - "snd (synthetic_divmod p c) = poly p c" - by (induct p, simp, simp add: split_def) + by (induct p arbitrary: a) simp_all + +lemma snd_synthetic_divmod: "snd (synthetic_divmod p c) = poly p c" + by (induct p) (simp_all add: split_def) lemma synthetic_div_pCons [simp]: "synthetic_div (pCons a p) c = pCons (poly p c) (synthetic_div p c)" - unfolding synthetic_div_def - by (simp add: split_def snd_synthetic_divmod) - -lemma synthetic_div_eq_0_iff: - "synthetic_div p c = 0 \ degree p = 0" + by (simp add: synthetic_div_def split_def snd_synthetic_divmod) + +lemma synthetic_div_eq_0_iff: "synthetic_div p c = 0 \ degree p = 0" proof (induct p) case 0 then show ?case by simp @@ -1616,59 +1556,55 @@ then show ?case by (cases p) simp qed -lemma degree_synthetic_div: - "degree (synthetic_div p c) = degree p - 1" +lemma degree_synthetic_div: "degree (synthetic_div p c) = degree p - 1" by (induct p) (simp_all add: synthetic_div_eq_0_iff) lemma synthetic_div_correct: "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)" by (induct p) simp_all -lemma synthetic_div_unique: - "p + smult c q = pCons r q \ r = poly p c \ q = synthetic_div p c" -apply (induct p arbitrary: q r) -apply (simp, frule synthetic_div_unique_lemma, simp) -apply (case_tac q, force) -done - -lemma synthetic_div_correct': - fixes c :: "'a::comm_ring_1" - shows "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p" - using synthetic_div_correct [of p c] - by (simp add: algebra_simps) - - +lemma synthetic_div_unique: "p + smult c q = pCons r q \ r = poly p c \ q = synthetic_div p c" + apply (induct p arbitrary: q r) + apply simp + apply (frule synthetic_div_unique_lemma) + apply simp + apply (case_tac q, force) + done + +lemma synthetic_div_correct': "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p" + for c :: "'a::comm_ring_1" + using synthetic_div_correct [of p c] by (simp add: algebra_simps) + + subsubsection \Polynomial roots\ - -lemma poly_eq_0_iff_dvd: - fixes c :: "'a::{comm_ring_1}" - shows "poly p c = 0 \ [:- c, 1:] dvd p" + +lemma poly_eq_0_iff_dvd: "poly p c = 0 \ [:- c, 1:] dvd p" + (is "?lhs \ ?rhs") + for c :: "'a::comm_ring_1" proof - assume "poly p c = 0" - with synthetic_div_correct' [of c p] - have "p = [:-c, 1:] * synthetic_div p c" by simp - then show "[:-c, 1:] dvd p" .. + assume ?lhs + with synthetic_div_correct' [of c p] have "p = [:-c, 1:] * synthetic_div p c" by simp + then show ?rhs .. next - assume "[:-c, 1:] dvd p" + assume ?rhs then obtain k where "p = [:-c, 1:] * k" by (rule dvdE) - then show "poly p c = 0" by simp + then show ?lhs by simp qed -lemma dvd_iff_poly_eq_0: - fixes c :: "'a::{comm_ring_1}" - shows "[:c, 1:] dvd p \ poly p (- c) = 0" +lemma dvd_iff_poly_eq_0: "[:c, 1:] dvd p \ poly p (- c) = 0" + for c :: "'a::comm_ring_1" by (simp add: poly_eq_0_iff_dvd) -lemma poly_roots_finite: - fixes p :: "'a::{comm_ring_1,ring_no_zero_divisors} poly" - shows "p \ 0 \ finite {x. poly p x = 0}" +lemma poly_roots_finite: "p \ 0 \ finite {x. poly p x = 0}" + for p :: "'a::{comm_ring_1,ring_no_zero_divisors} poly" proof (induct n \ "degree p" arbitrary: p) - case (0 p) + case 0 then obtain a where "a \ 0" and "p = [:a:]" - by (cases p, simp split: if_splits) - then show "finite {x. poly p x = 0}" by simp + by (cases p) (simp split: if_splits) + then show "finite {x. poly p x = 0}" + by simp next - case (Suc n p) + case (Suc n) show "finite {x. poly p x = 0}" proof (cases "\x. poly p x = 0") case False @@ -1676,84 +1612,92 @@ next case True then obtain a where "poly p a = 0" .. - then have "[:-a, 1:] dvd p" by (simp only: poly_eq_0_iff_dvd) + then have "[:-a, 1:] dvd p" + by (simp only: poly_eq_0_iff_dvd) then obtain k where k: "p = [:-a, 1:] * k" .. - with \p \ 0\ have "k \ 0" by auto + with \p \ 0\ have "k \ 0" + by auto with k have "degree p = Suc (degree k)" by (simp add: degree_mult_eq del: mult_pCons_left) - with \Suc n = degree p\ have "n = degree k" by simp - then have "finite {x. poly k x = 0}" using \k \ 0\ by (rule Suc.hyps) - then have "finite (insert a {x. poly k x = 0})" by simp + with \Suc n = degree p\ have "n = degree k" + by simp + from this \k \ 0\ have "finite {x. poly k x = 0}" + by (rule Suc.hyps) + then have "finite (insert a {x. poly k x = 0})" + by simp then show "finite {x. poly p x = 0}" by (simp add: k Collect_disj_eq del: mult_pCons_left) qed qed -lemma poly_eq_poly_eq_iff: - fixes p q :: "'a::{comm_ring_1,ring_no_zero_divisors,ring_char_0} poly" - shows "poly p = poly q \ p = q" (is "?P \ ?Q") +lemma poly_eq_poly_eq_iff: "poly p = poly q \ p = q" + (is "?lhs \ ?rhs") + for p q :: "'a::{comm_ring_1,ring_no_zero_divisors,ring_char_0} poly" proof - assume ?Q then show ?P by simp + assume ?rhs + then show ?lhs by simp next - { fix p :: "'a poly" - have "poly p = poly 0 \ p = 0" - apply (cases "p = 0", simp_all) - apply (drule poly_roots_finite) - apply (auto simp add: infinite_UNIV_char_0) - done - } note this [of "p - q"] - moreover assume ?P - ultimately show ?Q by auto + assume ?lhs + have "poly p = poly 0 \ p = 0" for p :: "'a poly" + apply (cases "p = 0") + apply simp_all + apply (drule poly_roots_finite) + apply (auto simp add: infinite_UNIV_char_0) + done + from \?lhs\ and this [of "p - q"] show ?rhs + by auto qed -lemma poly_all_0_iff_0: - fixes p :: "'a::{ring_char_0, comm_ring_1,ring_no_zero_divisors} poly" - shows "(\x. poly p x = 0) \ p = 0" +lemma poly_all_0_iff_0: "(\x. poly p x = 0) \ p = 0" + for p :: "'a::{ring_char_0,comm_ring_1,ring_no_zero_divisors} poly" by (auto simp add: poly_eq_poly_eq_iff [symmetric]) - + subsubsection \Order of polynomial roots\ definition order :: "'a::idom \ 'a poly \ nat" -where - "order a p = (LEAST n. \ [:-a, 1:] ^ Suc n dvd p)" - -lemma coeff_linear_power: - fixes a :: "'a::comm_semiring_1" - shows "coeff ([:a, 1:] ^ n) n = 1" -apply (induct n, simp_all) -apply (subst coeff_eq_0) -apply (auto intro: le_less_trans degree_power_le) -done - -lemma degree_linear_power: - fixes a :: "'a::comm_semiring_1" - shows "degree ([:a, 1:] ^ n) = n" -apply (rule order_antisym) -apply (rule ord_le_eq_trans [OF degree_power_le], simp) -apply (rule le_degree, simp add: coeff_linear_power) -done + where "order a p = (LEAST n. \ [:-a, 1:] ^ Suc n dvd p)" + +lemma coeff_linear_power: "coeff ([:a, 1:] ^ n) n = 1" + for a :: "'a::comm_semiring_1" + apply (induct n) + apply simp_all + apply (subst coeff_eq_0) + apply (auto intro: le_less_trans degree_power_le) + done + +lemma degree_linear_power: "degree ([:a, 1:] ^ n) = n" + for a :: "'a::comm_semiring_1" + apply (rule order_antisym) + apply (rule ord_le_eq_trans [OF degree_power_le]) + apply simp + apply (rule le_degree) + apply (simp add: coeff_linear_power) + done lemma order_1: "[:-a, 1:] ^ order a p dvd p" -apply (cases "p = 0", simp) -apply (cases "order a p", simp) -apply (subgoal_tac "nat < (LEAST n. \ [:-a, 1:] ^ Suc n dvd p)") -apply (drule not_less_Least, simp) -apply (fold order_def, simp) -done + apply (cases "p = 0") + apply simp + apply (cases "order a p") + apply simp + apply (subgoal_tac "nat < (LEAST n. \ [:-a, 1:] ^ Suc n dvd p)") + apply (drule not_less_Least) + apply simp + apply (fold order_def) + apply simp + done lemma order_2: "p \ 0 \ \ [:-a, 1:] ^ Suc (order a p) dvd p" -unfolding order_def -apply (rule LeastI_ex) -apply (rule_tac x="degree p" in exI) -apply (rule notI) -apply (drule (1) dvd_imp_degree_le) -apply (simp only: degree_linear_power) -done - -lemma order: - "p \ 0 \ [:-a, 1:] ^ order a p dvd p \ \ [:-a, 1:] ^ Suc (order a p) dvd p" -by (rule conjI [OF order_1 order_2]) + unfolding order_def + apply (rule LeastI_ex) + apply (rule_tac x="degree p" in exI) + apply (rule notI) + apply (drule (1) dvd_imp_degree_le) + apply (simp only: degree_linear_power) + done + +lemma order: "p \ 0 \ [:-a, 1:] ^ order a p dvd p \ \ [:-a, 1:] ^ Suc (order a p) dvd p" + by (rule conjI [OF order_1 order_2]) lemma order_degree: assumes p: "p \ 0" @@ -1761,18 +1705,19 @@ proof - have "order a p = degree ([:-a, 1:] ^ order a p)" by (simp only: degree_linear_power) - also have "\ \ degree p" - using order_1 p by (rule dvd_imp_degree_le) + also from order_1 p have "\ \ degree p" + by (rule dvd_imp_degree_le) finally show ?thesis . qed lemma order_root: "poly p a = 0 \ p = 0 \ order a p \ 0" -apply (cases "p = 0", simp_all) -apply (rule iffI) -apply (metis order_2 not_gr0 poly_eq_0_iff_dvd power_0 power_Suc_0 power_one_right) -unfolding poly_eq_0_iff_dvd -apply (metis dvd_power dvd_trans order_1) -done + apply (cases "p = 0") + apply simp_all + apply (rule iffI) + apply (metis order_2 not_gr0 poly_eq_0_iff_dvd power_0 power_Suc_0 power_one_right) + unfolding poly_eq_0_iff_dvd + apply (metis dvd_power dvd_trans order_1) + done lemma order_0I: "poly p a \ 0 \ order a p = 0" by (subst (asm) order_root) auto @@ -1781,23 +1726,24 @@ fixes p :: "'a::idom poly" assumes "[:-a, 1:] ^ n dvd p" "\ [:-a, 1:] ^ Suc n dvd p" shows "n = order a p" -unfolding Polynomial.order_def -apply (rule Least_equality [symmetric]) -apply (fact assms) -apply (rule classical) -apply (erule notE) -unfolding not_less_eq_eq -using assms(1) apply (rule power_le_dvd) -apply assumption + unfolding Polynomial.order_def + apply (rule Least_equality [symmetric]) + apply (fact assms) + apply (rule classical) + apply (erule notE) + unfolding not_less_eq_eq + using assms(1) + apply (rule power_le_dvd) + apply assumption done - + lemma order_mult: "p * q \ 0 \ order a (p * q) = order a p + order a q" proof - define i where "i = order a p" define j where "j = order a q" define t where "t = [:-a, 1:]" have t_dvd_iff: "\u. t dvd u \ poly u a = 0" - unfolding t_def by (simp add: dvd_iff_poly_eq_0) + by (simp add: t_def dvd_iff_poly_eq_0) assume "p * q \ 0" then show "order a (p * q) = i + j" apply clarsimp @@ -1806,255 +1752,252 @@ apply clarify apply (erule dvdE)+ apply (rule order_unique_lemma [symmetric], fold t_def) - apply (simp_all add: power_add t_dvd_iff) + apply (simp_all add: power_add t_dvd_iff) done qed lemma order_smult: - assumes "c \ 0" + assumes "c \ 0" shows "order x (smult c p) = order x p" proof (cases "p = 0") + case True + then show ?thesis + by simp +next case False have "smult c p = [:c:] * p" by simp - also from assms False have "order x \ = order x [:c:] + order x p" + also from assms False have "order x \ = order x [:c:] + order x p" by (subst order_mult) simp_all - also from assms have "order x [:c:] = 0" by (intro order_0I) auto - finally show ?thesis by simp -qed simp + also have "order x [:c:] = 0" + by (rule order_0I) (use assms in auto) + finally show ?thesis + by simp +qed (* Next two lemmas contributed by Wenda Li *) -lemma order_1_eq_0 [simp]:"order x 1 = 0" +lemma order_1_eq_0 [simp]:"order x 1 = 0" by (metis order_root poly_1 zero_neq_one) -lemma order_power_n_n: "order a ([:-a,1:]^n)=n" +lemma order_power_n_n: "order a ([:-a,1:]^n)=n" proof (induct n) (*might be proved more concisely using nat_less_induct*) case 0 - thus ?case by (metis order_root poly_1 power_0 zero_neq_one) -next + then show ?case + by (metis order_root poly_1 power_0 zero_neq_one) +next case (Suc n) - have "order a ([:- a, 1:] ^ Suc n)=order a ([:- a, 1:] ^ n) + order a [:-a,1:]" - by (metis (no_types, hide_lams) One_nat_def add_Suc_right monoid_add_class.add.right_neutral + have "order a ([:- a, 1:] ^ Suc n) = order a ([:- a, 1:] ^ n) + order a [:-a,1:]" + by (metis (no_types, hide_lams) One_nat_def add_Suc_right monoid_add_class.add.right_neutral one_neq_zero order_mult pCons_eq_0_iff power_add power_eq_0_iff power_one_right) - moreover have "order a [:-a,1:]=1" unfolding order_def - proof (rule Least_equality,rule ccontr) - assume "\ \ [:- a, 1:] ^ Suc 1 dvd [:- a, 1:]" - hence "[:- a, 1:] ^ Suc 1 dvd [:- a, 1:]" by simp - hence "degree ([:- a, 1:] ^ Suc 1) \ degree ([:- a, 1:] )" - by (rule dvd_imp_degree_le,auto) - thus False by auto - next - fix y assume asm:"\ [:- a, 1:] ^ Suc y dvd [:- a, 1:]" - show "1 \ y" - proof (rule ccontr) - assume "\ 1 \ y" - hence "y=0" by auto - hence "[:- a, 1:] ^ Suc y dvd [:- a, 1:]" by auto - thus False using asm by auto - qed + moreover have "order a [:-a,1:] = 1" + unfolding order_def + proof (rule Least_equality, rule notI) + assume "[:- a, 1:] ^ Suc 1 dvd [:- a, 1:]" + then have "degree ([:- a, 1:] ^ Suc 1) \ degree ([:- a, 1:])" + by (rule dvd_imp_degree_le) auto + then show False + by auto + next + fix y + assume *: "\ [:- a, 1:] ^ Suc y dvd [:- a, 1:]" + show "1 \ y" + proof (rule ccontr) + assume "\ 1 \ y" + then have "y = 0" by auto + then have "[:- a, 1:] ^ Suc y dvd [:- a, 1:]" by auto + with * show False by auto qed - ultimately show ?case using Suc by auto + qed + ultimately show ?case + using Suc by auto qed -lemma order_0_monom [simp]: - assumes "c \ 0" - shows "order 0 (monom c n) = n" - using assms order_power_n_n[of 0 n] by (simp add: monom_altdef order_smult) - -lemma dvd_imp_order_le: - "q \ 0 \ p dvd q \ Polynomial.order a p \ Polynomial.order a q" +lemma order_0_monom [simp]: "c \ 0 \ order 0 (monom c n) = n" + using order_power_n_n[of 0 n] by (simp add: monom_altdef order_smult) + +lemma dvd_imp_order_le: "q \ 0 \ p dvd q \ Polynomial.order a p \ Polynomial.order a q" by (auto simp: order_mult elim: dvdE) -text\Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').\ +text \Now justify the standard squarefree decomposition, i.e. \f / gcd f f'\.\ lemma order_divides: "[:-a, 1:] ^ n dvd p \ p = 0 \ n \ order a p" -apply (cases "p = 0", auto) -apply (drule order_2 [where a=a and p=p]) -apply (metis not_less_eq_eq power_le_dvd) -apply (erule power_le_dvd [OF order_1]) -done + apply (cases "p = 0") + apply auto + apply (drule order_2 [where a=a and p=p]) + apply (metis not_less_eq_eq power_le_dvd) + apply (erule power_le_dvd [OF order_1]) + done lemma order_decomp: assumes "p \ 0" shows "\q. p = [:- a, 1:] ^ order a p * q \ \ [:- a, 1:] dvd q" proof - - from assms have A: "[:- a, 1:] ^ order a p dvd p" - and B: "\ [:- a, 1:] ^ Suc (order a p) dvd p" by (auto dest: order) - from A obtain q where C: "p = [:- a, 1:] ^ order a p * q" .. - with B have "\ [:- a, 1:] ^ Suc (order a p) dvd [:- a, 1:] ^ order a p * q" + from assms have *: "[:- a, 1:] ^ order a p dvd p" + and **: "\ [:- a, 1:] ^ Suc (order a p) dvd p" + by (auto dest: order) + from * obtain q where q: "p = [:- a, 1:] ^ order a p * q" .. + with ** have "\ [:- a, 1:] ^ Suc (order a p) dvd [:- a, 1:] ^ order a p * q" by simp then have "\ [:- a, 1:] ^ order a p * [:- a, 1:] dvd [:- a, 1:] ^ order a p * q" by simp - then have D: "\ [:- a, 1:] dvd q" - using idom_class.dvd_mult_cancel_left [of "[:- a, 1:] ^ order a p" "[:- a, 1:]" q] - by auto - from C D show ?thesis by blast + with idom_class.dvd_mult_cancel_left [of "[:- a, 1:] ^ order a p" "[:- a, 1:]" q] + have "\ [:- a, 1:] dvd q" by auto + with q show ?thesis by blast qed -lemma monom_1_dvd_iff: - assumes "p \ 0" - shows "monom 1 n dvd p \ n \ order 0 p" - using assms order_divides[of 0 n p] by (simp add: monom_altdef) +lemma monom_1_dvd_iff: "p \ 0 \ monom 1 n dvd p \ n \ order 0 p" + using order_divides[of 0 n p] by (simp add: monom_altdef) subsection \Additional induction rules on polynomials\ text \ - An induction rule for induction over the roots of a polynomial with a certain property. + An induction rule for induction over the roots of a polynomial with a certain property. (e.g. all positive roots) \ lemma poly_root_induct [case_names 0 no_roots root]: fixes p :: "'a :: idom poly" assumes "Q 0" - assumes "\p. (\a. P a \ poly p a \ 0) \ Q p" - assumes "\a p. P a \ Q p \ Q ([:a, -1:] * p)" - shows "Q p" + and "\p. (\a. P a \ poly p a \ 0) \ Q p" + and "\a p. P a \ Q p \ Q ([:a, -1:] * p)" + shows "Q p" proof (induction "degree p" arbitrary: p rule: less_induct) case (less p) show ?case proof (cases "p = 0") - assume nz: "p \ 0" - show ?case + case True + with assms(1) show ?thesis by simp + next + case False + show ?thesis proof (cases "\a. P a \ poly p a = 0") case False - thus ?thesis by (intro assms(2)) blast + then show ?thesis by (intro assms(2)) blast next case True - then obtain a where a: "P a" "poly p a = 0" + then obtain a where a: "P a" "poly p a = 0" by blast - hence "-[:-a, 1:] dvd p" + then have "-[:-a, 1:] dvd p" by (subst minus_dvd_iff) (simp add: poly_eq_0_iff_dvd) then obtain q where q: "p = [:a, -1:] * q" by (elim dvdE) simp - with nz have q_nz: "q \ 0" by auto + with False have "q \ 0" by auto have "degree p = Suc (degree q)" - by (subst q, subst degree_mult_eq) (simp_all add: q_nz) - hence "Q q" by (intro less) simp - from a(1) and this have "Q ([:a, -1:] * q)" + by (subst q, subst degree_mult_eq) (simp_all add: \q \ 0\) + then have "Q q" by (intro less) simp + with a(1) have "Q ([:a, -1:] * q)" by (rule assms(3)) with q show ?thesis by simp qed - qed (simp add: assms(1)) + qed qed -lemma dropWhile_replicate_append: - "dropWhile (op= a) (replicate n a @ ys) = dropWhile (op= a) ys" - by (induction n) simp_all +lemma dropWhile_replicate_append: + "dropWhile (op = a) (replicate n a @ ys) = dropWhile (op = a) ys" + by (induct n) simp_all lemma Poly_append_replicate_0: "Poly (xs @ replicate n 0) = Poly xs" by (subst coeffs_eq_iff) (simp_all add: strip_while_def dropWhile_replicate_append) text \ - An induction rule for simultaneous induction over two polynomials, + An induction rule for simultaneous induction over two polynomials, prepending one coefficient in each step. \ lemma poly_induct2 [case_names 0 pCons]: assumes "P 0 0" "\a p b q. P p q \ P (pCons a p) (pCons b q)" - shows "P p q" + shows "P p q" proof - define n where "n = max (length (coeffs p)) (length (coeffs q))" define xs where "xs = coeffs p @ (replicate (n - length (coeffs p)) 0)" define ys where "ys = coeffs q @ (replicate (n - length (coeffs q)) 0)" - have "length xs = length ys" + have "length xs = length ys" by (simp add: xs_def ys_def n_def) - hence "P (Poly xs) (Poly ys)" - by (induction rule: list_induct2) (simp_all add: assms) - also have "Poly xs = p" + then have "P (Poly xs) (Poly ys)" + by (induct rule: list_induct2) (simp_all add: assms) + also have "Poly xs = p" by (simp add: xs_def Poly_append_replicate_0) - also have "Poly ys = q" + also have "Poly ys = q" by (simp add: ys_def Poly_append_replicate_0) finally show ?thesis . qed - + subsection \Composition of polynomials\ (* Several lemmas contributed by René Thiemann and Akihisa Yamada *) definition pcompose :: "'a::comm_semiring_0 poly \ 'a poly \ 'a poly" -where - "pcompose p q = fold_coeffs (\a c. [:a:] + q * c) p 0" + where "pcompose p q = fold_coeffs (\a c. [:a:] + q * c) p 0" notation pcompose (infixl "\\<^sub>p" 71) -lemma pcompose_0 [simp]: - "pcompose 0 q = 0" +lemma pcompose_0 [simp]: "pcompose 0 q = 0" by (simp add: pcompose_def) - -lemma pcompose_pCons: - "pcompose (pCons a p) q = [:a:] + q * pcompose p q" + +lemma pcompose_pCons: "pcompose (pCons a p) q = [:a:] + q * pcompose p q" by (cases "p = 0 \ a = 0") (auto simp add: pcompose_def) -lemma pcompose_1: - fixes p :: "'a :: comm_semiring_1 poly" - shows "pcompose 1 p = 1" - unfolding one_poly_def by (auto simp: pcompose_pCons) - -lemma poly_pcompose: - "poly (pcompose p q) x = poly p (poly q x)" +lemma pcompose_1: "pcompose 1 p = 1" + for p :: "'a::comm_semiring_1 poly" + by (auto simp: one_poly_def pcompose_pCons) + +lemma poly_pcompose: "poly (pcompose p q) x = poly p (poly q x)" by (induct p) (simp_all add: pcompose_pCons) -lemma degree_pcompose_le: - "degree (pcompose p q) \ degree p * degree q" -apply (induct p, simp) -apply (simp add: pcompose_pCons, clarify) -apply (rule degree_add_le, simp) -apply (rule order_trans [OF degree_mult_le], simp) -done - -lemma pcompose_add: - fixes p q r :: "'a :: {comm_semiring_0, ab_semigroup_add} poly" - shows "pcompose (p + q) r = pcompose p r + pcompose q r" +lemma degree_pcompose_le: "degree (pcompose p q) \ degree p * degree q" + apply (induct p) + apply simp + apply (simp add: pcompose_pCons) + apply clarify + apply (rule degree_add_le) + apply simp + apply (rule order_trans [OF degree_mult_le]) + apply simp + done + +lemma pcompose_add: "pcompose (p + q) r = pcompose p r + pcompose q r" + for p q r :: "'a::{comm_semiring_0, ab_semigroup_add} poly" proof (induction p q rule: poly_induct2) + case 0 + then show ?case by simp +next case (pCons a p b q) - have "pcompose (pCons a p + pCons b q) r = - [:a + b:] + r * pcompose p r + r * pcompose q r" + have "pcompose (pCons a p + pCons b q) r = [:a + b:] + r * pcompose p r + r * pcompose q r" by (simp_all add: pcompose_pCons pCons.IH algebra_simps) also have "[:a + b:] = [:a:] + [:b:]" by simp - also have "\ + r * pcompose p r + r * pcompose q r = - pcompose (pCons a p) r + pcompose (pCons b q) r" + also have "\ + r * pcompose p r + r * pcompose q r = + pcompose (pCons a p) r + pcompose (pCons b q) r" by (simp only: pcompose_pCons add_ac) finally show ?case . -qed simp - -lemma pcompose_uminus: - fixes p r :: "'a :: comm_ring poly" - shows "pcompose (-p) r = -pcompose p r" - by (induction p) (simp_all add: pcompose_pCons) - -lemma pcompose_diff: - fixes p q r :: "'a :: comm_ring poly" - shows "pcompose (p - q) r = pcompose p r - pcompose q r" +qed + +lemma pcompose_uminus: "pcompose (-p) r = -pcompose p r" + for p r :: "'a::comm_ring poly" + by (induct p) (simp_all add: pcompose_pCons) + +lemma pcompose_diff: "pcompose (p - q) r = pcompose p r - pcompose q r" + for p q r :: "'a::comm_ring poly" using pcompose_add[of p "-q"] by (simp add: pcompose_uminus) -lemma pcompose_smult: - fixes p r :: "'a :: comm_semiring_0 poly" - shows "pcompose (smult a p) r = smult a (pcompose p r)" - by (induction p) - (simp_all add: pcompose_pCons pcompose_add smult_add_right) - -lemma pcompose_mult: - fixes p q r :: "'a :: comm_semiring_0 poly" - shows "pcompose (p * q) r = pcompose p r * pcompose q r" - by (induction p arbitrary: q) - (simp_all add: pcompose_add pcompose_smult pcompose_pCons algebra_simps) - -lemma pcompose_assoc: - "pcompose p (pcompose q r :: 'a :: comm_semiring_0 poly ) = - pcompose (pcompose p q) r" - by (induction p arbitrary: q) - (simp_all add: pcompose_pCons pcompose_add pcompose_mult) - -lemma pcompose_idR[simp]: - fixes p :: "'a :: comm_semiring_1 poly" - shows "pcompose p [: 0, 1 :] = p" - by (induct p; simp add: pcompose_pCons) +lemma pcompose_smult: "pcompose (smult a p) r = smult a (pcompose p r)" + for p r :: "'a::comm_semiring_0 poly" + by (induct p) (simp_all add: pcompose_pCons pcompose_add smult_add_right) + +lemma pcompose_mult: "pcompose (p * q) r = pcompose p r * pcompose q r" + for p q r :: "'a::comm_semiring_0 poly" + by (induct p arbitrary: q) (simp_all add: pcompose_add pcompose_smult pcompose_pCons algebra_simps) + +lemma pcompose_assoc: "pcompose p (pcompose q r) = pcompose (pcompose p q) r" + for p q r :: "'a::comm_semiring_0 poly" + by (induct p arbitrary: q) (simp_all add: pcompose_pCons pcompose_add pcompose_mult) + +lemma pcompose_idR[simp]: "pcompose p [: 0, 1 :] = p" + for p :: "'a::comm_semiring_1 poly" + by (induct p) (simp_all add: pcompose_pCons) lemma pcompose_sum: "pcompose (sum f A) p = sum (\i. pcompose (f i) p) A" - by (cases "finite A", induction rule: finite_induct) - (simp_all add: pcompose_1 pcompose_add) + by (induct A rule: infinite_finite_induct) (simp_all add: pcompose_1 pcompose_add) lemma pcompose_prod: "pcompose (prod f A) p = prod (\i. pcompose (f i) p) A" - by (cases "finite A", induction rule: finite_induct) - (simp_all add: pcompose_1 pcompose_mult) + by (induct A rule: infinite_finite_induct) (simp_all add: pcompose_1 pcompose_mult) lemma pcompose_const [simp]: "pcompose [:a:] q = [:a:]" by (subst pcompose_pCons) simp @@ -2062,117 +2005,133 @@ lemma pcompose_0': "pcompose p 0 = [:coeff p 0:]" by (induct p) (auto simp add: pcompose_pCons) -lemma degree_pcompose: - fixes p q:: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" - shows "degree (pcompose p q) = degree p * degree q" +lemma degree_pcompose: "degree (pcompose p q) = degree p * degree q" + for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" proof (induct p) case 0 - thus ?case by auto + then show ?case by auto next case (pCons a p) - have "degree (q * pcompose p q) = 0 \ ?case" - proof (cases "p=0") + consider "degree (q * pcompose p q) = 0" | "degree (q * pcompose p q) > 0" + by blast + then show ?case + proof cases + case prems: 1 + show ?thesis + proof (cases "p = 0") case True - thus ?thesis by auto + then show ?thesis by auto next - case False assume "degree (q * pcompose p q) = 0" - hence "degree q=0 \ pcompose p q=0" by (auto simp add: degree_mult_eq_0) - moreover have "\pcompose p q=0;degree q\0\ \ False" using pCons.hyps(2) \p\0\ - proof - - assume "pcompose p q=0" "degree q\0" - hence "degree p=0" using pCons.hyps(2) by auto - then obtain a1 where "p=[:a1:]" - by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases) - thus False using \pcompose p q=0\ \p\0\ by auto - qed - ultimately have "degree (pCons a p) * degree q=0" by auto - moreover have "degree (pcompose (pCons a p) q) = 0" - proof - - have" 0 = max (degree [:a:]) (degree (q*pcompose p q))" - using \degree (q * pcompose p q) = 0\ by simp - also have "... \ degree ([:a:] + q * pcompose p q)" - by (rule degree_add_le_max) - finally show ?thesis by (auto simp add:pcompose_pCons) - qed + case False + from prems have "degree q = 0 \ pcompose p q = 0" + by (auto simp add: degree_mult_eq_0) + moreover have False if "pcompose p q = 0" "degree q \ 0" + proof - + from pCons.hyps(2) that have "degree p = 0" + by auto + then obtain a1 where "p = [:a1:]" + by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases) + with \pcompose p q = 0\ \p \ 0\ show False + by auto + qed + ultimately have "degree (pCons a p) * degree q = 0" + by auto + moreover have "degree (pcompose (pCons a p) q) = 0" + proof - + from prems have "0 = max (degree [:a:]) (degree (q * pcompose p q))" + by simp + also have "\ \ degree ([:a:] + q * pcompose p q)" + by (rule degree_add_le_max) + finally show ?thesis + by (auto simp add: pcompose_pCons) + qed ultimately show ?thesis by simp qed - moreover have "degree (q * pcompose p q)>0 \ ?case" - proof - - assume asm:"0 < degree (q * pcompose p q)" - hence "p\0" "q\0" "pcompose p q\0" by auto - have "degree (pcompose (pCons a p) q) = degree ( q * pcompose p q)" - unfolding pcompose_pCons - using degree_add_eq_right[of "[:a:]" ] asm by auto - thus ?thesis - using pCons.hyps(2) degree_mult_eq[OF \q\0\ \pcompose p q\0\] by auto - qed - ultimately show ?case by blast + next + case prems: 2 + then have "p \ 0" "q \ 0" "pcompose p q \ 0" + by auto + from prems degree_add_eq_right [of "[:a:]"] + have "degree (pcompose (pCons a p) q) = degree (q * pcompose p q)" + by (auto simp: pcompose_pCons) + with pCons.hyps(2) degree_mult_eq[OF \q\0\ \pcompose p q\0\] show ?thesis + by auto + qed qed lemma pcompose_eq_0: - fixes p q:: "'a :: {comm_semiring_0,semiring_no_zero_divisors} poly" - assumes "pcompose p q = 0" "degree q > 0" + fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" + assumes "pcompose p q = 0" "degree q > 0" shows "p = 0" proof - - have "degree p=0" using assms degree_pcompose[of p q] by auto - then obtain a where "p=[:a:]" + from assms degree_pcompose [of p q] have "degree p = 0" + by auto + then obtain a where "p = [:a:]" by (metis degree_pCons_eq_if gr0_conv_Suc neq0_conv pCons_cases) - hence "a=0" using assms(1) by auto - thus ?thesis using \p=[:a:]\ by simp + with assms(1) have "a = 0" + by auto + with \p = [:a:]\ show ?thesis + by simp qed lemma lead_coeff_comp: - fixes p q:: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" - assumes "degree q > 0" + fixes p q :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" + assumes "degree q > 0" shows "lead_coeff (pcompose p q) = lead_coeff p * lead_coeff q ^ (degree p)" proof (induct p) case 0 - thus ?case by auto + then show ?case by auto next case (pCons a p) - have "degree ( q * pcompose p q) = 0 \ ?case" - proof - - assume "degree ( q * pcompose p q) = 0" - hence "pcompose p q = 0" by (metis assms degree_0 degree_mult_eq_0 neq0_conv) - hence "p=0" using pcompose_eq_0[OF _ \degree q > 0\] by simp - thus ?thesis by auto - qed - moreover have "degree ( q * pcompose p q) > 0 \ ?case" - proof - - assume "degree (q * pcompose p q) > 0" - then have "degree [:a:] < degree (q * pcompose p q)" - by simp - then have "lead_coeff ([:a:] + q * p \\<^sub>p q) = lead_coeff (q * p \\<^sub>p q)" - by (rule lead_coeff_add_le) - then have "lead_coeff (pcompose (pCons a p) q) = lead_coeff (q * pcompose p q)" - by (simp add: pcompose_pCons) - also have "... = lead_coeff q * (lead_coeff p * lead_coeff q ^ degree p)" - using pCons.hyps(2) lead_coeff_mult[of q "pcompose p q"] by simp - also have "... = lead_coeff p * lead_coeff q ^ (degree p + 1)" - by (auto simp: mult_ac) - finally show ?thesis by auto - qed - ultimately show ?case by blast + consider "degree (q * pcompose p q) = 0" | "degree (q * pcompose p q) > 0" + by blast + then show ?case + proof cases + case prems: 1 + then have "pcompose p q = 0" + by (metis assms degree_0 degree_mult_eq_0 neq0_conv) + with pcompose_eq_0[OF _ \degree q > 0\] have "p = 0" + by simp + then show ?thesis + by auto + next + case prems: 2 + then have "degree [:a:] < degree (q * pcompose p q)" + by simp + then have "lead_coeff ([:a:] + q * p \\<^sub>p q) = lead_coeff (q * p \\<^sub>p q)" + by (rule lead_coeff_add_le) + then have "lead_coeff (pcompose (pCons a p) q) = lead_coeff (q * pcompose p q)" + by (simp add: pcompose_pCons) + also have "\ = lead_coeff q * (lead_coeff p * lead_coeff q ^ degree p)" + using pCons.hyps(2) lead_coeff_mult[of q "pcompose p q"] by simp + also have "\ = lead_coeff p * lead_coeff q ^ (degree p + 1)" + by (auto simp: mult_ac) + finally show ?thesis by auto + qed qed subsection \Shifting polynomials\ -definition poly_shift :: "nat \ ('a::zero) poly \ 'a poly" where - "poly_shift n p = Abs_poly (\i. coeff p (i + n))" +definition poly_shift :: "nat \ 'a::zero poly \ 'a poly" + where "poly_shift n p = Abs_poly (\i. coeff p (i + n))" lemma nth_default_drop: "nth_default x (drop n xs) m = nth_default x xs (m + n)" by (auto simp add: nth_default_def add_ac) - + lemma nth_default_take: "nth_default x (take n xs) m = (if m < n then nth_default x xs m else x)" by (auto simp add: nth_default_def add_ac) - + lemma coeff_poly_shift: "coeff (poly_shift n p) i = coeff p (i + n)" proof - - from MOST_coeff_eq_0[of p] obtain m where "\k>m. coeff p k = 0" by (auto simp: MOST_nat) - hence "\k>m. coeff p (k + n) = 0" by auto - hence "\\<^sub>\k. coeff p (k + n) = 0" by (auto simp: MOST_nat) - thus ?thesis by (simp add: poly_shift_def poly.Abs_poly_inverse) + from MOST_coeff_eq_0[of p] obtain m where "\k>m. coeff p k = 0" + by (auto simp: MOST_nat) + then have "\k>m. coeff p (k + n) = 0" + by auto + then have "\\<^sub>\k. coeff p (k + n) = 0" + by (auto simp: MOST_nat) + then show ?thesis + by (simp add: poly_shift_def poly.Abs_poly_inverse) qed lemma poly_shift_id [simp]: "poly_shift 0 = (\x. x)" @@ -2180,7 +2139,7 @@ lemma poly_shift_0 [simp]: "poly_shift n 0 = 0" by (simp add: poly_eq_iff coeff_poly_shift) - + lemma poly_shift_1: "poly_shift n 1 = (if n = 0 then 1 else 0)" by (simp add: poly_eq_iff coeff_poly_shift) @@ -2189,17 +2148,20 @@ lemma coeffs_shift_poly [code abstract]: "coeffs (poly_shift n p) = drop n (coeffs p)" proof (cases "p = 0") + case True + then show ?thesis by simp +next case False - thus ?thesis + then show ?thesis by (intro coeffs_eqI) - (simp_all add: coeff_poly_shift nth_default_drop last_coeffs_not_0 nth_default_coeffs_eq) -qed simp_all + (simp_all add: coeff_poly_shift nth_default_drop last_coeffs_not_0 nth_default_coeffs_eq) +qed subsection \Truncating polynomials\ -definition poly_cutoff where - "poly_cutoff n p = Abs_poly (\k. if k < n then coeff p k else 0)" +definition poly_cutoff + where "poly_cutoff n p = Abs_poly (\k. if k < n then coeff p k else 0)" lemma coeff_poly_cutoff: "coeff (poly_cutoff n p) k = (if k < n then coeff p k else 0)" unfolding poly_cutoff_def @@ -2211,35 +2173,38 @@ lemma poly_cutoff_1 [simp]: "poly_cutoff n 1 = (if n = 0 then 0 else 1)" by (simp add: poly_eq_iff coeff_poly_cutoff) -lemma coeffs_poly_cutoff [code abstract]: +lemma coeffs_poly_cutoff [code abstract]: "coeffs (poly_cutoff n p) = strip_while (op = 0) (take n (coeffs p))" proof (cases "strip_while (op = 0) (take n (coeffs p)) = []") case True - hence "coeff (poly_cutoff n p) k = 0" for k + then have "coeff (poly_cutoff n p) k = 0" for k unfolding coeff_poly_cutoff by (auto simp: nth_default_coeffs_eq [symmetric] nth_default_def set_conv_nth) - hence "poly_cutoff n p = 0" by (simp add: poly_eq_iff) - thus ?thesis by (subst True) simp_all + then have "poly_cutoff n p = 0" + by (simp add: poly_eq_iff) + then show ?thesis + by (subst True) simp_all next case False - have "no_trailing (op = 0) (strip_while (op = 0) (take n (coeffs p)))" by simp - with False have "last (strip_while (op = 0) (take n (coeffs p))) \ 0" + have "no_trailing (op = 0) (strip_while (op = 0) (take n (coeffs p)))" + by simp + with False have "last (strip_while (op = 0) (take n (coeffs p))) \ 0" unfolding no_trailing_unfold by auto - thus ?thesis + then show ?thesis by (intro coeffs_eqI) - (simp_all add: coeff_poly_cutoff last_coeffs_not_0 nth_default_take nth_default_coeffs_eq) + (simp_all add: coeff_poly_cutoff last_coeffs_not_0 nth_default_take nth_default_coeffs_eq) qed subsection \Reflecting polynomials\ -definition reflect_poly where - "reflect_poly p = Poly (rev (coeffs p))" - +definition reflect_poly :: "'a::zero poly \ 'a poly" + where "reflect_poly p = Poly (rev (coeffs p))" + lemma coeffs_reflect_poly [code abstract]: - "coeffs (reflect_poly p) = rev (dropWhile (op = 0) (coeffs p))" - unfolding reflect_poly_def by simp - + "coeffs (reflect_poly p) = rev (dropWhile (op = 0) (coeffs p))" + by (simp add: reflect_poly_def) + lemma reflect_poly_0 [simp]: "reflect_poly 0 = 0" by (simp add: reflect_poly_def) @@ -2248,9 +2213,10 @@ lemma coeff_reflect_poly: "coeff (reflect_poly p) n = (if n > degree p then 0 else coeff p (degree p - n))" - by (cases "p = 0") (auto simp add: reflect_poly_def nth_default_def - rev_nth degree_eq_length_coeffs coeffs_nth not_less - dest: le_imp_less_Suc) + by (cases "p = 0") + (auto simp add: reflect_poly_def nth_default_def + rev_nth degree_eq_length_coeffs coeffs_nth not_less + dest: le_imp_less_Suc) lemma coeff_0_reflect_poly_0_iff [simp]: "coeff (reflect_poly p) 0 = 0 \ p = 0" by (simp add: coeff_reflect_poly) @@ -2261,14 +2227,15 @@ lemma reflect_poly_pCons': "p \ 0 \ reflect_poly (pCons c p) = reflect_poly p + monom c (Suc (degree p))" by (intro poly_eqI) - (auto simp: coeff_reflect_poly coeff_pCons not_less Suc_diff_le split: nat.split) + (auto simp: coeff_reflect_poly coeff_pCons not_less Suc_diff_le split: nat.split) lemma reflect_poly_const [simp]: "reflect_poly [:a:] = [:a:]" by (cases "a = 0") (simp_all add: reflect_poly_def) lemma poly_reflect_poly_nz: - "(x :: 'a :: field) \ 0 \ poly (reflect_poly p) x = x ^ degree p * poly p (inverse x)" - by (induction rule: pCons_induct) (simp_all add: field_simps reflect_poly_pCons' poly_monom) + "x \ 0 \ poly (reflect_poly p) x = x ^ degree p * poly p (inverse x)" + for x :: "'a::field" + by (induct rule: pCons_induct) (simp_all add: field_simps reflect_poly_pCons' poly_monom) lemma coeff_0_reflect_poly [simp]: "coeff (reflect_poly p) 0 = lead_coeff p" by (simp add: coeff_reflect_poly) @@ -2282,24 +2249,21 @@ lemma degree_reflect_poly_le: "degree (reflect_poly p) \ degree p" by (simp add: degree_eq_length_coeffs coeffs_reflect_poly length_dropWhile_le diff_le_mono) -lemma reflect_poly_pCons: - "a \ 0 \ reflect_poly (pCons a p) = Poly (rev (a # coeffs p))" +lemma reflect_poly_pCons: "a \ 0 \ reflect_poly (pCons a p) = Poly (rev (a # coeffs p))" by (subst coeffs_eq_iff) (simp add: coeffs_reflect_poly) - + lemma degree_reflect_poly_eq [simp]: "coeff p 0 \ 0 \ degree (reflect_poly p) = degree p" by (cases p rule: pCons_cases) (simp add: reflect_poly_pCons degree_eq_length_coeffs) - + (* TODO: does this work with zero divisors as well? Probably not. *) -lemma reflect_poly_mult: - "reflect_poly (p * q) = - reflect_poly p * reflect_poly (q :: _ :: {comm_semiring_0,semiring_no_zero_divisors} poly)" +lemma reflect_poly_mult: "reflect_poly (p * q) = reflect_poly p * reflect_poly q" + for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" proof (cases "p = 0 \ q = 0") case False - hence [simp]: "p \ 0" "q \ 0" by auto + then have [simp]: "p \ 0" "q \ 0" by auto show ?thesis proof (rule poly_eqI) - fix i :: nat - show "coeff (reflect_poly (p * q)) i = coeff (reflect_poly p * reflect_poly q) i" + show "coeff (reflect_poly (p * q)) i = coeff (reflect_poly p * reflect_poly q) i" for i proof (cases "i \ degree (p * q)") case True define A where "A = {..i} \ {i - degree q..degree p}" @@ -2309,47 +2273,45 @@ from True have "coeff (reflect_poly (p * q)) i = coeff (p * q) (degree (p * q) - i)" by (simp add: coeff_reflect_poly) also have "\ = (\j\degree (p * q) - i. coeff p j * coeff q (degree (p * q) - i - j))" - unfolding coeff_mult by simp + by (simp add: coeff_mult) also have "\ = (\j\B. coeff p j * coeff q (degree (p * q) - i - j))" by (intro sum.mono_neutral_right) (auto simp: B_def degree_mult_eq not_le coeff_eq_0) also from True have "\ = (\j\A. coeff p (degree p - j) * coeff q (degree q - (i - j)))" by (intro sum.reindex_bij_witness[of _ ?f ?f]) - (auto simp: A_def B_def degree_mult_eq add_ac) - also have "\ = (\j\i. if j \ {i - degree q..degree p} then - coeff p (degree p - j) * coeff q (degree q - (i - j)) else 0)" + (auto simp: A_def B_def degree_mult_eq add_ac) + also have "\ = + (\j\i. + if j \ {i - degree q..degree p} + then coeff p (degree p - j) * coeff q (degree q - (i - j)) + else 0)" by (subst sum.inter_restrict [symmetric]) (simp_all add: A_def) - also have "\ = coeff (reflect_poly p * reflect_poly q) i" - by (fastforce simp: coeff_mult coeff_reflect_poly intro!: sum.cong) - finally show ?thesis . + also have "\ = coeff (reflect_poly p * reflect_poly q) i" + by (fastforce simp: coeff_mult coeff_reflect_poly intro!: sum.cong) + finally show ?thesis . qed (auto simp: coeff_mult coeff_reflect_poly coeff_eq_0 degree_mult_eq intro!: sum.neutral) qed qed auto -lemma reflect_poly_smult: - "reflect_poly (Polynomial.smult (c::'a::{comm_semiring_0,semiring_no_zero_divisors}) p) = - Polynomial.smult c (reflect_poly p)" +lemma reflect_poly_smult: "reflect_poly (smult c p) = smult c (reflect_poly p)" + for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" using reflect_poly_mult[of "[:c:]" p] by simp -lemma reflect_poly_power: - "reflect_poly (p ^ n :: 'a :: {comm_semiring_1,semiring_no_zero_divisors} poly) = - reflect_poly p ^ n" - by (induction n) (simp_all add: reflect_poly_mult) - -lemma reflect_poly_prod: - "reflect_poly (prod (f :: _ \ _ :: {comm_semiring_0,semiring_no_zero_divisors} poly) A) = - prod (\x. reflect_poly (f x)) A" - by (cases "finite A", induction rule: finite_induct) (simp_all add: reflect_poly_mult) - -lemma reflect_poly_prod_list: - "reflect_poly (prod_list (xs :: _ :: {comm_semiring_0,semiring_no_zero_divisors} poly list)) = - prod_list (map reflect_poly xs)" - by (induction xs) (simp_all add: reflect_poly_mult) - -lemma reflect_poly_Poly_nz: - "xs \ [] \ last xs \ 0 \ reflect_poly (Poly xs) = Poly (rev xs)" - unfolding reflect_poly_def coeffs_Poly by simp - -lemmas reflect_poly_simps = +lemma reflect_poly_power: "reflect_poly (p ^ n) = reflect_poly p ^ n" + for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" + by (induct n) (simp_all add: reflect_poly_mult) + +lemma reflect_poly_prod: "reflect_poly (prod f A) = prod (\x. reflect_poly (f x)) A" + for f :: "_ \ _::{comm_semiring_0,semiring_no_zero_divisors} poly" + by (induct A rule: infinite_finite_induct) (simp_all add: reflect_poly_mult) + +lemma reflect_poly_prod_list: "reflect_poly (prod_list xs) = prod_list (map reflect_poly xs)" + for xs :: "_::{comm_semiring_0,semiring_no_zero_divisors} poly list" + by (induct xs) (simp_all add: reflect_poly_mult) + +lemma reflect_poly_Poly_nz: "xs \ [] \ last xs \ 0 \ reflect_poly (Poly xs) = Poly (rev xs)" + by (simp add: reflect_poly_def) + +lemmas reflect_poly_simps = reflect_poly_0 reflect_poly_1 reflect_poly_const reflect_poly_smult reflect_poly_mult reflect_poly_power reflect_poly_prod reflect_poly_prod_list @@ -2357,8 +2319,7 @@ subsection \Derivatives\ function pderiv :: "('a :: {comm_semiring_1,semiring_no_zero_divisors}) poly \ 'a poly" -where - "pderiv (pCons a p) = (if p = 0 then 0 else p + pCons 0 (pderiv p))" + where "pderiv (pCons a p) = (if p = 0 then 0 else p + pCons 0 (pderiv p))" by (auto intro: pCons_cases) termination pderiv @@ -2366,253 +2327,252 @@ declare pderiv.simps[simp del] -lemma pderiv_0 [simp]: - "pderiv 0 = 0" +lemma pderiv_0 [simp]: "pderiv 0 = 0" using pderiv.simps [of 0 0] by simp -lemma pderiv_pCons: - "pderiv (pCons a p) = p + pCons 0 (pderiv p)" +lemma pderiv_pCons: "pderiv (pCons a p) = p + pCons 0 (pderiv p)" by (simp add: pderiv.simps) -lemma pderiv_1 [simp]: "pderiv 1 = 0" - unfolding one_poly_def by (simp add: pderiv_pCons) - -lemma pderiv_of_nat [simp]: "pderiv (of_nat n) = 0" +lemma pderiv_1 [simp]: "pderiv 1 = 0" + by (simp add: one_poly_def pderiv_pCons) + +lemma pderiv_of_nat [simp]: "pderiv (of_nat n) = 0" and pderiv_numeral [simp]: "pderiv (numeral m) = 0" by (simp_all add: of_nat_poly numeral_poly pderiv_pCons) lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)" - by (induct p arbitrary: n) - (auto simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split) - -fun pderiv_coeffs_code - :: "('a :: {comm_semiring_1,semiring_no_zero_divisors}) \ 'a list \ 'a list" where - "pderiv_coeffs_code f (x # xs) = cCons (f * x) (pderiv_coeffs_code (f+1) xs)" -| "pderiv_coeffs_code f [] = []" - -definition pderiv_coeffs :: - "'a :: {comm_semiring_1,semiring_no_zero_divisors} list \ 'a list" where - "pderiv_coeffs xs = pderiv_coeffs_code 1 (tl xs)" + by (induct p arbitrary: n) + (auto simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split) + +fun pderiv_coeffs_code :: "'a::{comm_semiring_1,semiring_no_zero_divisors} \ 'a list \ 'a list" + where + "pderiv_coeffs_code f (x # xs) = cCons (f * x) (pderiv_coeffs_code (f+1) xs)" + | "pderiv_coeffs_code f [] = []" + +definition pderiv_coeffs :: "'a::{comm_semiring_1,semiring_no_zero_divisors} list \ 'a list" + where "pderiv_coeffs xs = pderiv_coeffs_code 1 (tl xs)" (* Efficient code for pderiv contributed by René Thiemann and Akihisa Yamada *) -lemma pderiv_coeffs_code: - "nth_default 0 (pderiv_coeffs_code f xs) n = (f + of_nat n) * (nth_default 0 xs n)" +lemma pderiv_coeffs_code: + "nth_default 0 (pderiv_coeffs_code f xs) n = (f + of_nat n) * nth_default 0 xs n" proof (induct xs arbitrary: f n) - case (Cons x xs f n) - show ?case + case Nil + then show ?case by simp +next + case (Cons x xs) + show ?case proof (cases n) case 0 - thus ?thesis by (cases "pderiv_coeffs_code (f + 1) xs = [] \ f * x = 0", auto simp: cCons_def) + then show ?thesis + by (cases "pderiv_coeffs_code (f + 1) xs = [] \ f * x = 0") (auto simp: cCons_def) next - case (Suc m) note n = this - show ?thesis + case n: (Suc m) + show ?thesis proof (cases "pderiv_coeffs_code (f + 1) xs = [] \ f * x = 0") case False - hence "nth_default 0 (pderiv_coeffs_code f (x # xs)) n = - nth_default 0 (pderiv_coeffs_code (f + 1) xs) m" + then have "nth_default 0 (pderiv_coeffs_code f (x # xs)) n = + nth_default 0 (pderiv_coeffs_code (f + 1) xs) m" by (auto simp: cCons_def n) - also have "\ = (f + of_nat n) * (nth_default 0 xs m)" - unfolding Cons by (simp add: n add_ac) - finally show ?thesis by (simp add: n) + also have "\ = (f + of_nat n) * nth_default 0 xs m" + by (simp add: Cons n add_ac) + finally show ?thesis + by (simp add: n) next case True - { - fix g - have "pderiv_coeffs_code g xs = [] \ g + of_nat m = 0 \ nth_default 0 xs m = 0" - proof (induct xs arbitrary: g m) - case (Cons x xs g) - from Cons(2) have empty: "pderiv_coeffs_code (g + 1) xs = []" - and g: "(g = 0 \ x = 0)" - by (auto simp: cCons_def split: if_splits) - note IH = Cons(1)[OF empty] - from IH[of m] IH[of "m - 1"] g - show ?case by (cases m, auto simp: field_simps) - qed simp - } note empty = this + have empty: "pderiv_coeffs_code g xs = [] \ g + of_nat m = 0 \ nth_default 0 xs m = 0" for g + proof (induct xs arbitrary: g m) + case Nil + then show ?case by simp + next + case (Cons x xs) + from Cons(2) have empty: "pderiv_coeffs_code (g + 1) xs = []" and g: "g = 0 \ x = 0" + by (auto simp: cCons_def split: if_splits) + note IH = Cons(1)[OF empty] + from IH[of m] IH[of "m - 1"] g show ?case + by (cases m) (auto simp: field_simps) + qed from True have "nth_default 0 (pderiv_coeffs_code f (x # xs)) n = 0" by (auto simp: cCons_def n) - moreover have "(f + of_nat n) * nth_default 0 (x # xs) n = 0" using True - by (simp add: n, insert empty[of "f+1"], auto simp: field_simps) + moreover from True have "(f + of_nat n) * nth_default 0 (x # xs) n = 0" + by (simp add: n) (use empty[of "f+1"] in \auto simp: field_simps\) ultimately show ?thesis by simp qed qed -qed simp - -lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\ i. f (Suc i)) [0 ..< n]" - by (induct n arbitrary: f, auto) - -lemma coeffs_pderiv_code [code abstract]: - "coeffs (pderiv p) = pderiv_coeffs (coeffs p)" unfolding pderiv_coeffs_def +qed + +lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\i. f (Suc i)) [0 ..< n]" + by (induct n arbitrary: f) auto + +lemma coeffs_pderiv_code [code abstract]: "coeffs (pderiv p) = pderiv_coeffs (coeffs p)" + unfolding pderiv_coeffs_def proof (rule coeffs_eqI, unfold pderiv_coeffs_code coeff_pderiv, goal_cases) case (1 n) have id: "coeff p (Suc n) = nth_default 0 (map (\i. coeff p (Suc i)) [0.. degree p = 0" +lemma pderiv_eq_0_iff: "pderiv p = 0 \ degree p = 0" + for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly" apply (rule iffI) - apply (cases p, simp) - apply (simp add: poly_eq_iff coeff_pderiv del: of_nat_Suc) + apply (cases p) + apply simp + apply (simp add: poly_eq_iff coeff_pderiv del: of_nat_Suc) apply (simp add: poly_eq_iff coeff_pderiv coeff_eq_0) done -lemma degree_pderiv: "degree (pderiv (p :: 'a poly)) = degree p - 1" +lemma degree_pderiv: "degree (pderiv p) = degree p - 1" + for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly" apply (rule order_antisym [OF degree_le]) - apply (simp add: coeff_pderiv coeff_eq_0) - apply (cases "degree p", simp) + apply (simp add: coeff_pderiv coeff_eq_0) + apply (cases "degree p") + apply simp apply (rule le_degree) apply (simp add: coeff_pderiv del: of_nat_Suc) apply (metis degree_0 leading_coeff_0_iff nat.distinct(1)) done -lemma not_dvd_pderiv: - assumes "degree (p :: 'a poly) \ 0" +lemma not_dvd_pderiv: + fixes p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly" + assumes "degree p \ 0" shows "\ p dvd pderiv p" proof assume dvd: "p dvd pderiv p" - then obtain q where p: "pderiv p = p * q" unfolding dvd_def by auto + then obtain q where p: "pderiv p = p * q" + unfolding dvd_def by auto from dvd have le: "degree p \ degree (pderiv p)" by (simp add: assms dvd_imp_degree_le pderiv_eq_0_iff) - from this[unfolded degree_pderiv] assms show False by auto + from assms and this [unfolded degree_pderiv] + show False by auto qed -lemma dvd_pderiv_iff [simp]: "(p :: 'a poly) dvd pderiv p \ degree p = 0" +lemma dvd_pderiv_iff [simp]: "p dvd pderiv p \ degree p = 0" + for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly" using not_dvd_pderiv[of p] by (auto simp: pderiv_eq_0_iff [symmetric]) -end - lemma pderiv_singleton [simp]: "pderiv [:a:] = 0" -by (simp add: pderiv_pCons) + by (simp add: pderiv_pCons) lemma pderiv_add: "pderiv (p + q) = pderiv p + pderiv q" -by (rule poly_eqI, simp add: coeff_pderiv algebra_simps) + by (rule poly_eqI) (simp add: coeff_pderiv algebra_simps) lemma pderiv_minus: "pderiv (- p :: 'a :: idom poly) = - pderiv p" -by (rule poly_eqI, simp add: coeff_pderiv algebra_simps) + by (rule poly_eqI) (simp add: coeff_pderiv algebra_simps) lemma pderiv_diff: "pderiv ((p :: _ :: idom poly) - q) = pderiv p - pderiv q" -by (rule poly_eqI, simp add: coeff_pderiv algebra_simps) + by (rule poly_eqI) (simp add: coeff_pderiv algebra_simps) lemma pderiv_smult: "pderiv (smult a p) = smult a (pderiv p)" -by (rule poly_eqI, simp add: coeff_pderiv algebra_simps) + by (rule poly_eqI) (simp add: coeff_pderiv algebra_simps) lemma pderiv_mult: "pderiv (p * q) = p * pderiv q + q * pderiv p" -by (induct p) (auto simp: pderiv_add pderiv_smult pderiv_pCons algebra_simps) - -lemma pderiv_power_Suc: - "pderiv (p ^ Suc n) = smult (of_nat (Suc n)) (p ^ n) * pderiv p" -apply (induct n) -apply simp -apply (subst power_Suc) -apply (subst pderiv_mult) -apply (erule ssubst) -apply (simp only: of_nat_Suc smult_add_left smult_1_left) -apply (simp add: algebra_simps) -done - -lemma pderiv_prod: "pderiv (prod f (as)) = - (\a \ as. prod f (as - {a}) * pderiv (f a))" + by (induct p) (auto simp: pderiv_add pderiv_smult pderiv_pCons algebra_simps) + +lemma pderiv_power_Suc: "pderiv (p ^ Suc n) = smult (of_nat (Suc n)) (p ^ n) * pderiv p" + apply (induct n) + apply simp + apply (subst power_Suc) + apply (subst pderiv_mult) + apply (erule ssubst) + apply (simp only: of_nat_Suc smult_add_left smult_1_left) + apply (simp add: algebra_simps) + done + +lemma pderiv_prod: "pderiv (prod f (as)) = (\a\as. prod f (as - {a}) * pderiv (f a))" proof (induct as rule: infinite_finite_induct) case (insert a as) - hence id: "prod f (insert a as) = f a * prod f as" - "\ g. sum g (insert a as) = g a + sum g as" + then have id: "prod f (insert a as) = f a * prod f as" + "\g. sum g (insert a as) = g a + sum g as" "insert a as - {a} = as" by auto - { - fix b - assume "b \ as" - hence id2: "insert a as - {b} = insert a (as - {b})" using \a \ as\ by auto - have "prod f (insert a as - {b}) = f a * prod f (as - {b})" - unfolding id2 - by (subst prod.insert, insert insert, auto) - } note id2 = this - show ?case + have "prod f (insert a as - {b}) = f a * prod f (as - {b})" if "b \ as" for b + proof - + from \a \ as\ that have *: "insert a as - {b} = insert a (as - {b})" + by auto + show ?thesis + unfolding * by (subst prod.insert) (use insert in auto) + qed + then show ?case unfolding id pderiv_mult insert(3) sum_distrib_left - by (auto simp add: ac_simps id2 intro!: sum.cong) + by (auto simp add: ac_simps intro!: sum.cong) qed auto -lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)" -by (rule DERIV_cong, rule DERIV_pow, simp) +lemma DERIV_pow2: "DERIV (\x. x ^ Suc n) x :> real (Suc n) * (x ^ n)" + by (rule DERIV_cong, rule DERIV_pow) simp declare DERIV_pow2 [simp] DERIV_pow [simp] -lemma DERIV_add_const: "DERIV f x :> D ==> DERIV (%x. a + f x :: 'a::real_normed_field) x :> D" -by (rule DERIV_cong, rule DERIV_add, auto) - -lemma poly_DERIV [simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x" - by (induct p, auto intro!: derivative_eq_intros simp add: pderiv_pCons) - -lemma continuous_on_poly [continuous_intros]: +lemma DERIV_add_const: "DERIV f x :> D \ DERIV (\x. a + f x :: 'a::real_normed_field) x :> D" + by (rule DERIV_cong, rule DERIV_add) auto + +lemma poly_DERIV [simp]: "DERIV (\x. poly p x) x :> poly (pderiv p) x" + by (induct p) (auto intro!: derivative_eq_intros simp add: pderiv_pCons) + +lemma continuous_on_poly [continuous_intros]: fixes p :: "'a :: {real_normed_field} poly" assumes "continuous_on A f" - shows "continuous_on A (\x. poly p (f x))" + shows "continuous_on A (\x. poly p (f x))" proof - - have "continuous_on A (\x. (\i\degree p. (f x) ^ i * coeff p i))" + have "continuous_on A (\x. (\i\degree p. (f x) ^ i * coeff p i))" by (intro continuous_intros assms) - also have "\ = (\x. poly p (f x))" by (intro ext) (simp add: poly_altdef mult_ac) + also have "\ = (\x. poly p (f x))" + by (rule ext) (simp add: poly_altdef mult_ac) finally show ?thesis . qed -text\Consequences of the derivative theorem above\ - -lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (at x::real filter)" -apply (simp add: real_differentiable_def) -apply (blast intro: poly_DERIV) -done - -lemma poly_isCont[simp]: "isCont (%x. poly p x) (x::real)" -by (rule poly_DERIV [THEN DERIV_isCont]) - -lemma poly_IVT_pos: "[| a < b; poly p (a::real) < 0; 0 < poly p b |] - ==> \x. a < x & x < b & (poly p x = 0)" -using IVT_objl [of "poly p" a 0 b] -by (auto simp add: order_le_less) - -lemma poly_IVT_neg: "[| (a::real) < b; 0 < poly p a; poly p b < 0 |] - ==> \x. a < x & x < b & (poly p x = 0)" -by (insert poly_IVT_pos [where p = "- p" ]) simp - -lemma poly_IVT: - fixes p::"real poly" - assumes "ax>a. x < b \ poly p x = 0" -by (metis assms(1) assms(2) less_not_sym mult_less_0_iff poly_IVT_neg poly_IVT_pos) - -lemma poly_MVT: "(a::real) < b ==> - \x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)" -using MVT [of a b "poly p"] -apply auto -apply (rule_tac x = z in exI) -apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique]) -done +text \Consequences of the derivative theorem above.\ + +lemma poly_differentiable[simp]: "(\x. poly p x) differentiable (at x)" + for x :: real + by (simp add: real_differentiable_def) (blast intro: poly_DERIV) + +lemma poly_isCont[simp]: "isCont (\x. poly p x) x" + for x :: real + by (rule poly_DERIV [THEN DERIV_isCont]) + +lemma poly_IVT_pos: "a < b \ poly p a < 0 \ 0 < poly p b \ \x. a < x \ x < b \ poly p x = 0" + for a b :: real + using IVT_objl [of "poly p" a 0 b] by (auto simp add: order_le_less) + +lemma poly_IVT_neg: "a < b \ 0 < poly p a \ poly p b < 0 \ \x. a < x \ x < b \ poly p x = 0" + for a b :: real + using poly_IVT_pos [where p = "- p"] by simp + +lemma poly_IVT: "a < b \ poly p a * poly p b < 0 \ \x>a. x < b \ poly p x = 0" + for p :: "real poly" + by (metis less_not_sym mult_less_0_iff poly_IVT_neg poly_IVT_pos) + +lemma poly_MVT: "a < b \ \x. a < x \ x < b \ poly p b - poly p a = (b - a) * poly (pderiv p) x" + for a b :: real + using MVT [of a b "poly p"] + apply auto + apply (rule_tac x = z in exI) + apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique]) + done lemma poly_MVT': + fixes a b :: real assumes "{min a b..max a b} \ A" - shows "\x\A. poly p b - poly p a = (b - a) * poly (pderiv p) (x::real)" + shows "\x\A. poly p b - poly p a = (b - a) * poly (pderiv p) x" proof (cases a b rule: linorder_cases) case less from poly_MVT[OF less, of p] guess x by (elim exE conjE) - thus ?thesis by (intro bexI[of _ x]) (auto intro!: subsetD[OF assms]) - + then show ?thesis by (intro bexI[of _ x]) (auto intro!: subsetD[OF assms]) next case greater from poly_MVT[OF greater, of p] guess x by (elim exE conjE) - thus ?thesis by (intro bexI[of _ x]) (auto simp: algebra_simps intro!: subsetD[OF assms]) -qed (insert assms, auto) + then show ?thesis by (intro bexI[of _ x]) (auto simp: algebra_simps intro!: subsetD[OF assms]) +qed (use assms in auto) lemma poly_pinfty_gt_lc: fixes p :: "real poly" - assumes "lead_coeff p > 0" + assumes "lead_coeff p > 0" shows "\ n. \ x \ n. poly p x \ lead_coeff p" using assms proof (induct p) @@ -2637,7 +2597,7 @@ by (auto simp: n_def) with gt_0 have "\a\ / lead_coeff p \ \a\ / poly p x" and "poly p x > 0" by (auto intro: frac_le) - with \n\x\[unfolded n_def] have "x \ 1 + \a\ / poly p x" + with \n \ x\[unfolded n_def] have "x \ 1 + \a\ / poly p x" by auto with \lead_coeff p \ poly p x\ \poly p x > 0\ \p \ 0\ show "lead_coeff (pCons a p) \ poly (pCons a p) x" @@ -2650,88 +2610,87 @@ lemma lemma_order_pderiv1: "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q + smult (of_nat (Suc n)) (q * [:- a, 1:] ^ n)" -apply (simp only: pderiv_mult pderiv_power_Suc) -apply (simp del: power_Suc of_nat_Suc add: pderiv_pCons) -done + by (simp only: pderiv_mult pderiv_power_Suc) (simp del: power_Suc of_nat_Suc add: pderiv_pCons) lemma lemma_order_pderiv: fixes p :: "'a :: field_char_0 poly" - assumes n: "0 < n" - and pd: "pderiv p \ 0" - and pe: "p = [:- a, 1:] ^ n * q" - and nd: "~ [:- a, 1:] dvd q" - shows "n = Suc (order a (pderiv p))" -using n + assumes n: "0 < n" + and pd: "pderiv p \ 0" + and pe: "p = [:- a, 1:] ^ n * q" + and nd: "\ [:- a, 1:] dvd q" + shows "n = Suc (order a (pderiv p))" proof - - have "pderiv ([:- a, 1:] ^ n * q) \ 0" - using assms by auto - obtain n' where "n = Suc n'" "0 < Suc n'" "pderiv ([:- a, 1:] ^ Suc n' * q) \ 0" - using assms by (cases n) auto - have *: "!!k l. k dvd k * pderiv q + smult (of_nat (Suc n')) l \ k dvd l" + from assms have "pderiv ([:- a, 1:] ^ n * q) \ 0" + by auto + from assms obtain n' where "n = Suc n'" "0 < Suc n'" "pderiv ([:- a, 1:] ^ Suc n' * q) \ 0" + by (cases n) auto + have *: "k dvd k * pderiv q + smult (of_nat (Suc n')) l \ k dvd l" for k l by (auto simp del: of_nat_Suc simp: dvd_add_right_iff dvd_smult_iff) - have "n' = order a (pderiv ([:- a, 1:] ^ Suc n' * q))" + have "n' = order a (pderiv ([:- a, 1:] ^ Suc n' * q))" proof (rule order_unique_lemma) show "[:- a, 1:] ^ n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)" apply (subst lemma_order_pderiv1) apply (rule dvd_add) - apply (metis dvdI dvd_mult2 power_Suc2) + apply (metis dvdI dvd_mult2 power_Suc2) apply (metis dvd_smult dvd_triv_right) done - next show "\ [:- a, 1:] ^ Suc n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)" - apply (subst lemma_order_pderiv1) - by (metis * nd dvd_mult_cancel_right power_not_zero pCons_eq_0_iff power_Suc zero_neq_one) + apply (subst lemma_order_pderiv1) + apply (metis * nd dvd_mult_cancel_right power_not_zero pCons_eq_0_iff power_Suc zero_neq_one) + done qed then show ?thesis by (metis \n = Suc n'\ pe) qed -lemma order_pderiv: - "\pderiv p \ 0; order a (p :: 'a :: field_char_0 poly) \ 0\ \ - (order a p = Suc (order a (pderiv p)))" -apply (case_tac "p = 0", simp) -apply (drule_tac a = a and p = p in order_decomp) -using neq0_conv -apply (blast intro: lemma_order_pderiv) -done +lemma order_pderiv: "pderiv p \ 0 \ order a p \ 0 \ order a p = Suc (order a (pderiv p))" + for p :: "'a::field_char_0 poly" + apply (cases "p = 0") + apply simp + apply (drule_tac a = a and p = p in order_decomp) + using neq0_conv + apply (blast intro: lemma_order_pderiv) + done lemma poly_squarefree_decomp_order: - assumes "pderiv (p :: 'a :: field_char_0 poly) \ 0" - and p: "p = q * d" - and p': "pderiv p = e * d" - and d: "d = r * p + s * pderiv p" + fixes p :: "'a::field_char_0 poly" + assumes "pderiv p \ 0" + and p: "p = q * d" + and p': "pderiv p = e * d" + and d: "d = r * p + s * pderiv p" shows "order a q = (if order a p = 0 then 0 else 1)" proof (rule classical) - assume 1: "order a q \ (if order a p = 0 then 0 else 1)" + assume 1: "\ ?thesis" from \pderiv p \ 0\ have "p \ 0" by auto with p have "order a p = order a q + order a d" by (simp add: order_mult) - with 1 have "order a p \ 0" by (auto split: if_splits) - have "order a (pderiv p) = order a e + order a d" - using \pderiv p \ 0\ \pderiv p = e * d\ by (simp add: order_mult) - have "order a p = Suc (order a (pderiv p))" - using \pderiv p \ 0\ \order a p \ 0\ by (rule order_pderiv) - have "d \ 0" using \p \ 0\ \p = q * d\ by simp + with 1 have "order a p \ 0" + by (auto split: if_splits) + from \pderiv p \ 0\ \pderiv p = e * d\ have "order a (pderiv p) = order a e + order a d" + by (simp add: order_mult) + from \pderiv p \ 0\ \order a p \ 0\ have "order a p = Suc (order a (pderiv p))" + by (rule order_pderiv) + from \p \ 0\ \p = q * d\ have "d \ 0" + by simp have "([:-a, 1:] ^ (order a (pderiv p))) dvd d" apply (simp add: d) apply (rule dvd_add) - apply (rule dvd_mult) - apply (simp add: order_divides \p \ 0\ - \order a p = Suc (order a (pderiv p))\) + apply (rule dvd_mult) + apply (simp add: order_divides \p \ 0\ \order a p = Suc (order a (pderiv p))\) apply (rule dvd_mult) apply (simp add: order_divides) done - then have "order a (pderiv p) \ order a d" - using \d \ 0\ by (simp add: order_divides) + with \d \ 0\ have "order a (pderiv p) \ order a d" + by (simp add: order_divides) show ?thesis using \order a p = order a q + order a d\ - using \order a (pderiv p) = order a e + order a d\ - using \order a p = Suc (order a (pderiv p))\ - using \order a (pderiv p) \ order a d\ + and \order a (pderiv p) = order a e + order a d\ + and \order a p = Suc (order a (pderiv p))\ + and \order a (pderiv p) \ order a d\ by auto qed -lemma poly_squarefree_decomp_order2: +lemma poly_squarefree_decomp_order2: "\pderiv p \ (0 :: 'a :: field_char_0 poly); p = q * d; pderiv p = e * d; @@ -2739,7 +2698,7 @@ \ \ \a. order a q = (if order a p = 0 then 0 else 1)" by (blast intro: poly_squarefree_decomp_order) -lemma order_pderiv2: +lemma order_pderiv2: "\pderiv p \ 0; order a (p :: 'a :: field_char_0 poly) \ 0\ \ (order a (pderiv p) = n) = (order a p = Suc n)" by (auto dest: order_pderiv) @@ -2781,11 +2740,11 @@ subsection \Algebraic numbers\ text \ - Algebraic numbers can be defined in two equivalent ways: all real numbers that are - roots of rational polynomials or of integer polynomials. The Algebraic-Numbers AFP entry + Algebraic numbers can be defined in two equivalent ways: all real numbers that are + roots of rational polynomials or of integer polynomials. The Algebraic-Numbers AFP entry uses the rational definition, but we need the integer definition. - The equivalence is obvious since any rational polynomial can be multiplied with the + The equivalence is obvious since any rational polynomial can be multiplied with the LCM of its coefficients, yielding an integer polynomial with the same roots. \ @@ -2796,7 +2755,7 @@ assumes "\i. coeff p i \ \" "p \ 0" "poly p x = 0" shows "algebraic x" using assms unfolding algebraic_def by blast - + lemma algebraicE: assumes "algebraic x" obtains p where "\i. coeff p i \ \" "p \ 0" "poly p x = 0" @@ -2814,7 +2773,7 @@ define cs' where "cs' = map (quotient_of \ f) (coeffs p)" define d where "d = Lcm (set (map snd cs'))" define p' where "p' = smult (of_int d) p" - + have "\n. coeff p' n \ \" proof fix n :: nat @@ -2833,17 +2792,17 @@ by (simp add: of_rat_mult of_rat_divide) also from nz True have "b \ snd ` set cs'" unfolding cs'_def by (force simp: o_def b_def coeffs_def simp del: upt_Suc) - hence "b dvd (a * d)" unfolding d_def by simp - hence "of_int (a * d) / of_int b \ (\ :: rat set)" + then have "b dvd (a * d)" unfolding d_def by simp + then have "of_int (a * d) / of_int b \ (\ :: rat set)" by (rule of_int_divide_in_Ints) - hence "of_rat (of_int (a * d) / of_int b) \ \" by (elim Ints_cases) auto + then have "of_rat (of_int (a * d) / of_int b) \ \" by (elim Ints_cases) auto finally show ?thesis . qed (auto simp: p'_def not_le coeff_eq_0) qed - + moreover have "set (map snd cs') \ {0<..}" - unfolding cs'_def using quotient_of_denom_pos' by (auto simp: coeffs_def simp del: upt_Suc) - hence "d \ 0" unfolding d_def by (induction cs') simp_all + unfolding cs'_def using quotient_of_denom_pos' by (auto simp: coeffs_def simp del: upt_Suc) + then have "d \ 0" unfolding d_def by (induction cs') simp_all with nz have "p' \ 0" by (simp add: p'_def) moreover from root have "poly p' x = 0" by (simp add: p'_def) ultimately show "algebraic x" unfolding algebraic_def by blast @@ -2883,7 +2842,7 @@ also have "\ \ (\a\set (coeffs p). c dvd a)" proof safe fix n :: nat assume "\a\set (coeffs p). c dvd a" - thus "c dvd coeff p n" + then show "c dvd coeff p n" by (cases "n \ degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits) qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits) also have "\ \ c dvd content p" @@ -2893,7 +2852,7 @@ lemma content_dvd [simp]: "[:content p:] dvd p" by (subst const_poly_dvd_iff_dvd_content) simp_all - + lemma content_dvd_coeff [simp]: "content p dvd coeff p n" proof (cases "p = 0") case True @@ -2905,7 +2864,7 @@ by (cases "n \ degree p") (auto simp add: content_def not_le coeff_eq_0 coeff_in_coeffs intro: Gcd_fin_dvd) qed - + lemma content_dvd_coeffs: "c \ set (coeffs p) \ content p dvd c" by (simp add: content_def Gcd_fin_dvd) @@ -2915,8 +2874,8 @@ lemma is_unit_content_iff [simp]: "is_unit (content p) \ content p = 1" proof assume "is_unit (content p)" - hence "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content) - thus "content p = 1" by simp + then have "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content) + then show "content p = 1" by simp qed auto lemma content_smult [simp]: "content (smult c p) = normalize c * content p" @@ -2936,16 +2895,16 @@ shows "smult (content p) (primitive_part p) = p" proof (cases "p = 0") case False - thus ?thesis + then show ?thesis unfolding primitive_part_def - by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs + by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs intro: map_poly_idI) qed simp_all lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \ p = 0" proof (cases "p = 0") case False - hence "primitive_part p = map_poly (\x. x div content p) p" + then have "primitive_part p = map_poly (\x. x div content p) p" by (simp add: primitive_part_def) also from False have "\ = 0 \ p = 0" by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs) @@ -2957,7 +2916,7 @@ shows "content (primitive_part p) = 1" proof - have "p = smult (content p) (primitive_part p)" by simp - also have "content \ = content (primitive_part p) * content p" + also have "content \ = content (primitive_part p) * content p" by (simp del: content_times_primitive_part add: ac_simps) finally have "1 * content p = content (primitive_part p) * content p" by simp @@ -2972,7 +2931,7 @@ obtains p' where "p = smult (content p) p'" "content p' = 1" proof (cases "p = 0") case True - thus ?thesis by (intro that[of 1]) simp_all + then show ?thesis by (intro that[of 1]) simp_all next case False from content_dvd[of p] obtain r where r: "p = [:content p:] * r" by (erule dvdE) @@ -2984,13 +2943,13 @@ lemma content_dvd_contentI [intro]: "p dvd q \ content p dvd content q" using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast - + lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]" by (simp add: primitive_part_def map_poly_pCons) - + lemma primitive_part_prim: "content p = 1 \ primitive_part p = p" by (auto simp: primitive_part_def) - + lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p" proof (cases "p = 0") case False @@ -3004,29 +2963,29 @@ subsection \Division of polynomials\ subsubsection \Division in general\ - + instantiation poly :: (idom_divide) idom_divide begin -fun divide_poly_main :: "'a \ 'a poly \ 'a poly \ 'a poly +fun divide_poly_main :: "'a \ 'a poly \ 'a poly \ 'a poly \ nat \ nat \ 'a poly" where - "divide_poly_main lc q r d dr (Suc n) = (let cr = coeff r dr; a = cr div lc; mon = monom a n in + "divide_poly_main lc q r d dr (Suc n) = (let cr = coeff r dr; a = cr div lc; mon = monom a n in if False \ a * lc = cr then (* False \ is only because of problem in function-package *) - divide_poly_main - lc - (q + mon) - (r - mon * d) + divide_poly_main + lc + (q + mon) + (r - mon * d) d (dr - 1) n else 0)" | "divide_poly_main lc q r d dr 0 = q" definition divide_poly :: "'a poly \ 'a poly \ 'a poly" where "divide_poly f g = (if g = 0 then 0 else - divide_poly_main (coeff g (degree g)) 0 f g (degree f) (1 + length (coeffs f) - length (coeffs g)))" + divide_poly_main (coeff g (degree g)) 0 f g (degree f) (1 + length (coeffs f) - length (coeffs g)))" lemma divide_poly_main: assumes d: "d \ 0" "lc = coeff d (degree d)" - and *: "degree (d * r) \ dr" "divide_poly_main lc q (d * r) d dr n = q'" - "n = 1 + dr - degree d \ dr = 0 \ n = 0 \ d * r = 0" + and *: "degree (d * r) \ dr" "divide_poly_main lc q (d * r) d dr n = q'" + "n = 1 + dr - degree d \ dr = 0 \ n = 0 \ d * r = 0" shows "q' = q + r" using * proof (induct n arbitrary: q r dr) @@ -3043,7 +3002,7 @@ have "coeff (b * d) dr = coeff b n * coeff d (degree d)" proof (cases "?qq = 0") case False - hence n: "n = degree b" by (simp add: degree_monom_eq) + then have n: "n = degree b" by (simp add: degree_monom_eq) show ?thesis unfolding n dr by (simp add: coeff_mult_degree_sum) qed simp also have "\ = lc * coeff b n" unfolding d by simp @@ -3052,26 +3011,26 @@ have c1: "coeff (d * r) dr = lc * coeff r n" proof (cases "degree r = n") case True - thus ?thesis using Suc(2) unfolding dr using coeff_mult_degree_sum[of d r] d by (auto simp: ac_simps) + then show ?thesis using Suc(2) unfolding dr using coeff_mult_degree_sum[of d r] d by (auto simp: ac_simps) next case False have "degree r \ n" using dr Suc(2) by auto (metis add.commute add_le_cancel_left d(1) degree_0 degree_mult_eq diff_is_0_eq diff_zero le_cases) with False have r_n: "degree r < n" by auto - hence right: "lc * coeff r n = 0" by (simp add: coeff_eq_0) + then have right: "lc * coeff r n = 0" by (simp add: coeff_eq_0) have "coeff (d * r) dr = coeff (d * r) (degree d + n)" unfolding dr by (simp add: ac_simps) also have "\ = 0" using r_n - by (metis False Suc.prems(1) add.commute add_left_imp_eq coeff_degree_mult coeff_eq_0 + by (metis False Suc.prems(1) add.commute add_left_imp_eq coeff_degree_mult coeff_eq_0 coeff_mult_degree_sum degree_mult_le dr le_eq_less_or_eq) finally show ?thesis unfolding right . qed - have c0: "coeff ?rrr dr = 0" + have c0: "coeff ?rrr dr = 0" and id: "lc * (coeff (d * r) dr div lc) = coeff (d * r) dr" unfolding rrr coeff_diff c2 unfolding b_def coeff_monom coeff_smult c1 using lc by auto from res[unfolded divide_poly_main.simps[of lc q] Let_def] id - have res: "divide_poly_main lc ?qqq ?rrr d (dr - 1) n = q'" + have res: "divide_poly_main lc ?qqq ?rrr d (dr - 1) n = q'" by (simp del: divide_poly_main.simps add: field_simps) - note IH = Suc(1)[OF _ res] + note IH = Suc(1)[OF _ res] have dr: "dr = n + degree d" using Suc(4) by auto have deg_rr: "degree ?rr \ dr" using Suc(2) by auto have deg_bd: "degree (b * d) \ dr" @@ -3079,7 +3038,7 @@ have "degree ?rrr \ dr" unfolding rrr by (rule degree_diff_le[OF deg_rr deg_bd]) with c0 have deg_rrr: "degree ?rrr \ (dr - 1)" by (rule coeff_0_degree_minus_1) - have "n = 1 + (dr - 1) - degree d \ dr - 1 = 0 \ n = 0 \ ?rrr = 0" + have "n = 1 + (dr - 1) - degree d \ dr - 1 = 0 \ n = 0 \ ?rrr = 0" proof (cases dr) case 0 with Suc(4) have 0: "dr = 0" "n = 0" "degree d = 0" by auto @@ -3091,17 +3050,17 @@ show ?case using IH by simp next case (0 q r dr) - show ?case + show ?case proof (cases "r = 0") case True - thus ?thesis using 0 by auto + then show ?thesis using 0 by auto next case False - have "degree (d * r) = degree d + degree r" using d False + have "degree (d * r) = degree d + degree r" using d False by (subst degree_mult_eq, auto) - thus ?thesis using 0 d by auto + then show ?thesis using 0 d by auto qed -qed +qed lemma divide_poly_main_0: "divide_poly_main 0 0 r d dr n = 0" proof (induct n arbitrary: r d dr) @@ -3112,15 +3071,15 @@ lemma divide_poly: assumes g: "g \ 0" - shows "(f * g) div g = (f :: 'a poly)" -proof - - have "divide_poly_main (coeff g (degree g)) 0 (g * f) g (degree (g * f)) (1 + length (coeffs (g * f)) - length (coeffs g)) + shows "(f * g) div g = (f :: 'a poly)" +proof - + have "divide_poly_main (coeff g (degree g)) 0 (g * f) g (degree (g * f)) (1 + length (coeffs (g * f)) - length (coeffs g)) = (f * g) div g" unfolding divide_poly_def Let_def by (simp add: ac_simps) note main = divide_poly_main[OF g refl le_refl this] { fix f :: "'a poly" assume "f \ 0" - hence "length (coeffs f) = Suc (degree f)" unfolding degree_eq_length_coeffs by auto + then have "length (coeffs f) = Suc (degree f)" unfolding degree_eq_length_coeffs by auto } note len = this have "(f * g) div g = 0 + f" proof (rule main, goal_cases) @@ -3135,7 +3094,7 @@ show ?thesis unfolding len[OF fg] len[OF g] by auto qed qed - thus ?thesis by simp + then show ?thesis by simp qed lemma divide_poly_0: "f div 0 = (0 :: 'a poly)" @@ -3148,7 +3107,7 @@ instance poly :: (idom_divide) algebraic_semidom .. -lemma div_const_poly_conv_map_poly: +lemma div_const_poly_conv_map_poly: assumes "[:c:] dvd p" shows "p div [:c:] = map_poly (\x. x div c) p" proof (cases "c = 0") @@ -3204,7 +3163,7 @@ shows "monom (coeff p (degree p)) 0 = p" using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff) -lemma is_unit_const_poly_iff: +lemma is_unit_const_poly_iff: "[:c :: 'a :: {comm_semiring_1,semiring_no_zero_divisors}:] dvd 1 \ c dvd 1" by (auto simp: one_poly_def) @@ -3243,12 +3202,12 @@ shows "p dvd 1 \ (\c. p = [:c:] \ c dvd 1)" by (auto elim: is_unit_polyE simp add: is_unit_const_poly_iff) - + subsubsection \Pseudo-Division\ text\This part is by René Thiemann and Akihisa Yamada.\ -fun pseudo_divmod_main :: "'a :: comm_ring_1 \ 'a poly \ 'a poly \ 'a poly +fun pseudo_divmod_main :: "'a :: comm_ring_1 \ 'a poly \ 'a poly \ 'a poly \ nat \ nat \ 'a poly \ 'a poly" where "pseudo_divmod_main lc q r d dr (Suc n) = (let rr = smult lc r; @@ -3263,8 +3222,8 @@ pseudo_divmod_main (coeff q (degree q)) 0 p q (degree p) (1 + length (coeffs p) - length (coeffs q))" lemma pseudo_divmod_main: assumes d: "d \ 0" "lc = coeff d (degree d)" - and *: "degree r \ dr" "pseudo_divmod_main lc q r d dr n = (q',r')" - "n = 1 + dr - degree d \ dr = 0 \ n = 0 \ r = 0" + and *: "degree r \ dr" "pseudo_divmod_main lc q r d dr n = (q',r')" + "n = 1 + dr - degree d \ dr = 0 \ n = 0 \ r = 0" shows "(r' = 0 \ degree r' < degree d) \ smult (lc^n) (d * q + r) = d * q' + r'" using * proof (induct n arbitrary: q r dr) @@ -3275,14 +3234,14 @@ let ?rrr = "?rr - b * d" let ?qqq = "smult lc q + b" note res = Suc(3) - from res[unfolded pseudo_divmod_main.simps[of lc q] Let_def] - have res: "pseudo_divmod_main lc ?qqq ?rrr d (dr - 1) n = (q',r')" + from res[unfolded pseudo_divmod_main.simps[of lc q] Let_def] + have res: "pseudo_divmod_main lc ?qqq ?rrr d (dr - 1) n = (q',r')" by (simp del: pseudo_divmod_main.simps) have dr: "dr = n + degree d" using Suc(4) by auto have "coeff (b * d) dr = coeff b n * coeff d (degree d)" proof (cases "?qq = 0") case False - hence n: "n = degree b" by (simp add: degree_monom_eq) + then have n: "n = degree b" by (simp add: degree_monom_eq) show ?thesis unfolding n dr by (simp add: coeff_mult_degree_sum) qed auto also have "\ = lc * coeff b n" unfolding d by simp @@ -3290,8 +3249,8 @@ moreover have "coeff ?rr dr = lc * coeff r dr" by simp ultimately have c0: "coeff ?rrr dr = 0" by auto have dr: "dr = n + degree d" using Suc(4) by auto - have deg_rr: "degree ?rr \ dr" using Suc(2) - using degree_smult_le dual_order.trans by blast + have deg_rr: "degree ?rr \ dr" using Suc(2) + using degree_smult_le dual_order.trans by blast have deg_bd: "degree (b * d) \ dr" unfolding dr by(rule order.trans[OF degree_mult_le], auto simp: degree_monom_le) @@ -3303,7 +3262,7 @@ case 0 with Suc(4) have 0: "dr = 0" "n = 0" "degree d = 0" by auto with deg_rrr have "degree ?rrr = 0" by simp - hence "\ a. ?rrr = [: a :]" by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases) + then have "\ a. ?rrr = [: a :]" by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases) from this obtain a where rrr: "?rrr = [:a:]" by auto show ?thesis unfolding 0 using c0 unfolding rrr 0 by simp qed (insert Suc(4), auto) @@ -3318,7 +3277,7 @@ qed auto lemma pseudo_divmod: - assumes g: "g \ 0" and *: "pseudo_divmod f g = (q,r)" + assumes g: "g \ 0" and *: "pseudo_divmod f g = (q,r)" shows "smult (coeff g (degree g) ^ (Suc (degree f) - degree g)) f = g * q + r" (is ?A) and "r = 0 \ degree r < degree g" (is ?B) proof - @@ -3326,43 +3285,43 @@ have "pseudo_divmod_main (coeff g (degree g)) 0 f g (degree f) (1 + length (coeffs f) - length (coeffs g)) = (q, r)" by (auto simp: g) note main = pseudo_divmod_main[OF _ _ _ this, OF g refl le_refl] have "1 + length (coeffs f) - length (coeffs g) = 1 + degree f - degree g \ - degree f = 0 \ 1 + length (coeffs f) - length (coeffs g) = 0 \ f = 0" using g + degree f = 0 \ 1 + length (coeffs f) - length (coeffs g) = 0 \ f = 0" using g by (cases "f = 0"; cases "coeffs g", auto simp: degree_eq_length_coeffs) note main = main[OF this] from main show "r = 0 \ degree r < degree g" by auto - show "smult (coeff g (degree g) ^ (Suc (degree f) - degree g)) f = g * q + r" + show "smult (coeff g (degree g) ^ (Suc (degree f) - degree g)) f = g * q + r" by (subst main[THEN conjunct2, symmetric], simp add: degree_eq_length_coeffs, insert g, cases "f = 0"; cases "coeffs g", auto) qed - + definition "pseudo_mod_main lc r d dr n = snd (pseudo_divmod_main lc 0 r d dr n)" lemma snd_pseudo_divmod_main: "snd (pseudo_divmod_main lc q r d dr n) = snd (pseudo_divmod_main lc q' r d dr n)" by (induct n arbitrary: q q' lc r d dr; simp add: Let_def) -definition pseudo_mod +definition pseudo_mod :: "'a :: {comm_ring_1,semiring_1_no_zero_divisors} poly \ 'a poly \ 'a poly" where "pseudo_mod f g = snd (pseudo_divmod f g)" - + lemma pseudo_mod: fixes f g defines "r \ pseudo_mod f g" assumes g: "g \ 0" shows "\ a q. a \ 0 \ smult a f = g * q + r" "r = 0 \ degree r < degree g" -proof - +proof - let ?cg = "coeff g (degree g)" let ?cge = "?cg ^ (Suc (degree f) - degree g)" define a where "a = ?cge" obtain q where pdm: "pseudo_divmod f g = (q,r)" using r_def[unfolded pseudo_mod_def] by (cases "pseudo_divmod f g", auto) - from pseudo_divmod[OF g pdm] have id: "smult a f = g * q + r" and "r = 0 \ degree r < degree g" + from pseudo_divmod[OF g pdm] have id: "smult a f = g * q + r" and "r = 0 \ degree r < degree g" unfolding a_def by auto show "r = 0 \ degree r < degree g" by fact from g have "a \ 0" unfolding a_def by auto - thus "\ a q. a \ 0 \ smult a f = g * q + r" using id by auto + then show "\ a q. a \ 0 \ smult a f = g * q + r" using id by auto qed - + lemma fst_pseudo_divmod_main_as_divide_poly_main: assumes d: "d \ 0" defines lc: "lc \ coeff d (degree d)" @@ -3376,12 +3335,12 @@ pseudo_divmod_main lc (smult lc q + monom (coeff r dr) n) (smult lc r - monom (coeff r dr) n * d) d (dr - 1) n" by (simp add: Let_def ac_simps) - also have "fst ... = divide_poly_main lc + also have "fst \ = divide_poly_main lc (smult (lc^n) (smult lc q + monom (coeff r dr) n)) (smult (lc^n) (smult lc r - monom (coeff r dr) n * d)) d (dr - 1) n" unfolding Suc[unfolded divide_poly_main.simps Let_def].. - also have "... = divide_poly_main lc (smult (lc ^ Suc n) q) + also have "\ = divide_poly_main lc (smult (lc ^ Suc n) q) (smult (lc ^ Suc n) r) d dr (Suc n)" unfolding smult_monom smult_distribs mult_smult_left[symmetric] using lc0 by (simp add: Let_def ac_simps) @@ -3399,7 +3358,7 @@ from leading_coeff_neq_0[OF g] have c0: "c \ 0" unfolding c_def by auto from pseudo_divmod(1)[OF g *, folded c_def] have "smult c f = g * q + r" by auto - also have "smult (1/c) ... = g * smult (1/c) q + smult (1/c) r" by (simp add: smult_add_right) + also have "smult (1/c) \ = g * smult (1/c) q + smult (1/c) r" by (simp add: smult_add_right) finally show ?thesis using c0 by auto qed @@ -3415,7 +3374,7 @@ defines "f' \ smult ((1 / coeff g (degree g)) ^ (Suc (degree f) - degree g)) f" shows "(f::'a::field poly) div g = fst (pseudo_divmod f' g)" proof (cases "g = 0") - case True show ?thesis + case True show ?thesis unfolding divide_poly_def pseudo_divmod_def Let_def f'_def True by (simp add: divide_poly_main_0) next case False @@ -3424,7 +3383,7 @@ using length_coeffs_degree[of f'] length_coeffs_degree[of f] unfolding divide_poly_def pseudo_divmod_def Let_def divide_poly_main_field[OF False] - length_coeffs_degree[OF False] + length_coeffs_degree[OF False] f'_def by force qed @@ -3539,8 +3498,8 @@ lemma smult_content_normalize_primitive_part [simp]: "smult (content p) (normalize (primitive_part p)) = normalize p" proof - - have "smult (content p) (normalize (primitive_part p)) = - normalize ([:content p:] * primitive_part p)" + have "smult (content p) (normalize (primitive_part p)) = + normalize ([:content p:] * primitive_part p)" by (subst normalize_mult) (simp_all add: normalize_const_poly) also have "[:content p:] * primitive_part p = p" by simp finally show ?thesis . @@ -3551,14 +3510,14 @@ | eucl_rel_poly_dividesI: "y \ 0 \ x = q * y \ eucl_rel_poly x y (q, 0)" | eucl_rel_poly_remainderI: "y \ 0 \ degree r < degree y \ x = q * y + r \ eucl_rel_poly x y (q, r)" - + lemma eucl_rel_poly_iff: "eucl_rel_poly x y (q, r) \ x = q * y + r \ (if y = 0 then q = 0 else r = 0 \ degree r < degree y)" by (auto elim: eucl_rel_poly.cases intro: eucl_rel_poly_by0 eucl_rel_poly_dividesI eucl_rel_poly_remainderI) - + lemma eucl_rel_poly_0: "eucl_rel_poly 0 y (0, 0)" unfolding eucl_rel_poly_iff by simp @@ -3652,7 +3611,7 @@ instantiation poly :: (field) semidom_modulo begin - + definition modulo_poly :: "'a poly \ 'a poly \ 'a poly" where mod_poly_def: "f mod g = (if g = 0 then f else pseudo_mod (smult ((1 / lead_coeff g) ^ (Suc (degree f) - degree g)) f) g)" @@ -3673,9 +3632,9 @@ by (simp add: power_mult_distrib [symmetric] ac_simps) qed qed - + end - + lemma eucl_rel_poly: "eucl_rel_poly x y (x div y, x mod y)" unfolding eucl_rel_poly_iff proof show "x = x div y * y + x mod y" @@ -3701,10 +3660,10 @@ proof fix x y z :: "'a poly" assume "y \ 0" - hence "eucl_rel_poly (x + z * y) y (z + x div y, x mod y)" + then have "eucl_rel_poly (x + z * y) y (z + x div y, x mod y)" using eucl_rel_poly [of x y] by (simp add: eucl_rel_poly_iff distrib_right) - thus "(x + z * y) div y = z + x div y" + then show "(x + z * y) div y = z + x div y" by (rule div_poly_eq) next fix x y z :: "'a poly" @@ -3765,17 +3724,17 @@ lemma div_poly_less: "degree (x::'a::field poly) < degree y \ x div y = 0" proof - assume "degree x < degree y" - hence "eucl_rel_poly x y (0, x)" + then have "eucl_rel_poly x y (0, x)" by (simp add: eucl_rel_poly_iff) - thus "x div y = 0" by (rule div_poly_eq) + then show "x div y = 0" by (rule div_poly_eq) qed lemma mod_poly_less: "degree x < degree y \ x mod y = x" proof - assume "degree x < degree y" - hence "eucl_rel_poly x y (0, x)" + then have "eucl_rel_poly x y (0, x)" by (simp add: eucl_rel_poly_iff) - thus "x mod y = x" by (rule mod_poly_eq) + then show "x mod y = x" by (rule mod_poly_eq) qed lemma eucl_rel_poly_smult_left: @@ -3885,7 +3844,7 @@ apply (rule eucl_rel_poly_pCons [OF eucl_rel_poly y refl]) done - + subsubsection \List-based versions for fast implementation\ (* Subsection by: Sebastiaan Joosten @@ -3897,7 +3856,7 @@ | "minus_poly_rev_list xs [] = xs" | "minus_poly_rev_list [] (y # ys) = []" -fun pseudo_divmod_main_list :: "'a::comm_ring_1 \ 'a list \ 'a list \ 'a list +fun pseudo_divmod_main_list :: "'a::comm_ring_1 \ 'a list \ 'a list \ 'a list \ nat \ 'a list \ 'a list" where "pseudo_divmod_main_list lc q r d (Suc n) = (let rr = map (op * lc) r; @@ -3907,7 +3866,7 @@ in pseudo_divmod_main_list lc qqq rrr d n)" | "pseudo_divmod_main_list lc q r d 0 = (q,r)" -fun pseudo_mod_main_list :: "'a::comm_ring_1 \ 'a list \ 'a list +fun pseudo_mod_main_list :: "'a::comm_ring_1 \ 'a list \ 'a list \ nat \ 'a list" where "pseudo_mod_main_list lc r d (Suc n) = (let rr = map (op * lc) r; @@ -3917,7 +3876,7 @@ | "pseudo_mod_main_list lc r d 0 = r" -fun divmod_poly_one_main_list :: "'a::comm_ring_1 list \ 'a list \ 'a list +fun divmod_poly_one_main_list :: "'a::comm_ring_1 list \ 'a list \ 'a list \ nat \ 'a list \ 'a list" where "divmod_poly_one_main_list q r d (Suc n) = (let a = hd r; @@ -3926,7 +3885,7 @@ in divmod_poly_one_main_list qqq rr d n)" | "divmod_poly_one_main_list q r d 0 = (q,r)" -fun mod_poly_one_main_list :: "'a::comm_ring_1 list \ 'a list +fun mod_poly_one_main_list :: "'a::comm_ring_1 list \ 'a list \ nat \ 'a list" where "mod_poly_one_main_list r d (Suc n) = (let a = hd r; @@ -3938,14 +3897,14 @@ "pseudo_divmod_list p q = (if q = [] then ([],p) else (let rq = rev q; - (qu,re) = pseudo_divmod_main_list (hd rq) [] (rev p) rq (1 + length p - length q) in + (qu,re) = pseudo_divmod_main_list (hd rq) [] (rev p) rq (1 + length p - length q) in (qu,rev re)))" definition pseudo_mod_list :: "'a::comm_ring_1 list \ 'a list \ 'a list" where "pseudo_mod_list p q = (if q = [] then p else (let rq = rev q; - re = pseudo_mod_main_list (hd rq) (rev p) rq (1 + length p - length q) in + re = pseudo_mod_main_list (hd rq) (rev p) rq (1 + length p - length q) in (rev re)))" lemma minus_zero_does_nothing: @@ -3969,10 +3928,10 @@ Poly (rev (minus_poly_rev_list (rev p) (rev q))) = Poly p - monom 1 (length p - length q) * Poly q" proof (induct "rev p" "rev q" arbitrary: p q rule: minus_poly_rev_list.induct) - case (1 x xs y ys) + case (1 x xs y ys) have "length (rev q) \ length (rev p)" using 1 by simp from this[folded 1(2,3)] have ys_xs:"length ys \ length xs" by simp - hence a:"Poly (rev (minus_poly_rev_list xs ys)) = + then have a:"Poly (rev (minus_poly_rev_list xs ys)) = Poly (rev xs) - monom 1 (length xs - length ys) * Poly (rev ys)" by(subst "1.hyps"(1)[of "rev xs" "rev ys", unfolded rev_rev_ident length_rev],auto) have "Poly p - monom 1 (length p - length q) * Poly q @@ -3997,12 +3956,12 @@ hd (minus_poly_rev_list (map (op * (last d :: 'a :: comm_ring)) r) (map (op * (hd r)) (rev d))) = 0" proof(induct r) case (Cons a rs) - thus ?case by(cases "rev d", simp_all add:ac_simps) + then show ?case by(cases "rev d", simp_all add:ac_simps) qed simp lemma Poly_map: "Poly (map (op * a) p) = smult a (Poly p)" proof (induct p) - case(Cons x xs) thus ?case by (cases "Poly xs = 0",auto) + case(Cons x xs) then show ?case by (cases "Poly xs = 0",auto) qed simp lemma last_coeff_is_hd: "xs \ [] \ coeff (Poly xs) (length xs - 1) = hd (rev xs)" @@ -4014,8 +3973,8 @@ and dNonempty:"d \ []" and "pseudo_divmod_main_list lc q (rev r) (rev d) n = (q',rev r')" and "n = (1 + length r - length d)" - shows - "pseudo_divmod_main lc (monom 1 n * Poly q) (Poly r) (Poly d) (length r - 1) n = + shows + "pseudo_divmod_main lc (monom 1 n * Poly q) (Poly r) (Poly d) (length r - 1) n = (Poly q', Poly r')" using assms(4-) proof(induct "n" arbitrary: r q) @@ -4030,28 +3989,28 @@ have n: "n = (1 + length r - length d - 1)" using ifCond Suc(3) by simp have rr_val:"(length ?rrr) = (length r - 1)" using ifCond by auto - hence rr_smaller: "(1 + length r - length d - 1) = (1 + length ?rrr - length d)" + then have rr_smaller: "(1 + length r - length d - 1) = (1 + length ?rrr - length d)" using rNonempty ifCond unfolding One_nat_def by auto from ifCond have id: "Suc (length r) - length d = Suc (length r - length d)" by auto have "pseudo_divmod_main_list lc ?qq (rev ?rrr) (rev d) (1 + length r - length d - 1) = (q', rev r')" using Suc.prems ifCond by (simp add:Let_def if_0_minus_poly_rev_list id) - hence v:"pseudo_divmod_main_list lc ?qq (rev ?rrr) (rev d) n = (q', rev r')" + then have v:"pseudo_divmod_main_list lc ?qq (rev ?rrr) (rev d) n = (q', rev r')" using n by auto have sucrr:"Suc (length r) - length d = Suc (length r - length d)" using Suc_diff_le ifCond not_less_eq_eq by blast have n_ok : "n = 1 + (length ?rrr) - length d" using Suc(3) rNonempty by simp - have cong: "\ x1 x2 x3 x4 y1 y2 y3 y4. x1 = y1 \ x2 = y2 \ x3 = y3 \ x4 = y4 \ + have cong: "\x1 x2 x3 x4 y1 y2 y3 y4. x1 = y1 \ x2 = y2 \ x3 = y3 \ x4 = y4 \ pseudo_divmod_main lc x1 x2 x3 x4 n = pseudo_divmod_main lc y1 y2 y3 y4 n" by simp have hd_rev:"coeff (Poly r) (length r - Suc 0) = hd (rev r)" using last_coeff_is_hd[OF rNonempty] by simp show ?case unfolding Suc.hyps(1)[OF v n_ok, symmetric] pseudo_divmod_main.simps Let_def proof (rule cong[OF _ _ refl], goal_cases) - case 1 + case 1 show ?case unfolding monom_Suc hd_rev[symmetric] by (simp add: smult_monom Poly_map) next - case 2 - show ?case + case 2 + show ?case proof (subst Poly_on_rev_starting_with_0, goal_cases) show "hd (minus_poly_rev_list (map (op * lc) (rev r)) (map (op * (hd (rev r))) (rev d))) = 0" by (fold lc, subst head_minus_poly_rev_list, insert ifCond dNonempty,auto) @@ -4068,8 +4027,8 @@ map_prod poly_of_list poly_of_list (pseudo_divmod_list (coeffs f) (coeffs g))" proof (cases "g=0") case False - hence coeffs_g_nonempty:"(coeffs g) \ []" by simp - hence lastcoeffs:"last (coeffs g) = coeff g (degree g)" + then have coeffs_g_nonempty:"(coeffs g) \ []" by simp + then have lastcoeffs:"last (coeffs g) = coeff g (degree g)" by (simp add: hd_rev last_coeffs_eq_coeff_degree not_0_coeffs_not_Nil) obtain q r where qr: "pseudo_divmod_main_list (last (coeffs g)) (rev []) @@ -4094,14 +4053,14 @@ by auto qed -lemma pseudo_mod_main_list: "snd (pseudo_divmod_main_list l q +lemma pseudo_mod_main_list: "snd (pseudo_divmod_main_list l q xs ys n) = pseudo_mod_main_list l xs ys n" by (induct n arbitrary: l q xs ys, auto simp: Let_def) lemma pseudo_mod_impl[code]: "pseudo_mod f g = poly_of_list (pseudo_mod_list (coeffs f) (coeffs g))" proof - - have snd_case: "\ f g p. snd ((\ (x,y). (f x, g y)) p) = g (snd p)" + have snd_case: "\f g p. snd ((\(x,y). (f x, g y)) p) = g (snd p)" by auto show ?thesis unfolding pseudo_mod_def pseudo_divmod_impl pseudo_divmod_list_def @@ -4116,9 +4075,9 @@ lemma pdivmod_pdivmodrel: "eucl_rel_poly p q (r, s) \ (p div q, p mod q) = (r, s)" by (metis eucl_rel_poly eucl_rel_poly_unique) -lemma pdivmod_via_pseudo_divmod: "(f div g, f mod g) = (if g = 0 then (0,f) - else let - ilc = inverse (coeff g (degree g)); +lemma pdivmod_via_pseudo_divmod: "(f div g, f mod g) = (if g = 0 then (0,f) + else let + ilc = inverse (coeff g (degree g)); h = smult ilc g; (q,r) = pseudo_divmod f h in (smult ilc q, r))" (is "?l = ?r") @@ -4127,26 +4086,26 @@ define lc where "lc = inverse (coeff g (degree g))" define h where "h = smult lc g" from False have h1: "coeff h (degree h) = 1" and lc: "lc \ 0" unfolding h_def lc_def by auto - hence h0: "h \ 0" by auto + then have h0: "h \ 0" by auto obtain q r where p: "pseudo_divmod f h = (q,r)" by force - from False have id: "?r = (smult lc q, r)" + from False have id: "?r = (smult lc q, r)" unfolding Let_def h_def[symmetric] lc_def[symmetric] p by auto - from pseudo_divmod[OF h0 p, unfolded h1] + from pseudo_divmod[OF h0 p, unfolded h1] have f: "f = h * q + r" and r: "r = 0 \ degree r < degree h" by auto have "eucl_rel_poly f h (q, r)" unfolding eucl_rel_poly_iff using f r h0 by auto - hence "(f div h, f mod h) = (q,r)" by (simp add: pdivmod_pdivmodrel) - hence "(f div g, f mod g) = (smult lc q, r)" + then have "(f div h, f mod h) = (q,r)" by (simp add: pdivmod_pdivmodrel) + then have "(f div g, f mod g) = (smult lc q, r)" unfolding h_def div_smult_right[OF lc] mod_smult_right[OF lc] using lc by auto with id show ?thesis by auto qed simp -lemma pdivmod_via_pseudo_divmod_list: "(f div g, f mod g) = (let +lemma pdivmod_via_pseudo_divmod_list: "(f div g, f mod g) = (let cg = coeffs g in if cg = [] then (0,f) - else let + else let cf = coeffs f; - ilc = inverse (last cg); + ilc = inverse (last cg); ch = map (op * ilc) cg; (q,r) = pseudo_divmod_main_list 1 [] (rev cf) (rev ch) (1 + length cf - length cg) in (poly_of_list (map (op * ilc) q), poly_of_list (rev r)))" @@ -4155,22 +4114,22 @@ pseudo_divmod_impl pseudo_divmod_list_def show ?thesis proof (cases "g = 0") - case True thus ?thesis unfolding d by auto + case True then show ?thesis unfolding d by auto next case False define ilc where "ilc = inverse (coeff g (degree g))" from False have ilc: "ilc \ 0" unfolding ilc_def by auto - with False have id: "(g = 0) = False" "(coeffs g = []) = False" - "last (coeffs g) = coeff g (degree g)" + with False have id: "(g = 0) = False" "(coeffs g = []) = False" + "last (coeffs g) = coeff g (degree g)" "(coeffs (smult ilc g) = []) = False" - by (auto simp: last_coeffs_eq_coeff_degree) - have id2: "hd (rev (coeffs (smult ilc g))) = 1" + by (auto simp: last_coeffs_eq_coeff_degree) + have id2: "hd (rev (coeffs (smult ilc g))) = 1" by (subst hd_rev, insert id ilc, auto simp: coeffs_smult, subst last_map, auto simp: id ilc_def) - have id3: "length (coeffs (smult ilc g)) = length (coeffs g)" + have id3: "length (coeffs (smult ilc g)) = length (coeffs g)" "rev (coeffs (smult ilc g)) = rev (map (op * ilc) (coeffs g))" unfolding coeffs_smult using ilc by auto obtain q r where pair: "pseudo_divmod_main_list 1 [] (rev (coeffs f)) (rev (map (op * ilc) (coeffs g))) (1 + length (coeffs f) - length (coeffs g)) = (q,r)" by force - show ?thesis unfolding d Let_def id if_False ilc_def[symmetric] map_prod_def[symmetric] id2 + show ?thesis unfolding d Let_def id if_False ilc_def[symmetric] map_prod_def[symmetric] id2 unfolding id3 pair map_prod_def split by (auto simp: Poly_map) qed qed @@ -4185,11 +4144,11 @@ show ?case by (induct n arbitrary: q r d, auto simp: Let_def) qed -fun divide_poly_main_list :: "'a::idom_divide \ 'a list \ 'a list \ 'a list +fun divide_poly_main_list :: "'a::idom_divide \ 'a list \ 'a list \ 'a list \ nat \ 'a list" where "divide_poly_main_list lc q r d (Suc n) = (let cr = hd r - in if cr = 0 then divide_poly_main_list lc (cCons cr q) (tl r) d n else let + in if cr = 0 then divide_poly_main_list lc (cCons cr q) (tl r) d n else let a = cr div lc; qq = cCons a q; rr = minus_poly_rev_list r (map (op * a) d) @@ -4231,7 +4190,7 @@ by simp qed -definition div_field_poly_impl :: "'a :: field poly \ 'a poly \ 'a poly" where +definition div_field_poly_impl :: "'a :: field poly \ 'a poly \ 'a poly" where "div_field_poly_impl f g = ( let cg = coeffs g in if cg = [] then 0 @@ -4239,13 +4198,13 @@ q = fst (divmod_poly_one_main_list [] (rev cf) (rev ch) (1 + length cf - length cg)) in poly_of_list ((map (op * ilc) q)))" -text \We do not declare the following lemma as code equation, since then polynomial division - on non-fields will no longer be executable. However, a code-unfold is possible, since +text \We do not declare the following lemma as code equation, since then polynomial division + on non-fields will no longer be executable. However, a code-unfold is possible, since \div_field_poly_impl\ is a bit more efficient than the generic polynomial division.\ lemma div_field_poly_impl[code_unfold]: "op div = div_field_poly_impl" proof (intro ext) fix f g :: "'a poly" - have "fst (f div g, f mod g) = div_field_poly_impl f g" unfolding + have "fst (f div g, f mod g) = div_field_poly_impl f g" unfolding div_field_poly_impl_def pdivmod_via_divmod_list Let_def by (auto split: prod.splits) then show "f div g = div_field_poly_impl f g" by simp @@ -4256,7 +4215,7 @@ and lc:"last d = lc" and d:"d \ []" and "n = (1 + length r - length d)" - shows + shows "Poly (divide_poly_main_list lc q (rev r) (rev d) n) = divide_poly_main lc (monom 1 n * Poly q) (Poly r) (Poly d) (length r - 1) n" using assms(4-) @@ -4266,43 +4225,43 @@ have r: "r \ []" using ifCond d using Suc_leI length_greater_0_conv list.size(3) by fastforce then obtain rr lcr where r: "r = rr @ [lcr]" by (cases r rule: rev_cases, auto) - from d lc obtain dd where d: "d = dd @ [lc]" + from d lc obtain dd where d: "d = dd @ [lc]" by (cases d rule: rev_cases, auto) from Suc(2) ifCond have n: "n = 1 + length rr - length d" by (auto simp: r) from ifCond have len: "length dd \ length rr" by (simp add: r d) show ?case proof (cases "lcr div lc * lc = lcr") case False - thus ?thesis unfolding Suc(2)[symmetric] using r d + then show ?thesis unfolding Suc(2)[symmetric] using r d by (auto simp add: Let_def nth_default_append) next case True - hence id: + then have id: "?thesis = (Poly (divide_poly_main_list lc (cCons (lcr div lc) q) - (rev (rev (minus_poly_rev_list (rev rr) (rev (map (op * (lcr div lc)) dd))))) (rev d) n) = + (rev (rev (minus_poly_rev_list (rev rr) (rev (map (op * (lcr div lc)) dd))))) (rev d) n) = divide_poly_main lc (monom 1 (Suc n) * Poly q + monom (lcr div lc) n) (Poly r - monom (lcr div lc) n * Poly d) (Poly d) (length rr - 1) n)" - using r d - by (cases r rule: rev_cases; cases "d" rule: rev_cases; - auto simp add: Let_def rev_map nth_default_append) - have cong: "\ x1 x2 x3 x4 y1 y2 y3 y4. x1 = y1 \ x2 = y2 \ x3 = y3 \ x4 = y4 \ + using r d + by (cases r rule: rev_cases; cases "d" rule: rev_cases; + auto simp add: Let_def rev_map nth_default_append) + have cong: "\x1 x2 x3 x4 y1 y2 y3 y4. x1 = y1 \ x2 = y2 \ x3 = y3 \ x4 = y4 \ divide_poly_main lc x1 x2 x3 x4 n = divide_poly_main lc y1 y2 y3 y4 n" by simp - show ?thesis unfolding id + show ?thesis unfolding id proof (subst Suc(1), simp add: n, subst minus_poly_rev_list, force simp: len, rule cong[OF _ _ refl], goal_cases) - case 2 + case 2 have "monom lcr (length rr) = monom (lcr div lc) (length rr - length dd) * monom lc (length dd)" by (simp add: mult_monom len True) - thus ?case unfolding r d Poly_append n ring_distribs + then show ?case unfolding r d Poly_append n ring_distribs by (auto simp: Poly_map smult_monom smult_monom_mult) qed (auto simp: len monom_Suc smult_monom) qed qed simp -lemma divide_poly_list[code]: "f div g = divide_poly_list f g" +lemma divide_poly_list[code]: "f div g = divide_poly_list f g" proof - note d = divide_poly_def divide_poly_list_def show ?thesis @@ -4311,9 +4270,9 @@ show ?thesis unfolding d True by auto next case False - then obtain cg lcg where cg: "coeffs g = cg @ [lcg]" by (cases "coeffs g" rule: rev_cases, auto) + then obtain cg lcg where cg: "coeffs g = cg @ [lcg]" by (cases "coeffs g" rule: rev_cases, auto) with False have id: "(g = 0) = False" "(cg @ [lcg] = []) = False" by auto - from cg False have lcg: "coeff g (degree g) = lcg" + from cg False have lcg: "coeff g (degree g) = lcg" using last_coeffs_eq_coeff_degree last_snoc by force with False have lcg0: "lcg \ 0" by auto from cg have ltp: "Poly (cg @ [lcg]) = g"