src/HOL/Library/Polynomial_FPS.thy
author eberlm
Fri Jun 17 11:33:52 2016 +0200 (2016-06-17)
changeset 63319 bc8793d7bd21
parent 63317 ca187a9f66da
child 63539 70d4d9e5707b
permissions -rw-r--r--
fps_from_poly → fps_of_poly
eberlm@63317
     1
(*
eberlm@63317
     2
  File:      Polynomial_FPS.thy
eberlm@63317
     3
  Author:    Manuel Eberl (TUM)
eberlm@63317
     4
  
eberlm@63317
     5
  Converting polynomials to formal power series
eberlm@63317
     6
*)
eberlm@63317
     7
eberlm@63317
     8
section \<open>Converting polynomials to formal power series\<close>
eberlm@63317
     9
theory Polynomial_FPS
eberlm@63317
    10
imports Polynomial Formal_Power_Series
eberlm@63317
    11
begin
eberlm@63317
    12
eberlm@63319
    13
definition fps_of_poly where
eberlm@63319
    14
  "fps_of_poly p = Abs_fps (coeff p)"
eberlm@63317
    15
eberlm@63319
    16
lemma fps_of_poly_eq_iff: "fps_of_poly p = fps_of_poly q \<longleftrightarrow> p = q"
eberlm@63319
    17
  by (simp add: fps_of_poly_def poly_eq_iff fps_eq_iff)
eberlm@63317
    18
eberlm@63319
    19
lemma fps_of_poly_nth [simp]: "fps_of_poly p $ n = coeff p n"
eberlm@63319
    20
  by (simp add: fps_of_poly_def)
eberlm@63317
    21
  
eberlm@63319
    22
lemma fps_of_poly_const: "fps_of_poly [:c:] = fps_const c"
eberlm@63317
    23
proof (subst fps_eq_iff, clarify)
eberlm@63319
    24
  fix n :: nat show "fps_of_poly [:c:] $ n = fps_const c $ n"
eberlm@63319
    25
    by (cases n) (auto simp: fps_of_poly_def)
eberlm@63317
    26
qed
eberlm@63317
    27
eberlm@63319
    28
lemma fps_of_poly_0 [simp]: "fps_of_poly 0 = 0"
eberlm@63319
    29
  by (subst fps_const_0_eq_0 [symmetric], subst fps_of_poly_const [symmetric]) simp
eberlm@63317
    30
eberlm@63319
    31
lemma fps_of_poly_1 [simp]: "fps_of_poly 1 = 1"
eberlm@63319
    32
  by (subst fps_const_1_eq_1 [symmetric], subst fps_of_poly_const [symmetric])
eberlm@63317
    33
     (simp add: one_poly_def)
eberlm@63317
    34
eberlm@63319
    35
lemma fps_of_poly_1' [simp]: "fps_of_poly [:1:] = 1"
eberlm@63319
    36
  by (subst fps_const_1_eq_1 [symmetric], subst fps_of_poly_const [symmetric])
eberlm@63317
    37
     (simp add: one_poly_def)
eberlm@63317
    38
eberlm@63319
    39
lemma fps_of_poly_numeral [simp]: "fps_of_poly (numeral n) = numeral n"
eberlm@63319
    40
  by (simp add: numeral_fps_const fps_of_poly_const [symmetric] numeral_poly)
eberlm@63317
    41
eberlm@63319
    42
lemma fps_of_poly_numeral' [simp]: "fps_of_poly [:numeral n:] = numeral n"
eberlm@63319
    43
  by (simp add: numeral_fps_const fps_of_poly_const [symmetric] numeral_poly)
eberlm@63317
    44
eberlm@63319
    45
lemma fps_of_poly_X [simp]: "fps_of_poly [:0, 1:] = X"
eberlm@63319
    46
  by (auto simp add: fps_of_poly_def fps_eq_iff coeff_pCons split: nat.split)
eberlm@63317
    47
eberlm@63319
    48
lemma fps_of_poly_add: "fps_of_poly (p + q) = fps_of_poly p + fps_of_poly q"
eberlm@63319
    49
  by (simp add: fps_of_poly_def plus_poly.rep_eq fps_plus_def)
eberlm@63317
    50
eberlm@63319
    51
