equal
deleted
inserted
replaced
1 (* |
1 (* |
2 Sums with naturals as index domain |
2 Sums with naturals as index domain |
3 $Id$ |
3 $Id$ |
4 Author: Clemens Ballarin, started 12 December 1996 |
4 Author: Clemens Ballarin, started 12 December 1996 |
5 *) |
5 *) |
6 |
|
7 open NatSum; |
|
8 |
6 |
9 section "Basic Properties"; |
7 section "Basic Properties"; |
10 |
8 |
11 Goalw [SUM_def] "SUM 0 f = (f 0::'a::ring)"; |
9 Goalw [SUM_def] "SUM 0 f = (f 0::'a::ring)"; |
12 by (Asm_simp_tac 1); |
10 by (Asm_simp_tac 1); |
162 Goal |
160 Goal |
163 "!! f::(nat=>'a::ring). \ |
161 "!! f::(nat=>'a::ring). \ |
164 \ SUM n (%i. if i = x then f i else <0>) = (if x <= n then f x else <0>)"; |
162 \ SUM n (%i. if i = x then f i else <0>) = (if x <= n then f x else <0>)"; |
165 by (nat_ind_tac "n" 1); |
163 by (nat_ind_tac "n" 1); |
166 (* Base case *) |
164 (* Base case *) |
167 by (simp_tac (simpset() setloop (split_tac [expand_if])) 1); |
165 by (Simp_tac 1); |
168 (* Induction step *) |
166 (* Induction step *) |
169 by (asm_simp_tac (simpset() setloop (split_tac [expand_if])) 1); |
167 by (Asm_simp_tac 1); |
170 by (Clarify_tac 1); |
168 by (Clarify_tac 1); |
171 by (res_inst_tac [("f", "f")] arg_cong 1); |
169 by (res_inst_tac [("f", "f")] arg_cong 1); |
172 by (fast_arith_tac 1); |
170 by (arith_tac 1); |
173 qed "SUM_if_singleton"; |
171 qed "SUM_if_singleton"; |
174 |
172 |
175 Goal |
173 Goal |
176 "!! f::(nat=>'a::ring). \ |
174 "!! f::(nat=>'a::ring). \ |
177 \ m <= n & (ALL i. m < i & i <= n --> f i = <0>) --> \ |
175 \ m <= n & (ALL i. m < i & i <= n --> f i = <0>) --> \ |