src/HOL/Library/Polynomial.thy
 changeset 60500 903bb1495239 parent 60429 d3d1e185cd63 child 60562 24af00b010cf
```     1.1 --- a/src/HOL/Library/Polynomial.thy	Wed Jun 17 10:57:11 2015 +0200
1.2 +++ b/src/HOL/Library/Polynomial.thy	Wed Jun 17 11:03:05 2015 +0200
1.3 @@ -4,13 +4,13 @@
1.4      Author:     Florian Haftmann
1.5  *)
1.6
1.7 -section {* Polynomials as type over a ring structure *}
1.8 +section \<open>Polynomials as type over a ring structure\<close>
1.9
1.10  theory Polynomial
1.11  imports Main GCD "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Infinite_Set"
1.12  begin
1.13
1.14 -subsection {* Auxiliary: operations for lists (later) representing coefficients *}
1.15 +subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
1.16
1.17  definition cCons :: "'a::zero \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixr "##" 65)
1.18  where
1.19 @@ -50,7 +50,7 @@
1.20    "tl (x ## xs) = xs"
1.22
1.23 -subsection {* Definition of type @{text poly} *}
1.24 +subsection \<open>Definition of type @{text poly}\<close>
1.25
1.26  typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
1.27    morphisms coeff Abs_poly by (auto intro!: ALL_MOST)
1.28 @@ -67,7 +67,7 @@
1.29    using coeff [of p] by simp
1.30
1.31
1.32 -subsection {* Degree of a polynomial *}
1.33 +subsection \<open>Degree of a polynomial\<close>
1.34
1.35  definition degree :: "'a::zero poly \<Rightarrow> nat"
1.36  where
1.37 @@ -94,7 +94,7 @@
1.38    unfolding degree_def by (drule not_less_Least, simp)
1.39
1.40
1.41 -subsection {* The zero polynomial *}
1.42 +subsection \<open>The zero polynomial\<close>
1.43
1.44  instantiation poly :: (zero) zero
1.45  begin
1.46 @@ -119,21 +119,21 @@
1.47    shows "coeff p (degree p) \<noteq> 0"
1.48  proof (cases "degree p")
1.49    case 0
1.50 -  from `p \<noteq> 0` have "\<exists>n. coeff p n \<noteq> 0"
1.51 +  from \<open>p \<noteq> 0\<close> have "\<exists>n. coeff p n \<noteq> 0"
1.53    then obtain n where "coeff p n \<noteq> 0" ..
1.54    hence "n \<le> degree p" by (rule le_degree)
1.55 -  with `coeff p n \<noteq> 0` and `degree p = 0`
1.56 +  with \<open>coeff p n \<noteq> 0\<close> and \<open>degree p = 0\<close>
1.57    show "coeff p (degree p) \<noteq> 0" by simp
1.58  next
1.59    case (Suc n)
1.60 -  from `degree p = Suc n` have "n < degree p" by simp
1.61 +  from \<open>degree p = Suc n\<close> have "n < degree p" by simp
1.62    hence "\<exists>i>n. coeff p i \<noteq> 0" by (rule less_degree_imp)
1.63    then obtain i where "n < i" and "coeff p i \<noteq> 0" by fast
1.64 -  from `degree p = Suc n` and `n < i` have "degree p \<le> i" by simp
1.65 -  also from `coeff p i \<noteq> 0` have "i \<le> degree p" by (rule le_degree)
1.66 +  from \<open>degree p = Suc n\<close> and \<open>n < i\<close> have "degree p \<le> i" by simp
1.67 +  also from \<open>coeff p i \<noteq> 0\<close> have "i \<le> degree p" by (rule le_degree)
1.68    finally have "degree p = i" .
1.69 -  with `coeff p i \<noteq> 0` show "coeff p (degree p) \<noteq> 0" by simp
1.70 +  with \<open>coeff p i \<noteq> 0\<close> show "coeff p (degree p) \<noteq> 0" by simp
1.71  qed
1.72
1.74 @@ -141,7 +141,7 @@
1.76
1.77
1.78 -subsection {* List-style constructor for polynomials *}
1.79 +subsection \<open>List-style constructor for polynomials\<close>
1.80
1.81  lift_definition pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
1.82    is "\<lambda>a p. case_nat a (coeff p)"
1.83 @@ -228,24 +228,24 @@
1.84      then have "degree (pCons a q) = Suc (degree q)"
1.85        by (rule degree_pCons_eq)
1.86      then have "degree q < degree p"
1.87 -      using `p = pCons a q` by simp
1.88 +      using \<open>p = pCons a q\<close> by simp
1.89      then show "P q"
1.90        by (rule less.hyps)
1.91    qed
1.92    have "P (pCons a q)"
1.93    proof (cases "a \<noteq> 0 \<or> q \<noteq> 0")
1.94      case True
1.95 -    with `P q` show ?thesis by (auto intro: pCons)
1.96 +    with \<open>P q\<close> show ?thesis by (auto intro: pCons)
1.97    next
1.98      case False
1.99      with zero show ?thesis by simp
1.100    qed
1.101    then show ?case
1.102 -    using `p = pCons a q` by simp
1.103 +    using \<open>p = pCons a q\<close> by simp
1.104  qed
1.105
1.106
1.107 -subsection {* List-style syntax for polynomials *}
1.108 +subsection \<open>List-style syntax for polynomials\<close>
1.109
1.110  syntax
1.111    "_poly" :: "args \<Rightarrow> 'a poly"  ("[:(_):]")
1.112 @@ -256,7 +256,7 @@
1.113    "[:x:]" <= "CONST pCons x (_constrain 0 t)"
1.114
1.115
1.116 -subsection {* Representation of polynomials by lists of coefficients *}
1.117 +subsection \<open>Representation of polynomials by lists of coefficients\<close>
1.118
1.119  primrec Poly :: "'a::zero list \<Rightarrow> 'a poly"
1.120  where
1.121 @@ -399,7 +399,7 @@
1.122    by (simp add: is_zero_def null_def)
1.123
1.124
1.125 -subsection {* Fold combinator for polynomials *}
1.126 +subsection \<open>Fold combinator for polynomials\<close>
1.127
1.128  definition fold_coeffs :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b"
1.129  where
1.130 @@ -426,11 +426,11 @@
1.132
1.133
1.134 -subsection {* Canonical morphism on polynomials -- evaluation *}
1.135 +subsection \<open>Canonical morphism on polynomials -- evaluation\<close>
1.136
1.137  definition poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a"
1.138  where
1.139 -  "poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)" -- {* The Horner Schema *}
1.140 +  "poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)" -- \<open>The Horner Schema\<close>
1.141
1.142  lemma poly_0 [simp]:
1.143    "poly 0 x = 0"
1.144 @@ -441,7 +441,7 @@
1.145    by (cases "p = 0 \<and> a = 0") (auto simp add: poly_def)
1.146
1.147
1.148 -subsection {* Monomials *}
1.149 +subsection \<open>Monomials\<close>
1.150
1.151  lift_definition monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly"
1.152    is "\<lambda>a m n. if m = n then a else 0"
1.153 @@ -491,7 +491,7 @@
1.154      (induct n, simp_all add: mult.left_commute poly_def)
1.155
1.156
1.157 -subsection {* Addition and subtraction *}
1.159
1.161  begin
1.162 @@ -700,7 +700,7 @@
1.163    by (induct A rule: infinite_finite_induct) simp_all
1.164
1.165
1.166 -subsection {* Multiplication by a constant, polynomial multiplication and the unit polynomial *}
1.167 +subsection \<open>Multiplication by a constant, polynomial multiplication and the unit polynomial\<close>
1.168
1.169  lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
1.170    is "\<lambda>a p n. a * coeff p n"
1.171 @@ -908,7 +908,7 @@
1.172    by (induct n) simp_all
1.173
1.174
1.175 -subsection {* Lemmas about divisibility *}
1.177
1.178  lemma dvd_smult: "p dvd q \<Longrightarrow> p dvd smult a q"
1.179  proof -
1.180 @@ -948,7 +948,7 @@
1.181    by (auto elim: smult_dvd smult_dvd_cancel)
1.182
1.183
1.184 -subsection {* Polynomials form an integral domain *}
1.185 +subsection \<open>Polynomials form an integral domain\<close>
1.186
1.187  lemma coeff_mult_degree_sum:
1.188    "coeff (p * q) (degree p + degree q) =
1.189 @@ -963,7 +963,7 @@
1.190          coeff p (degree p) * coeff q (degree q)"
1.191      by (rule coeff_mult_degree_sum)
1.192    also have "coeff p (degree p) * coeff q (degree q) \<noteq> 0"
1.193 -    using `p \<noteq> 0` and `q \<noteq> 0` by simp
1.194 +    using \<open>p \<noteq> 0\<close> and \<open>q \<noteq> 0\<close> by simp
1.195    finally have "\<exists>n. coeff (p * q) n \<noteq> 0" ..
1.196    thus "p * q \<noteq> 0" by (simp add: poly_eq_iff)
1.197  qed
1.198 @@ -981,7 +981,7 @@
1.199    by (erule dvdE, simp add: degree_mult_eq)
1.200
1.201
1.202 -subsection {* Polynomials form an ordered integral domain *}
1.203 +subsection \<open>Polynomials form an ordered integral domain\<close>
1.204
1.205  definition pos_poly :: "'a::linordered_idom poly \<Rightarrow> bool"
1.206  where
1.207 @@ -1097,14 +1097,14 @@
1.208
1.209  end
1.210
1.211 -text {* TODO: Simplification rules for comparisons *}
1.212 +text \<open>TODO: Simplification rules for comparisons\<close>
1.213
1.214
1.215 -subsection {* Synthetic division and polynomial roots *}
1.216 +subsection \<open>Synthetic division and polynomial roots\<close>
1.217
1.218 -text {*
1.219 +text \<open>
1.220    Synthetic division is simply division by the linear polynomial @{term "x - c"}.
1.221 -*}
1.222 +\<close>
1.223
1.224  definition synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a"
1.225  where
1.226 @@ -1201,11 +1201,11 @@
1.227      then obtain a where "poly p a = 0" ..
1.228      then have "[:-a, 1:] dvd p" by (simp only: poly_eq_0_iff_dvd)
1.229      then obtain k where k: "p = [:-a, 1:] * k" ..
1.230 -    with `p \<noteq> 0` have "k \<noteq> 0" by auto
1.231 +    with \<open>p \<noteq> 0\<close> have "k \<noteq> 0" by auto
1.232      with k have "degree p = Suc (degree k)"
1.233        by (simp add: degree_mult_eq del: mult_pCons_left)
1.234 -    with `Suc n = degree p` have "n = degree k" by simp
1.235 -    then have "finite {x. poly k x = 0}" using `k \<noteq> 0` by (rule Suc.hyps)
1.236 +    with \<open>Suc n = degree p\<close> have "n = degree k" by simp
1.237 +    then have "finite {x. poly k x = 0}" using \<open>k \<noteq> 0\<close> by (rule Suc.hyps)
1.238      then have "finite (insert a {x. poly k x = 0})" by simp
1.239      then show "finite {x. poly p x = 0}"
1.240        by (simp add: k Collect_disj_eq del: mult_pCons_left)
1.241 @@ -1235,7 +1235,7 @@
1.242    by (auto simp add: poly_eq_poly_eq_iff [symmetric])
1.243
1.244
1.245 -subsection {* Long division of polynomials *}
1.246 +subsection \<open>Long division of polynomials\<close>
1.247
1.248  definition pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
1.249  where
1.250 @@ -1255,22 +1255,22 @@
1.251    shows "p = 0 \<or> degree p < n"
1.252  proof (cases n)
1.253    case 0
1.254 -  with `degree p \<le> n` and `coeff p n = 0`
1.255 +  with \<open>degree p \<le> n\<close> and \<open>coeff p n = 0\<close>
1.256    have "coeff p (degree p) = 0" by simp
1.257    then have "p = 0" by simp
1.258    then show ?thesis ..
1.259  next
1.260    case (Suc m)
1.261    have "\<forall>i>n. coeff p i = 0"
1.262 -    using `degree p \<le> n` by (simp add: coeff_eq_0)
1.263 +    using \<open>degree p \<le> n\<close> by (simp add: coeff_eq_0)
1.264    then have "\<forall>i\<ge>n. coeff p i = 0"
1.265 -    using `coeff p n = 0` by (simp add: le_less)
1.266 +    using \<open>coeff p n = 0\<close> by (simp add: le_less)
1.267    then have "\<forall>i>m. coeff p i = 0"
1.268 -    using `n = Suc m` by (simp add: less_eq_Suc_le)
1.269 +    using \<open>n = Suc m\<close> by (simp add: less_eq_Suc_le)
1.270    then have "degree p \<le> m"
1.271      by (rule degree_le)
1.272    then have "degree p < n"
1.273 -    using `n = Suc m` by (simp add: less_Suc_eq_le)
1.274 +    using \<open>n = Suc m\<close> by (simp add: less_Suc_eq_le)
1.275    then show ?thesis ..
1.276  qed
1.277
1.278 @@ -1298,12 +1298,12 @@
1.279      qed
1.280    next
1.281      show "coeff ?r (degree y) = 0"
1.282 -      using `y \<noteq> 0` unfolding b by simp
1.283 +      using \<open>y \<noteq> 0\<close> unfolding b by simp
1.284    qed
1.285
1.286    from 1 2 show ?thesis
1.287      unfolding pdivmod_rel_def
1.288 -    using `y \<noteq> 0` by simp
1.289 +    using \<open>y \<noteq> 0\<close> by simp
1.290  qed
1.291
1.292  lemma pdivmod_rel_exists: "\<exists>q r. pdivmod_rel x y q r"
1.293 @@ -1339,7 +1339,7 @@
1.294      with r3 have "degree (r2 - r1) < degree y" by simp
1.295      also have "degree y \<le> degree (q1 - q2) + degree y" by simp
1.296      also have "\<dots> = degree ((q1 - q2) * y)"
1.297 -      using `q1 \<noteq> q2` by (simp add: degree_mult_eq)
1.298 +      using \<open>q1 \<noteq> q2\<close> by (simp add: degree_mult_eq)
1.299      also have "\<dots> = degree (r2 - r1)"
1.300        using q3 by simp
1.301      finally have "degree (r2 - r1) < degree (r2 - r1)" .
1.302 @@ -1426,7 +1426,7 @@
1.303      case False then show ?thesis by auto
1.304    next
1.305      case True then have "y \<noteq> 0" and "z \<noteq> 0" by auto
1.306 -    with `x \<noteq> 0`
1.307 +    with \<open>x \<noteq> 0\<close>
1.308      have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
1.309        by (auto simp add: pdivmod_rel_def algebra_simps)
1.310          (rule classical, simp add: degree_mult_eq)
1.311 @@ -1611,7 +1611,7 @@
1.312    done
1.313
1.314
1.315 -subsection {* Order of polynomial roots *}
1.316 +subsection \<open>Order of polynomial roots\<close>
1.317
1.318  definition order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat"
1.319  where
1.320 @@ -1674,7 +1674,7 @@
1.321  done
1.322
1.323
1.324 -subsection {* GCD of polynomials *}
1.325 +subsection \<open>GCD of polynomials\<close>
1.326
1.327  instantiation poly :: (field) gcd
1.328  begin
1.329 @@ -1745,12 +1745,12 @@
1.330  next
1.331    case False with coeff have "q \<noteq> 0" by auto
1.332    have degree: "degree p = degree q"
1.333 -    using `p dvd q` `q dvd p` `p \<noteq> 0` `q \<noteq> 0`
1.334 +    using \<open>p dvd q\<close> \<open>q dvd p\<close> \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close>
1.335      by (intro order_antisym dvd_imp_degree_le)
1.336
1.337 -  from `p dvd q` obtain a where a: "q = p * a" ..
1.338 -  with `q \<noteq> 0` have "a \<noteq> 0" by auto
1.339 -  with degree a `p \<noteq> 0` have "degree a = 0"
1.340 +  from \<open>p dvd q\<close> obtain a where a: "q = p * a" ..
1.341 +  with \<open>q \<noteq> 0\<close> have "a \<noteq> 0" by auto
1.342 +  with degree a \<open>p \<noteq> 0\<close> have "degree a = 0"