src/HOL/IMP/Transition.thy
author nipkow
Wed May 06 11:46:00 1998 +0200 (1998-05-06)
changeset 4897 be11be0b6ea1
parent 4757 02b86e36e98f
child 4906 0537ee95d004
permissions -rw-r--r--
Changed [/] to [:=] and removed actual definition.
nipkow@1700
     1
(*  Title:      HOL/IMP/Transition.thy
nipkow@1700
     2
    ID:         $Id$
nipkow@1700
     3
    Author:     Tobias Nipkow & Robert Sandner, TUM
nipkow@1700
     4
    Copyright   1996 TUM
nipkow@1700
     5
nipkow@1700
     6
Transition semantics of commands
nipkow@1700
     7
*)
nipkow@1700
     8
nipkow@1700
     9
Transition = Natural + RelPow +
nipkow@1700
    10
nipkow@1700
    11
consts  evalc1    :: "((com*state)*(com*state))set"        
nipkow@1700
    12
	"@evalc1" :: "[(com*state),(com*state)] => bool"   
nipkow@1700
    13
				("_ -1-> _" [81,81] 100)
nipkow@1700
    14
	"@evalcn" :: "[(com*state),(com*state)] => nat => bool"
nipkow@1701
    15
				("_ -_-> _" [81,81] 100)
nipkow@1700
    16
	"@evalc*" :: "[(com*state),(com*state)] => bool"   
nipkow@1700
    17
				("_ -*-> _" [81,81] 100)
nipkow@1700
    18
nipkow@1700
    19
translations
nipkow@1700
    20
       	"cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
oheimb@4757
    21
	"cs0 -n-> cs1" == "(cs0,cs1) : evalc1^n"
oheimb@4757
    22
	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1^*"
nipkow@1700
    23
nipkow@1700
    24
paulson@1789
    25
inductive evalc1
nipkow@1700
    26
  intrs
nipkow@4897
    27
    Assign "(x := a,s) -1-> (SKIP,s[x := a s])"
nipkow@1700
    28
nipkow@1700
    29
    Semi1   "(SKIP;c,s) -1-> (c,s)"	
nipkow@1700
    30
    Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
nipkow@1700
    31
nipkow@1700
    32
    IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"
nipkow@1700
    33
    IfFalse "~b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c2,s)"
nipkow@1700
    34
nipkow@1700
    35
    WhileFalse "~b s ==> (WHILE b DO c,s) -1-> (SKIP,s)"
nipkow@1700
    36
    WhileTrue "b s ==> (WHILE b DO c,s) -1-> (c;WHILE b DO c,s)"
nipkow@1700
    37
nipkow@1700
    38
end