src/HOL/Algebra/poly/UnivPoly2.thy

the new subst tactic, by Lucas Dixon

(*
  Title:     Univariate Polynomials
  Id:        $Id$
  Author:    Clemens Ballarin, started 9 December 1996
  Copyright: Clemens Ballarin
*)

header {* Univariate Polynomials *}

theory UnivPoly2
imports "../abstract/Abstract"
begin

(* already proved in Finite_Set.thy

lemma setsum_cong:
  "[| A = B; !!i. i : B ==> f i = g i |] ==> setsum f A = setsum g B"
proof -
  assume prems: "A = B" "!!i. i : B ==> f i = g i"
  show ?thesis
  proof (cases "finite B")
    case True
    then have "!!A. [| A = B; !!i. i : B ==> f i = g i |] ==>
      setsum f A = setsum g B"
    proof induct
      case empty thus ?case by simp
    next
      case insert thus ?case by simp
    qed
    with prems show ?thesis by simp
  next
    case False with prems show ?thesis by (simp add: setsum_def)
  qed
qed
*)

(* Instruct simplifier to simplify assumptions introduced by congs.
   This makes setsum_cong more convenient to use, because assumptions
   like i:{m..n} get simplified (to m <= i & i <= n). *)

declare setsum_cong [cong]

ML_setup {* 
  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
*}

section {* Definition of type up *}

constdefs
  bound  :: "[nat, nat => 'a::zero] => bool"
  "bound n f == (ALL i. n < i --> f i = 0)"

lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f"
proof (unfold bound_def)
qed fast

lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P"
proof (unfold bound_def)
qed fast

lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0"
proof (unfold bound_def)
qed fast

lemma bound_below:
  assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m"
proof (rule classical)
  assume "~ ?thesis"
  then have "m < n" by arith
  with bound have "f n = 0" ..
  with nonzero show ?thesis by contradiction
qed

typedef (UP)
  ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}"
by (rule+)   (* Question: what does trace_rule show??? *)

section {* Constants *}

consts
  coeff  :: "['a up, nat] => ('a::zero)"
  monom  :: "['a::zero, nat] => 'a up"              ("(3_*X^/_)" [71, 71] 70)
  "*s"   :: "['a::{zero, times}, 'a up] => 'a up"   (infixl 70)

defs
  coeff_def: "coeff p n == Rep_UP p n"
  monom_def: "monom a n == Abs_UP (%i. if i=n then a else 0)"
  smult_def: "a *s p == Abs_UP (%i. a * Rep_UP p i)"

lemma coeff_bound_ex: "EX n. bound n (coeff p)"
proof -
  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
  then show ?thesis ..
qed
  
lemma bound_coeff_obtain:
  assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
proof -
  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
  with prem show P .
qed

text {* Ring operations *}

instance up :: (zero) zero ..
instance up :: (one) one ..
instance up :: (plus) plus ..
instance up :: (minus) minus ..
instance up :: (times) times ..
instance up :: (inverse) inverse ..
instance up :: (power) power ..

