# Theory LongDiv

Up to index of Isabelle/HOL/HOL-Algebra

theory LongDiv
imports PolyHomo
uses [LongDiv.ML]
begin

    (*
        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