src/HOL/IMP/Transition.thy
author oheimb
Mon Mar 30 21:03:14 1998 +0200 (1998-03-30)
changeset 4757 02b86e36e98f
parent 1789 aade046ec6d5
child 4897 be11be0b6ea1
permissions -rw-r--r--
removed superfluous translations
     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 	"cs0 -n-> cs1" == "(cs0,cs1) : evalc1^n"
    22 	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1^*"
    23 
    24 
    25 inductive evalc1
    26   intrs
    27     Assign "(x := a,s) -1-> (SKIP,s[a s / x])"
    28 
    29     Semi1   "(SKIP;c,s) -1-> (c,s)"	
    30     Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
    31 
    32     IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"
    33     IfFalse "~b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c2,s)"
    34 
    35     WhileFalse "~b s ==> (WHILE b DO c,s) -1-> (SKIP,s)"
    36     WhileTrue "b s ==> (WHILE b DO c,s) -1-> (c;WHILE b DO c,s)"
    37 
    38 end