43141
|
1 |
header "Small-Step Semantics of Commands"
|
|
2 |
|
|
3 |
theory Small_Step imports Star Big_Step begin
|
|
4 |
|
|
5 |
subsection "The transition relation"
|
|
6 |
|
|
7 |
inductive
|
|
8 |
small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55)
|
|
9 |
where
|
|
10 |
Assign: "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))" |
|
|
11 |
|
|
12 |
Semi1: "(SKIP;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
|
|
13 |
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')" |
|
|
14 |
|
|
15 |
IfTrue: "bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
|
|
16 |
IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
|
|
17 |
|
|
18 |
While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
|
|
19 |
|
|
20 |
|
|
21 |
abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
|
|
22 |
where "x \<rightarrow>* y == star small_step x y"
|
|
23 |
|
|
24 |
subsection{* Executability *}
|
|
25 |
|
|
26 |
code_pred small_step .
|
|
27 |
|
|
28 |
values "{(c',map t [''x'',''y'',''z'']) |c' t.
|
|
29 |
(''x'' ::= V ''z''; ''y'' ::= V ''x'',
|
43158
|
30 |
[''x'' \<rightarrow> 3, ''y'' \<rightarrow> 7, ''z'' \<rightarrow> 5]) \<rightarrow>* (c',t)}"
|
43141
|
31 |
|
|
32 |
|
|
33 |
subsection{* Proof infrastructure *}
|
|
34 |
|
|
35 |
subsubsection{* Induction rules *}
|
|
36 |
|
|
37 |
text{* The default induction rule @{thm[source] small_step.induct} only works
|
|
38 |
for lemmas of the form @{text"a \<rightarrow> b \<Longrightarrow> \<dots>"} where @{text a} and @{text b} are
|
|
39 |
not already pairs @{text"(DUMMY,DUMMY)"}. We can generate a suitable variant
|
|
40 |
of @{thm[source] small_step.induct} for pairs by ``splitting'' the arguments
|
|
41 |
@{text"\<rightarrow>"} into pairs: *}
|
|
42 |
lemmas small_step_induct = small_step.induct[split_format(complete)]
|
|
43 |
|
|
44 |
|
|
45 |
subsubsection{* Proof automation *}
|
|
46 |
|
|
47 |
declare small_step.intros[simp,intro]
|
|
48 |
|
|
49 |
text{* So called transitivity rules. See below. *}
|
|
50 |
|
|
51 |
declare step[trans] step1[trans]
|
|
52 |
|
|
53 |
lemma step2[trans]:
|
|
54 |
"cs \<rightarrow> cs' \<Longrightarrow> cs' \<rightarrow> cs'' \<Longrightarrow> cs \<rightarrow>* cs''"
|
|
55 |
by(metis refl step)
|
|
56 |
|
|
57 |
declare star_trans[trans]
|
|
58 |
|
|
59 |
text{* Rule inversion: *}
|
|
60 |
|
|
61 |
inductive_cases SkipE[elim!]: "(SKIP,s) \<rightarrow> ct"
|
|
62 |
thm SkipE
|
|
63 |
inductive_cases AssignE[elim!]: "(x::=a,s) \<rightarrow> ct"
|
|
64 |
thm AssignE
|
|
65 |
inductive_cases SemiE[elim]: "(c1;c2,s) \<rightarrow> ct"
|
|
66 |
thm SemiE
|
|
67 |
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<rightarrow> ct"
|
|
68 |
inductive_cases WhileE[elim]: "(WHILE b DO c, s) \<rightarrow> ct"
|
|
69 |
|
|
70 |
|
|
71 |
text{* A simple property: *}
|
|
72 |
lemma deterministic:
|
|
73 |
"cs \<rightarrow> cs' \<Longrightarrow> cs \<rightarrow> cs'' \<Longrightarrow> cs'' = cs'"
|
|
74 |
apply(induct arbitrary: cs'' rule: small_step.induct)
|
|
75 |
apply blast+
|
|
76 |
done
|
|
77 |
|
|
78 |
|
|
79 |
subsection "Equivalence with big-step semantics"
|
|
80 |
|
|
81 |
lemma star_semi2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')"
|
|
82 |
proof(induct rule: star_induct)
|
|
83 |
case refl thus ?case by simp
|
|
84 |
next
|
|
85 |
case step
|
|
86 |
thus ?case by (metis Semi2 star.step)
|
|
87 |
qed
|
|
88 |
|
|
89 |
lemma semi_comp:
|
|
90 |
"\<lbrakk> (c1,s1) \<rightarrow>* (SKIP,s2); (c2,s2) \<rightarrow>* (SKIP,s3) \<rbrakk>
|
|
91 |
\<Longrightarrow> (c1;c2, s1) \<rightarrow>* (SKIP,s3)"
|
|
92 |
by(blast intro: star.step star_semi2 star_trans)
|
|
93 |
|
|
94 |
text{* The following proof corresponds to one on the board where one would
|
|
95 |
show chains of @{text "\<rightarrow>"} and @{text "\<rightarrow>*"} steps. This is what the
|
|
96 |
also/finally proof steps do: they compose chains, implicitly using the rules
|
|
97 |
declared with attribute [trans] above. *}
|
|
98 |
|
|
99 |
lemma big_to_small:
|
|
100 |
"cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
|
|
101 |
proof (induct rule: big_step.induct)
|
|
102 |
fix s show "(SKIP,s) \<rightarrow>* (SKIP,s)" by simp
|
|
103 |
next
|
|
104 |
fix x a s show "(x ::= a,s) \<rightarrow>* (SKIP, s(x := aval a s))" by auto
|
|
105 |
next
|
|
106 |
fix c1 c2 s1 s2 s3
|
|
107 |
assume "(c1,s1) \<rightarrow>* (SKIP,s2)" and "(c2,s2) \<rightarrow>* (SKIP,s3)"
|
|
108 |
thus "(c1;c2, s1) \<rightarrow>* (SKIP,s3)" by (rule semi_comp)
|
|
109 |
next
|
|
110 |
fix s::state and b c0 c1 t
|
|
111 |
assume "bval b s"
|
|
112 |
hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c0,s)" by simp
|
|
113 |
also assume "(c0,s) \<rightarrow>* (SKIP,t)"
|
|
114 |
finally show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" . --"= by assumption"
|
|
115 |
next
|
|
116 |
fix s::state and b c0 c1 t
|
|
117 |
assume "\<not>bval b s"
|
|
118 |
hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c1,s)" by simp
|
|
119 |
also assume "(c1,s) \<rightarrow>* (SKIP,t)"
|
|
120 |
finally show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" .
|
|
121 |
next
|
|
122 |
fix b c and s::state
|
|
123 |
assume b: "\<not>bval b s"
|
|
124 |
let ?if = "IF b THEN c; WHILE b DO c ELSE SKIP"
|
|
125 |
have "(WHILE b DO c,s) \<rightarrow> (?if, s)" by blast
|
|
126 |
also have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b)
|
|
127 |
finally show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by auto
|
|
128 |
next
|
|
129 |
fix b c s s' t
|
|
130 |
let ?w = "WHILE b DO c"
|
|
131 |
let ?if = "IF b THEN c; ?w ELSE SKIP"
|
|
132 |
assume w: "(?w,s') \<rightarrow>* (SKIP,t)"
|
|
133 |
assume c: "(c,s) \<rightarrow>* (SKIP,s')"
|
|
134 |
assume b: "bval b s"
|
|
135 |
have "(?w,s) \<rightarrow> (?if, s)" by blast
|
|
136 |
also have "(?if, s) \<rightarrow> (c; ?w, s)" by (simp add: b)
|
|
137 |
also have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule semi_comp[OF c w])
|
|
138 |
finally show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by auto
|
|
139 |
qed
|
|
140 |
|
|
141 |
text{* Each case of the induction can be proved automatically: *}
|
|
142 |
lemma "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
|
|
143 |
proof (induct rule: big_step.induct)
|
|
144 |
case Skip show ?case by blast
|
|
145 |
next
|
|
146 |
case Assign show ?case by blast
|
|
147 |
next
|
|
148 |
case Semi thus ?case by (blast intro: semi_comp)
|
|
149 |
next
|
|
150 |
case IfTrue thus ?case by (blast intro: step)
|
|
151 |
next
|
|
152 |
case IfFalse thus ?case by (blast intro: step)
|
|
153 |
next
|
|
154 |
case WhileFalse thus ?case
|
|
155 |
by (metis step step1 small_step.IfFalse small_step.While)
|
|
156 |
next
|
|
157 |
case WhileTrue
|
|
158 |
thus ?case
|
|
159 |
by(metis While semi_comp small_step.IfTrue step[of small_step])
|
|
160 |
qed
|
|
161 |
|
|
162 |
lemma small1_big_continue:
|
|
163 |
"cs \<rightarrow> cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
|
|
164 |
apply (induct arbitrary: t rule: small_step.induct)
|
|
165 |
apply auto
|
|
166 |
done
|
|
167 |
|
|
168 |
lemma small_big_continue:
|
|
169 |
"cs \<rightarrow>* cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
|
|
170 |
apply (induct rule: star.induct)
|
|
171 |
apply (auto intro: small1_big_continue)
|
|
172 |
done
|
|
173 |
|
|
174 |
lemma small_to_big: "cs \<rightarrow>* (SKIP,t) \<Longrightarrow> cs \<Rightarrow> t"
|
|
175 |
by (metis small_big_continue Skip)
|
|
176 |
|
|
177 |
text {*
|
|
178 |
Finally, the equivalence theorem:
|
|
179 |
*}
|
|
180 |
theorem big_iff_small:
|
|
181 |
"cs \<Rightarrow> t = cs \<rightarrow>* (SKIP,t)"
|
|
182 |
by(metis big_to_small small_to_big)
|
|
183 |
|
|
184 |
|
|
185 |
subsection "Final configurations and infinite reductions"
|
|
186 |
|
|
187 |
definition "final cs \<longleftrightarrow> \<not>(EX cs'. cs \<rightarrow> cs')"
|
|
188 |
|
|
189 |
lemma finalD: "final (c,s) \<Longrightarrow> c = SKIP"
|
|
190 |
apply(simp add: final_def)
|
|
191 |
apply(induct c)
|
|
192 |
apply blast+
|
|
193 |
done
|
|
194 |
|
|
195 |
lemma final_iff_SKIP: "final (c,s) = (c = SKIP)"
|
|
196 |
by (metis SkipE finalD final_def)
|
|
197 |
|
|
198 |
text{* Now we can show that @{text"\<Rightarrow>"} yields a final state iff @{text"\<rightarrow>"}
|
|
199 |
terminates: *}
|
|
200 |
|
|
201 |
lemma big_iff_small_termination:
|
|
202 |
"(EX t. cs \<Rightarrow> t) \<longleftrightarrow> (EX cs'. cs \<rightarrow>* cs' \<and> final cs')"
|
|
203 |
by(simp add: big_iff_small final_iff_SKIP)
|
|
204 |
|
|
205 |
text{* This is the same as saying that the absence of a big step result is
|
|
206 |
equivalent with absence of a terminating small step sequence, i.e.\ with
|
|
207 |
nontermination. Since @{text"\<rightarrow>"} is determininistic, there is no difference
|
|
208 |
between may and must terminate. *}
|
|
209 |
|
|
210 |
end
|