1 (* Title: HOL/IMP/Natural.thy |
|
2 Author: Tobias Nipkow & Robert Sandner, TUM |
|
3 Isar Version: Gerwin Klein, 2001; additional proofs by Lawrence Paulson |
|
4 Copyright 1996 TUM |
|
5 *) |
|
6 |
|
7 header "Natural Semantics of Commands" |
|
8 |
|
9 theory Natural imports Com begin |
|
10 |
|
11 subsection "Execution of commands" |
|
12 |
|
13 text {* |
|
14 We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started |
|
15 in state @{text s}, terminates in state @{text s'}}. Formally, |
|
16 @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} is just another form of saying \emph{the tuple |
|
17 @{text "(c,s,s')"} is part of the relation @{text evalc}}: |
|
18 *} |
|
19 |
|
20 definition |
|
21 update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900) where |
|
22 "update = fun_upd" |
|
23 |
|
24 notation (xsymbols) |
|
25 update ("_/[_ \<mapsto> /_]" [900,0,0] 900) |
|
26 |
|
27 text {* Disable conflicting syntax from HOL Map theory. *} |
|
28 |
|
29 no_syntax |
|
30 "_maplet" :: "['a, 'a] => maplet" ("_ /|->/ _") |
|
31 "_maplets" :: "['a, 'a] => maplet" ("_ /[|->]/ _") |
|
32 "" :: "maplet => maplets" ("_") |
|
33 "_Maplets" :: "[maplet, maplets] => maplets" ("_,/ _") |
|
34 "_MapUpd" :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900) |
|
35 "_Map" :: "maplets => 'a ~=> 'b" ("(1[_])") |
|
36 |
|
37 text {* |
|
38 The big-step execution relation @{text evalc} is defined inductively: |
|
39 *} |
|
40 inductive |
|
41 evalc :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60) |
|
42 where |
|
43 Skip: "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s" |
|
44 | Assign: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s[x\<mapsto>a s]" |
|
45 |
|
46 | Semi: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
47 |
|
48 | IfTrue: "b s \<Longrightarrow> \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
49 | IfFalse: "\<not>b s \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
50 |
|
51 | WhileFalse: "\<not>b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s" |
|
52 | WhileTrue: "b s \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s' |
|
53 \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
54 |
|
55 lemmas evalc.intros [intro] -- "use those rules in automatic proofs" |
|
56 |
|
57 text {* |
|
58 The induction principle induced by this definition looks like this: |
|
59 |
|
60 @{thm [display] evalc.induct [no_vars]} |
|
61 |
|
62 |
|
63 (@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's |
|
64 meta symbols for @{text "\<forall>"} and @{text "\<longrightarrow>"}) |
|
65 *} |
|
66 |
|
67 text {* |
|
68 The rules of @{text evalc} are syntax directed, i.e.~for each |
|
69 syntactic category there is always only one rule applicable. That |
|
70 means we can use the rules in both directions. This property is called rule inversion. |
|
71 *} |
|
72 inductive_cases skipE [elim!]: "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
73 inductive_cases semiE [elim!]: "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
74 inductive_cases assignE [elim!]: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
75 inductive_cases ifE [elim!]: "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
76 inductive_cases whileE [elim]: "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
77 |
|
78 text {* The next proofs are all trivial by rule inversion. |
|
79 *} |
|
80 |
|
81 inductive_simps |
|
82 skip: "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
83 and assign: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
84 and semi: "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
85 |
|
86 lemma ifTrue: |
|
87 "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
88 by auto |
|
89 |
|
90 lemma ifFalse: |
|
91 "\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
92 by auto |
|
93 |
|
94 lemma whileFalse: |
|
95 "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)" |
|
96 by auto |
|
97 |
|
98 lemma whileTrue: |
|
99 "b s \<Longrightarrow> |
|
100 \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s' = |
|
101 (\<exists>s''. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s')" |
|
102 by auto |
|
103 |
|
104 text "Again, Isabelle may use these rules in automatic proofs:" |
|
105 lemmas evalc_cases [simp] = skip assign ifTrue ifFalse whileFalse semi whileTrue |
|
106 |
|
107 subsection "Equivalence of statements" |
|
108 |
|
109 text {* |
|
110 We call two statements @{text c} and @{text c'} equivalent wrt.~the |
|
111 big-step semantics when \emph{@{text c} started in @{text s} terminates |
|
112 in @{text s'} iff @{text c'} started in the same @{text s} also terminates |
|
113 in the same @{text s'}}. Formally: |
|
114 *} |
|
115 definition |
|
116 equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _" [56, 56] 55) where |
|
117 "c \<sim> c' = (\<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s')" |
|
118 |
|
119 text {* |
|
120 Proof rules telling Isabelle to unfold the definition |
|
121 if there is something to be proved about equivalent |
|
122 statements: *} |
|
123 lemma equivI [intro!]: |
|
124 "(\<And>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s') \<Longrightarrow> c \<sim> c'" |
|
125 by (unfold equiv_c_def) blast |
|
126 |
|
127 lemma equivD1: |
|
128 "c \<sim> c' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
129 by (unfold equiv_c_def) blast |
|
130 |
|
131 lemma equivD2: |
|
132 "c \<sim> c' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
133 by (unfold equiv_c_def) blast |
|
134 |
|
135 text {* |
|
136 As an example, we show that loop unfolding is an equivalence |
|
137 transformation on programs: |
|
138 *} |
|
139 lemma unfold_while: |
|
140 "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)" (is "?w \<sim> ?if") |
|
141 proof - |
|
142 -- "to show the equivalence, we look at the derivation tree for" |
|
143 -- "each side and from that construct a derivation tree for the other side" |
|
144 { fix s s' assume w: "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
145 -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s}," |
|
146 -- "then both statements do nothing:" |
|
147 hence "\<not>b s \<Longrightarrow> s = s'" by blast |
|
148 hence "\<not>b s \<Longrightarrow> \<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
149 moreover |
|
150 -- "on the other hand, if @{text b} is @{text True} in state @{text s}," |
|
151 -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"} *} |
|
152 { assume b: "b s" |
|
153 with w obtain s'' where |
|
154 "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto |
|
155 -- "now we can build a derivation tree for the @{text \<IF>}" |
|
156 -- "first, the body of the True-branch:" |
|
157 hence "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule Semi) |
|
158 -- "then the whole @{text \<IF>}" |
|
159 with b have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule IfTrue) |
|
160 } |
|
161 ultimately |
|
162 -- "both cases together give us what we want:" |
|
163 have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
164 } |
|
165 moreover |
|
166 -- "now the other direction:" |
|
167 { fix s s' assume "if": "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
168 -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch" |
|
169 -- "of the @{text \<IF>} is executed, and both statements do nothing:" |
|
170 hence "\<not>b s \<Longrightarrow> s = s'" by blast |
|
171 hence "\<not>b s \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
172 moreover |
|
173 -- "on the other hand, if @{text b} is @{text True} in state @{text s}," |
|
174 -- {* then this time only the @{text IfTrue} rule can have be used *} |
|
175 { assume b: "b s" |
|
176 with "if" have "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto |
|
177 -- "and for this, only the Semi-rule is applicable:" |
|
178 then obtain s'' where |
|
179 "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto |
|
180 -- "with this information, we can build a derivation tree for the @{text \<WHILE>}" |
|
181 with b |
|
182 have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule WhileTrue) |
|
183 } |
|
184 ultimately |
|
185 -- "both cases together again give us what we want:" |
|
186 have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
187 } |
|
188 ultimately |
|
189 show ?thesis by blast |
|
190 qed |
|
191 |
|
192 text {* |
|
193 Happily, such lengthy proofs are seldom necessary. Isabelle can prove many such facts automatically. |
|
194 *} |
|
195 |
|
196 lemma |
|
197 "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)" |
|
198 by blast |
|
199 |
|
200 lemma triv_if: |
|
201 "(\<IF> b \<THEN> c \<ELSE> c) \<sim> c" |
|
202 by blast |
|
203 |
|
204 lemma commute_if: |
|
205 "(\<IF> b1 \<THEN> (\<IF> b2 \<THEN> c11 \<ELSE> c12) \<ELSE> c2) |
|
206 \<sim> |
|
207 (\<IF> b2 \<THEN> (\<IF> b1 \<THEN> c11 \<ELSE> c2) \<ELSE> (\<IF> b1 \<THEN> c12 \<ELSE> c2))" |
|
208 by blast |
|
209 |
|
210 lemma while_equiv: |
|
211 "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> c \<sim> c' \<Longrightarrow> (c0 = \<WHILE> b \<DO> c) \<Longrightarrow> \<langle>\<WHILE> b \<DO> c', s\<rangle> \<longrightarrow>\<^sub>c u" |
|
212 by (induct rule: evalc.induct) (auto simp add: equiv_c_def) |
|
213 |
|
214 lemma equiv_while: |
|
215 "c \<sim> c' \<Longrightarrow> (\<WHILE> b \<DO> c) \<sim> (\<WHILE> b \<DO> c')" |
|
216 by (simp add: equiv_c_def) (metis equiv_c_def while_equiv) |
|
217 |
|
218 |
|
219 text {* |
|
220 Program equivalence is an equivalence relation. |
|
221 *} |
|
222 |
|
223 lemma equiv_refl: |
|
224 "c \<sim> c" |
|
225 by blast |
|
226 |
|
227 lemma equiv_sym: |
|
228 "c1 \<sim> c2 \<Longrightarrow> c2 \<sim> c1" |
|
229 by (auto simp add: equiv_c_def) |
|
230 |
|
231 lemma equiv_trans: |
|
232 "c1 \<sim> c2 \<Longrightarrow> c2 \<sim> c3 \<Longrightarrow> c1 \<sim> c3" |
|
233 by (auto simp add: equiv_c_def) |
|
234 |
|
235 text {* |
|
236 Program constructions preserve equivalence. |
|
237 *} |
|
238 |
|
239 lemma equiv_semi: |
|
240 "c1 \<sim> c1' \<Longrightarrow> c2 \<sim> c2' \<Longrightarrow> (c1; c2) \<sim> (c1'; c2')" |
|
241 by (force simp add: equiv_c_def) |
|
242 |
|
243 lemma equiv_if: |
|
244 "c1 \<sim> c1' \<Longrightarrow> c2 \<sim> c2' \<Longrightarrow> (\<IF> b \<THEN> c1 \<ELSE> c2) \<sim> (\<IF> b \<THEN> c1' \<ELSE> c2')" |
|
245 by (force simp add: equiv_c_def) |
|
246 |
|
247 lemma while_never: "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> c \<noteq> \<WHILE> (\<lambda>s. True) \<DO> c1" |
|
248 apply (induct rule: evalc.induct) |
|
249 apply auto |
|
250 done |
|
251 |
|
252 lemma equiv_while_True: |
|
253 "(\<WHILE> (\<lambda>s. True) \<DO> c1) \<sim> (\<WHILE> (\<lambda>s. True) \<DO> c2)" |
|
254 by (blast dest: while_never) |
|
255 |
|
256 |
|
257 subsection "Execution is deterministic" |
|
258 |
|
259 text {* |
|
260 This proof is automatic. |
|
261 *} |
|
262 theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = t" |
|
263 by (induct arbitrary: u rule: evalc.induct) blast+ |
|
264 |
|
265 |
|
266 text {* |
|
267 The following proof presents all the details: |
|
268 *} |
|
269 theorem com_det: |
|
270 assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u" |
|
271 shows "u = t" |
|
272 using assms |
|
273 proof (induct arbitrary: u set: evalc) |
|
274 fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u" |
|
275 thus "u = s" by blast |
|
276 next |
|
277 fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u" |
|
278 thus "u = s[x \<mapsto> a s]" by blast |
|
279 next |
|
280 fix c0 c1 s s1 s2 u |
|
281 assume IH0: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2" |
|
282 assume IH1: "\<And>u. \<langle>c1,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1" |
|
283 |
|
284 assume "\<langle>c0;c1, s\<rangle> \<longrightarrow>\<^sub>c u" |
|
285 then obtain s' where |
|
286 c0: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" and |
|
287 c1: "\<langle>c1,s'\<rangle> \<longrightarrow>\<^sub>c u" |
|
288 by auto |
|
289 |
|
290 from c0 IH0 have "s'=s2" by blast |
|
291 with c1 IH1 show "u=s1" by blast |
|
292 next |
|
293 fix b c0 c1 s s1 u |
|
294 assume IH: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1" |
|
295 |
|
296 assume "b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u" |
|
297 hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by blast |
|
298 with IH show "u = s1" by blast |
|
299 next |
|
300 fix b c0 c1 s s1 u |
|
301 assume IH: "\<And>u. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1" |
|
302 |
|
303 assume "\<not>b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u" |
|
304 hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by blast |
|
305 with IH show "u = s1" by blast |
|
306 next |
|
307 fix b c s u |
|
308 assume "\<not>b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u" |
|
309 thus "u = s" by blast |
|
310 next |
|
311 fix b c s s1 s2 u |
|
312 assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2" |
|
313 assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1" |
|
314 |
|
315 assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u" |
|
316 then obtain s' where |
|
317 c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and |
|
318 w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u" |
|
319 by auto |
|
320 |
|
321 from c "IH\<^sub>c" have "s' = s2" by blast |
|
322 with w "IH\<^sub>w" show "u = s1" by blast |
|
323 qed |
|
324 |
|
325 |
|
326 text {* |
|
327 This is the proof as you might present it in a lecture. The remaining |
|
328 cases are simple enough to be proved automatically: |
|
329 *} |
|
330 theorem |
|
331 assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u" |
|
332 shows "u = t" |
|
333 using assms |
|
334 proof (induct arbitrary: u) |
|
335 -- "the simple @{text \<SKIP>} case for demonstration:" |
|
336 fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u" |
|
337 thus "u = s" by blast |
|
338 next |
|
339 -- "and the only really interesting case, @{text \<WHILE>}:" |
|
340 fix b c s s1 s2 u |
|
341 assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2" |
|
342 assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1" |
|
343 |
|
344 assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u" |
|
345 then obtain s' where |
|
346 c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and |
|
347 w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u" |
|
348 by auto |
|
349 |
|
350 from c "IH\<^sub>c" have "s' = s2" by blast |
|
351 with w "IH\<^sub>w" show "u = s1" by blast |
|
352 qed blast+ -- "prove the rest automatically" |
|
353 |
|
354 end |
|