equal
deleted
inserted
replaced
22 val lcoeff_def = thm "lcoeff_def"; |
22 val lcoeff_def = thm "lcoeff_def"; |
23 val eucl_size_def = thm "eucl_size_def"; |
23 val eucl_size_def = thm "eucl_size_def"; |
24 |
24 |
25 val SUM_shrink_below_lemma = thm "SUM_shrink_below_lemma"; |
25 val SUM_shrink_below_lemma = thm "SUM_shrink_below_lemma"; |
26 |
26 |
|
27 fast_arith_split_limit := 0; (* FIXME: rewrite proofs *) |
|
28 |
27 Goal |
29 Goal |
28 "!! f::(nat=>'a::ring). \ |
30 "!! f::(nat=>'a::ring). \ |
29 \ [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |] \ |
31 \ [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |] \ |
30 \ ==> P (setsum f {..n})"; |
32 \ ==> P (setsum f {..n})"; |
31 by (asm_full_simp_tac |
33 by (asm_full_simp_tac |
275 by (Simp_tac 1); |
277 by (Simp_tac 1); |
276 by (Simp_tac 1); |
278 by (Simp_tac 1); |
277 by (rtac long_div_quo_unique 1); |
279 by (rtac long_div_quo_unique 1); |
278 by (REPEAT (atac 1)); |
280 by (REPEAT (atac 1)); |
279 qed "long_div_rem_unique"; |
281 qed "long_div_rem_unique"; |
|
282 |
|
283 fast_arith_split_limit := 9; (* FIXME *) |