summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | eberlm |

Mon, 07 Dec 2015 16:06:49 +0100 | |

changeset 61804 | 67381557cee8 |

parent 61802 | 1d81de0bddc4 |

child 61805 | 5d2ade78e002 |

Generalised derivative rule for division on formal power series

--- a/src/HOL/Library/Formal_Power_Series.thy Mon Dec 07 15:20:06 2015 +0100 +++ b/src/HOL/Library/Formal_Power_Series.thy Mon Dec 07 16:06:49 2015 +0100 @@ -1824,14 +1824,20 @@ shows "f * inverse f = 1" by (metis mult.commute inverse_mult_eq_1 f0) +(* FIXME: The last part of this proof should go through by simp once we have a proper + theorem collection for simplifying division on rings *) lemma fps_divide_deriv: - fixes a :: "'a::field fps" - assumes a0: "b$0 \<noteq> 0" - shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b\<^sup>2" - using fps_inverse_deriv[OF a0] a0 - by (simp add: fps_divide_unit field_simps - power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0]) - + assumes "b dvd (a :: 'a :: field fps)" + shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b^2" +proof - + have eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b div c" for a b c :: "'a :: field fps" + by (drule sym) (simp add: mult.assoc) + from assms have "a = a / b * b" by simp + also have "fps_deriv (a / b * b) = fps_deriv (a / b) * b + a / b * fps_deriv b" by simp + finally have "fps_deriv (a / b) * b^2 = fps_deriv a * b - a * fps_deriv b" using assms + by (simp add: power2_eq_square algebra_simps) + thus ?thesis by (cases "b = 0") (auto simp: eq_divide_imp) +qed lemma fps_inverse_gp': "inverse (Abs_fps (\<lambda>n. 1::'a::field)) = 1 - X" by (simp add: fps_inverse_gp fps_eq_iff X_def)