isabelle: src/HOL/Algebra/poly/LongDiv.thy@12833c7e0fa6 (annotated)

7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	1	(*
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	2	Experimental theory: long division of polynomials
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	3	$Id$
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	4	Author: Clemens Ballarin, started 23 June 1999
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	5	*)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	6
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 15481 diff changeset	7	theory LongDiv imports PolyHomo begin
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	8
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	9	consts
13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11093 diff changeset	10	lcoeff :: "'a::ring up => 'a"
14723 b77ce15b625a moved first lemma in LongDiv.ML to LongDiv.thy obua parents: 13735 diff changeset	11	eucl_size :: "'a::ring => nat"
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	12
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	13	defs
14723 b77ce15b625a moved first lemma in LongDiv.ML to LongDiv.thy obua parents: 13735 diff changeset	14	lcoeff_def: "lcoeff p == coeff p (deg p)"
b77ce15b625a moved first lemma in LongDiv.ML to LongDiv.thy obua parents: 13735 diff changeset	15	eucl_size_def: "eucl_size p == (if p = 0 then 0 else deg p+1)"
b77ce15b625a moved first lemma in LongDiv.ML to LongDiv.thy obua parents: 13735 diff changeset	16
b77ce15b625a moved first lemma in LongDiv.ML to LongDiv.thy obua parents: 13735 diff changeset	17	lemma SUM_shrink_below_lemma:
b77ce15b625a moved first lemma in LongDiv.ML to LongDiv.thy obua parents: 13735 diff changeset	18	"!! f::(nat=>'a::ring). (ALL i. i < m --> f i = 0) -->
b77ce15b625a moved first lemma in LongDiv.ML to LongDiv.thy obua parents: 13735 diff changeset	19	setsum (%i. f (i+m)) {..d} = setsum f {..m+d}"
b77ce15b625a moved first lemma in LongDiv.ML to LongDiv.thy obua parents: 13735 diff changeset	20	apply (induct_tac d)
15481 fc075ae929e4 the new subst tactic, by Lucas Dixon paulson parents: 14738 diff changeset	21	apply (induct_tac m)
fc075ae929e4 the new subst tactic, by Lucas Dixon paulson parents: 14738 diff changeset	22	apply (simp)
fc075ae929e4 the new subst tactic, by Lucas Dixon paulson parents: 14738 diff changeset	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 b77ce15b625a moved first lemma in LongDiv.ML to LongDiv.thy obua parents: 13735 diff changeset	25	done
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	26
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	27	end
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	28

author	wenzelm
	Thu, 16 Feb 2006 18:25:58 +0100
changeset 19075	12833c7e0fa6
parent 17274	746bb4c56800
child 21423	6cdd0589aa73
permissions	-rw-r--r--