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.7 -  Copyright: Clemens Ballarin
     1.8 +(*  Title:      HOL/Algebra/UnivPoly.thy
     1.9 +    Author:     Clemens Ballarin, started 9 December 1996
    1.10 +    Copyright:  Clemens Ballarin
    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
    1.93      zadd_zminus_inverse2 zadd_zmult_distrib)
    1.94