isabelle: src/HOLCF/Discrete1.ML@9b7026a0b0ed (annotated)

2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	1	(* Title: HOLCF/Discrete1.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
12030 46d57d0290a2 GPLed; wenzelm parents: 11346 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	5
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	6	Proves that 'a discr is a cpo
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	7	*)
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	8
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4721 diff changeset	9	Goalw [less_discr_def] "((x::('a::term)discr) << y) = (x=y)";
3018 e65b60b28341 Ran expandshort paulson parents: 2841 diff changeset	10	by (rtac refl 1);
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	11	qed "discr_less_eq";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	12	AddIffs [discr_less_eq];
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	13
11346 0d28bc664955 corrected ML names of definitions oheimb parents: 5192 diff changeset	14	Goalw [chain_def]
4721 c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin oheimb parents: 4098 diff changeset	15	"!!S::nat=>('a::term)discr. chain S ==> S i = S 0";
5192 704dd3a6d47d Adapted to new datatype package. berghofe parents: 5068 diff changeset	16	by (induct_tac "i" 1);
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3018 diff changeset	17	by (rtac refl 1);
3018 e65b60b28341 Ran expandshort paulson parents: 2841 diff changeset	18	by (etac subst 1);
e65b60b28341 Ran expandshort paulson parents: 2841 diff changeset	19	by (rtac sym 1);
e65b60b28341 Ran expandshort paulson parents: 2841 diff changeset	20	by (Fast_tac 1);
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	21	qed "discr_chain0";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	22
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4721 diff changeset	23	Goal
4721 c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin oheimb parents: 4098 diff changeset	24	"!!S::nat=>('a::term)discr. chain(S) ==> range(S) = {S 0}";
4098 71e05eb27fb6 isatool fixclasimp; wenzelm parents: 3323 diff changeset	25	by (fast_tac (claset() addEs [discr_chain0]) 1);
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	26	qed "discr_chain_range0";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	27	Addsimps [discr_chain_range0];
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	28
11346 0d28bc664955 corrected ML names of definitions oheimb parents: 5192 diff changeset	29	Goalw [is_lub_def,is_ub_def]
4721 c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin oheimb parents: 4098 diff changeset	30	"!!S. chain S ==> ? x::('a::term)discr. range(S) <<\| x";
3018 e65b60b28341 Ran expandshort paulson parents: 2841 diff changeset	31	by (Asm_simp_tac 1);
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	32	qed "discr_cpo";

author	wenzelm
	Wed, 14 Nov 2001 23:16:05 +0100
changeset 12186	9b7026a0b0ed
parent 12030	46d57d0290a2
child 12338	de0f4a63baa5
permissions	-rw-r--r--