482
|
1 |
(* Title: ZF/IMP/Denotation.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Heiko Loetzbeyer & Robert Sandner, TUM
|
|
4 |
Copyright 1994 TUM
|
511
|
5 |
|
|
6 |
Denotational semantics of expressions & commands
|
482
|
7 |
*)
|
|
8 |
|
511
|
9 |
Denotation = Com +
|
482
|
10 |
|
|
11 |
consts
|
1401
|
12 |
A :: i => i => i
|
|
13 |
B :: i => i => i
|
|
14 |
C :: i => i
|
|
15 |
Gamma :: [i,i,i] => i
|
482
|
16 |
|
753
|
17 |
rules (*NOT definitional*)
|
511
|
18 |
A_nat_def "A(N(n)) == (%sigma. n)"
|
|
19 |
A_loc_def "A(X(x)) == (%sigma. sigma`x)"
|
|
20 |
A_op1_def "A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
|
|
21 |
A_op2_def "A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
|
482
|
22 |
|
|
23 |
|
511
|
24 |
B_true_def "B(true) == (%sigma. 1)"
|
|
25 |
B_false_def "B(false) == (%sigma. 0)"
|
|
26 |
B_op_def "B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
|
482
|
27 |
|
|
28 |
|
511
|
29 |
B_not_def "B(noti(b)) == (%sigma. not(B(b,sigma)))"
|
|
30 |
B_and_def "B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))"
|
|
31 |
B_or_def "B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
|
|
32 |
|
|
33 |
C_skip_def "C(skip) == id(loc->nat)"
|
1155
|
34 |
C_assign_def "C(x := a) == {io:(loc->nat)*(loc->nat).
|
|
35 |
snd(io) = fst(io)[A(a,fst(io))/x]}"
|
482
|
36 |
|
511
|
37 |
C_comp_def "C(c0 ; c1) == C(c1) O C(c0)"
|
1155
|
38 |
C_if_def "C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un
|
|
39 |
{io:C(c1). B(b,fst(io))=0}"
|
482
|
40 |
|
1155
|
41 |
Gamma_def "Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un
|
|
42 |
{io : id(loc->nat). B(b,fst(io))=0})"
|
482
|
43 |
|
511
|
44 |
C_while_def "C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
|
482
|
45 |
|
|
46 |
end
|