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

1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	1	(* Title: HOLCF/cont.thy
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	3	Author: Franz Regensburger
243 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
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2838 diff changeset	14	of default class po
243 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
2838 2e908f29bc3d changed continuous functions from pcpo to cpo (including instances) slotosch parents: 1479 diff changeset	19	default po
243 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
2838 2e908f29bc3d changed continuous functions from pcpo to cpo (including instances) slotosch parents: 1479 diff changeset	22	monofun :: "('a => 'b) => bool" (* monotonicity *)
2e908f29bc3d changed continuous functions from pcpo to cpo (including instances) slotosch parents: 1479 diff changeset	23	contlub :: "('a::cpo => 'b::cpo) => bool" (* first cont. def *)
2e908f29bc3d changed continuous functions from pcpo to cpo (including instances) slotosch parents: 1479 diff changeset	24	cont :: "('a::cpo => 'b::cpo) => 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
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	28	monofun "monofun(f) == ! x y. x << y --> f(x) << f(y)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	29
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	30	contlub "contlub(f) == ! Y. is_chain(Y) -->
3842 b55686a7b22c fixed dots; wenzelm parents: 3323 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
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	33	cont "cont(f) == ! Y. is_chain(Y) -->
3842 b55686a7b22c fixed dots; wenzelm parents: 3323 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	wenzelm
	Mon, 20 Oct 1997 12:47:02 +0200
changeset 3952	dca1bce88ec8
parent 3842	b55686a7b22c
child 4721	c8a8482a8124
permissions	-rw-r--r--