src/HOL/IMP/Transition.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1789 aade046ec6d5
child 4757 02b86e36e98f
permissions -rw-r--r--
Dep. on Provers/nat_transitive
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@1701
    20
        "x -1-> (y,z)" == "(x,y,z) : evalc1" 
nipkow@1700
    21
       	"cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
nipkow@1701
    22
        "x -n-> (y,z)" == "(x,y,z) : evalc1 ^ n" 
nipkow@1701
    23
	"cs0 -n-> cs1" == "(cs0,cs1) : evalc1 ^ n"
nipkow@1700
    24
	"x -*-> (y,z)" == "(x,y,z) : evalc1 ^*" 
nipkow@1700
    25
	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1 ^*"
nipkow@1700
    26
nipkow@1700
    27
paulson@1789
    28
inductive evalc1
nipkow@1700
    29
  intrs
nipkow@1700
    30
    Assign "(x := a,s) -1-> (SKIP,s[a s / x])"
nipkow@1700
    31
nipkow@1700
    32
    Semi1   "(SKIP;c,s) -1-> (c,s)"	
nipkow@1700
    33
    Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
nipkow@1700
    34
nipkow@1700
    35
    IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"
nipkow@1700
    36
    IfFalse "~b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c2,s)"
nipkow@1700
    37
nipkow@1700
    38
    WhileFalse "~b s ==> (WHILE b DO c,s) -1-> (SKIP,s)"
nipkow@1700
    39
    WhileTrue "b s ==> (WHILE b DO c,s) -1-> (c;WHILE b DO c,s)"
nipkow@1700
    40
nipkow@1700
    41
end