|
7998
|
1 |
(*
|
|
|
2 |
Universal property and evaluation homomorphism of univariate polynomials
|
|
|
3 |
$Id$
|
|
|
4 |
Author: Clemens Ballarin, started 15 April 1997
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
PolyHomo = Degree +
|
|
|
8 |
|
|
|
9 |
(* Instantiate result from Degree.ML *)
|
|
|
10 |
|
|
|
11 |
instance
|
|
11093
|
12 |
up :: (domain) domain (up_one_not_zero, up_integral)
|
|
7998
|
13 |
|
|
|
14 |
consts
|
|
11779
|
15 |
EVAL2 :: "('a::ring => 'b) => 'b => 'a up => 'b::ring"
|
|
|
16 |
EVAL :: "'a::ring => 'a up => 'a"
|
|
7998
|
17 |
|
|
|
18 |
defs
|
|
11093
|
19 |
EVAL2_def "EVAL2 phi a p ==
|
|
|
20 |
setsum (%i. phi (coeff i p) * a ^ i) {..deg p}"
|
|
7998
|
21 |
EVAL_def "EVAL == EVAL2 (%x. x)"
|
|
|
22 |
|
|
|
23 |
end
|