src/HOL/Algebra/UnivPoly.thy
 changeset 36096 abc6a2ea4b88 parent 36092 8f1e60d9f7cc parent 35849 b5522b51cb1e child 38131 df8fc03995a4
```     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Apr 02 13:33:48 2010 +0200
1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed Apr 07 19:17:10 2010 +0200
1.3 @@ -1,7 +1,6 @@
1.4 -(*
1.5 -  Title:     HOL/Algebra/UnivPoly.thy
1.6 -  Author:    Clemens Ballarin, started 9 December 1996
1.8 +(*  Title:      HOL/Algebra/UnivPoly.thy
1.9 +    Author:     Clemens Ballarin, started 9 December 1996
1.11
1.12  Contributions, in particular on long division, by Jesus Aransay.
1.13  *)
1.14 @@ -10,7 +9,6 @@
1.15  imports Module RingHom
1.16  begin
1.17
1.18 -
1.19  section {* Univariate Polynomials *}
1.20
1.21  text {*
1.22 @@ -54,11 +52,12 @@
1.23    monom :: "['a, nat] => 'p"
1.24    coeff :: "['p, nat] => 'a"
1.25
1.26 -definition up :: "('a, 'm) ring_scheme => (nat => 'a) set"
1.27 -  where up_def: "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
1.28 +definition
1.29 +  up :: "('a, 'm) ring_scheme => (nat => 'a) set"
1.30 +  where "up R = {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
1.31
1.32  definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
1.33 -  where UP_def: "UP R == (|
1.34 +  where "UP R = (|
1.35     carrier = up R,
1.36     mult = (%p:up R. %q:up R. %n. \<Oplus>\<^bsub>R\<^esub>i \<in> {..n}. p i \<otimes>\<^bsub>R\<^esub> q (n-i)),
1.37     one = (%i. if i=0 then \<one>\<^bsub>R\<^esub> else \<zero>\<^bsub>R\<^esub>),
1.38 @@ -428,7 +427,8 @@
1.39      using l [of "(\<lambda>i. coeff P p i)" "(\<lambda>i. coeff P q i)" "n"] by (simp add: Pi_def m_comm)
1.40  qed (simp_all add: R1 R2)
1.41
1.42 -subsection{*Polynomials over a commutative ring for a commutative ring*}
1.43 +
1.44 +subsection {*Polynomials over a commutative ring for a commutative ring*}
1.45
1.46  theorem UP_cring:
1.47    "cring P" using UP_ring unfolding cring_def by (auto intro!: comm_monoidI UP_m_assoc UP_m_comm)
1.48 @@ -711,8 +711,9 @@
1.49
1.50  subsection {* The Degree Function *}
1.51
1.52 -definition deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
1.53 -  where "deg R p == LEAST n. bound \<zero>\<^bsub>R\<^esub> n (coeff (UP R) p)"
1.54 +definition
1.55 +  deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
1.56 +  where "deg R p = (LEAST n. bound \<zero>\<^bsub>R\<^esub> n (coeff (UP R) p))"
1.57
1.58  context UP_ring
1.59  begin
1.60 @@ -1173,8 +1174,8 @@
1.61  definition
1.62    eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
1.63             'a => 'b, 'b, nat => 'a] => 'b"
1.64 -  where "eval R S phi s == \<lambda>p \<in> carrier (UP R).
1.65 -    \<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i"
1.66 +  where "eval R S phi s = (\<lambda>p \<in> carrier (UP R).
1.67 +    \<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1.68
1.69  context UP
1.70  begin
1.71 @@ -1463,6 +1464,7 @@
1.72  lemma lcoeff_nonzero2: assumes p_in_R: "p \<in> carrier P" and p_not_zero: "p \<noteq> \<zero>\<^bsub>P\<^esub>" shows "lcoeff p \<noteq> \<zero>"
1.73    using lcoeff_nonzero [OF p_not_zero p_in_R] .
1.74
1.75 +
1.76  subsection{*The long division algorithm: some previous facts.*}
1.77
1.78  lemma coeff_minus [simp]:
1.79 @@ -1845,11 +1847,11 @@
1.80    by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro
1.81      ring_hom_cring_axioms.intro UP_cring.intro)
1.82
1.83 -definition  INTEG :: "int ring"
1.84 -  where INTEG_def: "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
1.85 +definition
1.86 +  INTEG :: "int ring"
1.87 +  where "INTEG = (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
1.88
1.89 -lemma INTEG_cring:
1.90 -  "cring INTEG"
1.91 +lemma INTEG_cring: "cring INTEG"
1.92    by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI