author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 64911  f0e07600de47 
child 65366  10ca63a18e56 
permissions  rwrr 
63317  1 
(* 
2 
File: Polynomial_FPS.thy 

3 
Author: Manuel Eberl (TUM) 

4 

5 
Converting polynomials to formal power series 

6 
*) 

7 

8 
section \<open>Converting polynomials to formal power series\<close> 

9 
theory Polynomial_FPS 

10 
imports Polynomial Formal_Power_Series 

11 
begin 

12 

63319  13 
definition fps_of_poly where 
14 
"fps_of_poly p = Abs_fps (coeff p)" 

63317  15 

63319  16 
lemma fps_of_poly_eq_iff: "fps_of_poly p = fps_of_poly q \<longleftrightarrow> p = q" 
17 
by (simp add: fps_of_poly_def poly_eq_iff fps_eq_iff) 

63317  18 

63319  19 
lemma fps_of_poly_nth [simp]: "fps_of_poly p $ n = coeff p n" 
20 
by (simp add: fps_of_poly_def) 

63317  21 

63319  22 
lemma fps_of_poly_const: "fps_of_poly [:c:] = fps_const c" 
63317  23 
proof (subst fps_eq_iff, clarify) 
63319  24 
fix n :: nat show "fps_of_poly [:c:] $ n = fps_const c $ n" 
25 
by (cases n) (auto simp: fps_of_poly_def) 

63317  26 
qed 
27 

63319  28 
lemma fps_of_poly_0 [simp]: "fps_of_poly 0 = 0" 
29 
by (subst fps_const_0_eq_0 [symmetric], subst fps_of_poly_const [symmetric]) simp 

63317  30 

63319  31 
lemma fps_of_poly_1 [simp]: "fps_of_poly 1 = 1" 
32 
by (subst fps_const_1_eq_1 [symmetric], subst fps_of_poly_const [symmetric]) 

63317  33 
(simp add: one_poly_def) 
34 

63319  35 
lemma fps_of_poly_1' [simp]: "fps_of_poly [:1:] = 1" 
36 
by (subst fps_const_1_eq_1 [symmetric], subst fps_of_poly_const [symmetric]) 

63317  37 
(simp add: one_poly_def) 
38 

63319  39 
lemma fps_of_poly_numeral [simp]: "fps_of_poly (numeral n) = numeral n" 
40 
by (simp add: numeral_fps_const fps_of_poly_const [symmetric] numeral_poly) 

63317  41 

63319  42 
lemma fps_of_poly_numeral' [simp]: "fps_of_poly [:numeral n:] = numeral n" 
43 
by (simp add: numeral_fps_const fps_of_poly_const [symmetric] numeral_poly) 

63317  44 

63319  45 
lemma fps_of_poly_X [simp]: "fps_of_poly [:0, 1:] = X" 
46 
by (auto simp add: fps_of_poly_def fps_eq_iff coeff_pCons split: nat.split) 

63317  47 

63319  48 
lemma fps_of_poly_add: "fps_of_poly (p + q) = fps_of_poly p + fps_of_poly q" 
49 
by (simp add: fps_of_poly_def plus_poly.rep_eq fps_plus_def) 

63317  50 

63319  51 
lemma fps_of_poly_diff: "fps_of_poly (p  q) = fps_of_poly p  fps_of_poly q" 
52 
by (simp add: fps_of_poly_def minus_poly.rep_eq fps_minus_def) 

63317  53 

63319  54 
lemma fps_of_poly_uminus: "fps_of_poly (p) = fps_of_poly p" 
55 
by (simp add: fps_of_poly_def uminus_poly.rep_eq fps_uminus_def) 

63317  56 

63319  57 
lemma fps_of_poly_mult: "fps_of_poly (p * q) = fps_of_poly p * fps_of_poly q" 
58 
by (simp add: fps_of_poly_def fps_times_def fps_eq_iff coeff_mult atLeast0AtMost) 

63317  59 

63319  60 
lemma fps_of_poly_smult: 
61 
"fps_of_poly (smult c p) = fps_const c * fps_of_poly p" 

