src/HOL/IMP/Denotation.thy
author clasohm
Wed Nov 29 17:01:41 1995 +0100 (1995-11-29)
changeset 1374 5e407f2a3323
parent 1151 c820b3cc3df0
child 1476 608483c2122a
permissions -rw-r--r--
removed quotes from consts and syntax sections
clasohm@924
     1
(*  Title: 	HOL/IMP/Denotation.thy
clasohm@924
     2
    ID:         $Id$
clasohm@924
     3
    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
clasohm@924
     4
    Copyright   1994 TUM
clasohm@924
     5
clasohm@924
     6
Denotational semantics of expressions & commands
clasohm@924
     7
*)
clasohm@924
     8
clasohm@924
     9
Denotation = Com + 
clasohm@924
    10
clasohm@924
    11
types com_den = "(state*state)set"
clasohm@924
    12
consts
clasohm@1374
    13
  A     :: aexp => state => nat
clasohm@1374
    14
  B     :: bexp => state => bool
clasohm@1374
    15
  C     :: com => com_den
clasohm@1374
    16
  Gamma :: [bexp,com_den] => (com_den => com_den)
clasohm@924
    17
clasohm@924
    18
primrec A aexp
clasohm@924
    19
  A_nat	"A(N(n)) = (%s. n)"
clasohm@924
    20
  A_loc	"A(X(x)) = (%s. s(x))" 
clasohm@924
    21
  A_op1	"A(Op1 f a) = (%s. f(A a s))"
clasohm@924
    22
  A_op2	"A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
clasohm@924
    23
clasohm@924
    24
primrec B bexp
clasohm@924
    25
  B_true  "B(true) = (%s. True)"
clasohm@924
    26
  B_false "B(false) = (%s. False)"
clasohm@924
    27
  B_op	  "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
clasohm@924
    28
  B_not	  "B(noti(b)) = (%s. ~(B b s))"
clasohm@924
    29
  B_and	  "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
clasohm@924
    30
  B_or	  "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
clasohm@924
    31
clasohm@924
    32
defs
clasohm@1151
    33
  Gamma_def	"Gamma b cd ==   
clasohm@1151
    34
		   (%phi.{st. st : (phi O cd) & B b (fst st)} Un 
clasohm@1151
    35
	                 {st. st : id & ~B b (fst st)})"
clasohm@924
    36
clasohm@924
    37
primrec C com
clasohm@924
    38
  C_skip    "C(skip) = id"
clasohm@924
    39
  C_assign  "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
clasohm@924
    40
  C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
clasohm@1151
    41
  C_if	    "C(ifc b then c0 else c1) =   
clasohm@1151
    42
		   {st. st:C(c0) & (B b (fst st))} Un 
clasohm@1151
    43
	           {st. st:C(c1) & ~(B b (fst st))}"
clasohm@924
    44
  C_while   "C(while b do c) = lfp (Gamma b (C c))"
clasohm@924
    45
clasohm@924
    46
end