src/HOL/Computational_Algebra/Polynomial.thy
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (17 months ago)
changeset 67091 1393c2340eec
parent 66806 a4e82b58d833
child 67369 7360fe6bb423
permissions -rw-r--r--
more symbols;
wenzelm@65435
     1
(*  Title:      HOL/Computational_Algebra/Polynomial.thy
huffman@29451
     2
    Author:     Brian Huffman
wenzelm@41959
     3
    Author:     Clemens Ballarin
haftmann@62352
     4
    Author:     Amine Chaieb
haftmann@52380
     5
    Author:     Florian Haftmann
huffman@29451
     6
*)
huffman@29451
     7
wenzelm@60500
     8
section \<open>Polynomials as type over a ring structure\<close>
huffman@29451
     9
huffman@29451
    10
theory Polynomial
haftmann@65417
    11
imports
wenzelm@66453
    12
  HOL.Deriv
wenzelm@66453
    13
  "HOL-Library.More_List"
wenzelm@66453
    14
  "HOL-Library.Infinite_Set"
haftmann@66805
    15
  Factorial_Ring
huffman@29451
    16
begin
huffman@29451
    17
wenzelm@60500
    18
subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
haftmann@52380
    19
haftmann@52380
    20
definition cCons :: "'a::zero \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixr "##" 65)
wenzelm@65346
    21
  where "x ## xs = (if xs = [] \<and> x = 0 then [] else x # xs)"
wenzelm@65346
    22
wenzelm@65346
    23
lemma cCons_0_Nil_eq [simp]: "0 ## [] = []"
haftmann@52380
    24
  by (simp add: cCons_def)
haftmann@52380
    25
wenzelm@65346
    26
lemma cCons_Cons_eq [simp]: "x ## y # ys = x # y # ys"
haftmann@52380
    27
  by (simp add: cCons_def)
haftmann@52380
    28
wenzelm@65346
    29
lemma cCons_append_Cons_eq [simp]: "x ## xs @ y # ys = x # xs @ y # ys"
haftmann@52380
    30
  by (simp add: cCons_def)
haftmann@52380
    31
wenzelm@65346
    32
lemma cCons_not_0_eq [simp]: "x \<noteq> 0 \<Longrightarrow> x ## xs = x # xs"
haftmann@52380
    33
  by (simp add: cCons_def)
haftmann@52380
    34
haftmann@52380
    35
lemma strip_while_not_0_Cons_eq [simp]:
haftmann@52380
    36
  "strip_while (\<lambda>x. x = 0) (x # xs) = x ## strip_while (\<lambda>x. x = 0) xs"
haftmann@52380
    37
proof (cases "x = 0")
wenzelm@65346
    38
  case False
wenzelm@65346
    39
  then show ?thesis by simp
haftmann@52380
    40
next
wenzelm@65346
    41
  case True
wenzelm@65346
    42
  show ?thesis
haftmann@52380
    43
  proof (induct xs rule: rev_induct)
wenzelm@65346
    44
    case Nil
wenzelm@65346
    45
    with True show ?case by simp
haftmann@52380
    46
  next
wenzelm@65346
    47
    case (snoc y ys)
wenzelm@65346
    48
    then show ?case
haftmann@52380
    49
      by (cases "y = 0") (simp_all add: append_Cons [symmetric] del: append_Cons)
haftmann@52380
    50
  qed
haftmann@52380
    51
qed
haftmann@52380
    52
wenzelm@65346
    53
lemma tl_cCons [simp]: "tl (x ## xs) = xs"
haftmann@52380
    54
  by (simp add: cCons_def)
haftmann@52380
    55
wenzelm@65346
    56
wenzelm@61585
    57
subsection \<open>Definition of type \<open>poly\<close>\<close>
huffman@29451
    58
wenzelm@61260
    59
typedef (overloaded) 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
wenzelm@63433
    60
  morphisms coeff Abs_poly
wenzelm@63433
    61
  by (auto intro!: ALL_MOST)
huffman@29451
    62
haftmann@59487
    63
setup_lifting type_definition_poly
haftmann@52380
    64
haftmann@52380
    65
lemma poly_eq_iff: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
wenzelm@45694
    66
  by (simp add: coeff_inject [symmetric] fun_eq_iff)
huffman@29451
    67
haftmann@52380
    68
lemma poly_eqI: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
haftmann@52380
    69
  by (simp add: poly_eq_iff)
haftmann@52380
    70
hoelzl@59983
    71
lemma MOST_coeff_eq_0: "\<forall>\<^sub>\<infinity> n. coeff p n = 0"
haftmann@52380
    72
  using coeff [of p] by simp
huffman@29451
    73
huffman@29451
    74
wenzelm@60500
    75
subsection \<open>Degree of a polynomial\<close>
huffman@29451
    76
haftmann@52380
    77
definition degree :: "'a::zero poly \<Rightarrow> nat"
wenzelm@65346
    78
  where "degree p = (LEAST n. \<forall>i>n. coeff p i = 0)"
huffman@29451
    79
haftmann@52380
    80
lemma coeff_eq_0:
haftmann@52380
    81
  assumes "degree p < n"
haftmann@52380
    82
  shows "coeff p n = 0"
huffman@29451
    83
proof -
hoelzl@59983
    84
  have "\<exists>n. \<forall>i>n. coeff p i = 0"
hoelzl@59983
    85
    using MOST_coeff_eq_0 by (simp add: MOST_nat)
haftmann@52380
    86
  then have "\<forall>i>degree p. coeff p i = 0"
huffman@29451
    87
    unfolding degree_def by (rule LeastI_ex)
haftmann@52380
    88
  with assms show ?thesis by simp
huffman@29451
    89
qed
huffman@29451
    90
huffman@29451
    91
lemma le_degree: "coeff p n \<noteq> 0 \<Longrightarrow> n \<le> degree p"
huffman@29451
    92
  by (erule contrapos_np, rule coeff_eq_0, simp)
huffman@29451
    93
huffman@29451
    94
lemma degree_le: "\<forall>i>n. coeff p i = 0 \<Longrightarrow> degree p \<le> n"
huffman@29451
    95
  unfolding degree_def by (erule Least_le)
huffman@29451
    96
huffman@29451
    97
lemma less_degree_imp: "n < degree p \<Longrightarrow> \<exists>i>n. coeff p i \<noteq> 0"
huffman@29451
    98
  unfolding degree_def by (drule not_less_Least, simp)
huffman@29451
    99
huffman@29451
   100
wenzelm@60500
   101
subsection \<open>The zero polynomial\<close>
huffman@29451
   102
huffman@29451
   103
instantiation poly :: (zero) zero
huffman@29451
   104
begin
huffman@29451
   105
haftmann@52380
   106
lift_definition zero_poly :: "'a poly"
haftmann@65390
   107
  is "\<lambda>_. 0"
haftmann@65390
   108
  by (rule MOST_I) simp
huffman@29451
   109
huffman@29451
   110
instance ..
haftmann@52380
   111
huffman@29451
   112
end
huffman@29451
   113
wenzelm@65346
   114
lemma coeff_0 [simp]: "coeff 0 n = 0"
haftmann@52380
   115
  by transfer rule
huffman@29451
   116
wenzelm@65346
   117
lemma degree_0 [simp]: "degree 0 = 0"
huffman@29451
   118
  by (rule order_antisym [OF degree_le le0]) simp
huffman@29451
   119
huffman@29451
   120
lemma leading_coeff_neq_0:
haftmann@52380
   121
  assumes "p \<noteq> 0"
haftmann@52380
   122
  shows "coeff p (degree p) \<noteq> 0"
huffman@29451
   123
proof (cases "degree p")
huffman@29451
   124
  case 0
wenzelm@65346
   125
  from \<open>p \<noteq> 0\<close> obtain n where "coeff p n \<noteq> 0"
wenzelm@65346
   126
    by (auto simp add: poly_eq_iff)
wenzelm@65346
   127
  then have "n \<le> degree p"
wenzelm@65346
   128
    by (rule le_degree)
wenzelm@65346
   129
  with \<open>coeff p n \<noteq> 0\<close> and \<open>degree p = 0\<close> show "coeff p (degree p) \<noteq> 0"
wenzelm@65346
   130
    by simp
huffman@29451
   131
next
huffman@29451
   132
  case (Suc n)
wenzelm@65346
   133
  from \<open>degree p = Suc n\<close> have "n < degree p"
wenzelm@65346
   134
    by simp
wenzelm@65346
   135
  then have "\<exists>i>n. coeff p i \<noteq> 0"
wenzelm@65346
   136
    by (rule less_degree_imp)
wenzelm@65346
   137
  then obtain i where "n < i" and "coeff p i \<noteq> 0"
wenzelm@65346
   138
    by blast
wenzelm@65346
   139
  from \<open>degree p = Suc n\<close> and \<open>n < i\<close> have "degree p \<le> i"
wenzelm@65346
   140
    by simp
wenzelm@65346
   141
  also from \<open>coeff p i \<noteq> 0\<close> have "i \<le> degree p"
wenzelm@65346
   142
    by (rule le_degree)
huffman@29451
   143
  finally have "degree p = i" .
wenzelm@60500
   144
  with \<open>coeff p i \<noteq> 0\<close> show "coeff p (degree p) \<noteq> 0" by simp
huffman@29451
   145
qed
huffman@29451
   146
wenzelm@65346
   147
lemma leading_coeff_0_iff [simp]: "coeff p (degree p) = 0 \<longleftrightarrow> p = 0"
wenzelm@65346
   148
  by (cases "p = 0") (simp_all add: leading_coeff_neq_0)
huffman@29451
   149
haftmann@64795
   150
lemma eq_zero_or_degree_less:
haftmann@64795
   151
  assumes "degree p \<le> n" and "coeff p n = 0"
haftmann@64795
   152
  shows "p = 0 \<or> degree p < n"
haftmann@64795
   153
proof (cases n)
haftmann@64795
   154
  case 0
wenzelm@65346
   155
  with \<open>degree p \<le> n\<close> and \<open>coeff p n = 0\<close> have "coeff p (degree p) = 0"
wenzelm@65346
   156
    by simp
haftmann@64795
   157
  then have "p = 0" by simp
haftmann@64795
   158
  then show ?thesis ..
haftmann@64795
   159
next
haftmann@64795
   160
  case (Suc m)
wenzelm@65346
   161
  from \<open>degree p \<le> n\<close> have "\<forall>i>n. coeff p i = 0"
wenzelm@65346
   162
    by (simp add: coeff_eq_0)
wenzelm@65346
   163
  with \<open>coeff p n = 0\<close> have "\<forall>i\<ge>n. coeff p i = 0"
wenzelm@65346
   164
    by (simp add: le_less)
wenzelm@65346
   165
  with \<open>n = Suc m\<close> have "\<forall>i>m. coeff p i = 0"
wenzelm@65346
   166
    by (simp add: less_eq_Suc_le)
haftmann@64795
   167
  then have "degree p \<le> m"
haftmann@64795
   168
    by (rule degree_le)
wenzelm@65346
   169
  with \<open>n = Suc m\<close> have "degree p < n"
wenzelm@65346
   170
    by (simp add: less_Suc_eq_le)
haftmann@64795
   171
  then show ?thesis ..
haftmann@64795
   172
qed
haftmann@64795
   173
haftmann@64795
   174
lemma coeff_0_degree_minus_1: "coeff rrr dr = 0 \<Longrightarrow> degree rrr \<le> dr \<Longrightarrow> degree rrr \<le> dr - 1"
haftmann@64795
   175
  using eq_zero_or_degree_less by fastforce
haftmann@64795
   176
huffman@29451
   177
wenzelm@60500
   178
subsection \<open>List-style constructor for polynomials\<close>
huffman@29451
   179
haftmann@52380
   180
lift_definition pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
blanchet@55415
   181
  is "\<lambda>a p. case_nat a (coeff p)"
hoelzl@59983
   182
  by (rule MOST_SucD) (simp add: MOST_coeff_eq_0)
huffman@29451
   183
haftmann@52380
   184
lemmas coeff_pCons = pCons.rep_eq
huffman@29455
   185
wenzelm@65346
   186
lemma coeff_pCons_0 [simp]: "coeff (pCons a p) 0 = a"
haftmann@52380
   187
  by transfer simp
huffman@29455
   188
wenzelm@65346
   189
lemma coeff_pCons_Suc [simp]: "coeff (pCons a p) (Suc n) = coeff p n"
huffman@29451
   190
  by (simp add: coeff_pCons)
huffman@29451
   191
wenzelm@65346
   192
lemma degree_pCons_le: "degree (pCons a p) \<le> Suc (degree p)"
haftmann@52380
   193
  by (rule degree_le) (simp add: coeff_eq_0 coeff_pCons split: nat.split)
huffman@29451
   194
wenzelm@65346
   195
lemma degree_pCons_eq: "p \<noteq> 0 \<Longrightarrow> degree (pCons a p) = Suc (degree p)"
haftmann@52380
   196
  apply (rule order_antisym [OF degree_pCons_le])
haftmann@52380
   197
  apply (rule le_degree, simp)
haftmann@52380
   198
  done
huffman@29451
   199
wenzelm@65346
   200
lemma degree_pCons_0: "degree (pCons a 0) = 0"
haftmann@52380
   201
  apply (rule order_antisym [OF _ le0])
haftmann@52380
   202
  apply (rule degree_le, simp add: coeff_pCons split: nat.split)
haftmann@52380
   203
  done
huffman@29451
   204
wenzelm@65346
   205
lemma degree_pCons_eq_if [simp]: "degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))"
haftmann@52380
   206
  apply (cases "p = 0", simp_all)
haftmann@52380
   207
  apply (rule order_antisym [OF _ le0])
haftmann@52380
   208
  apply (rule degree_le, simp add: coeff_pCons split: nat.split)
haftmann@52380
   209
  apply (rule order_antisym [OF degree_pCons_le])
haftmann@52380
   210
  apply (rule le_degree, simp)
haftmann@52380
   211
  done
huffman@29451
   212
wenzelm@65346
   213
lemma pCons_0_0 [simp]: "pCons 0 0 = 0"
haftmann@52380
   214
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
huffman@29451
   215
wenzelm@65346
   216
lemma pCons_eq_iff [simp]: "pCons a p = pCons b q \<longleftrightarrow> a = b \<and> p = q"
haftmann@52380
   217
proof safe
huffman@29451
   218
  assume "pCons a p = pCons b q"
wenzelm@65346
   219
  then have "coeff (pCons a p) 0 = coeff (pCons b q) 0"
wenzelm@65346
   220
    by simp
wenzelm@65346
   221
  then show "a = b"
wenzelm@65346
   222
    by simp
huffman@29451
   223
next
huffman@29451
   224
  assume "pCons a p = pCons b q"
wenzelm@65346
   225
  then have "coeff (pCons a p) (Suc n) = coeff (pCons b q) (Suc n)" for n
wenzelm@65346
   226
    by simp
wenzelm@65346
   227
  then show "p = q"
wenzelm@65346
   228
    by (simp add: poly_eq_iff)
huffman@29451
   229
qed
huffman@29451
   230
wenzelm@65346
   231
lemma pCons_eq_0_iff [simp]: "pCons a p = 0 \<longleftrightarrow> a = 0 \<and> p = 0"
huffman@29451
   232
  using pCons_eq_iff [of a p 0 0] by simp
huffman@29451
   233
huffman@29451
   234
lemma pCons_cases [cases type: poly]:
huffman@29451
   235
  obtains (pCons) a q where "p = pCons a q"
huffman@29451
   236
proof
huffman@29451
   237
  show "p = pCons (coeff p 0) (Abs_poly (\<lambda>n. coeff p (Suc n)))"
haftmann@52380
   238
    by transfer
wenzelm@65346
   239
      (simp_all add: MOST_inj[where f=Suc and P="\<lambda>n. p n = 0" for p] fun_eq_iff Abs_poly_inverse
wenzelm@65346
   240
        split: nat.split)
huffman@29451
   241
qed
huffman@29451
   242
huffman@29451
   243
lemma pCons_induct [case_names 0 pCons, induct type: poly]:
huffman@29451
   244
  assumes zero: "P 0"
haftmann@54856
   245
  assumes pCons: "\<And>a p. a \<noteq> 0 \<or> p \<noteq> 0 \<Longrightarrow> P p \<Longrightarrow> P (pCons a p)"
huffman@29451
   246
  shows "P p"
huffman@29451
   247
proof (induct p rule: measure_induct_rule [where f=degree])
huffman@29451
   248
  case (less p)
huffman@29451
   249
  obtain a q where "p = pCons a q" by (rule pCons_cases)
huffman@29451
   250
  have "P q"
huffman@29451
   251
  proof (cases "q = 0")
huffman@29451
   252
    case True
huffman@29451
   253
    then show "P q" by (simp add: zero)
huffman@29451
   254
  next
huffman@29451
   255
    case False
huffman@29451
   256
    then have "degree (pCons a q) = Suc (degree q)"
huffman@29451
   257
      by (rule degree_pCons_eq)
wenzelm@65346
   258
    with \<open>p = pCons a q\<close> have "degree q < degree p"
wenzelm@65346
   259
      by simp
huffman@29451
   260
    then show "P q"
huffman@29451
   261
      by (rule less.hyps)
huffman@29451
   262
  qed
haftmann@54856
   263
  have "P (pCons a q)"
haftmann@54856
   264
  proof (cases "a \<noteq> 0 \<or> q \<noteq> 0")
haftmann@54856
   265
    case True
wenzelm@60500
   266
    with \<open>P q\<close> show ?thesis by (auto intro: pCons)
haftmann@54856
   267
  next
haftmann@54856
   268
    case False
haftmann@54856
   269
    with zero show ?thesis by simp
haftmann@54856
   270
  qed
wenzelm@65346
   271
  with \<open>p = pCons a q\<close> show ?case
wenzelm@65346
   272
    by simp
huffman@29451
   273
qed
huffman@29451
   274
haftmann@60570
   275
lemma degree_eq_zeroE:
haftmann@60570
   276
  fixes p :: "'a::zero poly"
haftmann@60570
   277
  assumes "degree p = 0"
haftmann@60570
   278
  obtains a where "p = pCons a 0"
haftmann@60570
   279
proof -
wenzelm@65346
   280
  obtain a q where p: "p = pCons a q"
wenzelm@65346
   281
    by (cases p)
wenzelm@65346
   282
  with assms have "q = 0"
wenzelm@65346
   283
    by (cases "q = 0") simp_all
wenzelm@65346
   284
  with p have "p = pCons a 0"
wenzelm@65346
   285
    by simp
wenzelm@65346
   286
  then show thesis ..
haftmann@60570
   287
qed
haftmann@60570
   288
huffman@29451
   289
eberlm@62422
   290
subsection \<open>Quickcheck generator for polynomials\<close>
eberlm@62422
   291
eberlm@62422
   292
quickcheck_generator poly constructors: "0 :: _ poly", pCons
eberlm@62422
   293
eberlm@62422
   294
wenzelm@60500
   295
subsection \<open>List-style syntax for polynomials\<close>
haftmann@52380
   296
wenzelm@65346
   297
syntax "_poly" :: "args \<Rightarrow> 'a poly"  ("[:(_):]")
haftmann@52380
   298
translations
wenzelm@65346
   299
  "[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]"
wenzelm@65346
   300
  "[:x:]" \<rightleftharpoons> "CONST pCons x 0"
wenzelm@65346
   301
  "[:x:]" \<leftharpoondown> "CONST pCons x (_constrain 0 t)"
haftmann@52380
   302
haftmann@52380
   303
wenzelm@60500
   304
subsection \<open>Representation of polynomials by lists of coefficients\<close>
haftmann@52380
   305
haftmann@52380
   306
primrec Poly :: "'a::zero list \<Rightarrow> 'a poly"
wenzelm@65346
   307
  where
wenzelm@65346
   308
    [code_post]: "Poly [] = 0"
wenzelm@65346
   309
  | [code_post]: "Poly (a # as) = pCons a (Poly as)"
wenzelm@65346
   310
wenzelm@65346
   311
lemma Poly_replicate_0 [simp]: "Poly (replicate n 0) = 0"
haftmann@52380
   312
  by (induct n) simp_all
haftmann@52380
   313
wenzelm@65346
   314
lemma Poly_eq_0: "Poly as = 0 \<longleftrightarrow> (\<exists>n. as = replicate n 0)"
haftmann@52380
   315
  by (induct as) (auto simp add: Cons_replicate_eq)
rene@63027
   316
wenzelm@65346
   317
lemma Poly_append_replicate_zero [simp]: "Poly (as @ replicate n 0) = Poly as"
rene@63027
   318
  by (induct as) simp_all
rene@63027
   319
wenzelm@65346
   320
lemma Poly_snoc_zero [simp]: "Poly (as @ [0]) = Poly as"
rene@63027
   321
  using Poly_append_replicate_zero [of as 1] by simp
rene@63027
   322
wenzelm@65346
   323
lemma Poly_cCons_eq_pCons_Poly [simp]: "Poly (a ## p) = pCons a (Poly p)"
rene@63027
   324
  by (simp add: cCons_def)
