# HG changeset patch
# User obua
# Date 1084200054 -7200
# Node ID b77ce15b625abb7edc09096801514627845a39f5
# Parent  8e739a6eaf1124d5845625d5a651b59f78703b12
moved first lemma in LongDiv.ML to LongDiv.thy

diff -r 8e739a6eaf11 -r b77ce15b625a src/HOL/Algebra/poly/LongDiv.ML
--- a/src/HOL/Algebra/poly/LongDiv.ML	Sun May 09 23:04:36 2004 +0200
+++ b/src/HOL/Algebra/poly/LongDiv.ML	Mon May 10 16:40:54 2004 +0200
@@ -19,18 +19,10 @@
 val field_ax = thm "field_ax";
 val lcoeff_nonzero = thm "lcoeff_nonzero";
 
-Goal
-  "!! f::(nat=>'a::ring). \
-\    (ALL i. i < m --> f i = 0) --> \
-\      setsum (%i. f (i+m)) {..d} = setsum f {..m+d}";
-by (induct_tac "d" 1);
-(* Base case *)
-by (induct_tac "m" 1);
-by (Simp_tac 1);
-by (Force_tac 1);
-(* Induction step *)
-by (asm_simp_tac (simpset() addsimps add_ac) 1);
-val SUM_shrink_below_lemma = result();
+val lcoeff_def = thm "lcoeff_def";
+val eucl_size_def = thm "eucl_size_def";
+
+val SUM_shrink_below_lemma = thm "SUM_shrink_below_lemma";
 
 Goal
   "!! f::(nat=>'a::ring). \
diff -r 8e739a6eaf11 -r b77ce15b625a src/HOL/Algebra/poly/LongDiv.thy
--- a/src/HOL/Algebra/poly/LongDiv.thy	Sun May 09 23:04:36 2004 +0200
+++ b/src/HOL/Algebra/poly/LongDiv.thy	Mon May 10 16:40:54 2004 +0200
@@ -4,15 +4,27 @@
     Author: Clemens Ballarin, started 23 June 1999
 *)
 
-LongDiv = PolyHomo +
+theory LongDiv = PolyHomo:
 
 consts
   lcoeff :: "'a::ring up => 'a"
-  eucl_size :: 'a::ring => nat
+  eucl_size :: "'a::ring => nat"
 
 defs
-  lcoeff_def	"lcoeff p == coeff p (deg p)"
-  eucl_size_def "eucl_size p == if p = 0 then 0 else deg p+1"
+  lcoeff_def: "lcoeff p == coeff p (deg p)"
+  eucl_size_def: "eucl_size p == (if p = 0 then 0 else deg p+1)"
+
+lemma SUM_shrink_below_lemma:
+  "!! f::(nat=>'a::ring). (ALL i. i < m --> f i = 0) --> 
+  setsum (%i. f (i+m)) {..d} = setsum f {..m+d}"
+  apply (induct_tac d)
+  apply (induct_tac m)
+  apply (simp)
+  apply (force)
+  apply (simp)
+  apply (subst plus_ac0.commute[of m])
+  apply (simp)
+  done
 
 end