isabelle: src/HOLCF/Cont.thy@1358dc040edb (annotated)

243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	1	(* Title: HOLCF/cont.thy
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	3	Author: Franz Regensburger
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4	Copyright 1993 Technische Universitaet Muenchen
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6	Results about continuity and monotonicity
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	8
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	9	Cont = Fun3 +
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	11	(*
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	13	Now we change the default class! Form now on all untyped typevariables are
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	14	of default class pcpo
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	16	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	17
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	18
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	19	default pcpo
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	20
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	21	consts
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	22	monofun :: "('a::po => 'b::po) => bool" (* monotonicity *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	23	contlub :: "('a => 'b) => bool" (* first cont. def *)
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 1150 diff changeset	24	cont :: "('a => 'b) => bool" (* secnd cont. def *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	25
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 1150 diff changeset	26	defs
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	27
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	28	monofun "monofun(f) == ! x y. x << y --> f(x) << f(y)"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	29
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1168 diff changeset	30	contlub "contlub(f) == ! Y. is_chain(Y) -->
ea0668a1c0ba added 8bit pragmas regensbu parents: 1168 diff changeset	31	f(lub(range(Y))) = lub(range(% i.f(Y(i))))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	32
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1168 diff changeset	33	cont "cont(f) == ! Y. is_chain(Y) -->
ea0668a1c0ba added 8bit pragmas regensbu parents: 1168 diff changeset	34	range(% i.f(Y(i))) <<\| f(lub(range(Y)))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	35
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	36	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	37	(* the main purpose of cont.thy is to show: *)
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1168 diff changeset	38	(* monofun(f) & contlub(f) <==> cont(f) *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	39	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	40
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	41	end

author	clasohm
	Tue, 24 Oct 1995 14:45:35 +0100
changeset 1294	1358dc040edb
parent 1274	ea0668a1c0ba
child 1479	21eb5e156d91
permissions	-rw-r--r--