62 
using fps_of_poly_mult[of "[:c:]" p] by (simp add: fps_of_poly_mult fps_of_poly_const) 

63317  63 

64267  64 
lemma fps_of_poly_sum: "fps_of_poly (sum f A) = sum (\<lambda>x. fps_of_poly (f x)) A" 
63319  65 
by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_add) 
63317  66 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63539
diff
changeset

67 
lemma fps_of_poly_sum_list: "fps_of_poly (sum_list xs) = sum_list (map fps_of_poly xs)" 
63319  68 
by (induction xs) (simp_all add: fps_of_poly_add) 
63317  69 

64272  70 
lemma fps_of_poly_prod: "fps_of_poly (prod f A) = prod (\<lambda>x. fps_of_poly (f x)) A" 
63319  71 
by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_mult) 
63317  72 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63539
diff
changeset

73 
lemma fps_of_poly_prod_list: "fps_of_poly (prod_list xs) = prod_list (map fps_of_poly xs)" 
63319  74 
by (induction xs) (simp_all add: fps_of_poly_mult) 
63317  75 

63319  76 
lemma fps_of_poly_pCons: 
77 
"fps_of_poly (pCons (c :: 'a :: semiring_1) p) = fps_const c + fps_of_poly p * X" 

63317  78 
by (subst fps_mult_X_commute [symmetric], intro fps_ext) 
63319  79 
(auto simp: fps_of_poly_def coeff_pCons split: nat.split) 
63317  80 

63319  81 
lemma fps_of_poly_pderiv: "fps_of_poly (pderiv p) = fps_deriv (fps_of_poly p)" 
82 
by (intro fps_ext) (simp add: fps_of_poly_nth coeff_pderiv) 

63317  83 

63319  84 
lemma fps_of_poly_power: "fps_of_poly (p ^ n) = fps_of_poly p ^ n" 
85 
by (induction n) (simp_all add: fps_of_poly_mult) 

63317  86 

63319  87 
lemma fps_of_poly_monom: "fps_of_poly (monom (c :: 'a :: comm_ring_1) n) = fps_const c * X ^ n" 
63317  88 
by (intro fps_ext) simp_all 
89 

63319  90 
lemma fps_of_poly_monom': "fps_of_poly (monom (1 :: 'a :: comm_ring_1) n) = X ^ n" 
91 
by (simp add: fps_of_poly_monom) 

63317  92 

63319  93 
lemma fps_of_poly_div: 
63317  94 
assumes "(q :: 'a :: field poly) dvd p" 
63319  95 
shows "fps_of_poly (p div q) = fps_of_poly p / fps_of_poly q" 
63317  96 
proof (cases "q = 0") 
97 
case False 

63319  98 
from False fps_of_poly_eq_iff[of q 0] have nz: "fps_of_poly q \<noteq> 0" by simp 
63317  99 
from assms have "p = (p div q) * q" by simp 
63319  100 
also have "fps_of_poly \<dots> = fps_of_poly (p div q) * fps_of_poly q" 
101 
by (simp add: fps_of_poly_mult) 

102 
also from nz have "\<dots> / fps_of_poly q = fps_of_poly (p div q)" 

64240  103 
by (intro nonzero_mult_div_cancel_right) (auto simp: fps_of_poly_0) 
63317  104 
finally show ?thesis .. 
105 
qed simp 

106 

63319  107 
lemma fps_of_poly_divide_numeral: 
108 
"fps_of_poly (smult (inverse (numeral c :: 'a :: field)) p) = fps_of_poly p / numeral c" 

63317  109 
proof  
110 
have "smult (inverse (numeral c)) p = [:inverse (numeral c):] * p" by simp 

63319  111 
also have "fps_of_poly \<dots> = fps_of_poly p / numeral c" 
112 
by (subst fps_of_poly_mult) (simp add: numeral_fps_const fps_of_poly_pCons) 

63317  113 
finally show ?thesis by simp 
114 
qed 

115 

116 

