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