1 (* |
|
2 Instantiate polynomials to form a ring and prove further properties |
|
3 $Id$ |
|
4 Author: Clemens Ballarin, started 22 January 1997 |
|
5 *) |
|
6 |
|
7 (* Properties of *s: |
|
8 Polynomials form a module *) |
|
9 |
|
10 goal UnivPoly.thy "!!a::'a::ring. (a + b) *s p = a *s p + b *s p"; |
|
11 by (rtac up_eqI 1); |
|
12 by (simp_tac (simpset() addsimps [l_distr]) 1); |
|
13 qed "smult_l_distr"; |
|
14 |
|
15 goal UnivPoly.thy "!!a::'a::ring. a *s (p + q) = a *s p + a *s q"; |
|
16 by (rtac up_eqI 1); |
|
17 by (simp_tac (simpset() addsimps [r_distr]) 1); |
|
18 qed "smult_r_distr"; |
|
19 |
|
20 goal UnivPoly.thy "!!a::'a::ring. (a * b) *s p = a *s (b *s p)"; |
|
21 by (rtac up_eqI 1); |
|
22 by (simp_tac (simpset() addsimps [m_assoc]) 1); |
|
23 qed "smult_assoc1"; |
|
24 |
|
25 goal UnivPoly.thy "(<1>::'a::ring) *s p = p"; |
|
26 by (rtac up_eqI 1); |
|
27 by (Simp_tac 1); |
|
28 qed "smult_one"; |
|
29 |
|
30 (* Polynomials form an algebra *) |
|
31 |
|
32 goal UnivPoly.thy "!!a::'a::ring. (a *s p) * q = a *s (p * q)"; |
|
33 by (rtac up_eqI 1); |
|
34 by (simp_tac (simpset() addsimps [SUM_rdistr, m_assoc]) 1); |
|
35 qed "smult_assoc2"; |
|
36 |
|
37 (* the following can be derived from the above ones, |
|
38 for generality reasons, it is therefore done *) |
|
39 |
|
40 Goal "(0::'a::ring) *s p = 0"; |
|
41 by (rtac a_lcancel 1); |
|
42 by (rtac (smult_l_distr RS sym RS trans) 1); |
|
43 by (Simp_tac 1); |
|
44 qed "smult_l_null"; |
|
45 |
|
46 Goal "!!a::'a::ring. a *s 0 = 0"; |
|
47 by (rtac a_lcancel 1); |
|
48 by (rtac (smult_r_distr RS sym RS trans) 1); |
|
49 by (Simp_tac 1); |
|
50 qed "smult_r_null"; |
|
51 |
|
52 Goal "!!a::'a::ring. (-a) *s p = - (a *s p)"; |
|
53 by (rtac a_lcancel 1); |
|
54 by (rtac (r_neg RS sym RSN (2, trans)) 1); |
|
55 by (rtac (smult_l_distr RS sym RS trans) 1); |
|
56 by (simp_tac (simpset() addsimps [smult_l_null, r_neg]) 1); |
|
57 qed "smult_l_minus"; |
|
58 |
|
59 Goal "!!a::'a::ring. a *s (-p) = - (a *s p)"; |
|
60 by (rtac a_lcancel 1); |
|
61 by (rtac (r_neg RS sym RSN (2, trans)) 1); |
|
62 by (rtac (smult_r_distr RS sym RS trans) 1); |
|
63 by (simp_tac (simpset() addsimps [smult_r_null, r_neg]) 1); |
|
64 qed "smult_r_minus"; |
|
65 |
|
66 val smult_minus = [smult_l_minus, smult_r_minus]; |
|
67 |
|
68 Addsimps [smult_one, smult_l_null, smult_r_null]; |
|