author eberlm Fri, 17 Jun 2016 11:33:52 +0200 changeset 63319 bc8793d7bd21 parent 63318 008db47be9dc child 63320 b5bbf61b792f
fps_from_poly → fps_of_poly
--- a/src/HOL/Library/Polynomial_FPS.thy	Fri Jun 17 11:33:03 2016 +0200
+++ b/src/HOL/Library/Polynomial_FPS.thy	Fri Jun 17 11:33:52 2016 +0200
@@ -10,159 +10,159 @@
imports Polynomial Formal_Power_Series
begin

-definition fps_from_poly where
-  "fps_from_poly p = Abs_fps (coeff p)"
+definition fps_of_poly where
+  "fps_of_poly p = Abs_fps (coeff p)"

-lemma fps_from_poly_eq_iff: "fps_from_poly p = fps_from_poly q \<longleftrightarrow> p = q"
-  by (simp add: fps_from_poly_def poly_eq_iff fps_eq_iff)
+lemma fps_of_poly_eq_iff: "fps_of_poly p = fps_of_poly q \<longleftrightarrow> p = q"
+  by (simp add: fps_of_poly_def poly_eq_iff fps_eq_iff)

-lemma fps_from_poly_nth [simp]: "fps_from_poly p \$ n = coeff p n"
+lemma fps_of_poly_nth [simp]: "fps_of_poly p \$ n = coeff p n"

-lemma fps_from_poly_const: "fps_from_poly [:c:] = fps_const c"
+lemma fps_of_poly_const: "fps_of_poly [:c:] = fps_const c"
proof (subst fps_eq_iff, clarify)
-  fix n :: nat show "fps_from_poly [:c:] \$ n = fps_const c \$ n"
-    by (cases n) (auto simp: fps_from_poly_def)
+  fix n :: nat show "fps_of_poly [:c:] \$ n = fps_const c \$ n"
+    by (cases n) (auto simp: fps_of_poly_def)
qed

-lemma fps_from_poly_0 [simp]: "fps_from_poly 0 = 0"
-  by (subst fps_const_0_eq_0 [symmetric], subst fps_from_poly_const [symmetric]) simp
+lemma fps_of_poly_0 [simp]: "fps_of_poly 0 = 0"
+  by (subst fps_const_0_eq_0 [symmetric], subst fps_of_poly_const [symmetric]) simp

-lemma fps_from_poly_1 [simp]: "fps_from_poly 1 = 1"
-  by (subst fps_const_1_eq_1 [symmetric], subst fps_from_poly_const [symmetric])
+lemma fps_of_poly_1 [simp]: "fps_of_poly 1 = 1"
+  by (subst fps_const_1_eq_1 [symmetric], subst fps_of_poly_const [symmetric])

-lemma fps_from_poly_1' [simp]: "fps_from_poly [:1:] = 1"
-  by (subst fps_const_1_eq_1 [symmetric], subst fps_from_poly_const [symmetric])
+lemma fps_of_poly_1' [simp]: "fps_of_poly [:1:] = 1"
+  by (subst fps_const_1_eq_1 [symmetric], subst fps_of_poly_const [symmetric])

-lemma fps_from_poly_numeral [simp]: "fps_from_poly (numeral n) = numeral n"
-  by (simp add: numeral_fps_const fps_from_poly_const [symmetric] numeral_poly)
+lemma fps_of_poly_numeral [simp]: "fps_of_poly (numeral n) = numeral n"
+  by (simp add: numeral_fps_const fps_of_poly_const [symmetric] numeral_poly)

-lemma fps_from_poly_numeral' [simp]: "fps_from_poly [:numeral n:] = numeral n"
-  by (simp add: numeral_fps_const fps_from_poly_const [symmetric] numeral_poly)
+lemma fps_of_poly_numeral' [simp]: "fps_of_poly [:numeral n:] = numeral n"
+  by (simp add: numeral_fps_const fps_of_poly_const [symmetric] numeral_poly)

-lemma fps_from_poly_X [simp]: "fps_from_poly [:0, 1:] = X"
-  by (auto simp add: fps_from_poly_def fps_eq_iff coeff_pCons split: nat.split)
+lemma fps_of_poly_X [simp]: "fps_of_poly [:0, 1:] = X"
+  by (auto simp add: fps_of_poly_def fps_eq_iff coeff_pCons split: nat.split)

