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