|
1700
|
1 |
(* Title: HOL/IMP/Transition.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow & Robert Sandner, TUM
|
|
|
4 |
Copyright 1996 TUM
|
|
|
5 |
|
|
|
6 |
Transition semantics of commands
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Transition = Natural + RelPow +
|
|
|
10 |
|
|
|
11 |
consts evalc1 :: "((com*state)*(com*state))set"
|
|
|
12 |
"@evalc1" :: "[(com*state),(com*state)] => bool"
|
|
|
13 |
("_ -1-> _" [81,81] 100)
|
|
|
14 |
"@evalcn" :: "[(com*state),(com*state)] => nat => bool"
|
|
1701
|
15 |
("_ -_-> _" [81,81] 100)
|
|
1700
|
16 |
"@evalc*" :: "[(com*state),(com*state)] => bool"
|
|
|
17 |
("_ -*-> _" [81,81] 100)
|
|
|
18 |
|
|
|
19 |
translations
|
|
|
20 |
"cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
|
|
4757
|
21 |
"cs0 -n-> cs1" == "(cs0,cs1) : evalc1^n"
|
|
|
22 |
"cs0 -*-> cs1" == "(cs0,cs1) : evalc1^*"
|
|
1700
|
23 |
|
|
|
24 |
|
|
1789
|
25 |
inductive evalc1
|
|
1700
|
26 |
intrs
|
|
|
27 |
Assign "(x := a,s) -1-> (SKIP,s[a s / x])"
|
|
|
28 |
|
|
|
29 |
Semi1 "(SKIP;c,s) -1-> (c,s)"
|
|
|
30 |
Semi2 "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
|
|
|
31 |
|
|
|
32 |
IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"
|
|
|
33 |
IfFalse "~b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c2,s)"
|
|
|
34 |
|
|
|
35 |
WhileFalse "~b s ==> (WHILE b DO c,s) -1-> (SKIP,s)"
|
|
|
36 |
WhileTrue "b s ==> (WHILE b DO c,s) -1-> (c;WHILE b DO c,s)"
|
|
|
37 |
|
|
|
38 |
end
|