(*
Title: HOL/Algebra/UnivPoly.thy
Id: $Id$
Author: Clemens Ballarin, started 9 December 1996
Copyright: Clemens Ballarin
*)
header {* Univariate Polynomials *}
theory UnivPoly imports Module begin
text {*
Polynomials are formalised as modules with additional operations for
extracting coefficients from polynomials and for obtaining monomials
from coefficients and exponents (record @{text "up_ring"}). The
carrier set is a set of bounded functions from Nat to the
coefficient domain. Bounded means that these functions return zero
above a certain bound (the degree). There is a chapter on the
formalisation of polynomials in the PhD thesis \cite{Ballarin:1999},
which was implemented with axiomatic type classes. This was later
ported to Locales.
*}
subsection {* The Constructor for Univariate Polynomials *}
text {*
Functions with finite support.
*}
locale bound =
fixes z :: 'a
and n :: nat
and f :: "nat => 'a"
assumes bound: "!!m. n < m \ f m = z"
declare bound.intro [intro!]
and bound.bound [dest]
lemma bound_below:
assumes bound: "bound z m f" and nonzero: "f n \ z" shows "n \ m"
proof (rule classical)
assume "~ ?thesis"
then have "m < n" by arith
with bound have "f n = z" ..
with nonzero show ?thesis by contradiction
qed
record ('a, 'p) up_ring = "('a, 'p) module" +
monom :: "['a, nat] => 'p"
coeff :: "['p, nat] => 'a"
constdefs (structure R)
up :: "('a, 'm) ring_scheme => (nat => 'a) set"
"up R == {f. f \ UNIV -> carrier R & (EX n. bound \ n f)}"
UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
"UP R == (|
carrier = up R,
mult = (%p:up R. %q:up R. %n. \i \ {..n}. p i \ q (n-i)),
one = (%i. if i=0 then \ else \),
zero = (%i. \),
add = (%p:up R. %q:up R. %i. p i \ q i),
smult = (%a:carrier R. %p:up R. %i. a \ p i),
monom = (%a:carrier R. %n i. if i=n then a else \),
coeff = (%p:up R. %n. p n) |)"
text {*
Properties of the set of polynomials @{term up}.
*}
lemma mem_upI [intro]:
"[| !!n. f n \ carrier R; EX n. bound (zero R) n f |] ==> f \ up R"
by (simp add: up_def Pi_def)
lemma mem_upD [dest]:
"f \ up R ==> f n \ carrier R"
by (simp add: up_def Pi_def)
lemma (in cring) bound_upD [dest]:
"f \ up R ==> EX n. bound \ n f"
by (simp add: up_def)
lemma (in cring) up_one_closed:
"(%n. if n = 0 then \ else \) \ up R"
using up_def by force
lemma (in cring) up_smult_closed:
"[| a \ carrier R; p \ up R |] ==> (%i. a \ p i) \ up R"
by force
lemma (in cring) up_add_closed:
"[| p \ up R; q \ up R |] ==> (%i. p i \ q i) \ up R"
proof
fix n
assume "p \ up R" and "q \ up R"
then show "p n \ q n \ carrier R"
by auto
next
assume UP: "p \ up R" "q \ up R"
show "EX n. bound \ n (%i. p i \ q i)"
proof -
from UP obtain n where boundn: "bound \ n p" by fast
from UP obtain m where boundm: "bound \ m q" by fast
have "bound \ (max n m) (%i. p i \ q i)"
proof
fix i
assume "max n m < i"
with boundn and boundm and UP show "p i \ q i = \" by fastsimp
qed
then show ?thesis ..
qed
qed
lemma (in cring) up_a_inv_closed:
"p \ up R ==> (%i. \ (p i)) \ up R"
proof
assume R: "p \ up R"
then obtain n where "bound \ n p" by auto
then have "bound \ n (%i. \ p i)" by auto
then show "EX n. bound \ n (%i. \ p i)" by auto
qed auto
lemma (in cring) up_mult_closed:
"[| p \ up R; q \ up R |] ==>
(%n. \i \ {..n}. p i \ q (n-i)) \ up R"
proof
fix n
assume "p \ up R" "q \ up R"
then show "(\i \ {..n}. p i \ q (n-i)) \ carrier R"
by (simp add: mem_upD funcsetI)
next
assume UP: "p \ up R" "q \ up R"
show "EX n. bound \ n (%n. \i \ {..n}. p i \ q (n-i))"
proof -
from UP obtain n where boundn: "bound \ n p" by fast
from UP obtain m where boundm: "bound \ m q" by fast
have "bound \ (n + m) (%n. \i \ {..n}. p i \ q (n - i))"
proof
fix k assume bound: "n + m < k"
{
fix i
have "p i \ q (k-i) = \"
proof (cases "n < i")
case True
with boundn have "p i = \" by auto
moreover from UP have "q (k-i) \ carrier R" by auto
ultimately show ?thesis by simp
next
case False
with bound have "m < k-i" by arith
with boundm have "q (k-i) = \" by auto
moreover from UP have "p i \ carrier R" by auto
ultimately show ?thesis by simp
qed
}
then show "(\i \ {..k}. p i \ q (k-i)) = \"
by (simp add: Pi_def)
qed
then show ?thesis by fast
qed
qed
subsection {* Effect of operations on coefficients *}
locale UP = struct R + struct P +
defines P_def: "P == UP R"
locale UP_cring = UP + cring R
locale UP_domain = UP_cring + "domain" R
text {*
Temporarily declare @{thm [locale=UP] P_def} as simp rule.
*}
declare (in UP) P_def [simp]
lemma (in UP_cring) coeff_monom [simp]:
"a \ carrier R ==>
coeff P (monom P a m) n = (if m=n then a else \)"
proof -
assume R: "a \ carrier R"
then have "(%n. if n = m then a else \) \ up R"
using up_def by force
with R show ?thesis by (simp add: UP_def)
qed
lemma (in UP_cring) coeff_zero [simp]:
"coeff P \\<^bsub>P\<^esub> n = \"
by (auto simp add: UP_def)
lemma (in UP_cring) coeff_one [simp]:
"coeff P \\<^bsub>P\<^esub> n = (if n=0 then \ else \)"
using up_one_closed by (simp add: UP_def)
lemma (in UP_cring) coeff_smult [simp]:
"[| a \ carrier R; p \ carrier P |] ==>
coeff P (a \\<^bsub>P\<^esub> p) n = a \ coeff P p n"
by (simp add: UP_def up_smult_closed)
lemma (in UP_cring) coeff_add [simp]:
"[| p \ carrier P; q \ carrier P |] ==>
coeff P (p \\<^bsub>P\<^esub> q) n = coeff P p n \ coeff P q n"
by (simp add: UP_def up_add_closed)
lemma (in UP_cring) coeff_mult [simp]:
"[| p \ carrier P; q \ carrier P |] ==>
coeff P (p \\<^bsub>P\<^esub> q) n = (\i \ {..n}. coeff P p i \ coeff P q (n-i))"
by (simp add: UP_def up_mult_closed)
lemma (in UP) up_eqI:
assumes prem: "!!n. coeff P p n = coeff P q n"
and R: "p \ carrier P" "q \ carrier P"
shows "p = q"
proof
fix x
from prem and R show "p x = q x" by (simp add: UP_def)
qed
subsection {* Polynomials form a commutative ring. *}
text {* Operations are closed over @{term P}. *}
lemma (in UP_cring) UP_mult_closed [simp]:
"[| p \ carrier P; q \ carrier P |] ==> p \\<^bsub>P\<^esub> q \ carrier P"
by (simp add: UP_def up_mult_closed)
lemma (in UP_cring) UP_one_closed [simp]:
"\\<^bsub>P\<^esub> \ carrier P"
by (simp add: UP_def up_one_closed)
lemma (in UP_cring) UP_zero_closed [intro, simp]:
"\\<^bsub>P\<^esub> \ carrier P"
by (auto simp add: UP_def)
lemma (in UP_cring) UP_a_closed [intro, simp]:
"[| p \ carrier P; q \ carrier P |] ==> p \\<^bsub>P\<^esub> q \ carrier P"
by (simp add: UP_def up_add_closed)
lemma (in UP_cring) monom_closed [simp]:
"a \ carrier R ==> monom P a n \ carrier P"
by (auto simp add: UP_def up_def Pi_def)
lemma (in UP_cring) UP_smult_closed [simp]:
"[| a \ carrier R; p \ carrier P |] ==> a \\<^bsub>P\<^esub> p \ carrier P"
by (simp add: UP_def up_smult_closed)
lemma (in UP) coeff_closed [simp]:
"p \ carrier P ==> coeff P p n \ carrier R"
by (auto simp add: UP_def)
declare (in UP) P_def [simp del]
text {* Algebraic ring properties *}
lemma (in UP_cring) UP_a_assoc:
assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P"
shows "(p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r = p \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)"
by (rule up_eqI, simp add: a_assoc R, simp_all add: R)
lemma (in UP_cring) UP_l_zero [simp]:
assumes R: "p \ carrier P"
shows "\\<^bsub>P\<^esub> \\<^bsub>P\<^esub> p = p"
by (rule up_eqI, simp_all add: R)
lemma (in UP_cring) UP_l_neg_ex:
assumes R: "p \ carrier P"
shows "EX q : carrier P. q \\<^bsub>P\<^esub> p = \\<^bsub>P\<^esub>"
proof -
let ?q = "%i. \ (p i)"
from R have closed: "?q \ carrier P"
by (simp add: UP_def P_def up_a_inv_closed)
from R have coeff: "!!n. coeff P ?q n = \ (coeff P p n)"
by (simp add: UP_def P_def up_a_inv_closed)
show ?thesis
proof
show "?q \\<^bsub>P\<^esub> p = \\<^bsub>P\<^esub>"
by (auto intro!: up_eqI simp add: R closed coeff R.l_neg)
qed (rule closed)
qed
lemma (in UP_cring) UP_a_comm:
assumes R: "p \ carrier P" "q \ carrier P"
shows "p \\<^bsub>P\<^esub> q = q \\<^bsub>P\<^esub> p"
by (rule up_eqI, simp add: a_comm R, simp_all add: R)
ML_setup {*
simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
*}
lemma (in UP_cring) UP_m_assoc:
assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P"
shows "(p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r = p \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)"
proof (rule up_eqI)
fix n
{
fix k and a b c :: "nat=>'a"
assume R: "a \ UNIV -> carrier R" "b \ UNIV -> carrier R"
"c \ UNIV -> carrier R"
then have "k <= n ==>
(\j \ {..k}. (\i \ {..j}. a i \ b (j-i)) \ c (n-j)) =
(\j \ {..k}. a j \ (\i \ {..k-j}. b i \ c (n-j-i)))"
(concl is "?eq k")
proof (induct k)
case 0 then show ?case by (simp add: Pi_def m_assoc)
next
case (Suc k)
then have "k <= n" by arith
then have "?eq k" by (rule Suc)
with R show ?case
by (simp cong: finsum_cong
add: Suc_diff_le Pi_def l_distr r_distr m_assoc)
(simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc)
qed
}
with R show "coeff P ((p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r) n = coeff P (p \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)) n"
by (simp add: Pi_def)
qed (simp_all add: R)
ML_setup {*
simpset_ref() := simpset() setsubgoaler asm_simp_tac;
*}
lemma (in UP_cring) UP_l_one [simp]:
assumes R: "p \ carrier P"
shows "\\<^bsub>P\<^esub> \\<^bsub>P\<^esub> p = p"
proof (rule up_eqI)
fix n
show "coeff P (\\<^bsub>P\<^esub> \\<^bsub>P\<^esub> p) n = coeff P p n"
proof (cases n)
case 0 with R show ?thesis by simp
next
case Suc with R show ?thesis
by (simp del: finsum_Suc add: finsum_Suc2 Pi_def)
qed
qed (simp_all add: R)
lemma (in UP_cring) UP_l_distr:
assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P"
shows "(p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r = (p \\<^bsub>P\<^esub> r) \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)"
by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R)
lemma (in UP_cring) UP_m_comm:
assumes R: "p \ carrier P" "q \ carrier P"
shows "p \\<^bsub>P\<^esub> q = q \\<^bsub>P\<^esub> p"
proof (rule up_eqI)
fix n
{
fix k and a b :: "nat=>'a"
assume R: "a \ UNIV -> carrier R" "b \ UNIV -> carrier R"
then have "k <= n ==>
(\i \ {..k}. a i \ b (n-i)) =
(\i \ {..k}. a (k-i) \ b (i+n-k))"
(concl is "?eq k")
proof (induct k)
case 0 then show ?case by (simp add: Pi_def)
next
case (Suc k) then show ?case
by (subst (2) finsum_Suc2) (simp add: Pi_def a_comm)+
qed
}
note l = this
from R show "coeff P (p \\<^bsub>P\<^esub> q) n = coeff P (q \\<^bsub>P\<^esub> p) n"
apply (simp add: Pi_def)
apply (subst l)
apply (auto simp add: Pi_def)
apply (simp add: m_comm)
done
qed (simp_all add: R)
(*
Strange phenomenon in Isar:
theorem (in UP_cring) UP_cring:
"cring P"
proof (rule cringI)
show "abelian_group P" proof (rule abelian_groupI)
fix x y z
assume "x \ carrier P" and "y \ carrier P" and "z \ carrier P"
{
show "x \\<^bsub>P\<^esub> y \ carrier P" sorry
next
show "x \\<^bsub>P\<^esub> y \\<^bsub>P\<^esub> z = x \\<^bsub>P\<^esub> (y \\<^bsub>P\<^esub> z)" sorry
next
show "x \\<^bsub>P\<^esub> y = y \\<^bsub>P\<^esub> x" sorry
next
show "\\<^bsub>P\<^esub> \\<^bsub>P\<^esub> x = x" sorry
next
show "\y\carrier P. y \\<^bsub>P\<^esub> x = \\<^bsub>P\<^esub>" sorry
next
show "\\<^bsub>P\<^esub> \ carrier P" sorry last goal rejected!!!
*)
theorem (in UP_cring) UP_cring:
"cring P"
by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero
UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr)
lemma (in UP_cring) UP_ring: (* preliminary *)
"ring P"
by (auto intro: ring.intro cring.axioms UP_cring)
lemma (in UP_cring) UP_a_inv_closed [intro, simp]:
"p \ carrier P ==> \\<^bsub>P\<^esub> p \ carrier P"
by (rule abelian_group.a_inv_closed
[OF ring.is_abelian_group [OF UP_ring]])
lemma (in UP_cring) coeff_a_inv [simp]:
assumes R: "p \ carrier P"
shows "coeff P (\\<^bsub>P\<^esub> p) n = \ (coeff P p n)"
proof -
from R coeff_closed UP_a_inv_closed have
"coeff P (\\<^bsub>P\<^esub> p) n = \ coeff P p n \ (coeff P p n \ coeff P (\\<^bsub>P\<^esub> p) n)"
by algebra
also from R have "... = \ (coeff P p n)"
by (simp del: coeff_add add: coeff_add [THEN sym]
abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]])
finally show ?thesis .
qed
text {*
Instantiation of lemmas from @{term cring}.
*}
(* TODO: this should be automated with an instantiation command. *)
lemma (in UP_cring) UP_monoid:
"monoid P"
by (fast intro!: cring.is_comm_monoid comm_monoid.axioms monoid.intro
UP_cring)
(* TODO: provide cring.is_monoid *)
lemma (in UP_cring) UP_comm_monoid:
"comm_monoid P"
by (fast intro!: cring.is_comm_monoid UP_cring)
lemma (in UP_cring) UP_abelian_monoid:
"abelian_monoid P"
by (fast intro!: abelian_group.axioms ring.is_abelian_group UP_ring)
lemma (in UP_cring) UP_abelian_group:
"abelian_group P"
by (fast intro!: ring.is_abelian_group UP_ring)
lemmas (in UP_cring) UP_r_one [simp] =
monoid.r_one [OF UP_monoid]
lemmas (in UP_cring) UP_nat_pow_closed [intro, simp] =
monoid.nat_pow_closed [OF UP_monoid]
lemmas (in UP_cring) UP_nat_pow_0 [simp] =
monoid.nat_pow_0 [OF UP_monoid]
lemmas (in UP_cring) UP_nat_pow_Suc [simp] =
monoid.nat_pow_Suc [OF UP_monoid]
lemmas (in UP_cring) UP_nat_pow_one [simp] =
monoid.nat_pow_one [OF UP_monoid]
lemmas (in UP_cring) UP_nat_pow_mult =
monoid.nat_pow_mult [OF UP_monoid]
lemmas (in UP_cring) UP_nat_pow_pow =
monoid.nat_pow_pow [OF UP_monoid]
lemmas (in UP_cring) UP_m_lcomm =
comm_monoid.m_lcomm [OF UP_comm_monoid]
lemmas (in UP_cring) UP_m_ac = UP_m_assoc UP_m_comm UP_m_lcomm
lemmas (in UP_cring) UP_nat_pow_distr =
comm_monoid.nat_pow_distr [OF UP_comm_monoid]
lemmas (in UP_cring) UP_a_lcomm = abelian_monoid.a_lcomm [OF UP_abelian_monoid]
lemmas (in UP_cring) UP_r_zero [simp] =
abelian_monoid.r_zero [OF UP_abelian_monoid]
lemmas (in UP_cring) UP_a_ac = UP_a_assoc UP_a_comm UP_a_lcomm
lemmas (in UP_cring) UP_finsum_empty [simp] =
abelian_monoid.finsum_empty [OF UP_abelian_monoid]
lemmas (in UP_cring) UP_finsum_insert [simp] =
abelian_monoid.finsum_insert [OF UP_abelian_monoid]
lemmas (in UP_cring) UP_finsum_zero [simp] =
abelian_monoid.finsum_zero [OF UP_abelian_monoid]
lemmas (in UP_cring) UP_finsum_closed [simp] =
abelian_monoid.finsum_closed [OF UP_abelian_monoid]
lemmas (in UP_cring) UP_finsum_Un_Int =
abelian_monoid.finsum_Un_Int [OF UP_abelian_monoid]
lemmas (in UP_cring) UP_finsum_Un_disjoint =
abelian_monoid.finsum_Un_disjoint [OF UP_abelian_monoid]
lemmas (in UP_cring) UP_finsum_addf =
abelian_monoid.finsum_addf [OF UP_abelian_monoid]
lemmas (in UP_cring) UP_finsum_cong' =
abelian_monoid.finsum_cong' [OF UP_abelian_monoid]
lemmas (in UP_cring) UP_finsum_0 [simp] =
abelian_monoid.finsum_0 [OF UP_abelian_monoid]
lemmas (in UP_cring) UP_finsum_Suc [simp] =
abelian_monoid.finsum_Suc [OF UP_abelian_monoid]
lemmas (in UP_cring) UP_finsum_Suc2 =
abelian_monoid.finsum_Suc2 [OF UP_abelian_monoid]
lemmas (in UP_cring) UP_finsum_add [simp] =
abelian_monoid.finsum_add [OF UP_abelian_monoid]
lemmas (in UP_cring) UP_finsum_cong =
abelian_monoid.finsum_cong [OF UP_abelian_monoid]
lemmas (in UP_cring) UP_minus_closed [intro, simp] =
abelian_group.minus_closed [OF UP_abelian_group]
lemmas (in UP_cring) UP_a_l_cancel [simp] =
abelian_group.a_l_cancel [OF UP_abelian_group]
lemmas (in UP_cring) UP_a_r_cancel [simp] =
abelian_group.a_r_cancel [OF UP_abelian_group]
lemmas (in UP_cring) UP_l_neg =
abelian_group.l_neg [OF UP_abelian_group]
lemmas (in UP_cring) UP_r_neg =
abelian_group.r_neg [OF UP_abelian_group]
lemmas (in UP_cring) UP_minus_zero [simp] =
abelian_group.minus_zero [OF UP_abelian_group]
lemmas (in UP_cring) UP_minus_minus [simp] =
abelian_group.minus_minus [OF UP_abelian_group]
lemmas (in UP_cring) UP_minus_add =
abelian_group.minus_add [OF UP_abelian_group]
lemmas (in UP_cring) UP_r_neg2 =
abelian_group.r_neg2 [OF UP_abelian_group]
lemmas (in UP_cring) UP_r_neg1 =
abelian_group.r_neg1 [OF UP_abelian_group]
lemmas (in UP_cring) UP_r_distr =
ring.r_distr [OF UP_ring]
lemmas (in UP_cring) UP_l_null [simp] =
ring.l_null [OF UP_ring]
lemmas (in UP_cring) UP_r_null [simp] =
ring.r_null [OF UP_ring]
lemmas (in UP_cring) UP_l_minus =
ring.l_minus [OF UP_ring]
lemmas (in UP_cring) UP_r_minus =
ring.r_minus [OF UP_ring]
lemmas (in UP_cring) UP_finsum_ldistr =
cring.finsum_ldistr [OF UP_cring]
lemmas (in UP_cring) UP_finsum_rdistr =
cring.finsum_rdistr [OF UP_cring]
subsection {* Polynomials form an Algebra *}
lemma (in UP_cring) UP_smult_l_distr:
"[| a \ carrier R; b \ carrier R; p \ carrier P |] ==>
(a \ b) \\<^bsub>P\<^esub> p = a \\<^bsub>P\<^esub> p \\<^bsub>P\<^esub> b \\<^bsub>P\<^esub> p"
by (rule up_eqI) (simp_all add: R.l_distr)
lemma (in UP_cring) UP_smult_r_distr:
"[| a \ carrier R; p \ carrier P; q \ carrier P |] ==>
a \\<^bsub>P\<^esub> (p \\<^bsub>P\<^esub> q) = a \\<^bsub>P\<^esub> p \\<^bsub>P\<^esub> a \