author | krauss |
Wed, 02 Feb 2011 08:47:45 +0100 | |
changeset 41686 | d8efc2490b8e |
parent 41529 | ba60efa2fd08 |
permissions | -rw-r--r-- |
12431 | 1 |
(* Title: HOL/IMP/Natural.thy |
2 |
Author: Tobias Nipkow & Robert Sandner, TUM |
|
34055 | 3 |
Isar Version: Gerwin Klein, 2001; additional proofs by Lawrence Paulson |
12431 | 4 |
Copyright 1996 TUM |
1700 | 5 |
*) |
6 |
||
12431 | 7 |
header "Natural Semantics of Commands" |
8 |
||
16417 | 9 |
theory Natural imports Com begin |
12431 | 10 |
|
11 |
subsection "Execution of commands" |
|
1700 | 12 |
|
12431 | 13 |
text {* |
18372 | 14 |
We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started |
12431 | 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 |
*} |
|
1700 | 19 |
|
27362 | 20 |
definition |
21 |
update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900) where |
|
22 |
"update = fun_upd" |
|
12431 | 23 |
|
27362 | 24 |
notation (xsymbols) |
25 |
update ("_/[_ \<mapsto> /_]" [900,0,0] 900) |
|
12431 | 26 |
|
37085 | 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 |
||
12431 | 37 |
text {* |
38 |
The big-step execution relation @{text evalc} is defined inductively: |
|
39 |
*} |
|
23746 | 40 |
inductive |
41 |
evalc :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60) |
|
42 |
where |
|
12431 | 43 |
Skip: "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s" |
23746 | 44 |
| Assign: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s[x\<mapsto>a s]" |
12431 | 45 |
|
23746 | 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'" |
12431 | 47 |
|
23746 | 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'" |
|
12431 | 50 |
|
23746 | 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' |
|
12431 | 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 |
||
18372 | 63 |
(@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's |
12431 | 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 |
|
34055 | 70 |
means we can use the rules in both directions. This property is called rule inversion. |
12431 | 71 |
*} |
34055 | 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 |
||
37736
2bf3a2cb5e58
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn
parents:
37085
diff
changeset
|
81 |
inductive_simps |
2bf3a2cb5e58
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn
parents:
37085
diff
changeset
|
82 |
skip: "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'" |
2bf3a2cb5e58
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn
parents:
37085
diff
changeset
|
83 |
and assign: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s'" |
2bf3a2cb5e58
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn
parents:
37085
diff
changeset
|
84 |
and semi: "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'" |
1700 | 85 |
|
18372 | 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'" |
|
34055 | 88 |
by auto |
12431 | 89 |
|
18372 | 90 |
lemma ifFalse: |
12431 | 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'" |
34055 | 92 |
by auto |
12431 | 93 |
|
18372 | 94 |
lemma whileFalse: |
12431 | 95 |
"\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)" |
34055 | 96 |
by auto |
12431 | 97 |
|
18372 | 98 |
lemma whileTrue: |
99 |
"b s \<Longrightarrow> |
|
100 |
\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s' = |
|
12431 | 101 |
(\<exists>s''. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s')" |
34055 | 102 |
by auto |
12431 | 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" |
|
1700 | 108 |
|
12431 | 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: |
|
18372 | 114 |
*} |
27362 | 115 |
definition |
37085 | 116 |
equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _" [56, 56] 55) where |
27362 | 117 |
"c \<sim> c' = (\<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s')" |
12431 | 118 |
|
119 |
text {* |
|
120 |
Proof rules telling Isabelle to unfold the definition |
|
121 |
if there is something to be proved about equivalent |
|
18372 | 122 |
statements: *} |
12431 | 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 |
|
1700 | 134 |
|
12431 | 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" |
|
18372 | 143 |
-- "each side and from that construct a derivation tree for the other side" |
12431 | 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:" |
|
34055 | 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 |
|
12431 | 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 |
} |
|
18372 | 161 |
ultimately |
162 |
-- "both cases together give us what we want:" |
|
12431 | 163 |
have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
164 |
} |
|
165 |
moreover |
|
166 |
-- "now the other direction:" |
|
19796 | 167 |
{ fix s s' assume "if": "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" |
12431 | 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:" |
|
34055 | 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 |
|
12431 | 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" |
|
19796 | 176 |
with "if" have "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto |
12431 | 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 |
|
18372 | 182 |
have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule WhileTrue) |
12431 | 183 |
} |
18372 | 184 |
ultimately |
12431 | 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 |
||
34055 | 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 |
||
12431 | 256 |
|
257 |
subsection "Execution is deterministic" |
|
1700 | 258 |
|
12431 | 259 |
text {* |
34055 | 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 {* |
|
12431 | 267 |
The following proof presents all the details: |
268 |
*} |
|
18372 | 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" |
|
41529 | 272 |
using assms |
20503 | 273 |
proof (induct arbitrary: u set: evalc) |
18372 | 274 |
fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u" |
34055 | 275 |
thus "u = s" by blast |
18372 | 276 |
next |
277 |
fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u" |
|
34055 | 278 |
thus "u = s[x \<mapsto> a s]" by blast |
18372 | 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" |
|
12431 | 283 |
|
18372 | 284 |
assume "\<langle>c0;c1, s\<rangle> \<longrightarrow>\<^sub>c u" |
285 |
then obtain s' where |
|
12431 | 286 |
c0: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" and |
18372 | 287 |
c1: "\<langle>c1,s'\<rangle> \<longrightarrow>\<^sub>c u" |
288 |
by auto |
|
12431 | 289 |
|
18372 | 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" |
|
12431 | 295 |
|
18372 | 296 |
assume "b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u" |
34055 | 297 |
hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by blast |
18372 | 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" |
|
1700 | 302 |
|
18372 | 303 |
assume "\<not>b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u" |
34055 | 304 |
hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by blast |
18372 | 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" |
|
34055 | 309 |
thus "u = s" by blast |
18372 | 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 |
|
12431 | 317 |
c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and |
18372 | 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 |
|
12431 | 323 |
qed |
324 |
||
1700 | 325 |
|
12431 | 326 |
text {* |
327 |
This is the proof as you might present it in a lecture. The remaining |
|
18372 | 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" |
|
41529 | 333 |
using assms |
20503 | 334 |
proof (induct arbitrary: u) |
18372 | 335 |
-- "the simple @{text \<SKIP>} case for demonstration:" |
336 |
fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u" |
|
34055 | 337 |
thus "u = s" by blast |
18372 | 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 |
|
12431 | 346 |
c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and |
347 |
w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u" |
|
18372 | 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 |
|
34055 | 352 |
qed blast+ -- "prove the rest automatically" |
1700 | 353 |
|
354 |
end |