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