rene@63027
   325
wenzelm@65346
   326
lemma Poly_on_rev_starting_with_0 [simp]: "hd as = 0 \<Longrightarrow> Poly (rev (tl as)) = Poly (rev as)"
wenzelm@65346
   327
  by (cases as) simp_all
rene@63027
   328
eberlm@62065
   329
lemma degree_Poly: "degree (Poly xs) \<le> length xs"
wenzelm@65346
   330
  by (induct xs) simp_all
wenzelm@65346
   331
wenzelm@65346
   332
lemma coeff_Poly_eq [simp]: "coeff (Poly xs) = nth_default 0 xs"
rene@63027
   333
  by (induct xs) (simp_all add: fun_eq_iff coeff_pCons split: nat.splits)
rene@63027
   334
haftmann@52380
   335
definition coeffs :: "'a poly \<Rightarrow> 'a::zero list"
wenzelm@65346
   336
  where "coeffs p = (if p = 0 then [] else map (\<lambda>i. coeff p i) [0 ..< Suc (degree p)])"
wenzelm@65346
   337
wenzelm@65346
   338
lemma coeffs_eq_Nil [simp]: "coeffs p = [] \<longleftrightarrow> p = 0"
haftmann@52380
   339
  by (simp add: coeffs_def)
haftmann@52380
   340
wenzelm@65346
   341
lemma not_0_coeffs_not_Nil: "p \<noteq> 0 \<Longrightarrow> coeffs p \<noteq> []"
haftmann@52380
   342
  by simp
haftmann@52380
   343
wenzelm@65346
   344
lemma coeffs_0_eq_Nil [simp]: "coeffs 0 = []"
haftmann@52380
   345
  by simp
huffman@29454
   346
wenzelm@65346
   347
lemma coeffs_pCons_eq_cCons [simp]: "coeffs (pCons a p) = a ## coeffs p"
haftmann@52380
   348
proof -
wenzelm@65346
   349
  have *: "\<forall>m\<in>set ms. m > 0 \<Longrightarrow> map (case_nat x f) ms = map f (map (\<lambda>n. n - 1) ms)"
wenzelm@65346
   350
    for ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a"
wenzelm@65346
   351
    by (induct ms) (auto split: nat.split)
haftmann@52380
   352
  show ?thesis
wenzelm@65346
   353
    by (simp add: * coeffs_def upt_conv_Cons coeff_pCons map_decr_upt del: upt_Suc)
haftmann@52380
   354
qed
haftmann@52380
   355
eberlm@62065
   356
lemma length_coeffs: "p \<noteq> 0 \<Longrightarrow> length (coeffs p) = degree p + 1"
eberlm@62065
   357
  by (simp add: coeffs_def)
haftmann@64860
   358
wenzelm@65346
   359
lemma coeffs_nth: "p \<noteq> 0 \<Longrightarrow> n \<le> degree p \<Longrightarrow> coeffs p ! n = coeff p n"
wenzelm@65346
   360
  by (auto simp: coeffs_def simp del: upt_Suc)
wenzelm@65346
   361
wenzelm@65346
   362
lemma coeff_in_coeffs: "p \<noteq> 0 \<Longrightarrow> n \<le> degree p \<Longrightarrow> coeff p n \<in> set (coeffs p)"
wenzelm@65346
   363
  using coeffs_nth [of p n, symmetric] by (simp add: length_coeffs)
wenzelm@65346
   364
wenzelm@65346
   365
lemma not_0_cCons_eq [simp]: "p \<noteq> 0 \<Longrightarrow> a ## coeffs p = a # coeffs p"
haftmann@52380
   366
  by (simp add: cCons_def)
haftmann@52380
   367
wenzelm@65346
   368
lemma Poly_coeffs [simp, code abstype]: "Poly (coeffs p) = p"
haftmann@54856
   369
  by (induct p) auto
haftmann@52380
   370
wenzelm@65346
   371
lemma coeffs_Poly [simp]: "coeffs (Poly as) = strip_while (HOL.eq 0) as"
haftmann@52380
   372
proof (induct as)
wenzelm@65346
   373
  case Nil
wenzelm@65346
   374
  then show ?case by simp
haftmann@52380
   375
next
haftmann@52380
   376
  case (Cons a as)
wenzelm@65346
   377
  from replicate_length_same [of as 0] have "(\<forall>n. as \<noteq> replicate n 0) \<longleftrightarrow> (\<exists>a\<in>set as. a \<noteq> 0)"
wenzelm@65346
   378
    by (auto dest: sym [of _ as])
haftmann@52380
   379
  with Cons show ?case by auto
haftmann@52380
   380
qed
haftmann@52380
   381
haftmann@65390
   382
lemma no_trailing_coeffs [simp]:
haftmann@65390
   383
  "no_trailing (HOL.eq 0) (coeffs p)"
haftmann@65390
   384
  by (induct p)  auto
haftmann@65390
   385
haftmann@65390
   386
lemma strip_while_coeffs [simp]:
haftmann@65390
   387
  "strip_while (HOL.eq 0) (coeffs p) = coeffs p"
haftmann@65390
   388
  by simp
haftmann@52380
   389
wenzelm@65346
   390
lemma coeffs_eq_iff: "p = q \<longleftrightarrow> coeffs p = coeffs q"
wenzelm@65346
   391
  (is "?P \<longleftrightarrow> ?Q")
haftmann@52380
   392
proof
wenzelm@65346
   393
  assume ?P
wenzelm@65346
   394
  then show ?Q by simp
haftmann@52380
   395
next
haftmann@52380
   396
  assume ?Q
haftmann@52380
   397
  then have "Poly (coeffs p) = Poly (coeffs q)" by simp
haftmann@52380
   398
  then show ?P by simp
haftmann@52380
   399
qed
haftmann@52380
   400
wenzelm@65346
   401
lemma nth_default_coeffs_eq: "nth_default 0 (coeffs p) = coeff p"
haftmann@52380
   402
  by (simp add: fun_eq_iff coeff_Poly_eq [symmetric])
haftmann@52380
   403
wenzelm@65346
   404
lemma [code]: "coeff p = nth_default 0 (coeffs p)"
haftmann@52380
   405
  by (simp add: nth_default_coeffs_eq)
haftmann@52380
   406
haftmann@52380
   407
lemma coeffs_eqI:
haftmann@52380
   408
  assumes coeff: "\<And>n. coeff p n = nth_default 0 xs n"
haftmann@65390
   409
  assumes zero: "no_trailing (HOL.eq 0) xs"
haftmann@52380
   410
  shows "coeffs p = xs"
haftmann@52380
   411
proof -
haftmann@65390
   412
  from coeff have "p = Poly xs"
haftmann@65390
   413
    by (simp add: poly_eq_iff)
haftmann@65390
   414
  with zero show ?thesis by simp
haftmann@52380
   415
qed
haftmann@52380
   416
wenzelm@65346
   417
lemma degree_eq_length_coeffs [code]: "degree p = length (coeffs p) - 1"
haftmann@52380
   418
  by (simp add: coeffs_def)
haftmann@52380
   419
wenzelm@65346
   420
lemma length_coeffs_degree: "p \<noteq> 0 \<Longrightarrow> length (coeffs p) = Suc (degree p)"
wenzelm@65346
   421
  by (induct p) (auto simp: cCons_def)
wenzelm@65346
   422
wenzelm@65346
   423
lemma [code abstract]: "coeffs 0 = []"
haftmann@52380
   424
  by (fact coeffs_0_eq_Nil)
haftmann@52380
   425
wenzelm@65346
   426
lemma [code abstract]: "coeffs (pCons a p) = a ## coeffs p"
haftmann@52380
   427
  by (fact coeffs_pCons_eq_cCons)
haftmann@52380
   428
haftmann@65811
   429
lemma set_coeffs_subset_singleton_0_iff [simp]:
haftmann@65811
   430
  "set (coeffs p) \<subseteq> {0} \<longleftrightarrow> p = 0"
haftmann@65811
   431
  by (auto simp add: coeffs_def intro: classical)
haftmann@65811
   432
haftmann@65811
   433
lemma set_coeffs_not_only_0 [simp]:
haftmann@65811
   434
  "set (coeffs p) \<noteq> {0}"
haftmann@65811
   435
  by (auto simp add: set_eq_subset)
haftmann@65811
   436
haftmann@65811
   437
lemma forall_coeffs_conv:
haftmann@65811
   438
  "(\<forall>n. P (coeff p n)) \<longleftrightarrow> (\<forall>c \<in> set (coeffs p). P c)" if "P 0"
haftmann@65811
   439
  using that by (auto simp add: coeffs_def)
haftmann@65811
   440
    (metis atLeastLessThan_iff coeff_eq_0 not_less_iff_gr_or_eq zero_le)
haftmann@65811
   441
haftmann@52380
   442
instantiation poly :: ("{zero, equal}") equal
haftmann@52380
   443
begin
haftmann@52380
   444
wenzelm@65346
   445
definition [code]: "HOL.equal (p::'a poly) q \<longleftrightarrow> HOL.equal (coeffs p) (coeffs q)"
haftmann@52380
   446
wenzelm@60679
   447
instance
wenzelm@60679
   448
  by standard (simp add: equal equal_poly_def coeffs_eq_iff)
haftmann@52380
   449
haftmann@52380
   450
end
haftmann@52380
   451
wenzelm@60679
   452
lemma [code nbe]: "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
haftmann@52380
   453
  by (fact equal_refl)
huffman@29454
   454
haftmann@52380
   455
definition is_zero :: "'a::zero poly \<Rightarrow> bool"
wenzelm@65346
   456
  where [code]: "is_zero p \<longleftrightarrow> List.null (coeffs p)"
wenzelm@65346
   457
wenzelm@65346
   458
lemma is_zero_null [code_abbrev]: "is_zero p \<longleftrightarrow> p = 0"
haftmann@52380
   459
  by (simp add: is_zero_def null_def)
haftmann@52380
   460
wenzelm@65346
   461
rene@63027
   462
subsubsection \<open>Reconstructing the polynomial from the list\<close>
wenzelm@63145
   463
  \<comment> \<open>contributed by Sebastiaan J.C. Joosten and René Thiemann\<close>
rene@63027
   464
rene@63027
   465
definition poly_of_list :: "'a::comm_monoid_add list \<Rightarrow> 'a poly"
wenzelm@65346
   466
  where [simp]: "poly_of_list = Poly"
wenzelm@65346
   467
wenzelm@65346
   468
lemma poly_of_list_impl [code abstract]: "coeffs (poly_of_list as) = strip_while (HOL.eq 0) as"
rene@63027
   469
  by simp
rene@63027
   470
haftmann@52380
   471
wenzelm@60500
   472
subsection \<open>Fold combinator for polynomials\<close>
haftmann@52380
   473
haftmann@52380
   474
definition fold_coeffs :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b"
wenzelm@65346
   475
  where "fold_coeffs f p = foldr f (coeffs p)"
wenzelm@65346
   476
wenzelm@65346
   477
lemma fold_coeffs_0_eq [simp]: "fold_coeffs f 0 = id"
haftmann@52380
   478
  by (simp add: fold_coeffs_def)
haftmann@52380
   479
wenzelm@65346
   480
lemma fold_coeffs_pCons_eq [simp]: "f 0 = id \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
haftmann@52380
   481
  by (simp add: fold_coeffs_def cCons_def fun_eq_iff)
huffman@29454
   482
wenzelm@65346
   483
lemma fold_coeffs_pCons_0_0_eq [simp]: "fold_coeffs f (pCons 0 0) = id"
haftmann@52380
   484
  by (simp add: fold_coeffs_def)
haftmann@52380
   485
haftmann@52380
   486
lemma fold_coeffs_pCons_coeff_not_0_eq [simp]:
haftmann@52380
   487
  "a \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
haftmann@52380
   488
  by (simp add: fold_coeffs_def)
haftmann@52380
   489
haftmann@52380
   490
lemma fold_coeffs_pCons_not_0_0_eq [simp]:
haftmann@52380
   491
  "p \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
haftmann@52380
   492
  by (simp add: fold_coeffs_def)
haftmann@52380
   493
haftmann@64795
   494
wenzelm@60500
   495
subsection \<open>Canonical morphism on polynomials -- evaluation\<close>
haftmann@52380
   496
haftmann@52380
   497
definition poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a"
wenzelm@65346
   498
  where "poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)" \<comment> \<open>The Horner Schema\<close>
wenzelm@65346
   499
wenzelm@65346
   500
lemma poly_0 [simp]: "poly 0 x = 0"
haftmann@52380
   501
  by (simp add: poly_def)
wenzelm@65346
   502
wenzelm@65346
   503
lemma poly_pCons [simp]: "poly (pCons a p) x = a + x * poly p x"
haftmann@52380
   504
  by (cases "p = 0 \<and> a = 0") (auto simp add: poly_def)
huffman@29454
   505
wenzelm@65346
   506
lemma poly_altdef: "poly p x = (\<Sum>i\<le>degree p. coeff p i * x ^ i)"
wenzelm@65346
   507
  for x :: "'a::{comm_semiring_0,semiring_1}"
eberlm@62065
   508
proof (induction p rule: pCons_induct)
wenzelm@65346
   509
  case 0
wenzelm@65346
   510
  then show ?case
wenzelm@65346
   511
    by simp
wenzelm@65346
   512
next
eberlm@62065
   513
  case (pCons a p)
wenzelm@65346
   514
  show ?case
wenzelm@65346
   515
  proof (cases "p = 0")
wenzelm@65346
   516
    case True
wenzelm@65346
   517
    then show ?thesis by simp
wenzelm@65346
   518
  next
wenzelm@65346
   519
    case False
wenzelm@65346
   520
    let ?p' = "pCons a p"
wenzelm@65346
   521
    note poly_pCons[of a p x]
wenzelm@65346
   522
    also note pCons.IH
wenzelm@65346
   523
    also have "a + x * (\<Sum>i\<le>degree p. coeff p i * x ^ i) =
wenzelm@65346
   524
        coeff ?p' 0 * x^0 + (\<Sum>i\<le>degree p. coeff ?p' (Suc i) * x^Suc i)"
wenzelm@65346
   525
      by (simp add: field_simps sum_distrib_left coeff_pCons)
wenzelm@65346
   526
    also note sum_atMost_Suc_shift[symmetric]
wenzelm@65346
   527
    also note degree_pCons_eq[OF \<open>p \<noteq> 0\<close>, of a, symmetric]
wenzelm@65346
   528
    finally show ?thesis .
wenzelm@65346
   529
  qed
wenzelm@65346
   530
qed
eberlm@62065
   531
eberlm@62128
   532
lemma poly_0_coeff_0: "poly p 0 = coeff p 0"
eberlm@62128
   533
  by (cases p) (auto simp: poly_altdef)
eberlm@62128
   534
huffman@29454
   535
wenzelm@60500
   536
subsection \<open>Monomials\<close>
huffman@29451
   537
haftmann@52380
   538
lift_definition monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly"
haftmann@52380
   539
  is "\<lambda>a m n. if m = n then a else 0"
hoelzl@59983
   540
  by (simp add: MOST_iff_cofinite)
haftmann@52380
   541
wenzelm@65346
   542
lemma coeff_monom [simp]: "coeff (monom a m) n = (if m = n then a else 0)"
haftmann@52380
   543
  by transfer rule
huffman@29451
   544
wenzelm@65346
   545
lemma monom_0: "monom a 0 = pCons a 0"
haftmann@52380
   546
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
huffman@29451
   547
wenzelm@65346
   548
lemma monom_Suc: "monom a (Suc n) = pCons 0 (monom a n)"
haftmann@52380
   549
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
huffman@29451
   550
huffman@29451
   551
lemma monom_eq_0 [simp]: "monom 0 n = 0"
haftmann@52380
   552
  by (rule poly_eqI) simp
huffman@29451
   553
huffman@29451
   554
lemma monom_eq_0_iff [simp]: "monom a n = 0 \<longleftrightarrow> a = 0"
haftmann@52380
   555
  by (simp add: poly_eq_iff)
huffman@29451
   556
huffman@29451
   557
lemma monom_eq_iff [simp]: "monom a n = monom b n \<longleftrightarrow> a = b"
haftmann@52380
   558
  by (simp add: poly_eq_iff)
huffman@29451
   559
huffman@29451
   560
lemma degree_monom_le: "degree (monom a n) \<le> n"
huffman@29451
   561
  by (rule degree_le, simp)
huffman@29451
   562
huffman@29451
   563
lemma degree_monom_eq: "a \<noteq> 0 \<Longrightarrow> degree (monom a n) = n"
huffman@29451
   564
  apply (rule order_antisym [OF degree_monom_le])
wenzelm@65346
   565
  apply (rule le_degree)
wenzelm@65346
   566
  apply simp
huffman@29451
   567
  done
huffman@29451
   568
haftmann@52380
   569
lemma coeffs_monom [code abstract]:
haftmann@52380
   570
  "coeffs (monom a n) = (if a = 0 then [] else replicate n 0 @ [a])"
haftmann@52380
   571
  by (induct n) (simp_all add: monom_0 monom_Suc)
haftmann@52380
   572
wenzelm@65346
   573
lemma fold_coeffs_monom [simp]: "a \<noteq> 0 \<Longrightarrow> fold_coeffs f (monom a n) = f 0 ^^ n \<circ> f a"
haftmann@52380
   574
  by (simp add: fold_coeffs_def coeffs_monom fun_eq_iff)
haftmann@52380
   575
wenzelm@65346
   576
lemma poly_monom: "poly (monom a n) x = a * x ^ n"
wenzelm@65346
   577
  for a x :: "'a::comm_semiring_1"
wenzelm@65346
   578
  by (cases "a = 0", simp_all) (induct n, simp_all add: mult.left_commute poly_def)
eberlm@63317
   579
eberlm@63317
   580
lemma monom_eq_iff': "monom c n = monom d m \<longleftrightarrow>  c = d \<and> (c = 0 \<or> n = m)"
eberlm@63317
   581
  by (auto simp: poly_eq_iff)
wenzelm@65346
   582
eberlm@63317
   583
lemma monom_eq_const_iff: "monom c n = [:d:] \<longleftrightarrow> c = d \<and> (c = 0 \<or> n = 0)"
eberlm@63317
   584
  using monom_eq_iff'[of c n d 0] by (simp add: monom_0)
haftmann@64795
   585
haftmann@64795
   586
haftmann@64795
   587
subsection \<open>Leading coefficient\<close>
haftmann@64795
   588
haftmann@64795
   589
abbreviation lead_coeff:: "'a::zero poly \<Rightarrow> 'a"
haftmann@64795
   590
  where "lead_coeff p \<equiv> coeff p (degree p)"
haftmann@64795
   591
haftmann@64795
   592
lemma lead_coeff_pCons[simp]:
haftmann@64795
   593
  "p \<noteq> 0 \<Longrightarrow> lead_coeff (pCons a p) = lead_coeff p"
haftmann@64795
   594
  "p = 0 \<Longrightarrow> lead_coeff (pCons a p) = a"
haftmann@64795
   595
  by auto
haftmann@64795
   596
haftmann@64795
   597
lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
haftmann@64795
   598
  by (cases "c = 0") (simp_all add: degree_monom_eq)
haftmann@64795
   599
haftmann@66799
   600
lemma last_coeffs_eq_coeff_degree:
haftmann@66799
   601
  "last (coeffs p) = lead_coeff p" if "p \<noteq> 0"
haftmann@66799
   602
  using that by (simp add: coeffs_def)
haftmann@66799
   603
  
haftmann@64795
   604
wenzelm@60500
   605
subsection \<open>Addition and subtraction\<close>
huffman@29451
   606
huffman@29451
   607
instantiation poly :: (comm_monoid_add) comm_monoid_add
huffman@29451
   608
begin
huffman@29451
   609
haftmann@52380
   610
lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
haftmann@52380
   611
  is "\<lambda>p q n. coeff p n + coeff q n"
hoelzl@60040
   612
proof -
wenzelm@60679
   613
  fix q p :: "'a poly"
wenzelm@60679
   614
  show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0"
hoelzl@60040
   615
    using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
haftmann@52380
   616
qed
huffman@29451
   617
wenzelm@60679
   618
lemma coeff_add [simp]: "coeff (p + q) n = coeff p n + coeff q n"
haftmann@52380
   619
  by (simp add: plus_poly.rep_eq)
huffman@29451
   620
wenzelm@60679
   621
instance
wenzelm@60679
   622
proof
huffman@29451
   623
  fix p q r :: "'a poly"
huffman@29451
   624
  show "(p + q) + r = p + (q + r)"
haftmann@57512
   625
    by (simp add: poly_eq_iff add.assoc)
huffman@29451
   626
  show "p + q = q + p"
haftmann@57512
   627
    by (simp add: poly_eq_iff add.commute)
huffman@29451
   628
  show "0 + p = p"
haftmann@52380
   629
    by (simp add: poly_eq_iff)
huffman@29451
   630
qed
huffman@29451
   631