lemma fps_of_poly_diff: "fps_of_poly (p - q) = fps_of_poly p - fps_of_poly q"
eberlm@63319
    52
  by (simp add: fps_of_poly_def minus_poly.rep_eq fps_minus_def)
eberlm@63317
    53
eberlm@63319
    54
lemma fps_of_poly_uminus: "fps_of_poly (-p) = -fps_of_poly p"
eberlm@63319
    55
  by (simp add: fps_of_poly_def uminus_poly.rep_eq fps_uminus_def)
eberlm@63317
    56
eberlm@63319
    57
lemma fps_of_poly_mult: "fps_of_poly (p * q) = fps_of_poly p * fps_of_poly q"
eberlm@63319
    58
  by (simp add: fps_of_poly_def fps_times_def fps_eq_iff coeff_mult atLeast0AtMost)
eberlm@63317
    59
eberlm@63319
    60
lemma fps_of_poly_smult: 
eberlm@63319
    61
  "fps_of_poly (smult c p) = fps_const c * fps_of_poly p"
eberlm@63319
    62
  using fps_of_poly_mult[of "[:c:]" p] by (simp add: fps_of_poly_mult fps_of_poly_const)
eberlm@63317
    63
  
eberlm@63319
    64
lemma fps_of_poly_setsum: "fps_of_poly (setsum f A) = setsum (\<lambda>x. fps_of_poly (f x)) A"
eberlm@63319
    65
  by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_add)
eberlm@63317
    66
eberlm@63319
    67
lemma fps_of_poly_listsum: "fps_of_poly (listsum xs) = listsum (map fps_of_poly xs)"
eberlm@63319
    68
  by (induction xs) (simp_all add: fps_of_poly_add)
eberlm@63317
    69
  
eberlm@63319
    70
lemma fps_of_poly_setprod: "fps_of_poly (setprod f A) = setprod (\<lambda>x. fps_of_poly (f x)) A"
eberlm@63319
    71
  by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_mult)
eberlm@63317
    72
  
eberlm@63319
    73
lemma fps_of_poly_listprod: "fps_of_poly (listprod xs) = listprod (map fps_of_poly xs)"
eberlm@63319
    74
  by (induction xs) (simp_all add: fps_of_poly_mult)
eberlm@63317
    75
eberlm@63319
    76
lemma fps_of_poly_pCons: 
eberlm@63319
    77
  "fps_of_poly (pCons (c :: 'a :: semiring_1) p) = fps_const c + fps_of_poly p * X"
eberlm@63317
    78
  by (subst fps_mult_X_commute [symmetric], intro fps_ext) 
eberlm@63319
    79
     (auto simp: fps_of_poly_def coeff_pCons split: nat.split)
eberlm@63317
    80
  
eberlm@63319
    81
lemma fps_of_poly_pderiv: "fps_of_poly (pderiv p) = fps_deriv (fps_of_poly p)"
eberlm@63319
    82
  by (intro fps_ext) (simp add: fps_of_poly_nth coeff_pderiv)
eberlm@63317
    83
eberlm@63319
    84
lemma fps_of_poly_power: "fps_of_poly (p ^ n) = fps_of_poly p ^ n"
eberlm@63319
    85
  by (induction n) (simp_all add: fps_of_poly_mult)
eberlm@63317
    86
  
eberlm@63319
    87
lemma fps_of_poly_monom: "fps_of_poly (monom (c :: 'a :: comm_ring_1) n) = fps_const c * X ^ n"
eberlm@63317
    88
  by (intro fps_ext) simp_all
eberlm@63317
    89
eberlm@63319
    90
lemma fps_of_poly_monom': "fps_of_poly (monom (1 :: 'a :: comm_ring_1) n) = X ^ n"
eberlm@63319
    91
  by (simp add: fps_of_poly_monom)
eberlm@63317
    92
eberlm@63319
    93
lemma fps_of_poly_div:
eberlm@63317
    94
  assumes "(q :: 'a :: field poly) dvd p"
eberlm@63319
    95
  shows   "fps_of_poly (p div q) = fps_of_poly p / fps_of_poly q"
eberlm@63317
    96
proof (cases "q = 0")
eberlm@63317
    97
  case False
eberlm@63319
    98
  from False fps_of_poly_eq_iff[of q 0] have nz: "fps_of_poly q \<noteq> 0" by simp 
