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

author	kleing
	Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981	e73f8140af78
parent 12114	a8e860c86252
child 15563	9e125b675253
permissions	-rw-r--r--