huffman@29451
   632
end
huffman@29451
   633
haftmann@59815
   634
instantiation poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add
haftmann@59815
   635
begin
haftmann@59815
   636
haftmann@59815
   637
lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
haftmann@59815
   638
  is "\<lambda>p q n. coeff p n - coeff q n"
hoelzl@60040
   639
proof -
wenzelm@60679
   640
  fix q p :: "'a poly"
wenzelm@60679
   641
  show "\<forall>\<^sub>\<infinity>n. coeff p n - coeff q n = 0"
hoelzl@60040
   642
    using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
haftmann@59815
   643
qed
haftmann@59815
   644
wenzelm@60679
   645
lemma coeff_diff [simp]: "coeff (p - q) n = coeff p n - coeff q n"
haftmann@59815
   646
  by (simp add: minus_poly.rep_eq)
haftmann@59815
   647
wenzelm@60679
   648
instance
wenzelm@60679
   649
proof
huffman@29540
   650
  fix p q r :: "'a poly"
haftmann@59815
   651
  show "p + q - p = q"
haftmann@52380
   652
    by (simp add: poly_eq_iff)
haftmann@59815
   653
  show "p - q - r = p - (q + r)"
haftmann@59815
   654
    by (simp add: poly_eq_iff diff_diff_eq)
huffman@29540
   655
qed
huffman@29540
   656
haftmann@59815
   657
end
haftmann@59815
   658
huffman@29451
   659
instantiation poly :: (ab_group_add) ab_group_add
huffman@29451
   660
begin
huffman@29451
   661
haftmann@52380
   662
lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly"
haftmann@52380
   663
  is "\<lambda>p n. - coeff p n"
hoelzl@60040
   664
proof -
wenzelm@60679
   665
  fix p :: "'a poly"
wenzelm@60679
   666
  show "\<forall>\<^sub>\<infinity>n. - coeff p n = 0"
hoelzl@60040
   667
    using MOST_coeff_eq_0 by simp
haftmann@52380
   668
qed
huffman@29451
   669
huffman@29451
   670
lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
haftmann@52380
   671
  by (simp add: uminus_poly.rep_eq)
huffman@29451
   672
wenzelm@60679
   673
instance
wenzelm@60679
   674
proof
huffman@29451
   675
  fix p q :: "'a poly"
huffman@29451
   676
  show "- p + p = 0"
haftmann@52380
   677
    by (simp add: poly_eq_iff)
huffman@29451
   678
  show "p - q = p + - q"
haftmann@54230
   679
    by (simp add: poly_eq_iff)
huffman@29451
   680
qed
huffman@29451
   681
huffman@29451
   682
end
huffman@29451
   683
wenzelm@65346
   684
lemma add_pCons [simp]: "pCons a p + pCons b q = pCons (a + b) (p + q)"
wenzelm@65346
   685
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
wenzelm@65346
   686
wenzelm@65346
   687
lemma minus_pCons [simp]: "- pCons a p = pCons (- a) (- p)"
wenzelm@65346
   688
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
wenzelm@65346
   689
wenzelm@65346
   690
lemma diff_pCons [simp]: "pCons a p - pCons b q = pCons (a - b) (p - q)"
wenzelm@65346
   691
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
huffman@29451
   692
huffman@29539
   693
lemma degree_add_le_max: "degree (p + q) \<le> max (degree p) (degree q)"
wenzelm@65346
   694
  by (rule degree_le) (auto simp add: coeff_eq_0)
wenzelm@65346
   695
wenzelm@65346
   696
lemma degree_add_le: "degree p \<le> n \<Longrightarrow> degree q \<le> n \<Longrightarrow> degree (p + q) \<le> n"
huffman@29539
   697
  by (auto intro: order_trans degree_add_le_max)
huffman@29539
   698
wenzelm@65346
   699
lemma degree_add_less: "degree p < n \<Longrightarrow> degree q < n \<Longrightarrow> degree (p + q) < n"
huffman@29539
   700
  by (auto intro: le_less_trans degree_add_le_max)
huffman@29453
   701
wenzelm@65346
   702
lemma degree_add_eq_right: "degree p < degree q \<Longrightarrow> degree (p + q) = degree q"
wenzelm@65346
   703
  apply (cases "q = 0")
wenzelm@65346
   704
   apply simp
huffman@29451
   705
  apply (rule order_antisym)
wenzelm@65346
   706
   apply (simp add: degree_add_le)
huffman@29451
   707
  apply (rule le_degree)
huffman@29451
   708
  apply (simp add: coeff_eq_0)
huffman@29451
   709
  done
huffman@29451
   710
wenzelm@65346
   711
lemma degree_add_eq_left: "degree q < degree p \<Longrightarrow> degree (p + q) = degree p"
wenzelm@65346
   712
  using degree_add_eq_right [of q p] by (simp add: add.commute)
wenzelm@65346
   713
wenzelm@65346
   714
lemma degree_minus [simp]: "degree (- p) = degree p"
wenzelm@65346
   715
  by (simp add: degree_def)
wenzelm@65346
   716
wenzelm@65346
   717
lemma lead_coeff_add_le: "degree p < degree q \<Longrightarrow> lead_coeff (p + q) = lead_coeff q"
haftmann@64795
   718
  by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right)
haftmann@64795
   719
wenzelm@65346
   720
lemma lead_coeff_minus: "lead_coeff (- p) = - lead_coeff p"
haftmann@64795
   721
  by (metis coeff_minus degree_minus)
haftmann@64795
   722
wenzelm@65346
   723
lemma degree_diff_le_max: "degree (p - q) \<le> max (degree p) (degree q)"
wenzelm@65346
   724
  for p q :: "'a::ab_group_add poly"
wenzelm@65346
   725
  using degree_add_le [where p=p and q="-q"] by simp
wenzelm@65346
   726
wenzelm@65346
   727
lemma degree_diff_le: "degree p \<le> n \<Longrightarrow> degree q \<le> n \<Longrightarrow> degree (p - q) \<le> n"
wenzelm@65346
   728
  for p q :: "'a::ab_group_add poly"
wenzelm@65346
   729
  using degree_add_le [of p n "- q"] by simp
wenzelm@65346
   730
wenzelm@65346
   731
lemma degree_diff_less: "degree p < n \<Longrightarrow> degree q < n \<Longrightarrow> degree (p - q) < n"
wenzelm@65346
   732
  for p q :: "'a::ab_group_add poly"
wenzelm@65346
   733
  using degree_add_less [of p n "- q"] by simp
huffman@29453
   734
huffman@29451
   735
lemma add_monom: "monom a n + monom b n = monom (a + b) n"
haftmann@52380
   736
  by (rule poly_eqI) simp
huffman@29451
   737
huffman@29451
   738
lemma diff_monom: "monom a n - monom b n = monom (a - b) n"
haftmann@52380
   739
  by (rule poly_eqI) simp
huffman@29451
   740
wenzelm@65346
   741
lemma minus_monom: "- monom a n = monom (- a) n"
haftmann@52380
   742
  by (rule poly_eqI) simp
huffman@29451
   743
nipkow@64267
   744
lemma coeff_sum: "coeff (\<Sum>x\<in>A. p x) i = (\<Sum>x\<in>A. coeff (p x) i)"
wenzelm@65346
   745
  by (induct A rule: infinite_finite_induct) simp_all
huffman@29451
   746
nipkow@64267
   747
lemma monom_sum: "monom (\<Sum>x\<in>A. a x) n = (\<Sum>x\<in>A. monom (a x) n)"
nipkow@64267
   748
  by (rule poly_eqI) (simp add: coeff_sum)
haftmann@52380
   749
haftmann@52380
   750
fun plus_coeffs :: "'a::comm_monoid_add list \<Rightarrow> 'a list \<Rightarrow> 'a list"
wenzelm@65346
   751
  where
wenzelm@65346
   752
    "plus_coeffs xs [] = xs"
wenzelm@65346
   753
  | "plus_coeffs [] ys = ys"
wenzelm@65346
   754
  | "plus_coeffs (x # xs) (y # ys) = (x + y) ## plus_coeffs xs ys"
haftmann@52380
   755
haftmann@52380
   756
lemma coeffs_plus_eq_plus_coeffs [code abstract]:
haftmann@52380
   757
  "coeffs (p + q) = plus_coeffs (coeffs p) (coeffs q)"
haftmann@52380
   758
proof -
wenzelm@65346
   759
  have *: "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n"
wenzelm@65346
   760
    for xs ys :: "'a list" and n
wenzelm@65346
   761
  proof (induct xs ys arbitrary: n rule: plus_coeffs.induct)
haftmann@65390
   762
    case (3 x xs y ys n)
haftmann@65390
   763
    then show ?case
haftmann@65390
   764
      by (cases n) (auto simp add: cCons_def)
wenzelm@65346
   765
  qed simp_all
haftmann@65390
   766
  have **: "no_trailing (HOL.eq 0) (plus_coeffs xs ys)"
haftmann@65390
   767
    if "no_trailing (HOL.eq 0) xs" and "no_trailing (HOL.eq 0) ys"
haftmann@65390
   768
    for xs ys :: "'a list"
haftmann@65390
   769
    using that by (induct xs ys rule: plus_coeffs.induct) (simp_all add: cCons_def)
haftmann@52380
   770
  show ?thesis
haftmann@65390
   771
    by (rule coeffs_eqI) (auto simp add: * nth_default_coeffs_eq intro: **)
haftmann@52380
   772
qed
haftmann@52380
   773
haftmann@65390
   774
lemma coeffs_uminus [code abstract]:
haftmann@65390
   775
  "coeffs (- p) = map uminus (coeffs p)"
haftmann@65390
   776
proof -
haftmann@65390
   777
  have eq_0: "HOL.eq 0 \<circ> uminus = HOL.eq (0::'a)"
haftmann@65390
   778
    by (simp add: fun_eq_iff)
haftmann@65390
   779
  show ?thesis
haftmann@65390
   780
    by (rule coeffs_eqI) (simp_all add: nth_default_map_eq nth_default_coeffs_eq no_trailing_map eq_0)
haftmann@65390
   781
qed
haftmann@52380
   782
wenzelm@65346
   783
lemma [code]: "p - q = p + - q"
wenzelm@65346
   784
  for p q :: "'a::ab_group_add poly"
haftmann@59557
   785
  by (fact diff_conv_add_uminus)
haftmann@52380
   786
haftmann@52380
   787
lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
wenzelm@65346
   788
  apply (induct p arbitrary: q)
wenzelm@65346
   789
   apply simp
haftmann@52380
   790
  apply (case_tac q, simp, simp add: algebra_simps)
haftmann@52380
   791
  done
haftmann@52380
   792
wenzelm@65346
   793
lemma poly_minus [simp]: "poly (- p) x = - poly p x"
wenzelm@65346
   794
  for x :: "'a::comm_ring"
haftmann@52380
   795
  by (induct p) simp_all
haftmann@52380
   796
wenzelm@65346
   797
lemma poly_diff [simp]: "poly (p - q) x = poly p x - poly q x"
wenzelm@65346
   798
  for x :: "'a::comm_ring"
haftmann@54230
   799
  using poly_add [of p "- q" x] by simp
haftmann@52380
   800
nipkow@64267
   801
lemma poly_sum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
haftmann@52380
   802
  by (induct A rule: infinite_finite_induct) simp_all
huffman@29451
   803
wenzelm@65346
   804
lemma degree_sum_le: "finite S \<Longrightarrow> (\<And>p. p \<in> S \<Longrightarrow> degree (f p) \<le> n) \<Longrightarrow> degree (sum f S) \<le> n"
eberlm@62128
   805
proof (induct S rule: finite_induct)
wenzelm@65346
   806
  case empty
wenzelm@65346
   807
  then show ?case by simp
wenzelm@65346
   808
next
eberlm@62128
   809
  case (insert p S)
wenzelm@65346
   810
  then have "degree (sum f S) \<le> n" "degree (f p) \<le> n"
wenzelm@65346
   811
    by auto
wenzelm@65346
   812
  then show ?case
wenzelm@65346
   813
    unfolding sum.insert[OF insert(1-2)] by (metis degree_add_le)
wenzelm@65346
   814
qed
wenzelm@65346
   815
wenzelm@65346
   816
lemma poly_as_sum_of_monoms':
wenzelm@65346
   817
  assumes "degree p \<le> n"
eberlm@62128
   818
  shows "(\<Sum>i\<le>n. monom (coeff p i) i) = p"
eberlm@62128
   819
proof -
eberlm@62128
   820
  have eq: "\<And>i. {..n} \<inter> {i} = (if i \<le> n then {i} else {})"
eberlm@62128
   821
    by auto
wenzelm@65346
   822
  from assms show ?thesis
wenzelm@65346
   823
    by (simp add: poly_eq_iff coeff_sum coeff_eq_0 sum.If_cases eq
wenzelm@65346
   824
        if_distrib[where f="\<lambda>x. x * a" for a])
eberlm@62128
   825
qed
eberlm@62128
   826
eberlm@62128
   827
lemma poly_as_sum_of_monoms: "(\<Sum>i\<le>degree p. monom (coeff p i) i) = p"
eberlm@62128
   828
  by (intro poly_as_sum_of_monoms' order_refl)
eberlm@62128
   829
eberlm@62065
   830
lemma Poly_snoc: "Poly (xs @ [x]) = Poly xs + monom x (length xs)"
wenzelm@65346
   831
  by (induct xs) (simp_all add: monom_0 monom_Suc)
eberlm@62065
   832
huffman@29451
   833
wenzelm@60500
   834
subsection \<open>Multiplication by a constant, polynomial multiplication and the unit polynomial\<close>
huffman@29451
   835
haftmann@52380
   836
lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
haftmann@52380
   837
  is "\<lambda>a p n. a * coeff p n"
hoelzl@60040
   838
proof -
wenzelm@65346
   839
  fix a :: 'a and p :: "'a poly"
wenzelm@65346
   840
  show "\<forall>\<^sub>\<infinity> i. a * coeff p i = 0"
hoelzl@60040
   841
    using MOST_coeff_eq_0[of p] by eventually_elim simp
haftmann@52380
   842
qed
huffman@29451
   843
wenzelm@65346
   844
lemma coeff_smult [simp]: "coeff (smult a p) n = a * coeff p n"
haftmann@52380
   845
  by (simp add: smult.rep_eq)
huffman@29451
   846
huffman@29451
   847
lemma degree_smult_le: "degree (smult a p) \<le> degree p"
wenzelm@65346
   848
  by (rule degree_le) (simp add: coeff_eq_0)
huffman@29451
   849
huffman@29472
   850
lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p"
wenzelm@65346
   851
  by (rule poly_eqI) (simp add: mult.assoc)
huffman@29451
   852
huffman@29451
   853
lemma smult_0_right [simp]: "smult a 0 = 0"
wenzelm@65346
   854
  by (rule poly_eqI) simp
huffman@29451
   855
huffman@29451
   856
lemma smult_0_left [simp]: "smult 0 p = 0"
wenzelm@65346
   857
  by (rule poly_eqI) simp
huffman@29451
   858
huffman@29451
   859
lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p"
wenzelm@65346
   860
  by (rule poly_eqI) simp
wenzelm@65346
   861
wenzelm@65346
   862
lemma smult_add_right: "smult a (p + q) = smult a p + smult a q"
wenzelm@65346
   863
  by (rule poly_eqI) (simp add: algebra_simps)
wenzelm@65346
   864
wenzelm@65346
   865
lemma smult_add_left: "smult (a + b) p = smult a p + smult b p"
wenzelm@65346
   866
  by (rule poly_eqI) (simp add: algebra_simps)
wenzelm@65346
   867
wenzelm@65346
   868
lemma smult_minus_right [simp]: "smult a (- p) = - smult a p"
wenzelm@65346
   869
  for a :: "'a::comm_ring"
wenzelm@65346
   870
  by (rule poly_eqI) simp
wenzelm@65346
   871
wenzelm@65346
   872
lemma smult_minus_left [simp]: "smult (- a) p = - smult a p"
wenzelm@65346
   873
  for a :: "'a::comm_ring"
wenzelm@65346
   874
  by (rule poly_eqI) simp
wenzelm@65346
   875
wenzelm@65346
   876
lemma smult_diff_right: "smult a (p - q) = smult a p - smult a q"
wenzelm@65346
   877
  for a :: "'a::comm_ring"
wenzelm@65346
   878
  by (rule poly_eqI) (simp add: algebra_simps)
wenzelm@65346
   879
wenzelm@65346
   880
lemma smult_diff_left: "smult (a - b) p = smult a p - smult b p"
wenzelm@65346
   881
  for a b :: "'a::comm_ring"
wenzelm@65346
   882
  by (rule poly_eqI) (simp add: algebra_simps)
huffman@29451
   883
huffman@29472
   884
lemmas smult_distribs =
huffman@29472
   885
  smult_add_left smult_add_right
huffman@29472
   886
  smult_diff_left smult_diff_right
huffman@29472
   887
wenzelm@65346
   888
lemma smult_pCons [simp]: "smult a (pCons b p) = pCons (a * b) (smult a p)"
wenzelm@65346
   889
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
huffman@29451
   890
huffman@29451
   891
lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
wenzelm@65346
   892
  by (induct n) (simp_all add: monom_0 monom_Suc)
huffman@29451
   893
eberlm@63317
   894
lemma smult_Poly: "smult c (Poly xs) = Poly (map (op * c) xs)"
wenzelm@65346
   895
  by (auto simp: poly_eq_iff nth_default_def)
wenzelm@65346
   896
wenzelm@65346
   897
lemma degree_smult_eq [simp]: "degree (smult a p) = (if a = 0 then 0 else degree p)"
wenzelm@65346
   898
  for a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}"
wenzelm@65346
   899
  by (cases "a = 0") (simp_all add: degree_def)
wenzelm@65346
   900
wenzelm@65346
   901
lemma smult_eq_0_iff [simp]: "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0"
wenzelm@65346
   902
  for a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}"
haftmann@52380
   903
  by (simp add: poly_eq_iff)
wenzelm@65346
   904
haftmann@52380
   905
lemma coeffs_smult [code abstract]:
wenzelm@65346
   906
  "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))"
wenzelm@65346
   907
  for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
haftmann@65390
   908
proof -
haftmann@65390
   909
  have eq_0: "HOL.eq 0 \<circ> times a = HOL.eq (0::'a)" if "a \<noteq> 0"
haftmann@65390
   910
    using that by (simp add: fun_eq_iff)
haftmann@65390
   911
  show ?thesis
haftmann@65390
   912
    by (rule coeffs_eqI) (auto simp add: no_trailing_map nth_default_map_eq nth_default_coeffs_eq eq_0)
haftmann@65390
   913
qed  
haftmann@64795
   914
haftmann@64795
   915
lemma smult_eq_iff:
wenzelm@65346
   916
  fixes b :: "'a :: field"
wenzelm@65346
   917
  assumes "b \<noteq> 0"
wenzelm@65346
   918
  shows "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
wenzelm@65346
   919
    (is "?lhs \<longleftrightarrow> ?rhs")
haftmann@64795
   920
proof
wenzelm@65346
   921
  assume ?lhs
wenzelm@65346
   922
  also from assms have "smult (inverse b) \<dots> = q"
wenzelm@65346
   923
    by simp
wenzelm@65346
   924
  finally show ?rhs
wenzelm@65346
   925
    by (simp add: field_simps)
wenzelm@65346
   926
next
wenzelm@65346
   927
  assume ?rhs
wenzelm@65346
   928
  with assms show ?lhs by auto
wenzelm@65346
   929
qed
haftmann@64795
   930
huffman@29451
   931
instantiation poly :: (comm_semiring_0) comm_semiring_0
huffman@29451
   932
begin
huffman@29451
   933
wenzelm@65346
   934
definition "p * q = fold_coeffs (\<lambda>a p. smult a q + pCons 0 p) p 0"
huffman@29474
   935
huffman@29474
   936
lemma mult_poly_0_left: "(0::'a poly) * q = 0"
haftmann@52380
   937
  by (simp add: times_poly_def)
huffman@29474
   938
wenzelm@65346
   939
lemma mult_pCons_left [simp]: "pCons a p * q = smult a q + pCons 0 (p * q)"
haftmann@52380
   940
  by (cases "p = 0 \<and> a = 0") (auto simp add: times_poly_def)
huffman@29474
   941
huffman@29474
   942
lemma mult_poly_0_right: "p * (0::'a poly) = 0"
wenzelm@65346
   943
  by (induct p) (simp_all add: mult_poly_0_left)
wenzelm@65346
   944
wenzelm@65346
   945
lemma mult_pCons_right [simp]: "p * pCons a q = smult a p + pCons 0 (p * q)"
wenzelm@65346
   946
  by (induct p) (simp_all add: mult_poly_0_left algebra_simps)
huffman@29474
   947
huffman@29474
   948
lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right
huffman@29474
   949
wenzelm@65346
   950
lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)"
wenzelm@65346
   951
  by (induct p) (simp_all add: mult_poly_0 smult_add_right)
wenzelm@65346
   952
