src/HOL/IMP/Natural.thy

Quotes now optional around inductive set

(*  Title:      HOL/IMP/Natural.thy
    ID:         $Id$
    Author:     Tobias Nipkow & Robert Sandner, TUM
    Copyright   1996 TUM

Natural semantics of commands
*)

Natural = Com +

(** Execution of commands **)
consts  evalc    :: "(com*state*state)set"
        "@evalc" :: [com,state,state] => bool ("<_,_>/ -c-> _" [0,0,50] 50)

translations  "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"

constdefs assign :: [state,val,loc] => state    ("_[_'/_]" [95,0,0] 95)
  "s[m/x] ==  (%y. if y=x then m else s y)"


inductive evalc
  intrs
    Skip    "<SKIP,s> -c-> s"

    Assign  "<x := a,s> -c-> s[a(s)/x]"

    Semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] 
            ==> <c0 ; c1, s> -c-> s1"

    IfTrue "[| b s; <c0,s> -c-> s1 |] 
            ==> <IF b THEN c0 ELSE c1, s> -c-> s1"

    IfFalse "[| ~b s; <c1,s> -c-> s1 |] 
             ==> <IF b THEN c0 ELSE c1, s> -c-> s1"

    WhileFalse "~b s ==> <WHILE b DO c,s> -c-> s"

    WhileTrue  "[| b s;  <c,s> -c-> s2;  <WHILE b DO c, s2> -c-> s1 |] 
               ==> <WHILE b DO c, s> -c-> s1"

end