defs
  up_add_def:	"p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
  up_mult_def:  "p * q == Abs_UP (%n::nat. setsum
		     (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
  up_zero_def:  "0 == monom 0 0"
  up_one_def:   "1 == monom 1 0"
  up_uminus_def:"- p == (- 1) *s p"
                (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
                (* note: - 1 is different from -1; latter is of class number *)

  up_minus_def:   "(a::'a::{plus, minus} up) - b == a + (-b)"
  up_inverse_def: "inverse (a::'a::{zero, one, times, inverse} up) == 
                     (if a dvd 1 then THE x. a*x = 1 else 0)"
  up_divide_def:  "(a::'a::{times, inverse} up) / b == a * inverse b"
  up_power_def:   "(a::'a::{one, times, power} up) ^ n ==
                     nat_rec 1 (%u b. b * a) n"

subsection {* Effect of operations on coefficients *}

lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
proof -
  have "(%n. if n = m then a else 0) : UP"
    using UP_def by force
  from this show ?thesis
    by (simp add: coeff_def monom_def Abs_UP_inverse Rep_UP)
qed

lemma coeff_zero [simp]: "coeff 0 n = 0"
proof (unfold up_zero_def)
qed simp

lemma coeff_one [simp]: "coeff 1 n = (if n=0 then 1 else 0)"
proof (unfold up_one_def)
qed simp

(* term order
lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
proof -
  have "!!f. f : UP ==> (%n. a * f n) : UP"
    by (unfold UP_def) (force simp add: ring_simps)
*)      (* this force step is slow *)
(*  then show ?thesis
    apply (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
qed
*)
lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
proof -
  have "Rep_UP p : UP ==> (%n. a * Rep_UP p n) : UP"
    by (unfold UP_def) (force simp add: ring_simps)
      (* this force step is slow *)
  then show ?thesis
    by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
qed

lemma coeff_add [simp]: "coeff (p+q) n = (coeff p n + coeff q n::'a::ring)"
proof -
  {
    fix f g
    assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
    have "(%i. f i + g i) : UP"
    proof -
      from fup obtain n where boundn: "bound n f"
	by (unfold UP_def) fast
      from gup obtain m where boundm: "bound m g"
	by (unfold UP_def) fast
      have "bound (max n m) (%i. (f i + g i))"
      proof
	fix i
	assume "max n m < i"
	with boundn and boundm show "f i + g i = 0"
          by (fastsimp simp add: ring_simps)
      qed
      then show "(%i. (f i + g i)) : UP"
	by (unfold UP_def) fast
    qed
  }
  then show ?thesis
    by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
qed

lemma coeff_mult [simp]:
  "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
proof -
  {
    fix f g
    assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
    have "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
    proof -
      from fup obtain n where "bound n f"
	by (unfold UP_def) fast
      from gup obtain m where "bound m g"
	by (unfold UP_def) fast
      have "bound (n + m) (%n. setsum (%i. f i * g (n-i)) {..n})"
      proof
	fix k
	assume bound: "n + m < k"
	{
	  fix i
	  have "f i * g (k-i) = 0"
	  proof cases
	    assume "n < i"
	    show ?thesis by (auto! simp add: ring_simps)
	  next
	    assume "~ (n < i)"
	    with bound have "m < k-i" by arith
	    then show ?thesis by (auto! simp add: ring_simps)
	  qed
	}
	then show "setsum (%i. f i * g (k-i)) {..k} = 0"
	  by (simp add: ring_simps)
      qed
      then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
	by (unfold UP_def) fast
    qed
  }
  then show ?thesis
    by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
qed

lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
by (unfold up_uminus_def) (simp add: ring_simps)

(* Other lemmas *)

lemma up_eqI: assumes prem: "(!! n. coeff p n = coeff q n)" shows "p = q"
proof -
  have "p = Abs_UP (%u. Rep_UP p u)" by (simp add: Rep_UP_inverse)
  also from prem have "... = Abs_UP (Rep_UP q)" by (simp only: coeff_def)
  also have "... = q" by (simp add: Rep_UP_inverse)
  finally show ?thesis .
qed

(* ML_setup {* Addsimprocs [ring_simproc] *} *)

instance up :: (ring) ring
proof
  fix p q r :: "'a::ring up"
  fix n
  show "(p + q) + r = p + (q + r)"
    by (rule up_eqI) simp
  show "0 + p = p"
    by (rule up_eqI) simp
  show "(-p) + p = 0"
    by (rule up_eqI) simp
  show "p + q = q + p"
    by (rule up_eqI) simp
  show "(p * q) * r = p * (q * r)"
  proof (rule up_eqI)
    fix n 
    {
      fix k and a b c :: "nat=>'a::ring"
      have "k <= n ==> 
	setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} = 
	setsum (%j. a j * setsum  (%i. b i * c (n-j-i)) {..k-j}) {..k}"
	(is "_ ==> ?eq k")
      proof (induct k)
	case 0 show ?case by simp
      next
	case (Suc k)
	then have "k <= n" by arith
	then have "?eq k" by (rule Suc)
	then show ?case
	  by (simp add: Suc_diff_le natsum_ldistr)
      qed
    }
    then show "coeff ((p * q) * r) n = coeff (p * (q * r)) n"
      by simp
  qed
  show "1 * p = p"
  proof (rule up_eqI)
    fix n
    show "coeff (1 * p) n = coeff p n"
    proof (cases n)
      case 0 then show ?thesis by simp
    next
      case Suc then show ?thesis by (simp del: natsum_Suc add: natsum_Suc2)
    qed
  qed
  show "(p + q) * r = p * r + q * r"
    by (rule up_eqI) simp
  show "p * q = q * p"
  proof (rule up_eqI)
    fix n 
    {
      fix k
      fix a b :: "nat=>'a::ring"
      have "k <= n ==> 
	setsum (%i. a i * b (n-i)) {..k} =
	setsum (%i. a (k-i) * b (i+n-k)) {..k}"
	(is "_ ==> ?eq k")
      proof (induct k)
	case 0 show ?case by simp
      next
	case (Suc k) then show ?case by (subst natsum_Suc2) simp
      qed
    }
    then show "coeff (p * q) n = coeff (q * p) n"
      by simp
  qed

  show "p - q = p + (-q)"
    by (simp add: up_minus_def)
  show "inverse p = (if p dvd 1 then THE x. p*x = 1 else 0)"
    by (simp add: up_inverse_def)
  show "p / q = p * inverse q"
    by (simp add: up_divide_def)
  show "p ^ n = nat_rec 1 (%u b. b * p) n"
    by (simp add: up_power_def)
  qed

(* Further properties of monom *)

lemma monom_zero [simp]:
  "monom 0 n = 0"
  by (simp add: monom_def up_zero_def)
(* term order: application of coeff_mult goes wrong: rule not symmetric
lemma monom_mult_is_smult:
  "monom (a::'a::ring) 0 * p = a *s p"
proof (rule up_eqI)
  fix k
  show "coeff (monom a 0 * p) k = coeff (a *s p) k"
  proof (cases k)
    case 0 then show ?thesis by simp
  next
    case Suc then show ?thesis by simp
  qed
qed
*)
ML_setup {* Delsimprocs [ring_simproc] *}

lemma monom_mult_is_smult:
  "monom (a::'a::ring) 0 * p = a *s p"
proof (rule up_eqI)
  fix k
  have "coeff (p * monom a 0) k = coeff (a *s p) k"
  proof (cases k)
    case 0 then show ?thesis by simp ring
  next
    case Suc then show ?thesis by (simp add: ring_simps) ring
  qed
  then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
qed

ML_setup {* Addsimprocs [ring_simproc] *}

lemma monom_add [simp]:
  "monom (a + b) n = monom (a::'a::ring) n + monom b n"
by (rule up_eqI) simp

lemma monom_mult_smult:
  "monom (a * b) n = a *s monom (b::'a::ring) n"
by (rule up_eqI) simp

lemma monom_uminus [simp]:
  "monom (-a) n = - monom (a::'a::ring) n"
by (rule up_eqI) simp

lemma monom_one [simp]:
  "monom 1 0 = 1"
by (simp add: up_one_def)

lemma monom_inj:
  "(monom a n = monom b n) = (a = b)"
proof
  assume "monom a n = monom b n"
  then have "coeff (monom a n) n = coeff (monom b n) n" by simp
  then show "a = b" by simp
next
  assume "a = b" then show "monom a n = monom b n" by simp
qed

(* Properties of *s:
   Polynomials form a module *)

lemma smult_l_distr:
  "(a + b::'a::ring) *s p = a *s p + b *s p"
by (rule up_eqI) simp

lemma smult_r_distr:
  "(a::'a::ring) *s (p + q) = a *s p + a *s q"
by (rule up_eqI) simp

lemma smult_assoc1:
  "(a * b::'a::ring) *s p = a *s (b *s p)"
by (rule up_eqI) simp

lemma smult_one [simp]:
  "(1::'a::ring) *s p = p"
by (rule up_eqI) simp

(* Polynomials form an algebra *)

ML_setup {* Delsimprocs [ring_simproc] *}

lemma smult_assoc2:
  "(a *s p) * q = (a::'a::ring) *s (p * q)"
by (rule up_eqI) (simp add: natsum_rdistr m_assoc)
(* Simproc fails. *)

ML_setup {* Addsimprocs [ring_simproc] *}

(* the following can be derived from the above ones,
   for generality reasons, it is therefore done *)

lemma smult_l_null [simp]:
  "(0::'a::ring) *s p = 0"
proof -
  fix a
  have "0 *s p = (0 *s p + a *s p) + - (a *s p)" by simp
  also have "... = (0 + a) *s p + - (a *s p)" by (simp only: smult_l_distr)
  also have "... = 0" by simp
  finally show ?thesis .
qed

lemma smult_r_null [simp]:
  "(a::'a::ring) *s 0 = 0";
proof -
  fix p
  have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp
  also have "... = a *s (0 + p) + - (a *s p)" by (simp only: smult_r_distr)
  also have "... = 0" by simp
  finally show ?thesis .
qed

lemma smult_l_minus:
  "(-a::'a::ring) *s p = - (a *s p)"
proof -
  have "(-a) *s p = (-a *s p + a *s p) + -(a *s p)" by simp 
  also have "... = (-a + a) *s p + -(a *s p)" by (simp only: smult_l_distr)
  also have "... = -(a *s p)" by simp
  finally show ?thesis .
qed

lemma smult_r_minus:
  "(a::'a::ring) *s (-p) = - (a *s p)"
proof -
  have "a *s (-p) = (a *s -p + a *s p) + -(a *s p)" by simp
  also have "... = a *s (-p + p) + -(a *s p)" by (simp only: smult_r_distr)
  also have "... = -(a *s p)" by simp
  finally show ?thesis .
qed

section {* The degree function *}

constdefs
  deg :: "('a::zero) up => nat"
  "deg p == LEAST n. bound n (coeff p)"

lemma deg_aboveI:
  "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"
by (unfold deg_def) (fast intro: Least_le)

lemma deg_aboveD:
  assumes prem: "deg p < m" shows "coeff p m = 0"
proof -
  obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain)
  then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI)
  then show "coeff p m = 0" by (rule boundD)