wenzelm@65346
   953
lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)"
wenzelm@65346
   954
  by (induct q) (simp_all add: mult_poly_0 smult_add_right)
wenzelm@65346
   955
wenzelm@65346
   956
lemma mult_poly_add_left: "(p + q) * r = p * r + q * r"
wenzelm@65346
   957
  for p q r :: "'a poly"
wenzelm@65346
   958
  by (induct r) (simp_all add: mult_poly_0 smult_distribs algebra_simps)
huffman@29451
   959
wenzelm@60679
   960
instance
wenzelm@60679
   961
proof
huffman@29451
   962
  fix p q r :: "'a poly"
huffman@29451
   963
  show 0: "0 * p = 0"
huffman@29474
   964
    by (rule mult_poly_0_left)
huffman@29451
   965
  show "p * 0 = 0"
huffman@29474
   966
    by (rule mult_poly_0_right)
huffman@29451
   967
  show "(p + q) * r = p * r + q * r"
huffman@29474
   968
    by (rule mult_poly_add_left)
huffman@29451
   969
  show "(p * q) * r = p * (q * r)"
wenzelm@65346
   970
    by (induct p) (simp_all add: mult_poly_0 mult_poly_add_left)
huffman@29451
   971
  show "p * q = q * p"
wenzelm@65346
   972
    by (induct p) (simp_all add: mult_poly_0)
huffman@29451
   973
qed
huffman@29451
   974
huffman@29451
   975
end
huffman@29451
   976
eberlm@63498
   977
lemma coeff_mult_degree_sum:
wenzelm@65346
   978
  "coeff (p * q) (degree p + degree q) = coeff p (degree p) * coeff q (degree q)"
wenzelm@65346
   979
  by (induct p) (simp_all add: coeff_eq_0)
eberlm@63498
   980
eberlm@63498
   981
instance poly :: ("{comm_semiring_0,semiring_no_zero_divisors}") semiring_no_zero_divisors
eberlm@63498
   982
proof
eberlm@63498
   983
  fix p q :: "'a poly"
eberlm@63498
   984
  assume "p \<noteq> 0" and "q \<noteq> 0"
wenzelm@65346
   985
  have "coeff (p * q) (degree p + degree q) = coeff p (degree p) * coeff q (degree q)"
eberlm@63498
   986
    by (rule coeff_mult_degree_sum)
wenzelm@65346
   987
  also from \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> have "coeff p (degree p) * coeff q (degree q) \<noteq> 0"
wenzelm@65346
   988
    by simp
eberlm@63498
   989
  finally have "\<exists>n. coeff (p * q) n \<noteq> 0" ..
wenzelm@65346
   990
  then show "p * q \<noteq> 0"
wenzelm@65346
   991
    by (simp add: poly_eq_iff)
eberlm@63498
   992
qed
eberlm@63498
   993
huffman@29540
   994
instance poly :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
huffman@29540
   995
wenzelm@65346
   996
lemma coeff_mult: "coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (n-i))"
huffman@29474
   997
proof (induct p arbitrary: n)
wenzelm@65346
   998
  case 0
wenzelm@65346
   999
  show ?case by simp
huffman@29474
  1000
next
wenzelm@65346
  1001
  case (pCons a p n)
wenzelm@65346
  1002
  then show ?case
wenzelm@65346
  1003
    by (cases n) (simp_all add: sum_atMost_Suc_shift del: sum_atMost_Suc)
huffman@29474
  1004
qed
huffman@29451
  1005
huffman@29474
  1006
lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q"
wenzelm@65346
  1007
  apply (rule degree_le)
wenzelm@65346
  1008
  apply (induct p)
wenzelm@65346
  1009
   apply simp
wenzelm@65346
  1010
  apply (simp add: coeff_eq_0 coeff_pCons split: nat.split)
wenzelm@65346
  1011
  done
huffman@29451
  1012
huffman@29451
  1013
lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
wenzelm@60679
  1014
  by (induct m) (simp add: monom_0 smult_monom, simp add: monom_Suc)
huffman@29451
  1015
huffman@29451
  1016
instantiation poly :: (comm_semiring_1) comm_semiring_1
huffman@29451
  1017
begin
huffman@29451
  1018
haftmann@65486
  1019
lift_definition one_poly :: "'a poly"
haftmann@65486
  1020
  is "\<lambda>n. of_bool (n = 0)"
haftmann@65486
  1021
  by (rule MOST_SucD) simp
haftmann@65486
  1022
haftmann@65486
  1023
lemma coeff_1 [simp]:
haftmann@65486
  1024
  "coeff 1 n = of_bool (n = 0)"
haftmann@65486
  1025
  by (simp add: one_poly.rep_eq)
haftmann@65486
  1026
haftmann@65486
  1027
lemma one_pCons:
haftmann@65486
  1028
  "1 = [:1:]"
haftmann@65486
  1029
  by (simp add: poly_eq_iff coeff_pCons split: nat.splits)
haftmann@65486
  1030
haftmann@65486
  1031
lemma pCons_one:
haftmann@65486
  1032
  "[:1:] = 1"
haftmann@65486
  1033
  by (simp add: one_pCons)
huffman@29451
  1034
wenzelm@60679
  1035
instance
haftmann@65486
  1036
  by standard (simp_all add: one_pCons)
huffman@29451
  1037
huffman@29451
  1038
end
huffman@29451
  1039
haftmann@65486
  1040
lemma poly_1 [simp]:
haftmann@65486
  1041
  "poly 1 x = 1"
haftmann@65486
  1042
  by (simp add: one_pCons)
haftmann@65486
  1043
haftmann@65486
  1044
lemma one_poly_eq_simps [simp]:
haftmann@65486
  1045
  "1 = [:1:] \<longleftrightarrow> True"
haftmann@65486
  1046
  "[:1:] = 1 \<longleftrightarrow> True"
haftmann@65486
  1047
  by (simp_all add: one_pCons)
haftmann@65486
  1048
haftmann@65486
  1049
lemma degree_1 [simp]:
haftmann@65486
  1050
  "degree 1 = 0"
haftmann@65486
  1051
  by (simp add: one_pCons)
haftmann@65486
  1052
haftmann@65486
  1053
lemma coeffs_1_eq [simp, code abstract]:
haftmann@65486
  1054
  "coeffs 1 = [1]"
haftmann@65486
  1055
  by (simp add: one_pCons)
haftmann@65486
  1056
haftmann@65486
  1057
lemma smult_one [simp]:
haftmann@65486
  1058
  "smult c 1 = [:c:]"
haftmann@65486
  1059
  by (simp add: one_pCons)
haftmann@65486
  1060
haftmann@65486
  1061
lemma monom_eq_1 [simp]:
haftmann@65486
  1062
  "monom 1 0 = 1"
haftmann@65486
  1063
  by (simp add: monom_0 one_pCons)
haftmann@65486
  1064
haftmann@65486
  1065
lemma monom_eq_1_iff:
haftmann@65486
  1066
  "monom c n = 1 \<longleftrightarrow> c = 1 \<and> n = 0"
haftmann@65486
  1067
  using monom_eq_const_iff [of c n 1] by auto
haftmann@65486
  1068
haftmann@65486
  1069
lemma monom_altdef:
haftmann@65486
  1070
  "monom c n = smult c ([:0, 1:] ^ n)"
haftmann@65486
  1071
  by (induct n) (simp_all add: monom_0 monom_Suc)  
haftmann@65486
  1072
eberlm@63498
  1073
instance poly :: ("{comm_semiring_1,semiring_1_no_zero_divisors}") semiring_1_no_zero_divisors ..
haftmann@52380
  1074
instance poly :: (comm_ring) comm_ring ..
haftmann@52380
  1075
instance poly :: (comm_ring_1) comm_ring_1 ..
eberlm@63498
  1076
instance poly :: (comm_ring_1) comm_semiring_1_cancel ..
eberlm@63498
  1077
wenzelm@65346
  1078
lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
haftmann@52380
  1079
  by (induct n) (auto intro: order_trans degree_mult_le)
haftmann@52380
  1080
wenzelm@65346
  1081
lemma coeff_0_power: "coeff (p ^ n) 0 = coeff p 0 ^ n"
wenzelm@65346
  1082
  by (induct n) (simp_all add: coeff_mult)
wenzelm@65346
  1083
wenzelm@65346
  1084
lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x"
wenzelm@65346
  1085
  by (induct p) (simp_all add: algebra_simps)
wenzelm@65346
  1086
wenzelm@65346
  1087
lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x"
wenzelm@65346
  1088
  by (induct p) (simp_all add: algebra_simps)
wenzelm@65346
  1089
wenzelm@65346
  1090
lemma poly_power [simp]: "poly (p ^ n) x = poly p x ^ n"
wenzelm@65346
  1091
  for p :: "'a::comm_semiring_1 poly"
haftmann@52380
  1092
  by (induct n) simp_all
haftmann@52380
  1093
nipkow@64272
  1094
lemma poly_prod: "poly (\<Prod>k\<in>A. p k) x = (\<Prod>k\<in>A. poly (p k) x)"
eberlm@62128
  1095
  by (induct A rule: infinite_finite_induct) simp_all
eberlm@62128
  1096
wenzelm@67091
  1097
lemma degree_prod_sum_le: "finite S \<Longrightarrow> degree (prod f S) \<le> sum (degree \<circ> f) S"
eberlm@62128
  1098
proof (induct S rule: finite_induct)
wenzelm@65346
  1099
  case empty
wenzelm@65346
  1100
  then show ?case by simp
wenzelm@65346
  1101
next
eberlm@62128
  1102
  case (insert a S)
wenzelm@65346
  1103
  show ?case
wenzelm@65346
  1104
    unfolding prod.insert[OF insert(1-2)] sum.insert[OF insert(1-2)]
wenzelm@65346
  1105
    by (rule le_trans[OF degree_mult_le]) (use insert in auto)
wenzelm@65346
  1106
qed
wenzelm@65346
  1107
wenzelm@65346
  1108
lemma coeff_0_prod_list: "coeff (prod_list xs) 0 = prod_list (map (\<lambda>p. coeff p 0) xs)"
wenzelm@65346
  1109
  by (induct xs) (simp_all add: coeff_mult)
wenzelm@65346
  1110
wenzelm@65346
  1111
lemma coeff_monom_mult: "coeff (monom c n * p) k = (if k < n then 0 else c * coeff p (k - n))"
haftmann@64795
  1112
proof -
haftmann@64795
  1113
  have "coeff (monom c n * p) k = (\<Sum>i\<le>k. (if n = i then c else 0) * coeff p (k - i))"
haftmann@64795
  1114
    by (simp add: coeff_mult)
haftmann@64795
  1115
  also have "\<dots> = (\<Sum>i\<le>k. (if n = i then c * coeff p (k - i) else 0))"
haftmann@64795
  1116
    by (intro sum.cong) simp_all
wenzelm@65346
  1117
  also have "\<dots> = (if k < n then 0 else c * coeff p (k - n))"
haftmann@66799
  1118
    by simp
haftmann@64795
  1119
  finally show ?thesis .
haftmann@64795
  1120
qed
haftmann@64795
  1121
wenzelm@65346
  1122
lemma monom_1_dvd_iff': "monom 1 n dvd p \<longleftrightarrow> (\<forall>k<n. coeff p k = 0)"
haftmann@64795
  1123
proof
haftmann@64795
  1124
  assume "monom 1 n dvd p"
wenzelm@65346
  1125
  then obtain r where "p = monom 1 n * r"
wenzelm@65346
  1126
    by (rule dvdE)
wenzelm@65346
  1127
  then show "\<forall>k<n. coeff p k = 0"
wenzelm@65346
  1128
    by (simp add: coeff_mult)
haftmann@64795
  1129
next
haftmann@64795
  1130
  assume zero: "(\<forall>k<n. coeff p k = 0)"
haftmann@64795
  1131
  define r where "r = Abs_poly (\<lambda>k. coeff p (k + n))"
haftmann@64795
  1132
  have "\<forall>\<^sub>\<infinity>k. coeff p (k + n) = 0"
wenzelm@65346
  1133
    by (subst cofinite_eq_sequentially, subst eventually_sequentially_seg,
haftmann@64795
  1134
        subst cofinite_eq_sequentially [symmetric]) transfer
wenzelm@65346
  1135
  then have coeff_r [simp]: "coeff r k = coeff p (k + n)" for k
wenzelm@65346
  1136
    unfolding r_def by (subst poly.Abs_poly_inverse) simp_all
haftmann@64795
  1137
  have "p = monom 1 n * r"
wenzelm@65346
  1138
    by (rule poly_eqI, subst coeff_monom_mult) (simp_all add: zero)
wenzelm@65346
  1139
  then show "monom 1 n dvd p" by simp
haftmann@64795
  1140
qed
haftmann@64795
  1141
haftmann@64591
  1142
haftmann@64591
  1143
subsection \<open>Mapping polynomials\<close>
haftmann@64591
  1144
wenzelm@65346
  1145
definition map_poly :: "('a :: zero \<Rightarrow> 'b :: zero) \<Rightarrow> 'a poly \<Rightarrow> 'b poly"
wenzelm@65346
  1146
  where "map_poly f p = Poly (map f (coeffs p))"
haftmann@64591
  1147
haftmann@64591
  1148
lemma map_poly_0 [simp]: "map_poly f 0 = 0"
haftmann@64591
  1149
  by (simp add: map_poly_def)
haftmann@64591
  1150
haftmann@64591
  1151
lemma map_poly_1: "map_poly f 1 = [:f 1:]"
haftmann@64591
  1152
  by (simp add: map_poly_def)
haftmann@64591
  1153
haftmann@64591
  1154
lemma map_poly_1' [simp]: "f 1 = 1 \<Longrightarrow> map_poly f 1 = 1"
haftmann@65486
  1155
  by (simp add: map_poly_def one_pCons)
haftmann@64591
  1156
haftmann@64591
  1157
lemma coeff_map_poly:
haftmann@64591
  1158
  assumes "f 0 = 0"
wenzelm@65346
  1159
  shows "coeff (map_poly f p) n = f (coeff p n)"
wenzelm@65346
  1160
  by (auto simp: assms map_poly_def nth_default_def coeffs_def not_less Suc_le_eq coeff_eq_0
wenzelm@65346
  1161
      simp del: upt_Suc)
wenzelm@65346
  1162
wenzelm@65346
  1163
lemma coeffs_map_poly [code abstract]:
wenzelm@65346
  1164
  "coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))"
haftmann@64591
  1165
  by (simp add: map_poly_def)
haftmann@64591
  1166
wenzelm@65346
  1167
lemma coeffs_map_poly':
wenzelm@65346
  1168
  assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
wenzelm@65346
  1169
  shows "coeffs (map_poly f p) = map f (coeffs p)"
haftmann@66799
  1170
  using assms
haftmann@66799
  1171
  by (auto simp add: coeffs_map_poly strip_while_idem_iff
haftmann@66799
  1172
    last_coeffs_eq_coeff_degree no_trailing_unfold last_map)
haftmann@65390
  1173
haftmann@65390
  1174
lemma set_coeffs_map_poly:
haftmann@65390
  1175
  "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
haftmann@65390
  1176
  by (simp add: coeffs_map_poly')
haftmann@64591
  1177
haftmann@64591
  1178
lemma degree_map_poly:
haftmann@64591
  1179
  assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
wenzelm@65346
  1180
  shows "degree (map_poly f p) = degree p"
haftmann@64591
  1181
  by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms)
haftmann@64591
  1182
haftmann@64591
  1183
lemma map_poly_eq_0_iff:
haftmann@64591
  1184
  assumes "f 0 = 0" "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
wenzelm@65346
  1185
  shows "map_poly f p = 0 \<longleftrightarrow> p = 0"
haftmann@64591
  1186
proof -
wenzelm@65346
  1187
  have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" for n
wenzelm@65346
  1188
  proof -
wenzelm@65346
  1189
    have "coeff (map_poly f p) n = f (coeff p n)"
wenzelm@65346
  1190
      by (simp add: coeff_map_poly assms)
haftmann@64591
  1191
    also have "\<dots> = 0 \<longleftrightarrow> coeff p n = 0"
haftmann@64591
  1192
    proof (cases "n < length (coeffs p)")
haftmann@64591
  1193
      case True
wenzelm@65346
  1194
      then have "coeff p n \<in> set (coeffs p)"
wenzelm@65346
  1195
        by (auto simp: coeffs_def simp del: upt_Suc)
wenzelm@65346
  1196
      with assms show "f (coeff p n) = 0 \<longleftrightarrow> coeff p n = 0"
wenzelm@65346
  1197
        by auto
wenzelm@65346
  1198
    next
wenzelm@65346
  1199
      case False
wenzelm@65346
  1200
      then show ?thesis
wenzelm@65346
  1201
        by (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def)
wenzelm@65346
  1202
    qed
wenzelm@65346
  1203
    finally show ?thesis .
wenzelm@65346
  1204
  qed
wenzelm@65346
  1205
  then show ?thesis by (auto simp: poly_eq_iff)
haftmann@64591
  1206
qed
haftmann@64591
  1207
haftmann@64591
  1208
lemma map_poly_smult:
haftmann@64591
  1209
  assumes "f 0 = 0""\<And>c x. f (c * x) = f c * f x"
wenzelm@65346
  1210
  shows "map_poly f (smult c p) = smult (f c) (map_poly f p)"
haftmann@64591
  1211
  by (intro poly_eqI) (simp_all add: assms coeff_map_poly)
haftmann@64591
  1212
haftmann@64591
  1213
lemma map_poly_pCons:
haftmann@64591
  1214
  assumes "f 0 = 0"
wenzelm@65346
  1215
  shows "map_poly f (pCons c p) = pCons (f c) (map_poly f p)"
haftmann@64591
  1216
  by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits)
haftmann@64591
  1217
haftmann@64591
  1218
lemma map_poly_map_poly:
haftmann@64591
  1219
  assumes "f 0 = 0" "g 0 = 0"
wenzelm@65346
  1220
  shows "map_poly f (map_poly g p) = map_poly (f \<circ> g) p"
haftmann@64591
  1221
  by (intro poly_eqI) (simp add: coeff_map_poly assms)
haftmann@64591
  1222
haftmann@64591
  1223
lemma map_poly_id [simp]: "map_poly id p = p"
haftmann@64591
  1224
  by (simp add: map_poly_def)
haftmann@64591
  1225
haftmann@64591
  1226
lemma map_poly_id' [simp]: "map_poly (\<lambda>x. x) p = p"
haftmann@64591
  1227
  by (simp add: map_poly_def)
haftmann@64591
  1228
wenzelm@65346
  1229
lemma map_poly_cong:
haftmann@64591
  1230
  assumes "(\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = g x)"
wenzelm@65346
  1231
  shows "map_poly f p = map_poly g p"
haftmann@64591
  1232
proof -
wenzelm@65346
  1233
  from assms have "map f (coeffs p) = map g (coeffs p)"
wenzelm@65346
  1234
    by (intro map_cong) simp_all
wenzelm@65346
  1235
  then show ?thesis
wenzelm@65346
  1236
    by (simp only: coeffs_eq_iff coeffs_map_poly)
haftmann@64591
  1237
qed
haftmann@64591
  1238
haftmann@64591
  1239
lemma map_poly_monom: "f 0 = 0 \<Longrightarrow> map_poly f (monom c n) = monom (f c) n"
haftmann@64591
  1240
  by (intro poly_eqI) (simp_all add: coeff_map_poly)
haftmann@64591
  1241
haftmann@64591
  1242
lemma map_poly_idI:
haftmann@64591
  1243
  assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
wenzelm@65346
  1244
  shows "map_poly f p = p"
haftmann@64591
  1245
  using map_poly_cong[OF assms, of _ id] by simp
haftmann@64591
  1246
haftmann@64591
  1247
lemma map_poly_idI':
haftmann@64591
  1248
  assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
wenzelm@65346
  1249
  shows "p = map_poly f p"
haftmann@64591
  1250
  using map_poly_cong[OF assms, of _ id] by simp
haftmann@64591
  1251
haftmann@64591
  1252
lemma smult_conv_map_poly: "smult c p = map_poly (\<lambda>x. c * x) p"
haftmann@64591
  1253
  by (intro poly_eqI) (simp_all add: coeff_map_poly)
haftmann@64591
  1254
haftmann@64591
  1255
haftmann@65484
  1256
subsection \<open>Conversions\<close>
haftmann@65484
  1257
haftmann@65484
  1258
lemma of_nat_poly:
haftmann@65484
  1259
  "of_nat n = [:of_nat n:]"
haftmann@65486
  1260
  by (induct n) (simp_all add: one_pCons)
haftmann@65484
  1261
haftmann@65484
  1262
lemma of_nat_monom:
haftmann@65484
  1263
  "of_nat n = monom (of_nat n) 0"
haftmann@65484
  1264
  by (simp add: of_nat_poly monom_0)
haftmann@65484
  1265
haftmann@65484
  1266
lemma degree_of_nat [simp]:
haftmann@65484
  1267
  "degree (of_nat n) = 0"
