isabelle: src/HOLCF/IMP/Denotational.thy@e7c9900cca4d (annotated)

2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	1	(* Title: HOLCF/IMP/Denotational.thy
2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	2	ID: $Id$
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	3	Author: Tobias Nipkow & Robert Sandner, TUM
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	4	Copyright 1996 TUM
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	5
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	6	Denotational semantics of commands in HOLCF
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	7	*)
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	8
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	9	Denotational = HOLCF + Natural +
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	10
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	11	constdefs
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	12	dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)"
3842 b55686a7b22c fixed dots; wenzelm parents: 2841 diff changeset	13	"dlift f == (LAM x. case x of Undef => UU \| Def(y) => f`(Discr y))"
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	14
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	15	consts D :: "com => state discr -> state lift"
2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	16
5192 704dd3a6d47d Adapted to new datatype package. berghofe parents: 4904 diff changeset	17	primrec
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	18	"D(SKIP) = (LAM s. Def(undiscr s))"
9247 ad9f986616de disambiguated := ; added Examples (factorial) oheimb parents: 5192 diff changeset	19	"D(X :== a) = (LAM s. Def((undiscr s)[X ::= a(undiscr s)]))"
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	20	"D(c0 ; c1) = (dlift(D c1) oo (D c0))"
2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	21	"D(IF b THEN c1 ELSE c2) =
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	22	(LAM s. if b(undiscr s) then (D c1)`s else (D c2)`s)"
2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	23	"D(WHILE b DO c) =
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	24	fix`(LAM w s. if b(undiscr s) then (dlift w)`((D c)`s)
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	25	else Def(undiscr s))"
2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	26
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	27	end

author	wenzelm
	Fri, 01 Dec 2000 19:42:05 +0100
changeset 10567	e7c9900cca4d
parent 9247	ad9f986616de
child 10835	f4745d77e620
permissions	-rw-r--r--