63319  117 
lemma subdegree_fps_of_poly: 
63317  118 
assumes "p \<noteq> 0" 
119 
defines "n \<equiv> Polynomial.order 0 p" 

63319  120 
shows "subdegree (fps_of_poly p) = n" 
63317  121 
proof (rule subdegreeI) 
122 
from assms have "monom 1 n dvd p" by (simp add: monom_1_dvd_iff) 

63319  123 
thus zero: "fps_of_poly p $ i = 0" if "i < n" for i 
63317  124 
using that by (simp add: monom_1_dvd_iff') 
125 

126 
from assms have "\<not>monom 1 (Suc n) dvd p" 

127 
by (auto simp: monom_1_dvd_iff simp del: power_Suc) 

63539  128 
then obtain k where k: "k \<le> n" "fps_of_poly p $ k \<noteq> 0" 
63317  129 
by (auto simp: monom_1_dvd_iff' less_Suc_eq_le) 
63539  130 
with zero[of k] have "k = n" by linarith 
131 
with k show "fps_of_poly p $ n \<noteq> 0" by simp 

63317  132 
qed 
133 

63319  134 
lemma fps_of_poly_dvd: 
63317  135 
assumes "p dvd q" 
63319  136 
shows "fps_of_poly (p :: 'a :: field poly) dvd fps_of_poly q" 
63317  137 
proof (cases "p = 0 \<or> q = 0") 
138 
case False 

63319  139 
with assms fps_of_poly_eq_iff[of p 0] fps_of_poly_eq_iff[of q 0] show ?thesis 
140 
by (auto simp: fps_dvd_iff subdegree_fps_of_poly dvd_imp_order_le) 

63317  141 
qed (insert assms, auto) 
142 

143 

63319  144 
lemmas fps_of_poly_simps = 
145 
fps_of_poly_0 fps_of_poly_1 fps_of_poly_numeral fps_of_poly_const fps_of_poly_X 

146 
fps_of_poly_add fps_of_poly_diff fps_of_poly_uminus fps_of_poly_mult fps_of_poly_smult 

64272  147 
fps_of_poly_sum fps_of_poly_sum_list fps_of_poly_prod fps_of_poly_prod_list 
63319  148 
fps_of_poly_pCons fps_of_poly_pderiv fps_of_poly_power fps_of_poly_monom 
149 
fps_of_poly_divide_numeral 

63317  150 

63319  151 
lemma fps_of_poly_pcompose: 
63317  152 
assumes "coeff q 0 = (0 :: 'a :: idom)" 
63319  153 
shows "fps_of_poly (pcompose p q) = fps_compose (fps_of_poly p) (fps_of_poly q)" 
63317  154 
using assms by (induction p rule: pCons_induct) 
63319  155 
(auto simp: pcompose_pCons fps_of_poly_simps fps_of_poly_pCons 
63317  156 
fps_compose_add_distrib fps_compose_mult_distrib) 
157 

158 
lemmas reify_fps_atom = 

63319  159 
fps_of_poly_0 fps_of_poly_1' fps_of_poly_numeral' fps_of_poly_const fps_of_poly_X 
63317  160 

161 

162 
text \<open> 

163 
The following simproc can reduce the equality of two polynomial FPSs two equality of the 

164 
respective polynomials. A polynomial FPS is one that only has finitely many nonzero 

63319  165 
coefficients and can therefore be written as @{term "fps_of_poly p"} for some 
64911  166 
polynomial \<open>p\<close>. 
63317  167 

168 
This may sound trivial, but it covers a number of annoying side conditions like 

169 
@{term "1 + X \<noteq> 0"} that would otherwise not be solved automatically. 

170 
\<close> 

171 

172 
ML \<open> 

173 

174 
(* TODO: Support for division *) 

175 
signature POLY_FPS = sig 

176 

177 
val reify_conv : conv 

178 
val eq_conv : conv 

179 
val eq_simproc : cterm > thm option 

180 

181 
end 

182 

183 

184 
structure Poly_Fps = struct 

185 

186 
fun const_binop_conv s conv ct = 

187 
case Thm.term_of ct of 

188 
(Const (s', _) $ _ $ _) => 

189 
if s = s' then 

190 
Conv.binop_conv conv ct 

191 
else 

192 
raise CTERM ("const_binop_conv", [ct]) 

193 
 _ => raise CTERM ("const_binop_conv", [ct]) 

194 

195 
fun reify_conv ct = 

196 
let 

197 
val rewr = Conv.rewrs_conv o map (fn thm => thm RS @{thm eq_reflection}) 

198 
val un = Conv.arg_conv reify_conv 

199 
val bin = Conv.binop_conv reify_conv 

200 
in 

201 
case Thm.term_of ct of 

63319  202 
(Const (@{const_name "fps_of_poly"}, _) $ _) => ct > Conv.all_conv 
63317  203 
 (Const (@{const_name "Groups.plus"}, _) $ _ $ _) => ct > ( 
63319  204 
bin then_conv rewr @{thms fps_of_poly_add [symmetric]}) 
63317  205 
 (Const (@{const_name "Groups.uminus"}, _) $ _) => ct > ( 
63319  206 
un then_conv rewr @{thms fps_of_poly_uminus [symmetric]}) 
63317  207 
 (Const (@{const_name "Groups.minus"}, _) $ _ $ _) => ct > ( 
63319  208 
bin then_conv rewr @{thms fps_of_poly_diff [symmetric]}) 
63317  209 
 (Const (@{const_name "Groups.times"}, _) $ _ $ _) => ct > ( 
63319  210 
bin then_conv rewr @{thms fps_of_poly_mult [symmetric]}) 
63317  211 
 (Const (@{const_name "Rings.divide"}, _) $ _ $ (Const (@{const_name "Num.numeral"}, _) $ _)) 
212 
=> ct > (Conv.fun_conv (Conv.arg_conv reify_conv) 

63319  213 
then_conv rewr @{thms fps_of_poly_divide_numeral [symmetric]}) 
63317  214 
 (Const (@{const_name "Power.power"}, _) $ Const (@{const_name "X"},_) $ _) => ct > ( 
63319  215 
rewr @{thms fps_of_poly_monom' [symmetric]}) 
63317  216 
 (Const (@{const_name "Power.power"}, _) $ _ $ _) => ct > ( 
217 
Conv.fun_conv (Conv.arg_conv reify_conv) 

63319  218 
then_conv rewr @{thms fps_of_poly_power [symmetric]}) 
63317  219 
 _ => ct > ( 
220 
rewr @{thms reify_fps_atom [symmetric]}) 

221 
end 

222 

223 

224 
fun eq_conv ct = 

225 
case Thm.term_of ct of 

226 
(Const (@{const_name "HOL.eq"}, _) $ _ $ _) => ct > ( 

227 
Conv.binop_conv reify_conv 

63319  228 
then_conv Conv.rewr_conv @{thm fps_of_poly_eq_iff[THEN eq_reflection]}) 
63317  229 
 _ => raise CTERM ("poly_fps_eq_conv", [ct]) 
230 

231 
val eq_simproc = try eq_conv 

232 

233 
end 

234 
\<close> 

235 

236 
simproc_setup poly_fps_eq ("(f :: 'a fps) = g") = \<open>K (K Poly_Fps.eq_simproc)\<close> 

237 

63319  238 
lemma fps_of_poly_linear: "fps_of_poly [:a,1 :: 'a :: field:] = X + fps_const a" 
63317  239 
by simp 
240 

63319  241 
lemma fps_of_poly_linear': "fps_of_poly [:1,a :: 'a :: field:] = 1 + fps_const a * X" 
63317  242 
by simp 
243 

63319  244 
lemma fps_of_poly_cutoff [simp]: 
245 
"fps_of_poly (poly_cutoff n p) = fps_cutoff n (fps_of_poly p)" 

63317  246 
by (simp add: fps_eq_iff coeff_poly_cutoff) 
247 

63319  248 
lemma fps_of_poly_shift [simp]: "fps_of_poly (poly_shift n p) = fps_shift n (fps_of_poly p)" 
63317  249 
by (simp add: fps_eq_iff coeff_poly_shift) 
250 

251 

252 
definition poly_subdegree :: "'a::zero poly \<Rightarrow> nat" where 

63319  253 
"poly_subdegree p = subdegree (fps_of_poly p)" 
63317  254 

255 
lemma coeff_less_poly_subdegree: 

256 
"k < poly_subdegree p \<Longrightarrow> coeff p k = 0" 

63319  257 
unfolding poly_subdegree_def using nth_less_subdegree_zero[of k "fps_of_poly p"] by simp 
63317  258 

259 
(* TODO: Move ? *) 

260 
definition prefix_length :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat" where 

261 
"prefix_length P xs = length (takeWhile P xs)" 

262 

263 
primrec prefix_length_aux :: "('a \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat" where 

264 
"prefix_length_aux P acc [] = acc" 

265 
 "prefix_length_aux P acc (x#xs) = (if P x then prefix_length_aux P (Suc acc) xs else acc)" 

266 

267 
lemma prefix_length_aux_correct: "prefix_length_aux P acc xs = prefix_length P xs + acc" 

268 
by (induction xs arbitrary: acc) (simp_all add: prefix_length_def) 

269 

270 
lemma prefix_length_code [code]: "prefix_length P xs = prefix_length_aux P 0 xs" 

271 
by (simp add: prefix_length_aux_correct) 

272 

273 
lemma prefix_length_le_length: "prefix_length P xs \<le> length xs" 

274 
by (induction xs) (simp_all add: prefix_length_def) 

275 

276 
lemma prefix_length_less_length: "(\<exists>x\<in>set xs. \<not>P x) \<Longrightarrow> prefix_length P xs < length xs" 

277 
by (induction xs) (simp_all add: prefix_length_def) 

278 

279 
lemma nth_prefix_length: 

280 
"(\<exists>x\<in>set xs. \<not>P x) \<Longrightarrow> \<not>P (xs ! prefix_length P xs)" 

281 
by (induction xs) (simp_all add: prefix_length_def) 

282 

283 
lemma nth_less_prefix_length: 

284 
"n < prefix_length P xs \<Longrightarrow> P (xs ! n)" 

285 
by (induction xs arbitrary: n) 

286 
(auto simp: prefix_length_def nth_Cons split: if_splits nat.splits) 

287 
(* END TODO *) 

288 

289 
lemma poly_subdegree_code [code]: "poly_subdegree p = prefix_length (op = 0) (coeffs p)" 

290 
proof (cases "p = 0") 

291 
case False 

292 
note [simp] = this 

293 
define n where "n = prefix_length (op = 0) (coeffs p)" 

294 
from False have "\<exists>k. coeff p k \<noteq> 0" by (auto simp: poly_eq_iff) 

295 
hence ex: "\<exists>x\<in>set (coeffs p). x \<noteq> 0" by (auto simp: coeffs_def) 

296 
hence n_less: "n < length (coeffs p)" and nonzero: "coeffs p ! n \<noteq> 0" 

297 
unfolding n_def by (auto intro!: prefix_length_less_length nth_prefix_length) 

298 
show ?thesis unfolding poly_subdegree_def 

299 
proof (intro subdegreeI) 

63319  300 
from n_less have "fps_of_poly p $ n = coeffs p ! n" 
63317  301 
by (subst coeffs_nth) (simp_all add: degree_eq_length_coeffs) 
63319  302 
with nonzero show "fps_of_poly p $ prefix_length (op = 0) (coeffs p) \<noteq> 0" 
63317  303 
unfolding n_def by simp 
304 
next 

305 
fix k assume A: "k < prefix_length (op = 0) (coeffs p)" 

306 
also have "\<dots> \<le> length (coeffs p)" by (rule prefix_length_le_length) 

63319  307 
finally show "fps_of_poly p $ k = 0" 
63317  308 
using nth_less_prefix_length[OF A] 
309 
by (simp add: coeffs_nth degree_eq_length_coeffs) 

310 
qed 

311 
qed (simp_all add: poly_subdegree_def prefix_length_def) 

312 

313 
end 