-lemma fps_from_poly_add: "fps_from_poly (p + q) = fps_from_poly p + fps_from_poly q"
-  by (simp add: fps_from_poly_def plus_poly.rep_eq fps_plus_def)
+lemma fps_of_poly_add: "fps_of_poly (p + q) = fps_of_poly p + fps_of_poly q"
+  by (simp add: fps_of_poly_def plus_poly.rep_eq fps_plus_def)

-lemma fps_from_poly_diff: "fps_from_poly (p - q) = fps_from_poly p - fps_from_poly q"
-  by (simp add: fps_from_poly_def minus_poly.rep_eq fps_minus_def)
+lemma fps_of_poly_diff: "fps_of_poly (p - q) = fps_of_poly p - fps_of_poly q"
+  by (simp add: fps_of_poly_def minus_poly.rep_eq fps_minus_def)

-lemma fps_from_poly_uminus: "fps_from_poly (-p) = -fps_from_poly p"
-  by (simp add: fps_from_poly_def uminus_poly.rep_eq fps_uminus_def)
+lemma fps_of_poly_uminus: "fps_of_poly (-p) = -fps_of_poly p"
+  by (simp add: fps_of_poly_def uminus_poly.rep_eq fps_uminus_def)

-lemma fps_from_poly_mult: "fps_from_poly (p * q) = fps_from_poly p * fps_from_poly q"
-  by (simp add: fps_from_poly_def fps_times_def fps_eq_iff coeff_mult atLeast0AtMost)
+lemma fps_of_poly_mult: "fps_of_poly (p * q) = fps_of_poly p * fps_of_poly q"
+  by (simp add: fps_of_poly_def fps_times_def fps_eq_iff coeff_mult atLeast0AtMost)

-lemma fps_from_poly_smult:
-  "fps_from_poly (smult c p) = fps_const c * fps_from_poly p"
-  using fps_from_poly_mult[of "[:c:]" p] by (simp add: fps_from_poly_mult fps_from_poly_const)
+lemma fps_of_poly_smult:
+  "fps_of_poly (smult c p) = fps_const c * fps_of_poly p"
+  using fps_of_poly_mult[of "[:c:]" p] by (simp add: fps_of_poly_mult fps_of_poly_const)

-lemma fps_from_poly_setsum: "fps_from_poly (setsum f A) = setsum (\<lambda>x. fps_from_poly (f x)) A"
+lemma fps_of_poly_setsum: "fps_of_poly (setsum f A) = setsum (\<lambda>x. fps_of_poly (f x)) A"

-lemma fps_from_poly_listsum: "fps_from_poly (listsum xs) = listsum (map fps_from_poly xs)"
+lemma fps_of_poly_listsum: "fps_of_poly (listsum xs) = listsum (map fps_of_poly xs)"

-lemma fps_from_poly_setprod: "fps_from_poly (setprod f A) = setprod (\<lambda>x. fps_from_poly (f x)) A"
-  by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_from_poly_mult)
+lemma fps_of_poly_setprod: "fps_of_poly (setprod f A) = setprod (\<lambda>x. fps_of_poly (f x)) A"
+  by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_mult)

-lemma fps_from_poly_listprod: "fps_from_poly (listprod xs) = listprod (map fps_from_poly xs)"
-  by (induction xs) (simp_all add: fps_from_poly_mult)
+lemma fps_of_poly_listprod: "fps_of_poly (listprod xs) = listprod (map fps_of_poly xs)"
+  by (induction xs) (simp_all add: fps_of_poly_mult)

-lemma fps_from_poly_pCons:
-  "fps_from_poly (pCons (c :: 'a :: semiring_1) p) = fps_const c + fps_from_poly p * X"
+lemma fps_of_poly_pCons:
+  "fps_of_poly (pCons (c :: 'a :: semiring_1) p) = fps_const c + fps_of_poly p * X"
by (subst fps_mult_X_commute [symmetric], intro fps_ext)
-     (auto simp: fps_from_poly_def coeff_pCons split: nat.split)
+     (auto simp: fps_of_poly_def coeff_pCons split: nat.split)

-lemma fps_from_poly_pderiv: "fps_from_poly (pderiv p) = fps_deriv (fps_from_poly p)"
-  by (intro fps_ext) (simp add: fps_from_poly_nth coeff_pderiv)
+lemma fps_of_poly_pderiv: "fps_of_poly (pderiv p) = fps_deriv (fps_of_poly p)"
+  by (intro fps_ext) (simp add: fps_of_poly_nth coeff_pderiv)

