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