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.21    by (simp add: cCons_def)
    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.52      by (simp add: poly_eq_iff)
    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.73  lemma leading_coeff_0_iff [simp]:
    1.74 @@ -141,7 +141,7 @@
    1.75    by (cases "p = 0", simp, simp add: leading_coeff_neq_0)
    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.131    by (simp add: fold_coeffs_def)
   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.158 +subsection \<open>Addition and subtraction\<close>
   1.159  
   1.160  instantiation poly :: (comm_monoid_add) comm_monoid_add
   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.176 +subsection \<open>Lemmas about divisibility\<close>
   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"
   1.343      by (simp add: degree_mult_eq)
   1.344    with coeff a show "p = q"
   1.345      by (cases a, auto split: if_splits)
   1.346 @@ -1805,7 +1805,7 @@
   1.347    by (simp add: gcd_poly.simps)
   1.348  
   1.349  
   1.350 -subsection {* Composition of polynomials *}
   1.351 +subsection \<open>Composition of polynomials\<close>
   1.352  
   1.353  definition pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   1.354  where