Up to index of Isabelle/HOL/HOL-Algebra
theory LongDiv(* Experimental theory: long division of polynomials $Id: LongDiv.thy,v 1.8 2005/09/06 14:59:48 wenzelm Exp $ Author: Clemens Ballarin, started 23 June 1999 *) theory LongDiv imports PolyHomo begin consts lcoeff :: "'a::ring up => 'a" eucl_size :: "'a::ring => nat" defs lcoeff_def: "lcoeff p == coeff p (deg p)" eucl_size_def: "eucl_size p == (if p = 0 then 0 else deg p+1)" lemma SUM_shrink_below_lemma: "!! f::(nat=>'a::ring). (ALL i. i < m --> f i = 0) --> setsum (%i. f (i+m)) {..d} = setsum f {..m+d}" apply (induct_tac d) apply (induct_tac m) apply (simp) apply (force) apply (simp add: ab_semigroup_add_class.add_commute[of m]) done end
lemma SUM_shrink_below_lemma:
(∀i<m. f i = (0::'a)) --> (∑i≤d. f (i + m)) = setsum f {..m + d}
theorem SUM_extend_below:
[| m ≤ n; !!i. i < m ==> f i = (0::'a); P (∑i≤n - m. f (i + m)) |] ==> P (setsum f {..n})
theorem up_repr2D:
[| deg p ≤ n; P (∑i≤n. coeff p i*X^i) |] ==> P p
theorem deg_lcoeff_cancel:
[| deg p ≤ deg r; deg q ≤ deg r; coeff p (deg r) = - coeff q (deg r); deg r ≠ 0 |] ==> deg (p + q) < deg r
theorem deg_lcoeff_cancel2:
[| deg p ≤ deg r; deg q ≤ deg r; p ≠ - q; coeff p (deg r) = - coeff q (deg r) |] ==> deg (p + q) < deg r
theorem long_div_eucl_size:
g ≠ 0 ==> Ex (%(q, r, k). lcoeff g ^ k *s f = q * g + r ∧ eucl_size r < eucl_size g)
theorem long_div_ring:
g ≠ 0 ==> Ex (%(q, r, k). lcoeff g ^ k *s f = q * g + r ∧ (r = 0 ∨ deg r < deg g))
theorem long_div_unit:
[| g ≠ 0; lcoeff g dvd (1::'a) |] ==> Ex (%(q, r). f = q * g + r ∧ (r = 0 ∨ deg r < deg g))
theorem long_div_theorem:
g ≠ 0 ==> Ex (%(q, r). f = q * g + r ∧ (r = 0 ∨ deg r < deg g))
theorem long_div_quo_unique:
[| g ≠ 0; f = q1.0 * g + r1.0; r1.0 = 0 ∨ deg r1.0 < deg g; f = q2.0 * g + r2.0; r2.0 = 0 ∨ deg r2.0 < deg g |] ==> q1.0 = q2.0
theorem long_div_rem_unique:
[| g ≠ 0; f = q1.0 * g + r1.0; r1.0 = 0 ∨ deg r1.0 < deg g; f = q2.0 * g + r2.0; r2.0 = 0 ∨ deg r2.0 < deg g |] ==> r1.0 = r2.0