qed

lemma deg_belowI:
  assumes prem: "n ~= 0 ==> coeff p n ~= 0" shows "n <= deg p"
(* logically, this is a slightly stronger version of deg_aboveD *)
proof (cases "n=0")
  case True then show ?thesis by simp
next
  case False then have "coeff p n ~= 0" by (rule prem)
  then have "~ deg p < n" by (fast dest: deg_aboveD)
  then show ?thesis by arith
qed

lemma lcoeff_nonzero_deg:
  assumes deg: "deg p ~= 0" shows "coeff p (deg p) ~= 0"
proof -
  obtain m where "deg p <= m" and m_coeff: "coeff p m ~= 0"
  proof -
    have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
      by arith (* make public?, why does proof not work with "1" *)
    from deg have "deg p - 1 < (LEAST n. bound n (coeff p))"
      by (unfold deg_def) arith
    then have "~ bound (deg p - 1) (coeff p)" by (rule not_less_Least)
    then have "EX m. deg p - 1 < m & coeff p m ~= 0"
      by (unfold bound_def) fast
    then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus)
    then show ?thesis by auto 
  qed
  with deg_belowI have "deg p = m" by fastsimp
  with m_coeff show ?thesis by simp
qed

lemma lcoeff_nonzero_nonzero:
  assumes deg: "deg p = 0" and nonzero: "p ~= 0" shows "coeff p 0 ~= 0"
