diff -r 19f1f7066917 -r 5443079512ea src/HOL/Algebra/UnivPoly.thy --- a/src/HOL/Algebra/UnivPoly.thy Sun Mar 21 15:57:40 2010 +0100 +++ b/src/HOL/Algebra/UnivPoly.thy Sun Mar 21 16:51:37 2010 +0100 @@ -54,11 +54,12 @@ monom :: "['a, nat] => 'p" coeff :: "['p, nat] => 'a" -definition up :: "('a, 'm) ring_scheme => (nat => 'a) set" - where up_def: "up R == {f. f \ UNIV -> carrier R & (EX n. bound \\<^bsub>R\<^esub> n f)}" +definition + up :: "('a, 'm) ring_scheme => (nat => 'a) set" + where "up R = {f. f \ UNIV -> carrier R & (EX n. bound \\<^bsub>R\<^esub> n f)}" definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring" - where UP_def: "UP R == (| + where "UP R = (| carrier = up R, mult = (%p:up R. %q:up R. %n. \\<^bsub>R\<^esub>i \ {..n}. p i \\<^bsub>R\<^esub> q (n-i)), one = (%i. if i=0 then \\<^bsub>R\<^esub> else \\<^bsub>R\<^esub>), @@ -711,8 +712,9 @@ subsection {* The Degree Function *} -definition deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat" - where "deg R p == LEAST n. bound \\<^bsub>R\<^esub> n (coeff (UP R) p)" +definition + deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat" + where "deg R p = (LEAST n. bound \\<^bsub>R\<^esub> n (coeff (UP R) p))" context UP_ring begin @@ -1173,8 +1175,8 @@ definition eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme, 'a => 'b, 'b, nat => 'a] => 'b" - where "eval R S phi s == \p \ carrier (UP R). - \\<^bsub>S\<^esub>i \ {..deg R p}. phi (coeff (UP R) p i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i" + where "eval R S phi s = (\p \ carrier (UP R). + \\<^bsub>S\<^esub>i \ {..deg R p}. phi (coeff (UP R) p i) \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" context UP begin @@ -1854,11 +1856,11 @@ by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro ring_hom_cring_axioms.intro UP_cring.intro) -definition INTEG :: "int ring" - where INTEG_def: "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)" +definition + INTEG :: "int ring" + where "INTEG = (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)" -lemma INTEG_cring: - "cring INTEG" +lemma INTEG_cring: "cring INTEG" by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI zadd_zminus_inverse2 zadd_zmult_distrib)