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