author | kleing |
Mon, 17 Jun 2013 11:39:51 -0700 | |
changeset 52386 | 167dfa940c71 |
parent 52376 | 90fd1922f45f |
child 52391 | e65dedce4a17 |
permissions | -rw-r--r-- |
43141 | 1 |
(* Author: Gerwin Klein, Tobias Nipkow *) |
2 |
||
3 |
theory Big_Step imports Com begin |
|
4 |
||
5 |
subsection "Big-Step Semantics of Commands" |
|
6 |
||
52370 | 7 |
text {* |
8 |
The big-step semantics is a straight-forward inductive definition |
|
9 |
with concrete syntax. Note that the first paramenter is a tuple, |
|
10 |
so the syntax becomes @{text "(c,s) \<Rightarrow> s'"}. |
|
11 |
*} |
|
12 |
||
49191 | 13 |
text_raw{*\snip{BigStepdef}{0}{1}{% *} |
43141 | 14 |
inductive |
15 |
big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55) |
|
16 |
where |
|
17 |
Skip: "(SKIP,s) \<Rightarrow> s" | |
|
18 |
Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" | |
|
47818 | 19 |
Seq: "\<lbrakk> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow> |
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
52021
diff
changeset
|
20 |
(c\<^isub>1;;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" | |
43141 | 21 |
|
22 |
IfTrue: "\<lbrakk> bval b s; (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> |
|
50054 | 23 |
(IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" | |
43141 | 24 |
IfFalse: "\<lbrakk> \<not>bval b s; (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> |
50054 | 25 |
(IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" | |
43141 | 26 |
|
27 |
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" | |
|
52376 | 28 |
WhileTrue: "\<lbrakk> bval b s\<^isub>1; (c,s\<^isub>1) \<Rightarrow> s\<^isub>2; (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> |
29 |
\<Longrightarrow> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
|
49191 | 30 |
text_raw{*}%endsnip*} |
43141 | 31 |
|
49191 | 32 |
text_raw{*\snip{BigStepEx}{1}{2}{% *} |
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
52021
diff
changeset
|
33 |
schematic_lemma ex: "(''x'' ::= N 5;; ''y'' ::= V ''x'', s) \<Rightarrow> ?t" |
47818 | 34 |
apply(rule Seq) |
43141 | 35 |
apply(rule Assign) |
36 |
apply simp |
|
37 |
apply(rule Assign) |
|
38 |
done |
|
49191 | 39 |
text_raw{*}%endsnip*} |
43141 | 40 |
|
41 |
thm ex[simplified] |
|
42 |
||
43 |
text{* We want to execute the big-step rules: *} |
|
44 |
||
45 |
code_pred big_step . |
|
46 |
||
47 |
text{* For inductive definitions we need command |
|
48 |
\texttt{values} instead of \texttt{value}. *} |
|
49 |
||
44923 | 50 |
values "{t. (SKIP, \<lambda>_. 0) \<Rightarrow> t}" |
43141 | 51 |
|
52 |
text{* We need to translate the result state into a list |
|
53 |
to display it. *} |
|
54 |
||
44036 | 55 |
values "{map t [''x''] |t. (SKIP, <''x'' := 42>) \<Rightarrow> t}" |
43141 | 56 |
|
44036 | 57 |
values "{map t [''x''] |t. (''x'' ::= N 2, <''x'' := 42>) \<Rightarrow> t}" |
43141 | 58 |
|
59 |
values "{map t [''x'',''y''] |t. |
|
60 |
(WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)), |
|
44036 | 61 |
<''x'' := 0, ''y'' := 13>) \<Rightarrow> t}" |
43141 | 62 |
|
63 |
||
64 |
text{* Proof automation: *} |
|
65 |
||
52370 | 66 |
text {* The introduction rules are good for automatically |
67 |
construction small program executions. The recursive cases |
|
68 |
may require backtracking, so we declare the set as unsafe |
|
69 |
intro rules. *} |
|
43141 | 70 |
declare big_step.intros [intro] |
71 |
||
72 |
text{* The standard induction rule |
|
73 |
@{thm [display] big_step.induct [no_vars]} *} |
|
74 |
||
75 |
thm big_step.induct |
|
76 |
||
52370 | 77 |
text{* |
78 |
This induction schema is almost perfect for our purposes, but |
|
79 |
our trick for reusing the tuple syntax means that the induction |
|
80 |
schema has two parameters instead of the @{text c}, @{text s}, |
|
81 |
and @{text s'} that we are likely to encounter. Splitting |
|
82 |
the tuple parameter fixes this: |
|
83 |
*} |
|
43141 | 84 |
lemmas big_step_induct = big_step.induct[split_format(complete)] |
85 |
thm big_step_induct |
|
86 |
text {* |
|
87 |
@{thm [display] big_step_induct [no_vars]} |
|
88 |
*} |
|
89 |
||
90 |
||
91 |
subsection "Rule inversion" |
|
92 |
||
93 |
text{* What can we deduce from @{prop "(SKIP,s) \<Rightarrow> t"} ? |
|
94 |
That @{prop "s = t"}. This is how we can automatically prove it: *} |
|
95 |
||
51513 | 96 |
inductive_cases SkipE[elim!]: "(SKIP,s) \<Rightarrow> t" |
97 |
thm SkipE |
|
43141 | 98 |
|
99 |
text{* This is an \emph{elimination rule}. The [elim] attribute tells auto, |
|
100 |
blast and friends (but not simp!) to use it automatically; [elim!] means that |
|
101 |
it is applied eagerly. |
|
102 |
||
103 |
Similarly for the other commands: *} |
|
104 |
||
105 |
inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t" |
|
106 |
thm AssignE |
|
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
52021
diff
changeset
|
107 |
inductive_cases SeqE[elim!]: "(c1;;c2,s1) \<Rightarrow> s3" |
47818 | 108 |
thm SeqE |
43141 | 109 |
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t" |
110 |
thm IfE |
|
111 |
||
112 |
inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t" |
|
113 |
thm WhileE |
|
114 |
text{* Only [elim]: [elim!] would not terminate. *} |
|
115 |
||
116 |
text{* An automatic example: *} |
|
117 |
||
118 |
lemma "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t \<Longrightarrow> t = s" |
|
119 |
by blast |
|
120 |
||
121 |
text{* Rule inversion by hand via the ``cases'' method: *} |
|
122 |
||
123 |
lemma assumes "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t" |
|
124 |
shows "t = s" |
|
125 |
proof- |
|
126 |
from assms show ?thesis |
|
127 |
proof cases --"inverting assms" |
|
128 |
case IfTrue thm IfTrue |
|
129 |
thus ?thesis by blast |
|
130 |
next |
|
131 |
case IfFalse thus ?thesis by blast |
|
132 |
qed |
|
133 |
qed |
|
134 |
||
44070 | 135 |
(* Using rule inversion to prove simplification rules: *) |
136 |
lemma assign_simp: |
|
137 |
"(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))" |
|
138 |
by auto |
|
43141 | 139 |
|
52376 | 140 |
text {* An example combining rule inversion and derivations *} |
141 |
lemma Semi_assoc: |
|
142 |
"(c1;; c2;; c3, s) \<Rightarrow> s' \<longleftrightarrow> (c1;; (c2;; c3), s) \<Rightarrow> s'" |
|
143 |
proof |
|
144 |
assume "(c1;; c2;; c3, s) \<Rightarrow> s'" |
|
145 |
then obtain s1 s2 where |
|
146 |
c1: "(c1, s) \<Rightarrow> s1" and |
|
147 |
c2: "(c2, s1) \<Rightarrow> s2" and |
|
148 |
c3: "(c3, s2) \<Rightarrow> s'" by auto |
|
149 |
from c2 c3 |
|
150 |
have "(c2;; c3, s1) \<Rightarrow> s'" by (rule Seq) |
|
151 |
with c1 |
|
152 |
show "(c1;; (c2;; c3), s) \<Rightarrow> s'" by (rule Seq) |
|
153 |
next |
|
154 |
-- "The other direction is analogous" |
|
155 |
assume "(c1;; (c2;; c3), s) \<Rightarrow> s'" |
|
156 |
thus "(c1;; c2;; c3, s) \<Rightarrow> s'" by auto |
|
157 |
qed |
|
158 |
||
159 |
||
43141 | 160 |
subsection "Command Equivalence" |
161 |
||
162 |
text {* |
|
163 |
We call two statements @{text c} and @{text c'} equivalent wrt.\ the |
|
164 |
big-step semantics when \emph{@{text c} started in @{text s} terminates |
|
165 |
in @{text s'} iff @{text c'} started in the same @{text s} also terminates |
|
166 |
in the same @{text s'}}. Formally: |
|
167 |
*} |
|
49191 | 168 |
text_raw{*\snip{BigStepEquiv}{0}{1}{% *} |
43141 | 169 |
abbreviation |
170 |
equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where |
|
52372 | 171 |
"c \<sim> c' \<equiv> (\<forall>s t. (c,s) \<Rightarrow> t = (c',s) \<Rightarrow> t)" |
49191 | 172 |
text_raw{*}%endsnip*} |
43141 | 173 |
|
174 |
text {* |
|
175 |
Warning: @{text"\<sim>"} is the symbol written \verb!\ < s i m >! (without spaces). |
|
176 |
||
177 |
As an example, we show that loop unfolding is an equivalence |
|
178 |
transformation on programs: |
|
179 |
*} |
|
180 |
lemma unfold_while: |
|
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
52021
diff
changeset
|
181 |
"(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw") |
43141 | 182 |
proof - |
183 |
-- "to show the equivalence, we look at the derivation tree for" |
|
184 |
-- "each side and from that construct a derivation tree for the other side" |
|
185 |
{ fix s t assume "(?w, s) \<Rightarrow> t" |
|
186 |
-- "as a first thing we note that, if @{text b} is @{text False} in state @{text s}," |
|
187 |
-- "then both statements do nothing:" |
|
188 |
{ assume "\<not>bval b s" |
|
189 |
hence "t = s" using `(?w,s) \<Rightarrow> t` by blast |
|
190 |
hence "(?iw, s) \<Rightarrow> t" using `\<not>bval b s` by blast |
|
191 |
} |
|
192 |
moreover |
|
193 |
-- "on the other hand, if @{text b} is @{text True} in state @{text s}," |
|
194 |
-- {* then only the @{text WhileTrue} rule can have been used to derive @{text "(?w, s) \<Rightarrow> t"} *} |
|
195 |
{ assume "bval b s" |
|
196 |
with `(?w, s) \<Rightarrow> t` obtain s' where |
|
197 |
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto |
|
198 |
-- "now we can build a derivation tree for the @{text IF}" |
|
199 |
-- "first, the body of the True-branch:" |
|
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
52021
diff
changeset
|
200 |
hence "(c;; ?w, s) \<Rightarrow> t" by (rule Seq) |
43141 | 201 |
-- "then the whole @{text IF}" |
202 |
with `bval b s` have "(?iw, s) \<Rightarrow> t" by (rule IfTrue) |
|
203 |
} |
|
204 |
ultimately |
|
205 |
-- "both cases together give us what we want:" |
|
206 |
have "(?iw, s) \<Rightarrow> t" by blast |
|
207 |
} |
|
208 |
moreover |
|
209 |
-- "now the other direction:" |
|
210 |
{ fix s t assume "(?iw, s) \<Rightarrow> t" |
|
211 |
-- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch" |
|
212 |
-- "of the @{text IF} is executed, and both statements do nothing:" |
|
213 |
{ assume "\<not>bval b s" |
|
214 |
hence "s = t" using `(?iw, s) \<Rightarrow> t` by blast |
|
215 |
hence "(?w, s) \<Rightarrow> t" using `\<not>bval b s` by blast |
|
216 |
} |
|
217 |
moreover |
|
218 |
-- "on the other hand, if @{text b} is @{text True} in state @{text s}," |
|
219 |
-- {* then this time only the @{text IfTrue} rule can have be used *} |
|
220 |
{ assume "bval b s" |
|
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
52021
diff
changeset
|
221 |
with `(?iw, s) \<Rightarrow> t` have "(c;; ?w, s) \<Rightarrow> t" by auto |
47818 | 222 |
-- "and for this, only the Seq-rule is applicable:" |
43141 | 223 |
then obtain s' where |
224 |
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto |
|
225 |
-- "with this information, we can build a derivation tree for the @{text WHILE}" |
|
226 |
with `bval b s` |
|
227 |
have "(?w, s) \<Rightarrow> t" by (rule WhileTrue) |
|
228 |
} |
|
229 |
ultimately |
|
230 |
-- "both cases together again give us what we want:" |
|
231 |
have "(?w, s) \<Rightarrow> t" by blast |
|
232 |
} |
|
233 |
ultimately |
|
234 |
show ?thesis by blast |
|
235 |
qed |
|
236 |
||
237 |
text {* Luckily, such lengthy proofs are seldom necessary. Isabelle can |
|
238 |
prove many such facts automatically. *} |
|
239 |
||
45321 | 240 |
lemma while_unfold: |
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
52021
diff
changeset
|
241 |
"(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)" |
43141 | 242 |
by blast |
243 |
||
244 |
lemma triv_if: |
|
245 |
"(IF b THEN c ELSE c) \<sim> c" |
|
246 |
by blast |
|
247 |
||
248 |
lemma commute_if: |
|
249 |
"(IF b1 THEN (IF b2 THEN c11 ELSE c12) ELSE c2) |
|
250 |
\<sim> |
|
251 |
(IF b2 THEN (IF b1 THEN c11 ELSE c2) ELSE (IF b1 THEN c12 ELSE c2))" |
|
252 |
by blast |
|
253 |
||
51513 | 254 |
lemma sim_while_cong_aux: |
255 |
"(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> c \<sim> c' \<Longrightarrow> (WHILE b DO c',s) \<Rightarrow> t" |
|
256 |
apply(induction "WHILE b DO c" s t arbitrary: b c rule: big_step_induct) |
|
257 |
apply blast |
|
258 |
apply blast |
|
259 |
done |
|
260 |
||
261 |
lemma sim_while_cong: "c \<sim> c' \<Longrightarrow> WHILE b DO c \<sim> WHILE b DO c'" |
|
262 |
by (metis sim_while_cong_aux) |
|
263 |
||
52021
59963cda805a
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
kleing
parents:
51513
diff
changeset
|
264 |
text {* Command equivalence is an equivalence relation, i.e.\ it is |
59963cda805a
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
kleing
parents:
51513
diff
changeset
|
265 |
reflexive, symmetric, and transitive. Because we used an abbreviation |
59963cda805a
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
kleing
parents:
51513
diff
changeset
|
266 |
above, Isabelle derives this automatically. *} |
59963cda805a
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
kleing
parents:
51513
diff
changeset
|
267 |
|
59963cda805a
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
kleing
parents:
51513
diff
changeset
|
268 |
lemma sim_refl: "c \<sim> c" by simp |
59963cda805a
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
kleing
parents:
51513
diff
changeset
|
269 |
lemma sim_sym: "(c \<sim> c') = (c' \<sim> c)" by auto |
59963cda805a
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
kleing
parents:
51513
diff
changeset
|
270 |
lemma sim_trans: "c \<sim> c' \<Longrightarrow> c' \<sim> c'' \<Longrightarrow> c \<sim> c''" by auto |
43141 | 271 |
|
272 |
subsection "Execution is deterministic" |
|
273 |
||
274 |
text {* This proof is automatic. *} |
|
49191 | 275 |
text_raw{*\snip{BigStepDeterministic}{0}{1}{% *} |
43141 | 276 |
theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t" |
45321 | 277 |
by (induction arbitrary: u rule: big_step.induct) blast+ |
49191 | 278 |
text_raw{*}%endsnip*} |
45321 | 279 |
|
43141 | 280 |
|
281 |
text {* |
|
282 |
This is the proof as you might present it in a lecture. The remaining |
|
283 |
cases are simple enough to be proved automatically: |
|
284 |
*} |
|
49191 | 285 |
text_raw{*\snip{BigStepDetLong}{0}{2}{% *} |
43141 | 286 |
theorem |
287 |
"(c,s) \<Rightarrow> t \<Longrightarrow> (c,s) \<Rightarrow> t' \<Longrightarrow> t' = t" |
|
45015 | 288 |
proof (induction arbitrary: t' rule: big_step.induct) |
43141 | 289 |
-- "the only interesting case, @{text WhileTrue}:" |
52386 | 290 |
fix b c s s\<^isub>1 t t' |
43141 | 291 |
-- "The assumptions of the rule:" |
52386 | 292 |
assume "bval b s" and "(c,s) \<Rightarrow> s\<^isub>1" and "(WHILE b DO c,s\<^isub>1) \<Rightarrow> t" |
43141 | 293 |
-- {* Ind.Hyp; note the @{text"\<And>"} because of arbitrary: *} |
52386 | 294 |
assume IHc: "\<And>t'. (c,s) \<Rightarrow> t' \<Longrightarrow> t' = s\<^isub>1" |
295 |
assume IHw: "\<And>t'. (WHILE b DO c,s\<^isub>1) \<Rightarrow> t' \<Longrightarrow> t' = t" |
|
43141 | 296 |
-- "Premise of implication:" |
297 |
assume "(WHILE b DO c,s) \<Rightarrow> t'" |
|
52386 | 298 |
with `bval b s` obtain s\<^isub>1' where |
299 |
c: "(c,s) \<Rightarrow> s\<^isub>1'" and |
|
300 |
w: "(WHILE b DO c,s\<^isub>1') \<Rightarrow> t'" |
|
43141 | 301 |
by auto |
52386 | 302 |
from c IHc have "s\<^isub>1' = s\<^isub>1" by blast |
43141 | 303 |
with w IHw show "t' = t" by blast |
304 |
qed blast+ -- "prove the rest automatically" |
|
49191 | 305 |
text_raw{*}%endsnip*} |
43141 | 306 |
|
307 |
end |