author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45415  bf39b07a7a8e 
child 47818  151d137f1095 
permissions  rwrr 
43141  1 
header "SmallStep Semantics of Commands" 
2 

3 
theory Small_Step imports Star Big_Step begin 

4 

5 
subsection "The transition relation" 

6 

45415
bf39b07a7a8e
more fragments to export, removed the one from Com
kleing
parents:
45265
diff
changeset

7 
text_raw{*\begin{isaverbatimwrite}\newcommand{\SmallStepDef}{% *} 
43141  8 
inductive 
9 
small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55) 

10 
where 

11 
Assign: "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))"  

12 

13 
Semi1: "(SKIP;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)"  

14 
Semi2: "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';c\<^isub>2,s')"  

15 

16 
IfTrue: "bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)"  

17 
IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)"  

18 

19 
While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)" 

45415
bf39b07a7a8e
more fragments to export, removed the one from Com
kleing
parents:
45265
diff
changeset

20 
text_raw{*}\end{isaverbatimwrite}*} 
43141  21 

22 

23 
abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55) 

24 
where "x \<rightarrow>* y == star small_step x y" 

25 

26 
subsection{* Executability *} 

27 

28 
code_pred small_step . 

29 

30 
values "{(c',map t [''x'',''y'',''z'']) c' t. 

31 
(''x'' ::= V ''z''; ''y'' ::= V ''x'', 

44036  32 
<''x'' := 3, ''y'' := 7, ''z'' := 5>) \<rightarrow>* (c',t)}" 
43141  33 

34 

35 
subsection{* Proof infrastructure *} 

36 

37 
subsubsection{* Induction rules *} 

38 

39 
text{* The default induction rule @{thm[source] small_step.induct} only works 

40 
for lemmas of the form @{text"a \<rightarrow> b \<Longrightarrow> \<dots>"} where @{text a} and @{text b} are 

41 
not already pairs @{text"(DUMMY,DUMMY)"}. We can generate a suitable variant 

42 
of @{thm[source] small_step.induct} for pairs by ``splitting'' the arguments 

43 
@{text"\<rightarrow>"} into pairs: *} 

44 
lemmas small_step_induct = small_step.induct[split_format(complete)] 

45 

46 

47 
subsubsection{* Proof automation *} 

48 

49 
declare small_step.intros[simp,intro] 

50 

51 
text{* Rule inversion: *} 

52 

53 
inductive_cases SkipE[elim!]: "(SKIP,s) \<rightarrow> ct" 

54 
thm SkipE 

55 
inductive_cases AssignE[elim!]: "(x::=a,s) \<rightarrow> ct" 

56 
thm AssignE 

57 
inductive_cases SemiE[elim]: "(c1;c2,s) \<rightarrow> ct" 

58 
thm SemiE 

59 
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<rightarrow> ct" 

60 
inductive_cases WhileE[elim]: "(WHILE b DO c, s) \<rightarrow> ct" 

61 

62 

63 
text{* A simple property: *} 

64 
lemma deterministic: 

65 
"cs \<rightarrow> cs' \<Longrightarrow> cs \<rightarrow> cs'' \<Longrightarrow> cs'' = cs'" 

45015  66 
apply(induction arbitrary: cs'' rule: small_step.induct) 
43141  67 
apply blast+ 
68 
done 

69 

70 

71 
subsection "Equivalence with bigstep semantics" 

72 

73 
lemma star_semi2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')" 

45015  74 
proof(induction rule: star_induct) 
43141  75 
case refl thus ?case by simp 
76 
next 

77 
case step 

78 
thus ?case by (metis Semi2 star.step) 

79 
qed 

80 

81 
lemma semi_comp: 

82 
"\<lbrakk> (c1,s1) \<rightarrow>* (SKIP,s2); (c2,s2) \<rightarrow>* (SKIP,s3) \<rbrakk> 

83 
\<Longrightarrow> (c1;c2, s1) \<rightarrow>* (SKIP,s3)" 

84 
by(blast intro: star.step star_semi2 star_trans) 

85 

86 
text{* The following proof corresponds to one on the board where one would 

45218  87 
show chains of @{text "\<rightarrow>"} and @{text "\<rightarrow>*"} steps. *} 
43141  88 

89 
lemma big_to_small: 

90 
"cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)" 

45015  91 
proof (induction rule: big_step.induct) 
43141  92 
fix s show "(SKIP,s) \<rightarrow>* (SKIP,s)" by simp 
93 
next 

94 
fix x a s show "(x ::= a,s) \<rightarrow>* (SKIP, s(x := aval a s))" by auto 

95 
next 

96 
fix c1 c2 s1 s2 s3 

97 
assume "(c1,s1) \<rightarrow>* (SKIP,s2)" and "(c2,s2) \<rightarrow>* (SKIP,s3)" 

98 
thus "(c1;c2, s1) \<rightarrow>* (SKIP,s3)" by (rule semi_comp) 

99 
next 

100 
fix s::state and b c0 c1 t 

101 
assume "bval b s" 

102 
hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c0,s)" by simp 

