src/HOL/IMP/Transition.thy
author nipkow
Mon Apr 29 15:48:27 1996 +0200 (1996-04-29)
changeset 1700 afd3b60660db
child 1701 a26fbeaaaabd
permissions -rw-r--r--
Natural and Transition semantics.
     1 (*  Title:      HOL/IMP/Transition.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Robert Sandner, TUM
     4     Copyright   1996 TUM
     5 
     6 Transition semantics of commands
     7 *)
     8 
     9 Transition = Natural + RelPow +
    10 
    11 consts  evalc1    :: "((com*state)*(com*state))set"        
    12 	"@evalc1" :: "[(com*state),(com*state)] => bool"   
    13 				("_ -1-> _" [81,81] 100)
    14 	"@evalcn" :: "[(com*state),(com*state)] => nat => bool"
    15 				("_ -(_)-> _" [81,81] 100)
    16 	"@evalc*" :: "[(com*state),(com*state)] => bool"   
    17 				("_ -*-> _" [81,81] 100)
    18 
    19 translations
    20        	"cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
    21         "x -(n)-> (y,z)" == "(x,y,z) : evalc1 ^ n" 
    22 	"cs0 -(n)-> cs1" == "(cs0,cs1) : evalc1 ^ n"
    23 	"x -*-> (y,z)" == "(x,y,z) : evalc1 ^*" 
    24 	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1 ^*"
    25 
    26 
    27 inductive "evalc1"
    28   intrs
    29     Assign "(x := a,s) -1-> (SKIP,s[a s / x])"
    30 
    31     Semi1   "(SKIP;c,s) -1-> (c,s)"	
    32     Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
    33 
    34     IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"
    35     IfFalse "~b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c2,s)"
    36 
    37     WhileFalse "~b s ==> (WHILE b DO c,s) -1-> (SKIP,s)"
    38     WhileTrue "b s ==> (WHILE b DO c,s) -1-> (c;WHILE b DO c,s)"
    39 
    40 end