# HG changeset patch # User eberlm # Date 1466156032 -7200 # Node ID bc8793d7bd217972e32648b09c965cc61bfaaa00 # Parent 008db47be9dce9b3dd0774bcac5e9cc995494476 fps_from_poly → fps_of_poly diff -r 008db47be9dc -r bc8793d7bd21 src/HOL/Library/Polynomial_FPS.thy --- 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 \ 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 \ 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" - by (simp add: fps_from_poly_def) +lemma fps_of_poly_nth [simp]: "fps_of_poly p $ n = coeff p n" + by (simp add: fps_of_poly_def) -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]) (simp add: one_poly_def) -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]) (simp add: one_poly_def) -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 (\x. fps_from_poly (f x)) A" - by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_from_poly_add) +lemma fps_of_poly_setsum: "fps_of_poly (setsum f A) = setsum (\x. fps_of_poly (f x)) A" + by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_add) -lemma fps_from_poly_listsum: "fps_from_poly (listsum xs) = listsum (map fps_from_poly xs)" - by (induction xs) (simp_all add: fps_from_poly_add) +lemma fps_of_poly_listsum: "fps_of_poly (listsum xs) = listsum (map fps_of_poly xs)" + by (induction xs) (simp_all add: fps_of_poly_add) -lemma fps_from_poly_setprod: "fps_from_poly (setprod f A) = setprod (\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 (\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" - by (simp add: fps_from_poly_monom) +lemma fps_of_poly_monom': "fps_of_poly (monom (1 :: 'a :: comm_ring_1) n) = X ^ n" + by (simp add: fps_of_poly_monom) -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 \ 0" by simp + from False fps_of_poly_eq_iff[of q 0] have nz: "fps_of_poly q \ 0" by simp from assms have "p = (p div q) * q" by simp - also have "fps_from_poly \ = fps_from_poly (p div q) * fps_from_poly q" - by (simp add: fps_from_poly_mult) - also from nz have "\ / 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 \ = fps_of_poly (p div q) * fps_of_poly q" + by (simp add: fps_of_poly_mult) + also from nz have "\ / 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 \ = 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 \ = 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 \ 0" defines "n \ 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 "\monom 1 (Suc n) dvd p" by (auto simp: monom_1_dvd_iff simp del: power_Suc) - then obtain k where "k \ n" "fps_from_poly p $ k \ 0" + then obtain k where "k \ n" "fps_of_poly p $ k \ 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 \ 0" by simp + ultimately show "fps_of_poly p $ n \ 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 \ 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 fps_compose_add_distrib fps_compose_mult_distrib) 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 \ 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") = \K (K Poly_Fps.eq_simproc)\ -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)" by (simp add: fps_eq_iff coeff_poly_cutoff) -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)" by (simp add: fps_eq_iff coeff_poly_shift) definition poly_subdegree :: "'a::zero poly \ 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 \ 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 \ bool) \ 'a list \ 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) \ 0" + with nonzero show "fps_of_poly p $ prefix_length (op = 0) (coeffs p) \ 0" unfolding n_def by simp next fix k assume A: "k < prefix_length (op = 0) (coeffs p)" also have "\ \ 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] by (simp add: coeffs_nth degree_eq_length_coeffs) qed