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