eberlm@63317
    99
  from assms have "p = (p div q) * q" by simp
eberlm@63319
   100
  also have "fps_of_poly \<dots> = fps_of_poly (p div q) * fps_of_poly q" 
eberlm@63319
   101
    by (simp add: fps_of_poly_mult)
eberlm@63319
   102
  also from nz have "\<dots> / fps_of_poly q = fps_of_poly (p div q)"
eberlm@63319
   103
    by (intro div_mult_self2_is_id) (auto simp: fps_of_poly_0)
eberlm@63317
   104
  finally show ?thesis ..
eberlm@63317
   105
qed simp
eberlm@63317
   106
eberlm@63319
   107
lemma fps_of_poly_divide_numeral:
eberlm@63319
   108
  "fps_of_poly (smult (inverse (numeral c :: 'a :: field)) p) = fps_of_poly p / numeral c"
eberlm@63317
   109
proof -
eberlm@63317
   110
  have "smult (inverse (numeral c)) p = [:inverse (numeral c):] * p" by simp
eberlm@63319
   111
  also have "fps_of_poly \<dots> = fps_of_poly p / numeral c"
eberlm@63319
   112
    by (subst fps_of_poly_mult) (simp add: numeral_fps_const fps_of_poly_pCons)
eberlm@63317
   113
  finally show ?thesis by simp
eberlm@63317
   114
qed
eberlm@63317
   115
eberlm@63317
   116
eberlm@63319
   117
lemma subdegree_fps_of_poly:
eberlm@63317
   118
  assumes "p \<noteq> 0"
eberlm@63317
   119
  defines "n \<equiv> Polynomial.order 0 p"
eberlm@63319
   120
  shows   "subdegree (fps_of_poly p) = n"
eberlm@63317
   121
proof (rule subdegreeI)
eberlm@63317
   122
  from assms have "monom 1 n dvd p" by (simp add: monom_1_dvd_iff)
eberlm@63319
   123
  thus zero: "fps_of_poly p $ i = 0" if "i < n" for i
