author eberlm Mon Jan 11 16:38:39 2016 +0100 (2016-01-11) changeset 62128 3201ddb00097 parent 62127 d8e7738bd2e9 child 62129 72d19e588e97 child 62131 1baed43f453e
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
 src/HOL/Binomial.thy file | annotate | diff | revisions src/HOL/Int.thy 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/Set_Interval.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Binomial.thy	Mon Jan 11 15:20:17 2016 +0100
1.2 +++ b/src/HOL/Binomial.thy	Mon Jan 11 16:38:39 2016 +0100
1.3 @@ -76,7 +76,7 @@
1.4        by (metis of_nat_mult order_refl power_Suc)
1.5      finally show ?case .
1.6    qed simp
1.7 -
1.8 +
1.9  end
1.10
1.11  text\<open>Note that @{term "fact 0 = fact 1"}\<close>
1.12 @@ -94,11 +94,17 @@
1.13    shows "1 \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact n"
1.14    by (induct n) (auto simp: dvdI le_Suc_eq)
1.15
1.16 +lemma fact_ge_self: "fact n \<ge> n"
1.17 +  by (cases "n = 0") (simp_all add: dvd_imp_le dvd_fact)
1.18 +
1.19  lemma fact_altdef_nat: "fact n = \<Prod>{1..n}"
1.20    by (induct n) (auto simp: atLeastAtMostSuc_conv)
1.21
1.22 -lemma fact_altdef: "fact n = setprod of_nat {1..n}"
1.23 +lemma fact_altdef: "fact n = (\<Prod>i=1..n. of_nat i)"
1.24    by (induct n) (auto simp: atLeastAtMostSuc_conv)
1.25 +
1.26 +lemma fact_altdef': "fact n = of_nat (\<Prod>{1..n})"
1.27 +  by (subst fact_altdef_nat [symmetric]) simp
1.28
1.29  lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a :: {semiring_div,linordered_semidom})"
1.30    by (induct m) (auto simp: le_Suc_eq)
1.31 @@ -1538,4 +1544,42 @@
1.32         (simp_all only: ac_simps diff_Suc_Suc Suc_diff_le diff_add_inverse fact_Suc of_nat_id)
1.33  qed
1.34
1.35 +
1.36 +
1.37 +lemma fact_code [code]:
1.38 +  "fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a :: semiring_char_0)"
1.39 +proof -
1.40 +  have "fact n = (of_nat (\<Prod>{1..n}) :: 'a)" by (simp add: fact_altdef')
1.41 +  also have "\<Prod>{1..n} = \<Prod>{2..n}"
1.42 +    by (intro setprod.mono_neutral_right) auto
1.43 +  also have "\<dots> = fold_atLeastAtMost_nat (op *) 2 n 1"
1.44 +    by (simp add: setprod_atLeastAtMost_code)
1.45 +  finally show ?thesis .
1.46 +qed
1.47 +
1.48 +lemma pochhammer_code [code]:
1.49 +  "pochhammer a n = (if n = 0 then 1 else
1.50 +       fold_atLeastAtMost_nat (\<lambda>n acc. (a + of_nat n) * acc) 0 (n - 1) 1)"
1.51 +  by (simp add: setprod_atLeastAtMost_code pochhammer_def)
1.52 +
1.53 +lemma gbinomial_code [code]:
1.54 +  "a gchoose n = (if n = 0 then 1 else
1.55 +     fold_atLeastAtMost_nat (\<lambda>n acc. (a - of_nat n) * acc) 0 (n - 1) 1 / fact n)"
1.56 +  by (simp add: setprod_atLeastAtMost_code gbinomial_def)
1.57 +
1.58 +lemma binomial_code [code]:
1.59 +  "(n choose k) =
1.60 +      (if k > n then 0
1.61 +       else if 2 * k > n then (n choose (n - k))
1.62 +       else (fold_atLeastAtMost_nat (op *) (n-k+1) n 1 div fact k))"
1.63 +proof -
1.64 +  {
1.65 +    assume "k \<le> n"
1.66 +    hence "{1..n} = {1..n-k} \<union> {n-k+1..n}" by auto
1.67 +    hence "(fact n :: nat) = fact (n-k) * \<Prod>{n-k+1..n}"
1.68 +      by (simp add: setprod.union_disjoint fact_altdef_nat)
1.69 +  }
1.70 +  thus ?thesis by (auto simp: binomial_altdef_nat mult_ac setprod_atLeastAtMost_code)
1.71 +qed
1.72 +
1.73  end
```
```     2.1 --- a/src/HOL/Int.thy	Mon Jan 11 15:20:17 2016 +0100
2.2 +++ b/src/HOL/Int.thy	Mon Jan 11 16:38:39 2016 +0100
2.3 @@ -314,6 +314,12 @@
2.4    "of_int z < 1 \<longleftrightarrow> z < 1"
2.5    using of_int_less_iff [of z 1] by simp
2.6
2.7 +lemma of_int_pos: "z > 0 \<Longrightarrow> of_int z > 0"
2.8 +  by simp
2.9 +
2.10 +lemma of_int_nonneg: "z \<ge> 0 \<Longrightarrow> of_int z \<ge> 0"
2.11 +  by simp
2.12 +
2.13  end
2.14
2.15  text \<open>Comparisons involving @{term of_int}.\<close>
```
```     3.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Jan 11 15:20:17 2016 +0100
3.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Jan 11 16:38:39 2016 +0100
3.3 @@ -1066,11 +1066,6 @@
3.4    qed
3.5  qed
3.6
3.7 -lemma divides_degree:
3.8 -  assumes pq: "p dvd (q:: complex poly)"
3.9 -  shows "degree p \<le> degree q \<or> q = 0"
3.10 -  by (metis dvd_imp_degree_le pq)
3.11 -
3.12  text \<open>Arithmetic operations on multivariate polynomials.\<close>
3.13
3.14  lemma mpoly_base_conv:
```
```     4.1 --- a/src/HOL/Library/Poly_Deriv.thy	Mon Jan 11 15:20:17 2016 +0100
4.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Mon Jan 11 16:38:39 2016 +0100
4.3 @@ -11,7 +11,7 @@
4.4
4.5  subsection \<open>Derivatives of univariate polynomials\<close>
4.6
4.7 -function pderiv :: "'a::real_normed_field poly \<Rightarrow> 'a poly"
4.8 +function pderiv :: "('a :: semidom) poly \<Rightarrow> 'a poly"
4.9  where
4.10    [simp del]: "pderiv (pCons a p) = (if p = 0 then 0 else p + pCons 0 (pderiv p))"
4.11    by (auto intro: pCons_cases)
4.12 @@ -27,27 +27,98 @@
4.13    "pderiv (pCons a p) = p + pCons 0 (pderiv p)"
4.15
4.16 +lemma pderiv_1 [simp]: "pderiv 1 = 0"
4.17 +  unfolding one_poly_def by (simp add: pderiv_pCons)
4.18 +
4.19 +lemma pderiv_of_nat  [simp]: "pderiv (of_nat n) = 0"
4.20 +  and pderiv_numeral [simp]: "pderiv (numeral m) = 0"
4.21 +  by (simp_all add: of_nat_poly numeral_poly pderiv_pCons)
4.22 +
4.23  lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)"
4.24    by (induct p arbitrary: n)
4.25       (auto simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
4.26
4.27 -primrec pderiv_coeffs :: "'a::comm_monoid_add list \<Rightarrow> 'a list"
4.28 -where
4.29 -  "pderiv_coeffs [] = []"
4.30 -| "pderiv_coeffs (x # xs) = plus_coeffs xs (cCons 0 (pderiv_coeffs xs))"
4.31 +fun pderiv_coeffs_code :: "('a :: semidom) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
4.32 +  "pderiv_coeffs_code f (x # xs) = cCons (f * x) (pderiv_coeffs_code (f+1) xs)"
4.33 +| "pderiv_coeffs_code f [] = []"
4.34 +
4.35 +definition pderiv_coeffs :: "('a :: semidom) list \<Rightarrow> 'a list" where
4.36 +  "pderiv_coeffs xs = pderiv_coeffs_code 1 (tl xs)"
4.37
4.38 -lemma coeffs_pderiv [code abstract]:
4.39 -  "coeffs (pderiv p) = pderiv_coeffs (coeffs p)"
4.40 -  by (rule sym, induct p) (simp_all add: pderiv_pCons coeffs_plus_eq_plus_coeffs cCons_def)
4.41 +(* Efficient code for pderiv contributed by René Thiemann and Akihisa Yamada *)
4.42 +lemma pderiv_coeffs_code:
4.43 +  "nth_default 0 (pderiv_coeffs_code f xs) n = (f + of_nat n) * (nth_default 0 xs n)"
4.44 +proof (induct xs arbitrary: f n)
4.45 +  case (Cons x xs f n)
4.46 +  show ?case
4.47 +  proof (cases n)
4.48 +    case 0
4.49 +    thus ?thesis by (cases "pderiv_coeffs_code (f + 1) xs = [] \<and> f * x = 0", auto simp: cCons_def)
4.50 +  next
4.51 +    case (Suc m) note n = this
4.52 +    show ?thesis
4.53 +    proof (cases "pderiv_coeffs_code (f + 1) xs = [] \<and> f * x = 0")
4.54 +      case False
4.55 +      hence "nth_default 0 (pderiv_coeffs_code f (x # xs)) n =
4.56 +               nth_default 0 (pderiv_coeffs_code (f + 1) xs) m"
4.57 +        by (auto simp: cCons_def n)
4.58 +      also have "\<dots> = (f + of_nat n) * (nth_default 0 xs m)"
4.60 +      finally show ?thesis by (simp add: n)
4.61 +    next
4.62 +      case True
4.63 +      {
4.64 +        fix g
4.65 +        have "pderiv_coeffs_code g xs = [] \<Longrightarrow> g + of_nat m = 0 \<or> nth_default 0 xs m = 0"
4.66 +        proof (induct xs arbitrary: g m)
4.67 +          case (Cons x xs g)
4.68 +          from Cons(2) have empty: "pderiv_coeffs_code (g + 1) xs = []"
4.69 +                            and g: "(g = 0 \<or> x = 0)"
4.70 +            by (auto simp: cCons_def split: if_splits)
4.71 +          note IH = Cons(1)[OF empty]
4.72 +          from IH[of m] IH[of "m - 1"] g
4.73 +          show ?case by (cases m, auto simp: field_simps)
4.74 +        qed simp
4.75 +      } note empty = this
4.76 +      from True have "nth_default 0 (pderiv_coeffs_code f (x # xs)) n = 0"
4.77 +        by (auto simp: cCons_def n)
4.78 +      moreover have "(f + of_nat n) * nth_default 0 (x # xs) n = 0" using True
4.79 +        by (simp add: n, insert empty[of "f+1"], auto simp: field_simps)
4.80 +      ultimately show ?thesis by simp
4.81 +    qed
4.82 +  qed
4.83 +qed simp
4.84
4.85 -lemma pderiv_eq_0_iff: "pderiv p = 0 \<longleftrightarrow> degree p = 0"
4.86 +lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda> i. f (Suc i)) [0 ..< n]"
4.87 +  by (induct n arbitrary: f, auto)
4.88 +
4.89 +lemma coeffs_pderiv_code [code abstract]:
4.90 +  "coeffs (pderiv p) = pderiv_coeffs (coeffs p)" unfolding pderiv_coeffs_def
4.91 +proof (rule coeffs_eqI, unfold pderiv_coeffs_code coeff_pderiv, goal_cases)
4.92 +  case (1 n)
4.93 +  have id: "coeff p (Suc n) = nth_default 0 (map (\<lambda>i. coeff p (Suc i)) [0..<degree p]) n"
4.94 +    by (cases "n < degree p", auto simp: nth_default_def coeff_eq_0)
4.95 +  show ?case unfolding coeffs_def map_upt_Suc by (auto simp: id)
4.96 +next
4.97 +  case 2
4.98 +  obtain n xs where id: "tl (coeffs p) = xs" "(1 :: 'a) = n" by auto
4.99 +  from 2 show ?case
4.100 +    unfolding id by (induct xs arbitrary: n, auto simp: cCons_def)
4.101 +qed
4.102 +
4.103 +context
4.104 +  assumes "SORT_CONSTRAINT('a::{semidom, semiring_char_0})"
4.105 +begin
4.106 +
4.107 +lemma pderiv_eq_0_iff:
4.108 +  "pderiv (p :: 'a poly) = 0 \<longleftrightarrow> degree p = 0"
4.109    apply (rule iffI)
4.110    apply (cases p, simp)
4.111    apply (simp add: poly_eq_iff coeff_pderiv del: of_nat_Suc)
4.112    apply (simp add: poly_eq_iff coeff_pderiv coeff_eq_0)
4.113    done
4.114
4.115 -lemma degree_pderiv: "degree (pderiv p) = degree p - 1"
4.116 +lemma degree_pderiv: "degree (pderiv (p :: 'a poly)) = degree p - 1"
4.117    apply (rule order_antisym [OF degree_le])
4.118    apply (simp add: coeff_pderiv coeff_eq_0)
4.119    apply (cases "degree p", simp)
4.120 @@ -56,14 +127,30 @@
4.121    apply (metis degree_0 leading_coeff_0_iff nat.distinct(1))
4.122    done
4.123
4.124 +lemma not_dvd_pderiv:
4.125 +  assumes "degree (p :: 'a poly) \<noteq> 0"
4.126 +  shows "\<not> p dvd pderiv p"
4.127 +proof
4.128 +  assume dvd: "p dvd pderiv p"
4.129 +  then obtain q where p: "pderiv p = p * q" unfolding dvd_def by auto
4.130 +  from dvd have le: "degree p \<le> degree (pderiv p)"
4.131 +    by (simp add: assms dvd_imp_degree_le pderiv_eq_0_iff)
4.132 +  from this[unfolded degree_pderiv] assms show False by auto
4.133 +qed
4.134 +
4.135 +lemma dvd_pderiv_iff [simp]: "(p :: 'a poly) dvd pderiv p \<longleftrightarrow> degree p = 0"
4.136 +  using not_dvd_pderiv[of p] by (auto simp: pderiv_eq_0_iff [symmetric])
4.137 +
4.138 +end
4.139 +
4.140  lemma pderiv_singleton [simp]: "pderiv [:a:] = 0"
4.142
4.143  lemma pderiv_add: "pderiv (p + q) = pderiv p + pderiv q"
4.144  by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
4.145
4.146 -lemma pderiv_minus: "pderiv (- p) = - pderiv p"
4.147 -by (rule poly_eqI, simp add: coeff_pderiv)
4.148 +lemma pderiv_minus: "pderiv (- p :: 'a :: idom poly) = - pderiv p"
4.149 +by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
4.150
4.151  lemma pderiv_diff: "pderiv (p - q) = pderiv p - pderiv q"
4.152  by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
4.153 @@ -85,6 +172,27 @@
4.155  done
4.156
4.157 +lemma pderiv_setprod: "pderiv (setprod f (as)) =
4.158 +  (\<Sum>a \<in> as. setprod f (as - {a}) * pderiv (f a))"
4.159 +proof (induct as rule: infinite_finite_induct)
4.160 +  case (insert a as)
4.161 +  hence id: "setprod f (insert a as) = f a * setprod f as"
4.162 +    "\<And> g. setsum g (insert a as) = g a + setsum g as"
4.163 +    "insert a as - {a} = as"
4.164 +    by auto
4.165 +  {
4.166 +    fix b
4.167 +    assume "b \<in> as"
4.168 +    hence id2: "insert a as - {b} = insert a (as - {b})" using `a \<notin> as` by auto
4.169 +    have "setprod f (insert a as - {b}) = f a * setprod f (as - {b})"
4.170 +      unfolding id2
4.171 +      by (subst setprod.insert, insert insert, auto)
4.172 +  } note id2 = this
4.173 +  show ?case
4.174 +    unfolding id pderiv_mult insert(3) setsum_right_distrib
4.175 +    by (auto simp add: ac_simps id2 intro!: setsum.cong)
4.176 +qed auto
4.177 +
4.178  lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)"
4.179  by (rule DERIV_cong, rule DERIV_pow, simp)
4.180  declare DERIV_pow2 [simp] DERIV_pow [simp]
4.181 @@ -92,7 +200,7 @@
4.182  lemma DERIV_add_const: "DERIV f x :> D ==>  DERIV (%x. a + f x :: 'a::real_normed_field) x :> D"
4.183  by (rule DERIV_cong, rule DERIV_add, auto)
4.184
4.185 -lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
4.186 +lemma poly_DERIV [simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
4.187    by (induct p, auto intro!: derivative_eq_intros simp add: pderiv_pCons)
4.188
4.189  lemma continuous_on_poly [continuous_intros]:
4.190 @@ -186,6 +294,104 @@
4.191  qed
4.192
4.193
4.194 +subsection \<open>Algebraic numbers\<close>
4.195 +
4.196 +text \<open>
4.197 +  Algebraic numbers can be defined in two equivalent ways: all real numbers that are
4.198 +  roots of rational polynomials or of integer polynomials. The Algebraic-Numbers AFP entry
4.199 +  uses the rational definition, but we need the integer definition.
4.200 +
4.201 +  The equivalence is obvious since any rational polynomial can be multiplied with the
4.202 +  LCM of its coefficients, yielding an integer polynomial with the same roots.
4.203 +\<close>
4.204 +subsection \<open>Algebraic numbers\<close>
4.205 +
4.206 +definition algebraic :: "'a :: field_char_0 \<Rightarrow> bool" where
4.207 +  "algebraic x \<longleftrightarrow> (\<exists>p. (\<forall>i. coeff p i \<in> \<int>) \<and> p \<noteq> 0 \<and> poly p x = 0)"
4.208 +
4.209 +lemma algebraicI:
4.210 +  assumes "\<And>i. coeff p i \<in> \<int>" "p \<noteq> 0" "poly p x = 0"
4.211 +  shows   "algebraic x"
4.212 +  using assms unfolding algebraic_def by blast
4.213 +
4.214 +lemma algebraicE:
4.215 +  assumes "algebraic x"
4.216 +  obtains p where "\<And>i. coeff p i \<in> \<int>" "p \<noteq> 0" "poly p x = 0"
4.217 +  using assms unfolding algebraic_def by blast
4.218 +
4.219 +lemma quotient_of_denom_pos': "snd (quotient_of x) > 0"
4.220 +  using quotient_of_denom_pos[OF surjective_pairing] .
4.221 +
4.222 +lemma of_int_div_in_Ints:
4.223 +  "b dvd a \<Longrightarrow> of_int a div of_int b \<in> (\<int> :: 'a :: ring_div set)"
4.224 +proof (cases "of_int b = (0 :: 'a)")
4.225 +  assume "b dvd a" "of_int b \<noteq> (0::'a)"
4.226 +  then obtain c where "a = b * c" by (elim dvdE)
4.227 +  with \<open>of_int b \<noteq> (0::'a)\<close> show ?thesis by simp
4.228 +qed auto
4.229 +
4.230 +lemma of_int_divide_in_Ints:
4.231 +  "b dvd a \<Longrightarrow> of_int a / of_int b \<in> (\<int> :: 'a :: field set)"
4.232 +proof (cases "of_int b = (0 :: 'a)")
4.233 +  assume "b dvd a" "of_int b \<noteq> (0::'a)"
4.234 +  then obtain c where "a = b * c" by (elim dvdE)
4.235 +  with \<open>of_int b \<noteq> (0::'a)\<close> show ?thesis by simp
4.236 +qed auto
4.237 +
4.238 +lemma algebraic_altdef:
4.239 +  fixes p :: "'a :: field_char_0 poly"
4.240 +  shows "algebraic x \<longleftrightarrow> (\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)"
4.241 +proof safe
4.242 +  fix p assume rat: "\<forall>i. coeff p i \<in> \<rat>" and root: "poly p x = 0" and nz: "p \<noteq> 0"
4.243 +  def cs \<equiv> "coeffs p"
4.244 +  from rat have "\<forall>c\<in>range (coeff p). \<exists>c'. c = of_rat c'" unfolding Rats_def by blast
4.245 +  then obtain f where f: "\<And>i. coeff p i = of_rat (f (coeff p i))"
4.246 +    by (subst (asm) bchoice_iff) blast
4.247 +  def cs' \<equiv> "map (quotient_of \<circ> f) (coeffs p)"
4.248 +  def d \<equiv> "Lcm (set (map snd cs'))"
4.249 +  def p' \<equiv> "smult (of_int d) p"
4.250 +
4.251 +  have "\<forall>n. coeff p' n \<in> \<int>"
4.252 +  proof
4.253 +    fix n :: nat
4.254 +    show "coeff p' n \<in> \<int>"
4.255 +    proof (cases "n \<le> degree p")
4.256 +      case True
4.257 +      def c \<equiv> "coeff p n"
4.258 +      def a \<equiv> "fst (quotient_of (f (coeff p n)))" and b \<equiv> "snd (quotient_of (f (coeff p n)))"
4.259 +      have b_pos: "b > 0" unfolding b_def using quotient_of_denom_pos' by simp
4.260 +      have "coeff p' n = of_int d * coeff p n" by (simp add: p'_def)
4.261 +      also have "coeff p n = of_rat (of_int a / of_int b)" unfolding a_def b_def
4.262 +        by (subst quotient_of_div [of "f (coeff p n)", symmetric])
4.263 +           (simp_all add: f [symmetric])
4.264 +      also have "of_int d * \<dots> = of_rat (of_int (a*d) / of_int b)"
4.265 +        by (simp add: of_rat_mult of_rat_divide)
4.266 +      also from nz True have "b \<in> snd ` set cs'" unfolding cs'_def
4.267 +        by (force simp: o_def b_def coeffs_def simp del: upt_Suc)
4.268 +      hence "b dvd (a * d)" unfolding d_def by simp
4.269 +      hence "of_int (a * d) / of_int b \<in> (\<int> :: rat set)"
4.270 +        by (rule of_int_divide_in_Ints)
4.271 +      hence "of_rat (of_int (a * d) / of_int b) \<in> \<int>" by (elim Ints_cases) auto
4.272 +      finally show ?thesis .
4.273 +    qed (auto simp: p'_def not_le coeff_eq_0)
4.274 +  qed
4.275 +
4.276 +  moreover have "set (map snd cs') \<subseteq> {0<..}"
4.277 +    unfolding cs'_def using quotient_of_denom_pos' by (auto simp: coeffs_def simp del: upt_Suc)
4.278 +  hence "d \<noteq> 0" unfolding d_def by (induction cs') simp_all
4.279 +  with nz have "p' \<noteq> 0" by (simp add: p'_def)
4.280 +  moreover from root have "poly p' x = 0" by (simp add: p'_def)
4.281 +  ultimately show "algebraic x" unfolding algebraic_def by blast
4.282 +next
4.283 +
4.284 +  assume "algebraic x"
4.285 +  then obtain p where p: "\<And>i. coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0"
4.286 +    by (force simp: algebraic_def)
4.287 +  moreover have "coeff p i \<in> \<int> \<Longrightarrow> coeff p i \<in> \<rat>" for i by (elim Ints_cases) simp
4.288 +  ultimately show  "(\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)" by auto
4.289 +qed
4.290 +
4.291 +
4.292  text\<open>Lemmas for Derivatives\<close>
4.293
4.294  lemma order_unique_lemma:
4.295 @@ -209,12 +415,8 @@
4.296  apply (simp del: power_Suc of_nat_Suc add: pderiv_pCons)
4.297  done
4.298
4.300 -  fixes a b c :: "'a::comm_ring_1"
4.301 -  shows "a dvd b + c \<Longrightarrow> a dvd b \<Longrightarrow> a dvd c"
4.302 -  by (drule (1) Rings.dvd_diff, simp)
4.303 -
4.304  lemma lemma_order_pderiv:
4.305 +  fixes p :: "'a :: field_char_0 poly"
4.306    assumes n: "0 < n"
4.307        and pd: "pderiv p \<noteq> 0"
4.308        and pe: "p = [:- a, 1:] ^ n * q"
4.309 @@ -226,8 +428,8 @@
4.310      using assms by auto
4.311    obtain n' where "n = Suc n'" "0 < Suc n'" "pderiv ([:- a, 1:] ^ Suc n' * q) \<noteq> 0"
4.312      using assms by (cases n) auto
4.313 -  then have *: "!!k l. k dvd k * pderiv q + smult (of_nat (Suc n')) l \<Longrightarrow> k dvd l"
4.314 -    by (metis dvd_add_cancel1 dvd_smult_iff dvd_triv_left of_nat_eq_0_iff old.nat.distinct(2))
4.315 +  have *: "!!k l. k dvd k * pderiv q + smult (of_nat (Suc n')) l \<Longrightarrow> k dvd l"
4.316 +    by (auto simp del: of_nat_Suc simp: dvd_add_right_iff dvd_smult_iff)
4.317    have "n' = order a (pderiv ([:- a, 1:] ^ Suc n' * q))"
4.318    proof (rule order_unique_lemma)
4.319      show "[:- a, 1:] ^ n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
4.320 @@ -262,8 +464,9 @@
4.321    from C D show ?thesis by blast
4.322  qed
4.323
4.324 -lemma order_pderiv: "[| pderiv p \<noteq> 0; order a p \<noteq> 0 |]
4.325 -      ==> (order a p = Suc (order a (pderiv p)))"
4.326 +lemma order_pderiv:
4.327 +  "\<lbrakk>pderiv p \<noteq> 0; order a (p :: 'a :: field_char_0 poly) \<noteq> 0\<rbrakk> \<Longrightarrow>
4.328 +     (order a p = Suc (order a (pderiv p)))"
4.329  apply (case_tac "p = 0", simp)
4.330  apply (drule_tac a = a and p = p in order_decomp)
4.331  using neq0_conv
4.332 @@ -344,7 +547,7 @@
4.333  done
4.334
4.335  lemma poly_squarefree_decomp_order:
4.336 -  assumes "pderiv p \<noteq> 0"
4.337 +  assumes "pderiv (p :: 'a :: field_char_0 poly) \<noteq> 0"
4.338    and p: "p = q * d"
4.339    and p': "pderiv p = e * d"
4.340    and d: "d = r * p + s * pderiv p"
4.341 @@ -379,28 +582,31 @@
4.342      by auto
4.343  qed
4.344
4.345 -lemma poly_squarefree_decomp_order2: "[| pderiv p \<noteq> 0;
4.346 -         p = q * d;
4.347 -         pderiv p = e * d;
4.348 -         d = r * p + s * pderiv p
4.349 -      |] ==> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
4.350 +lemma poly_squarefree_decomp_order2:
4.351 +     "\<lbrakk>pderiv p \<noteq> (0 :: 'a :: field_char_0 poly);
4.352 +       p = q * d;
4.353 +       pderiv p = e * d;
4.354 +       d = r * p + s * pderiv p
4.355 +      \<rbrakk> \<Longrightarrow> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
4.356  by (blast intro: poly_squarefree_decomp_order)
4.357
4.358 -lemma order_pderiv2: "[| pderiv p \<noteq> 0; order a p \<noteq> 0 |]
4.359 -      ==> (order a (pderiv p) = n) = (order a p = Suc n)"
4.360 +lemma order_pderiv2:
4.361 +  "\<lbrakk>pderiv p \<noteq> 0; order a (p :: 'a :: field_char_0 poly) \<noteq> 0\<rbrakk>
4.362 +      \<Longrightarrow> (order a (pderiv p) = n) = (order a p = Suc n)"
4.363  by (auto dest: order_pderiv)
4.364
4.365  definition
4.366    rsquarefree :: "'a::idom poly => bool" where
4.367    "rsquarefree p = (p \<noteq> 0 & (\<forall>a. (order a p = 0) | (order a p = 1)))"
4.368
4.369 -lemma pderiv_iszero: "pderiv p = 0 \<Longrightarrow> \<exists>h. p = [:h:]"
4.370 +lemma pderiv_iszero: "pderiv p = 0 \<Longrightarrow> \<exists>h. p = [:h :: 'a :: {semidom,semiring_char_0}:]"
4.372  apply (case_tac p, auto split: if_splits)
4.373  done
4.374
4.375  lemma rsquarefree_roots:
4.376 -  "rsquarefree p = (\<forall>a. ~(poly p a = 0 & poly (pderiv p) a = 0))"
4.377 +  fixes p :: "'a :: field_char_0 poly"
4.378 +  shows "rsquarefree p = (\<forall>a. \<not>(poly p a = 0 \<and> poly (pderiv p) a = 0))"
4.380  apply (case_tac "p = 0", simp, simp)
4.381  apply (case_tac "pderiv p = 0")
4.382 @@ -411,7 +617,7 @@
4.383  done
4.384
4.385  lemma poly_squarefree_decomp:
4.386 -  assumes "pderiv p \<noteq> 0"
4.387 +  assumes "pderiv (p :: 'a :: field_char_0 poly) \<noteq> 0"
4.388      and "p = q * d"
4.389      and "pderiv p = e * d"
4.390      and "d = r * p + s * pderiv p"
```
```     5.1 --- a/src/HOL/Library/Polynomial.thy	Mon Jan 11 15:20:17 2016 +0100
5.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Jan 11 16:38:39 2016 +0100
5.3 @@ -456,7 +456,7 @@
5.4  lemma poly_0 [simp]:
5.5    "poly 0 x = 0"
5.7 -
5.8 +
5.9  lemma poly_pCons [simp]:
5.10    "poly (pCons a p) x = a + x * poly p x"
5.11    by (cases "p = 0 \<and> a = 0") (auto simp add: poly_def)
5.12 @@ -480,6 +480,9 @@
5.13     qed simp
5.14  qed simp
5.15
5.16 +lemma poly_0_coeff_0: "poly p 0 = coeff p 0"
5.17 +  by (cases p) (auto simp: poly_altdef)
5.18 +
5.19
5.20  subsection \<open>Monomials\<close>
5.21
5.22 @@ -744,6 +747,28 @@
5.23  lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
5.24    by (induct A rule: infinite_finite_induct) simp_all
5.25
5.26 +lemma degree_setsum_le: "finite S \<Longrightarrow> (\<And> p . p \<in> S \<Longrightarrow> degree (f p) \<le> n)
5.27 +  \<Longrightarrow> degree (setsum f S) \<le> n"
5.28 +proof (induct S rule: finite_induct)
5.29 +  case (insert p S)
5.30 +  hence "degree (setsum f S) \<le> n" "degree (f p) \<le> n" by auto
5.31 +  thus ?case unfolding setsum.insert[OF insert(1-2)] by (metis degree_add_le)
5.32 +qed simp
5.33 +
5.34 +lemma poly_as_sum_of_monoms':
5.35 +  assumes n: "degree p \<le> n"
5.36 +  shows "(\<Sum>i\<le>n. monom (coeff p i) i) = p"
5.37 +proof -
5.38 +  have eq: "\<And>i. {..n} \<inter> {i} = (if i \<le> n then {i} else {})"
5.39 +    by auto
5.40 +  show ?thesis
5.41 +    using n by (simp add: poly_eq_iff coeff_setsum coeff_eq_0 setsum.If_cases eq
5.42 +                  if_distrib[where f="\<lambda>x. x * a" for a])
5.43 +qed
5.44 +
5.45 +lemma poly_as_sum_of_monoms: "(\<Sum>i\<le>degree p. monom (coeff p i) i) = p"
5.46 +  by (intro poly_as_sum_of_monoms' order_refl)
5.47 +
5.48  lemma Poly_snoc: "Poly (xs @ [x]) = Poly xs + monom x (length xs)"
5.49    by (induction xs) (simp_all add: monom_0 monom_Suc)
5.50
5.51 @@ -957,7 +982,16 @@
5.52    shows "poly (p ^ n) x = poly p x ^ n"
5.53    by (induct n) simp_all
5.54
5.55 -
5.56 +lemma poly_setprod: "poly (\<Prod>k\<in>A. p k) x = (\<Prod>k\<in>A. poly (p k) x)"
5.57 +  by (induct A rule: infinite_finite_induct) simp_all
5.58 +
5.59 +lemma degree_setprod_setsum_le: "finite S \<Longrightarrow> degree (setprod f S) \<le> setsum (degree o f) S"
5.60 +proof (induct S rule: finite_induct)
5.61 +  case (insert a S)
5.62 +  show ?case unfolding setprod.insert[OF insert(1-2)] setsum.insert[OF insert(1-2)]
5.63 +    by (rule le_trans[OF degree_mult_le], insert insert, auto)
5.64 +qed simp
5.65 +
5.66  subsection \<open>Conversions from natural numbers\<close>
5.67
5.68  lemma of_nat_poly: "of_nat n = [:of_nat n :: 'a :: comm_semiring_1:]"
5.69 @@ -991,7 +1025,7 @@
5.70  qed
5.71
5.72  lemma dvd_smult_cancel:
5.73 -  fixes a :: "'a::field"
5.74 +  fixes a :: "'a :: field"
5.75    shows "p dvd smult a q \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> p dvd q"
5.76    by (drule dvd_smult [where a="inverse a"]) simp
5.77
5.78 @@ -1041,29 +1075,33 @@
5.79  qed
5.80
5.81  lemma degree_mult_eq:
5.82 -  fixes p q :: "'a::idom poly"
5.83 +  fixes p q :: "'a::semidom poly"
5.84    shows "\<lbrakk>p \<noteq> 0; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree (p * q) = degree p + degree q"
5.85  apply (rule order_antisym [OF degree_mult_le le_degree])
5.87  done
5.88
5.89  lemma degree_mult_right_le:
5.90 -  fixes p q :: "'a::idom poly"
5.91 +  fixes p q :: "'a::semidom poly"
5.92    assumes "q \<noteq> 0"
5.93    shows "degree p \<le> degree (p * q)"
5.94    using assms by (cases "p = 0") (simp_all add: degree_mult_eq)
5.95
5.96  lemma coeff_degree_mult:
5.97 -  fixes p q :: "'a::idom poly"
5.98 +  fixes p q :: "'a::semidom poly"
5.99    shows "coeff (p * q) (degree (p * q)) =
5.100      coeff q (degree q) * coeff p (degree p)"
5.101 -  by (cases "p = 0 \<or> q = 0") (auto simp add: degree_mult_eq coeff_mult_degree_sum)
5.102 +  by (cases "p = 0 \<or> q = 0") (auto simp add: degree_mult_eq coeff_mult_degree_sum mult_ac)
5.103
5.104  lemma dvd_imp_degree_le:
5.105 -  fixes p q :: "'a::idom poly"
5.106 +  fixes p q :: "'a::semidom poly"
5.107    shows "\<lbrakk>p dvd q; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree p \<le> degree q"
5.108 -  by (erule dvdE, simp add: degree_mult_eq)
5.109 +  by (erule dvdE, hypsubst, subst degree_mult_eq) auto
5.110
5.111 +lemma divides_degree:
5.112 +  assumes pq: "p dvd (q :: 'a :: semidom poly)"
5.113 +  shows "degree p \<le> degree q \<or> q = 0"
5.114 +  by (metis dvd_imp_degree_le pq)
5.115
5.116  subsection \<open>Polynomials form an ordered integral domain\<close>
5.117
5.118 @@ -2048,18 +2086,27 @@
5.119
5.120  subsection \<open>Composition of polynomials\<close>
5.121
5.122 +(* Several lemmas contributed by René Thiemann and Akihisa Yamada *)
5.123 +
5.124  definition pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
5.125  where
5.126    "pcompose p q = fold_coeffs (\<lambda>a c. [:a:] + q * c) p 0"
5.127
5.128 +notation pcompose (infixl "\<circ>\<^sub>p" 71)
5.129 +
5.130  lemma pcompose_0 [simp]:
5.131    "pcompose 0 q = 0"
5.133 -
5.134 +
5.135  lemma pcompose_pCons:
5.136    "pcompose (pCons a p) q = [:a:] + q * pcompose p q"
5.137    by (cases "p = 0 \<and> a = 0") (auto simp add: pcompose_def)
5.138
5.139 +lemma pcompose_1:
5.140 +  fixes p :: "'a :: comm_semiring_1 poly"
5.141 +  shows "pcompose 1 p = 1"
5.142 +  unfolding one_poly_def by (auto simp: pcompose_pCons)
5.143 +
5.144  lemma poly_pcompose:
5.145    "poly (pcompose p q) x = poly p (poly q x)"
5.146    by (induct p) (simp_all add: pcompose_pCons)
5.147 @@ -2087,7 +2134,7 @@
5.148    finally show ?case .
5.149  qed simp
5.150
5.151 -lemma pcompose_minus:
5.152 +lemma pcompose_uminus:
5.153    fixes p r :: "'a :: comm_ring poly"
5.154    shows "pcompose (-p) r = -pcompose p r"
5.155    by (induction p) (simp_all add: pcompose_pCons)
5.156 @@ -2095,7 +2142,7 @@
5.157  lemma pcompose_diff:
5.158    fixes p q r :: "'a :: comm_ring poly"
5.159    shows "pcompose (p - q) r = pcompose p r - pcompose q r"
5.162
5.163  lemma pcompose_smult:
5.164    fixes p r :: "'a :: comm_semiring_0 poly"
5.165 @@ -2115,24 +2162,27 @@
5.166    by (induction p arbitrary: q)
5.168
5.169 +lemma pcompose_idR[simp]:
5.170 +  fixes p :: "'a :: comm_semiring_1 poly"
5.171 +  shows "pcompose p [: 0, 1 :] = p"
5.172 +  by (induct p; simp add: pcompose_pCons)
5.173 +
5.174
5.175  (* The remainder of this section and the next were contributed by Wenda Li *)
5.176
5.177  lemma degree_mult_eq_0:
5.178 -  fixes p q:: "'a :: idom poly"
5.179 +  fixes p q:: "'a :: semidom poly"
5.180    shows "degree (p*q) = 0 \<longleftrightarrow> p=0 \<or> q=0 \<or> (p\<noteq>0 \<and> q\<noteq>0 \<and> degree p =0 \<and> degree q =0)"
5.182
5.183  lemma pcompose_const[simp]:"pcompose [:a:] q = [:a:]" by (subst pcompose_pCons,simp)
5.184
5.185 -lemma pcompose_0':"pcompose p 0=[:coeff p 0:]"
5.186 -  apply (induct p)
5.187 -  apply (auto simp add:pcompose_pCons)
5.188 -done
5.189 +lemma pcompose_0': "pcompose p 0 = [:coeff p 0:]"
5.190 +  by (induct p) (auto simp add:pcompose_pCons)
5.191
5.192  lemma degree_pcompose:
5.193 -  fixes p q:: "'a::idom poly"
5.194 -  shows "degree(pcompose p q) = degree p * degree q"
5.195 +  fixes p q:: "'a::semidom poly"
5.196 +  shows "degree (pcompose p q) = degree p * degree q"
5.197  proof (induct p)
5.198    case 0
5.199    thus ?case by auto
5.200 @@ -2144,7 +2194,7 @@
5.201        thus ?thesis by auto
5.202      next
5.203        case False assume "degree (q * pcompose p q) = 0"
5.204 -      hence "degree q=0 \<or> pcompose p q=0" by (auto simp add:degree_mult_eq_0)
5.205 +      hence "degree q=0 \<or> pcompose p q=0" by (auto simp add: degree_mult_eq_0)
5.206        moreover have "\<lbrakk>pcompose p q=0;degree q\<noteq>0\<rbrakk> \<Longrightarrow> False" using pCons.hyps(2) \<open>p\<noteq>0\<close>
5.207          proof -
5.208            assume "pcompose p q=0" "degree q\<noteq>0"
5.209 @@ -2178,9 +2228,9 @@
5.210  qed
5.211
5.212  lemma pcompose_eq_0:
5.213 -  fixes p q:: "'a::idom poly"
5.214 -  assumes "pcompose p q=0" "degree q>0"
5.215 -  shows "p=0"
5.216 +  fixes p q:: "'a :: semidom poly"
5.217 +  assumes "pcompose p q = 0" "degree q > 0"
5.218 +  shows "p = 0"
5.219  proof -
5.220    have "degree p=0" using assms degree_pcompose[of p q] by auto
5.221    then obtain a where "p=[:a:]"
```
```     6.1 --- a/src/HOL/Set_Interval.thy	Mon Jan 11 15:20:17 2016 +0100
6.2 +++ b/src/HOL/Set_Interval.thy	Mon Jan 11 16:38:39 2016 +0100
6.3 @@ -1902,4 +1902,52 @@
6.4    finally show ?thesis .
6.5  qed
6.6
6.7 +
6.8 +subsection \<open>Efficient folding over intervals\<close>
6.9 +
6.10 +function fold_atLeastAtMost_nat where
6.11 +  [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc =
6.12 +                 (if a > b then acc else fold_atLeastAtMost_nat f (a+1) b (f a acc))"
6.13 +by pat_completeness auto
6.14 +termination by (relation "measure (\<lambda>(_,a,b,_). Suc b - a)") auto
6.15 +
6.16 +lemma fold_atLeastAtMost_nat:
6.17 +  assumes "comp_fun_commute f"
6.18 +  shows   "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}"
6.19 +using assms
6.20 +proof (induction f a b acc rule: fold_atLeastAtMost_nat.induct, goal_cases)
6.21 +  case (1 f a b acc)
6.22 +  interpret comp_fun_commute f by fact
6.23 +  show ?case
6.24 +  proof (cases "a > b")
6.25 +    case True
6.26 +    thus ?thesis by (subst fold_atLeastAtMost_nat.simps) auto
6.27 +  next
6.28 +    case False
6.29 +    with 1 show ?thesis
6.30 +      by (subst fold_atLeastAtMost_nat.simps)
6.31 +         (auto simp: atLeastAtMost_insertL[symmetric] fold_fun_left_comm)
6.32 +  qed
6.33 +qed
6.34 +
6.35 +lemma setsum_atLeastAtMost_code:
6.36 +  "setsum f {a..b} = fold_atLeastAtMost_nat (\<lambda>a acc. f a + acc) a b 0"
6.37 +proof -
6.38 +  have "comp_fun_commute (\<lambda>a. op + (f a))"
6.39 +    by unfold_locales (auto simp: o_def add_ac)
6.40 +  thus ?thesis
6.41 +    by (simp add: setsum.eq_fold fold_atLeastAtMost_nat o_def)
6.42 +qed
6.43 +
6.44 +lemma setprod_atLeastAtMost_code:
6.45 +  "setprod f {a..b} = fold_atLeastAtMost_nat (\<lambda>a acc. f a * acc) a b 1"
6.46 +proof -
6.47 +  have "comp_fun_commute (\<lambda>a. op * (f a))"
6.48 +    by unfold_locales (auto simp: o_def mult_ac)
6.49 +  thus ?thesis
6.50 +    by (simp add: setprod.eq_fold fold_atLeastAtMost_nat o_def)
6.51 +qed
6.52 +
6.53 +(* TODO: Add support for more kinds of intervals here *)
6.54 +
6.55  end
```