equal
deleted
inserted
replaced
|
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 |
|
12 up :: (domain) domain (up_integral) |
|
13 |
|
14 consts |
|
15 EVAL2 :: ('a::ringS => 'b) => 'b => 'a up => 'b::ringS |
|
16 EVAL :: 'a => 'a up => 'a |
|
17 |
|
18 defs |
|
19 EVAL2_def "EVAL2 phi a p == SUM (deg p) (%i. phi (coeff i p) * a ^ i)" |
|
20 EVAL_def "EVAL == EVAL2 (%x. x)" |
|
21 |
|
22 end |