eberlm@62065
  1268
  by (simp add: of_nat_poly)
eberlm@62065
  1269
haftmann@64795
  1270
lemma lead_coeff_of_nat [simp]:
haftmann@65484
  1271
  "lead_coeff (of_nat n) = of_nat n"
haftmann@64795
  1272
  by (simp add: of_nat_poly)
haftmann@64795
  1273
haftmann@65484
  1274
lemma of_int_poly:
haftmann@65484
  1275
  "of_int k = [:of_int k:]"
haftmann@64793
  1276
  by (simp only: of_int_of_nat of_nat_poly) simp
haftmann@64793
  1277
haftmann@65484
  1278
lemma of_int_monom:
haftmann@65484
  1279
  "of_int k = monom (of_int k) 0"
haftmann@65484
  1280
  by (simp add: of_int_poly monom_0)
haftmann@65484
  1281
haftmann@65484
  1282
lemma degree_of_int [simp]:
haftmann@65484
  1283
  "degree (of_int k) = 0"
haftmann@64795
  1284
  by (simp add: of_int_poly)
haftmann@64795
  1285
haftmann@64795
  1286
lemma lead_coeff_of_int [simp]:
haftmann@65484
  1287
  "lead_coeff (of_int k) = of_int k"
haftmann@64793
  1288
  by (simp add: of_int_poly)
eberlm@62065
  1289
eberlm@62065
  1290
lemma numeral_poly: "numeral n = [:numeral n:]"
haftmann@65484
  1291
proof -
haftmann@65484
  1292
  have "numeral n = of_nat (numeral n)"
haftmann@65484
  1293
    by simp
haftmann@65484
  1294
  also have "\<dots> = [:of_nat (numeral n):]"
haftmann@65484
  1295
    by (simp add: of_nat_poly)
haftmann@65484
  1296
  finally show ?thesis
haftmann@65484
  1297
    by simp
haftmann@65484
  1298
qed
haftmann@65484
  1299
haftmann@65484
  1300
lemma numeral_monom:
haftmann@65484
  1301
  "numeral n = monom (numeral n) 0"
haftmann@65484
  1302
  by (simp add: numeral_poly monom_0)
haftmann@65484
  1303
haftmann@65484
  1304
lemma degree_numeral [simp]:
haftmann@65484
  1305
  "degree (numeral n) = 0"
haftmann@65484
  1306
  by (simp add: numeral_poly)
haftmann@52380
  1307
wenzelm@65346
  1308
lemma lead_coeff_numeral [simp]:
haftmann@64795
  1309
  "lead_coeff (numeral n) = numeral n"
haftmann@64795
  1310
  by (simp add: numeral_poly)
haftmann@64795
  1311
haftmann@64591
  1312
wenzelm@60500
  1313
subsection \<open>Lemmas about divisibility\<close>
huffman@29979
  1314
wenzelm@65346
  1315
lemma dvd_smult:
wenzelm@65346
  1316
  assumes "p dvd q"
wenzelm@65346
  1317
  shows "p dvd smult a q"
huffman@29979
  1318
proof -
wenzelm@65346
  1319
  from assms obtain k where "q = p * k" ..
huffman@29979
  1320
  then have "smult a q = p * smult a k" by simp
huffman@29979
  1321
  then show "p dvd smult a q" ..
huffman@29979
  1322
qed
huffman@29979
  1323
wenzelm@65346
  1324
lemma dvd_smult_cancel: "p dvd smult a q \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> p dvd q"
wenzelm@65346
  1325
  for a :: "'a::field"
huffman@29979
  1326
  by (drule dvd_smult [where a="inverse a"]) simp
huffman@29979
  1327
wenzelm@65346
  1328
lemma dvd_smult_iff: "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
wenzelm@65346
  1329
  for a :: "'a::field"
huffman@29979
  1330
  by (safe elim!: dvd_smult dvd_smult_cancel)
huffman@29979
  1331
huffman@31663
  1332
lemma smult_dvd_cancel:
wenzelm@65346
  1333
  assumes "smult a p dvd q"
wenzelm@65346
  1334
  shows "p dvd q"
huffman@31663
  1335
proof -
wenzelm@65346
  1336
  from assms obtain k where "q = smult a p * k" ..
huffman@31663
  1337
  then have "q = p * smult a k" by simp
huffman@31663
  1338
  then show "p dvd q" ..
huffman@31663
  1339
qed
huffman@31663
  1340
wenzelm@65346
  1341
lemma smult_dvd: "p dvd q \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> smult a p dvd q"
wenzelm@65346
  1342
  for a :: "'a::field"
huffman@31663
  1343
  by (rule smult_dvd_cancel [where a="inverse a"]) simp
huffman@31663
  1344
wenzelm@65346
  1345
lemma smult_dvd_iff: "smult a p dvd q \<longleftrightarrow> (if a = 0 then q = 0 else p dvd q)"
wenzelm@65346
  1346
  for a :: "'a::field"
huffman@31663
  1347
  by (auto elim: smult_dvd smult_dvd_cancel)
huffman@31663
  1348
haftmann@64795
  1349
lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
haftmann@64795
  1350
proof -
haftmann@64795
  1351
  have "smult c p = [:c:] * p" by simp
haftmann@64795
  1352
  also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
haftmann@64795
  1353
  proof safe
wenzelm@65346
  1354
    assume *: "[:c:] * p dvd 1"
wenzelm@65346
  1355
    then show "p dvd 1"
wenzelm@65346
  1356
      by (rule dvd_mult_right)
wenzelm@65346
  1357
    from * obtain q where q: "1 = [:c:] * p * q"
wenzelm@65346
  1358
      by (rule dvdE)
wenzelm@65346
  1359
    have "c dvd c * (coeff p 0 * coeff q 0)"
wenzelm@65346
  1360
      by simp
wenzelm@65346
  1361
    also have "\<dots> = coeff ([:c:] * p * q) 0"
wenzelm@65346
  1362
      by (simp add: mult.assoc coeff_mult)
wenzelm@65346
  1363
    also note q [symmetric]
wenzelm@65346
  1364
    finally have "c dvd coeff 1 0" .
wenzelm@65346
  1365
    then show "c dvd 1" by simp
haftmann@64795
  1366
  next
haftmann@64795
  1367
    assume "c dvd 1" "p dvd 1"
wenzelm@65346
  1368
    from this(1) obtain d where "1 = c * d"
wenzelm@65346
  1369
      by (rule dvdE)
wenzelm@65346
  1370
    then have "1 = [:c:] * [:d:]"
haftmann@65486
  1371
      by (simp add: one_pCons ac_simps)
wenzelm@65346
  1372
    then have "[:c:] dvd 1"
wenzelm@65346
  1373
      by (rule dvdI)
wenzelm@65346
  1374
    from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1"
wenzelm@65346
  1375
      by simp
haftmann@64795
  1376
  qed
haftmann@64795
  1377
  finally show ?thesis .
haftmann@64795
  1378
qed
haftmann@64795
  1379
huffman@29451
  1380
wenzelm@60500
  1381
subsection \<open>Polynomials form an integral domain\<close>
huffman@29451
  1382
eberlm@63498
  1383
instance poly :: (idom) idom ..
huffman@29451
  1384
haftmann@65577
  1385
instance poly :: ("{ring_char_0, comm_ring_1}") ring_char_0
haftmann@65577
  1386
  by standard (auto simp add: of_nat_poly intro: injI)
haftmann@65577
  1387
wenzelm@65346
  1388
lemma degree_mult_eq: "p \<noteq> 0 \<Longrightarrow> q \<noteq> 0 \<Longrightarrow> degree (p * q) = degree p + degree q"
wenzelm@65346
  1389
  for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
wenzelm@65346
  1390
  by (rule order_antisym [OF degree_mult_le le_degree]) (simp add: coeff_mult_degree_sum)
huffman@29451
  1391
haftmann@64591
  1392
lemma degree_mult_eq_0:
wenzelm@65346
  1393
  "degree (p * q) = 0 \<longleftrightarrow> p = 0 \<or> q = 0 \<or> (p \<noteq> 0 \<and> q \<noteq> 0 \<and> degree p = 0 \<and> degree q = 0)"
wenzelm@65346
  1394
  for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
wenzelm@65346
  1395
  by (auto simp: degree_mult_eq)
haftmann@64591
  1396
eberlm@66550
  1397
lemma degree_power_eq: "p \<noteq> 0 \<Longrightarrow> degree ((p :: 'a :: idom poly) ^ n) = n * degree p"
eberlm@66550
  1398
  by (induction n) (simp_all add: degree_mult_eq)
eberlm@66550
  1399
haftmann@60570
  1400
lemma degree_mult_right_le:
eberlm@63498
  1401
  fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
haftmann@60570
  1402
  assumes "q \<noteq> 0"
haftmann@60570
  1403
  shows "degree p \<le> degree (p * q)"
haftmann@60570
  1404
  using assms by (cases "p = 0") (simp_all add: degree_mult_eq)
haftmann@60570
  1405
wenzelm@65346
  1406
lemma coeff_degree_mult: "coeff (p * q) (degree (p * q)) = coeff q (degree q) * coeff p (degree p)"
wenzelm@65346
  1407
  for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
wenzelm@65346
  1408
  by (cases "p = 0 \<or> q = 0") (auto simp: degree_mult_eq coeff_mult_degree_sum mult_ac)
wenzelm@65346
  1409
wenzelm@65346
  1410
lemma dvd_imp_degree_le: "p dvd q \<Longrightarrow> q \<noteq> 0 \<Longrightarrow> degree p \<le> degree q"
wenzelm@65346
  1411
  for p q :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
eberlm@62128
  1412
  by (erule dvdE, hypsubst, subst degree_mult_eq) auto
huffman@29451
  1413
eberlm@62128
  1414
lemma divides_degree:
wenzelm@65346
  1415
  fixes p q :: "'a ::{comm_semiring_1,semiring_no_zero_divisors} poly"
wenzelm@65346
  1416
  assumes "p dvd q"
eberlm@62128
  1417
  shows "degree p \<le> degree q \<or> q = 0"
wenzelm@65346
  1418
  by (metis dvd_imp_degree_le assms)
wenzelm@65346
  1419
eberlm@63498
  1420
lemma const_poly_dvd_iff:
wenzelm@65346
  1421
  fixes c :: "'a::{comm_semiring_1,semiring_no_zero_divisors}"
eberlm@63498
  1422
  shows "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)"
eberlm@63498
  1423
proof (cases "c = 0 \<or> p = 0")
wenzelm@65346
  1424
  case True
wenzelm@65346
  1425
  then show ?thesis
wenzelm@65346
  1426
    by (auto intro!: poly_eqI)
wenzelm@65346
  1427
next
eberlm@63498
  1428
  case False
eberlm@63498
  1429
  show ?thesis
eberlm@63498
  1430
  proof
eberlm@63498
  1431
    assume "[:c:] dvd p"
wenzelm@65346
  1432
    then show "\<forall>n. c dvd coeff p n"
wenzelm@65346
  1433
      by (auto elim!: dvdE simp: coeffs_def)
eberlm@63498
  1434
  next
eberlm@63498
  1435
    assume *: "\<forall>n. c dvd coeff p n"
wenzelm@65346
  1436
    define mydiv where "mydiv x y = (SOME z. x = y * z)" for x y :: 'a
eberlm@63498
  1437
    have mydiv: "x = y * mydiv x y" if "y dvd x" for x y
eberlm@63498
  1438
      using that unfolding mydiv_def dvd_def by (rule someI_ex)
eberlm@63498
  1439
    define q where "q = Poly (map (\<lambda>a. mydiv a c) (coeffs p))"
eberlm@63498
  1440
    from False * have "p = q * [:c:]"
wenzelm@65346
  1441
      by (intro poly_eqI)
wenzelm@65346
  1442
        (auto simp: q_def nth_default_def not_less length_coeffs_degree coeffs_nth
wenzelm@65346
  1443
          intro!: coeff_eq_0 mydiv)
wenzelm@65346
  1444
    then show "[:c:] dvd p"
wenzelm@65346
  1445
      by (simp only: dvd_triv_right)
eberlm@63498
  1446
  qed
wenzelm@65346
  1447
qed
wenzelm@65346
  1448
wenzelm@65346
  1449
lemma const_poly_dvd_const_poly_iff [simp]: "[:a:] dvd [:b:] \<longleftrightarrow> a dvd b"
wenzelm@65346
  1450
  for a b :: "'a::{comm_semiring_1,semiring_no_zero_divisors}"
eberlm@63498
  1451
  by (subst const_poly_dvd_iff) (auto simp: coeff_pCons split: nat.splits)
eberlm@63498
  1452
wenzelm@65346
  1453
lemma lead_coeff_mult: "lead_coeff (p * q) = lead_coeff p * lead_coeff q"
wenzelm@65346
  1454
  for p q :: "'a::{comm_semiring_0, semiring_no_zero_divisors} poly"
wenzelm@65346
  1455
  by (cases "p = 0 \<or> q = 0") (auto simp: coeff_mult_degree_sum degree_mult_eq)
wenzelm@65346
  1456
wenzelm@65346
  1457
lemma lead_coeff_smult: "lead_coeff (smult c p) = c * lead_coeff p"
wenzelm@65346
  1458
  for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
haftmann@64795
  1459
proof -
haftmann@64795
  1460
  have "smult c p = [:c:] * p" by simp
haftmann@64795
  1461
  also have "lead_coeff \<dots> = c * lead_coeff p"
haftmann@64795
  1462
    by (subst lead_coeff_mult) simp_all
haftmann@64795
  1463
  finally show ?thesis .
haftmann@64795
  1464
qed
haftmann@64795
  1465
haftmann@64795
  1466
lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1"
haftmann@64795
  1467
  by simp
haftmann@64795
  1468
wenzelm@65346
  1469
lemma lead_coeff_power: "lead_coeff (p ^ n) = lead_coeff p ^ n"
wenzelm@65346
  1470
  for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
wenzelm@65346
  1471
  by (induct n) (simp_all add: lead_coeff_mult)
haftmann@64795
  1472
huffman@29451
  1473
wenzelm@60500
  1474
subsection \<open>Polynomials form an ordered integral domain\<close>
huffman@29878
  1475
eberlm@63498
  1476
definition pos_poly :: "'a::linordered_semidom poly \<Rightarrow> bool"
wenzelm@65346
  1477
  where "pos_poly p \<longleftrightarrow> 0 < coeff p (degree p)"
wenzelm@65346
  1478
wenzelm@65346
  1479
lemma pos_poly_pCons: "pos_poly (pCons a p) \<longleftrightarrow> pos_poly p \<or> (p = 0 \<and> 0 < a)"
wenzelm@65346
  1480
  by (simp add: pos_poly_def)
huffman@29878
  1481
huffman@29878
  1482
lemma not_pos_poly_0 [simp]: "\<not> pos_poly 0"
wenzelm@65346
  1483
  by (simp add: pos_poly_def)
wenzelm@65346
  1484
wenzelm@65346
  1485
lemma pos_poly_add: "pos_poly p \<Longrightarrow> pos_poly q \<Longrightarrow> pos_poly (p + q)"
wenzelm@65346
  1486
  apply (induct p arbitrary: q)
wenzelm@65346
  1487
   apply simp
wenzelm@65346
  1488
  apply (case_tac q)
wenzelm@65346
  1489
  apply (force simp add: pos_poly_pCons add_pos_pos)
huffman@29878
  1490
  done
huffman@29878
  1491
wenzelm@65346
  1492
lemma pos_poly_mult: "pos_poly p \<Longrightarrow> pos_poly q \<Longrightarrow> pos_poly (p * q)"
huffman@29878
  1493
  unfolding pos_poly_def
huffman@29878
  1494
  apply (subgoal_tac "p \<noteq> 0 \<and> q \<noteq> 0")
wenzelm@65346
  1495
   apply (simp add: degree_mult_eq coeff_mult_degree_sum)
huffman@29878
  1496
  apply auto
huffman@29878
  1497
  done
huffman@29878
  1498
wenzelm@65346
  1499
lemma pos_poly_total: "p = 0 \<or> pos_poly p \<or> pos_poly (- p)"
wenzelm@65346
  1500
  for p :: "'a::linordered_idom poly"
wenzelm@65346
  1501
  by (induct p) (auto simp: pos_poly_pCons)
wenzelm@65346
  1502
wenzelm@65346
  1503
lemma pos_poly_coeffs [code]: "pos_poly p \<longleftrightarrow> (let as = coeffs p in as \<noteq> [] \<and> last as > 0)"
wenzelm@65346
  1504
  (is "?lhs \<longleftrightarrow> ?rhs")
haftmann@52380
  1505
proof
wenzelm@65346
  1506
  assume ?rhs
wenzelm@65346
  1507
  then show ?lhs
wenzelm@65346
  1508
    by (auto simp add: pos_poly_def last_coeffs_eq_coeff_degree)
haftmann@52380
  1509
next
wenzelm@65346
  1510
  assume ?lhs
wenzelm@65346
  1511
  then have *: "0 < coeff p (degree p)"
wenzelm@65346
  1512
    by (simp add: pos_poly_def)
wenzelm@65346
  1513
  then have "p \<noteq> 0"
wenzelm@65346
  1514
    by auto
wenzelm@65346
  1515
  with * show ?rhs
wenzelm@65346
  1516
    by (simp add: last_coeffs_eq_coeff_degree)
haftmann@52380
  1517
qed
haftmann@52380
  1518
haftmann@35028
  1519
instantiation poly :: (linordered_idom) linordered_idom
huffman@29878
  1520
begin
huffman@29878
  1521
wenzelm@65346
  1522
definition "x < y \<longleftrightarrow> pos_poly (y - x)"
wenzelm@65346
  1523
wenzelm@65346
  1524
definition "x \<le> y \<longleftrightarrow> x = y \<or> pos_poly (y - x)"
wenzelm@65346
  1525
wenzelm@65346
  1526
definition "\<bar>x::'a poly\<bar> = (if x < 0 then - x else x)"
wenzelm@65346
  1527
wenzelm@65346
  1528
definition "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
huffman@29878
  1529
wenzelm@60679
  1530
instance
wenzelm@60679
  1531
proof
wenzelm@60679
  1532
  fix x y z :: "'a poly"
huffman@29878
  1533
  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
huffman@29878
  1534
    unfolding less_eq_poly_def less_poly_def
huffman@29878
  1535
    apply safe
wenzelm@65346
  1536
     apply simp
huffman@29878
  1537
    apply (drule (1) pos_poly_add)
huffman@29878
  1538
    apply simp
huffman@29878
  1539
    done
wenzelm@60679
  1540
  show "x \<le> x"
wenzelm@65346
  1541
    by (simp add: less_eq_poly_def)
wenzelm@60679
  1542
  show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
huffman@29878
  1543
    unfolding less_eq_poly_def
huffman@29878
  1544
    apply safe
huffman@29878
  1545
    apply (drule (1) pos_poly_add)
huffman@29878
  1546
    apply (simp add: algebra_simps)
huffman@29878
  1547
    done
wenzelm@60679
  1548
  show "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
huffman@29878
  1549
    unfolding less_eq_poly_def
huffman@29878
  1550
    apply safe
huffman@29878
  1551
    apply (drule (1) pos_poly_add)
huffman@29878
  1552
    apply simp
huffman@29878
  1553
    done
wenzelm@60679
  1554
  show "x \<le> y \<Longrightarrow> z + x \<le> z + y"
huffman@29878
  1555
    unfolding less_eq_poly_def
huffman@29878
  1556
    apply safe
huffman@29878
  1557
    apply (simp add: algebra_simps)
huffman@29878
  1558
    done
huffman@29878
  1559
  show "x \<le> y \<or> y \<le> x"
huffman@29878
  1560
    unfolding less_eq_poly_def
huffman@29878
  1561
    using pos_poly_total [of "x - y"]
huffman@29878
  1562
    by auto
wenzelm@60679
  1563
  show "x < y \<Longrightarrow> 0 < z \<Longrightarrow> z * x < z * y"
wenzelm@65346
  1564
    by (simp add: less_poly_def right_diff_distrib [symmetric] pos_poly_mult)
huffman@29878
  1565
  show "\<bar>x\<bar> = (if x < 0 then - x else x)"
huffman@29878
  1566
    by (rule abs_poly_def)
huffman@29878
  1567
  show "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
huffman@29878
  1568
    by (rule sgn_poly_def)
huffman@29878
  1569
qed
huffman@29878
  1570
huffman@29878
  1571
end
huffman@29878
  1572
wenzelm@60500
  1573
text \<open>TODO: Simplification rules for comparisons\<close>
huffman@29878
  1574
huffman@29878
  1575
wenzelm@60500
  1576
subsection \<open>Synthetic division and polynomial roots\<close>
haftmann@52380
  1577
wenzelm@65346
  1578
subsubsection \<open>Synthetic division\<close>
wenzelm@65346
  1579
wenzelm@65346
  1580
text \<open>Synthetic division is simply division by the linear polynomial @{term "x - c"}.\<close>
haftmann@52380
  1581