proof -
  have "EX m. coeff p m ~= 0"
  proof (rule classical)
    assume "~ ?thesis"
    then have "p = 0" by (auto intro: up_eqI)
    with nonzero show ?thesis by contradiction
  qed
  then obtain m where coeff: "coeff p m ~= 0" ..
  then have "m <= deg p" by (rule deg_belowI)
  then have "m = 0" by (simp add: deg)
  with coeff show ?thesis by simp
qed

lemma lcoeff_nonzero:
  "p ~= 0 ==> coeff p (deg p) ~= 0"
proof (cases "deg p = 0")
  case True
  assume "p ~= 0"
  with True show ?thesis by (simp add: lcoeff_nonzero_nonzero)
next
  case False
  assume "p ~= 0"
  with False show ?thesis by (simp add: lcoeff_nonzero_deg)
qed

lemma deg_eqI:
  "[| !!m. n < m ==> coeff p m = 0;
      !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n"
by (fast intro: le_anti_sym deg_aboveI deg_belowI)

(* Degree and polynomial operations *)

lemma deg_add [simp]:
  "deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
proof (cases "deg p <= deg q")
  case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD) 
next
  case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD)
qed

lemma deg_monom_ring:
  "deg (monom a n::'a::ring up) <= n"
by (rule deg_aboveI) simp

