1822 lemma inverse_mult_eq_1': |
1822 lemma inverse_mult_eq_1': |
1823 assumes f0: "f$0 \<noteq> (0::'a::field)" |
1823 assumes f0: "f$0 \<noteq> (0::'a::field)" |
1824 shows "f * inverse f = 1" |
1824 shows "f * inverse f = 1" |
1825 by (metis mult.commute inverse_mult_eq_1 f0) |
1825 by (metis mult.commute inverse_mult_eq_1 f0) |
1826 |
1826 |
|
1827 (* FIXME: The last part of this proof should go through by simp once we have a proper |
|
1828 theorem collection for simplifying division on rings *) |
1827 lemma fps_divide_deriv: |
1829 lemma fps_divide_deriv: |
1828 fixes a :: "'a::field fps" |
1830 assumes "b dvd (a :: 'a :: field fps)" |
1829 assumes a0: "b$0 \<noteq> 0" |
1831 shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b^2" |
1830 shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b\<^sup>2" |
1832 proof - |
1831 using fps_inverse_deriv[OF a0] a0 |
1833 have eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b div c" for a b c :: "'a :: field fps" |
1832 by (simp add: fps_divide_unit field_simps |
1834 by (drule sym) (simp add: mult.assoc) |
1833 power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0]) |
1835 from assms have "a = a / b * b" by simp |
1834 |
1836 also have "fps_deriv (a / b * b) = fps_deriv (a / b) * b + a / b * fps_deriv b" by simp |
|
1837 finally have "fps_deriv (a / b) * b^2 = fps_deriv a * b - a * fps_deriv b" using assms |
|
1838 by (simp add: power2_eq_square algebra_simps) |
|
1839 thus ?thesis by (cases "b = 0") (auto simp: eq_divide_imp) |
|
1840 qed |
1835 |
1841 |
1836 lemma fps_inverse_gp': "inverse (Abs_fps (\<lambda>n. 1::'a::field)) = 1 - X" |
1842 lemma fps_inverse_gp': "inverse (Abs_fps (\<lambda>n. 1::'a::field)) = 1 - X" |
1837 by (simp add: fps_inverse_gp fps_eq_iff X_def) |
1843 by (simp add: fps_inverse_gp fps_eq_iff X_def) |
1838 |
1844 |
1839 lemma fps_nth_deriv_X[simp]: "fps_nth_deriv n X = (if n = 0 then X else if n=1 then 1 else 0)" |
1845 lemma fps_nth_deriv_X[simp]: "fps_nth_deriv n X = (if n = 0 then X else if n=1 then 1 else 0)" |