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