src/HOL/IMP/Transition.thy
changeset 1700 afd3b60660db
child 1701 a26fbeaaaabd
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IMP/Transition.thy	Mon Apr 29 15:48:27 1996 +0200
     1.3 @@ -0,0 +1,40 @@
     1.4 +(*  Title:      HOL/IMP/Transition.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow & Robert Sandner, TUM
     1.7 +    Copyright   1996 TUM
     1.8 +
     1.9 +Transition semantics of commands
    1.10 +*)
    1.11 +
    1.12 +Transition = Natural + RelPow +
    1.13 +
    1.14 +consts  evalc1    :: "((com*state)*(com*state))set"        
    1.15 +	"@evalc1" :: "[(com*state),(com*state)] => bool"   
    1.16 +				("_ -1-> _" [81,81] 100)
    1.17 +	"@evalcn" :: "[(com*state),(com*state)] => nat => bool"
    1.18 +				("_ -(_)-> _" [81,81] 100)
    1.19 +	"@evalc*" :: "[(com*state),(com*state)] => bool"   
    1.20 +				("_ -*-> _" [81,81] 100)
    1.21 +
    1.22 +translations
    1.23 +       	"cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
    1.24 +        "x -(n)-> (y,z)" == "(x,y,z) : evalc1 ^ n" 
    1.25 +	"cs0 -(n)-> cs1" == "(cs0,cs1) : evalc1 ^ n"
    1.26 +	"x -*-> (y,z)" == "(x,y,z) : evalc1 ^*" 
    1.27 +	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1 ^*"
    1.28 +
    1.29 +
    1.30 +inductive "evalc1"
    1.31 +  intrs
    1.32 +    Assign "(x := a,s) -1-> (SKIP,s[a s / x])"
    1.33 +
    1.34 +    Semi1   "(SKIP;c,s) -1-> (c,s)"	
    1.35 +    Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
    1.36 +
    1.37 +    IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"
    1.38 +    IfFalse "~b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c2,s)"
    1.39 +
    1.40 +    WhileFalse "~b s ==> (WHILE b DO c,s) -1-> (SKIP,s)"
    1.41 +    WhileTrue "b s ==> (WHILE b DO c,s) -1-> (c;WHILE b DO c,s)"
    1.42 +
    1.43 +end