src/HOL/IMP/Transition.thy
author nipkow
Wed Nov 24 12:12:36 1999 +0100 (1999-11-24)
changeset 8029 05446a898852
parent 5855 9be441c17f6d
child 9241 f961c1fdff50
permissions -rw-r--r--
Basis now Main.
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@8029
     9
Transition = Natural +
nipkow@1700
    10
wenzelm@4906
    11
consts  evalc1    :: "((com*state)*(com*state))set"
wenzelm@4906
    12
wenzelm@4906
    13
syntax
wenzelm@4906
    14
        "@evalc1" :: "[(com*state),(com*state)] => bool"
wenzelm@4906
    15
                                ("_ -1-> _" [81,81] 100)
paulson@5855
    16
        "@evalcn" :: "[(com*state),nat,(com*state)] => bool"
wenzelm@4906
    17
                                ("_ -_-> _" [81,81] 100)
wenzelm@4906
    18
        "@evalc*" :: "[(com*state),(com*state)] => bool"
wenzelm@4906
    19
                                ("_ -*-> _" [81,81] 100)
nipkow@1700
    20
nipkow@1700
    21
translations
wenzelm@4906
    22
  "cs0 -1-> cs1"	== "(cs0,cs1) : evalc1"
wenzelm@4906
    23
  "cs0 -1-> (c1,s1)"	<= "cs0 -1-> (_args c1 s1)"
wenzelm@4906
    24
wenzelm@4906
    25
  "cs0 -n-> cs1" 	== "(cs0,cs1) : evalc1^n"
wenzelm@4906
    26
  "cs0 -n-> (c1,s1)" 	<= "cs0 -n-> (_args c1 s1)"
wenzelm@4906
    27
wenzelm@4906
    28
  "cs0 -*-> cs1" 	== "(cs0,cs1) : evalc1^*"
wenzelm@4906
    29
  "cs0 -*-> (c1,s1)" 	<= "cs0 -*-> (_args c1 s1)"
nipkow@1700
    30
nipkow@1700
    31
paulson@1789
    32
inductive evalc1
nipkow@1700
    33
  intrs
nipkow@4897
    34
    Assign "(x := a,s) -1-> (SKIP,s[x := a s])"
nipkow@1700
    35
wenzelm@4906
    36
    Semi1   "(SKIP;c,s) -1-> (c,s)"     
nipkow@1700
    37
    Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
nipkow@1700
    38
nipkow@1700
    39
    IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"
nipkow@1700
    40
    IfFalse "~b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c2,s)"
nipkow@1700
    41
nipkow@1700
    42
    WhileFalse "~b s ==> (WHILE b DO c,s) -1-> (SKIP,s)"
nipkow@1700
    43
    WhileTrue "b s ==> (WHILE b DO c,s) -1-> (c;WHILE b DO c,s)"
nipkow@1700
    44
nipkow@1700
    45
end