src/HOL/Algebra/UnivPoly.thy
changeset 35848 5443079512ea
parent 34915 7894c7dab132
child 35849 b5522b51cb1e
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sun Mar 21 15:57:40 2010 +0100
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Sun Mar 21 16:51:37 2010 +0100
     1.3 @@ -54,11 +54,12 @@
     1.4    monom :: "['a, nat] => 'p"
     1.5    coeff :: "['p, nat] => 'a"
     1.6  
     1.7 -definition up :: "('a, 'm) ring_scheme => (nat => 'a) set"
     1.8 -  where up_def: "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
     1.9 +definition
    1.10 +  up :: "('a, 'm) ring_scheme => (nat => 'a) set"
    1.11 +  where "up R = {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
    1.12  
    1.13  definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
    1.14 -  where UP_def: "UP R == (|
    1.15 +  where "UP R = (|
    1.16     carrier = up R,
    1.17     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.18     one = (%i. if i=0 then \<one>\<^bsub>R\<^esub> else \<zero>\<^bsub>R\<^esub>),
    1.19 @@ -711,8 +712,9 @@
    1.20  
    1.21  subsection {* The Degree Function *}
    1.22  
    1.23 -definition deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
    1.24 -  where "deg R p == LEAST n. bound \<zero>\<^bsub>R\<^esub> n (coeff (UP R) p)"
    1.25 +definition
    1.26 +  deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
    1.27 +  where "deg R p = (LEAST n. bound \<zero>\<^bsub>R\<^esub> n (coeff (UP R) p))"
    1.28  
    1.29  context UP_ring
    1.30  begin
    1.31 @@ -1173,8 +1175,8 @@
    1.32  definition
    1.33    eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
    1.34             'a => 'b, 'b, nat => 'a] => 'b"
    1.35 -  where "eval R S phi s == \<lambda>p \<in> carrier (UP R).
    1.36 -    \<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.37 +  where "eval R S phi s = (\<lambda>p \<in> carrier (UP R).
    1.38 +    \<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.39  
    1.40  context UP
    1.41  begin
    1.42 @@ -1854,11 +1856,11 @@
    1.43    by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro
    1.44      ring_hom_cring_axioms.intro UP_cring.intro)
    1.45  
    1.46 -definition  INTEG :: "int ring"
    1.47 -  where INTEG_def: "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
    1.48 +definition
    1.49 +  INTEG :: "int ring"
    1.50 +  where "INTEG = (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
    1.51  
    1.52 -lemma INTEG_cring:
    1.53 -  "cring INTEG"
    1.54 +lemma INTEG_cring: "cring INTEG"
    1.55    by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
    1.56      zadd_zminus_inverse2 zadd_zmult_distrib)
    1.57