src/HOL/Library/Polynomial_FPS.thy
 author haftmann Sun Oct 16 09:31:04 2016 +0200 (2016-10-16) changeset 64240 eabf80376aab parent 63882 018998c00003 child 64267 b9a1486e79be permissions -rw-r--r--
more standardized names
 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 \Converting polynomials to formal power series\ ``` 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 \ 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 (\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` nipkow@63882 ` 67` ```lemma fps_of_poly_sum_list: "fps_of_poly (sum_list xs) = sum_list (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 (\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` ``` ``` nipkow@63882 ` 73` ```lemma fps_of_poly_prod_list: "fps_of_poly (prod_list xs) = prod_list (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 \ 0" by simp ``` eberlm@63317 ` 99` ``` from assms have "p = (p div q) * q" by simp ``` eberlm@63319 ` 100` ``` also have "fps_of_poly \ = 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 "\ / fps_of_poly q = fps_of_poly (p div q)" ``` haftmann@64240 ` 103` ``` by (intro nonzero_mult_div_cancel_right) (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 \ = 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 \ 0" ``` eberlm@63317 ` 119` ``` defines "n \ 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 "\monom 1 (Suc n) dvd p" ``` eberlm@63317 ` 127` ``` by (auto simp: monom_1_dvd_iff simp del: power_Suc) ``` wenzelm@63539 ` 128` ``` then obtain k where k: "k \ n" "fps_of_poly p \$ k \ 0" ``` eberlm@63317 ` 129` ``` by (auto simp: monom_1_dvd_iff' less_Suc_eq_le) ``` wenzelm@63539 ` 130` ``` with zero[of k] have "k = n" by linarith ``` wenzelm@63539 ` 131` ``` with k show "fps_of_poly p \$ n \ 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 \ 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 ``` nipkow@63882 ` 147` ``` fps_of_poly_setsum fps_of_poly_sum_list fps_of_poly_setprod fps_of_poly_prod_list ``` 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 \ ``` 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 \ 0"} that would otherwise not be solved automatically. ``` eberlm@63317 ` 170` ```\ ``` eberlm@63317 ` 171` eberlm@63317 ` 172` ```ML \ ``` 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` ```\ ``` eberlm@63317 ` 235` eberlm@63317 ` 236` ```simproc_setup poly_fps_eq ("(f :: 'a fps) = g") = \K (K Poly_Fps.eq_simproc)\ ``` 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 \ 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 \ 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 \ bool) \ 'a list \ nat" where ``` eberlm@63317 ` 261` ``` "prefix_length P xs = length (takeWhile P xs)" ``` eberlm@63317 ` 262` eberlm@63317 ` 263` ```primrec prefix_length_aux :: "('a \ bool) \ nat \ 'a list \ 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 \ 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: "(\x\set xs. \P x) \ 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` ``` "(\x\set xs. \P x) \ \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 \ 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 "\k. coeff p k \ 0" by (auto simp: poly_eq_iff) ``` eberlm@63317 ` 295` ``` hence ex: "\x\set (coeffs p). x \ 0" by (auto simp: coeffs_def) ``` eberlm@63317 ` 296` ``` hence n_less: "n < length (coeffs p)" and nonzero: "coeffs p ! n \ 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) \ 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 "\ \ 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 ```