8177

1 
(* Title: HOL/IMPP/Natural.thy


2 
ID: $Id$


3 
Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM


4 
Copyright 1999 TUM


5 
*)


6 

17477

7 
header {* Natural semantics of commands *}


8 


9 
theory Natural


10 
imports Com


11 
begin

8177

12 


13 
(** Execution of commands **)

17477

14 
consts


15 
evalc :: "(com * state * state) set"


16 
evaln :: "(com * state * nat * state) set"

8177

17 

17477

18 
syntax


19 
"@evalc":: "[com,state, state] => bool" ("<_,_>/ c> _" [0,0, 51] 51)


20 
"@evaln":: "[com,state,nat,state] => bool" ("<_,_>/ _> _" [0,0,0,51] 51)


21 


22 
translations


23 
"<c,s> c> s'" == "(c,s, s') : evalc"


24 
"<c,s> n> s'" == "(c,s,n,s') : evaln"

8177

25 


26 
consts


27 
newlocs :: locals

17477

28 
setlocs :: "state => locals => state"


29 
getlocs :: "state => locals"


30 
update :: "state => vname => val => state" ("_/[_/::=/_]" [900,0,0] 900)

8177

31 
syntax (* IN Natural.thy *)

17477

32 
loc :: "state => locals" ("_<_>" [75,0] 75)

8177

33 
translations


34 
"s<X>" == "getlocs s X"


35 


36 
inductive evalc

17477

37 
intros


38 
Skip: "<SKIP,s> c> s"

8177

39 

17477

40 
Assign: "<X :== a,s> c> s[X::=a s]"

8177

41 

17477

42 
Local: "<c, s0[Loc Y::= a s0]> c> s1 ==>


43 
<LOCAL Y := a IN c, s0> c> s1[Loc Y::=s0<Y>]"

8177

44 

17477

45 
Semi: "[ <c0,s0> c> s1; <c1,s1> c> s2 ] ==>


46 
<c0;; c1, s0> c> s2"

8177

47 

17477

48 
IfTrue: "[ b s; <c0,s> c> s1 ] ==>


49 
<IF b THEN c0 ELSE c1, s> c> s1"

8177

50 

17477

51 
IfFalse: "[ ~b s; <c1,s> c> s1 ] ==>


52 
<IF b THEN c0 ELSE c1, s> c> s1"

8177

53 

17477

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

8177

55 

17477

56 
WhileTrue: "[ b s0; <c,s0> c> s1; <WHILE b DO c, s1> c> s2 ] ==>


57 
<WHILE b DO c, s0> c> s2"

8177

58 

17477

59 
Body: "<the (body pn), s0> c> s1 ==>


60 
<BODY pn, s0> c> s1"

8177

61 

17477

62 
Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> c> s1 ==>


63 
<X:=CALL pn(a), s0> c> (setlocs s1 (getlocs s0))


64 
[X::=s1<Res>]"

8177

65 


66 
inductive evaln

17477

67 
intros


68 
Skip: "<SKIP,s> n> s"


69 


70 
Assign: "<X :== a,s> n> s[X::=a s]"

8177

71 

17477

72 
Local: "<c, s0[Loc Y::= a s0]> n> s1 ==>


73 
<LOCAL Y := a IN c, s0> n> s1[Loc Y::=s0<Y>]"


74 


75 
Semi: "[ <c0,s0> n> s1; <c1,s1> n> s2 ] ==>


76 
<c0;; c1, s0> n> s2"

8177

77 

17477

78 
IfTrue: "[ b s; <c0,s> n> s1 ] ==>


79 
<IF b THEN c0 ELSE c1, s> n> s1"

8177

80 

17477

81 
IfFalse: "[ ~b s; <c1,s> n> s1 ] ==>


82 
<IF b THEN c0 ELSE c1, s> n> s1"

8177

83 

17477

84 
WhileFalse: "~b s ==> <WHILE b DO c,s> n> s"


85 


86 
WhileTrue: "[ b s0; <c,s0> n> s1; <WHILE b DO c, s1> n> s2 ] ==>


87 
<WHILE b DO c, s0> n> s2"

8177

88 

17477

89 
Body: "<the (body pn), s0>  n> s1 ==>


90 
<BODY pn, s0> Suc n> s1"

8177

91 

17477

92 
Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> n> s1 ==>


93 
<X:=CALL pn(a), s0> n> (setlocs s1 (getlocs s0))


94 
[X::=s1<Res>]"

8177

95 


96 

17477

97 
inductive_cases evalc_elim_cases:


98 
"<SKIP,s> c> t" "<X:==a,s> c> t" "<LOCAL Y:=a IN c,s> c> t"


99 
"<c1;;c2,s> c> t" "<IF b THEN c1 ELSE c2,s> c> t"


100 
"<BODY P,s> c> s1" "<X:=CALL P(a),s> c> s1"

8177

101 

17477

102 
inductive_cases evaln_elim_cases:


103 
"<SKIP,s> n> t" "<X:==a,s> n> t" "<LOCAL Y:=a IN c,s> n> t"


104 
"<c1;;c2,s> n> t" "<IF b THEN c1 ELSE c2,s> n> t"


105 
"<BODY P,s> n> s1" "<X:=CALL P(a),s> n> s1"


106 


107 
inductive_cases evalc_WHILE_case: "<WHILE b DO c,s> c> t"


108 
inductive_cases evaln_WHILE_case: "<WHILE b DO c,s> n> t"


109 


110 
ML {* use_legacy_bindings (the_context ()) *}


111 

8177

112 
end