-lemma fps_from_poly_power: "fps_from_poly (p ^ n) = fps_from_poly p ^ n"
-  by (induction n) (simp_all add: fps_from_poly_mult)
+lemma fps_of_poly_power: "fps_of_poly (p ^ n) = fps_of_poly p ^ n"
+  by (induction n) (simp_all add: fps_of_poly_mult)

-lemma fps_from_poly_monom: "fps_from_poly (monom (c :: 'a :: comm_ring_1) n) = fps_const c * X ^ n"
+lemma fps_of_poly_monom: "fps_of_poly (monom (c :: 'a :: comm_ring_1) n) = fps_const c * X ^ n"
by (intro fps_ext) simp_all

-lemma fps_from_poly_monom': "fps_from_poly (monom (1 :: 'a :: comm_ring_1) n) = X ^ n"
+lemma fps_of_poly_monom': "fps_of_poly (monom (1 :: 'a :: comm_ring_1) n) = X ^ n"

-lemma fps_from_poly_div:
+lemma fps_of_poly_div:
assumes "(q :: 'a :: field poly) dvd p"
-  shows   "fps_from_poly (p div q) = fps_from_poly p / fps_from_poly q"
+  shows   "fps_of_poly (p div q) = fps_of_poly p / fps_of_poly q"
proof (cases "q = 0")
case False
-  from False fps_from_poly_eq_iff[of q 0] have nz: "fps_from_poly q \<noteq> 0" by simp
+  from False fps_of_poly_eq_iff[of q 0] have nz: "fps_of_poly q \<noteq> 0" by simp
from assms have "p = (p div q) * q" by simp
-  also have "fps_from_poly \<dots> = fps_from_poly (p div q) * fps_from_poly q"
-  also from nz have "\<dots> / fps_from_poly q = fps_from_poly (p div q)"
-    by (intro div_mult_self2_is_id) (auto simp: fps_from_poly_0)
+  also have "fps_of_poly \<dots> = fps_of_poly (p div q) * fps_of_poly q"
+  also from nz have "\<dots> / fps_of_poly q = fps_of_poly (p div q)"
+    by (intro div_mult_self2_is_id) (auto simp: fps_of_poly_0)
finally show ?thesis ..
qed simp

-lemma fps_from_poly_divide_numeral:
-  "fps_from_poly (smult (inverse (numeral c :: 'a :: field)) p) = fps_from_poly p / numeral c"
+lemma fps_of_poly_divide_numeral:
+  "fps_of_poly (smult (inverse (numeral c :: 'a :: field)) p) = fps_of_poly p / numeral c"
proof -
have "smult (inverse (numeral c)) p = [:inverse (numeral c):] * p" by simp
-  also have "fps_from_poly \<dots> = fps_from_poly p / numeral c"
-    by (subst fps_from_poly_mult) (simp add: numeral_fps_const fps_from_poly_pCons)
+  also have "fps_of_poly \<dots> = fps_of_poly p / numeral c"
+    by (subst fps_of_poly_mult) (simp add: numeral_fps_const fps_of_poly_pCons)
finally show ?thesis by simp
qed

