isabelle: src/HOLCF/Discrete.ML@fdf9434b04ea (annotated)

2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	1	(* Title: HOLCF/Discrete.ML
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	2	ID: $Id$
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	3	Author: Tobias Nipkow
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	4	*)
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	5
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4721 diff changeset	6	Goalw [undiscr_def] "undiscr(Discr x) = x";
4423 a129b817b58a expandshort; wenzelm parents: 4098 diff changeset	7	by (Simp_tac 1);
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	8	qed "undiscr_Discr";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	9	Addsimps [undiscr_Discr];
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	10
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4721 diff changeset	11	Goal
12338 de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type"); wenzelm parents: 12030 diff changeset	12	"!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
4423 a129b817b58a expandshort; wenzelm parents: 4098 diff changeset	13	by (fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	14	qed "discr_chain_f_range0";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	15
12338 de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type"); wenzelm parents: 12030 diff changeset	16	Goalw [cont,is_lub_def,is_ub_def] "cont(%x::('a::type)discr. f x)";
4423 a129b817b58a expandshort; wenzelm parents: 4098 diff changeset	17	by (simp_tac (simpset() addsimps [discr_chain_f_range0]) 1);
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	18	qed "cont_discr";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	19	AddIffs [cont_discr];

author	berghofe
	Thu, 27 Jan 2005 12:37:02 +0100
changeset 15475	fdf9434b04ea
parent 14981	e73f8140af78
permissions	-rw-r--r--