haftmann@52380
  1582
definition synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a"
wenzelm@65346
  1583
  where "synthetic_divmod p c = fold_coeffs (\<lambda>a (q, r). (pCons r q, a + c * r)) p (0, 0)"
haftmann@52380
  1584
haftmann@52380
  1585
definition synthetic_div :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly"
wenzelm@65346
  1586
  where "synthetic_div p c = fst (synthetic_divmod p c)"
wenzelm@65346
  1587
wenzelm@65346
  1588
lemma synthetic_divmod_0 [simp]: "synthetic_divmod 0 c = (0, 0)"
haftmann@52380
  1589
  by (simp add: synthetic_divmod_def)
haftmann@52380
  1590
haftmann@52380
  1591
lemma synthetic_divmod_pCons [simp]:
haftmann@52380
  1592
  "synthetic_divmod (pCons a p) c = (\<lambda>(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)"
haftmann@52380
  1593
  by (cases "p = 0 \<and> a = 0") (auto simp add: synthetic_divmod_def)
haftmann@52380
  1594
wenzelm@65346
  1595
lemma synthetic_div_0 [simp]: "synthetic_div 0 c = 0"
wenzelm@65346
  1596
  by (simp add: synthetic_div_def)
haftmann@52380
  1597
haftmann@52380
  1598
lemma synthetic_div_unique_lemma: "smult c p = pCons a p \<Longrightarrow> p = 0"
wenzelm@65346
  1599
  by (induct p arbitrary: a) simp_all
wenzelm@65346
  1600
wenzelm@65346
  1601
lemma snd_synthetic_divmod: "snd (synthetic_divmod p c) = poly p c"
wenzelm@65346
  1602
  by (induct p) (simp_all add: split_def)
haftmann@52380
  1603
haftmann@52380
  1604
lemma synthetic_div_pCons [simp]:
haftmann@52380
  1605
  "synthetic_div (pCons a p) c = pCons (poly p c) (synthetic_div p c)"
wenzelm@65346
  1606
  by (simp add: synthetic_div_def split_def snd_synthetic_divmod)
wenzelm@65346
  1607
wenzelm@65346
  1608
lemma synthetic_div_eq_0_iff: "synthetic_div p c = 0 \<longleftrightarrow> degree p = 0"
wenzelm@63649
  1609
proof (induct p)
wenzelm@63649
  1610
  case 0
wenzelm@63649
  1611
  then show ?case by simp
wenzelm@63649
  1612
next
wenzelm@63649
  1613
  case (pCons a p)
wenzelm@63649
  1614
  then show ?case by (cases p) simp
wenzelm@63649
  1615
qed
haftmann@52380
  1616
wenzelm@65346
  1617
lemma degree_synthetic_div: "degree (synthetic_div p c) = degree p - 1"
wenzelm@63649
  1618
  by (induct p) (simp_all add: synthetic_div_eq_0_iff)
haftmann@52380
  1619
haftmann@52380
  1620
lemma synthetic_div_correct:
haftmann@52380
  1621
  "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)"
haftmann@52380
  1622
  by (induct p) simp_all
haftmann@52380
  1623
wenzelm@65346
  1624
lemma synthetic_div_unique: "p + smult c q = pCons r q \<Longrightarrow> r = poly p c \<and> q = synthetic_div p c"
wenzelm@65346
  1625
  apply (induct p arbitrary: q r)
wenzelm@65346
  1626
   apply simp
wenzelm@65346
  1627
   apply (frule synthetic_div_unique_lemma)
wenzelm@65346
  1628
   apply simp
wenzelm@65346
  1629
  apply (case_tac q, force)
wenzelm@65346
  1630
  done
wenzelm@65346
  1631
wenzelm@65346
  1632
lemma synthetic_div_correct': "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p"
wenzelm@65346
  1633
  for c :: "'a::comm_ring_1"
wenzelm@65346
  1634
  using synthetic_div_correct [of p c] by (simp add: algebra_simps)
wenzelm@65346
  1635
wenzelm@65346
  1636
haftmann@64795
  1637
subsubsection \<open>Polynomial roots\<close>
wenzelm@65346
  1638
wenzelm@65346
  1639
lemma poly_eq_0_iff_dvd: "poly p c = 0 \<longleftrightarrow> [:- c, 1:] dvd p"
wenzelm@65346
  1640
  (is "?lhs \<longleftrightarrow> ?rhs")
wenzelm@65346
  1641
  for c :: "'a::comm_ring_1"
haftmann@52380
  1642
proof
wenzelm@65346
  1643
  assume ?lhs
wenzelm@65346
  1644
  with synthetic_div_correct' [of c p] have "p = [:-c, 1:] * synthetic_div p c" by simp
wenzelm@65346
  1645
  then show ?rhs ..
haftmann@52380
  1646
next
wenzelm@65346
  1647
  assume ?rhs
haftmann@52380
  1648
  then obtain k where "p = [:-c, 1:] * k" by (rule dvdE)
wenzelm@65346
  1649
  then show ?lhs by simp
haftmann@52380
  1650
qed
haftmann@52380
  1651
wenzelm@65346
  1652
lemma dvd_iff_poly_eq_0: "[:c, 1:] dvd p \<longleftrightarrow> poly p (- c) = 0"
wenzelm@65346
  1653
  for c :: "'a::comm_ring_1"
haftmann@52380
  1654
  by (simp add: poly_eq_0_iff_dvd)
haftmann@52380
  1655
wenzelm@65346
  1656
lemma poly_roots_finite: "p \<noteq> 0 \<Longrightarrow> finite {x. poly p x = 0}"
wenzelm@65346
  1657
  for p :: "'a::{comm_ring_1,ring_no_zero_divisors} poly"
haftmann@52380
  1658
proof (induct n \<equiv> "degree p" arbitrary: p)
wenzelm@65346
  1659
  case 0
haftmann@52380
  1660
  then obtain a where "a \<noteq> 0" and "p = [:a:]"
wenzelm@65346
  1661
    by (cases p) (simp split: if_splits)
wenzelm@65346
  1662
  then show "finite {x. poly p x = 0}"
wenzelm@65346
  1663
    by simp
haftmann@52380
  1664
next
wenzelm@65346
  1665
  case (Suc n)
haftmann@52380
  1666
  show "finite {x. poly p x = 0}"
haftmann@52380
  1667
  proof (cases "\<exists>x. poly p x = 0")
haftmann@52380
  1668
    case False
haftmann@52380
  1669
    then show "finite {x. poly p x = 0}" by simp
haftmann@52380
  1670
  next
haftmann@52380
  1671
    case True
haftmann@52380
  1672
    then obtain a where "poly p a = 0" ..
wenzelm@65346
  1673
    then have "[:-a, 1:] dvd p"
wenzelm@65346
  1674
      by (simp only: poly_eq_0_iff_dvd)
haftmann@52380
  1675
    then obtain k where k: "p = [:-a, 1:] * k" ..
wenzelm@65346
  1676
    with \<open>p \<noteq> 0\<close> have "k \<noteq> 0"
wenzelm@65346
  1677
      by auto
haftmann@52380
  1678
    with k have "degree p = Suc (degree k)"
haftmann@52380
  1679
      by (simp add: degree_mult_eq del: mult_pCons_left)
wenzelm@65346
  1680
    with \<open>Suc n = degree p\<close> have "n = degree k"
wenzelm@65346
  1681
      by simp
wenzelm@65346
  1682
    from this \<open>k \<noteq> 0\<close> have "finite {x. poly k x = 0}"
wenzelm@65346
  1683
      by (rule Suc.hyps)
wenzelm@65346
  1684
    then have "finite (insert a {x. poly k x = 0})"
wenzelm@65346
  1685
      by simp
haftmann@52380
  1686
    then show "finite {x. poly p x = 0}"
wenzelm@57862
  1687
      by (simp add: k Collect_disj_eq del: mult_pCons_left)
haftmann@52380
  1688
  qed
haftmann@52380
  1689
qed
haftmann@52380
  1690
wenzelm@65346
  1691
lemma poly_eq_poly_eq_iff: "poly p = poly q \<longleftrightarrow> p = q"
wenzelm@65346
  1692
  (is "?lhs \<longleftrightarrow> ?rhs")
wenzelm@65346
  1693
  for p q :: "'a::{comm_ring_1,ring_no_zero_divisors,ring_char_0} poly"
haftmann@52380
  1694
proof
wenzelm@65346
  1695
  assume ?rhs
wenzelm@65346
  1696
  then show ?lhs by simp
haftmann@52380
  1697
next
wenzelm@65346
  1698
  assume ?lhs
wenzelm@65346
  1699
  have "poly p = poly 0 \<longleftrightarrow> p = 0" for p :: "'a poly"
wenzelm@65346
  1700
    apply (cases "p = 0")
wenzelm@65346
  1701
     apply simp_all
wenzelm@65346
  1702
    apply (drule poly_roots_finite)
wenzelm@65346
  1703
    apply (auto simp add: infinite_UNIV_char_0)
wenzelm@65346
  1704
    done
wenzelm@65346
  1705
  from \<open>?lhs\<close> and this [of "p - q"] show ?rhs
wenzelm@65346
  1706
    by auto
haftmann@52380
  1707
qed
haftmann@52380
  1708
wenzelm@65346
  1709
lemma poly_all_0_iff_0: "(\<forall>x. poly p x = 0) \<longleftrightarrow> p = 0"
wenzelm@65346
  1710
  for p :: "'a::{ring_char_0,comm_ring_1,ring_no_zero_divisors} poly"
haftmann@52380
  1711
  by (auto simp add: poly_eq_poly_eq_iff [symmetric])
haftmann@52380
  1712
wenzelm@65346
  1713
haftmann@64795
  1714
subsubsection \<open>Order of polynomial roots\<close>
huffman@29977
  1715
haftmann@52380
  1716
definition order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat"
wenzelm@65346
  1717
  where "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
wenzelm@65346
  1718
wenzelm@65346
  1719
lemma coeff_linear_power: "coeff ([:a, 1:] ^ n) n = 1"
wenzelm@65346
  1720
  for a :: "'a::comm_semiring_1"
wenzelm@65346
  1721
  apply (induct n)
wenzelm@65346
  1722
   apply simp_all
wenzelm@65346
  1723
  apply (subst coeff_eq_0)
wenzelm@65346
  1724
   apply (auto intro: le_less_trans degree_power_le)
wenzelm@65346
  1725
  done
wenzelm@65346
  1726
wenzelm@65346
  1727
lemma degree_linear_power: "degree ([:a, 1:] ^ n) = n"
wenzelm@65346
  1728
  for a :: "'a::comm_semiring_1"
wenzelm@65346
  1729
  apply (rule order_antisym)
wenzelm@65346
  1730
   apply (rule ord_le_eq_trans [OF degree_power_le])
wenzelm@65346
  1731
   apply simp
wenzelm@65346
  1732
  apply (rule le_degree)
wenzelm@65346
  1733
  apply (simp add: coeff_linear_power)
wenzelm@65346
  1734
  done
huffman@29977
  1735
huffman@29977
  1736
lemma order_1: "[:-a, 1:] ^ order a p dvd p"
wenzelm@65346
  1737
  apply (cases "p = 0")
wenzelm@65346
  1738
   apply simp
wenzelm@65346
  1739
  apply (cases "order a p")
wenzelm@65346
  1740
   apply simp
wenzelm@65346
  1741
  apply (subgoal_tac "nat < (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)")
wenzelm@65346
  1742
   apply (drule not_less_Least)
wenzelm@65346
  1743
   apply simp
wenzelm@65346
  1744
  apply (fold order_def)
wenzelm@65346
  1745
  apply simp
wenzelm@65346
  1746
  done
huffman@29977
  1747
huffman@29977
  1748
lemma order_2: "p \<noteq> 0 \<Longrightarrow> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
wenzelm@65346
  1749
  unfolding order_def
wenzelm@65346
  1750
  apply (rule LeastI_ex)
wenzelm@65346
  1751
  apply (rule_tac x="degree p" in exI)
wenzelm@65346
  1752
  apply (rule notI)
wenzelm@65346
  1753
  apply (drule (1) dvd_imp_degree_le)
wenzelm@65346
  1754
  apply (simp only: degree_linear_power)
wenzelm@65346
  1755
  done
wenzelm@65346
  1756
wenzelm@65346
  1757
lemma order: "p \<noteq> 0 \<Longrightarrow> [:-a, 1:] ^ order a p dvd p \<and> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
wenzelm@65346
  1758
  by (rule conjI [OF order_1 order_2])
huffman@29977
  1759
huffman@29977
  1760
lemma order_degree:
huffman@29977
  1761
  assumes p: "p \<noteq> 0"
huffman@29977
  1762
  shows "order a p \<le> degree p"
huffman@29977
  1763
proof -
huffman@29977
  1764
  have "order a p = degree ([:-a, 1:] ^ order a p)"
huffman@29977
  1765
    by (simp only: degree_linear_power)
wenzelm@65346
  1766
  also from order_1 p have "\<dots> \<le> degree p"
wenzelm@65346
  1767
    by (rule dvd_imp_degree_le)
huffman@29977
  1768
  finally show ?thesis .
huffman@29977
  1769
qed
huffman@29977
  1770
huffman@29977
  1771
lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0"
wenzelm@65346
  1772
  apply (cases "p = 0")
wenzelm@65346
  1773
   apply simp_all
wenzelm@65346
  1774
  apply (rule iffI)
wenzelm@65346
  1775
   apply (metis order_2 not_gr0 poly_eq_0_iff_dvd power_0 power_Suc_0 power_one_right)
wenzelm@65346
  1776
  unfolding poly_eq_0_iff_dvd
wenzelm@65346
  1777
  apply (metis dvd_power dvd_trans order_1)
wenzelm@65346
  1778
  done
huffman@29977
  1779
eberlm@62065
  1780
lemma order_0I: "poly p a \<noteq> 0 \<Longrightarrow> order a p = 0"
eberlm@62065
  1781
  by (subst (asm) order_root) auto
eberlm@62065
  1782
haftmann@64795
  1783
lemma order_unique_lemma:
haftmann@64795
  1784
  fixes p :: "'a::idom poly"
haftmann@64795
  1785
  assumes "[:-a, 1:] ^ n dvd p" "\<not> [:-a, 1:] ^ Suc n dvd p"
haftmann@64795
  1786
  shows "n = order a p"
wenzelm@65346
  1787
  unfolding Polynomial.order_def
wenzelm@65346
  1788
  apply (rule Least_equality [symmetric])
wenzelm@65346
  1789
   apply (fact assms)
wenzelm@65346
  1790
  apply (rule classical)
wenzelm@65346
  1791
  apply (erule notE)
wenzelm@65346
  1792
  unfolding not_less_eq_eq
wenzelm@65346
  1793
  using assms(1)
wenzelm@65346
  1794
  apply (rule power_le_dvd)
wenzelm@65346
  1795
  apply assumption
haftmann@64795
  1796
  done
wenzelm@65346
  1797
haftmann@64795
  1798
lemma order_mult: "p * q \<noteq> 0 \<Longrightarrow> order a (p * q) = order a p + order a q"
haftmann@64795
  1799
proof -
haftmann@64795
  1800
  define i where "i = order a p"
haftmann@64795
  1801
  define j where "j = order a q"
haftmann@64795
  1802
  define t where "t = [:-a, 1:]"
haftmann@64795
  1803
  have t_dvd_iff: "\<And>u. t dvd u \<longleftrightarrow> poly u a = 0"
wenzelm@65346
  1804
    by (simp add: t_def dvd_iff_poly_eq_0)
haftmann@64795
  1805
  assume "p * q \<noteq> 0"
haftmann@64795
  1806
  then show "order a (p * q) = i + j"
haftmann@64795
  1807
    apply clarsimp
haftmann@64795
  1808
    apply (drule order [where a=a and p=p, folded i_def t_def])
haftmann@64795
  1809
    apply (drule order [where a=a and p=q, folded j_def t_def])
haftmann@64795
  1810
    apply clarify
haftmann@64795
  1811
    apply (erule dvdE)+
haftmann@64795
  1812
    apply (rule order_unique_lemma [symmetric], fold t_def)
wenzelm@65346
  1813
     apply (simp_all add: power_add t_dvd_iff)
haftmann@64795
  1814
    done
haftmann@64795
  1815
qed
haftmann@64795
  1816
haftmann@64795
  1817
lemma order_smult:
wenzelm@65346
  1818
  assumes "c \<noteq> 0"
haftmann@64795
  1819
  shows "order x (smult c p) = order x p"
haftmann@64795
  1820
proof (cases "p = 0")
wenzelm@65346
  1821
  case True
wenzelm@65346
  1822
  then show ?thesis
wenzelm@65346
  1823
    by simp
wenzelm@65346
  1824
next
haftmann@64795
  1825
  case False
haftmann@64795
  1826
  have "smult c p = [:c:] * p" by simp
wenzelm@65346
  1827
  also from assms False have "order x \<dots> = order x [:c:] + order x p"
haftmann@64795
  1828
    by (subst order_mult) simp_all
wenzelm@65346
  1829
  also have "order x [:c:] = 0"
wenzelm@65346
  1830
    by (rule order_0I) (use assms in auto)
wenzelm@65346
  1831
  finally show ?thesis
wenzelm@65346
  1832
    by simp
wenzelm@65346
  1833
qed
haftmann@64795
  1834
haftmann@64795
  1835
(* Next two lemmas contributed by Wenda Li *)
wenzelm@65346
  1836
lemma order_1_eq_0 [simp]:"order x 1 = 0"
haftmann@64795
  1837
  by (metis order_root poly_1 zero_neq_one)
haftmann@64795
  1838
wenzelm@65346
  1839
lemma order_power_n_n: "order a ([:-a,1:]^n)=n"
haftmann@64795
  1840
proof (induct n) (*might be proved more concisely using nat_less_induct*)
haftmann@64795
  1841
  case 0
wenzelm@65346
  1842
  then show ?case
wenzelm@65346
  1843
    by (metis order_root poly_1 power_0 zero_neq_one)
wenzelm@65346
  1844
next
haftmann@64795
  1845
  case (Suc n)
wenzelm@65346
  1846
  have "order a ([:- a, 1:] ^ Suc n) = order a ([:- a, 1:] ^ n) + order a [:-a,1:]"
wenzelm@65346
  1847
    by (metis (no_types, hide_lams) One_nat_def add_Suc_right monoid_add_class.add.right_neutral
haftmann@64795
  1848
      one_neq_zero order_mult pCons_eq_0_iff power_add power_eq_0_iff power_one_right)
wenzelm@65346
  1849
  moreover have "order a [:-a,1:] = 1"
wenzelm@65346
  1850
    unfolding order_def
wenzelm@65346
  1851
  proof (rule Least_equality, rule notI)
wenzelm@65346
  1852
    assume "[:- a, 1:] ^ Suc 1 dvd [:- a, 1:]"
wenzelm@65346
  1853
    then have "degree ([:- a, 1:] ^ Suc 1) \<le> degree ([:- a, 1:])"
wenzelm@65346
  1854
      by (rule dvd_imp_degree_le) auto
wenzelm@65346
  1855
    then show False
wenzelm@65346
  1856
      by auto
wenzelm@65346
  1857
  next
wenzelm@65346
  1858
    fix y
wenzelm@65346
  1859
    assume *: "\<not> [:- a, 1:] ^ Suc y dvd [:- a, 1:]"
wenzelm@65346
  1860
    show "1 \<le> y"
wenzelm@65346
  1861
    proof (rule ccontr)
wenzelm@65346
  1862
      assume "\<not> 1 \<le> y"
wenzelm@65346
  1863
      then have "y = 0" by auto
wenzelm@65346
  1864
      then have "[:- a, 1:] ^ Suc y dvd [:- a, 1:]" by auto
wenzelm@65346
  1865
      with * show False by auto
haftmann@64795
  1866
    qed
wenzelm@65346
  1867
  qed
wenzelm@65346
  1868
  ultimately show ?case
wenzelm@65346
  1869
    using Suc by auto
haftmann@64795
  1870
qed
haftmann@64795
  1871
wenzelm@65346
  1872
lemma order_0_monom [simp]: "c \<noteq> 0 \<Longrightarrow> order 0 (monom c n) = n"
wenzelm@65346
  1873
  using order_power_n_n[of 0 n] by (simp add: monom_altdef order_smult)
wenzelm@65346
  1874
wenzelm@65346
  1875
lemma dvd_imp_order_le: "q \<noteq> 0 \<Longrightarrow> p dvd q \<Longrightarrow> Polynomial.order a p \<le> Polynomial.order a q"
haftmann@64795
  1876
  by (auto simp: order_mult elim: dvdE)
haftmann@64795
  1877
wenzelm@65346
  1878
text \<open>Now justify the standard squarefree decomposition, i.e. \<open>f / gcd f f'\<close>.\<close>
haftmann@64795
  1879
haftmann@64795
  1880
lemma order_divides: "[:-a, 1:] ^ n dvd p \<longleftrightarrow> p = 0 \<or> n \<le> order a p"
wenzelm@65346
  1881
  apply (cases "p = 0")