lemma deg_monom [simp]:
  "a ~= 0 ==> deg (monom a n::'a::ring up) = n"
by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)

lemma deg_const [simp]:
  "deg (monom (a::'a::ring) 0) = 0"
proof (rule le_anti_sym)
  show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp
next
  show "0 <= deg (monom a 0)" by (rule deg_belowI) simp
qed

lemma deg_zero [simp]:
  "deg 0 = 0"
proof (rule le_anti_sym)
  show "deg 0 <= 0" by (rule deg_aboveI) simp
next
  show "0 <= deg 0" by (rule deg_belowI) simp
qed

lemma deg_one [simp]:
  "deg 1 = 0"
proof (rule le_anti_sym)
  show "deg 1 <= 0" by (rule deg_aboveI) simp
next
  show "0 <= deg 1" by (rule deg_belowI) simp
qed

lemma uminus_monom:
  "!!a::'a::ring. (-a = 0) = (a = 0)"
proof
  fix a::"'a::ring"
  assume "a = 0"
  then show "-a = 0" by simp
next
  fix a::"'a::ring"
  assume "- a = 0"
  then have "-(- a) = 0" by simp
  then show "a = 0" by simp
qed

lemma deg_uminus [simp]:
  "deg (-p::('a::ring) up) = deg p"
proof (rule le_anti_sym)
  show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD)
next
  show "deg p <= deg (- p)" 
  by (simp add: deg_belowI lcoeff_nonzero_deg uminus_monom)
qed

lemma deg_smult_ring:
  "deg ((a::'a::ring) *s p) <= (if a = 0 then 0 else deg p)"
proof (cases "a = 0")
qed (simp add: deg_aboveI deg_aboveD)+

lemma deg_smult [simp]:
  "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)"
proof (rule le_anti_sym)
  show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring)
next
  show "(if a = 0 then 0 else deg p) <= deg (a *s p)"
  proof (cases "a = 0")
  qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff)
qed

lemma deg_mult_ring:
  "deg (p * q::'a::ring up) <= deg p + deg q"
proof (rule deg_aboveI)
  fix m
  assume boundm: "deg p + deg q < m"
  {
    fix k i
    assume boundk: "deg p + deg q < k"
    then have "coeff p i * coeff q (k - i) = 0"
    proof (cases "deg p < i")
      case True then show ?thesis by (simp add: deg_aboveD)
    next
      case False with boundk have "deg q < k - i" by arith
      then show ?thesis by (simp add: deg_aboveD)
    qed
  }
      (* This is similar to bound_mult_zero and deg_above_mult_zero in the old
         proofs. *)
  with boundm show "coeff (p * q) m = 0" by simp
qed

lemma deg_mult [simp]:
  "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q"
proof (rule le_anti_sym)
  show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring)
next
  let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))"
  assume nz: "p ~= 0" "q ~= 0"
  have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
  show "deg p + deg q <= deg (p * q)"
  proof (rule deg_belowI, simp)
    have "setsum ?s {.. deg p + deg q}
      = setsum ?s ({..< deg p} Un {deg p .. deg p + deg q})"
      by (simp only: ivl_disj_un_one)
    also have "... = setsum ?s {deg p .. deg p + deg q}"
      by (simp add: setsum_Un_disjoint ivl_disj_int_one
        setsum_0 deg_aboveD less_add_diff)
    also have "... = setsum ?s ({deg p} Un {deg p <.. deg p + deg q})"
      by (simp only: ivl_disj_un_singleton)
    also have "... = coeff p (deg p) * coeff q (deg q)" 
      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
        setsum_0 deg_aboveD)
    finally have "setsum ?s {.. deg p + deg q} 
      = coeff p (deg p) * coeff q (deg q)" .
    with nz show "setsum ?s {.. deg p + deg q} ~= 0"
      by (simp add: integral_iff lcoeff_nonzero)
    qed
  qed

