|
7998
|
1 |
(*
|
|
|
2 |
Univariate Polynomials
|
|
|
3 |
$Id$
|
|
|
4 |
Author: Clemens Ballarin, started 9 December 1996
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
UnivPoly = ProtoPoly +
|
|
|
8 |
|
|
|
9 |
typedef (UP)
|
|
|
10 |
('a) up = "{f :: nat => 'a::ringS. EX n. bound n f}" (UP_witness)
|
|
|
11 |
|
|
|
12 |
instance
|
|
|
13 |
up :: (ringS) ringS
|
|
|
14 |
|
|
|
15 |
consts
|
|
|
16 |
coeff :: [nat, 'a up] => 'a::ringS
|
|
|
17 |
"*s" :: ['a::ringS, 'a up] => 'a up (infixl 70)
|
|
|
18 |
monom :: nat => ('a::ringS) up
|
|
|
19 |
const :: 'a::ringS => 'a up
|
|
|
20 |
|
|
|
21 |
"*X^" :: ['a, nat] => 'a up ("(3_*X^/_)" [71, 71] 70)
|
|
|
22 |
|
|
|
23 |
translations
|
|
|
24 |
"a *X^ n" == "a *s monom n"
|
|
|
25 |
(* this translation is only nice for non-nested polynomials *)
|
|
|
26 |
|
|
|
27 |
defs
|
|
|
28 |
coeff_def "coeff n p == Rep_UP p n"
|
|
|
29 |
up_add_def "p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
|
|
|
30 |
up_smult_def "a *s p == Abs_UP (%n. a * Rep_UP p n)"
|
|
11093
|
31 |
monom_def "monom m == Abs_UP (%n. if m=n then <1> else 0)"
|
|
|
32 |
const_def "const a == Abs_UP (%n. if n=0 then a else 0)"
|
|
|
33 |
up_mult_def "p * q == Abs_UP (%n::nat. setsum
|
|
|
34 |
(%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
|
|
7998
|
35 |
|
|
11093
|
36 |
up_zero_def "0 == Abs_UP (%x. 0)"
|
|
7998
|
37 |
up_one_def "<1> == monom 0"
|
|
|
38 |
up_uminus_def "- p == (-<1>) *s p"
|
|
11093
|
39 |
up_inverse_def "inverse (a::'a::ringS up) == (if a dvd <1> then @x. a*x = <1> else 0)"
|
|
10448
|
40 |
up_divide_def "(a::'a::ringS up) / b == a * inverse b"
|
|
7998
|
41 |
up_power_def "a ^ n == nat_rec (<1>::('a::ringS) up) (%u b. b * a) n"
|
|
|
42 |
end
|
|
|
43 |
|
|
|
44 |
|