wenzelm@65346
  1882
  apply auto
wenzelm@65346
  1883
   apply (drule order_2 [where a=a and p=p])
wenzelm@65346
  1884
   apply (metis not_less_eq_eq power_le_dvd)
wenzelm@65346
  1885
  apply (erule power_le_dvd [OF order_1])
wenzelm@65346
  1886
  done
haftmann@64795
  1887
haftmann@64795
  1888
lemma order_decomp:
haftmann@64795
  1889
  assumes "p \<noteq> 0"
haftmann@64795
  1890
  shows "\<exists>q. p = [:- a, 1:] ^ order a p * q \<and> \<not> [:- a, 1:] dvd q"
haftmann@64795
  1891
proof -
wenzelm@65346
  1892
  from assms have *: "[:- a, 1:] ^ order a p dvd p"
wenzelm@65346
  1893
    and **: "\<not> [:- a, 1:] ^ Suc (order a p) dvd p"
wenzelm@65346
  1894
    by (auto dest: order)
wenzelm@65346
  1895
  from * obtain q where q: "p = [:- a, 1:] ^ order a p * q" ..
wenzelm@65346
  1896
  with ** have "\<not> [:- a, 1:] ^ Suc (order a p) dvd [:- a, 1:] ^ order a p * q"
haftmann@64795
  1897
    by simp
haftmann@64795
  1898
  then have "\<not> [:- a, 1:] ^ order a p * [:- a, 1:] dvd [:- a, 1:] ^ order a p * q"
haftmann@64795
  1899
    by simp
wenzelm@65346
  1900
  with idom_class.dvd_mult_cancel_left [of "[:- a, 1:] ^ order a p" "[:- a, 1:]" q]
wenzelm@65346
  1901
  have "\<not> [:- a, 1:] dvd q" by auto
wenzelm@65346
  1902
  with q show ?thesis by blast
haftmann@64795
  1903
qed
haftmann@64795
  1904
wenzelm@65346
  1905
lemma monom_1_dvd_iff: "p \<noteq> 0 \<Longrightarrow> monom 1 n dvd p \<longleftrightarrow> n \<le> order 0 p"
wenzelm@65346
  1906
  using order_divides[of 0 n p] by (simp add: monom_altdef)
haftmann@64795
  1907
huffman@29977
  1908
eberlm@62065
  1909
subsection \<open>Additional induction rules on polynomials\<close>
eberlm@62065
  1910
eberlm@62065
  1911
text \<open>
wenzelm@65346
  1912
  An induction rule for induction over the roots of a polynomial with a certain property.
eberlm@62065
  1913
  (e.g. all positive roots)
eberlm@62065
  1914
\<close>
eberlm@62065
  1915
lemma poly_root_induct [case_names 0 no_roots root]:
eberlm@62065
  1916
  fixes p :: "'a :: idom poly"
eberlm@62065
  1917
  assumes "Q 0"
wenzelm@65346
  1918
    and "\<And>p. (\<And>a. P a \<Longrightarrow> poly p a \<noteq> 0) \<Longrightarrow> Q p"
wenzelm@65346
  1919
    and "\<And>a p. P a \<Longrightarrow> Q p \<Longrightarrow> Q ([:a, -1:] * p)"
wenzelm@65346
  1920
  shows "Q p"
eberlm@62065
  1921
proof (induction "degree p" arbitrary: p rule: less_induct)
eberlm@62065
  1922
  case (less p)
eberlm@62065
  1923
  show ?case
eberlm@62065
  1924
  proof (cases "p = 0")
wenzelm@65346
  1925
    case True
wenzelm@65346
  1926
    with assms(1) show ?thesis by simp
wenzelm@65346
  1927
  next
wenzelm@65346
  1928
    case False
wenzelm@65346
  1929
    show ?thesis
eberlm@62065
  1930
    proof (cases "\<exists>a. P a \<and> poly p a = 0")
eberlm@62065
  1931
      case False
wenzelm@65346
  1932
      then show ?thesis by (intro assms(2)) blast
eberlm@62065
  1933
    next
eberlm@62065
  1934
      case True
wenzelm@65346
  1935
      then obtain a where a: "P a" "poly p a = 0"
eberlm@62065
  1936
        by blast
wenzelm@65346
  1937
      then have "-[:-a, 1:] dvd p"
eberlm@62065
  1938
        by (subst minus_dvd_iff) (simp add: poly_eq_0_iff_dvd)
eberlm@62065
  1939
      then obtain q where q: "p = [:a, -1:] * q" by (elim dvdE) simp
wenzelm@65346
  1940
      with False have "q \<noteq> 0" by auto
eberlm@62065
  1941
      have "degree p = Suc (degree q)"
wenzelm@65346
  1942
        by (subst q, subst degree_mult_eq) (simp_all add: \<open>q \<noteq> 0\<close>)
wenzelm@65346
  1943
      then have "Q q" by (intro less) simp
wenzelm@65346
  1944
      with a(1) have "Q ([:a, -1:] * q)"
eberlm@62065
  1945
        by (rule assms(3))
eberlm@62065
  1946
      with q show ?thesis by simp
eberlm@62065
  1947
    qed
wenzelm@65346
  1948
  qed
eberlm@62065
  1949
qed
eberlm@62065
  1950
wenzelm@65346
  1951
lemma dropWhile_replicate_append:
wenzelm@65346
  1952
  "dropWhile (op = a) (replicate n a @ ys) = dropWhile (op = a) ys"
wenzelm@65346
  1953
  by (induct n) simp_all
eberlm@62065
  1954
eberlm@62065
  1955
lemma Poly_append_replicate_0: "Poly (xs @ replicate n 0) = Poly xs"
eberlm@62065
  1956
  by (subst coeffs_eq_iff) (simp_all add: strip_while_def dropWhile_replicate_append)
eberlm@62065
  1957
eberlm@62065
  1958
text \<open>
wenzelm@65346
  1959
  An induction rule for simultaneous induction over two polynomials,
eberlm@62065
  1960
  prepending one coefficient in each step.
eberlm@62065
  1961
\<close>
eberlm@62065
  1962
lemma poly_induct2 [case_names 0 pCons]:
eberlm@62065
  1963
  assumes "P 0 0" "\<And>a p b q. P p q \<Longrightarrow> P (pCons a p) (pCons b q)"
wenzelm@65346
  1964
  shows "P p q"
eberlm@62065
  1965
proof -
wenzelm@63040
  1966
  define n where "n = max (length (coeffs p)) (length (coeffs q))"
wenzelm@63040
  1967
  define xs where "xs = coeffs p @ (replicate (n - length (coeffs p)) 0)"
wenzelm@63040
  1968
  define ys where "ys = coeffs q @ (replicate (n - length (coeffs q)) 0)"
wenzelm@65346
  1969
  have "length xs = length ys"
eberlm@62065
  1970
    by (simp add: xs_def ys_def n_def)
wenzelm@65346
  1971
  then have "P (Poly xs) (Poly ys)"
wenzelm@65346
  1972
    by (induct rule: list_induct2) (simp_all add: assms)
wenzelm@65346
  1973
  also have "Poly xs = p"
eberlm@62065
  1974
    by (simp add: xs_def Poly_append_replicate_0)
wenzelm@65346
  1975
  also have "Poly ys = q"
eberlm@62065
  1976
    by (simp add: ys_def Poly_append_replicate_0)
eberlm@62065
  1977
  finally show ?thesis .
eberlm@62065
  1978
qed
eberlm@62065
  1979
wenzelm@65346
  1980
wenzelm@60500
  1981
subsection \<open>Composition of polynomials\<close>
huffman@29478
  1982
eberlm@62128
  1983
(* Several lemmas contributed by René Thiemann and Akihisa Yamada *)
eberlm@62128
  1984
haftmann@52380
  1985
definition pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
wenzelm@65346
  1986
  where "pcompose p q = fold_coeffs (\<lambda>a c. [:a:] + q * c) p 0"
haftmann@52380
  1987
eberlm@62128
  1988
notation pcompose (infixl "\<circ>\<^sub>p" 71)
eberlm@62128
  1989
wenzelm@65346
  1990
lemma pcompose_0 [simp]: "pcompose 0 q = 0"
haftmann@52380
  1991
  by (simp add: pcompose_def)
wenzelm@65346
  1992
wenzelm@65346
  1993
lemma pcompose_pCons: "pcompose (pCons a p) q = [:a:] + q * pcompose p q"
haftmann@52380
  1994
  by (cases "p = 0 \<and> a = 0") (auto simp add: pcompose_def)
haftmann@52380
  1995
wenzelm@65346
  1996
lemma pcompose_1: "pcompose 1 p = 1"
wenzelm@65346
  1997
  for p :: "'a::comm_semiring_1 poly"
haftmann@65486
  1998
  by (auto simp: one_pCons pcompose_pCons)
wenzelm@65346
  1999
wenzelm@65346
  2000
lemma poly_pcompose: "poly (pcompose p q) x = poly p (poly q x)"
haftmann@52380
  2001
  by (induct p) (simp_all add: pcompose_pCons)
haftmann@52380
  2002
wenzelm@65346
  2003
lemma degree_pcompose_le: "degree (pcompose p q) \<le> degree p * degree q"
wenzelm@65346
  2004
  apply (induct p)
wenzelm@65346
  2005
   apply simp
wenzelm@65346
  2006
  apply (simp add: pcompose_pCons)
wenzelm@65346
  2007
  apply clarify
wenzelm@65346
  2008
  apply (rule degree_add_le)
wenzelm@65346
  2009
   apply simp
wenzelm@65346
  2010
  apply (rule order_trans [OF degree_mult_le])
wenzelm@65346
  2011
  apply simp
wenzelm@65346
  2012
  done
wenzelm@65346
  2013
wenzelm@65346
  2014
lemma pcompose_add: "pcompose (p + q) r = pcompose p r + pcompose q r"
wenzelm@65346
  2015
  for p q r :: "'a::{comm_semiring_0, ab_semigroup_add} poly"
eberlm@62065
  2016
proof (induction p q rule: poly_induct2)
wenzelm@65346
  2017
  case 0
wenzelm@65346
  2018
  then show ?case by simp
wenzelm@65346
  2019
next
eberlm@62065
  2020
  case (pCons a p b q)
wenzelm@65346
  2021
  have "pcompose (pCons a p + pCons b q) r = [:a + b:] + r * pcompose p r + r * pcompose q r"
eberlm@62065
  2022
    by (simp_all add: pcompose_pCons pCons.IH algebra_simps)
eberlm@62065
  2023
  also have "[:a + b:] = [:a:] + [:b:]" by simp
wenzelm@65346
  2024
  also have "\<dots> + r * pcompose p r + r * pcompose q r =
wenzelm@65346
  2025
    pcompose (pCons a p) r + pcompose (pCons b q) r"
eberlm@62065
  2026
    by (simp only: pcompose_pCons add_ac)
eberlm@62065
  2027
  finally show ?case .
wenzelm@65346
  2028
qed
wenzelm@65346
  2029
wenzelm@65346
  2030
lemma pcompose_uminus: "pcompose (-p) r = -pcompose p r"
wenzelm@65346
  2031
  for p r :: "'a::comm_ring poly"
wenzelm@65346
  2032
  by (induct p) (simp_all add: pcompose_pCons)
wenzelm@65346
  2033
wenzelm@65346
  2034
lemma pcompose_diff: "pcompose (p - q) r = pcompose p r - pcompose q r"
wenzelm@65346
  2035
  for p q r :: "'a::comm_ring poly"
eberlm@62128
  2036
  using pcompose_add[of p "-q"] by (simp add: pcompose_uminus)
eberlm@62065
  2037
wenzelm@65346
  2038
lemma pcompose_smult: "pcompose (smult a p) r = smult a (pcompose p r)"
wenzelm@65346
  2039
  for p r :: "'a::comm_semiring_0 poly"
wenzelm@65346
  2040
  by (induct p) (simp_all add: pcompose_pCons pcompose_add smult_add_right)
wenzelm@65346
  2041
wenzelm@65346
  2042
lemma pcompose_mult: "pcompose (p * q) r = pcompose p r * pcompose q r"
wenzelm@65346
  2043
  for p q r :: "'a::comm_semiring_0 poly"
wenzelm@65346
  2044
  by (induct p arbitrary: q) (simp_all add: pcompose_add pcompose_smult pcompose_pCons algebra_simps)
wenzelm@65346
  2045
wenzelm@65346
  2046
lemma pcompose_assoc: "pcompose p (pcompose q r) = pcompose (pcompose p q) r"
wenzelm@65346
  2047
  for p q r :: "'a::comm_semiring_0 poly"
wenzelm@65346
  2048
  by (induct p arbitrary: q) (simp_all add: pcompose_pCons pcompose_add pcompose_mult)
wenzelm@65346
  2049
wenzelm@65346
  2050
lemma pcompose_idR[simp]: "pcompose p [: 0, 1 :] = p"
wenzelm@65346
  2051
  for p :: "'a::comm_semiring_1 poly"
wenzelm@65346
  2052
  by (induct p) (simp_all add: pcompose_pCons)
eberlm@62128
  2053
nipkow@64267
  2054
lemma pcompose_sum: "pcompose (sum f A) p = sum (\<lambda>i. pcompose (f i) p) A"
wenzelm@65346
  2055
  by (induct A rule: infinite_finite_induct) (simp_all add: pcompose_1 pcompose_add)
eberlm@63317
  2056
nipkow@64272
  2057
lemma pcompose_prod: "pcompose (prod f A) p = prod (\<lambda>i. pcompose (f i) p) A"
wenzelm@65346
  2058
  by (induct A rule: infinite_finite_induct) (simp_all add: pcompose_1 pcompose_mult)
eberlm@63317
  2059
haftmann@64591
  2060
lemma pcompose_const [simp]: "pcompose [:a:] q = [:a:]"
haftmann@64591
  2061
  by (subst pcompose_pCons) simp
eberlm@62065
  2062
eberlm@62128
  2063
lemma pcompose_0': "pcompose p 0 = [:coeff p 0:]"
haftmann@64591
  2064
  by (induct p) (auto simp add: pcompose_pCons)
eberlm@62065
  2065
wenzelm@65346
  2066
lemma degree_pcompose: "degree (pcompose p q) = degree p * degree q"
wenzelm@65346
  2067
  for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
eberlm@62065
  2068
proof (induct p)
eberlm@62065
  2069
  case 0
wenzelm@65346
  2070
  then show ?case by auto
eberlm@62065
  2071
next
eberlm@62065
  2072
  case (pCons a p)
wenzelm@65346
  2073
  consider "degree (q * pcompose p q) = 0" | "degree (q * pcompose p q) > 0"
wenzelm@65346
  2074
    by blast
wenzelm@65346
  2075
  then show ?case
wenzelm@65346
  2076
  proof cases
wenzelm@65346
  2077
    case prems: 1
wenzelm@65346
  2078
    show ?thesis
wenzelm@65346
  2079
    proof (cases "p = 0")
eberlm@62065
  2080
      case True
wenzelm@65346
  2081
      then show ?thesis by auto
eberlm@62065
  2082
    next
wenzelm@65346
  2083
      case False
wenzelm@65346
  2084
      from prems have "degree q = 0 \<or> pcompose p q = 0"
wenzelm@65346
  2085
        by (auto simp add: degree_mult_eq_0)
wenzelm@65346
  2086
      moreover have False if "pcompose p q = 0" "degree q \<noteq> 0"
wenzelm@65346
  2087
      proof -
wenzelm@65346
  2088
        from pCons.hyps(2) that have "degree p = 0"
wenzelm@65346
  2089
          by auto
wenzelm@65346
  2090
        then obtain a1 where "p = [:a1:]"
wenzelm@65346
  2091
          by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases)
wenzelm@65346
  2092
        with \<open>pcompose p q = 0\<close> \<open>p \<noteq> 0\<close> show False
wenzelm@65346
  2093
          by auto
wenzelm@65346
  2094
      qed
wenzelm@65346
  2095
      ultimately have "degree (pCons a p) * degree q = 0"
wenzelm@65346
  2096
        by auto
wenzelm@65346
  2097
      moreover have "degree (pcompose (pCons a p) q) = 0"
wenzelm@65346
  2098
      proof -
wenzelm@65346
  2099
        from prems have "0 = max (degree [:a:]) (degree (q * pcompose p q))"
wenzelm@65346
  2100
          by simp
wenzelm@65346
  2101
        also have "\<dots> \<ge> degree ([:a:] + q * pcompose p q)"
wenzelm@65346
  2102
          by (rule degree_add_le_max)
wenzelm@65346
  2103
        finally show ?thesis
wenzelm@65346
  2104
          by (auto simp add: pcompose_pCons)
wenzelm@65346
  2105
      qed
eberlm@62065
  2106
      ultimately show ?thesis by simp
eberlm@62065
  2107
    qed
wenzelm@65346
  2108
  next
wenzelm@65346
  2109
    case prems: 2
wenzelm@65346
  2110
    then have "p \<noteq> 0" "q \<noteq> 0" "pcompose p q \<noteq> 0"
wenzelm@65346
  2111
      by auto
wenzelm@65346
  2112
    from prems degree_add_eq_right [of "[:a:]"]
wenzelm@65346
  2113
    have "degree (pcompose (pCons a p) q) = degree (q * pcompose p q)"
wenzelm@65346
  2114
      by (auto simp: pcompose_pCons)
wenzelm@65346
  2115
    with pCons.hyps(2) degree_mult_eq[OF \<open>q\<noteq>0\<close> \<open>pcompose p q\<noteq>0\<close>] show ?thesis
wenzelm@65346
  2116
      by auto
wenzelm@65346
  2117
  qed
eberlm@62065
  2118
qed
eberlm@62065
  2119
eberlm@62065
  2120
lemma pcompose_eq_0:
wenzelm@65346
  2121
  fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
wenzelm@65346
  2122
  assumes "pcompose p q = 0" "degree q > 0"
eberlm@62128
  2123
  shows "p = 0"
eberlm@62065
  2124
proof -
wenzelm@65346
  2125
  from assms degree_pcompose [of p q] have "degree p = 0"
wenzelm@65346
  2126
    by auto
wenzelm@65346
  2127
  then obtain a where "p = [:a:]"
eberlm@62065
  2128
    by (metis degree_pCons_eq_if gr0_conv_Suc neq0_conv pCons_cases)
wenzelm@65346
  2129
  with assms(1) have "a = 0"
wenzelm@65346
  2130
    by auto
wenzelm@65346
  2131
  with \<open>p = [:a:]\<close> show ?thesis
wenzelm@65346
  2132
    by simp
eberlm@62065
  2133
qed
eberlm@62065
  2134
eberlm@62065
  2135
lemma lead_coeff_comp:
wenzelm@65346
  2136
  fixes p q :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
wenzelm@65346
  2137
  assumes "degree q > 0"
eberlm@62065
  2138
  shows "lead_coeff (pcompose p q) = lead_coeff p * lead_coeff q ^ (degree p)"
eberlm@62065
  2139
proof (induct p)
eberlm@62065
  2140
  case 0
wenzelm@65346
  2141
  then show ?case by auto
eberlm@62065
  2142
next
eberlm@62065
  2143
  case (pCons a p)
wenzelm@65346
  2144
  consider "degree (q * pcompose p q) = 0" | "degree (q * pcompose p q) > 0"
wenzelm@65346
  2145
    by blast
wenzelm@65346
  2146
  then show ?case
wenzelm@65346
  2147
  proof cases
wenzelm@65346
  2148
    case prems: 1
wenzelm@65346
  2149
    then have "pcompose p q = 0"
wenzelm@65346
  2150
      by (metis assms degree_0 degree_mult_eq_0 neq0_conv)
wenzelm@65346
  2151
    with pcompose_eq_0[OF _ \<open>degree q > 0\<close>] have "p = 0"
wenzelm@65346
  2152
      by simp
wenzelm@65346
  2153
    then show ?thesis
wenzelm@65346
  2154
      by auto
wenzelm@65346
  2155
  next
wenzelm@65346
  2156
    case prems: 2
wenzelm@65346
  2157
    then have "degree [:a:] < degree (q * pcompose p q)"
wenzelm@65346
  2158
      by simp
wenzelm@65346
  2159
    then have "lead_coeff ([:a:] + q * p \<circ>\<^sub>p q) = lead_coeff (q * p \<circ>\<^sub>p q)"
wenzelm@65346
  2160
      by (rule lead_coeff_add_le)
wenzelm@65346
  2161
    then have "lead_coeff (pcompose (pCons a p) q) = lead_coeff (q * pcompose p q)"
wenzelm@65346
  2162
      by (simp add: pcompose_pCons)
wenzelm@65346
  2163
    also have "\<dots> = lead_coeff q * (lead_coeff p * lead_coeff q ^ degree p)"
wenzelm@65346
  2164
      using pCons.hyps(2) lead_coeff_mult[of q "pcompose p q"] by simp
wenzelm@65346
  2165
    also have "\<dots> = lead_coeff p * lead_coeff q ^ (degree p + 1)"