eberlm@63317
   124
    using that by (simp add: monom_1_dvd_iff')
eberlm@63317
   125
    
eberlm@63317
   126
  from assms have "\<not>monom 1 (Suc n) dvd p"
eberlm@63317
   127
    by (auto simp: monom_1_dvd_iff simp del: power_Suc)
eberlm@63319
   128
  then obtain k where "k \<le> n" "fps_of_poly p $ k \<noteq> 0" 
eberlm@63317
   129
    by (auto simp: monom_1_dvd_iff' less_Suc_eq_le)
eberlm@63317
   130
  moreover from this and zero[of k] have "k = n" by linarith
eberlm@63319
   131
  ultimately show "fps_of_poly p $ n \<noteq> 0" by simp
eberlm@63317
   132
qed
eberlm@63317
   133
eberlm@63319
   134
lemma fps_of_poly_dvd:
eberlm@63317
   135
  assumes "p dvd q"
eberlm@63319
   136
  shows   "fps_of_poly (p :: 'a :: field poly) dvd fps_of_poly q"
eberlm@63317
   137
proof (cases "p = 0 \<or> q = 0")
eberlm@63317
   138
  case False
eberlm@63319
   139
  with assms fps_of_poly_eq_iff[of p 0] fps_of_poly_eq_iff[of q 0] show ?thesis
eberlm@63319
   140
    by (auto simp: fps_dvd_iff subdegree_fps_of_poly dvd_imp_order_le)
eberlm@63317
   141
qed (insert assms, auto)
eberlm@63317
   142
eberlm@63317
   143
eberlm@63319
   144
lemmas fps_of_poly_simps =
eberlm@63319
   145
  fps_of_poly_0 fps_of_poly_1 fps_of_poly_numeral fps_of_poly_const fps_of_poly_X
eberlm@63319
   146
  fps_of_poly_add fps_of_poly_diff fps_of_poly_uminus fps_of_poly_mult fps_of_poly_smult
eberlm@63319
   147
  fps_of_poly_setsum fps_of_poly_listsum fps_of_poly_setprod fps_of_poly_listprod
eberlm@63319
   148
  fps_of_poly_pCons fps_of_poly_pderiv fps_of_poly_power fps_of_poly_monom
eberlm@63319
   149
  fps_of_poly_divide_numeral
eberlm@63317
   150
eberlm@63319
   151
lemma fps_of_poly_pcompose:
eberlm@63317
   152
  assumes "coeff q 0 = (0 :: 'a :: idom)"
eberlm@63319
   153
  shows   "fps_of_poly (pcompose p q) = fps_compose (fps_of_poly p) (fps_of_poly q)"
eberlm@63317
   154
  using assms by (induction p rule: pCons_induct)
eberlm@63319
   155
                 (auto simp: pcompose_pCons fps_of_poly_simps fps_of_poly_pCons 
eberlm@63317
   156
                             fps_compose_add_distrib fps_compose_mult_distrib)
eberlm@63317
   157
  
eberlm@63317
   158
lemmas reify_fps_atom =
eberlm@63319
   159
  fps_of_poly_0 fps_of_poly_1' fps_of_poly_numeral' fps_of_poly_const fps_of_poly_X
eberlm@63317
   160
eberlm@63317
   161
eberlm@63317
   162
text \<open>
eberlm@63317
   163
  The following simproc can reduce the equality of two polynomial FPSs two equality of the
eberlm@63317
   164
  respective polynomials. A polynomial FPS is one that only has finitely many non-zero 
eberlm@63319
   165
  coefficients and can therefore be written as @{term "fps_of_poly p"} for some 
eberlm@63317
   166
  polynomial @{text "p"}.
eberlm@63317
   167
  
eberlm@63317
   168
  This may sound trivial, but it covers a number of annoying side conditions like 
eberlm@63317
   169
  @{term "1 + X \<noteq> 0"} that would otherwise not be solved automatically.
eberlm@63317
   170
\<close>
eberlm@63317
   171
eberlm@63317
   172
ML \<open>
eberlm@63317
   173
eberlm@63317
   174
(* TODO: Support for division *)
eberlm@63317
   175
signature POLY_FPS = sig
eberlm@63317
   176
eberlm@63317
   177
val reify_conv : conv
eberlm@63317
   178
val eq_conv : conv
eberlm@63317
   179
val eq_simproc : cterm -> thm option
eberlm@63317
   180
eberlm@63317
   181
end
eberlm@63317
   182
eberlm@63317
   183
eberlm@63317
   184
structure Poly_Fps = struct
eberlm@63317
   185
eberlm@63317
   186
fun const_binop_conv s conv ct =
eberlm@63317
   187
  case Thm.term_of ct of
eberlm@63317
   188
    (Const (s', _) $ _ $ _) => 
eberlm@63317
   189
      if s = s' then 
eberlm@63317
   190
        Conv.binop_conv conv ct 
eberlm@63317
   191
      else 
eberlm@63317
   192
        raise CTERM ("const_binop_conv", [ct])
eberlm@63317
   193
  | _ => raise CTERM ("const_binop_conv", [ct])
eberlm@63317
   194
eberlm@63317
   195
fun reify_conv ct = 
eberlm@63317
   196
  let
eberlm@63317
   197
    val rewr = Conv.rewrs_conv o map (fn thm => thm RS @{thm eq_reflection})
eberlm@63317
   198
    val un = Conv.arg_conv reify_conv
eberlm@63317
   199
    val bin = Conv.binop_conv reify_conv
eberlm@63317
   200
  in
eberlm@63317
   201
    case Thm.term_of ct of
eberlm@63319
   202
      (Const (@{const_name "fps_of_poly"}, _) $ _) => ct |> Conv.all_conv
eberlm@63317
   203
    | (Const (@{const_name "Groups.plus"}, _) $ _ $ _) => ct |> (
eberlm@63319
   204
        bin then_conv rewr @{thms fps_of_poly_add [symmetric]})
eberlm@63317
   205
    | (Const (@{const_name "Groups.uminus"}, _) $ _) => ct |> (
eberlm@63319
   206
        un then_conv rewr @{thms fps_of_poly_uminus [symmetric]})
eberlm@63317
   207
    | (Const (@{const_name "Groups.minus"}, _) $ _ $ _) => ct |> (
eberlm@63319
   208
        bin then_conv rewr @{thms fps_of_poly_diff [symmetric]})
eberlm@63317
   209
    | (Const (@{const_name "Groups.times"}, _) $ _ $ _) => ct |> (
eberlm@63319
   210
        bin then_conv rewr @{thms fps_of_poly_mult [symmetric]})
eberlm@63317
   211
    | (Const (@{const_name "Rings.divide"}, _) $ _ $ (Const (@{const_name "Num.numeral"}, _) $ _))
eberlm@63317
   212
        => ct |> (Conv.fun_conv (Conv.arg_conv reify_conv)
eberlm@63319
   213
             then_conv rewr @{thms fps_of_poly_divide_numeral [symmetric]})
eberlm@63317
   214
    | (Const (@{const_name "Power.power"}, _) $ Const (@{const_name "X"},_) $ _) => ct |> (
eberlm@63319
   215
        rewr @{thms fps_of_poly_monom' [symmetric]}) 
eberlm@63317
   216
    | (Const (@{const_name "Power.power"}, _) $ _ $ _) => ct |> (
eberlm@63317
   217
        Conv.fun_conv (Conv.arg_conv reify_conv) 
eberlm@63319
   218
        then_conv rewr @{thms fps_of_poly_power [symmetric]})
eberlm@63317
   219
    | _ => ct |> (
eberlm@63317
   220
        rewr @{thms reify_fps_atom [symmetric]})
eberlm@63317
   221
  end
eberlm@63317
   222
    
eberlm@63317
   223
eberlm@63317
   224
fun eq_conv ct =
eberlm@63317
   225
  case Thm.term_of ct of
eberlm@63317
   226
    (Const (@{const_name "HOL.eq"}, _) $ _ $ _) => ct |> (
eberlm@63317
   227
      Conv.binop_conv reify_conv
eberlm@63319
   228
      then_conv Conv.rewr_conv @{thm fps_of_poly_eq_iff[THEN eq_reflection]})
eberlm@63317
   229
  | _ => raise CTERM ("poly_fps_eq_conv", [ct])
eberlm@63317
   230
eberlm@63317
   231
val eq_simproc = try eq_conv
eberlm@63317
   232
eberlm@63317
   233
end
eberlm@63317
   234
\<close> 
eberlm@63317
   235
eberlm@63317
   236
simproc_setup poly_fps_eq ("(f :: 'a fps) = g") = \<open>K (K Poly_Fps.eq_simproc)\<close>
eberlm@63317
   237
eberlm@63319
   238
lemma fps_of_poly_linear: "fps_of_poly [:a,1 :: 'a :: field:] = X + fps_const a"
eberlm@63317
   239
  by simp
eberlm@63317
   240
eberlm@63319
   241
lemma fps_of_poly_linear': "fps_of_poly [:1,a :: 'a :: field:] = 1 + fps_const a * X"
eberlm@63317
   242
  by simp
eberlm@63317
   243
eberlm@63319
   244
lemma fps_of_poly_cutoff [simp]: 
eberlm@63319
   245
  "fps_of_poly (poly_cutoff n p) = fps_cutoff n (fps_of_poly p)"
eberlm@63317
   246
  by (simp add: fps_eq_iff coeff_poly_cutoff)
eberlm@63317
   247
eberlm@63319
   248
lemma fps_of_poly_shift [simp]: "fps_of_poly (poly_shift n p) = fps_shift n (fps_of_poly p)"
eberlm@63317
   249
  by (simp add: fps_eq_iff coeff_poly_shift)
eberlm@63317
   250
eberlm@63317
   251
eberlm@63317
   252
definition poly_subdegree :: "'a::zero poly \<Rightarrow> nat" where
eberlm@63319
   253
  "poly_subdegree p = subdegree (fps_of_poly p)"
eberlm@63317
   254
eberlm@63317
   255
lemma coeff_less_poly_subdegree:
eberlm@63317
   256
  "k < poly_subdegree p \<Longrightarrow> coeff p k = 0"
eberlm@63319
   257
  unfolding poly_subdegree_def using nth_less_subdegree_zero[of k "fps_of_poly p"] by simp
eberlm@63317
   258
eberlm@63317
   259
(* TODO: Move ? *)
eberlm@63317
   260
definition prefix_length :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat" where
eberlm@63317
   261
  "prefix_length P xs = length (takeWhile P xs)"
eberlm@63317
   262
eberlm@63317
   263
primrec prefix_length_aux :: "('a \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat" where
eberlm@63317
   264
  "prefix_length_aux P acc [] = acc"
eberlm@63317
   265
| "prefix_length_aux P acc (x#xs) = (if P x then prefix_length_aux P (Suc acc) xs else acc)"
eberlm@63317
   266
eberlm@63317
   267
lemma prefix_length_aux_correct: "prefix_length_aux P acc xs = prefix_length P xs + acc"
eberlm@63317
   268
  by (induction xs arbitrary: acc) (simp_all add: prefix_length_def)
eberlm@63317
   269
eberlm@63317
   270
lemma prefix_length_code [code]: "prefix_length P xs = prefix_length_aux P 0 xs"
eberlm@63317
   271
  by (simp add: prefix_length_aux_correct)
eberlm@63317
   272
eberlm@63317
   273
lemma prefix_length_le_length: "prefix_length P xs \<le> length xs"
eberlm@63317
   274
  by (induction xs) (simp_all add: prefix_length_def)
eberlm@63317
   275
  
eberlm@63317
   276
lemma prefix_length_less_length: "(\<exists>x\<in>set xs. \<not>P x) \<Longrightarrow> prefix_length P xs < length xs"
eberlm@63317
   277
  by (induction xs) (simp_all add: prefix_length_def)
eberlm@63317
   278
eberlm@63317
   279
lemma nth_prefix_length:
eberlm@63317
   280
  "(\<exists>x\<in>set xs. \<not>P x) \<Longrightarrow> \<not>P (xs ! prefix_length P xs)"
eberlm@63317
   281
  by (induction xs) (simp_all add: prefix_length_def)
eberlm@63317
   282
  
eberlm@63317
   283
lemma nth_less_prefix_length:
eberlm@63317
   284
  "n < prefix_length P xs \<Longrightarrow> P (xs ! n)"
eberlm@63317
   285
  by (induction xs arbitrary: n) 
eberlm@63317
   286
     (auto simp: prefix_length_def nth_Cons split: if_splits nat.splits)
eberlm@63317
   287
(* END TODO *)
eberlm@63317
   288
  
eberlm@63317
   289
lemma poly_subdegree_code [code]: "poly_subdegree p = prefix_length (op = 0) (coeffs p)"
eberlm@63317
   290
proof (cases "p = 0")
eberlm@63317
   291
  case False
eberlm@63317
   292
  note [simp] = this
eberlm@63317
   293
  define n where "n = prefix_length (op = 0) (coeffs p)"
eberlm@63317
   294
  from False have "\<exists>k. coeff p k \<noteq> 0" by (auto simp: poly_eq_iff)
eberlm@63317
   295
  hence ex: "\<exists>x\<in>set (coeffs p). x \<noteq> 0" by (auto simp: coeffs_def)
eberlm@63317
   296
  hence n_less: "n < length (coeffs p)" and nonzero: "coeffs p ! n \<noteq> 0" 
eberlm@63317
   297
    unfolding n_def by (auto intro!: prefix_length_less_length nth_prefix_length)
eberlm@63317
   298
  show ?thesis unfolding poly_subdegree_def
eberlm@63317
   299
  proof (intro subdegreeI)
eberlm@63319
   300
    from n_less have "fps_of_poly p $ n = coeffs p ! n"
eberlm@63317
   301
      by (subst coeffs_nth) (simp_all add: degree_eq_length_coeffs)
eberlm@63319
   302
    with nonzero show "fps_of_poly p $ prefix_length (op = 0) (coeffs p) \<noteq> 0"
eberlm@63317
   303
      unfolding n_def by simp
eberlm@63317
   304
  next
eberlm@63317
   305
    fix k assume A: "k < prefix_length (op = 0) (coeffs p)"
eberlm@63317
   306
    also have "\<dots> \<le> length (coeffs p)" by (rule prefix_length_le_length)
eberlm@63319
   307
    finally show "fps_of_poly p $ k = 0"
eberlm@63317
   308
      using nth_less_prefix_length[OF A]
eberlm@63317
   309
      by (simp add: coeffs_nth degree_eq_length_coeffs)
eberlm@63317
   310
  qed
eberlm@63317
   311
qed (simp_all add: poly_subdegree_def prefix_length_def)
eberlm@63317
   312
eberlm@63317
   313
end