isabelle: src/HOLCF/Pcpo.thy@bb2ee88aa43f (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	Copyright 1993 Technische Universitaet Muenchen
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: *)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	14	cpo "is_chain S ==> ? x. range(S) <<\| (x::'a::po)"
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
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 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
91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	25	syntax (symbols)
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
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	31	end

author	paulson
	Wed, 07 May 1997 12:49:02 +0200
changeset 3119	bb2ee88aa43f
parent 2640	ee4dfce170a0
child 3326	930c9bed5a09
permissions	-rw-r--r--