src/HOL/IMP/Transition.thy
author paulson
Thu Jun 06 14:39:44 1996 +0200 (1996-06-06)
changeset 1789 aade046ec6d5
parent 1701 a26fbeaaaabd
child 4757 02b86e36e98f
permissions -rw-r--r--
Quotes now optional around inductive set
     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         "x -1-> (y,z)" == "(x,y,z) : evalc1" 
    21        	"cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
    22         "x -n-> (y,z)" == "(x,y,z) : evalc1 ^ n" 
    23 	"cs0 -n-> cs1" == "(cs0,cs1) : evalc1 ^ n"
    24 	"x -*-> (y,z)" == "(x,y,z) : evalc1 ^*" 
    25 	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1 ^*"
    26 
    27 
    28 inductive evalc1
    29   intrs
    30     Assign "(x := a,s) -1-> (SKIP,s[a s / x])"
    31 
    32     Semi1   "(SKIP;c,s) -1-> (c,s)"	
    33     Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
    34 
    35     IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"
    36     IfFalse "~b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c2,s)"
    37 
    38     WhileFalse "~b s ==> (WHILE b DO c,s) -1-> (SKIP,s)"
    39     WhileTrue "b s ==> (WHILE b DO c,s) -1-> (c;WHILE b DO c,s)"
    40 
    41 end