author | wenzelm |
Sat, 06 Oct 2001 00:02:46 +0200 | |
changeset 11704 | 3c50a2cd6f00 |
parent 11701 | 3d51fbf81c17 |
child 13735 | 7de9342aca7a |
permissions | -rw-r--r-- |
7998 | 1 |
(* |
2 |
Universal property and evaluation homomorphism of univariate polynomials |
|
3 |
$Id$ |
|
4 |
Author: Clemens Ballarin, started 16 April 1997 |
|
5 |
*) |
|
6 |
||
7 |
(* Ring homomorphisms and polynomials *) |
|
8 |
||
9 |
Goal "homo (const::'a::ring=>'a up)"; |
|
10 |
by (auto_tac (claset() addSIs [homoI], simpset())); |
|
11 |
qed "const_homo"; |
|
12 |
||
13 |
Delsimps [const_add, const_mult, const_one, const_zero]; |
|
14 |
Addsimps [const_homo]; |
|
15 |
||
16 |
Goal |
|
17 |
"!!f::'a::ring up=>'b::ring. homo f ==> f (a *s p) = f (const a) * f p"; |
|
18 |
by (asm_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1); |
|
19 |
qed "homo_smult"; |
|
20 |
||
21 |
Addsimps [homo_smult]; |
|
22 |
||
23 |
(* Evaluation homomorphism *) |
|
24 |
||
25 |
Goal |
|
26 |
"!! phi::('a::ring=>'b::ring). homo phi ==> homo (EVAL2 phi a)"; |
|
27 |
by (rtac homoI 1); |
|
28 |
by (rewtac EVAL2_def); |
|
29 |
(* + commutes *) |
|
30 |
(* degree estimations: |
|
31 |
bound of all sums can be extended to max (deg aa) (deg b) *) |
|
32 |
by (res_inst_tac [("m", "deg (aa + b)"), ("n", "max (deg aa) (deg b)")] |
|
33 |
SUM_shrink 1); |
|
34 |
by (rtac deg_add 1); |
|
35 |
by (asm_simp_tac (simpset() delsimps [coeff_add] addsimps [deg_aboveD]) 1); |
|
36 |
by (res_inst_tac [("m", "deg aa"), ("n", "max (deg aa) (deg b)")] |
|
37 |
SUM_shrink 1); |
|
38 |
by (rtac le_maxI1 1); |
|
39 |
by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); |
|
40 |
by (res_inst_tac [("m", "deg b"), ("n", "max (deg aa) (deg b)")] |
|
41 |
SUM_shrink 1); |
|
42 |
by (rtac le_maxI2 1); |
|
43 |
by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); |
|
44 |
(* actual homom property + *) |
|
45 |
by (asm_simp_tac (simpset() addsimps [l_distr, SUM_add]) 1); |
|
46 |
||
47 |
(* * commutes *) |
|
48 |
by (res_inst_tac [("m", "deg (aa * b)"), ("n", "deg aa + deg b")] |
|
49 |
SUM_shrink 1); |
|
50 |
by (rtac deg_mult_ring 1); |
|
51 |
by (asm_simp_tac (simpset() delsimps [coeff_mult] addsimps [deg_aboveD]) 1); |
|
52 |
by (rtac trans 1); |
|
53 |
by (rtac CauchySum 2); |
|
54 |
by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2); |
|
55 |
by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2); |
|
56 |
(* getting a^i and a^(k-i) together is difficult, so we do is manually *) |
|
57 |
by (res_inst_tac [("s", |
|
11093 | 58 |
" setsum \ |
59 |
\ (%k. setsum \ |
|
7998 | 60 |
\ (%i. phi (coeff i aa) * (phi (coeff (k - i) b) * \ |
11093 | 61 |
\ (a ^ i * a ^ (k - i)))) {..k}) \ |
62 |
\ {..deg aa + deg b}")] trans 1); |
|
7998 | 63 |
by (asm_simp_tac (simpset() |
64 |
addsimps [power_mult, leD RS add_diff_inverse, SUM_ldistr]) 1); |
|
65 |
by (simp_tac (simpset() addsimps m_ac) 1); |
|
66 |
by (simp_tac (simpset() addsimps m_ac) 1); |
|
67 |
(* <1> commutes *) |
|
68 |
by (Asm_simp_tac 1); |
|
69 |
qed "EVAL2_homo"; |
|
70 |
||
71 |
Goalw [EVAL2_def] |
|
72 |
"!! phi::'a::ring=>'b::ring. EVAL2 phi a (const b) = phi b"; |
|
73 |
by (Simp_tac 1); |
|
74 |
qed "EVAL2_const"; |
|
75 |
||
76 |
Goalw [EVAL2_def] |
|
11093 | 77 |
"!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1) = a"; |
78 |
(* Must be able to distinguish 0 from <1>, hence 'a::domain *) |
|
7998 | 79 |
by (Asm_simp_tac 1); |
80 |
qed "EVAL2_monom1"; |
|
81 |
||
82 |
Goalw [EVAL2_def] |
|
11093 | 83 |
"!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom n) = a ^ n"; |
7998 | 84 |
by (Simp_tac 1); |
8707 | 85 |
by (case_tac "n" 1); |
86 |
by Auto_tac; |
|
7998 | 87 |
qed "EVAL2_monom"; |
88 |
||
89 |
Goal |
|
90 |
"!! phi::'a::ring=>'b::ring. \ |
|
91 |
\ homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p"; |
|
92 |
by (asm_simp_tac |
|
93 |
(simpset() addsimps [const_mult_is_smult RS sym, EVAL2_homo, EVAL2_const]) 1); |
|
94 |
qed "EVAL2_smult"; |
|
95 |
||
96 |
Goalw [EVAL_def] "!! a::'a::ring. homo (EVAL a)"; |
|
97 |
by (asm_simp_tac (simpset() addsimps [EVAL2_homo, id_homo]) 1); |
|
98 |
qed "EVAL_homo"; |
|
99 |
||
100 |
Goalw [EVAL_def] "!! a::'a::ring. EVAL a (const b) = b"; |
|
101 |
by (asm_simp_tac (simpset() addsimps [EVAL2_const]) 1); |
|
102 |
qed "EVAL_const"; |
|
103 |
||
11093 | 104 |
Goalw [EVAL_def] "!! a::'a::domain. EVAL a (monom n) = a ^ n"; |
7998 | 105 |
by (asm_simp_tac (simpset() addsimps [EVAL2_monom]) 1); |
106 |
qed "EVAL_monom"; |
|
107 |
||
108 |
Goalw [EVAL_def] "!! a::'a::ring. EVAL a (b *s p) = b * EVAL a p"; |
|
109 |
by (asm_simp_tac (simpset() addsimps [EVAL2_smult]) 1); |
|
110 |
qed "EVAL_smult"; |
|
111 |
||
112 |
(* Examples *) |
|
113 |
||
114 |
Goal |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
115 |
"EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c"; |
7998 | 116 |
by (asm_simp_tac (simpset() delsimps [power_Suc] |
117 |
addsimps [EVAL_homo, EVAL_monom, EVAL_smult]) 1); |
|
118 |
result(); |
|
119 |
||
120 |
Goal |
|
11093 | 121 |
"EVAL (y::'a::domain) \ |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
122 |
\ (EVAL (const x) (monom 1 + const (a*X^2 + b*X^1 + c*X^0))) = \ |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
123 |
\ x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)"; |
7998 | 124 |
by (asm_simp_tac (simpset() delsimps [power_Suc] |
125 |
addsimps [EVAL_homo, EVAL_monom, EVAL_smult, EVAL_const]) 1); |
|
126 |
result(); |
|
127 |