-lemma subdegree_fps_from_poly:
+lemma subdegree_fps_of_poly:
assumes "p \<noteq> 0"
defines "n \<equiv> Polynomial.order 0 p"
-  shows   "subdegree (fps_from_poly p) = n"
+  shows   "subdegree (fps_of_poly p) = n"
proof (rule subdegreeI)
from assms have "monom 1 n dvd p" by (simp add: monom_1_dvd_iff)
-  thus zero: "fps_from_poly p \$ i = 0" if "i < n" for i
+  thus zero: "fps_of_poly p \$ i = 0" if "i < n" for i
using that by (simp add: monom_1_dvd_iff')

from assms have "\<not>monom 1 (Suc n) dvd p"
by (auto simp: monom_1_dvd_iff simp del: power_Suc)
-  then obtain k where "k \<le> n" "fps_from_poly p \$ k \<noteq> 0"
+  then obtain k where "k \<le> n" "fps_of_poly p \$ k \<noteq> 0"
by (auto simp: monom_1_dvd_iff' less_Suc_eq_le)
moreover from this and zero[of k] have "k = n" by linarith
-  ultimately show "fps_from_poly p \$ n \<noteq> 0" by simp
+  ultimately show "fps_of_poly p \$ n \<noteq> 0" by simp
qed

-lemma fps_from_poly_dvd:
+lemma fps_of_poly_dvd:
assumes "p dvd q"
-  shows   "fps_from_poly (p :: 'a :: field poly) dvd fps_from_poly q"
+  shows   "fps_of_poly (p :: 'a :: field poly) dvd fps_of_poly q"
proof (cases "p = 0 \<or> q = 0")
case False
-  with assms fps_from_poly_eq_iff[of p 0] fps_from_poly_eq_iff[of q 0] show ?thesis
-    by (auto simp: fps_dvd_iff subdegree_fps_from_poly dvd_imp_order_le)
+  with assms fps_of_poly_eq_iff[of p 0] fps_of_poly_eq_iff[of q 0] show ?thesis
+    by (auto simp: fps_dvd_iff subdegree_fps_of_poly dvd_imp_order_le)
qed (insert assms, auto)

-lemmas fps_from_poly_simps =
-  fps_from_poly_0 fps_from_poly_1 fps_from_poly_numeral fps_from_poly_const fps_from_poly_X
-  fps_from_poly_add fps_from_poly_diff fps_from_poly_uminus fps_from_poly_mult fps_from_poly_smult
-  fps_from_poly_setsum fps_from_poly_listsum fps_from_poly_setprod fps_from_poly_listprod
-  fps_from_poly_pCons fps_from_poly_pderiv fps_from_poly_power fps_from_poly_monom
-  fps_from_poly_divide_numeral
+lemmas fps_of_poly_simps =
+  fps_of_poly_0 fps_of_poly_1 fps_of_poly_numeral fps_of_poly_const fps_of_poly_X
+  fps_of_poly_add fps_of_poly_diff fps_of_poly_uminus fps_of_poly_mult fps_of_poly_smult
+  fps_of_poly_setsum fps_of_poly_listsum fps_of_poly_setprod fps_of_poly_listprod
+  fps_of_poly_pCons fps_of_poly_pderiv fps_of_poly_power fps_of_poly_monom
+  fps_of_poly_divide_numeral

-lemma fps_from_poly_pcompose:
+lemma fps_of_poly_pcompose:
assumes "coeff q 0 = (0 :: 'a :: idom)"
-  shows   "fps_from_poly (pcompose p q) = fps_compose (fps_from_poly p) (fps_from_poly q)"
+  shows   "fps_of_poly (pcompose p q) = fps_compose (fps_of_poly p) (fps_of_poly q)"
using assms by (induction p rule: pCons_induct)
-                 (auto simp: pcompose_pCons fps_from_poly_simps fps_from_poly_pCons
+                 (auto simp: pcompose_pCons fps_of_poly_simps fps_of_poly_pCons

lemmas reify_fps_atom =
-  fps_from_poly_0 fps_from_poly_1' fps_from_poly_numeral' fps_from_poly_const fps_from_poly_X
+  fps_of_poly_0 fps_of_poly_1' fps_of_poly_numeral' fps_of_poly_const fps_of_poly_X

text \<open>
The following simproc can reduce the equality of two polynomial FPSs two equality of the
respective polynomials. A polynomial FPS is one that only has finitely many non-zero
-  coefficients and can therefore be written as @{term "fps_from_poly p"} for some
+  coefficients and can therefore be written as @{term "fps_of_poly p"} for some
polynomial @{text "p"}.

This may sound trivial, but it covers a number of annoying side conditions like
@@ -199,23 +199,23 @@
val bin = Conv.binop_conv reify_conv
in
case Thm.term_of ct of
-      (Const (@{const_name "fps_from_poly"}, _) \$ _) => ct |> Conv.all_conv
+      (Const (@{const_name "fps_of_poly"}, _) \$ _) => ct |> Conv.all_conv
| (Const (@{const_name "Groups.plus"}, _) \$ _ \$ _) => ct |> (
-        bin then_conv rewr @{thms fps_from_poly_add [symmetric]})
+        bin then_conv rewr @{thms fps_of_poly_add [symmetric]})
| (Const (@{const_name "Groups.uminus"}, _) \$ _) => ct |> (
-        un then_conv rewr @{thms fps_from_poly_uminus [symmetric]})
+        un then_conv rewr @{thms fps_of_poly_uminus [symmetric]})
| (Const (@{const_name "Groups.minus"}, _) \$ _ \$ _) => ct |> (
-        bin then_conv rewr @{thms fps_from_poly_diff [symmetric]})
+        bin then_conv rewr @{thms fps_of_poly_diff [symmetric]})
| (Const (@{const_name "Groups.times"}, _) \$ _ \$ _) => ct |> (
-        bin then_conv rewr @{thms fps_from_poly_mult [symmetric]})
+        bin then_conv rewr @{thms fps_of_poly_mult [symmetric]})
| (Const (@{const_name "Rings.divide"}, _) \$ _ \$ (Const (@{const_name "Num.numeral"}, _) \$ _))
=> ct |> (Conv.fun_conv (Conv.arg_conv reify_conv)
-             then_conv rewr @{thms fps_from_poly_divide_numeral [symmetric]})
+             then_conv rewr @{thms fps_of_poly_divide_numeral [symmetric]})
| (Const (@{const_name "Power.power"}, _) \$ Const (@{const_name "X"},_) \$ _) => ct |> (
-        rewr @{thms fps_from_poly_monom' [symmetric]})
+        rewr @{thms fps_of_poly_monom' [symmetric]})
| (Const (@{const_name "Power.power"}, _) \$ _ \$ _) => ct |> (
Conv.fun_conv (Conv.arg_conv reify_conv)
-        then_conv rewr @{thms fps_from_poly_power [symmetric]})
+        then_conv rewr @{thms fps_of_poly_power [symmetric]})
| _ => ct |> (
rewr @{thms reify_fps_atom [symmetric]})
end
@@ -225,7 +225,7 @@
case Thm.term_of ct of
(Const (@{const_name "HOL.eq"}, _) \$ _ \$ _) => ct |> (
Conv.binop_conv reify_conv
-      then_conv Conv.rewr_conv @{thm fps_from_poly_eq_iff[THEN eq_reflection]})
+      then_conv Conv.rewr_conv @{thm fps_of_poly_eq_iff[THEN eq_reflection]})
| _ => raise CTERM ("poly_fps_eq_conv", [ct])

val eq_simproc = try eq_conv
@@ -235,26 +235,26 @@

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

-lemma fps_from_poly_linear: "fps_from_poly [:a,1 :: 'a :: field:] = X + fps_const a"
+lemma fps_of_poly_linear: "fps_of_poly [:a,1 :: 'a :: field:] = X + fps_const a"
by simp

-lemma fps_from_poly_linear': "fps_from_poly [:1,a :: 'a :: field:] = 1 + fps_const a * X"
+lemma fps_of_poly_linear': "fps_of_poly [:1,a :: 'a :: field:] = 1 + fps_const a * X"
by simp

