src/ZF/IMP/Denotation.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 6047 f2e0938ba38d
     1.1 --- a/src/ZF/IMP/Denotation.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/IMP/Denotation.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	ZF/IMP/Denotation.thy
     1.5 +(*  Title:      ZF/IMP/Denotation.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     1.8 +    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     1.9      Copyright   1994 TUM
    1.10  
    1.11  Denotational semantics of expressions & commands
    1.12 @@ -14,33 +14,33 @@
    1.13    C     :: i => i
    1.14    Gamma :: [i,i,i] => i
    1.15  
    1.16 -rules	(*NOT definitional*)
    1.17 -  A_nat_def	"A(N(n)) == (%sigma. n)"
    1.18 -  A_loc_def	"A(X(x)) == (%sigma. sigma`x)" 
    1.19 -  A_op1_def	"A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
    1.20 -  A_op2_def	"A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
    1.21 +rules   (*NOT definitional*)
    1.22 +  A_nat_def     "A(N(n)) == (%sigma. n)"
    1.23 +  A_loc_def     "A(X(x)) == (%sigma. sigma`x)" 
    1.24 +  A_op1_def     "A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
    1.25 +  A_op2_def     "A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
    1.26  
    1.27  
    1.28 -  B_true_def	"B(true) == (%sigma. 1)"
    1.29 -  B_false_def	"B(false) == (%sigma. 0)"
    1.30 -  B_op_def	"B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)" 
    1.31 +  B_true_def    "B(true) == (%sigma. 1)"
    1.32 +  B_false_def   "B(false) == (%sigma. 0)"
    1.33 +  B_op_def      "B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)" 
    1.34  
    1.35  
    1.36 -  B_not_def	"B(noti(b)) == (%sigma. not(B(b,sigma)))"
    1.37 -  B_and_def	"B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))"
    1.38 -  B_or_def	"B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
    1.39 +  B_not_def     "B(noti(b)) == (%sigma. not(B(b,sigma)))"
    1.40 +  B_and_def     "B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))"
    1.41 +  B_or_def      "B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
    1.42  
    1.43 -  C_skip_def	"C(skip) == id(loc->nat)"
    1.44 -  C_assign_def	"C(x := a) == {io:(loc->nat)*(loc->nat). 
    1.45 -			       snd(io) = fst(io)[A(a,fst(io))/x]}"
    1.46 +  C_skip_def    "C(skip) == id(loc->nat)"
    1.47 +  C_assign_def  "C(x := a) == {io:(loc->nat)*(loc->nat). 
    1.48 +                               snd(io) = fst(io)[A(a,fst(io))/x]}"
    1.49  
    1.50 -  C_comp_def	"C(c0 ; c1) == C(c1) O C(c0)"
    1.51 -  C_if_def	"C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un 
    1.52 -			 	             {io:C(c1). B(b,fst(io))=0}"
    1.53 +  C_comp_def    "C(c0 ; c1) == C(c1) O C(c0)"
    1.54 +  C_if_def      "C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un 
    1.55 +                                             {io:C(c1). B(b,fst(io))=0}"
    1.56  
    1.57 -  Gamma_def	"Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un 
    1.58 -			 	     {io : id(loc->nat). B(b,fst(io))=0})"
    1.59 +  Gamma_def     "Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un 
    1.60 +                                     {io : id(loc->nat). B(b,fst(io))=0})"
    1.61  
    1.62 -  C_while_def	"C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
    1.63 +  C_while_def   "C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
    1.64  
    1.65  end