isabelle: src/HOLCF/Pcpo.thy@70b2651af635 (annotated)

2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	1	(* Title: HOLCF/Pcpo.thy
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	2	ID: $Id$
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	3	Author: Franz Regensburger
12030 46d57d0290a2 GPLed; wenzelm parents: 5438 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	5
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	6	introduction of the classes cpo and pcpo
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	7	*)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	8	Pcpo = Porder +
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	9
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	10	(* The class cpo of chain complete partial orders *)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	11	(* ********************************************** *)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	12	axclass cpo < po
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	13	(* class axiom: *)
5438 c89ee3a46a74 simplified definition of axclass cpo oheimb parents: 4721 diff changeset	14	cpo "chain S ==> ? x. range S <<\| x"
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	15
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	16	(* The class pcpo of pointed cpos *)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	17	(* ****************************** *)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	18	axclass pcpo < cpo
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	19
3842 b55686a7b22c fixed dots; wenzelm parents: 3326 diff changeset	20	least "? x.!y. x<<y"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	21
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	22	consts
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	23	UU :: "'a::pcpo"
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	24
12114 a8e860c86252 eliminated old "symbols" syntax, use "xsymbols" instead; wenzelm parents: 12030 diff changeset	25	syntax (xsymbols)
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	26	UU :: "'a::pcpo" ("\\<bottom>")
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	27
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	28	defs
3842 b55686a7b22c fixed dots; wenzelm parents: 3326 diff changeset	29	UU_def "UU == @x.!y. x<<y"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	30
3326 930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo. slotosch parents: 2640 diff changeset	31	(* further useful classes for HOLCF domains *)
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo. slotosch parents: 2640 diff changeset	32
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo. slotosch parents: 2640 diff changeset	33	axclass chfin<cpo
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo. slotosch parents: 2640 diff changeset	34
4721 c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin oheimb parents: 3842 diff changeset	35	chfin "!Y. chain Y-->(? n. max_in_chain n Y)"
3326 930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo. slotosch parents: 2640 diff changeset	36
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo. slotosch parents: 2640 diff changeset	37	axclass flat<pcpo
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo. slotosch parents: 2640 diff changeset	38
3842 b55686a7b22c fixed dots; wenzelm parents: 3326 diff changeset	39	ax_flat "! x y. x << y --> (x = UU) \| (x=y)"
3326 930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo. slotosch parents: 2640 diff changeset	40
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	41	end

author	paulson
	Wed, 16 Jan 2002 17:53:22 +0100
changeset 12777	70b2651af635
parent 12114	a8e860c86252
child 14981	e73f8140af78
permissions	-rw-r--r--