Old_HOL: IMP/Denotation.thy@a9f7ff3a464c (annotated)

132 47be9d22a0d6 Renamed a few types and vars nipkow parents: 131 diff changeset	1	(* Title: HOL/IMP/Denotation.thy
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	2	ID: $Id$
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	3	Author: Heiko Loetzbeyer & Robert Sandner, TUM
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	4	Copyright 1994 TUM
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	5
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	6	Denotational semantics of expressions & commands
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	7	*)
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	8
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	9	Denotation = Com +
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	10
144 6254f50e5ec9 Definition of C was not truly prim rec because C was called inside Gamma nipkow parents: 138 diff changeset	11	types com_den = "(state*state)set"
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	12	consts
132 47be9d22a0d6 Renamed a few types and vars nipkow parents: 131 diff changeset	13	A :: "aexp => state => nat"
47be9d22a0d6 Renamed a few types and vars nipkow parents: 131 diff changeset	14	B :: "bexp => state => bool"
144 6254f50e5ec9 Definition of C was not truly prim rec because C was called inside Gamma nipkow parents: 138 diff changeset	15	C :: "com => com_den"
6254f50e5ec9 Definition of C was not truly prim rec because C was called inside Gamma nipkow parents: 138 diff changeset	16	Gamma :: "[bexp,com_den] => (com_den => com_den)"
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	17
137 bca8203b0e91 Converted rules to primrecs nipkow parents: 132 diff changeset	18	primrec A aexp
138 bf044f0db994 changed names nipkow parents: 137 diff changeset	19	A_nat "A(N(n)) = (%s. n)"
bf044f0db994 changed names nipkow parents: 137 diff changeset	20	A_loc "A(X(x)) = (%s. s(x))"
bf044f0db994 changed names nipkow parents: 137 diff changeset	21	A_op1 "A(Op1(f,a)) = (%s. f(A(a,s)))"
bf044f0db994 changed names nipkow parents: 137 diff changeset	22	A_op2 "A(Op2(f,a0,a1)) = (%s. f(A(a0,s),A(a1,s)))"
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	23
137 bca8203b0e91 Converted rules to primrecs nipkow parents: 132 diff changeset	24	primrec B bexp
138 bf044f0db994 changed names nipkow parents: 137 diff changeset	25	B_true "B(true) = (%s. True)"
bf044f0db994 changed names nipkow parents: 137 diff changeset	26	B_false "B(false) = (%s. False)"
bf044f0db994 changed names nipkow parents: 137 diff changeset	27	B_op "B(ROp(f,a0,a1)) = (%s. f(A(a0,s),A(a1,s)))"
bf044f0db994 changed names nipkow parents: 137 diff changeset	28	B_not "B(noti(b)) = (%s. ~B(b,s))"
bf044f0db994 changed names nipkow parents: 137 diff changeset	29	B_and "B(b0 andi b1) = (%s. B(b0,s) & B(b1,s))"
bf044f0db994 changed names nipkow parents: 137 diff changeset	30	B_or "B(b0 ori b1) = (%s. B(b0,s) \| B(b1,s))"
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	31
137 bca8203b0e91 Converted rules to primrecs nipkow parents: 132 diff changeset	32	defs
144 6254f50e5ec9 Definition of C was not truly prim rec because C was called inside Gamma nipkow parents: 138 diff changeset	33	Gamma_def "Gamma(b,cd) == \
6254f50e5ec9 Definition of C was not truly prim rec because C was called inside Gamma nipkow parents: 138 diff changeset	34	\ (%phi.{st. st : (phi O cd) & B(b,fst(st))} Un \
6254f50e5ec9 Definition of C was not truly prim rec because C was called inside Gamma nipkow parents: 138 diff changeset	35	\ {st. st : id & ~B(b,fst(st))})"
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	36
137 bca8203b0e91 Converted rules to primrecs nipkow parents: 132 diff changeset	37	primrec C com
138 bf044f0db994 changed names nipkow parents: 137 diff changeset	38	C_skip "C(skip) = id"
144 6254f50e5ec9 Definition of C was not truly prim rec because C was called inside Gamma nipkow parents: 138 diff changeset	39	C_assign "C(x := a) = {st . snd(st) = fst(st)[A(a,fst(st))/x]}"
138 bf044f0db994 changed names nipkow parents: 137 diff changeset	40	C_comp "C(c0 ; c1) = C(c1) O C(c0)"
bf044f0db994 changed names nipkow parents: 137 diff changeset	41	C_if "C(ifc b then c0 else c1) = \
144 6254f50e5ec9 Definition of C was not truly prim rec because C was called inside Gamma nipkow parents: 138 diff changeset	42	\ {st. st:C(c0) & B(b,fst(st))} Un \
6254f50e5ec9 Definition of C was not truly prim rec because C was called inside Gamma nipkow parents: 138 diff changeset	43	\ {st. st:C(c1) & ~B(b,fst(st))}"
6254f50e5ec9 Definition of C was not truly prim rec because C was called inside Gamma nipkow parents: 138 diff changeset	44	C_while "C(while b do c) = lfp(Gamma(b,C(c)))"
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	45
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	46	end

author	wenzelm
	Wed, 21 Sep 1994 15:40:41 +0200
changeset 145	a9f7ff3a464c
parent 144	6254f50e5ec9
child 249	492493334e0f
permissions	-rw-r--r--