-lemma fps_from_poly_cutoff [simp]:
-  "fps_from_poly (poly_cutoff n p) = fps_cutoff n (fps_from_poly p)"
+lemma fps_of_poly_cutoff [simp]:
+  "fps_of_poly (poly_cutoff n p) = fps_cutoff n (fps_of_poly p)"

-lemma fps_from_poly_shift [simp]: "fps_from_poly (poly_shift n p) = fps_shift n (fps_from_poly p)"
+lemma fps_of_poly_shift [simp]: "fps_of_poly (poly_shift n p) = fps_shift n (fps_of_poly p)"

definition poly_subdegree :: "'a::zero poly \<Rightarrow> nat" where
-  "poly_subdegree p = subdegree (fps_from_poly p)"
+  "poly_subdegree p = subdegree (fps_of_poly p)"

lemma coeff_less_poly_subdegree:
"k < poly_subdegree p \<Longrightarrow> coeff p k = 0"
-  unfolding poly_subdegree_def using nth_less_subdegree_zero[of k "fps_from_poly p"] by simp
+  unfolding poly_subdegree_def using nth_less_subdegree_zero[of k "fps_of_poly p"] by simp

(* TODO: Move ? *)
definition prefix_length :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat" where
@@ -297,14 +297,14 @@
unfolding n_def by (auto intro!: prefix_length_less_length nth_prefix_length)
show ?thesis unfolding poly_subdegree_def
proof (intro subdegreeI)
-    from n_less have "fps_from_poly p \$ n = coeffs p ! n"
+    from n_less have "fps_of_poly p \$ n = coeffs p ! n"
by (subst coeffs_nth) (simp_all add: degree_eq_length_coeffs)
-    with nonzero show "fps_from_poly p \$ prefix_length (op = 0) (coeffs p) \<noteq> 0"
+    with nonzero show "fps_of_poly p \$ prefix_length (op = 0) (coeffs p) \<noteq> 0"
unfolding n_def by simp
next
fix k assume A: "k < prefix_length (op = 0) (coeffs p)"
also have "\<dots> \<le> length (coeffs p)" by (rule prefix_length_le_length)
-    finally show "fps_from_poly p \$ k = 0"
+    finally show "fps_of_poly p \$ k = 0"
using nth_less_prefix_length[OF A]