lifting for primitive definitions;
authorhaftmann
Sat Jun 15 17:19:23 2013 +0200 (2013-06-15)
changeset 523803cc46b8cca5e
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
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Library/Poly_Deriv.thy
src/HOL/Library/Polynomial.thy
src/HOL/List.thy
src/HOL/Set_Interval.thy
     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.251  lemma leading_coeff_neq_0:
   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.672  instantiation poly :: (comm_monoid_add) comm_monoid_add
   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.679 -lemma Poly_add:
   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.723  instantiation poly :: (ab_group_add) ab_group_add
   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.801    by (simp add: diff_minus degree_add_less)
   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.929  lemma smult_add_right:
   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.934  lemma smult_add_left:
   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.960    smult_add_left smult_add_right
   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.1045  lemma mult_poly_add_left:
  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 = [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.4  apply(simp add:setsum_head_upt_Suc)
     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: