| author | obua |
| Tue, 11 May 2004 20:11:08 +0200 | |
| changeset 14738 | 83f1a514dcb4 |
| parent 14723 | b77ce15b625a |
| child 15481 | fc075ae929e4 |
| permissions | -rw-r--r-- |
1 (*
2 Experimental theory: long division of polynomials
3 $Id$
4 Author: Clemens Ballarin, started 23 June 1999
5 *)
7 theory LongDiv = PolyHomo:
9 consts
10 lcoeff :: "'a::ring up => 'a"
11 eucl_size :: "'a::ring => nat"
13 defs
14 lcoeff_def: "lcoeff p == coeff p (deg p)"
15 eucl_size_def: "eucl_size p == (if p = 0 then 0 else deg p+1)"
17 lemma SUM_shrink_below_lemma:
18 "!! f::(nat=>'a::ring). (ALL i. i < m --> f i = 0) -->
19 setsum (%i. f (i+m)) {..d} = setsum f {..m+d}"
20 apply (induct_tac d)
21 apply (induct_tac m)
22 apply (simp)
23 apply (force)
24 apply (simp)
25 apply (subst ab_semigroup_add.add_commute[of m])
26 apply (simp)
27 done
29 end