src/HOL/IMP/Transition.thy
author oheimb
Tue Jul 04 10:54:46 2000 +0200 (2000-07-04)
changeset 9241 f961c1fdff50
parent 8029 05446a898852
child 9364 e783491b9a1f
permissions -rw-r--r--
disambiguated := ; added Examples (factorial)
     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 +
    10 
    11 consts  evalc1    :: "((com*state)*(com*state))set"
    12 
    13 syntax
    14         "@evalc1" :: "[(com*state),(com*state)] => bool"
    15                                 ("_ -1-> _" [81,81] 100)
    16         "@evalcn" :: "[(com*state),nat,(com*state)] => bool"
    17                                 ("_ -_-> _" [81,81] 100)
    18         "@evalc*" :: "[(com*state),(com*state)] => bool"
    19                                 ("_ -*-> _" [81,81] 100)
    20 
    21 translations
    22   "cs0 -1-> cs1"	== "(cs0,cs1) : evalc1"
    23   "cs0 -1-> (c1,s1)"	<= "cs0 -1-> (_args c1 s1)"
    24 
    25   "cs0 -n-> cs1" 	== "(cs0,cs1) : evalc1^n"
    26   "cs0 -n-> (c1,s1)" 	<= "cs0 -n-> (_args c1 s1)"
    27 
    28   "cs0 -*-> cs1" 	== "(cs0,cs1) : evalc1^*"
    29   "cs0 -*-> (c1,s1)" 	<= "cs0 -*-> (_args c1 s1)"
    30 
    31 
    32 inductive evalc1
    33   intrs
    34     Assign "(x :== a,s) -1-> (SKIP,s[x ::= a s])"
    35 
    36     Semi1   "(SKIP;c,s) -1-> (c,s)"     
    37     Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
    38 
    39     IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"
    40     IfFalse "~b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c2,s)"
    41 
    42     WhileFalse "~b s ==> (WHILE b DO c,s) -1-> (SKIP,s)"
    43     WhileTrue "b s ==> (WHILE b DO c,s) -1-> (c;WHILE b DO c,s)"
    44 
    45 end