| author | aspinall |
| Fri, 30 Sep 2005 18:18:34 +0200 | |
| changeset 17740 | fc385ce6187d |
| parent 17274 | 746bb4c56800 |
| child 21423 | 6cdd0589aa73 |
| permissions | -rw-r--r-- |
| 7998 | 1 |
(* |
2 |
Experimental theory: long division of polynomials |
|
3 |
$Id$ |
|
4 |
Author: Clemens Ballarin, started 23 June 1999 |
|
5 |
*) |
|
6 |
||
| 16417 | 7 |
theory LongDiv imports PolyHomo begin |
| 7998 | 8 |
|
9 |
consts |
|
| 13735 | 10 |
lcoeff :: "'a::ring up => 'a" |
| 14723 | 11 |
eucl_size :: "'a::ring => nat" |
| 7998 | 12 |
|
13 |
defs |
|
| 14723 | 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)" |
|
16 |
||
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) |
|
| 15481 | 21 |
apply (induct_tac m) |
22 |
apply (simp) |
|
23 |
apply (force) |
|
|
17274
746bb4c56800
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
16417
diff
changeset
|
24 |
apply (simp add: ab_semigroup_add_class.add_commute[of m]) |
| 14723 | 25 |
done |
| 7998 | 26 |
|
27 |
end |
|
28 |