wenzelm@65346
  2166
      by (auto simp: mult_ac)
wenzelm@65346
  2167
    finally show ?thesis by auto
wenzelm@65346
  2168
  qed
eberlm@62065
  2169
qed
eberlm@62065
  2170
haftmann@62352
  2171
eberlm@63317
  2172
subsection \<open>Shifting polynomials\<close>
eberlm@63317
  2173
wenzelm@65346
  2174
definition poly_shift :: "nat \<Rightarrow> 'a::zero poly \<Rightarrow> 'a poly"
wenzelm@65346
  2175
  where "poly_shift n p = Abs_poly (\<lambda>i. coeff p (i + n))"
eberlm@63317
  2176
eberlm@63317
  2177
lemma nth_default_drop: "nth_default x (drop n xs) m = nth_default x xs (m + n)"
eberlm@63317
  2178
  by (auto simp add: nth_default_def add_ac)
wenzelm@65346
  2179
eberlm@63317
  2180
lemma nth_default_take: "nth_default x (take n xs) m = (if m < n then nth_default x xs m else x)"
eberlm@63317
  2181
  by (auto simp add: nth_default_def add_ac)
wenzelm@65346
  2182
eberlm@63317
  2183
lemma coeff_poly_shift: "coeff (poly_shift n p) i = coeff p (i + n)"
eberlm@63317
  2184
proof -
wenzelm@65346
  2185
  from MOST_coeff_eq_0[of p] obtain m where "\<forall>k>m. coeff p k = 0"
wenzelm@65346
  2186
    by (auto simp: MOST_nat)
wenzelm@65346
  2187
  then have "\<forall>k>m. coeff p (k + n) = 0"
wenzelm@65346
  2188
    by auto
wenzelm@65346
  2189
  then have "\<forall>\<^sub>\<infinity>k. coeff p (k + n) = 0"
wenzelm@65346
  2190
    by (auto simp: MOST_nat)
wenzelm@65346
  2191
  then show ?thesis
wenzelm@65346
  2192
    by (simp add: poly_shift_def poly.Abs_poly_inverse)
eberlm@63317
  2193
qed
eberlm@63317
  2194
eberlm@63317
  2195
lemma poly_shift_id [simp]: "poly_shift 0 = (\<lambda>x. x)"
eberlm@63317
  2196
  by (simp add: poly_eq_iff fun_eq_iff coeff_poly_shift)
eberlm@63317
  2197
eberlm@63317
  2198
lemma poly_shift_0 [simp]: "poly_shift n 0 = 0"
eberlm@63317
  2199
  by (simp add: poly_eq_iff coeff_poly_shift)
wenzelm@65346
  2200
eberlm@63317
  2201
lemma poly_shift_1: "poly_shift n 1 = (if n = 0 then 1 else 0)"
eberlm@63317
  2202
  by (simp add: poly_eq_iff coeff_poly_shift)
eberlm@63317
  2203
eberlm@63317
  2204
lemma poly_shift_monom: "poly_shift n (monom c m) = (if m \<ge> n then monom c (m - n) else 0)"
eberlm@63317
  2205
  by (auto simp add: poly_eq_iff coeff_poly_shift)
eberlm@63317
  2206
haftmann@65390
  2207
lemma coeffs_shift_poly [code abstract]:
haftmann@65390
  2208
  "coeffs (poly_shift n p) = drop n (coeffs p)"
eberlm@63317
  2209
proof (cases "p = 0")
wenzelm@65346
  2210
  case True
wenzelm@65346
  2211
  then show ?thesis by simp
wenzelm@65346
  2212
next
eberlm@63317
  2213
  case False
wenzelm@65346
  2214
  then show ?thesis
eberlm@63317
  2215
    by (intro coeffs_eqI)
haftmann@65390
  2216
      (simp_all add: coeff_poly_shift nth_default_drop nth_default_coeffs_eq)
wenzelm@65346
  2217
qed
eberlm@63317
  2218
eberlm@63317
  2219
eberlm@63317
  2220
subsection \<open>Truncating polynomials\<close>
eberlm@63317
  2221
wenzelm@65346
  2222
definition poly_cutoff
wenzelm@65346
  2223
  where "poly_cutoff n p = Abs_poly (\<lambda>k. if k < n then coeff p k else 0)"
eberlm@63317
  2224
eberlm@63317
  2225
lemma coeff_poly_cutoff: "coeff (poly_cutoff n p) k = (if k < n then coeff p k else 0)"
eberlm@63317
  2226
  unfolding poly_cutoff_def
eberlm@63317
  2227
  by (subst poly.Abs_poly_inverse) (auto simp: MOST_nat intro: exI[of _ n])
eberlm@63317
  2228
eberlm@63317
  2229
lemma poly_cutoff_0 [simp]: "poly_cutoff n 0 = 0"
eberlm@63317
  2230
  by (simp add: poly_eq_iff coeff_poly_cutoff)
eberlm@63317
  2231
eberlm@63317
  2232
lemma poly_cutoff_1 [simp]: "poly_cutoff n 1 = (if n = 0 then 0 else 1)"
eberlm@63317
  2233
  by (simp add: poly_eq_iff coeff_poly_cutoff)
eberlm@63317
  2234
wenzelm@65346
  2235
lemma coeffs_poly_cutoff [code abstract]:
eberlm@63317
  2236
  "coeffs (poly_cutoff n p) = strip_while (op = 0) (take n (coeffs p))"
eberlm@63317
  2237
proof (cases "strip_while (op = 0) (take n (coeffs p)) = []")
eberlm@63317
  2238
  case True
wenzelm@65346
  2239
  then have "coeff (poly_cutoff n p) k = 0" for k
eberlm@63317
  2240
    unfolding coeff_poly_cutoff
eberlm@63317
  2241
    by (auto simp: nth_default_coeffs_eq [symmetric] nth_default_def set_conv_nth)
wenzelm@65346
  2242
  then have "poly_cutoff n p = 0"
wenzelm@65346
  2243
    by (simp add: poly_eq_iff)
wenzelm@65346
  2244
  then show ?thesis
wenzelm@65346
  2245
    by (subst True) simp_all
eberlm@63317
  2246
next
eberlm@63317
  2247
  case False
wenzelm@65346
  2248
  have "no_trailing (op = 0) (strip_while (op = 0) (take n (coeffs p)))"
wenzelm@65346
  2249
    by simp
wenzelm@65346
  2250
  with False have "last (strip_while (op = 0) (take n (coeffs p))) \<noteq> 0"
eberlm@63317
  2251
    unfolding no_trailing_unfold by auto
wenzelm@65346
  2252
  then show ?thesis
eberlm@63317
  2253
    by (intro coeffs_eqI)
haftmann@65390
  2254
      (simp_all add: coeff_poly_cutoff nth_default_take nth_default_coeffs_eq)
eberlm@63317
  2255
qed
eberlm@63317
  2256
eberlm@63317
  2257
eberlm@63317
  2258
subsection \<open>Reflecting polynomials\<close>
eberlm@63317
  2259
wenzelm@65346
  2260
definition reflect_poly :: "'a::zero poly \<Rightarrow> 'a poly"
wenzelm@65346
  2261
  where "reflect_poly p = Poly (rev (coeffs p))"
wenzelm@65346
  2262
eberlm@63317
  2263
lemma coeffs_reflect_poly [code abstract]:
wenzelm@65346
  2264
  "coeffs (reflect_poly p) = rev (dropWhile (op = 0) (coeffs p))"
wenzelm@65346
  2265
  by (simp add: reflect_poly_def)
wenzelm@65346
  2266
eberlm@63317
  2267
lemma reflect_poly_0 [simp]: "reflect_poly 0 = 0"
eberlm@63317
  2268
  by (simp add: reflect_poly_def)
eberlm@63317
  2269
eberlm@63317
  2270
lemma reflect_poly_1 [simp]: "reflect_poly 1 = 1"
haftmann@65486
  2271
  by (simp add: reflect_poly_def one_pCons)
eberlm@63317
  2272
eberlm@63317
  2273
lemma coeff_reflect_poly:
eberlm@63317
  2274
  "coeff (reflect_poly p) n = (if n > degree p then 0 else coeff p (degree p - n))"
wenzelm@65346
  2275
  by (cases "p = 0")
wenzelm@65346
  2276
    (auto simp add: reflect_poly_def nth_default_def
wenzelm@65346
  2277
      rev_nth degree_eq_length_coeffs coeffs_nth not_less
wenzelm@65346
  2278
      dest: le_imp_less_Suc)
eberlm@63317
  2279
eberlm@63317
  2280
lemma coeff_0_reflect_poly_0_iff [simp]: "coeff (reflect_poly p) 0 = 0 \<longleftrightarrow> p = 0"
eberlm@63317
  2281
  by (simp add: coeff_reflect_poly)
eberlm@63317
  2282
eberlm@63317
  2283
lemma reflect_poly_at_0_eq_0_iff [simp]: "poly (reflect_poly p) 0 = 0 \<longleftrightarrow> p = 0"
eberlm@63317
  2284
  by (simp add: coeff_reflect_poly poly_0_coeff_0)
eberlm@63317
  2285
eberlm@63317
  2286
lemma reflect_poly_pCons':
eberlm@63317
  2287
  "p \<noteq> 0 \<Longrightarrow> reflect_poly (pCons c p) = reflect_poly p + monom c (Suc (degree p))"
eberlm@63317
  2288
  by (intro poly_eqI)
wenzelm@65346
  2289
    (auto simp: coeff_reflect_poly coeff_pCons not_less Suc_diff_le split: nat.split)
eberlm@63317
  2290
eberlm@63317
  2291
lemma reflect_poly_const [simp]: "reflect_poly [:a:] = [:a:]"
eberlm@63317
  2292
  by (cases "a = 0") (simp_all add: reflect_poly_def)
eberlm@63317
  2293
eberlm@63317
  2294
lemma poly_reflect_poly_nz:
wenzelm@65346
  2295
  "x \<noteq> 0 \<Longrightarrow> poly (reflect_poly p) x = x ^ degree p * poly p (inverse x)"
wenzelm@65346
  2296
  for x :: "'a::field"
wenzelm@65346
  2297
  by (induct rule: pCons_induct) (simp_all add: field_simps reflect_poly_pCons' poly_monom)
eberlm@63317
  2298
eberlm@63317
  2299
lemma coeff_0_reflect_poly [simp]: "coeff (reflect_poly p) 0 = lead_coeff p"
haftmann@64794
  2300
  by (simp add: coeff_reflect_poly)
eberlm@63317
  2301
eberlm@63317
  2302
lemma poly_reflect_poly_0 [simp]: "poly (reflect_poly p) 0 = lead_coeff p"
eberlm@63317
  2303
  by (simp add: poly_0_coeff_0)
eberlm@63317
  2304
eberlm@63317
  2305
lemma reflect_poly_reflect_poly [simp]: "coeff p 0 \<noteq> 0 \<Longrightarrow> reflect_poly (reflect_poly p) = p"
eberlm@63317
  2306
  by (cases p rule: pCons_cases) (simp add: reflect_poly_def )
eberlm@63317
  2307
eberlm@63317
  2308
lemma degree_reflect_poly_le: "degree (reflect_poly p) \<le> degree p"
eberlm@63317
  2309
  by (simp add: degree_eq_length_coeffs coeffs_reflect_poly length_dropWhile_le diff_le_mono)
eberlm@63317
  2310
wenzelm@65346
  2311
lemma reflect_poly_pCons: "a \<noteq> 0 \<Longrightarrow> reflect_poly (pCons a p) = Poly (rev (a # coeffs p))"
eberlm@63317
  2312
  by (subst coeffs_eq_iff) (simp add: coeffs_reflect_poly)
wenzelm@65346
  2313
eberlm@63317
  2314
lemma degree_reflect_poly_eq [simp]: "coeff p 0 \<noteq> 0 \<Longrightarrow> degree (reflect_poly p) = degree p"
eberlm@63317
  2315
  by (cases p rule: pCons_cases) (simp add: reflect_poly_pCons degree_eq_length_coeffs)
wenzelm@65346
  2316
eberlm@63498
  2317
(* TODO: does this work with zero divisors as well? Probably not. *)
wenzelm@65346
  2318
lemma reflect_poly_mult: "reflect_poly (p * q) = reflect_poly p * reflect_poly q"
wenzelm@65346
  2319
  for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
eberlm@63317
  2320
proof (cases "p = 0 \<or> q = 0")
eberlm@63317
  2321
  case False
wenzelm@65346
  2322
  then have [simp]: "p \<noteq> 0" "q \<noteq> 0" by auto
eberlm@63317
  2323
  show ?thesis
eberlm@63317
  2324
  proof (rule poly_eqI)
wenzelm@65346
  2325
    show "coeff (reflect_poly (p * q)) i = coeff (reflect_poly p * reflect_poly q) i" for i
eberlm@63317
  2326
    proof (cases "i \<le> degree (p * q)")
eberlm@63317
  2327
      case True
haftmann@64811
  2328
      define A where "A = {..i} \<inter> {i - degree q..degree p}"
haftmann@64811
  2329
      define B where "B = {..degree p} \<inter> {degree p - i..degree (p*q) - i}"
eberlm@63317
  2330
      let ?f = "\<lambda>j. degree p - j"
eberlm@63317
  2331
eberlm@63317
  2332
      from True have "coeff (reflect_poly (p * q)) i = coeff (p * q) (degree (p * q) - i)"
eberlm@63317
  2333
        by (simp add: coeff_reflect_poly)
eberlm@63317
  2334
      also have "\<dots> = (\<Sum>j\<le>degree (p * q) - i. coeff p j * coeff q (degree (p * q) - i - j))"
wenzelm@65346
  2335
        by (simp add: coeff_mult)
eberlm@63317
  2336
      also have "\<dots> = (\<Sum>j\<in>B. coeff p j * coeff q (degree (p * q) - i - j))"
nipkow@64267
  2337
        by (intro sum.mono_neutral_right) (auto simp: B_def degree_mult_eq not_le coeff_eq_0)
eberlm@63317
  2338
      also from True have "\<dots> = (\<Sum>j\<in>A. coeff p (degree p - j) * coeff q (degree q - (i - j)))"
nipkow@64267
  2339
        by (intro sum.reindex_bij_witness[of _ ?f ?f])
wenzelm@65346
  2340
          (auto simp: A_def B_def degree_mult_eq add_ac)
wenzelm@65346
  2341
      also have "\<dots> =
wenzelm@65346
  2342
        (\<Sum>j\<le>i.
wenzelm@65346
  2343
          if j \<in> {i - degree q..degree p}
wenzelm@65346
  2344
          then coeff p (degree p - j) * coeff q (degree q - (i - j))
wenzelm@65346
  2345
          else 0)"
nipkow@64267
  2346
        by (subst sum.inter_restrict [symmetric]) (simp_all add: A_def)
wenzelm@65346
  2347
      also have "\<dots> = coeff (reflect_poly p * reflect_poly q) i"
wenzelm@65346
  2348
        by (fastforce simp: coeff_mult coeff_reflect_poly intro!: sum.cong)
wenzelm@65346
  2349
      finally show ?thesis .
nipkow@64267
  2350
    qed (auto simp: coeff_mult coeff_reflect_poly coeff_eq_0 degree_mult_eq intro!: sum.neutral)
eberlm@63317
  2351
  qed
eberlm@63317
  2352
qed auto
eberlm@63317
  2353
wenzelm@65346
  2354
lemma reflect_poly_smult: "reflect_poly (smult c p) = smult c (reflect_poly p)"
wenzelm@65346
  2355
  for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
eberlm@63317
  2356
  using reflect_poly_mult[of "[:c:]" p] by simp
eberlm@63317
  2357
wenzelm@65346
  2358
lemma reflect_poly_power: "reflect_poly (p ^ n) = reflect_poly p ^ n"
wenzelm@65346
  2359
  for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
wenzelm@65346
  2360
  by (induct n) (simp_all add: reflect_poly_mult)
wenzelm@65346
  2361
wenzelm@65346
  2362
lemma reflect_poly_prod: "reflect_poly (prod f A) = prod (\<lambda>x. reflect_poly (f x)) A"
wenzelm@65346
  2363
  for f :: "_ \<Rightarrow> _::{comm_semiring_0,semiring_no_zero_divisors} poly"
wenzelm@65346
  2364
  by (induct A rule: infinite_finite_induct) (simp_all add: reflect_poly_mult)
wenzelm@65346
  2365
wenzelm@65346
  2366
lemma reflect_poly_prod_list: "reflect_poly (prod_list xs) = prod_list (map reflect_poly xs)"
wenzelm@65346
  2367
  for xs :: "_::{comm_semiring_0,semiring_no_zero_divisors} poly list"
wenzelm@65346
  2368
  by (induct xs) (simp_all add: reflect_poly_mult)
wenzelm@65346
  2369
haftmann@65390
  2370
lemma reflect_poly_Poly_nz:
haftmann@65390
  2371
  "no_trailing (HOL.eq 0) xs \<Longrightarrow> reflect_poly (Poly xs) = Poly (rev xs)"
wenzelm@65346
  2372
  by (simp add: reflect_poly_def)
wenzelm@65346
  2373
wenzelm@65346
  2374
lemmas reflect_poly_simps =
eberlm@63317
  2375
  reflect_poly_0 reflect_poly_1 reflect_poly_const reflect_poly_smult reflect_poly_mult
nipkow@64272
  2376
  reflect_poly_power reflect_poly_prod reflect_poly_prod_list
eberlm@63317
  2377
eberlm@63317
  2378
haftmann@64795
  2379
subsection \<open>Derivatives\<close>
haftmann@62352
  2380
eberlm@63498
  2381
function pderiv :: "('a :: {comm_semiring_1,semiring_no_zero_divisors}) poly \<Rightarrow> 'a poly"
wenzelm@65346
  2382
  where "pderiv (pCons a p) = (if p = 0 then 0 else p + pCons 0 (pderiv p))"
haftmann@62352
  2383
  by (auto intro: pCons_cases)
haftmann@62352
  2384
haftmann@62352
  2385
termination pderiv
haftmann@62352
  2386
  by (relation "measure degree") simp_all
haftmann@62352
  2387
rene@63027
  2388
declare pderiv.simps[simp del]
rene@63027
  2389
wenzelm@65346
  2390
lemma pderiv_0 [simp]: "pderiv 0 = 0"
haftmann@62352
  2391
  using pderiv.simps [of 0 0] by simp
haftmann@62352
  2392
wenzelm@65346
  2393
lemma pderiv_pCons: "pderiv (pCons a p) = p + pCons 0 (pderiv p)"
haftmann@62352
  2394
  by (simp add: pderiv.simps)
haftmann@62352
  2395
wenzelm@65346
  2396
lemma pderiv_1 [simp]: "pderiv 1 = 0"
haftmann@65486
  2397
  by (simp add: one_pCons pderiv_pCons)
wenzelm@65346
  2398
wenzelm@65346
  2399
lemma pderiv_of_nat [simp]: "pderiv (of_nat n) = 0"
haftmann@62352
  2400
  and pderiv_numeral [simp]: "pderiv (numeral m) = 0"
haftmann@62352
  2401
  by (simp_all add: of_nat_poly numeral_poly pderiv_pCons)
haftmann@62352
  2402
haftmann@62352
  2403
lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)"
wenzelm@65346
  2404
  by (induct p arbitrary: n)
wenzelm@65346
  2405
    (auto simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
wenzelm@65346
  2406
wenzelm@65346
  2407
fun pderiv_coeffs_code :: "'a::{comm_semiring_1,semiring_no_zero_divisors} \<Rightarrow> 'a list \<Rightarrow> 'a list"
wenzelm@65346
  2408
  where
wenzelm@65346
  2409
    "pderiv_coeffs_code f (x # xs) = cCons (f * x) (pderiv_coeffs_code (f+1) xs)"
wenzelm@65346
  2410
  | "pderiv_coeffs_code f [] = []"
wenzelm@65346
  2411
wenzelm@65346
  2412
definition pderiv_coeffs :: "'a::{comm_semiring_1,semiring_no_zero_divisors} list \<Rightarrow> 'a list"
wenzelm@65346
  2413
  where "pderiv_coeffs xs = pderiv_coeffs_code 1 (tl xs)"
haftmann@62352
  2414
haftmann@62352
  2415
(* Efficient code for pderiv contributed by René Thiemann and Akihisa Yamada *)
wenzelm@65346
  2416
lemma pderiv_coeffs_code:
wenzelm@65346
  2417
  "nth_default 0 (pderiv_coeffs_code f xs) n = (f + of_nat n) * nth_default 0 xs n"
haftmann@62352
  2418
proof (induct xs arbitrary: f n)
wenzelm@65346
  2419
  case Nil
wenzelm@65346
  2420
  then show ?case by simp
wenzelm@65346
  2421
next
wenzelm@65346
  2422
  case (Cons x xs)
wenzelm@65346
  2423
  show ?case
haftmann@62352
  2424
  proof (cases n)
haftmann@62352
  2425
    case 0