isabelle: src/HOL/Algebra/poly/ProtoPoly.ML@50be659d4222 (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	Prepearing definitions for 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 9 December 1996
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
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	7	open ProtoPoly;
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	(* Rules for bound *)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	10
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	11	val prem = goalw ProtoPoly.thy [bound_def]
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	12	"[\| !! m. n < m ==> f m = <0> \|] ==> bound n f";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	13	by (fast_tac (claset() addIs prem) 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	14	qed "boundI";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	15
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	16	Goalw [bound_def]
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	17	"!! f. [\| bound n f; n < m \|] ==> f m = <0>";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	18	by (Fast_tac 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	19	qed "boundD";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	20
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	21	Goalw [bound_def]
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	22	"!! f. [\| bound n f; n <= m \|] ==> bound m f";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	23	by (fast_tac (set_cs addIs [le_less_trans]) 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	24	(* Need set_cs, otherwise starts reasoning about naturals *)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	25	qed "le_bound";
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	AddSIs [boundI];
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	28	AddDs [boundD];
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	29
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	30	Goal "(%x. <0>) : {f. EX n. bound n f}";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	31	by (Blast_tac 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	32	qed "UP_witness";

author	wenzelm
	Fri, 06 Oct 2000 17:35:58 +0200
changeset 10168	50be659d4222
parent 7998	3d0c34795831
child 10448	da7d0e28f746
permissions	-rw-r--r--