src/HOL/Library/Polynomial_FPS.thy
author wenzelm
Tue Jan 17 13:59:10 2017 +0100 (2017-01-17)
changeset 64911 f0e07600de47
parent 64272 f76b6dda2e56
child 65366 10ca63a18e56
permissions -rw-r--r--
isabelle update_cartouches -c -t;
     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 
    13 definition fps_of_poly where
    14   "fps_of_poly p = Abs_fps (coeff p)"
    15 
    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)
    18 
    19 lemma fps_of_poly_nth [simp]: "fps_of_poly p $ n = coeff p n"
    20   by (simp add: fps_of_poly_def)
    21   
    22 lemma fps_of_poly_const: "fps_of_poly [:c:] = fps_const c"
    23 proof (subst fps_eq_iff, clarify)
    24   fix n :: nat show "fps_of_poly [:c:] $ n = fps_const c $ n"
    25     by (cases n) (auto simp: fps_of_poly_def)
    26 qed
    27 
    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
    30 
    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])
    33      (simp add: one_poly_def)
    34 
    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])
    37      (simp add: one_poly_def)
    38 
    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)
    41 
    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)
    44 
    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)
    47 
    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)
    50 
    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)
    53 
    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)
    56 
    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)
    59 
    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)
    63   
    64 lemma fps_of_poly_sum: "fps_of_poly (sum f A) = sum (\<lambda>x. fps_of_poly (f x)) A"
    65   by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_add)
    66 
    67 lemma fps_of_poly_sum_list: "fps_of_poly (sum_list xs) = sum_list (map fps_of_poly xs)"
    68   by (induction xs) (simp_all add: fps_of_poly_add)
    69   
    70 lemma fps_of_poly_prod: "fps_of_poly (prod f A) = prod (\<lambda>x. fps_of_poly (f x)) A"
    71   by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_mult)
    72   
    73 lemma fps_of_poly_prod_list: "fps_of_poly (prod_list xs) = prod_list (map fps_of_poly xs)"
    74   by (induction xs) (simp_all add: fps_of_poly_mult)
    75 
    76 lemma fps_of_poly_pCons: 
    77   "fps_of_poly (pCons (c :: 'a :: semiring_1) p) = fps_const c + fps_of_poly p * X"
    78   by (subst fps_mult_X_commute [symmetric], intro fps_ext) 
    79      (auto simp: fps_of_poly_def coeff_pCons split: nat.split)
    80   
    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)
    83 
    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)
    86   
    87 lemma fps_of_poly_monom: "fps_of_poly (monom (c :: 'a :: comm_ring_1) n) = fps_const c * X ^ n"
    88   by (intro fps_ext) simp_all
    89 
    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)
    92 
    93 lemma fps_of_poly_div:
    94   assumes "(q :: 'a :: field poly) dvd p"
    95   shows   "fps_of_poly (p div q) = fps_of_poly p / fps_of_poly q"
    96 proof (cases "q = 0")
    97   case False
    98   from False fps_of_poly_eq_iff[of q 0] have nz: "fps_of_poly q \<noteq> 0" by simp 
    99   from assms have "p = (p div q) * q" by simp
   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)"
   103     by (intro nonzero_mult_div_cancel_right) (auto simp: fps_of_poly_0)
   104   finally show ?thesis ..
   105 qed simp
   106 
   107 lemma fps_of_poly_divide_numeral:
   108   "fps_of_poly (smult (inverse (numeral c :: 'a :: field)) p) = fps_of_poly p / numeral c"
   109 proof -
   110   have "smult (inverse (numeral c)) p = [:inverse (numeral c):] * p" by simp
   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)
   113   finally show ?thesis by simp
   114 qed
   115 
   116 
   117 lemma subdegree_fps_of_poly:
   118   assumes "p \<noteq> 0"
   119   defines "n \<equiv> Polynomial.order 0 p"
   120   shows   "subdegree (fps_of_poly p) = n"
   121 proof (rule subdegreeI)
   122   from assms have "monom 1 n dvd p" by (simp add: monom_1_dvd_iff)
   123   thus zero: "fps_of_poly p $ i = 0" if "i < n" for i
   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)
   128   then obtain k where k: "k \<le> n" "fps_of_poly p $ k \<noteq> 0" 
   129     by (auto simp: monom_1_dvd_iff' less_Suc_eq_le)
   130   with zero[of k] have "k = n" by linarith
   131   with k show "fps_of_poly p $ n \<noteq> 0" by simp
   132 qed
   133 
   134 lemma fps_of_poly_dvd:
   135   assumes "p dvd q"
   136   shows   "fps_of_poly (p :: 'a :: field poly) dvd fps_of_poly q"
   137 proof (cases "p = 0 \<or> q = 0")
   138   case False
   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)
   141 qed (insert assms, auto)
   142 
   143 
   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
   147   fps_of_poly_sum fps_of_poly_sum_list fps_of_poly_prod fps_of_poly_prod_list
   148   fps_of_poly_pCons fps_of_poly_pderiv fps_of_poly_power fps_of_poly_monom
   149   fps_of_poly_divide_numeral
   150 
   151 lemma fps_of_poly_pcompose:
   152   assumes "coeff q 0 = (0 :: 'a :: idom)"
   153   shows   "fps_of_poly (pcompose p q) = fps_compose (fps_of_poly p) (fps_of_poly q)"
   154   using assms by (induction p rule: pCons_induct)
   155                  (auto simp: pcompose_pCons fps_of_poly_simps fps_of_poly_pCons 
   156                              fps_compose_add_distrib fps_compose_mult_distrib)
   157   
   158 lemmas reify_fps_atom =
   159   fps_of_poly_0 fps_of_poly_1' fps_of_poly_numeral' fps_of_poly_const fps_of_poly_X
   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 non-zero 
   165   coefficients and can therefore be written as @{term "fps_of_poly p"} for some 
   166   polynomial \<open>p\<close>.
   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
   202       (Const (@{const_name "fps_of_poly"}, _) $ _) => ct |> Conv.all_conv
   203     | (Const (@{const_name "Groups.plus"}, _) $ _ $ _) => ct |> (
   204         bin then_conv rewr @{thms fps_of_poly_add [symmetric]})
   205     | (Const (@{const_name "Groups.uminus"}, _) $ _) => ct |> (
   206         un then_conv rewr @{thms fps_of_poly_uminus [symmetric]})
   207     | (Const (@{const_name "Groups.minus"}, _) $ _ $ _) => ct |> (
   208         bin then_conv rewr @{thms fps_of_poly_diff [symmetric]})
   209     | (Const (@{const_name "Groups.times"}, _) $ _ $ _) => ct |> (
   210         bin then_conv rewr @{thms fps_of_poly_mult [symmetric]})
   211     | (Const (@{const_name "Rings.divide"}, _) $ _ $ (Const (@{const_name "Num.numeral"}, _) $ _))
   212         => ct |> (Conv.fun_conv (Conv.arg_conv reify_conv)
   213              then_conv rewr @{thms fps_of_poly_divide_numeral [symmetric]})
   214     | (Const (@{const_name "Power.power"}, _) $ Const (@{const_name "X"},_) $ _) => ct |> (
   215         rewr @{thms fps_of_poly_monom' [symmetric]}) 
   216     | (Const (@{const_name "Power.power"}, _) $ _ $ _) => ct |> (
   217         Conv.fun_conv (Conv.arg_conv reify_conv) 
   218         then_conv rewr @{thms fps_of_poly_power [symmetric]})
   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
   228       then_conv Conv.rewr_conv @{thm fps_of_poly_eq_iff[THEN eq_reflection]})
   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 
   238 lemma fps_of_poly_linear: "fps_of_poly [:a,1 :: 'a :: field:] = X + fps_const a"
   239   by simp
   240 
   241 lemma fps_of_poly_linear': "fps_of_poly [:1,a :: 'a :: field:] = 1 + fps_const a * X"
   242   by simp
   243 
   244 lemma fps_of_poly_cutoff [simp]: 
   245   "fps_of_poly (poly_cutoff n p) = fps_cutoff n (fps_of_poly p)"
   246   by (simp add: fps_eq_iff coeff_poly_cutoff)
   247 
   248 lemma fps_of_poly_shift [simp]: "fps_of_poly (poly_shift n p) = fps_shift n (fps_of_poly p)"
   249   by (simp add: fps_eq_iff coeff_poly_shift)
   250 
   251 
   252 definition poly_subdegree :: "'a::zero poly \<Rightarrow> nat" where
   253   "poly_subdegree p = subdegree (fps_of_poly p)"
   254 
   255 lemma coeff_less_poly_subdegree:
   256   "k < poly_subdegree p \<Longrightarrow> coeff p k = 0"
   257   unfolding poly_subdegree_def using nth_less_subdegree_zero[of k "fps_of_poly p"] by simp
   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)
   300     from n_less have "fps_of_poly p $ n = coeffs p ! n"
   301       by (subst coeffs_nth) (simp_all add: degree_eq_length_coeffs)
   302     with nonzero show "fps_of_poly p $ prefix_length (op = 0) (coeffs p) \<noteq> 0"
   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)
   307     finally show "fps_of_poly p $ k = 0"
   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