45218  103 
moreover assume "(c0,s) \<rightarrow>* (SKIP,t)" 
104 
ultimately 

105 
show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" by (metis star.simps) 

43141  106 
next 
107 
fix s::state and b c0 c1 t 

108 
assume "\<not>bval b s" 

109 
hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c1,s)" by simp 

45218  110 
moreover assume "(c1,s) \<rightarrow>* (SKIP,t)" 
111 
ultimately 

112 
show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" by (metis star.simps) 

43141  113 
next 
114 
fix b c and s::state 

115 
assume b: "\<not>bval b s" 

116 
let ?if = "IF b THEN c; WHILE b DO c ELSE SKIP" 

117 
have "(WHILE b DO c,s) \<rightarrow> (?if, s)" by blast 

45218  118 
moreover have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b) 
45265  119 
ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by(metis star.refl star.step) 
43141  120 
next 
121 
fix b c s s' t 

122 
let ?w = "WHILE b DO c" 

123 
let ?if = "IF b THEN c; ?w ELSE SKIP" 

124 
assume w: "(?w,s') \<rightarrow>* (SKIP,t)" 

125 
assume c: "(c,s) \<rightarrow>* (SKIP,s')" 

126 
assume b: "bval b s" 

127 
have "(?w,s) \<rightarrow> (?if, s)" by blast 

45218  128 
moreover have "(?if, s) \<rightarrow> (c; ?w, s)" by (simp add: b) 
129 
moreover have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule semi_comp[OF c w]) 

130 
ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by (metis star.simps) 

43141  131 
qed 
132 

133 
text{* Each case of the induction can be proved automatically: *} 

134 
lemma "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)" 

45015  135 
proof (induction rule: big_step.induct) 
43141  136 
case Skip show ?case by blast 
137 
next 

138 
case Assign show ?case by blast 

139 
next 

140 
case Semi thus ?case by (blast intro: semi_comp) 

141 
next 

45265  142 
case IfTrue thus ?case by (blast intro: star.step) 
43141  143 
next 
45265  144 
case IfFalse thus ?case by (blast intro: star.step) 
43141  145 
next 
146 
case WhileFalse thus ?case 

45265  147 
by (metis star.step star_step1 small_step.IfFalse small_step.While) 
43141  148 
next 
149 
case WhileTrue 

150 
thus ?case 

45265  151 
by(metis While semi_comp small_step.IfTrue star.step[of small_step]) 
43141  152 
qed 
153 

154 
lemma small1_big_continue: 

155 
"cs \<rightarrow> cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t" 

45015  156 
apply (induction arbitrary: t rule: small_step.induct) 
43141  157 
apply auto 
158 
done 

159 

160 
lemma small_big_continue: 

161 
"cs \<rightarrow>* cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t" 

45015  162 
apply (induction rule: star.induct) 
43141  163 
apply (auto intro: small1_big_continue) 
164 
done 

165 

166 
lemma small_to_big: "cs \<rightarrow>* (SKIP,t) \<Longrightarrow> cs \<Rightarrow> t" 

167 
by (metis small_big_continue Skip) 

168 

169 
text {* 

170 
Finally, the equivalence theorem: 

171 
*} 

172 
theorem big_iff_small: 

173 
"cs \<Rightarrow> t = cs \<rightarrow>* (SKIP,t)" 

174 
by(metis big_to_small small_to_big) 

175 

176 

177 
subsection "Final configurations and infinite reductions" 

178 

179 
definition "final cs \<longleftrightarrow> \<not>(EX cs'. cs \<rightarrow> cs')" 

180 

181 
lemma finalD: "final (c,s) \<Longrightarrow> c = SKIP" 

182 
apply(simp add: final_def) 

45015  183 
apply(induction c) 
43141  184 
apply blast+ 
185 
done 

186 

187 
lemma final_iff_SKIP: "final (c,s) = (c = SKIP)" 

188 
by (metis SkipE finalD final_def) 

189 

190 
text{* Now we can show that @{text"\<Rightarrow>"} yields a final state iff @{text"\<rightarrow>"} 

191 
terminates: *} 

192 

193 
lemma big_iff_small_termination: 

194 
"(EX t. cs \<Rightarrow> t) \<longleftrightarrow> (EX cs'. cs \<rightarrow>* cs' \<and> final cs')" 

195 
by(simp add: big_iff_small final_iff_SKIP) 

196 

197 
text{* This is the same as saying that the absence of a big step result is 

198 
equivalent with absence of a terminating small step sequence, i.e.\ with 

199 
nontermination. Since @{text"\<rightarrow>"} is determininistic, there is no difference 

200 
between may and must terminate. *} 

201 

202 
end 