|
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 |