src/HOL/Algebra/UnivPoly.thy
changeset 14651 02b8f3bcf7fe
parent 14590 276ef51cedbf
child 14666 65f8680c3f16
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Apr 22 11:00:22 2004 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu Apr 22 11:01:34 2004 +0200
     1.3 @@ -58,18 +58,18 @@
     1.4    monom :: "['a, nat] => 'p"
     1.5    coeff :: "['p, nat] => 'a"
     1.6  
     1.7 -constdefs
     1.8 -  up :: "('a, 'm) ring_scheme => (nat => 'a) set"
     1.9 -  "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound (zero R) n f)}"
    1.10 -  UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
    1.11 +constdefs (structure R)
    1.12 +  up :: "_ => (nat => 'a) set"
    1.13 +  "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero> n f)}"
    1.14 +  UP :: "_ => ('a, nat => 'a) up_ring"
    1.15    "UP R == (|
    1.16      carrier = up R,
    1.17 -    mult = (%p:up R. %q:up R. %n. finsum R (%i. mult R (p i) (q (n-i))) {..n}),
    1.18 -    one = (%i. if i=0 then one R else zero R),
    1.19 -    zero = (%i. zero R),
    1.20 -    add = (%p:up R. %q:up R. %i. add R (p i) (q i)),
    1.21 -    smult = (%a:carrier R. %p:up R. %i. mult R a (p i)),
    1.22 -    monom = (%a:carrier R. %n i. if i=n then a else zero R),
    1.23 +    mult = (%p:up R. %q:up R. %n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)),
    1.24 +    one = (%i. if i=0 then \<one> else \<zero>),
    1.25 +    zero = (%i. \<zero>),
    1.26 +    add = (%p:up R. %q:up R. %i. p i \<oplus> q i),
    1.27 +    smult = (%a:carrier R. %p:up R. %i. a \<otimes> p i),
    1.28 +    monom = (%a:carrier R. %n i. if i=n then a else \<zero>),
    1.29      coeff = (%p:up R. %n. p n) |)"
    1.30  
    1.31  text {*
    1.32 @@ -179,9 +179,8 @@
    1.33  locale UP_domain = UP_cring + "domain" R
    1.34  
    1.35  text {*
    1.36 -  Temporarily declare UP.P\_def as simp rule.
    1.37 -*}
    1.38 -(* TODO: use antiquotation once text (in locale) is supported. *)
    1.39 +  Temporarily declare @{text UP.P_def} as simp rule.
    1.40 +*}  (* TODO: use antiquotation once text (in locale) is supported. *)
    1.41  
    1.42  declare (in UP) P_def [simp]
    1.43  
    1.44 @@ -785,9 +784,9 @@
    1.45  
    1.46  subsection {* The degree function *}
    1.47  
    1.48 -constdefs
    1.49 -  deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
    1.50 -  "deg R p == LEAST n. bound (zero R) n (coeff (UP R) p)"
    1.51 +constdefs (structure R)
    1.52 +  deg :: "[_, nat => 'a] => nat"
    1.53 +  "deg R p == LEAST n. bound \<zero> n (coeff (UP R) p)"
    1.54  
    1.55  lemma (in UP_cring) deg_aboveI:
    1.56    "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n" 
    1.57 @@ -1248,11 +1247,10 @@
    1.58    "(%a. monom P a 0) \<in> ring_hom R P"
    1.59    by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult)
    1.60  
    1.61 -constdefs
    1.62 -  eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
    1.63 -          'a => 'b, 'b, nat => 'a] => 'b"
    1.64 -  "eval R S phi s == (\<lambda>p \<in> carrier (UP R).
    1.65 -    finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p})"
    1.66 +constdefs (structure S)
    1.67 +  eval :: "[_, _, 'a => 'b, 'b, nat => 'a] => 'b"
    1.68 +  "eval R S phi s == \<lambda>p \<in> carrier (UP R).
    1.69 +    \<Oplus>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes> pow S s i"
    1.70  (*
    1.71    "eval R S phi s p == if p \<in> carrier (UP R)
    1.72    then finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p}
    1.73 @@ -1566,5 +1564,4 @@
    1.74  
    1.75  -- {* Calculates @{term "x = 500"} *}
    1.76  
    1.77 -
    1.78  end