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

author	wenzelm
	Fri, 10 Nov 2000 19:15:38 +0100
changeset 10448	da7d0e28f746
parent 7998	3d0c34795831
child 11093	62c2e0af1d30
permissions	-rw-r--r--