author haftmann Sat Jun 15 17:19:23 2013 +0200 (2013-06-15) changeset 52380 3cc46b8cca5e parent 52379 7f864f2219a9 child 52381 63eec9cea2c7
lifting for primitive definitions;
explicit conversions from and to lists of coefficients, used for generated code;
replaced recursion operator poly_rec by fold_coeffs, preferring function definitions for non-trivial recursions;
prefer pre-existing gcd operation for gcd
 NEWS file | annotate | diff | revisions src/HOL/Library/Fundamental_Theorem_Algebra.thy file | annotate | diff | revisions src/HOL/Library/Poly_Deriv.thy file | annotate | diff | revisions src/HOL/Library/Polynomial.thy file | annotate | diff | revisions src/HOL/List.thy file | annotate | diff | revisions src/HOL/Set_Interval.thy file | annotate | diff | revisions
```     1.1 --- a/NEWS	Sat Jun 15 17:19:23 2013 +0200
1.2 +++ b/NEWS	Sat Jun 15 17:19:23 2013 +0200
1.3 @@ -61,6 +61,17 @@
1.4
1.5  *** HOL ***
1.6
1.7 +* Library/Polynomial.thy:
1.8 +  * Use lifting for primitive definitions.
1.9 +  * Explicit conversions from and to lists of coefficients, used for generated code.
1.10 +  * Replaced recursion operator poly_rec by fold_coeffs.
1.11 +  * Prefer pre-existing gcd operation for gcd.
1.12 +  * Fact renames:
1.13 +    poly_eq_iff ~> poly_eq_poly_eq_iff
1.14 +    poly_ext ~> poly_eqI
1.15 +    expand_poly_eq ~> poly_eq_iff
1.16 +IMCOMPATIBILTIY.
1.17 +
1.18  * Reification and reflection:
1.19    * Reification is now directly available in HOL-Main in structure "Reification".
1.20    * Reflection now handles multiple lists with variables also.
```
```     2.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Jun 15 17:19:23 2013 +0200
2.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Jun 15 17:19:23 2013 +0200
2.3 @@ -93,16 +93,17 @@
2.4
2.5  text{* Offsetting the variable in a polynomial gives another of same degree *}
2.6
2.7 -definition
2.8 -  "offset_poly p h = poly_rec 0 (\<lambda>a p q. smult h q + pCons a q) p"
2.9 +definition offset_poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly"
2.10 +where
2.11 +  "offset_poly p h = fold_coeffs (\<lambda>a q. smult h q + pCons a q) p 0"
2.12
2.13  lemma offset_poly_0: "offset_poly 0 h = 0"
2.14 -  unfolding offset_poly_def by (simp add: poly_rec_0)
2.15 +  by (simp add: offset_poly_def)
2.16
2.17  lemma offset_poly_pCons:
2.18    "offset_poly (pCons a p) h =
2.19      smult h (offset_poly p h) + pCons a (offset_poly p h)"
2.20 -  unfolding offset_poly_def by (simp add: poly_rec_pCons)
2.21 +  by (cases "p = 0 \<and> a = 0") (auto simp add: offset_poly_def)
2.22
2.23  lemma offset_poly_single: "offset_poly [:a:] h = [:a:]"
2.24  by (simp add: offset_poly_pCons offset_poly_0)
2.25 @@ -644,7 +645,7 @@
2.26      let ?r = "smult (inverse ?a0) q"
2.27      have lgqr: "psize q = psize ?r"
2.28        using a00 unfolding psize_def degree_def
2.29 -      by (simp add: expand_poly_eq)
2.30 +      by (simp add: poly_eq_iff)
2.31      {assume h: "\<And>x y. poly ?r x = poly ?r y"
2.32        {fix x y
2.33          from qr[rule_format, of x]
2.34 @@ -887,9 +888,7 @@
2.35  proof-
2.36    {assume pe: "p = 0"
2.37      hence eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0"
2.38 -      apply auto
2.39 -      apply (rule poly_zero [THEN iffD1])
2.40 -      by (rule ext, simp)
2.41 +      by (auto simp add: poly_all_0_iff_0)
2.42      {assume "p dvd (q ^ (degree p))"
2.43        then obtain r where r: "q ^ (degree p) = p * r" ..
2.44        from r pe have False by simp}
2.45 @@ -927,7 +926,7 @@
2.46    assume l: ?lhs
2.47    from l[unfolded constant_def, rule_format, of _ "0"]
2.48    have th: "poly p = poly [:poly p 0:]" apply - by (rule ext, simp)
2.49 -  then have "p = [:poly p 0:]" by (simp add: poly_eq_iff)
2.50 +  then have "p = [:poly p 0:]" by (simp add: poly_eq_poly_eq_iff)
2.51    then have "degree p = degree [:poly p 0:]" by simp
2.52    then show ?rhs by simp
2.53  next
2.54 @@ -1050,7 +1049,7 @@
2.55  lemma  basic_cqe_conv_2b: "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> (p \<noteq> 0)"
2.56  proof-
2.57    have "p = 0 \<longleftrightarrow> poly p = poly 0"
2.58 -    by (simp add: poly_zero)
2.59 +    by (simp add: poly_eq_poly_eq_iff)
2.60    also have "\<dots> \<longleftrightarrow> (\<not> (\<exists>x. poly p x \<noteq> 0))" by auto
2.61    finally show "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> p \<noteq> 0"
2.62      by - (atomize (full), blast)
2.63 @@ -1074,7 +1073,7 @@
2.64    shows "p dvd (q ^ n) \<equiv> p dvd r"
2.65  proof-
2.66    from h have "poly (q ^ n) = poly r" by auto
2.67 -  then have "(q ^ n) = r" by (simp add: poly_eq_iff)
2.68 +  then have "(q ^ n) = r" by (simp add: poly_eq_poly_eq_iff)
2.69    thus "p dvd (q ^ n) \<equiv> p dvd r" by simp
2.70  qed
2.71
```
```     3.1 --- a/src/HOL/Library/Poly_Deriv.thy	Sat Jun 15 17:19:23 2013 +0200
3.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Sat Jun 15 17:19:23 2013 +0200
3.3 @@ -11,26 +11,41 @@
3.4
3.5  subsection {* Derivatives of univariate polynomials *}
3.6
3.7 -definition
3.8 -  pderiv :: "'a::real_normed_field poly \<Rightarrow> 'a poly" where
3.9 -  "pderiv = poly_rec 0 (\<lambda>a p p'. p + pCons 0 p')"
3.10 +function pderiv :: "'a::real_normed_field poly \<Rightarrow> 'a poly"
3.11 +where
3.12 +  [simp del]: "pderiv (pCons a p) = (if p = 0 then 0 else p + pCons 0 (pderiv p))"
3.13 +  by (auto intro: pCons_cases)
3.14 +
3.15 +termination pderiv
3.16 +  by (relation "measure degree") simp_all
3.17
3.18 -lemma pderiv_0 [simp]: "pderiv 0 = 0"
3.19 -  unfolding pderiv_def by (simp add: poly_rec_0)
3.20 +lemma pderiv_0 [simp]:
3.21 +  "pderiv 0 = 0"
3.22 +  using pderiv.simps [of 0 0] by simp
3.23
3.24 -lemma pderiv_pCons: "pderiv (pCons a p) = p + pCons 0 (pderiv p)"
3.25 -  unfolding pderiv_def by (simp add: poly_rec_pCons)
3.26 +lemma pderiv_pCons:
3.27 +  "pderiv (pCons a p) = p + pCons 0 (pderiv p)"
3.28 +  by (simp add: pderiv.simps)
3.29
3.30  lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)"
3.31    apply (induct p arbitrary: n, simp)
3.32    apply (simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
3.33    done
3.34
3.35 +primrec pderiv_coeffs :: "'a::comm_monoid_add list \<Rightarrow> 'a list"
3.36 +where
3.37 +  "pderiv_coeffs [] = []"
3.38 +| "pderiv_coeffs (x # xs) = plus_coeffs xs (cCons 0 (pderiv_coeffs xs))"
3.39 +
3.40 +lemma coeffs_pderiv [code abstract]:
3.41 +  "coeffs (pderiv p) = pderiv_coeffs (coeffs p)"
3.42 +  by (rule sym, induct p) (simp_all add: pderiv_pCons coeffs_plus_eq_plus_coeffs cCons_def)
3.43 +
3.44  lemma pderiv_eq_0_iff: "pderiv p = 0 \<longleftrightarrow> degree p = 0"
3.45    apply (rule iffI)
3.46    apply (cases p, simp)
3.47 -  apply (simp add: expand_poly_eq coeff_pderiv del: of_nat_Suc)
3.48 -  apply (simp add: expand_poly_eq coeff_pderiv coeff_eq_0)
3.49 +  apply (simp add: poly_eq_iff coeff_pderiv del: of_nat_Suc)
3.50 +  apply (simp add: poly_eq_iff coeff_pderiv coeff_eq_0)
3.51    done
3.52
3.53  lemma degree_pderiv: "degree (pderiv p) = degree p - 1"
3.54 @@ -47,16 +62,16 @@
3.55  by (simp add: pderiv_pCons)
3.56
3.57  lemma pderiv_add: "pderiv (p + q) = pderiv p + pderiv q"
3.58 -by (rule poly_ext, simp add: coeff_pderiv algebra_simps)
3.59 +by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
3.60
3.61  lemma pderiv_minus: "pderiv (- p) = - pderiv p"
3.62 -by (rule poly_ext, simp add: coeff_pderiv)
3.63 +by (rule poly_eqI, simp add: coeff_pderiv)
3.64
3.65  lemma pderiv_diff: "pderiv (p - q) = pderiv p - pderiv q"
3.66 -by (rule poly_ext, simp add: coeff_pderiv algebra_simps)
3.67 +by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
3.68
3.69  lemma pderiv_smult: "pderiv (smult a p) = smult a (pderiv p)"
3.70 -by (rule poly_ext, simp add: coeff_pderiv algebra_simps)
3.71 +by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
3.72
3.73  lemma pderiv_mult: "pderiv (p * q) = p * pderiv q + q * pderiv p"
3.74  apply (induct p)
3.75 @@ -75,6 +90,7 @@
3.76  apply (simp add: algebra_simps) (* FIXME *)
3.77  done
3.78
3.79 +
3.80  lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c :: real) x :> D * c"
3.81  by (simp add: DERIV_cmult mult_commute [of _ c])
3.82
```
```     4.1 --- a/src/HOL/Library/Polynomial.thy	Sat Jun 15 17:19:23 2013 +0200
4.2 +++ b/src/HOL/Library/Polynomial.thy	Sat Jun 15 17:19:23 2013 +0200
4.3 @@ -1,47 +1,201 @@
4.4  (*  Title:      HOL/Library/Polynomial.thy
4.5      Author:     Brian Huffman
4.6      Author:     Clemens Ballarin
4.7 +    Author:     Florian Haftmann
4.8  *)
4.9
4.10 -header {* Univariate Polynomials *}
4.11 +header {* Polynomials as type over a ring structure *}
4.12
4.13  theory Polynomial
4.14 -imports Main
4.15 +imports Main GCD
4.16  begin
4.17
4.18 +subsection {* Auxiliary: operations for lists (later) representing coefficients *}
4.19 +
4.20 +definition strip_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
4.21 +where
4.22 +  "strip_while P = rev \<circ> dropWhile P \<circ> rev"
4.23 +
4.24 +lemma strip_while_Nil [simp]:
4.25 +  "strip_while P [] = []"
4.26 +  by (simp add: strip_while_def)
4.27 +
4.28 +lemma strip_while_append [simp]:
4.29 +  "\<not> P x \<Longrightarrow> strip_while P (xs @ [x]) = xs @ [x]"
4.30 +  by (simp add: strip_while_def)
4.31 +
4.32 +lemma strip_while_append_rec [simp]:
4.33 +  "P x \<Longrightarrow> strip_while P (xs @ [x]) = strip_while P xs"
4.34 +  by (simp add: strip_while_def)
4.35 +
4.36 +lemma strip_while_Cons [simp]:
4.37 +  "\<not> P x \<Longrightarrow> strip_while P (x # xs) = x # strip_while P xs"
4.38 +  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
4.39 +
4.40 +lemma strip_while_eq_Nil [simp]:
4.41 +  "strip_while P xs = [] \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
4.42 +  by (simp add: strip_while_def)
4.43 +
4.44 +lemma strip_while_eq_Cons_rec:
4.45 +  "strip_while P (x # xs) = x # strip_while P xs \<longleftrightarrow> \<not> (P x \<and> (\<forall>x\<in>set xs. P x))"
4.46 +  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
4.47 +
4.48 +lemma strip_while_not_last [simp]:
4.49 +  "\<not> P (last xs) \<Longrightarrow> strip_while P xs = xs"
4.50 +  by (cases xs rule: rev_cases) simp_all
4.51 +
4.52 +lemma split_strip_while_append:
4.53 +  fixes xs :: "'a list"
4.54 +  obtains ys zs :: "'a list"
4.55 +  where "strip_while P xs = ys" and "\<forall>x\<in>set zs. P x" and "xs = ys @ zs"
4.56 +proof (rule that)
4.57 +  show "strip_while P xs = strip_while P xs" ..
4.58 +  show "\<forall>x\<in>set (rev (takeWhile P (rev xs))). P x" by (simp add: takeWhile_eq_all_conv [symmetric])
4.59 +  have "rev xs = rev (strip_while P xs @ rev (takeWhile P (rev xs)))"
4.60 +    by (simp add: strip_while_def)
4.61 +  then show "xs = strip_while P xs @ rev (takeWhile P (rev xs))"
4.62 +    by (simp only: rev_is_rev_conv)
4.63 +qed
4.64 +
4.65 +
4.66 +definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
4.67 +where
4.68 +  "nth_default x xs n = (if n < length xs then xs ! n else x)"
4.69 +
4.70 +lemma nth_default_Nil [simp]:
4.71 +  "nth_default y [] n = y"
4.72 +  by (simp add: nth_default_def)
4.73 +
4.74 +lemma nth_default_Cons_0 [simp]:
4.75 +  "nth_default y (x # xs) 0 = x"
4.76 +  by (simp add: nth_default_def)
4.77 +
4.78 +lemma nth_default_Cons_Suc [simp]:
4.79 +  "nth_default y (x # xs) (Suc n) = nth_default y xs n"
4.80 +  by (simp add: nth_default_def)
4.81 +
4.82 +lemma nth_default_map_eq:
4.83 +  "f y = x \<Longrightarrow> nth_default x (map f xs) n = f (nth_default y xs n)"
4.84 +  by (simp add: nth_default_def)
4.85 +
4.86 +lemma nth_default_strip_while_eq [simp]:
4.87 +  "nth_default x (strip_while (HOL.eq x) xs) n = nth_default x xs n"
4.88 +proof -
4.89 +  from split_strip_while_append obtain ys zs
4.90 +    where "strip_while (HOL.eq x) xs = ys" and "\<forall>z\<in>set zs. x = z" and "xs = ys @ zs" by blast
4.91 +  then show ?thesis by (simp add: nth_default_def not_less nth_append)
4.92 +qed
4.93 +
4.94 +
4.95 +definition cCons :: "'a::zero \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixr "##" 65)
4.96 +where
4.97 +  "x ## xs = (if xs = [] \<and> x = 0 then [] else x # xs)"
4.98 +
4.99 +lemma cCons_0_Nil_eq [simp]:
4.100 +  "0 ## [] = []"
4.101 +  by (simp add: cCons_def)
4.102 +
4.103 +lemma cCons_Cons_eq [simp]:
4.104 +  "x ## y # ys = x # y # ys"
4.105 +  by (simp add: cCons_def)
4.106 +
4.107 +lemma cCons_append_Cons_eq [simp]:
4.108 +  "x ## xs @ y # ys = x # xs @ y # ys"
4.109 +  by (simp add: cCons_def)
4.110 +
4.111 +lemma cCons_not_0_eq [simp]:
4.112 +  "x \<noteq> 0 \<Longrightarrow> x ## xs = x # xs"
4.113 +  by (simp add: cCons_def)
4.114 +
4.115 +lemma strip_while_not_0_Cons_eq [simp]:
4.116 +  "strip_while (\<lambda>x. x = 0) (x # xs) = x ## strip_while (\<lambda>x. x = 0) xs"
4.117 +proof (cases "x = 0")
4.118 +  case False then show ?thesis by simp
4.119 +next
4.120 +  case True show ?thesis
4.121 +  proof (induct xs rule: rev_induct)
4.122 +    case Nil with True show ?case by simp
4.123 +  next
4.124 +    case (snoc y ys) then show ?case
4.125 +      by (cases "y = 0") (simp_all add: append_Cons [symmetric] del: append_Cons)
4.126 +  qed
4.127 +qed
4.128 +
4.129 +lemma tl_cCons [simp]:
4.130 +  "tl (x ## xs) = xs"
4.131 +  by (simp add: cCons_def)
4.132 +
4.133 +
4.134 +subsection {* Almost everywhere zero functions *}
4.135 +
4.136 +definition almost_everywhere_zero :: "(nat \<Rightarrow> 'a::zero) \<Rightarrow> bool"
4.137 +where
4.138 +  "almost_everywhere_zero f \<longleftrightarrow> (\<exists>n. \<forall>i>n. f i = 0)"
4.139 +
4.140 +lemma almost_everywhere_zeroI:
4.141 +  "(\<And>i. i > n \<Longrightarrow> f i = 0) \<Longrightarrow> almost_everywhere_zero f"
4.142 +  by (auto simp add: almost_everywhere_zero_def)
4.143 +
4.144 +lemma almost_everywhere_zeroE:
4.145 +  assumes "almost_everywhere_zero f"
4.146 +  obtains n where "\<And>i. i > n \<Longrightarrow> f i = 0"
4.147 +proof -
4.148 +  from assms have "\<exists>n. \<forall>i>n. f i = 0" by (simp add: almost_everywhere_zero_def)
4.149 +  then obtain n where "\<And>i. i > n \<Longrightarrow> f i = 0" by blast
4.150 +  with that show thesis .
4.151 +qed
4.152 +
4.153 +lemma almost_everywhere_zero_nat_case:
4.154 +  assumes "almost_everywhere_zero f"
4.155 +  shows "almost_everywhere_zero (nat_case a f)"
4.156 +  using assms
4.157 +  by (auto intro!: almost_everywhere_zeroI elim!: almost_everywhere_zeroE split: nat.split)
4.158 +    blast
4.159 +
4.160 +lemma almost_everywhere_zero_Suc:
4.161 +  assumes "almost_everywhere_zero f"
4.162 +  shows "almost_everywhere_zero (\<lambda>n. f (Suc n))"
4.163 +proof -
4.164 +  from assms obtain n where "\<And>i. i > n \<Longrightarrow> f i = 0" by (erule almost_everywhere_zeroE)
4.165 +  then have "\<And>i. i > n \<Longrightarrow> f (Suc i) = 0" by auto
4.166 +  then show ?thesis by (rule almost_everywhere_zeroI)
4.167 +qed
4.168 +
4.169 +
4.170  subsection {* Definition of type @{text poly} *}
4.171
4.172 -definition "Poly = {f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"
4.173 -
4.174 -typedef 'a poly = "Poly :: (nat => 'a::zero) set"
4.175 +typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. almost_everywhere_zero f}"
4.176    morphisms coeff Abs_poly
4.177 -  unfolding Poly_def by auto
4.178 +  unfolding almost_everywhere_zero_def by auto
4.179
4.180 -(* FIXME should be named poly_eq_iff *)
4.181 -lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
4.182 +setup_lifting (no_code) type_definition_poly
4.183 +
4.184 +lemma poly_eq_iff: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
4.185    by (simp add: coeff_inject [symmetric] fun_eq_iff)
4.186
4.187 -(* FIXME should be named poly_eqI *)
4.188 -lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
4.189 -  by (simp add: expand_poly_eq)
4.190 +lemma poly_eqI: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
4.191 +  by (simp add: poly_eq_iff)
4.192 +
4.193 +lemma coeff_almost_everywhere_zero:
4.194 +  "almost_everywhere_zero (coeff p)"
4.195 +  using coeff [of p] by simp
4.196
4.197
4.198  subsection {* Degree of a polynomial *}
4.199
4.200 -definition
4.201 -  degree :: "'a::zero poly \<Rightarrow> nat" where
4.202 +definition degree :: "'a::zero poly \<Rightarrow> nat"
4.203 +where
4.204    "degree p = (LEAST n. \<forall>i>n. coeff p i = 0)"
4.205
4.206 -lemma coeff_eq_0: "degree p < n \<Longrightarrow> coeff p n = 0"
4.207 +lemma coeff_eq_0:
4.208 +  assumes "degree p < n"
4.209 +  shows "coeff p n = 0"
4.210  proof -
4.211 -  have "coeff p \<in> Poly"
4.212 -    by (rule coeff)
4.213 -  hence "\<exists>n. \<forall>i>n. coeff p i = 0"
4.214 -    unfolding Poly_def by simp
4.215 -  hence "\<forall>i>degree p. coeff p i = 0"
4.216 +  from coeff_almost_everywhere_zero
4.217 +  have "\<exists>n. \<forall>i>n. coeff p i = 0" by (blast intro: almost_everywhere_zeroE)
4.218 +  then have "\<forall>i>degree p. coeff p i = 0"
4.219      unfolding degree_def by (rule LeastI_ex)
4.220 -  moreover assume "degree p < n"
4.221 -  ultimately show ?thesis by simp
4.222 +  with assms show ?thesis by simp
4.223  qed
4.224
4.225  lemma le_degree: "coeff p n \<noteq> 0 \<Longrightarrow> n \<le> degree p"
4.226 @@ -59,25 +213,28 @@
4.227  instantiation poly :: (zero) zero
4.228  begin
4.229
4.230 -definition
4.231 -  zero_poly_def: "0 = Abs_poly (\<lambda>n. 0)"
4.232 +lift_definition zero_poly :: "'a poly"
4.233 +  is "\<lambda>_. 0" by (rule almost_everywhere_zeroI) simp
4.234
4.235  instance ..
4.236 +
4.237  end
4.238
4.239 -lemma coeff_0 [simp]: "coeff 0 n = 0"
4.240 -  unfolding zero_poly_def
4.241 -  by (simp add: Abs_poly_inverse Poly_def)
4.242 +lemma coeff_0 [simp]:
4.243 +  "coeff 0 n = 0"
4.244 +  by transfer rule
4.245
4.246 -lemma degree_0 [simp]: "degree 0 = 0"
4.247 +lemma degree_0 [simp]:
4.248 +  "degree 0 = 0"
4.249    by (rule order_antisym [OF degree_le le0]) simp
4.250
4.252 -  assumes "p \<noteq> 0" shows "coeff p (degree p) \<noteq> 0"
4.253 +  assumes "p \<noteq> 0"
4.254 +  shows "coeff p (degree p) \<noteq> 0"
4.255  proof (cases "degree p")
4.256    case 0
4.257    from `p \<noteq> 0` have "\<exists>n. coeff p n \<noteq> 0"
4.258 -    by (simp add: expand_poly_eq)
4.259 +    by (simp add: poly_eq_iff)
4.260    then obtain n where "coeff p n \<noteq> 0" ..
4.261    hence "n \<le> degree p" by (rule le_degree)
4.262    with `coeff p n \<noteq> 0` and `degree p = 0`
4.263 @@ -93,68 +250,59 @@
4.264    with `coeff p i \<noteq> 0` show "coeff p (degree p) \<noteq> 0" by simp
4.265  qed
4.266
4.267 -lemma leading_coeff_0_iff [simp]: "coeff p (degree p) = 0 \<longleftrightarrow> p = 0"
4.268 +lemma leading_coeff_0_iff [simp]:
4.269 +  "coeff p (degree p) = 0 \<longleftrightarrow> p = 0"
4.270    by (cases "p = 0", simp, simp add: leading_coeff_neq_0)
4.271
4.272
4.273  subsection {* List-style constructor for polynomials *}
4.274
4.275 -definition
4.276 -  pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
4.277 -where
4.278 -  "pCons a p = Abs_poly (nat_case a (coeff p))"
4.279 +lift_definition pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
4.280 +  is "\<lambda>a p. nat_case a (coeff p)"
4.281 +  using coeff_almost_everywhere_zero by (rule almost_everywhere_zero_nat_case)
4.282
4.283 -syntax
4.284 -  "_poly" :: "args \<Rightarrow> 'a poly"  ("[:(_):]")
4.285 +lemmas coeff_pCons = pCons.rep_eq
4.286
4.287 -translations
4.288 -  "[:x, xs:]" == "CONST pCons x [:xs:]"
4.289 -  "[:x:]" == "CONST pCons x 0"
4.290 -  "[:x:]" <= "CONST pCons x (_constrain 0 t)"
4.291 +lemma coeff_pCons_0 [simp]:
4.292 +  "coeff (pCons a p) 0 = a"
4.293 +  by transfer simp
4.294
4.295 -lemma Poly_nat_case: "f \<in> Poly \<Longrightarrow> nat_case a f \<in> Poly"
4.296 -  unfolding Poly_def by (auto split: nat.split)
4.297 -
4.298 -lemma coeff_pCons:
4.299 -  "coeff (pCons a p) = nat_case a (coeff p)"
4.300 -  unfolding pCons_def
4.301 -  by (simp add: Abs_poly_inverse Poly_nat_case coeff)
4.302 -
4.303 -lemma coeff_pCons_0 [simp]: "coeff (pCons a p) 0 = a"
4.304 +lemma coeff_pCons_Suc [simp]:
4.305 +  "coeff (pCons a p) (Suc n) = coeff p n"
4.306    by (simp add: coeff_pCons)
4.307
4.308 -lemma coeff_pCons_Suc [simp]: "coeff (pCons a p) (Suc n) = coeff p n"
4.309 -  by (simp add: coeff_pCons)
4.310 -
4.311 -lemma degree_pCons_le: "degree (pCons a p) \<le> Suc (degree p)"
4.312 -by (rule degree_le, simp add: coeff_eq_0 coeff_pCons split: nat.split)
4.313 +lemma degree_pCons_le:
4.314 +  "degree (pCons a p) \<le> Suc (degree p)"
4.315 +  by (rule degree_le) (simp add: coeff_eq_0 coeff_pCons split: nat.split)
4.316
4.317  lemma degree_pCons_eq:
4.318    "p \<noteq> 0 \<Longrightarrow> degree (pCons a p) = Suc (degree p)"
4.319 -apply (rule order_antisym [OF degree_pCons_le])
4.320 -apply (rule le_degree, simp)
4.321 -done
4.322 +  apply (rule order_antisym [OF degree_pCons_le])
4.323 +  apply (rule le_degree, simp)
4.324 +  done
4.325
4.326 -lemma degree_pCons_0: "degree (pCons a 0) = 0"
4.327 -apply (rule order_antisym [OF _ le0])
4.328 -apply (rule degree_le, simp add: coeff_pCons split: nat.split)
4.329 -done
4.330 +lemma degree_pCons_0:
4.331 +  "degree (pCons a 0) = 0"
4.332 +  apply (rule order_antisym [OF _ le0])
4.333 +  apply (rule degree_le, simp add: coeff_pCons split: nat.split)
4.334 +  done
4.335
4.336  lemma degree_pCons_eq_if [simp]:
4.337    "degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))"
4.338 -apply (cases "p = 0", simp_all)
4.339 -apply (rule order_antisym [OF _ le0])
4.340 -apply (rule degree_le, simp add: coeff_pCons split: nat.split)
4.341 -apply (rule order_antisym [OF degree_pCons_le])
4.342 -apply (rule le_degree, simp)
4.343 -done
4.344 +  apply (cases "p = 0", simp_all)
4.345 +  apply (rule order_antisym [OF _ le0])
4.346 +  apply (rule degree_le, simp add: coeff_pCons split: nat.split)
4.347 +  apply (rule order_antisym [OF degree_pCons_le])
4.348 +  apply (rule le_degree, simp)
4.349 +  done
4.350
4.351 -lemma pCons_0_0 [simp, code_post]: "pCons 0 0 = 0"
4.352 -by (rule poly_ext, simp add: coeff_pCons split: nat.split)
4.353 +lemma pCons_0_0 [simp]:
4.354 +  "pCons 0 0 = 0"
4.355 +  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
4.356
4.357  lemma pCons_eq_iff [simp]:
4.358    "pCons a p = pCons b q \<longleftrightarrow> a = b \<and> p = q"
4.359 -proof (safe)
4.360 +proof safe
4.361    assume "pCons a p = pCons b q"
4.362    then have "coeff (pCons a p) 0 = coeff (pCons b q) 0" by simp
4.363    then show "a = b" by simp
4.364 @@ -162,23 +310,19 @@
4.365    assume "pCons a p = pCons b q"
4.366    then have "\<forall>n. coeff (pCons a p) (Suc n) =
4.367                   coeff (pCons b q) (Suc n)" by simp
4.368 -  then show "p = q" by (simp add: expand_poly_eq)
4.369 +  then show "p = q" by (simp add: poly_eq_iff)
4.370  qed
4.371
4.372 -lemma pCons_eq_0_iff [simp]: "pCons a p = 0 \<longleftrightarrow> a = 0 \<and> p = 0"
4.373 +lemma pCons_eq_0_iff [simp]:
4.374 +  "pCons a p = 0 \<longleftrightarrow> a = 0 \<and> p = 0"
4.375    using pCons_eq_iff [of a p 0 0] by simp
4.376
4.377 -lemma Poly_Suc: "f \<in> Poly \<Longrightarrow> (\<lambda>n. f (Suc n)) \<in> Poly"
4.378 -  unfolding Poly_def
4.379 -  by (clarify, rule_tac x=n in exI, simp)
4.380 -
4.381  lemma pCons_cases [cases type: poly]:
4.382    obtains (pCons) a q where "p = pCons a q"
4.383  proof
4.384    show "p = pCons (coeff p 0) (Abs_poly (\<lambda>n. coeff p (Suc n)))"
4.385 -    by (rule poly_ext)
4.386 -       (simp add: Abs_poly_inverse Poly_Suc coeff coeff_pCons
4.387 -             split: nat.split)
4.388 +    by transfer
4.389 +      (simp add: Abs_poly_inverse almost_everywhere_zero_Suc fun_eq_iff split: nat.split)
4.390  qed
4.391
4.392  lemma pCons_induct [case_names 0 pCons, induct type: poly]:
4.393 @@ -208,52 +352,227 @@
4.394  qed
4.395
4.396
4.397 -subsection {* Recursion combinator for polynomials *}
4.398 +subsection {* List-style syntax for polynomials *}
4.399 +
4.400 +syntax
4.401 +  "_poly" :: "args \<Rightarrow> 'a poly"  ("[:(_):]")
4.402 +
4.403 +translations
4.404 +  "[:x, xs:]" == "CONST pCons x [:xs:]"
4.405 +  "[:x:]" == "CONST pCons x 0"
4.406 +  "[:x:]" <= "CONST pCons x (_constrain 0 t)"
4.407 +
4.408 +
4.409 +subsection {* Representation of polynomials by lists of coefficients *}
4.410 +
4.411 +primrec Poly :: "'a::zero list \<Rightarrow> 'a poly"
4.412 +where
4.413 +  "Poly [] = 0"
4.414 +| "Poly (a # as) = pCons a (Poly as)"
4.415 +
4.416 +lemma Poly_replicate_0 [simp]:
4.417 +  "Poly (replicate n 0) = 0"
4.418 +  by (induct n) simp_all
4.419 +
4.420 +lemma Poly_eq_0:
4.421 +  "Poly as = 0 \<longleftrightarrow> (\<exists>n. as = replicate n 0)"
4.422 +  by (induct as) (auto simp add: Cons_replicate_eq)
4.423 +
4.424 +definition coeffs :: "'a poly \<Rightarrow> 'a::zero list"
4.425 +where
4.426 +  "coeffs p = (if p = 0 then [] else map (\<lambda>i. coeff p i) [0 ..< Suc (degree p)])"
4.427 +
4.428 +lemma coeffs_eq_Nil [simp]:
4.429 +  "coeffs p = [] \<longleftrightarrow> p = 0"
4.430 +  by (simp add: coeffs_def)
4.431 +
4.432 +lemma not_0_coeffs_not_Nil:
4.433 +  "p \<noteq> 0 \<Longrightarrow> coeffs p \<noteq> []"
4.434 +  by simp
4.435 +
4.436 +lemma coeffs_0_eq_Nil [simp]:
4.437 +  "coeffs 0 = []"
4.438 +  by simp
4.439
4.440 -function
4.441 -  poly_rec :: "'b \<Rightarrow> ('a::zero \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b"
4.442 -where
4.443 -  poly_rec_pCons_eq_if [simp del]:
4.444 -    "poly_rec z f (pCons a p) = f a p (if p = 0 then z else poly_rec z f p)"
4.445 -by (case_tac x, rename_tac q, case_tac q, auto)
4.446 +lemma coeffs_pCons_eq_cCons [simp]:
4.447 +  "coeffs (pCons a p) = a ## coeffs p"
4.448 +proof -
4.449 +  { fix ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a"
4.450 +    assume "\<forall>m\<in>set ms. m > 0"
4.451 +    then have "map (nat_case x f) ms = map f (map (\<lambda>n. n - 1) ms)"
4.452 +      by (induct ms) (auto, metis Suc_pred' nat_case_Suc) }
4.453 +  note * = this
4.454 +  show ?thesis
4.455 +    by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt One_nat_def del: upt_Suc)
4.456 +qed
4.457 +
4.458 +lemma not_0_cCons_eq [simp]:
4.459 +  "p \<noteq> 0 \<Longrightarrow> a ## coeffs p = a # coeffs p"
4.460 +  by (simp add: cCons_def)
4.461 +
4.462 +lemma Poly_coeffs [simp, code abstype]:
4.463 +  "Poly (coeffs p) = p"
4.464 +  by (induct p) (simp_all add: cCons_def)
4.465 +
4.466 +lemma coeffs_Poly [simp]:
4.467 +  "coeffs (Poly as) = strip_while (HOL.eq 0) as"
4.468 +proof (induct as)
4.469 +  case Nil then show ?case by simp
4.470 +next
4.471 +  case (Cons a as)
4.472 +  have "(\<forall>n. as \<noteq> replicate n 0) \<longleftrightarrow> (\<exists>a\<in>set as. a \<noteq> 0)"
4.473 +    using replicate_length_same [of as 0] by (auto dest: sym [of _ as])
4.474 +  with Cons show ?case by auto
4.475 +qed
4.476 +
4.477 +lemma last_coeffs_not_0:
4.478 +  "p \<noteq> 0 \<Longrightarrow> last (coeffs p) \<noteq> 0"
4.479 +  by (induct p) (auto simp add: cCons_def)
4.480 +
4.481 +lemma strip_while_coeffs [simp]:
4.482 +  "strip_while (HOL.eq 0) (coeffs p) = coeffs p"
4.483 +  by (cases "p = 0") (auto dest: last_coeffs_not_0 intro: strip_while_not_last)
4.484 +
4.485 +lemma coeffs_eq_iff:
4.486 +  "p = q \<longleftrightarrow> coeffs p = coeffs q" (is "?P \<longleftrightarrow> ?Q")
4.487 +proof
4.488 +  assume ?P then show ?Q by simp
4.489 +next
4.490 +  assume ?Q
4.491 +  then have "Poly (coeffs p) = Poly (coeffs q)" by simp
4.492 +  then show ?P by simp
4.493 +qed
4.494 +
4.495 +lemma coeff_Poly_eq:
4.496 +  "coeff (Poly xs) n = nth_default 0 xs n"
4.497 +  apply (induct xs arbitrary: n) apply simp_all
4.498 +  by (metis nat_case_0 nat_case_Suc not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
4.499
4.500 -termination poly_rec
4.501 -by (relation "measure (degree \<circ> snd \<circ> snd)", simp)
4.502 -   (simp add: degree_pCons_eq)
4.503 +lemma nth_default_coeffs_eq:
4.504 +  "nth_default 0 (coeffs p) = coeff p"
4.505 +  by (simp add: fun_eq_iff coeff_Poly_eq [symmetric])
4.506 +
4.507 +lemma [code]:
4.508 +  "coeff p = nth_default 0 (coeffs p)"
4.509 +  by (simp add: nth_default_coeffs_eq)
4.510 +
4.511 +lemma coeffs_eqI:
4.512 +  assumes coeff: "\<And>n. coeff p n = nth_default 0 xs n"
4.513 +  assumes zero: "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0"
4.514 +  shows "coeffs p = xs"
4.515 +proof -
4.516 +  from coeff have "p = Poly xs" by (simp add: poly_eq_iff coeff_Poly_eq)
4.517 +  with zero show ?thesis by simp (cases xs, simp_all)
4.518 +qed
4.519 +
4.520 +lemma degree_eq_length_coeffs [code]:
4.521 +  "degree p = length (coeffs p) - 1"
4.522 +  by (simp add: coeffs_def)
4.523 +
4.524 +lemma length_coeffs_degree:
4.525 +  "p \<noteq> 0 \<Longrightarrow> length (coeffs p) = Suc (degree p)"
4.526 +  by (induct p) (auto simp add: cCons_def)
4.527 +
4.528 +lemma [code abstract]:
4.529 +  "coeffs 0 = []"
4.530 +  by (fact coeffs_0_eq_Nil)
4.531 +
4.532 +lemma [code abstract]:
4.533 +  "coeffs (pCons a p) = a ## coeffs p"
4.534 +  by (fact coeffs_pCons_eq_cCons)
4.535 +
4.536 +instantiation poly :: ("{zero, equal}") equal
4.537 +begin
4.538 +
4.539 +definition
4.540 +  [code]: "HOL.equal (p::'a poly) q \<longleftrightarrow> HOL.equal (coeffs p) (coeffs q)"
4.541 +
4.542 +instance proof
4.543 +qed (simp add: equal equal_poly_def coeffs_eq_iff)
4.544 +
4.545 +end
4.546 +
4.547 +lemma [code nbe]:
4.548 +  "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
4.549 +  by (fact equal_refl)
4.550
4.551 -lemma poly_rec_0:
4.552 -  "f 0 0 z = z \<Longrightarrow> poly_rec z f 0 = z"
4.553 -  using poly_rec_pCons_eq_if [of z f 0 0] by simp
4.554 +definition is_zero :: "'a::zero poly \<Rightarrow> bool"
4.555 +where
4.556 +  [code]: "is_zero p \<longleftrightarrow> List.null (coeffs p)"
4.557 +
4.558 +lemma is_zero_null [code_abbrev]:
4.559 +  "is_zero p \<longleftrightarrow> p = 0"
4.560 +  by (simp add: is_zero_def null_def)
4.561 +
4.562 +
4.563 +subsection {* Fold combinator for polynomials *}
4.564 +
4.565 +definition fold_coeffs :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b"
4.566 +where
4.567 +  "fold_coeffs f p = foldr f (coeffs p)"
4.568 +
4.569 +lemma fold_coeffs_0_eq [simp]:
4.570 +  "fold_coeffs f 0 = id"
4.571 +  by (simp add: fold_coeffs_def)
4.572 +
4.573 +lemma fold_coeffs_pCons_eq [simp]:
4.574 +  "f 0 = id \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
4.575 +  by (simp add: fold_coeffs_def cCons_def fun_eq_iff)
4.576
4.577 -lemma poly_rec_pCons:
4.578 -  "f 0 0 z = z \<Longrightarrow> poly_rec z f (pCons a p) = f a p (poly_rec z f p)"
4.579 -  by (simp add: poly_rec_pCons_eq_if poly_rec_0)
4.580 +lemma fold_coeffs_pCons_0_0_eq [simp]:
4.581 +  "fold_coeffs f (pCons 0 0) = id"
4.582 +  by (simp add: fold_coeffs_def)
4.583 +
4.584 +lemma fold_coeffs_pCons_coeff_not_0_eq [simp]:
4.585 +  "a \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
4.586 +  by (simp add: fold_coeffs_def)
4.587 +
4.588 +lemma fold_coeffs_pCons_not_0_0_eq [simp]:
4.589 +  "p \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
4.590 +  by (simp add: fold_coeffs_def)
4.591 +
4.592 +
4.593 +subsection {* Canonical morphism on polynomials -- evaluation *}
4.594 +
4.595 +definition poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a"
4.596 +where
4.597 +  "poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)" -- {* The Horner Schema *}
4.598 +
4.599 +lemma poly_0 [simp]:
4.600 +  "poly 0 x = 0"
4.601 +  by (simp add: poly_def)
4.602 +
4.603 +lemma poly_pCons [simp]:
4.604 +  "poly (pCons a p) x = a + x * poly p x"
4.605 +  by (cases "p = 0 \<and> a = 0") (auto simp add: poly_def)
4.606
4.607
4.608  subsection {* Monomials *}
4.609
4.610 -definition
4.611 -  monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly" where
4.612 -  "monom a m = Abs_poly (\<lambda>n. if m = n then a else 0)"
4.613 +lift_definition monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly"
4.614 +  is "\<lambda>a m n. if m = n then a else 0"
4.615 +  by (auto intro!: almost_everywhere_zeroI)
4.616 +
4.617 +lemma coeff_monom [simp]:
4.618 +  "coeff (monom a m) n = (if m = n then a else 0)"
4.619 +  by transfer rule
4.620
4.621 -lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
4.622 -  unfolding monom_def
4.623 -  by (subst Abs_poly_inverse, auto simp add: Poly_def)
4.624 +lemma monom_0:
4.625 +  "monom a 0 = pCons a 0"
4.626 +  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
4.627
4.628 -lemma monom_0: "monom a 0 = pCons a 0"
4.629 -  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
4.630 -
4.631 -lemma monom_Suc: "monom a (Suc n) = pCons 0 (monom a n)"
4.632 -  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
4.633 +lemma monom_Suc:
4.634 +  "monom a (Suc n) = pCons 0 (monom a n)"
4.635 +  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
4.636
4.637  lemma monom_eq_0 [simp]: "monom 0 n = 0"
4.638 -  by (rule poly_ext) simp
4.639 +  by (rule poly_eqI) simp
4.640
4.641  lemma monom_eq_0_iff [simp]: "monom a n = 0 \<longleftrightarrow> a = 0"
4.642 -  by (simp add: expand_poly_eq)
4.643 +  by (simp add: poly_eq_iff)
4.644
4.645  lemma monom_eq_iff [simp]: "monom a n = monom b n \<longleftrightarrow> a = b"
4.646 -  by (simp add: expand_poly_eq)
4.647 +  by (simp add: poly_eq_iff)
4.648
4.649  lemma degree_monom_le: "degree (monom a n) \<le> n"
4.650    by (rule degree_le, simp)
4.651 @@ -263,37 +582,47 @@
4.652    apply (rule le_degree, simp)
4.653    done
4.654
4.655 +lemma coeffs_monom [code abstract]:
4.656 +  "coeffs (monom a n) = (if a = 0 then [] else replicate n 0 @ [a])"
4.657 +  by (induct n) (simp_all add: monom_0 monom_Suc)
4.658 +
4.659 +lemma fold_coeffs_monom [simp]:
4.660 +  "a \<noteq> 0 \<Longrightarrow> fold_coeffs f (monom a n) = f 0 ^^ n \<circ> f a"
4.661 +  by (simp add: fold_coeffs_def coeffs_monom fun_eq_iff)
4.662 +
4.663 +lemma poly_monom:
4.664 +  fixes a x :: "'a::{comm_semiring_1}"
4.665 +  shows "poly (monom a n) x = a * x ^ n"
4.666 +  by (cases "a = 0", simp_all)
4.667 +    (induct n, simp_all add: mult.left_commute poly_def)
4.668 +
4.669
4.670  subsection {* Addition and subtraction *}
4.671
4.673  begin
4.674
4.675 -definition
4.676 -  plus_poly_def:
4.677 -    "p + q = Abs_poly (\<lambda>n. coeff p n + coeff q n)"
4.678 -
4.680 -  fixes f g :: "nat \<Rightarrow> 'a"
4.681 -  shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. f n + g n) \<in> Poly"
4.682 -  unfolding Poly_def
4.683 -  apply (clarify, rename_tac m n)
4.684 -  apply (rule_tac x="max m n" in exI, simp)
4.685 -  done
4.686 +lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
4.687 +  is "\<lambda>p q n. coeff p n + coeff q n"
4.688 +proof (rule almost_everywhere_zeroI)
4.689 +  fix q p :: "'a poly" and i
4.690 +  assume "max (degree q) (degree p) < i"
4.691 +  then show "coeff p i + coeff q i = 0"
4.692 +    by (simp add: coeff_eq_0)
4.693 +qed
4.694
4.695  lemma coeff_add [simp]:
4.696    "coeff (p + q) n = coeff p n + coeff q n"
4.697 -  unfolding plus_poly_def
4.698 -  by (simp add: Abs_poly_inverse coeff Poly_add)
4.699 +  by (simp add: plus_poly.rep_eq)
4.700
4.701  instance proof
4.702    fix p q r :: "'a poly"
4.703    show "(p + q) + r = p + (q + r)"
4.704 -    by (simp add: expand_poly_eq add_assoc)
4.705 +    by (simp add: poly_eq_iff add_assoc)
4.706    show "p + q = q + p"
4.707 -    by (simp add: expand_poly_eq add_commute)
4.708 +    by (simp add: poly_eq_iff add_commute)
4.709    show "0 + p = p"
4.710 -    by (simp add: expand_poly_eq)
4.711 +    by (simp add: poly_eq_iff)
4.712  qed
4.713
4.714  end
4.715 @@ -302,60 +631,58 @@
4.716  proof
4.717    fix p q r :: "'a poly"
4.718    assume "p + q = p + r" thus "q = r"
4.719 -    by (simp add: expand_poly_eq)
4.720 +    by (simp add: poly_eq_iff)
4.721  qed
4.722
4.724  begin
4.725
4.726 -definition
4.727 -  uminus_poly_def:
4.728 -    "- p = Abs_poly (\<lambda>n. - coeff p n)"
4.729 -
4.730 -definition
4.731 -  minus_poly_def:
4.732 -    "p - q = Abs_poly (\<lambda>n. coeff p n - coeff q n)"
4.733 +lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly"
4.734 +  is "\<lambda>p n. - coeff p n"
4.735 +proof (rule almost_everywhere_zeroI)
4.736 +  fix p :: "'a poly" and i
4.737 +  assume "degree p < i"
4.738 +  then show "- coeff p i = 0"
4.739 +    by (simp add: coeff_eq_0)
4.740 +qed
4.741
4.742 -lemma Poly_minus:
4.743 -  fixes f :: "nat \<Rightarrow> 'a"
4.744 -  shows "f \<in> Poly \<Longrightarrow> (\<lambda>n. - f n) \<in> Poly"
4.745 -  unfolding Poly_def by simp
4.746 -
4.747 -lemma Poly_diff:
4.748 -  fixes f g :: "nat \<Rightarrow> 'a"
4.749 -  shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. f n - g n) \<in> Poly"
4.750 -  unfolding diff_minus by (simp add: Poly_add Poly_minus)
4.751 +lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
4.752 +  is "\<lambda>p q n. coeff p n - coeff q n"
4.753 +proof (rule almost_everywhere_zeroI)
4.754 +  fix q p :: "'a poly" and i
4.755 +  assume "max (degree q) (degree p) < i"
4.756 +  then show "coeff p i - coeff q i = 0"
4.757 +    by (simp add: coeff_eq_0)
4.758 +qed
4.759
4.760  lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
4.761 -  unfolding uminus_poly_def
4.762 -  by (simp add: Abs_poly_inverse coeff Poly_minus)
4.763 +  by (simp add: uminus_poly.rep_eq)
4.764
4.765  lemma coeff_diff [simp]:
4.766    "coeff (p - q) n = coeff p n - coeff q n"
4.767 -  unfolding minus_poly_def
4.768 -  by (simp add: Abs_poly_inverse coeff Poly_diff)
4.769 +  by (simp add: minus_poly.rep_eq)
4.770
4.771  instance proof
4.772    fix p q :: "'a poly"
4.773    show "- p + p = 0"
4.774 -    by (simp add: expand_poly_eq)
4.775 +    by (simp add: poly_eq_iff)
4.776    show "p - q = p + - q"
4.777 -    by (simp add: expand_poly_eq diff_minus)
4.778 +    by (simp add: poly_eq_iff diff_minus)
4.779  qed
4.780
4.781  end
4.782
4.783  lemma add_pCons [simp]:
4.784    "pCons a p + pCons b q = pCons (a + b) (p + q)"
4.785 -  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
4.786 +  by (rule poly_eqI, simp add: coeff_pCons split: nat.split)
4.787
4.788  lemma minus_pCons [simp]:
4.789    "- pCons a p = pCons (- a) (- p)"
4.790 -  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
4.791 +  by (rule poly_eqI, simp add: coeff_pCons split: nat.split)
4.792
4.793  lemma diff_pCons [simp]:
4.794    "pCons a p - pCons b q = pCons (a - b) (p - q)"
4.795 -  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
4.796 +  by (rule poly_eqI, simp add: coeff_pCons split: nat.split)
4.797
4.798  lemma degree_add_le_max: "degree (p + q) \<le> max (degree p) (degree q)"
4.799    by (rule degree_le, auto simp add: coeff_eq_0)
4.800 @@ -398,75 +725,133 @@
4.802
4.803  lemma add_monom: "monom a n + monom b n = monom (a + b) n"
4.804 -  by (rule poly_ext) simp
4.805 +  by (rule poly_eqI) simp
4.806
4.807  lemma diff_monom: "monom a n - monom b n = monom (a - b) n"
4.808 -  by (rule poly_ext) simp
4.809 +  by (rule poly_eqI) simp
4.810
4.811  lemma minus_monom: "- monom a n = monom (-a) n"
4.812 -  by (rule poly_ext) simp
4.813 +  by (rule poly_eqI) simp
4.814
4.815  lemma coeff_setsum: "coeff (\<Sum>x\<in>A. p x) i = (\<Sum>x\<in>A. coeff (p x) i)"
4.816    by (cases "finite A", induct set: finite, simp_all)
4.817
4.818  lemma monom_setsum: "monom (\<Sum>x\<in>A. a x) n = (\<Sum>x\<in>A. monom (a x) n)"
4.819 -  by (rule poly_ext) (simp add: coeff_setsum)
4.820 +  by (rule poly_eqI) (simp add: coeff_setsum)
4.821 +
4.822 +fun plus_coeffs :: "'a::comm_monoid_add list \<Rightarrow> 'a list \<Rightarrow> 'a list"
4.823 +where
4.824 +  "plus_coeffs xs [] = xs"
4.825 +| "plus_coeffs [] ys = ys"
4.826 +| "plus_coeffs (x # xs) (y # ys) = (x + y) ## plus_coeffs xs ys"
4.827 +
4.828 +lemma coeffs_plus_eq_plus_coeffs [code abstract]:
4.829 +  "coeffs (p + q) = plus_coeffs (coeffs p) (coeffs q)"
4.830 +proof -
4.831 +  { fix xs ys :: "'a list" and n
4.832 +    have "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n"
4.833 +    proof (induct xs ys arbitrary: n rule: plus_coeffs.induct)
4.834 +      case (3 x xs y ys n) then show ?case by (cases n) (auto simp add: cCons_def)
4.835 +    qed simp_all }
4.836 +  note * = this
4.837 +  { fix xs ys :: "'a list"
4.838 +    assume "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0" and "ys \<noteq> [] \<Longrightarrow> last ys \<noteq> 0"
4.839 +    moreover assume "plus_coeffs xs ys \<noteq> []"
4.840 +    ultimately have "last (plus_coeffs xs ys) \<noteq> 0"
4.841 +    proof (induct xs ys rule: plus_coeffs.induct)
4.842 +      case (3 x xs y ys) then show ?case by (auto simp add: cCons_def) metis
4.843 +    qed simp_all }
4.844 +  note ** = this
4.845 +  show ?thesis
4.846 +    apply (rule coeffs_eqI)
4.847 +    apply (simp add: * nth_default_coeffs_eq)
4.848 +    apply (rule **)
4.849 +    apply (auto dest: last_coeffs_not_0)
4.850 +    done
4.851 +qed
4.852 +
4.853 +lemma coeffs_uminus [code abstract]:
4.854 +  "coeffs (- p) = map (\<lambda>a. - a) (coeffs p)"
4.855 +  by (rule coeffs_eqI)
4.856 +    (simp_all add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq)
4.857 +
4.858 +lemma [code]:
4.859 +  fixes p q :: "'a::ab_group_add poly"
4.860 +  shows "p - q = p + - q"
4.861 +  by simp
4.862 +
4.863 +lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
4.864 +  apply (induct p arbitrary: q, simp)
4.865 +  apply (case_tac q, simp, simp add: algebra_simps)
4.866 +  done
4.867 +
4.868 +lemma poly_minus [simp]:
4.869 +  fixes x :: "'a::comm_ring"
4.870 +  shows "poly (- p) x = - poly p x"
4.871 +  by (induct p) simp_all
4.872 +
4.873 +lemma poly_diff [simp]:
4.874 +  fixes x :: "'a::comm_ring"
4.875 +  shows "poly (p - q) x = poly p x - poly q x"
4.876 +  by (simp add: diff_minus)
4.877 +
4.878 +lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
4.879 +  by (induct A rule: infinite_finite_induct) simp_all
4.880
4.881
4.882 -subsection {* Multiplication by a constant *}
4.883 -
4.884 -definition
4.885 -  smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
4.886 -  "smult a p = Abs_poly (\<lambda>n. a * coeff p n)"
4.887 +subsection {* Multiplication by a constant, polynomial multiplication and the unit polynomial *}
4.888
4.889 -lemma Poly_smult:
4.890 -  fixes f :: "nat \<Rightarrow> 'a::comm_semiring_0"
4.891 -  shows "f \<in> Poly \<Longrightarrow> (\<lambda>n. a * f n) \<in> Poly"
4.892 -  unfolding Poly_def
4.893 -  by (clarify, rule_tac x=n in exI, simp)
4.894 +lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
4.895 +  is "\<lambda>a p n. a * coeff p n"
4.896 +proof (rule almost_everywhere_zeroI)
4.897 +  fix a :: 'a and p :: "'a poly" and i
4.898 +  assume "degree p < i"
4.899 +  then show "a * coeff p i = 0"
4.900 +    by (simp add: coeff_eq_0)
4.901 +qed
4.902
4.903 -lemma coeff_smult [simp]: "coeff (smult a p) n = a * coeff p n"
4.904 -  unfolding smult_def
4.905 -  by (simp add: Abs_poly_inverse Poly_smult coeff)
4.906 +lemma coeff_smult [simp]:
4.907 +  "coeff (smult a p) n = a * coeff p n"
4.908 +  by (simp add: smult.rep_eq)
4.909
4.910  lemma degree_smult_le: "degree (smult a p) \<le> degree p"
4.911    by (rule degree_le, simp add: coeff_eq_0)
4.912
4.913  lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p"
4.914 -  by (rule poly_ext, simp add: mult_assoc)
4.915 +  by (rule poly_eqI, simp add: mult_assoc)
4.916
4.917  lemma smult_0_right [simp]: "smult a 0 = 0"
4.918 -  by (rule poly_ext, simp)
4.919 +  by (rule poly_eqI, simp)
4.920
4.921  lemma smult_0_left [simp]: "smult 0 p = 0"
4.922 -  by (rule poly_ext, simp)
4.923 +  by (rule poly_eqI, simp)
4.924
4.925  lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p"
4.926 -  by (rule poly_ext, simp)
4.927 +  by (rule poly_eqI, simp)
4.928
4.930    "smult a (p + q) = smult a p + smult a q"
4.931 -  by (rule poly_ext, simp add: algebra_simps)
4.932 +  by (rule poly_eqI, simp add: algebra_simps)
4.933
4.935    "smult (a + b) p = smult a p + smult b p"
4.936 -  by (rule poly_ext, simp add: algebra_simps)
4.937 +  by (rule poly_eqI, simp add: algebra_simps)
4.938
4.939  lemma smult_minus_right [simp]:
4.940    "smult (a::'a::comm_ring) (- p) = - smult a p"
4.941 -  by (rule poly_ext, simp)
4.942 +  by (rule poly_eqI, simp)
4.943
4.944  lemma smult_minus_left [simp]:
4.945    "smult (- a::'a::comm_ring) p = - smult a p"
4.946 -  by (rule poly_ext, simp)
4.947 +  by (rule poly_eqI, simp)
4.948
4.949  lemma smult_diff_right:
4.950    "smult (a::'a::comm_ring) (p - q) = smult a p - smult a q"
4.951 -  by (rule poly_ext, simp add: algebra_simps)
4.952 +  by (rule poly_eqI, simp add: algebra_simps)
4.953
4.954  lemma smult_diff_left:
4.955    "smult (a - b::'a::comm_ring) p = smult a p - smult b p"
4.956 -  by (rule poly_ext, simp add: algebra_simps)
4.957 +  by (rule poly_eqI, simp add: algebra_simps)
4.958
4.959  lemmas smult_distribs =
4.961 @@ -474,7 +859,7 @@
4.962
4.963  lemma smult_pCons [simp]:
4.964    "smult a (pCons b p) = pCons (a * b) (smult a p)"
4.965 -  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
4.966 +  by (rule poly_eqI, simp add: coeff_pCons split: nat.split)
4.967
4.968  lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
4.969    by (induct n, simp add: monom_0, simp add: monom_Suc)
4.970 @@ -487,65 +872,48 @@
4.971  lemma smult_eq_0_iff [simp]:
4.972    fixes a :: "'a::idom"
4.973    shows "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0"
4.974 -  by (simp add: expand_poly_eq)
4.975 -
4.976 -
4.977 -subsection {* Multiplication of polynomials *}
4.978 +  by (simp add: poly_eq_iff)
4.979
4.980 -(* TODO: move to Set_Interval.thy *)
4.981 -lemma setsum_atMost_Suc_shift:
4.982 -  fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
4.983 -  shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
4.984 -proof (induct n)
4.985 -  case 0 show ?case by simp
4.986 -next
4.987 -  case (Suc n) note IH = this
4.988 -  have "(\<Sum>i\<le>Suc (Suc n). f i) = (\<Sum>i\<le>Suc n. f i) + f (Suc (Suc n))"
4.989 -    by (rule setsum_atMost_Suc)
4.990 -  also have "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
4.991 -    by (rule IH)
4.992 -  also have "f 0 + (\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) =
4.993 -             f 0 + ((\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)))"
4.994 -    by (rule add_assoc)
4.995 -  also have "(\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) = (\<Sum>i\<le>Suc n. f (Suc i))"
4.996 -    by (rule setsum_atMost_Suc [symmetric])
4.997 -  finally show ?case .
4.998 -qed
4.999 +lemma coeffs_smult [code abstract]:
4.1000 +  fixes p :: "'a::idom poly"
4.1001 +  shows "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))"
4.1002 +  by (rule coeffs_eqI)
4.1003 +    (auto simp add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq)
4.1004
4.1005  instantiation poly :: (comm_semiring_0) comm_semiring_0
4.1006  begin
4.1007
4.1008  definition
4.1009 -  times_poly_def:
4.1010 -    "p * q = poly_rec 0 (\<lambda>a p pq. smult a q + pCons 0 pq) p"
4.1011 +  "p * q = fold_coeffs (\<lambda>a p. smult a q + pCons 0 p) p 0"
4.1012
4.1013  lemma mult_poly_0_left: "(0::'a poly) * q = 0"
4.1014 -  unfolding times_poly_def by (simp add: poly_rec_0)
4.1015 +  by (simp add: times_poly_def)
4.1016
4.1017  lemma mult_pCons_left [simp]:
4.1018    "pCons a p * q = smult a q + pCons 0 (p * q)"
4.1019 -  unfolding times_poly_def by (simp add: poly_rec_pCons)
4.1020 +  by (cases "p = 0 \<and> a = 0") (auto simp add: times_poly_def)
4.1021
4.1022  lemma mult_poly_0_right: "p * (0::'a poly) = 0"
4.1023 -  by (induct p, simp add: mult_poly_0_left, simp)
4.1024 +  by (induct p) (simp add: mult_poly_0_left, simp)
4.1025
4.1026  lemma mult_pCons_right [simp]:
4.1027    "p * pCons a q = smult a p + pCons 0 (p * q)"
4.1028 -  by (induct p, simp add: mult_poly_0_left, simp add: algebra_simps)
4.1029 +  by (induct p) (simp add: mult_poly_0_left, simp add: algebra_simps)
4.1030
4.1031  lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right
4.1032
4.1033 -lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)"
4.1034 -  by (induct p, simp add: mult_poly_0, simp add: smult_add_right)
4.1035 +lemma mult_smult_left [simp]:
4.1036 +  "smult a p * q = smult a (p * q)"
4.1037 +  by (induct p) (simp add: mult_poly_0, simp add: smult_add_right)
4.1038
4.1039 -lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)"
4.1040 -  by (induct q, simp add: mult_poly_0, simp add: smult_add_right)
4.1041 +lemma mult_smult_right [simp]:
4.1042 +  "p * smult a q = smult a (p * q)"
4.1043 +  by (induct q) (simp add: mult_poly_0, simp add: smult_add_right)
4.1044
4.1046    fixes p q r :: "'a poly"
4.1047    shows "(p + q) * r = p * r + q * r"
4.1048 -  by (induct r, simp add: mult_poly_0,
4.1049 -                simp add: smult_distribs algebra_simps)
4.1050 +  by (induct r) (simp add: mult_poly_0, simp add: smult_distribs algebra_simps)
4.1051
4.1052  instance proof
4.1053    fix p q r :: "'a poly"
4.1054 @@ -585,20 +953,15 @@
4.1055  lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
4.1056    by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc)
4.1057
4.1058 -
4.1059 -subsection {* The unit polynomial and exponentiation *}
4.1060 -
4.1061  instantiation poly :: (comm_semiring_1) comm_semiring_1
4.1062  begin
4.1063
4.1064 -definition
4.1065 -  one_poly_def:
4.1066 -    "1 = pCons 1 0"
4.1067 +definition one_poly_def:
4.1068 +  "1 = pCons 1 0"
4.1069
4.1070  instance proof
4.1071    fix p :: "'a poly" show "1 * p = p"
4.1072 -    unfolding one_poly_def
4.1073 -    by simp
4.1074 +    unfolding one_poly_def by simp
4.1075  next
4.1076    show "0 \<noteq> (1::'a poly)"
4.1077      unfolding one_poly_def by simp
4.1078 @@ -608,6 +971,10 @@
4.1079
4.1080  instance poly :: (comm_semiring_1_cancel) comm_semiring_1_cancel ..
4.1081
4.1082 +instance poly :: (comm_ring) comm_ring ..
4.1083 +
4.1084 +instance poly :: (comm_ring_1) comm_ring_1 ..
4.1085 +
4.1086  lemma coeff_1 [simp]: "coeff 1 n = (if n = 0 then 1 else 0)"
4.1087    unfolding one_poly_def
4.1088    by (simp add: coeff_pCons split: nat.split)
4.1089 @@ -616,7 +983,33 @@
4.1090    unfolding one_poly_def
4.1091    by (rule degree_pCons_0)
4.1092
4.1093 -text {* Lemmas about divisibility *}
4.1094 +lemma coeffs_1_eq [simp, code abstract]:
4.1095 +  "coeffs 1 = "
4.1096 +  by (simp add: one_poly_def)
4.1097 +
4.1098 +lemma degree_power_le:
4.1099 +  "degree (p ^ n) \<le> degree p * n"
4.1100 +  by (induct n) (auto intro: order_trans degree_mult_le)
4.1101 +
4.1102 +lemma poly_smult [simp]:
4.1103 +  "poly (smult a p) x = a * poly p x"
4.1104 +  by (induct p, simp, simp add: algebra_simps)
4.1105 +
4.1106 +lemma poly_mult [simp]:
4.1107 +  "poly (p * q) x = poly p x * poly q x"
4.1108 +  by (induct p, simp_all, simp add: algebra_simps)
4.1109 +
4.1110 +lemma poly_1 [simp]:
4.1111 +  "poly 1 x = 1"
4.1112 +  by (simp add: one_poly_def)
4.1113 +
4.1114 +lemma poly_power [simp]:
4.1115 +  fixes p :: "'a::{comm_semiring_1} poly"
4.1116 +  shows "poly (p ^ n) x = poly p x ^ n"
4.1117 +  by (induct n) simp_all
4.1118 +
4.1119 +
4.1120 +subsection {* Lemmas about divisibility *}
4.1121
4.1122  lemma dvd_smult: "p dvd q \<Longrightarrow> p dvd smult a q"
4.1123  proof -
4.1124 @@ -655,13 +1048,6 @@
4.1125    shows "smult a p dvd q \<longleftrightarrow> (if a = 0 then q = 0 else p dvd q)"
4.1126    by (auto elim: smult_dvd smult_dvd_cancel)
4.1127
4.1128 -lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
4.1129 -by (induct n, simp, auto intro: order_trans degree_mult_le)
4.1130 -
4.1131 -instance poly :: (comm_ring) comm_ring ..
4.1132 -
4.1133 -instance poly :: (comm_ring_1) comm_ring_1 ..
4.1134 -
4.1135
4.1136  subsection {* Polynomials form an integral domain *}
4.1137
4.1138 @@ -680,7 +1066,7 @@
4.1139    also have "coeff p (degree p) * coeff q (degree q) \<noteq> 0"
4.1140      using `p \<noteq> 0` and `q \<noteq> 0` by simp
4.1141    finally have "\<exists>n. coeff (p * q) n \<noteq> 0" ..
4.1142 -  thus "p * q \<noteq> 0" by (simp add: expand_poly_eq)
4.1143 +  thus "p * q \<noteq> 0" by (simp add: poly_eq_iff)
4.1144  qed
4.1145
4.1146  lemma degree_mult_eq:
4.1147 @@ -698,8 +1084,7 @@
4.1148
4.1149  subsection {* Polynomials form an ordered integral domain *}
4.1150
4.1151 -definition
4.1152 -  pos_poly :: "'a::linordered_idom poly \<Rightarrow> bool"
4.1153 +definition pos_poly :: "'a::linordered_idom poly \<Rightarrow> bool"
4.1154  where
4.1155    "pos_poly p \<longleftrightarrow> 0 < coeff p (degree p)"
4.1156
4.1157 @@ -725,6 +1110,20 @@
4.1158  lemma pos_poly_total: "p = 0 \<or> pos_poly p \<or> pos_poly (- p)"
4.1159  by (induct p) (auto simp add: pos_poly_pCons)
4.1160
4.1161 +lemma last_coeffs_eq_coeff_degree:
4.1162 +  "p \<noteq> 0 \<Longrightarrow> last (coeffs p) = coeff p (degree p)"
4.1163 +  by (simp add: coeffs_def)
4.1164 +
4.1165 +lemma pos_poly_coeffs [code]:
4.1166 +  "pos_poly p \<longleftrightarrow> (let as = coeffs p in as \<noteq> [] \<and> last as > 0)" (is "?P \<longleftrightarrow> ?Q")
4.1167 +proof
4.1168 +  assume ?Q then show ?P by (auto simp add: pos_poly_def last_coeffs_eq_coeff_degree)
4.1169 +next
4.1170 +  assume ?P then have *: "0 < coeff p (degree p)" by (simp add: pos_poly_def)
4.1171 +  then have "p \<noteq> 0" by auto
4.1172 +  with * show ?Q by (simp add: last_coeffs_eq_coeff_degree)
4.1173 +qed
4.1174 +
4.1175  instantiation poly :: (linordered_idom) linordered_idom
4.1176  begin
4.1177
4.1178 @@ -802,10 +1201,145 @@
4.1179  text {* TODO: Simplification rules for comparisons *}
4.1180
4.1181
4.1182 +subsection {* Synthetic division and polynomial roots *}
4.1183 +
4.1184 +text {*
4.1185 +  Synthetic division is simply division by the linear polynomial @{term "x - c"}.
4.1186 +*}
4.1187 +
4.1188 +definition synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a"
4.1189 +where
4.1190 +  "synthetic_divmod p c = fold_coeffs (\<lambda>a (q, r). (pCons r q, a + c * r)) p (0, 0)"
4.1191 +
4.1192 +definition synthetic_div :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly"
4.1193 +where
4.1194 +  "synthetic_div p c = fst (synthetic_divmod p c)"
4.1195 +
4.1196 +lemma synthetic_divmod_0 [simp]:
4.1197 +  "synthetic_divmod 0 c = (0, 0)"
4.1198 +  by (simp add: synthetic_divmod_def)
4.1199 +
4.1200 +lemma synthetic_divmod_pCons [simp]:
4.1201 +  "synthetic_divmod (pCons a p) c = (\<lambda>(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)"
4.1202 +  by (cases "p = 0 \<and> a = 0") (auto simp add: synthetic_divmod_def)
4.1203 +
4.1204 +lemma synthetic_div_0 [simp]:
4.1205 +  "synthetic_div 0 c = 0"
4.1206 +  unfolding synthetic_div_def by simp
4.1207 +
4.1208 +lemma synthetic_div_unique_lemma: "smult c p = pCons a p \<Longrightarrow> p = 0"
4.1209 +by (induct p arbitrary: a) simp_all
4.1210 +
4.1211 +lemma snd_synthetic_divmod:
4.1212 +  "snd (synthetic_divmod p c) = poly p c"
4.1213 +  by (induct p, simp, simp add: split_def)
4.1214 +
4.1215 +lemma synthetic_div_pCons [simp]:
4.1216 +  "synthetic_div (pCons a p) c = pCons (poly p c) (synthetic_div p c)"
4.1217 +  unfolding synthetic_div_def
4.1218 +  by (simp add: split_def snd_synthetic_divmod)
4.1219 +
4.1220 +lemma synthetic_div_eq_0_iff:
4.1221 +  "synthetic_div p c = 0 \<longleftrightarrow> degree p = 0"
4.1222 +  by (induct p, simp, case_tac p, simp)
4.1223 +
4.1224 +lemma degree_synthetic_div:
4.1225 +  "degree (synthetic_div p c) = degree p - 1"
4.1226 +  by (induct p, simp, simp add: synthetic_div_eq_0_iff)
4.1227 +
4.1228 +lemma synthetic_div_correct:
4.1229 +  "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)"
4.1230 +  by (induct p) simp_all
4.1231 +
4.1232 +lemma synthetic_div_unique:
4.1233 +  "p + smult c q = pCons r q \<Longrightarrow> r = poly p c \<and> q = synthetic_div p c"
4.1234 +apply (induct p arbitrary: q r)
4.1235 +apply (simp, frule synthetic_div_unique_lemma, simp)
4.1236 +apply (case_tac q, force)
4.1237 +done
4.1238 +
4.1239 +lemma synthetic_div_correct':
4.1240 +  fixes c :: "'a::comm_ring_1"
4.1241 +  shows "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p"
4.1242 +  using synthetic_div_correct [of p c]
4.1243 +  by (simp add: algebra_simps)
4.1244 +
4.1245 +lemma poly_eq_0_iff_dvd:
4.1246 +  fixes c :: "'a::idom"
4.1247 +  shows "poly p c = 0 \<longleftrightarrow> [:-c, 1:] dvd p"
4.1248 +proof
4.1249 +  assume "poly p c = 0"
4.1250 +  with synthetic_div_correct' [of c p]
4.1251 +  have "p = [:-c, 1:] * synthetic_div p c" by simp
4.1252 +  then show "[:-c, 1:] dvd p" ..
4.1253 +next
4.1254 +  assume "[:-c, 1:] dvd p"
4.1255 +  then obtain k where "p = [:-c, 1:] * k" by (rule dvdE)
4.1256 +  then show "poly p c = 0" by simp
4.1257 +qed
4.1258 +
4.1259 +lemma dvd_iff_poly_eq_0:
4.1260 +  fixes c :: "'a::idom"
4.1261 +  shows "[:c, 1:] dvd p \<longleftrightarrow> poly p (-c) = 0"
4.1262 +  by (simp add: poly_eq_0_iff_dvd)
4.1263 +
4.1264 +lemma poly_roots_finite:
4.1265 +  fixes p :: "'a::idom poly"
4.1266 +  shows "p \<noteq> 0 \<Longrightarrow> finite {x. poly p x = 0}"
4.1267 +proof (induct n \<equiv> "degree p" arbitrary: p)
4.1268 +  case (0 p)
4.1269 +  then obtain a where "a \<noteq> 0" and "p = [:a:]"
4.1270 +    by (cases p, simp split: if_splits)
4.1271 +  then show "finite {x. poly p x = 0}" by simp
4.1272 +next
4.1273 +  case (Suc n p)
4.1274 +  show "finite {x. poly p x = 0}"
4.1275 +  proof (cases "\<exists>x. poly p x = 0")
4.1276 +    case False
4.1277 +    then show "finite {x. poly p x = 0}" by simp
4.1278 +  next
4.1279 +    case True
4.1280 +    then obtain a where "poly p a = 0" ..
4.1281 +    then have "[:-a, 1:] dvd p" by (simp only: poly_eq_0_iff_dvd)
4.1282 +    then obtain k where k: "p = [:-a, 1:] * k" ..
4.1283 +    with `p \<noteq> 0` have "k \<noteq> 0" by auto
4.1284 +    with k have "degree p = Suc (degree k)"
4.1285 +      by (simp add: degree_mult_eq del: mult_pCons_left)
4.1286 +    with `Suc n = degree p` have "n = degree k" by simp
4.1287 +    then have "finite {x. poly k x = 0}" using `k \<noteq> 0` by (rule Suc.hyps)
4.1288 +    then have "finite (insert a {x. poly k x = 0})" by simp
4.1289 +    then show "finite {x. poly p x = 0}"
4.1290 +      by (simp add: k uminus_add_conv_diff Collect_disj_eq
4.1291 +               del: mult_pCons_left)
4.1292 +  qed
4.1293 +qed
4.1294 +
4.1295 +lemma poly_eq_poly_eq_iff:
4.1296 +  fixes p q :: "'a::{idom,ring_char_0} poly"
4.1297 +  shows "poly p = poly q \<longleftrightarrow> p = q" (is "?P \<longleftrightarrow> ?Q")
4.1298 +proof
4.1299 +  assume ?Q then show ?P by simp
4.1300 +next
4.1301 +  { fix p :: "'a::{idom,ring_char_0} poly"
4.1302 +    have "poly p = poly 0 \<longleftrightarrow> p = 0"
4.1303 +      apply (cases "p = 0", simp_all)
4.1304 +      apply (drule poly_roots_finite)
4.1305 +      apply (auto simp add: infinite_UNIV_char_0)
4.1306 +      done
4.1307 +  } note this [of "p - q"]
4.1308 +  moreover assume ?P
4.1309 +  ultimately show ?Q by auto
4.1310 +qed
4.1311 +
4.1312 +lemma poly_all_0_iff_0:
4.1313 +  fixes p :: "'a::{ring_char_0, idom} poly"
4.1314 +  shows "(\<forall>x. poly p x = 0) \<longleftrightarrow> p = 0"
4.1315 +  by (auto simp add: poly_eq_poly_eq_iff [symmetric])
4.1316 +
4.1317 +
4.1318  subsection {* Long division of polynomials *}
4.1319
4.1320 -definition
4.1321 -  pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
4.1322 +definition pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
4.1323  where
4.1324    "pdivmod_rel x y q r \<longleftrightarrow>
4.1325      x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
4.1326 @@ -1106,327 +1640,54 @@
4.1327  apply (rule pdivmod_rel_pCons [OF pdivmod_rel y refl])
4.1328  done
4.1329
4.1330 -
4.1331 -subsection {* GCD of polynomials *}
4.1332 -
4.1333 -function
4.1334 -  poly_gcd :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
4.1335 -  "poly_gcd x 0 = smult (inverse (coeff x (degree x))) x"
4.1336 -| "y \<noteq> 0 \<Longrightarrow> poly_gcd x y = poly_gcd y (x mod y)"
4.1337 -by auto
4.1338 -
4.1339 -termination poly_gcd
4.1340 -by (relation "measure (\<lambda>(x, y). if y = 0 then 0 else Suc (degree y))")
4.1341 -   (auto dest: degree_mod_less)
4.1342 -
4.1343 -declare poly_gcd.simps [simp del]
4.1344 -
4.1345 -lemma poly_gcd_dvd1 [iff]: "poly_gcd x y dvd x"
4.1346 -  and poly_gcd_dvd2 [iff]: "poly_gcd x y dvd y"
4.1347 -  apply (induct x y rule: poly_gcd.induct)
4.1348 -  apply (simp_all add: poly_gcd.simps)
4.1349 -  apply (fastforce simp add: smult_dvd_iff dest: inverse_zero_imp_zero)
4.1350 -  apply (blast dest: dvd_mod_imp_dvd)
4.1351 -  done
4.1352 -
4.1353 -lemma poly_gcd_greatest: "k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd poly_gcd x y"
4.1354 -  by (induct x y rule: poly_gcd.induct)
4.1355 -     (simp_all add: poly_gcd.simps dvd_mod dvd_smult)
4.1356 -
4.1357 -lemma dvd_poly_gcd_iff [iff]:
4.1358 -  "k dvd poly_gcd x y \<longleftrightarrow> k dvd x \<and> k dvd y"
4.1359 -  by (blast intro!: poly_gcd_greatest intro: dvd_trans)
4.1360 +definition pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
4.1361 +where
4.1362 +  "pdivmod p q = (p div q, p mod q)"
4.1363
4.1364 -lemma poly_gcd_monic:
4.1365 -  "coeff (poly_gcd x y) (degree (poly_gcd x y)) =
4.1366 -    (if x = 0 \<and> y = 0 then 0 else 1)"
4.1367 -  by (induct x y rule: poly_gcd.induct)
4.1368 -     (simp_all add: poly_gcd.simps nonzero_imp_inverse_nonzero)
4.1369 -
4.1370 -lemma poly_gcd_zero_iff [simp]:
4.1371 -  "poly_gcd x y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
4.1372 -  by (simp only: dvd_0_left_iff [symmetric] dvd_poly_gcd_iff)
4.1373 -
4.1374 -lemma poly_gcd_0_0 [simp]: "poly_gcd 0 0 = 0"
4.1375 -  by simp
4.1376 +lemma div_poly_code [code]:
4.1377 +  "p div q = fst (pdivmod p q)"
4.1378 +  by (simp add: pdivmod_def)
4.1379
4.1380 -lemma poly_dvd_antisym:
4.1381 -  fixes p q :: "'a::idom poly"
4.1382 -  assumes coeff: "coeff p (degree p) = coeff q (degree q)"
4.1383 -  assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q"
4.1384 -proof (cases "p = 0")
4.1385 -  case True with coeff show "p = q" by simp
4.1386 -next
4.1387 -  case False with coeff have "q \<noteq> 0" by auto
4.1388 -  have degree: "degree p = degree q"
4.1389 -    using `p dvd q` `q dvd p` `p \<noteq> 0` `q \<noteq> 0`
4.1390 -    by (intro order_antisym dvd_imp_degree_le)
4.1391 -
4.1392 -  from `p dvd q` obtain a where a: "q = p * a" ..
4.1393 -  with `q \<noteq> 0` have "a \<noteq> 0" by auto
4.1394 -  with degree a `p \<noteq> 0` have "degree a = 0"
4.1395 -    by (simp add: degree_mult_eq)
4.1396 -  with coeff a show "p = q"
4.1397 -    by (cases a, auto split: if_splits)
4.1398 -qed
4.1399 +lemma mod_poly_code [code]:
4.1400 +  "p mod q = snd (pdivmod p q)"
4.1401 +  by (simp add: pdivmod_def)
4.1402
4.1403 -lemma poly_gcd_unique:
4.1404 -  assumes dvd1: "d dvd x" and dvd2: "d dvd y"
4.1405 -    and greatest: "\<And>k. k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd d"
4.1406 -    and monic: "coeff d (degree d) = (if x = 0 \<and> y = 0 then 0 else 1)"
4.1407 -  shows "poly_gcd x y = d"
4.1408 -proof -
4.1409 -  have "coeff (poly_gcd x y) (degree (poly_gcd x y)) = coeff d (degree d)"
4.1410 -    by (simp_all add: poly_gcd_monic monic)
4.1411 -  moreover have "poly_gcd x y dvd d"
4.1412 -    using poly_gcd_dvd1 poly_gcd_dvd2 by (rule greatest)
4.1413 -  moreover have "d dvd poly_gcd x y"
4.1414 -    using dvd1 dvd2 by (rule poly_gcd_greatest)
4.1415 -  ultimately show ?thesis
4.1416 -    by (rule poly_dvd_antisym)
4.1417 -qed
4.1418 -
4.1419 -interpretation poly_gcd: abel_semigroup poly_gcd
4.1420 -proof
4.1421 -  fix x y z :: "'a poly"
4.1422 -  show "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
4.1423 -    by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
4.1424 -  show "poly_gcd x y = poly_gcd y x"
4.1425 -    by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
4.1426 -qed
4.1427 -
4.1428 -lemmas poly_gcd_assoc = poly_gcd.assoc
4.1429 -lemmas poly_gcd_commute = poly_gcd.commute
4.1430 -lemmas poly_gcd_left_commute = poly_gcd.left_commute
4.1431 -
4.1432 -lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute
4.1433 -
4.1434 -lemma poly_gcd_1_left [simp]: "poly_gcd 1 y = 1"
4.1435 -by (rule poly_gcd_unique) simp_all
4.1436 +lemma pdivmod_0:
4.1437 +  "pdivmod 0 q = (0, 0)"
4.1438 +  by (simp add: pdivmod_def)
4.1439
4.1440 -lemma poly_gcd_1_right [simp]: "poly_gcd x 1 = 1"
4.1441 -by (rule poly_gcd_unique) simp_all
4.1442 -
4.1443 -lemma poly_gcd_minus_left [simp]: "poly_gcd (- x) y = poly_gcd x y"
4.1444 -by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
4.1445 -
4.1446 -lemma poly_gcd_minus_right [simp]: "poly_gcd x (- y) = poly_gcd x y"
4.1447 -by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
4.1448 -
4.1449 -
4.1450 -subsection {* Evaluation of polynomials *}
4.1451 -
4.1452 -definition
4.1453 -  poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a" where
4.1454 -  "poly = poly_rec (\<lambda>x. 0) (\<lambda>a p f x. a + x * f x)"
4.1455 -
4.1456 -lemma poly_0 [simp]: "poly 0 x = 0"
4.1457 -  unfolding poly_def by (simp add: poly_rec_0)
4.1458 -
4.1459 -lemma poly_pCons [simp]: "poly (pCons a p) x = a + x * poly p x"
4.1460 -  unfolding poly_def by (simp add: poly_rec_pCons)
4.1461 -
4.1462 -lemma poly_1 [simp]: "poly 1 x = 1"
4.1463 -  unfolding one_poly_def by simp
4.1464 -
4.1465 -lemma poly_monom:
4.1466 -  fixes a x :: "'a::{comm_semiring_1}"
4.1467 -  shows "poly (monom a n) x = a * x ^ n"
4.1468 -  by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac)
4.1469 -
4.1470 -lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
4.1471 -  apply (induct p arbitrary: q, simp)
4.1472 -  apply (case_tac q, simp, simp add: algebra_simps)
4.1473 +lemma pdivmod_pCons:
4.1474 +  "pdivmod (pCons a p) q =
4.1475 +    (if q = 0 then (0, pCons a p) else
4.1476 +      (let (s, r) = pdivmod p q;
4.1477 +           b = coeff (pCons a r) (degree q) / coeff q (degree q)
4.1478 +        in (pCons b s, pCons a r - smult b q)))"
4.1479 +  apply (simp add: pdivmod_def Let_def, safe)
4.1480 +  apply (rule div_poly_eq)
4.1481 +  apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
4.1482 +  apply (rule mod_poly_eq)
4.1483 +  apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
4.1484    done
4.1485
4.1486 -lemma poly_minus [simp]:
4.1487 -  fixes x :: "'a::comm_ring"
4.1488 -  shows "poly (- p) x = - poly p x"
4.1489 -  by (induct p, simp_all)
4.1490 -
4.1491 -lemma poly_diff [simp]:
4.1492 -  fixes x :: "'a::comm_ring"
4.1493 -  shows "poly (p - q) x = poly p x - poly q x"
4.1494 -  by (simp add: diff_minus)
4.1495 -
4.1496 -lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
4.1497 -  by (cases "finite A", induct set: finite, simp_all)
4.1498 -
4.1499 -lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x"
4.1500 -  by (induct p, simp, simp add: algebra_simps)
4.1501 -
4.1502 -lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x"
4.1503 -  by (induct p, simp_all, simp add: algebra_simps)
4.1504 -
4.1505 -lemma poly_power [simp]:
4.1506 -  fixes p :: "'a::{comm_semiring_1} poly"
4.1507 -  shows "poly (p ^ n) x = poly p x ^ n"
4.1508 -  by (induct n, simp, simp add: power_Suc)
4.1509 -
4.1510 -
4.1511 -subsection {* Synthetic division *}
4.1512 -
4.1513 -text {*
4.1514 -  Synthetic division is simply division by the
4.1515 -  linear polynomial @{term "x - c"}.
4.1516 -*}
4.1517 -
4.1518 -definition
4.1519 -  synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a"
4.1520 -where
4.1521 -  "synthetic_divmod p c =
4.1522 -    poly_rec (0, 0) (\<lambda>a p (q, r). (pCons r q, a + c * r)) p"
4.1523 -
4.1524 -definition
4.1525 -  synthetic_div :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly"
4.1526 -where
4.1527 -  "synthetic_div p c = fst (synthetic_divmod p c)"
4.1528 -
4.1529 -lemma synthetic_divmod_0 [simp]:
4.1530 -  "synthetic_divmod 0 c = (0, 0)"
4.1531 -  unfolding synthetic_divmod_def
4.1532 -  by (simp add: poly_rec_0)
4.1533 -
4.1534 -lemma synthetic_divmod_pCons [simp]:
4.1535 -  "synthetic_divmod (pCons a p) c =
4.1536 -    (\<lambda>(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)"
4.1537 -  unfolding synthetic_divmod_def
4.1538 -  by (simp add: poly_rec_pCons)
4.1539 -
4.1540 -lemma snd_synthetic_divmod: "snd (synthetic_divmod p c) = poly p c"
4.1541 -  by (induct p, simp, simp add: split_def)
4.1542 -
4.1543 -lemma synthetic_div_0 [simp]: "synthetic_div 0 c = 0"
4.1544 -  unfolding synthetic_div_def by simp
4.1545 -
4.1546 -lemma synthetic_div_pCons [simp]:
4.1547 -  "synthetic_div (pCons a p) c = pCons (poly p c) (synthetic_div p c)"
4.1548 -  unfolding synthetic_div_def
4.1549 -  by (simp add: split_def snd_synthetic_divmod)
4.1550 -
4.1551 -lemma synthetic_div_eq_0_iff:
4.1552 -  "synthetic_div p c = 0 \<longleftrightarrow> degree p = 0"
4.1553 -  by (induct p, simp, case_tac p, simp)
4.1554 -
4.1555 -lemma degree_synthetic_div:
4.1556 -  "degree (synthetic_div p c) = degree p - 1"
4.1557 -  by (induct p, simp, simp add: synthetic_div_eq_0_iff)
4.1558 -
4.1559 -lemma synthetic_div_correct:
4.1560 -  "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)"
4.1561 -  by (induct p) simp_all
4.1562 -
4.1563 -lemma synthetic_div_unique_lemma: "smult c p = pCons a p \<Longrightarrow> p = 0"
4.1564 -by (induct p arbitrary: a) simp_all
4.1565 -
4.1566 -lemma synthetic_div_unique:
4.1567 -  "p + smult c q = pCons r q \<Longrightarrow> r = poly p c \<and> q = synthetic_div p c"
4.1568 -apply (induct p arbitrary: q r)
4.1569 -apply (simp, frule synthetic_div_unique_lemma, simp)
4.1570 -apply (case_tac q, force)
4.1571 -done
4.1572 -
4.1573 -lemma synthetic_div_correct':
4.1574 -  fixes c :: "'a::comm_ring_1"
4.1575 -  shows "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p"
4.1576 -  using synthetic_div_correct [of p c]
4.1577 -  by (simp add: algebra_simps)
4.1578 -
4.1579 -lemma poly_eq_0_iff_dvd:
4.1580 -  fixes c :: "'a::idom"
4.1581 -  shows "poly p c = 0 \<longleftrightarrow> [:-c, 1:] dvd p"
4.1582 -proof
4.1583 -  assume "poly p c = 0"
4.1584 -  with synthetic_div_correct' [of c p]
4.1585 -  have "p = [:-c, 1:] * synthetic_div p c" by simp
4.1586 -  then show "[:-c, 1:] dvd p" ..
4.1587 -next
4.1588 -  assume "[:-c, 1:] dvd p"
4.1589 -  then obtain k where "p = [:-c, 1:] * k" by (rule dvdE)
4.1590 -  then show "poly p c = 0" by simp
4.1591 -qed
4.1592 -
4.1593 -lemma dvd_iff_poly_eq_0:
4.1594 -  fixes c :: "'a::idom"
4.1595 -  shows "[:c, 1:] dvd p \<longleftrightarrow> poly p (-c) = 0"
4.1596 -  by (simp add: poly_eq_0_iff_dvd)
4.1597 -
4.1598 -lemma poly_roots_finite:
4.1599 -  fixes p :: "'a::idom poly"
4.1600 -  shows "p \<noteq> 0 \<Longrightarrow> finite {x. poly p x = 0}"
4.1601 -proof (induct n \<equiv> "degree p" arbitrary: p)
4.1602 -  case (0 p)
4.1603 -  then obtain a where "a \<noteq> 0" and "p = [:a:]"
4.1604 -    by (cases p, simp split: if_splits)
4.1605 -  then show "finite {x. poly p x = 0}" by simp
4.1606 -next
4.1607 -  case (Suc n p)
4.1608 -  show "finite {x. poly p x = 0}"
4.1609 -  proof (cases "\<exists>x. poly p x = 0")
4.1610 -    case False
4.1611 -    then show "finite {x. poly p x = 0}" by simp
4.1612 -  next
4.1613 -    case True
4.1614 -    then obtain a where "poly p a = 0" ..
4.1615 -    then have "[:-a, 1:] dvd p" by (simp only: poly_eq_0_iff_dvd)
4.1616 -    then obtain k where k: "p = [:-a, 1:] * k" ..
4.1617 -    with `p \<noteq> 0` have "k \<noteq> 0" by auto
4.1618 -    with k have "degree p = Suc (degree k)"
4.1619 -      by (simp add: degree_mult_eq del: mult_pCons_left)
4.1620 -    with `Suc n = degree p` have "n = degree k" by simp
4.1621 -    then have "finite {x. poly k x = 0}" using `k \<noteq> 0` by (rule Suc.hyps)
4.1622 -    then have "finite (insert a {x. poly k x = 0})" by simp
4.1623 -    then show "finite {x. poly p x = 0}"
4.1624 -      by (simp add: k uminus_add_conv_diff Collect_disj_eq
4.1625 -               del: mult_pCons_left)
4.1626 -  qed
4.1627 -qed
4.1628 -
4.1629 -lemma poly_zero:
4.1630 -  fixes p :: "'a::{idom,ring_char_0} poly"
4.1631 -  shows "poly p = poly 0 \<longleftrightarrow> p = 0"
4.1632 -apply (cases "p = 0", simp_all)
4.1633 -apply (drule poly_roots_finite)
4.1634 -apply (auto simp add: infinite_UNIV_char_0)
4.1635 -done
4.1636 -
4.1637 -lemma poly_eq_iff:
4.1638 -  fixes p q :: "'a::{idom,ring_char_0} poly"
4.1639 -  shows "poly p = poly q \<longleftrightarrow> p = q"
4.1640 -  using poly_zero [of "p - q"]
4.1641 -  by (simp add: fun_eq_iff)
4.1642 -
4.1643 -
4.1644 -subsection {* Composition of polynomials *}
4.1645 -
4.1646 -definition
4.1647 -  pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
4.1648 -where
4.1649 -  "pcompose p q = poly_rec 0 (\<lambda>a _ c. [:a:] + q * c) p"
4.1650 -
4.1651 -lemma pcompose_0 [simp]: "pcompose 0 q = 0"
4.1652 -  unfolding pcompose_def by (simp add: poly_rec_0)
4.1653 -
4.1654 -lemma pcompose_pCons:
4.1655 -  "pcompose (pCons a p) q = [:a:] + q * pcompose p q"
4.1656 -  unfolding pcompose_def by (simp add: poly_rec_pCons)
4.1657 -
4.1658 -lemma poly_pcompose: "poly (pcompose p q) x = poly p (poly q x)"
4.1659 -  by (induct p) (simp_all add: pcompose_pCons)
4.1660 -
4.1661 -lemma degree_pcompose_le:
4.1662 -  "degree (pcompose p q) \<le> degree p * degree q"
4.1663 -apply (induct p, simp)
4.1664 -apply (simp add: pcompose_pCons, clarify)
4.1665 -apply (rule degree_add_le, simp)
4.1666 -apply (rule order_trans [OF degree_mult_le], simp)
4.1667 -done
4.1668 +lemma pdivmod_fold_coeffs [code]:
4.1669 +  "pdivmod p q = (if q = 0 then (0, p)
4.1670 +    else fold_coeffs (\<lambda>a (s, r).
4.1671 +      let b = coeff (pCons a r) (degree q) / coeff q (degree q)
4.1672 +      in (pCons b s, pCons a r - smult b q)
4.1673 +   ) p (0, 0))"
4.1674 +  apply (cases "q = 0")
4.1675 +  apply (simp add: pdivmod_def)
4.1676 +  apply (rule sym)
4.1677 +  apply (induct p)
4.1678 +  apply (simp_all add: pdivmod_0 pdivmod_pCons)
4.1679 +  apply (case_tac "a = 0 \<and> p = 0")
4.1680 +  apply (auto simp add: pdivmod_def)
4.1681 +  done
4.1682
4.1683
4.1684  subsection {* Order of polynomial roots *}
4.1685
4.1686 -definition
4.1687 -  order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat"
4.1688 +definition order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat"
4.1689  where
4.1690    "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
4.1691
4.1692 @@ -1490,107 +1751,161 @@
4.1693  done
4.1694
4.1695
4.1696 -subsection {* Configuration of the code generator *}
4.1697 -
4.1698 -code_datatype "0::'a::zero poly" pCons
4.1699 +subsection {* GCD of polynomials *}
4.1700
4.1701 -quickcheck_generator poly constructors: "0::'a::zero poly", pCons
4.1702 -
4.1703 -instantiation poly :: ("{zero, equal}") equal
4.1704 +instantiation poly :: (field) gcd
4.1705  begin
4.1706
4.1707 -definition
4.1708 -  "HOL.equal (p::'a poly) q \<longleftrightarrow> p = q"
4.1709 +function gcd_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
4.1710 +where
4.1711 +  "gcd (x::'a poly) 0 = smult (inverse (coeff x (degree x))) x"
4.1712 +| "y \<noteq> 0 \<Longrightarrow> gcd (x::'a poly) y = gcd y (x mod y)"
4.1713 +by auto
4.1714
4.1715 -instance proof
4.1716 -qed (rule equal_poly_def)
4.1717 +termination "gcd :: _ poly \<Rightarrow> _"
4.1718 +by (relation "measure (\<lambda>(x, y). if y = 0 then 0 else Suc (degree y))")
4.1719 +   (auto dest: degree_mod_less)
4.1720 +
4.1721 +declare gcd_poly.simps [simp del]
4.1722 +
4.1723 +instance ..
4.1724
4.1725  end
4.1726
4.1727 -lemma eq_poly_code [code]:
4.1728 -  "HOL.equal (0::_ poly) (0::_ poly) \<longleftrightarrow> True"
4.1729 -  "HOL.equal (0::_ poly) (pCons b q) \<longleftrightarrow> HOL.equal 0 b \<and> HOL.equal 0 q"
4.1730 -  "HOL.equal (pCons a p) (0::_ poly) \<longleftrightarrow> HOL.equal a 0 \<and> HOL.equal p 0"
4.1731 -  "HOL.equal (pCons a p) (pCons b q) \<longleftrightarrow> HOL.equal a b \<and> HOL.equal p q"
4.1732 -  by (simp_all add: equal)
4.1733 +lemma
4.1734 +  fixes x y :: "_ poly"
4.1735 +  shows poly_gcd_dvd1 [iff]: "gcd x y dvd x"
4.1736 +    and poly_gcd_dvd2 [iff]: "gcd x y dvd y"
4.1737 +  apply (induct x y rule: gcd_poly.induct)
4.1738 +  apply (simp_all add: gcd_poly.simps)
4.1739 +  apply (fastforce simp add: smult_dvd_iff dest: inverse_zero_imp_zero)
4.1740 +  apply (blast dest: dvd_mod_imp_dvd)
4.1741 +  done
4.1742
4.1743 -lemma [code nbe]:
4.1744 -  "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
4.1745 -  by (fact equal_refl)
4.1746 +lemma poly_gcd_greatest:
4.1747 +  fixes k x y :: "_ poly"
4.1748 +  shows "k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd gcd x y"
4.1749 +  by (induct x y rule: gcd_poly.induct)
4.1750 +     (simp_all add: gcd_poly.simps dvd_mod dvd_smult)
4.1751
4.1752 -lemmas coeff_code [code] =
4.1753 -  coeff_0 coeff_pCons_0 coeff_pCons_Suc
4.1754 +lemma dvd_poly_gcd_iff [iff]:
4.1755 +  fixes k x y :: "_ poly"
4.1756 +  shows "k dvd gcd x y \<longleftrightarrow> k dvd x \<and> k dvd y"
4.1757 +  by (blast intro!: poly_gcd_greatest intro: dvd_trans)
4.1758
4.1759 -lemmas degree_code [code] =
4.1760 -  degree_0 degree_pCons_eq_if
4.1761 +lemma poly_gcd_monic:
4.1762 +  fixes x y :: "_ poly"
4.1763 +  shows "coeff (gcd x y) (degree (gcd x y)) =
4.1764 +    (if x = 0 \<and> y = 0 then 0 else 1)"
4.1765 +  by (induct x y rule: gcd_poly.induct)
4.1766 +     (simp_all add: gcd_poly.simps nonzero_imp_inverse_nonzero)
4.1767
4.1768 -lemmas monom_poly_code [code] =
4.1769 -  monom_0 monom_Suc
4.1770 +lemma poly_gcd_zero_iff [simp]:
4.1771 +  fixes x y :: "_ poly"
4.1772 +  shows "gcd x y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
4.1773 +  by (simp only: dvd_0_left_iff [symmetric] dvd_poly_gcd_iff)
4.1774
4.1775 -lemma add_poly_code [code]:
4.1776 -  "0 + q = (q :: _ poly)"
4.1777 -  "p + 0 = (p :: _ poly)"
4.1778 -  "pCons a p + pCons b q = pCons (a + b) (p + q)"
4.1779 -by simp_all
4.1780 +lemma poly_gcd_0_0 [simp]:
4.1781 +  "gcd (0::_ poly) 0 = 0"
4.1782 +  by simp
4.1783
4.1784 -lemma minus_poly_code [code]:
4.1785 -  "- 0 = (0 :: _ poly)"
4.1786 -  "- pCons a p = pCons (- a) (- p)"
4.1787 -by simp_all
4.1788 +lemma poly_dvd_antisym:
4.1789 +  fixes p q :: "'a::idom poly"
4.1790 +  assumes coeff: "coeff p (degree p) = coeff q (degree q)"
4.1791 +  assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q"
4.1792 +proof (cases "p = 0")
4.1793 +  case True with coeff show "p = q" by simp
4.1794 +next
4.1795 +  case False with coeff have "q \<noteq> 0" by auto
4.1796 +  have degree: "degree p = degree q"
4.1797 +    using `p dvd q` `q dvd p` `p \<noteq> 0` `q \<noteq> 0`
4.1798 +    by (intro order_antisym dvd_imp_degree_le)
4.1799
4.1800 -lemma diff_poly_code [code]:
4.1801 -  "0 - q = (- q :: _ poly)"
4.1802 -  "p - 0 = (p :: _ poly)"
4.1803 -  "pCons a p - pCons b q = pCons (a - b) (p - q)"
4.1804 -by simp_all
4.1805 +  from `p dvd q` obtain a where a: "q = p * a" ..
4.1806 +  with `q \<noteq> 0` have "a \<noteq> 0" by auto
4.1807 +  with degree a `p \<noteq> 0` have "degree a = 0"
4.1808 +    by (simp add: degree_mult_eq)
4.1809 +  with coeff a show "p = q"
4.1810 +    by (cases a, auto split: if_splits)
4.1811 +qed
4.1812
4.1813 -lemmas smult_poly_code [code] =
4.1814 -  smult_0_right smult_pCons
4.1815 -
4.1816 -lemma mult_poly_code [code]:
4.1817 -  "0 * q = (0 :: _ poly)"
4.1818 -  "pCons a p * q = smult a q + pCons 0 (p * q)"
4.1819 -by simp_all
4.1820 +lemma poly_gcd_unique:
4.1821 +  fixes d x y :: "_ poly"
4.1822 +  assumes dvd1: "d dvd x" and dvd2: "d dvd y"
4.1823 +    and greatest: "\<And>k. k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd d"
4.1824 +    and monic: "coeff d (degree d) = (if x = 0 \<and> y = 0 then 0 else 1)"
4.1825 +  shows "gcd x y = d"
4.1826 +proof -
4.1827 +  have "coeff (gcd x y) (degree (gcd x y)) = coeff d (degree d)"
4.1828 +    by (simp_all add: poly_gcd_monic monic)
4.1829 +  moreover have "gcd x y dvd d"
4.1830 +    using poly_gcd_dvd1 poly_gcd_dvd2 by (rule greatest)
4.1831 +  moreover have "d dvd gcd x y"
4.1832 +    using dvd1 dvd2 by (rule poly_gcd_greatest)
4.1833 +  ultimately show ?thesis
4.1834 +    by (rule poly_dvd_antisym)
4.1835 +qed
4.1836
4.1837 -lemmas poly_code [code] =
4.1838 -  poly_0 poly_pCons
4.1839 -
4.1840 -lemmas synthetic_divmod_code [code] =
4.1841 -  synthetic_divmod_0 synthetic_divmod_pCons
4.1842 +interpretation gcd_poly!: abel_semigroup "gcd :: _ poly \<Rightarrow> _"
4.1843 +proof
4.1844 +  fix x y z :: "'a poly"
4.1845 +  show "gcd (gcd x y) z = gcd x (gcd y z)"
4.1846 +    by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
4.1847 +  show "gcd x y = gcd y x"
4.1848 +    by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
4.1849 +qed
4.1850
4.1851 -text {* code generator setup for div and mod *}
4.1852 +lemmas poly_gcd_assoc = gcd_poly.assoc
4.1853 +lemmas poly_gcd_commute = gcd_poly.commute
4.1854 +lemmas poly_gcd_left_commute = gcd_poly.left_commute
4.1855
4.1856 -definition
4.1857 -  pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
4.1858 -where
4.1859 -  "pdivmod x y = (x div y, x mod y)"
4.1860 +lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute
4.1861 +
4.1862 +lemma poly_gcd_1_left [simp]: "gcd 1 y = (1 :: _ poly)"
4.1863 +by (rule poly_gcd_unique) simp_all
4.1864
4.1865 -lemma div_poly_code [code]: "x div y = fst (pdivmod x y)"
4.1866 -  unfolding pdivmod_def by simp
4.1867 +lemma poly_gcd_1_right [simp]: "gcd x 1 = (1 :: _ poly)"
4.1868 +by (rule poly_gcd_unique) simp_all
4.1869 +
4.1870 +lemma poly_gcd_minus_left [simp]: "gcd (- x) y = gcd x (y :: _ poly)"
4.1871 +by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
4.1872
4.1873 -lemma mod_poly_code [code]: "x mod y = snd (pdivmod x y)"
4.1874 -  unfolding pdivmod_def by simp
4.1875 +lemma poly_gcd_minus_right [simp]: "gcd x (- y) = gcd x (y :: _ poly)"
4.1876 +by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
4.1877
4.1878 -lemma pdivmod_0 [code]: "pdivmod 0 y = (0, 0)"
4.1879 -  unfolding pdivmod_def by simp
4.1880 +lemma poly_gcd_code [code]:
4.1881 +  "gcd x y = (if y = 0 then smult (inverse (coeff x (degree x))) x else gcd y (x mod (y :: _ poly)))"
4.1882 +  by (simp add: gcd_poly.simps)
4.1883 +
4.1884 +
4.1885 +subsection {* Composition of polynomials *}
4.1886
4.1887 -lemma pdivmod_pCons [code]:
4.1888 -  "pdivmod (pCons a x) y =
4.1889 -    (if y = 0 then (0, pCons a x) else
4.1890 -      (let (q, r) = pdivmod x y;
4.1891 -           b = coeff (pCons a r) (degree y) / coeff y (degree y)
4.1892 -        in (pCons b q, pCons a r - smult b y)))"
4.1893 -apply (simp add: pdivmod_def Let_def, safe)
4.1894 -apply (rule div_poly_eq)
4.1895 -apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
4.1896 -apply (rule mod_poly_eq)
4.1897 -apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
4.1898 +definition pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
4.1899 +where
4.1900 +  "pcompose p q = fold_coeffs (\<lambda>a c. [:a:] + q * c) p 0"
4.1901 +
4.1902 +lemma pcompose_0 [simp]:
4.1903 +  "pcompose 0 q = 0"
4.1904 +  by (simp add: pcompose_def)
4.1905 +
4.1906 +lemma pcompose_pCons:
4.1907 +  "pcompose (pCons a p) q = [:a:] + q * pcompose p q"
4.1908 +  by (cases "p = 0 \<and> a = 0") (auto simp add: pcompose_def)
4.1909 +
4.1910 +lemma poly_pcompose:
4.1911 +  "poly (pcompose p q) x = poly p (poly q x)"
4.1912 +  by (induct p) (simp_all add: pcompose_pCons)
4.1913 +
4.1914 +lemma degree_pcompose_le:
4.1915 +  "degree (pcompose p q) \<le> degree p * degree q"
4.1916 +apply (induct p, simp)
4.1917 +apply (simp add: pcompose_pCons, clarify)
4.1918 +apply (rule degree_add_le, simp)
4.1919 +apply (rule order_trans [OF degree_mult_le], simp)
4.1920  done
4.1921
4.1922 -lemma poly_gcd_code [code]:
4.1923 -  "poly_gcd x y =
4.1924 -    (if y = 0 then smult (inverse (coeff x (degree x))) x
4.1925 -              else poly_gcd y (x mod y))"
4.1926 -  by (simp add: poly_gcd.simps)
4.1927 +
4.1928 +no_notation cCons (infixr "##" 65)
4.1929
4.1930  end
4.1931 +
```
```     5.1 --- a/src/HOL/List.thy	Sat Jun 15 17:19:23 2013 +0200
5.2 +++ b/src/HOL/List.thy	Sat Jun 15 17:19:23 2013 +0200
5.3 @@ -2308,6 +2308,14 @@
5.4    ==> dropWhile P l = dropWhile Q k"
5.5  by (induct k arbitrary: l, simp_all)
5.6
5.7 +lemma takeWhile_idem [simp]:
5.8 +  "takeWhile P (takeWhile P xs) = takeWhile P xs"
5.9 +  by (induct xs) auto
5.10 +
5.11 +lemma dropWhile_idem [simp]:
5.12 +  "dropWhile P (dropWhile P xs) = dropWhile P xs"
5.13 +  by (induct xs) auto
5.14 +
5.15
5.16  subsubsection {* @{const zip} *}
5.17
5.18 @@ -2947,6 +2955,10 @@
5.19  apply (auto simp add: less_diff_conv)
5.20  done
5.21
5.22 +lemma map_decr_upt:
5.23 +  "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
5.24 +  by (induct n) simp_all
5.25 +
5.26  lemma nth_take_lemma:
5.27    "k <= length xs ==> k <= length ys ==>
5.28       (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
5.29 @@ -3703,7 +3715,6 @@
5.30  apply clarsimp
5.31  done
5.32
5.33 -
5.34  lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
5.35  by (induct n) auto
5.36
5.37 @@ -3819,6 +3830,22 @@
5.38    then show ?thesis by blast
5.39  qed
5.40
5.41 +lemma Cons_replicate_eq:
5.42 +  "x # xs = replicate n y \<longleftrightarrow> x = y \<and> n > 0 \<and> xs = replicate (n - 1) x"
5.43 +  by (induct n) auto
5.44 +
5.45 +lemma replicate_length_same:
5.46 +  "(\<forall>y\<in>set xs. y = x) \<Longrightarrow> replicate (length xs) x = xs"
5.47 +  by (induct xs) simp_all
5.48 +
5.49 +lemma foldr_replicate [simp]:
5.50 +  "foldr f (replicate n x) = f x ^^ n"
5.51 +  by (induct n) (simp_all)
5.52 +
5.53 +lemma fold_replicate [simp]:
5.54 +  "fold f (replicate n x) = f x ^^ n"
5.55 +  by (subst foldr_fold [symmetric]) simp_all
5.56 +
5.57
5.58  subsubsection {* @{const enumerate} *}
5.59
```
```     6.1 --- a/src/HOL/Set_Interval.thy	Sat Jun 15 17:19:23 2013 +0200
6.2 +++ b/src/HOL/Set_Interval.thy	Sat Jun 15 17:19:23 2013 +0200
6.3 @@ -1438,6 +1438,26 @@
6.5  done
6.6
6.7 +lemma setsum_atMost_Suc_shift:
6.8 +  fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
6.9 +  shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
6.10 +proof (induct n)
6.11 +  case 0 show ?case by simp
6.12 +next
6.13 +  case (Suc n) note IH = this
6.14 +  have "(\<Sum>i\<le>Suc (Suc n). f i) = (\<Sum>i\<le>Suc n. f i) + f (Suc (Suc n))"
6.15 +    by (rule setsum_atMost_Suc)
6.16 +  also have "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
6.17 +    by (rule IH)
6.18 +  also have "f 0 + (\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) =
6.19 +             f 0 + ((\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)))"
6.20 +    by (rule add_assoc)
6.21 +  also have "(\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) = (\<Sum>i\<le>Suc n. f (Suc i))"
6.22 +    by (rule setsum_atMost_Suc [symmetric])
6.23 +  finally show ?case .
6.24 +qed
6.25 +
6.26 +
6.27  subsection {* The formula for geometric sums *}
6.28
6.29  lemma geometric_sum:
```