1 (* |
|
2 Universal property and evaluation homomorphism of univariate polynomials |
|
3 $Id$ |
|
4 Author: Clemens Ballarin, started 16 April 1997 |
|
5 *) |
|
6 |
|
7 (* Summation result for tactic-style proofs *) |
|
8 |
|
9 val natsum_add = thm "natsum_add"; |
|
10 val natsum_ldistr = thm "natsum_ldistr"; |
|
11 val natsum_rdistr = thm "natsum_rdistr"; |
|
12 |
|
13 Goal |
|
14 "!! f::(nat=>'a::ring). \ |
|
15 \ m <= n & (ALL i. m < i & i <= n --> f i = 0) --> \ |
|
16 \ setsum f {..m} = setsum f {..n}"; |
|
17 by (induct_tac "n" 1); |
|
18 (* Base case *) |
|
19 by (Simp_tac 1); |
|
20 (* Induction step *) |
|
21 by (case_tac "m <= n" 1); |
|
22 by Auto_tac; |
|
23 by (subgoal_tac "m = Suc n" 1); |
|
24 by (Asm_simp_tac 1); |
|
25 by (fast_arith_tac 1); |
|
26 val SUM_shrink_lemma = result(); |
|
27 |
|
28 Goal |
|
29 "!! f::(nat=>'a::ring). \ |
|
30 \ [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..n}) |] \ |
|
31 \ ==> P (setsum f {..m})"; |
|
32 by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1); |
|
33 by (Asm_full_simp_tac 1); |
|
34 qed "SUM_shrink"; |
|
35 |
|
36 Goal |
|
37 "!! f::(nat=>'a::ring). \ |
|
38 \ [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..m}) |] \ |
|
39 \ ==> P (setsum f {..n})"; |
|
40 by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1); |
|
41 by (Asm_full_simp_tac 1); |
|
42 qed "SUM_extend"; |
|
43 |
|
44 Goal |
|
45 "!!f::nat=>'a::ring. j <= n + m --> \ |
|
46 \ setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..j} = \ |
|
47 \ setsum (%k. setsum (%i. f k * g i) {..j - k}) {..j}"; |
|
48 by (induct_tac "j" 1); |
|
49 (* Base case *) |
|
50 by (Simp_tac 1); |
|
51 (* Induction step *) |
|
52 by (simp_tac (simpset() addsimps [Suc_diff_le, natsum_add]) 1); |
|
53 (* |
|
54 by (asm_simp_tac (simpset() addsimps a_ac) 1); |
|
55 *) |
|
56 by (Asm_simp_tac 1); |
|
57 val DiagSum_lemma = result(); |
|
58 |
|
59 Goal |
|
60 "!!f::nat=>'a::ring. \ |
|
61 \ setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..n + m} = \ |
|
62 \ setsum (%k. setsum (%i. f k * g i) {..n + m - k}) {..n + m}"; |
|
63 by (rtac (DiagSum_lemma RS mp) 1); |
|
64 by (rtac le_refl 1); |
|
65 qed "DiagSum"; |
|
66 |
|
67 Goal |
|
68 "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==> \ |
|
69 \ setsum (%k. setsum (%i. f i * g (k-i)) {..k}) {..n + m} = \ |
|
70 \ setsum f {..n} * setsum g {..m}"; |
|
71 by (simp_tac (simpset() addsimps [natsum_ldistr, DiagSum]) 1); |
|
72 (* SUM_rdistr must be applied after SUM_ldistr ! *) |
|
73 by (simp_tac (simpset() addsimps [natsum_rdistr]) 1); |
|
74 by (res_inst_tac [("m", "n"), ("n", "n+m")] SUM_extend 1); |
|
75 by (rtac le_add1 1); |
|
76 by (Force_tac 1); |
|
77 by (rtac (thm "natsum_cong") 1); |
|
78 by (rtac refl 1); |
|
79 by (res_inst_tac [("m", "m"), ("n", "n+m-i")] SUM_shrink 1); |
|
80 by (asm_simp_tac (simpset() addsimps [le_add_diff]) 1); |
|
81 by Auto_tac; |
|
82 qed "CauchySum"; |
|
83 |
|
84 (* Ring homomorphisms and polynomials *) |
|
85 (* |
|
86 Goal "homo (const::'a::ring=>'a up)"; |
|
87 by (auto_tac (claset() addSIs [homoI], simpset())); |
|
88 qed "const_homo"; |
|
89 |
|
90 Delsimps [const_add, const_mult, const_one, const_zero]; |
|
91 Addsimps [const_homo]; |
|
92 |
|
93 Goal |
|
94 "!!f::'a::ring up=>'b::ring. homo f ==> f (a *s p) = f (const a) * f p"; |
|
95 by (asm_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1); |
|
96 qed "homo_smult"; |
|
97 |
|
98 Addsimps [homo_smult]; |
|
99 *) |
|
100 |
|
101 val deg_add = thm "deg_add"; |
|
102 val deg_mult_ring = thm "deg_mult_ring"; |
|
103 val deg_aboveD = thm "deg_aboveD"; |
|
104 val coeff_add = thm "coeff_add"; |
|
105 val coeff_mult = thm "coeff_mult"; |
|
106 val boundI = thm "boundI"; |
|
107 val monom_mult_is_smult = thm "monom_mult_is_smult"; |
|
108 |
|
109 (* Evaluation homomorphism *) |
|
110 |
|
111 Goal |
|
112 "!! phi::('a::ring=>'b::ring). homo phi ==> homo (EVAL2 phi a)"; |
|
113 by (rtac homoI 1); |
|
114 by (rewtac (thm "EVAL2_def")); |
|
115 (* + commutes *) |
|
116 (* degree estimations: |
|
117 bound of all sums can be extended to max (deg aa) (deg b) *) |
|
118 by (res_inst_tac [("m", "deg (aa + b)"), ("n", "max (deg aa) (deg b)")] |
|
119 SUM_shrink 1); |
|
120 by (rtac deg_add 1); |
|
121 by (asm_simp_tac (simpset() delsimps [coeff_add] addsimps [deg_aboveD]) 1); |
|
122 by (res_inst_tac [("m", "deg aa"), ("n", "max (deg aa) (deg b)")] |
|
123 SUM_shrink 1); |
|
124 by (rtac le_maxI1 1); |
|
125 by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); |
|
126 by (res_inst_tac [("m", "deg b"), ("n", "max (deg aa) (deg b)")] |
|
127 SUM_shrink 1); |
|
128 by (rtac le_maxI2 1); |
|
129 by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); |
|
130 (* actual homom property + *) |
|
131 by (asm_simp_tac (simpset() addsimps [l_distr, natsum_add]) 1); |
|
132 |
|
133 (* * commutes *) |
|
134 by (res_inst_tac [("m", "deg (aa * b)"), ("n", "deg aa + deg b")] |
|
135 SUM_shrink 1); |
|
136 by (rtac deg_mult_ring 1); |
|
137 by (asm_simp_tac (simpset() delsimps [coeff_mult] addsimps [deg_aboveD]) 1); |
|
138 by (rtac trans 1); |
|
139 by (rtac CauchySum 2); |
|
140 by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2); |
|
141 by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2); |
|
142 (* getting a^i and a^(k-i) together is difficult, so we do it manually *) |
|
143 by (res_inst_tac [("s", |
|
144 " setsum \ |
|
145 \ (%k. setsum \ |
|
146 \ (%i. phi (coeff aa i) * (phi (coeff b (k - i)) * \ |
|
147 \ (a ^ i * a ^ (k - i)))) {..k}) \ |
|
148 \ {..deg aa + deg b}")] trans 1); |
|
149 by (asm_simp_tac (simpset() |
|
150 addsimps [power_mult, leD RS add_diff_inverse, natsum_ldistr]) 1); |
|
151 by (Simp_tac 1); |
|
152 (* 1 commutes *) |
|
153 by (Asm_simp_tac 1); |
|
154 qed "EVAL2_homo"; |
|
155 |
|
156 Goalw [thm "EVAL2_def"] |
|
157 "!! phi::'a::ring=>'b::ring. EVAL2 phi a (monom b 0) = phi b"; |
|
158 by (Simp_tac 1); |
|
159 qed "EVAL2_const"; |
|
160 |
|
161 Goalw [thm "EVAL2_def"] |
|
162 "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 1) = a"; |
|
163 (* Must be able to distinguish 0 from 1, hence 'a::domain *) |
|
164 by (Asm_simp_tac 1); |
|
165 qed "EVAL2_monom1"; |
|
166 |
|
167 Goalw [thm "EVAL2_def"] |
|
168 "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 n) = a ^ n"; |
|
169 by (Simp_tac 1); |
|
170 by (case_tac "n" 1); |
|
171 by Auto_tac; |
|
172 qed "EVAL2_monom"; |
|
173 |
|
174 Goal |
|
175 "!! phi::'a::ring=>'b::ring. \ |
|
176 \ homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p"; |
|
177 by (asm_simp_tac (simpset() |
|
178 addsimps [monom_mult_is_smult RS sym, EVAL2_homo, EVAL2_const]) 1); |
|
179 qed "EVAL2_smult"; |
|
180 |
|
181 val up_eqI = thm "up_eqI"; |
|
182 |
|
183 Goal "monom (a::'a::ring) n = monom a 0 * monom 1 n"; |
|
184 by (simp_tac (simpset() addsimps [monom_mult_is_smult]) 1); |
|
185 by (rtac up_eqI 1); |
|
186 by (Simp_tac 1); |
|
187 qed "monom_decomp"; |
|
188 |
|
189 Goal |
|
190 "!! phi::'a::domain=>'b::ring. \ |
|
191 \ homo phi ==> EVAL2 phi a (monom b n) = phi b * a ^ n"; |
|
192 by (stac monom_decomp 1); |
|
193 by (asm_simp_tac (simpset() |
|
194 addsimps [EVAL2_homo, EVAL2_const, EVAL2_monom]) 1); |
|
195 qed "EVAL2_monom_n"; |
|
196 |
|
197 Goalw [thm "EVAL_def"] "!! a::'a::ring. homo (EVAL a)"; |
|
198 by (asm_simp_tac (simpset() addsimps [EVAL2_homo]) 1); |
|
199 qed "EVAL_homo"; |
|
200 |
|
201 Goalw [thm "EVAL_def"] "!! a::'a::ring. EVAL a (monom b 0) = b"; |
|
202 by (asm_simp_tac (simpset() addsimps [EVAL2_const]) 1); |
|
203 qed "EVAL_const"; |
|
204 |
|
205 Goalw [thm "EVAL_def"] "!! a::'a::domain. EVAL a (monom 1 n) = a ^ n"; |
|
206 by (asm_simp_tac (simpset() addsimps [EVAL2_monom]) 1); |
|
207 qed "EVAL_monom"; |
|
208 |
|
209 Goalw [thm "EVAL_def"] "!! a::'a::ring. EVAL a (b *s p) = b * EVAL a p"; |
|
210 by (asm_simp_tac (simpset() addsimps [EVAL2_smult]) 1); |
|
211 qed "EVAL_smult"; |
|
212 |
|
213 Goalw [thm "EVAL_def"] "!! a::'a::domain. EVAL a (monom b n) = b * a ^ n"; |
|
214 by (asm_simp_tac (simpset() addsimps [EVAL2_monom_n]) 1); |
|
215 qed "EVAL_monom_n"; |
|
216 |
|
217 (* Examples *) |
|
218 |
|
219 Goal |
|
220 "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c"; |
|
221 by (asm_simp_tac (simpset() delsimps [power_Suc] |
|
222 addsimps [EVAL_homo, EVAL_monom, EVAL_monom_n]) 1); |
|
223 result(); |
|
224 |
|
225 Goal |
|
226 "EVAL (y::'a::domain) \ |
|
227 \ (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) = \ |
|
228 \ x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)"; |
|
229 by (asm_simp_tac (simpset() delsimps [power_Suc] |
|
230 addsimps [EVAL_homo, EVAL_monom, EVAL_monom_n, EVAL_const]) 1); |
|
231 result(); |
|
232 |
|