author | wenzelm |
Sat, 17 Sep 2005 20:49:14 +0200 | |
changeset 17479 | 68a7acb5f22e |
parent 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 |
||
13735 | 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 |
||
7998 | 84 |
(* Ring homomorphisms and polynomials *) |
13735 | 85 |
(* |
7998 | 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]; |
|
13735 | 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"; |
|
7998 | 108 |
|
109 |
(* Evaluation homomorphism *) |
|
110 |
||
111 |
Goal |
|
112 |
"!! phi::('a::ring=>'b::ring). homo phi ==> homo (EVAL2 phi a)"; |
|
113 |
by (rtac homoI 1); |
|
17479 | 114 |
by (rewtac (thm "EVAL2_def")); |
7998 | 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 + *) |
|
13735 | 131 |
by (asm_simp_tac (simpset() addsimps [l_distr, natsum_add]) 1); |
7998 | 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); |
|
13735 | 142 |
(* getting a^i and a^(k-i) together is difficult, so we do it manually *) |
7998 | 143 |
by (res_inst_tac [("s", |
11093 | 144 |
" setsum \ |
145 |
\ (%k. setsum \ |
|
13735 | 146 |
\ (%i. phi (coeff aa i) * (phi (coeff b (k - i)) * \ |
11093 | 147 |
\ (a ^ i * a ^ (k - i)))) {..k}) \ |
148 |
\ {..deg aa + deg b}")] trans 1); |
|
7998 | 149 |
by (asm_simp_tac (simpset() |
13735 | 150 |
addsimps [power_mult, leD RS add_diff_inverse, natsum_ldistr]) 1); |
151 |
by (Simp_tac 1); |
|
152 |
(* 1 commutes *) |
|
7998 | 153 |
by (Asm_simp_tac 1); |
154 |
qed "EVAL2_homo"; |
|
155 |
||
17479 | 156 |
Goalw [thm "EVAL2_def"] |
13735 | 157 |
"!! phi::'a::ring=>'b::ring. EVAL2 phi a (monom b 0) = phi b"; |
7998 | 158 |
by (Simp_tac 1); |
159 |
qed "EVAL2_const"; |
|
160 |
||
17479 | 161 |
Goalw [thm "EVAL2_def"] |
13735 | 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 *) |
|
7998 | 164 |
by (Asm_simp_tac 1); |
165 |
qed "EVAL2_monom1"; |
|
166 |
||
17479 | 167 |
Goalw [thm "EVAL2_def"] |
13735 | 168 |
"!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 n) = a ^ n"; |
7998 | 169 |
by (Simp_tac 1); |
8707 | 170 |
by (case_tac "n" 1); |
171 |
by Auto_tac; |
|
7998 | 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"; |
|
13735 | 177 |
by (asm_simp_tac (simpset() |
178 |
addsimps [monom_mult_is_smult RS sym, EVAL2_homo, EVAL2_const]) 1); |
|
7998 | 179 |
qed "EVAL2_smult"; |
180 |
||
13735 | 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 |
||
17479 | 197 |
Goalw [thm "EVAL_def"] "!! a::'a::ring. homo (EVAL a)"; |
13735 | 198 |
by (asm_simp_tac (simpset() addsimps [EVAL2_homo]) 1); |
7998 | 199 |
qed "EVAL_homo"; |
200 |
||
17479 | 201 |
Goalw [thm "EVAL_def"] "!! a::'a::ring. EVAL a (monom b 0) = b"; |
7998 | 202 |
by (asm_simp_tac (simpset() addsimps [EVAL2_const]) 1); |
203 |
qed "EVAL_const"; |
|
204 |
||
17479 | 205 |
Goalw [thm "EVAL_def"] "!! a::'a::domain. EVAL a (monom 1 n) = a ^ n"; |
7998 | 206 |
by (asm_simp_tac (simpset() addsimps [EVAL2_monom]) 1); |
207 |
qed "EVAL_monom"; |
|
208 |
||
17479 | 209 |
Goalw [thm "EVAL_def"] "!! a::'a::ring. EVAL a (b *s p) = b * EVAL a p"; |
7998 | 210 |
by (asm_simp_tac (simpset() addsimps [EVAL2_smult]) 1); |
211 |
qed "EVAL_smult"; |
|
212 |
||
17479 | 213 |
Goalw [thm "EVAL_def"] "!! a::'a::domain. EVAL a (monom b n) = b * a ^ n"; |
13735 | 214 |
by (asm_simp_tac (simpset() addsimps [EVAL2_monom_n]) 1); |
215 |
qed "EVAL_monom_n"; |
|
216 |
||
7998 | 217 |
(* Examples *) |
218 |
||
219 |
Goal |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
220 |
"EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c"; |
7998 | 221 |
by (asm_simp_tac (simpset() delsimps [power_Suc] |
13735 | 222 |
addsimps [EVAL_homo, EVAL_monom, EVAL_monom_n]) 1); |
7998 | 223 |
result(); |
224 |
||
225 |
Goal |
|
11093 | 226 |
"EVAL (y::'a::domain) \ |
13735 | 227 |
\ (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) = \ |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
228 |
\ x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)"; |
7998 | 229 |
by (asm_simp_tac (simpset() delsimps [power_Suc] |
13735 | 230 |
addsimps [EVAL_homo, EVAL_monom, EVAL_monom_n, EVAL_const]) 1); |
7998 | 231 |
result(); |
232 |