lemma coeff_natsum:
  "((coeff (setsum p A) k)::'a::ring) = 
   setsum (%i. coeff (p i) k) A"
proof (cases "finite A")
  case True then show ?thesis by induct auto
next
  case False then show ?thesis by (simp add: setsum_def)
qed
(* Instance of a more general result!!! *)

(*
lemma coeff_natsum:
  "((coeff (setsum p {..n::nat}) k)::'a::ring) = 
   setsum (%i. coeff (p i) k) {..n}"
by (induct n) auto
*)

lemma up_repr:
  "setsum (%i. monom (coeff p i) i) {..deg (p::'a::ring up)} = p"
proof (rule up_eqI)
  let ?s = "(%i. monom (coeff p i) i)"
  fix k
  show "coeff (setsum ?s {..deg p}) k = coeff p k"
  proof (cases "k <= deg p")
    case True
    hence "coeff (setsum ?s {..deg p}) k = 
          coeff (setsum ?s ({..k} Un {k<..deg p})) k"
      by (simp only: ivl_disj_un_one)
    also from True
    have "... = coeff (setsum ?s {..k}) k"
      by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2
        setsum_0 coeff_natsum )
    also
    have "... = coeff (setsum ?s ({..<k} Un {k})) k"
      by (simp only: ivl_disj_un_singleton)
    also have "... = coeff p k"
      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
        setsum_0 coeff_natsum deg_aboveD)
    finally show ?thesis .
  next
    case False
    hence "coeff (setsum ?s {..deg p}) k = 
          coeff (setsum ?s ({..<deg p} Un {deg p})) k"
      by (simp only: ivl_disj_un_singleton)
    also from False have "... = coeff p k"
      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
        setsum_0 coeff_natsum deg_aboveD)
    finally show ?thesis .
  qed
qed

lemma up_repr_le:
  "deg (p::'a::ring up) <= n ==> setsum (%i. monom (coeff p i) i) {..n} = p"
proof -
  let ?s = "(%i. monom (coeff p i) i)"
  assume "deg p <= n"
  then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {deg p<..n})"
    by (simp only: ivl_disj_un_one)
  also have "... = setsum ?s {..deg p}"
    by (simp add: setsum_Un_disjoint ivl_disj_int_one
      setsum_0 deg_aboveD)
  also have "... = p" by (rule up_repr)
  finally show ?thesis .
qed

instance up :: ("domain") "domain"
proof
  show "1 ~= (0::'a up)"
  proof (* notI is applied here *)
    assume "1 = (0::'a up)"
    hence "coeff 1 0 = (coeff 0 0::'a)" by simp
    hence "1 = (0::'a)" by simp
    with one_not_zero show "False" by contradiction
  qed
next
  fix p q :: "'a::domain up"
  assume pq: "p * q = 0"
  show "p = 0 | q = 0"
  proof (rule classical)
    assume c: "~ (p = 0 | q = 0)"
    then have "deg p + deg q = deg (p * q)" by simp
    also from pq have "... = 0" by simp
    finally have "deg p + deg q = 0" .
    then have f1: "deg p = 0 & deg q = 0" by simp
    from f1 have "p = setsum (%i. (monom (coeff p i) i)) {..0}"
      by (simp only: up_repr_le)
    also have "... = monom (coeff p 0) 0" by simp
    finally have p: "p = monom (coeff p 0) 0" .
    from f1 have "q = setsum (%i. (monom (coeff q i) i)) {..0}"
      by (simp only: up_repr_le)
    also have "... = monom (coeff q 0) 0" by simp
    finally have q: "q = monom (coeff q 0) 0" .
    have "coeff p 0 * coeff q 0 = coeff (p * q) 0" by simp
    also from pq have "... = 0" by simp
    finally have "coeff p 0 * coeff q 0 = 0" .
    then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff)
    with p q show "p = 0 | q = 0" by fastsimp
  qed
qed

lemma monom_inj_zero:
  "(monom a n = 0) = (a = 0)"
proof -
  have "(monom a n = 0) = (monom a n = monom 0 n)" by simp
  also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero)
  finally show ?thesis .
qed
(* term order: makes this simpler!!!
lemma smult_integral:
  "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast
*)
lemma smult_integral:
  "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero)

end