1700
|
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 |
|
1789
|
21 |
inductive evalc
|
1700
|
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
|