src/HOL/IMP/Natural.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1789 aade046ec6d5
child 4897 be11be0b6ea1
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     1 (*  Title:      HOL/IMP/Natural.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Robert Sandner, TUM
     4     Copyright   1996 TUM
     5 
     6 Natural semantics of commands
     7 *)
     8 
     9 Natural = Com +
    10 
    11 (** Execution of commands **)
    12 consts  evalc    :: "(com*state*state)set"
    13         "@evalc" :: [com,state,state] => bool ("<_,_>/ -c-> _" [0,0,50] 50)
    14 
    15 translations  "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
    16 
    17 constdefs assign :: [state,val,loc] => state    ("_[_'/_]" [95,0,0] 95)
    18   "s[m/x] ==  (%y. if y=x then m else s y)"
    19 
    20 
    21 inductive evalc
    22   intrs
    23     Skip    "<SKIP,s> -c-> s"
    24 
    25     Assign  "<x := a,s> -c-> s[a(s)/x]"
    26 
    27     Semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] 
    28             ==> <c0 ; c1, s> -c-> s1"
    29 
    30     IfTrue "[| b s; <c0,s> -c-> s1 |] 
    31             ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
    32 
    33     IfFalse "[| ~b s; <c1,s> -c-> s1 |] 
    34              ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
    35 
    36     WhileFalse "~b s ==> <WHILE b DO c,s> -c-> s"
    37 
    38     WhileTrue  "[| b s;  <c,s> -c-> s2;  <WHILE b DO c, s2> -c-> s1 |] 
    39                ==> <WHILE b DO c, s> -c-> s1"
    40 
    41 end