Old_HOL: IMP/Denotation.thy@760641387b20 (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
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	11	consts
132 47be9d22a0d6 Renamed a few types and vars nipkow parents: 131 diff changeset	12	A :: "aexp => state => nat"
47be9d22a0d6 Renamed a few types and vars nipkow parents: 131 diff changeset	13	B :: "bexp => state => bool"
47be9d22a0d6 Renamed a few types and vars nipkow parents: 131 diff changeset	14	C :: "com => (state*state)set"
47be9d22a0d6 Renamed a few types and vars nipkow parents: 131 diff changeset	15	Gamma :: "[bexp,com,(statestate)set] => (statestate)set"
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	16
137 bca8203b0e91 Converted rules to primrecs nipkow parents: 132 diff changeset	17	primrec A aexp
138 bf044f0db994 changed names nipkow parents: 137 diff changeset	18	A_nat "A(N(n)) = (%s. n)"
bf044f0db994 changed names nipkow parents: 137 diff changeset	19	A_loc "A(X(x)) = (%s. s(x))"
bf044f0db994 changed names nipkow parents: 137 diff changeset	20	A_op1 "A(Op1(f,a)) = (%s. f(A(a,s)))"
bf044f0db994 changed names nipkow parents: 137 diff changeset	21	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	22
137 bca8203b0e91 Converted rules to primrecs nipkow parents: 132 diff changeset	23	primrec B bexp
138 bf044f0db994 changed names nipkow parents: 137 diff changeset	24	B_true "B(true) = (%s. True)"
bf044f0db994 changed names nipkow parents: 137 diff changeset	25	B_false "B(false) = (%s. False)"
bf044f0db994 changed names nipkow parents: 137 diff changeset	26	B_op "B(ROp(f,a0,a1)) = (%s. f(A(a0,s),A(a1,s)))"
bf044f0db994 changed names nipkow parents: 137 diff changeset	27	B_not "B(noti(b)) = (%s. ~B(b,s))"
bf044f0db994 changed names nipkow parents: 137 diff changeset	28	B_and "B(b0 andi b1) = (%s. B(b0,s) & B(b1,s))"
bf044f0db994 changed names nipkow parents: 137 diff changeset	29	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	30
137 bca8203b0e91 Converted rules to primrecs nipkow parents: 132 diff changeset	31	defs
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	32	Gamma_def "Gamma(b,c) == \
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	33	\ (%phi.{io. io : (phi O C(c)) & B(b,fst(io))} Un \
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	34	\ {io. io : id & ~B(b,fst(io))})"
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	35
137 bca8203b0e91 Converted rules to primrecs nipkow parents: 132 diff changeset	36	primrec C com
138 bf044f0db994 changed names nipkow parents: 137 diff changeset	37	C_skip "C(skip) = id"
bf044f0db994 changed names nipkow parents: 137 diff changeset	38	C_assign "C(x := a) = {io . snd(io) = fst(io)[A(a,fst(io))/x]}"
bf044f0db994 changed names nipkow parents: 137 diff changeset	39	C_comp "C(c0 ; c1) = C(c1) O C(c0)"
bf044f0db994 changed names nipkow parents: 137 diff changeset	40	C_if "C(ifc b then c0 else c1) = \
137 bca8203b0e91 Converted rules to primrecs nipkow parents: 132 diff changeset	41	\ {io. io:C(c0) & B(b,fst(io))} Un \
bca8203b0e91 Converted rules to primrecs nipkow parents: 132 diff changeset	42	\ {io. io:C(c1) & ~B(b,fst(io))}"
138 bf044f0db994 changed names nipkow parents: 137 diff changeset	43	C_while "C(while b do c) = lfp(Gamma(b,c))"
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	44
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	45	end

author	wenzelm
	Wed, 14 Sep 1994 16:05:28 +0200
changeset 142	760641387b20
parent 138	bf044f0db994
child 144	6254f50e5ec9
permissions	-rw-r--r--