|
7998
|
1 |
(*
|
|
|
2 |
Experimental theory: long division of polynomials
|
|
|
3 |
$Id$
|
|
|
4 |
Author: Clemens Ballarin, started 23 June 1999
|
|
|
5 |
*)
|
|
|
6 |
|
|
14723
|
7 |
theory LongDiv = PolyHomo:
|
|
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)
|
|
|
21 |
apply (induct_tac m)
|
|
|
22 |
apply (simp)
|
|
|
23 |
apply (force)
|
|
|
24 |
apply (simp)
|
|
14738
|
25 |
apply (subst ab_semigroup_add.add_commute[of m])
|
|
14723
|
26 |
apply (simp)
|
|
|
27 |
done
|
|
7998
|
28 |
|
|
|
29 |
end
|
|
|
30 |
|