author | paulson |
Wed, 21 Dec 2005 12:02:57 +0100 | |
changeset 18447 | da548623916a |
parent 18372 | 2bffdf62fe7f |
child 18557 | 60a0f9caa0a2 |
permissions | -rw-r--r-- |
12431 | 1 |
(* Title: HOL/IMP/Transition.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow & Robert Sandner, TUM |
|
4 |
Isar Version: Gerwin Klein, 2001 |
|
5 |
Copyright 1996 TUM |
|
1700 | 6 |
*) |
7 |
||
12431 | 8 |
header "Transition Semantics of Commands" |
9 |
||
16417 | 10 |
theory Transition imports Natural begin |
12431 | 11 |
|
12 |
subsection "The transition relation" |
|
1700 | 13 |
|
12431 | 14 |
text {* |
15 |
We formalize the transition semantics as in \cite{Nielson}. This |
|
16 |
makes some of the rules a bit more intuitive, but also requires |
|
17 |
some more (internal) formal overhead. |
|
18372 | 18 |
|
19 |
Since configurations that have terminated are written without |
|
20 |
a statement, the transition relation is not |
|
12431 | 21 |
@{typ "((com \<times> state) \<times> (com \<times> state)) set"} |
22 |
but instead: |
|
23 |
*} |
|
24 |
consts evalc1 :: "((com option \<times> state) \<times> (com option \<times> state)) set" |
|
4906 | 25 |
|
12431 | 26 |
text {* |
18372 | 27 |
Some syntactic sugar that we will use to hide the |
12431 | 28 |
@{text option} part in configurations: |
29 |
*} |
|
4906 | 30 |
syntax |
12546 | 31 |
"_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>") |
32 |
"_angle2" :: "state \<Rightarrow> com option \<times> state" ("<_>") |
|
12431 | 33 |
|
34 |
syntax (xsymbols) |
|
12546 | 35 |
"_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>") |
36 |
"_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>") |
|
12431 | 37 |
|
14565 | 38 |
syntax (HTML output) |
39 |
"_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>") |
|
40 |
"_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>") |
|
41 |
||
12431 | 42 |
translations |
43 |
"\<langle>c,s\<rangle>" == "(Some c, s)" |
|
44 |
"\<langle>s\<rangle>" == "(None, s)" |
|
45 |
||
46 |
text {* |
|
47 |
More syntactic sugar for the transition relation, and its |
|
48 |
iteration. |
|
49 |
*} |
|
50 |
syntax |
|
12546 | 51 |
"_evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool" |
12434 | 52 |
("_ -1-> _" [60,60] 60) |
12546 | 53 |
"_evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool" |
12434 | 54 |
("_ -_-> _" [60,60,60] 60) |
12546 | 55 |
"_evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool" |
12434 | 56 |
("_ -*-> _" [60,60] 60) |
12431 | 57 |
|
58 |
syntax (xsymbols) |
|
12546 | 59 |
"_evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool" |
12434 | 60 |
("_ \<longrightarrow>\<^sub>1 _" [60,60] 61) |
12546 | 61 |
"_evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool" |
12434 | 62 |
("_ -_\<rightarrow>\<^sub>1 _" [60,60,60] 60) |
12546 | 63 |
"_evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool" |
12434 | 64 |
("_ \<longrightarrow>\<^sub>1\<^sup>* _" [60,60] 60) |
1700 | 65 |
|
66 |
translations |
|
12431 | 67 |
"cs \<longrightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1" |
18372 | 68 |
"cs -n\<rightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1^n" |
69 |
"cs \<longrightarrow>\<^sub>1\<^sup>* cs'" == "(cs,cs') \<in> evalc1^*" |
|
12431 | 70 |
|
18372 | 71 |
-- {* Isabelle/HOL converts @{text "(cs0,(c1,s1))"} to @{term "(cs0,c1,s1)"}, |
12431 | 72 |
so we also include: *} |
18372 | 73 |
"cs0 \<longrightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1" |
12431 | 74 |
"cs0 -n\<rightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^n" |
18372 | 75 |
"cs0 \<longrightarrow>\<^sub>1\<^sup>* (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^*" |
12431 | 76 |
|
77 |
text {* |
|
78 |
Now, finally, we are set to write down the rules for our small step semantics: |
|
79 |
*} |
|
80 |
inductive evalc1 |
|
81 |
intros |
|
18372 | 82 |
Skip: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" |
12431 | 83 |
Assign: "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> a s]\<rangle>" |
84 |
||
85 |
Semi1: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0;c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s'\<rangle>" |
|
86 |
Semi2: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0',s'\<rangle> \<Longrightarrow> \<langle>c0;c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0';c1,s'\<rangle>" |
|
87 |
||
88 |
IfTrue: "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c1 \<ELSE> c2,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>" |
|
89 |
IfFalse: "\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c1 \<ELSE> c2,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c2,s\<rangle>" |
|
90 |
||
91 |
While: "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>,s\<rangle>" |
|
92 |
||
93 |
lemmas [intro] = evalc1.intros -- "again, use these rules in automatic proofs" |
|
94 |
||
95 |
(*<*) |
|
96 |
(* fixme: move to Relation_Power.thy *) |
|
97 |
lemma rel_pow_Suc_E2 [elim!]: |
|
98 |
"[| (x, z) \<in> R ^ Suc n; !!y. [| (x, y) \<in> R; (y, z) \<in> R ^ n |] ==> P |] ==> P" |
|
18372 | 99 |
by (blast dest: rel_pow_Suc_D2) |
12431 | 100 |
|
101 |
lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n" |
|
18372 | 102 |
proof (induct p) |
103 |
fix x y |
|
104 |
assume "(x, y) \<in> R\<^sup>*" |
|
105 |
thus "\<exists>n. (x, y) \<in> R^n" |
|
12431 | 106 |
proof induct |
18372 | 107 |
fix a have "(a, a) \<in> R^0" by simp |
108 |
thus "\<exists>n. (a, a) \<in> R ^ n" .. |
|
12431 | 109 |
next |
18372 | 110 |
fix a b c assume "\<exists>n. (a, b) \<in> R ^ n" |
111 |
then obtain n where "(a, b) \<in> R^n" .. |
|
112 |
moreover assume "(b, c) \<in> R" |
|
113 |
ultimately have "(a, c) \<in> R^(Suc n)" by auto |
|
114 |
thus "\<exists>n. (a, c) \<in> R^n" .. |
|
12431 | 115 |
qed |
18372 | 116 |
qed |
117 |
(*>*) |
|
12431 | 118 |
text {* |
18372 | 119 |
As for the big step semantics you can read these rules in a |
12431 | 120 |
syntax directed way: |
121 |
*} |
|
18372 | 122 |
lemma SKIP_1: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s\<rangle>)" |
123 |
by (rule, cases set: evalc1, auto) |
|
12431 | 124 |
|
125 |
lemma Assign_1: "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s[x \<mapsto> a s]\<rangle>)" |
|
126 |
by (rule, cases set: evalc1, auto) |
|
127 |
||
18372 | 128 |
lemma Cond_1: |
12431 | 129 |
"\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 y = ((b s \<longrightarrow> y = \<langle>c1, s\<rangle>) \<and> (\<not>b s \<longrightarrow> y = \<langle>c2, s\<rangle>))" |
130 |
by (rule, cases set: evalc1, auto) |
|
131 |
||
18372 | 132 |
lemma While_1: |
12434 | 133 |
"\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>, s\<rangle>)" |
12431 | 134 |
by (rule, cases set: evalc1, auto) |
135 |
||
136 |
lemmas [simp] = SKIP_1 Assign_1 Cond_1 While_1 |
|
137 |
||
138 |
||
139 |
subsection "Examples" |
|
140 |
||
18372 | 141 |
lemma |
12434 | 142 |
"s x = 0 \<Longrightarrow> \<langle>\<WHILE> \<lambda>s. s x \<noteq> 1 \<DO> (x:== \<lambda>s. s x+1), s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x \<mapsto> 1]\<rangle>" |
12431 | 143 |
(is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* _") |
144 |
proof - |
|
12434 | 145 |
let ?c = "x:== \<lambda>s. s x+1" |
146 |
let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>" |
|
12431 | 147 |
assume [simp]: "s x = 0" |
148 |
have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" .. |
|
18372 | 149 |
also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp |
150 |
also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 1]\<rangle>" by (rule Semi1) simp |
|
12431 | 151 |
also have "\<langle>?w, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 1]\<rangle>" .. |
152 |
also have "\<langle>?if, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle>" by (simp add: update_def) |
|
153 |
also have "\<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> 1]\<rangle>" .. |
|
154 |
finally show ?thesis .. |
|
155 |
qed |
|
4906 | 156 |
|
18372 | 157 |
lemma |
12434 | 158 |
"s x = 2 \<Longrightarrow> \<langle>\<WHILE> \<lambda>s. s x \<noteq> 1 \<DO> (x:== \<lambda>s. s x+1), s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'" |
12431 | 159 |
(is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'") |
160 |
proof - |
|
161 |
let ?c = "x:== \<lambda>s. s x+1" |
|
18372 | 162 |
let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>" |
12431 | 163 |
assume [simp]: "s x = 2" |
164 |
note update_def [simp] |
|
165 |
have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" .. |
|
166 |
also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp |
|
18372 | 167 |
also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 3]\<rangle>" by (rule Semi1) simp |
12431 | 168 |
also have "\<langle>?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 3]\<rangle>" .. |
169 |
also have "\<langle>?if, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s[x \<mapsto> 3]\<rangle>" by simp |
|
18372 | 170 |
also have "\<langle>?c; ?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 4]\<rangle>" by (rule Semi1) simp |
12431 | 171 |
also have "\<langle>?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 4]\<rangle>" .. |
172 |
also have "\<langle>?if, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s[x \<mapsto> 4]\<rangle>" by simp |
|
18372 | 173 |
also have "\<langle>?c; ?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 5]\<rangle>" by (rule Semi1) simp |
12431 | 174 |
oops |
175 |
||
176 |
subsection "Basic properties" |
|
177 |
||
18372 | 178 |
text {* |
12431 | 179 |
There are no \emph{stuck} programs: |
180 |
*} |
|
181 |
lemma no_stuck: "\<exists>y. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 y" |
|
182 |
proof (induct c) |
|
183 |
-- "case Semi:" |
|
18372 | 184 |
fix c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" |
12431 | 185 |
then obtain y where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" .. |
186 |
then obtain c1' s' where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<or> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1',s'\<rangle>" |
|
18372 | 187 |
by (cases y, cases "fst y") auto |
12431 | 188 |
thus "\<exists>s'. \<langle>c1;c2,s\<rangle> \<longrightarrow>\<^sub>1 s'" by auto |
189 |
next |
|
190 |
-- "case If:" |
|
191 |
fix b c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" and "\<exists>y. \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>1 y" |
|
192 |
thus "\<exists>y. \<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 y" by (cases "b s") auto |
|
193 |
qed auto -- "the rest is trivial" |
|
194 |
||
195 |
text {* |
|
196 |
If a configuration does not contain a statement, the program |
|
197 |
has terminated and there is no next configuration: |
|
198 |
*} |
|
18372 | 199 |
lemma stuck [elim!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1 y \<Longrightarrow> P" |
12434 | 200 |
by (auto elim: evalc1.elims) |
201 |
||
18372 | 202 |
lemma evalc_None_retrancl [simp, dest!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = \<langle>s\<rangle>" |
203 |
by (induct set: rtrancl) auto |
|
12431 | 204 |
|
205 |
(*<*) |
|
18372 | 206 |
(* FIXME: relpow.simps don't work *) |
12431 | 207 |
lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by simp |
18372 | 208 |
lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp |
12431 | 209 |
lemmas [simp del] = relpow.simps |
210 |
(*>*) |
|
12434 | 211 |
lemma evalc1_None_0 [simp, dest!]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)" |
12431 | 212 |
by (cases n) auto |
4906 | 213 |
|
18372 | 214 |
lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1" |
12431 | 215 |
by (cases n) auto |
216 |
||
217 |
subsection "Equivalence to natural semantics (after Nielson and Nielson)" |
|
218 |
||
219 |
text {* |
|
220 |
We first need two lemmas about semicolon statements: |
|
221 |
decomposition and composition. |
|
222 |
*} |
|
223 |
lemma semiD: |
|
18372 | 224 |
"\<langle>c1; c2, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> |
12431 | 225 |
\<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> n = i+j" |
18372 | 226 |
proof (induct n fixing: c1 c2 s s'') |
227 |
case 0 |
|
228 |
then show ?case by simp |
|
12431 | 229 |
next |
18372 | 230 |
case (Suc n) |
231 |
||
232 |
from `\<langle>c1; c2, s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>` |
|
233 |
obtain y where |
|
12431 | 234 |
1: "\<langle>c1; c2, s\<rangle> \<longrightarrow>\<^sub>1 y" and |
235 |
n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" |
|
18372 | 236 |
by blast |
12431 | 237 |
|
18372 | 238 |
from 1 |
239 |
show "\<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> Suc n = i+j" |
|
240 |
(is "\<exists>i j s'. ?Q i j s'") |
|
241 |
proof (cases set: evalc1) |
|
242 |
case Semi1 |
|
243 |
then obtain s' where |
|
12431 | 244 |
"y = \<langle>c2, s'\<rangle>" and "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>" |
18372 | 245 |
by auto |
246 |
with 1 n have "?Q 1 n s'" by simp |
|
247 |
thus ?thesis by blast |
|
248 |
next |
|
249 |
case Semi2 |
|
250 |
then obtain c1' s' where |
|
12431 | 251 |
y: "y = \<langle>c1'; c2, s'\<rangle>" and |
252 |
c1: "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'\<rangle>" |
|
18372 | 253 |
by auto |
254 |
with n have "\<langle>c1'; c2, s'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp |
|
255 |
with Suc.hyps obtain i j s0 where |
|
12431 | 256 |
c1': "\<langle>c1',s'\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and |
257 |
c2: "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and |
|
258 |
i: "n = i+j" |
|
18372 | 259 |
by fast |
260 |
||
261 |
from c1 c1' |
|
262 |
have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto intro: rel_pow_Suc_I2) |
|
263 |
with c2 i |
|
264 |
have "?Q (i+1) j s0" by simp |
|
265 |
thus ?thesis by blast |
|
266 |
qed auto -- "the remaining cases cannot occur" |
|
12431 | 267 |
qed |
1700 | 268 |
|
269 |
||
18372 | 270 |
lemma semiI: |
271 |
"\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" |
|
272 |
proof (induct n fixing: c0 s s'') |
|
273 |
case 0 |
|
274 |
from `\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>` |
|
275 |
have False by simp |
|
276 |
thus ?case .. |
|
12431 | 277 |
next |
18372 | 278 |
case (Suc n) |
279 |
note c0 = `\<langle>c0,s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>` |
|
280 |
note c1 = `\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>` |
|
281 |
note IH = `\<And>c0 s s''. |
|
282 |
\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>` |
|
283 |
from c0 obtain y where |
|
12431 | 284 |
1: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 y" and n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast |
285 |
from 1 obtain c0' s0' where |
|
18372 | 286 |
"y = \<langle>s0'\<rangle> \<or> y = \<langle>c0', s0'\<rangle>" |
287 |
by (cases y, cases "fst y") auto |
|
12431 | 288 |
moreover |
289 |
{ assume y: "y = \<langle>s0'\<rangle>" |
|
290 |
with n have "s'' = s0'" by simp |
|
291 |
with y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1, s''\<rangle>" by blast |
|
292 |
with c1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans) |
|
293 |
} |
|
294 |
moreover |
|
295 |
{ assume y: "y = \<langle>c0', s0'\<rangle>" |
|
296 |
with n have "\<langle>c0', s0'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast |
|
297 |
with IH c1 have "\<langle>c0'; c1,s0'\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast |
|
298 |
moreover |
|
299 |
from y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0'; c1,s0'\<rangle>" by blast |
|
300 |
hence "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c0'; c1,s0'\<rangle>" by blast |
|
301 |
ultimately |
|
302 |
have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans) |
|
303 |
} |
|
304 |
ultimately |
|
305 |
show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast |
|
306 |
qed |
|
307 |
||
308 |
text {* |
|
309 |
The easy direction of the equivalence proof: |
|
310 |
*} |
|
18372 | 311 |
lemma evalc_imp_evalc1: |
312 |
assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
313 |
shows "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" |
|
314 |
using prems |
|
315 |
proof induct |
|
316 |
fix s show "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" by auto |
|
317 |
next |
|
318 |
fix x a s show "\<langle>x :== a ,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x\<mapsto>a s]\<rangle>" by auto |
|
319 |
next |
|
320 |
fix c0 c1 s s'' s' |
|
321 |
assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>" |
|
322 |
then obtain n where "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow) |
|
323 |
moreover |
|
324 |
assume "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" |
|
325 |
ultimately |
|
326 |
show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule semiI) |
|
327 |
next |
|
328 |
fix s::state and b c0 c1 s' |
|
329 |
assume "b s" |
|
330 |
hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0,s\<rangle>" by simp |
|
331 |
also assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" |
|
332 |
finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" . |
|
333 |
next |
|
334 |
fix s::state and b c0 c1 s' |
|
335 |
assume "\<not>b s" |
|
336 |
hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>" by simp |
|
337 |
also assume "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" |
|
338 |
finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" . |
|
339 |
next |
|
340 |
fix b c and s::state |
|
341 |
assume b: "\<not>b s" |
|
342 |
let ?if = "\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>" |
|
343 |
have "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast |
|
344 |
also have "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" by (simp add: b) |
|
345 |
also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" by blast |
|
346 |
finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" .. |
|
347 |
next |
|
348 |
fix b c s s'' s' |
|
349 |
let ?w = "\<WHILE> b \<DO> c" |
|
350 |
let ?if = "\<IF> b \<THEN> c; ?w \<ELSE> \<SKIP>" |
|
351 |
assume w: "\<langle>?w,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" |
|
352 |
assume c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>" |
|
353 |
assume b: "b s" |
|
354 |
have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast |
|
355 |
also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c; ?w, s\<rangle>" by (simp add: b) |
|
356 |
also |
|
357 |
from c obtain n where "\<langle>c,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow) |
|
358 |
with w have "\<langle>c; ?w,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by - (rule semiI) |
|
359 |
finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .. |
|
12431 | 360 |
qed |
361 |
||
362 |
text {* |
|
363 |
Finally, the equivalence theorem: |
|
364 |
*} |
|
365 |
theorem evalc_equiv_evalc1: |
|
366 |
"\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" |
|
367 |
proof |
|
368 |
assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
369 |
show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1) |
|
18372 | 370 |
next |
12431 | 371 |
assume "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" |
372 |
then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow) |
|
373 |
moreover |
|
18372 | 374 |
have "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" |
375 |
proof (induct fixing: c s s' rule: less_induct) |
|
12431 | 376 |
fix n |
18372 | 377 |
assume IH: "\<And>m c s s'. m < n \<Longrightarrow> \<langle>c,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" |
12431 | 378 |
fix c s s' |
379 |
assume c: "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" |
|
380 |
then obtain m where n: "n = Suc m" by (cases n) auto |
|
18372 | 381 |
with c obtain y where |
12431 | 382 |
c': "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1 y" and m: "y -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by blast |
18372 | 383 |
show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" |
12431 | 384 |
proof (cases c) |
385 |
case SKIP |
|
386 |
with c n show ?thesis by auto |
|
18372 | 387 |
next |
12431 | 388 |
case Assign |
389 |
with c n show ?thesis by auto |
|
390 |
next |
|
391 |
fix c1 c2 assume semi: "c = (c1; c2)" |
|
392 |
with c obtain i j s'' where |
|
18372 | 393 |
c1: "\<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and |
394 |
c2: "\<langle>c2, s''\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" and |
|
395 |
ij: "n = i+j" |
|
12431 | 396 |
by (blast dest: semiD) |
18372 | 397 |
from c1 c2 obtain |
12431 | 398 |
"0 < i" and "0 < j" by (cases i, auto, cases j, auto) |
399 |
with ij obtain |
|
400 |
i: "i < n" and j: "j < n" by simp |
|
18372 | 401 |
from IH i c1 |
402 |
have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" . |
|
12431 | 403 |
moreover |
18372 | 404 |
from IH j c2 |
405 |
have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" . |
|
12431 | 406 |
moreover |
407 |
note semi |
|
408 |
ultimately |
|
409 |
show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
410 |
next |
|
411 |
fix b c1 c2 assume If: "c = \<IF> b \<THEN> c1 \<ELSE> c2" |
|
412 |
{ assume True: "b s = True" |
|
413 |
with If c n |
|
18372 | 414 |
have "\<langle>c1,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto |
12431 | 415 |
with n IH |
416 |
have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
417 |
with If True |
|
18372 | 418 |
have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp |
12431 | 419 |
} |
420 |
moreover |
|
421 |
{ assume False: "b s = False" |
|
422 |
with If c n |
|
18372 | 423 |
have "\<langle>c2,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto |
12431 | 424 |
with n IH |
425 |
have "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
426 |
with If False |
|
18372 | 427 |
have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp |
12431 | 428 |
} |
429 |
ultimately |
|
430 |
show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases "b s") auto |
|
431 |
next |
|
432 |
fix b c' assume w: "c = \<WHILE> b \<DO> c'" |
|
18372 | 433 |
with c n |
12431 | 434 |
have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" |
435 |
(is "\<langle>?if,_\<rangle> -m\<rightarrow>\<^sub>1 _") by auto |
|
436 |
with n IH |
|
437 |
have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
438 |
moreover note unfold_while [of b c'] |
|
439 |
-- {* @{thm unfold_while [of b c']} *} |
|
18372 | 440 |
ultimately |
12431 | 441 |
have "\<langle>\<WHILE> b \<DO> c',s\<rangle> \<longrightarrow>\<^sub>c s'" by (blast dest: equivD2) |
442 |
with w show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp |
|
443 |
qed |
|
444 |
qed |
|
445 |
ultimately |
|
446 |
show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
447 |
qed |
|
448 |
||
449 |
||
450 |
subsection "Winskel's Proof" |
|
451 |
||
452 |
declare rel_pow_0_E [elim!] |
|
453 |
||
454 |
text {* |
|
18372 | 455 |
Winskel's small step rules are a bit different \cite{Winskel}; |
12431 | 456 |
we introduce their equivalents as derived rules: |
457 |
*} |
|
458 |
lemma whileFalse1 [intro]: |
|
18372 | 459 |
"\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>") |
12431 | 460 |
proof - |
461 |
assume "\<not>b s" |
|
462 |
have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" .. |
|
463 |
also have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" .. |
|
464 |
also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" .. |
|
465 |
finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" .. |
|
466 |
qed |
|
467 |
||
468 |
lemma whileTrue1 [intro]: |
|
18372 | 469 |
"b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;\<WHILE> b \<DO> c, s\<rangle>" |
12431 | 470 |
(is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>") |
471 |
proof - |
|
472 |
assume "b s" |
|
473 |
have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" .. |
|
474 |
also have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c;?w, s\<rangle>" .. |
|
475 |
finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>" .. |
|
476 |
qed |
|
1700 | 477 |
|
18372 | 478 |
inductive_cases evalc1_SEs: |
479 |
"\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1 t" |
|
12431 | 480 |
"\<langle>x:==a,s\<rangle> \<longrightarrow>\<^sub>1 t" |
481 |
"\<langle>c1;c2, s\<rangle> \<longrightarrow>\<^sub>1 t" |
|
482 |
"\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 t" |
|
483 |
"\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 t" |
|
484 |
||
485 |
inductive_cases evalc1_E: "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 t" |
|
486 |
||
487 |
declare evalc1_SEs [elim!] |
|
488 |
||
489 |
lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>" |
|
18372 | 490 |
apply (induct set: evalc) |
12431 | 491 |
|
18372 | 492 |
-- SKIP |
12431 | 493 |
apply blast |
494 |
||
18372 | 495 |
-- ASSIGN |
12431 | 496 |
apply fast |
497 |
||
18372 | 498 |
-- SEMI |
12431 | 499 |
apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI) |
500 |
||
18372 | 501 |
-- IF |
12566
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12546
diff
changeset
|
502 |
apply (fast intro: converse_rtrancl_into_rtrancl) |
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12546
diff
changeset
|
503 |
apply (fast intro: converse_rtrancl_into_rtrancl) |
12431 | 504 |
|
18372 | 505 |
-- WHILE |
12431 | 506 |
apply fast |
12566
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12546
diff
changeset
|
507 |
apply (fast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI) |
12431 | 508 |
|
509 |
done |
|
510 |
||
511 |
||
18372 | 512 |
lemma lemma2: |
513 |
"\<langle>c;d,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<Longrightarrow> \<exists>t m. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<and> \<langle>d,t\<rangle> -m\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<and> m \<le> n" |
|
514 |
apply (induct n fixing: c d s u) |
|
12431 | 515 |
-- "case n = 0" |
516 |
apply fastsimp |
|
517 |
-- "induction step" |
|
18372 | 518 |
apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2 |
12566
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12546
diff
changeset
|
519 |
elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl) |
12431 | 520 |
done |
521 |
||
18372 | 522 |
lemma evalc1_impl_evalc: |
523 |
"\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" |
|
524 |
apply (induct c fixing: s t) |
|
12431 | 525 |
apply (safe dest!: rtrancl_imp_UN_rel_pow) |
526 |
||
527 |
-- SKIP |
|
528 |
apply (simp add: SKIP_n) |
|
529 |
||
18372 | 530 |
-- ASSIGN |
12431 | 531 |
apply (fastsimp elim: rel_pow_E2) |
532 |
||
533 |
-- SEMI |
|
534 |
apply (fast dest!: rel_pow_imp_rtrancl lemma2) |
|
535 |
||
18372 | 536 |
-- IF |
12431 | 537 |
apply (erule rel_pow_E2) |
538 |
apply simp |
|
539 |
apply (fast dest!: rel_pow_imp_rtrancl) |
|
540 |
||
541 |
-- "WHILE, induction on the length of the computation" |
|
542 |
apply (rename_tac b c s t n) |
|
543 |
apply (erule_tac P = "?X -n\<rightarrow>\<^sub>1 ?Y" in rev_mp) |
|
544 |
apply (rule_tac x = "s" in spec) |
|
18372 | 545 |
apply (induct_tac n rule: nat_less_induct) |
12431 | 546 |
apply (intro strip) |
547 |
apply (erule rel_pow_E2) |
|
548 |
apply simp |
|
549 |
apply (erule evalc1_E) |
|
550 |
||
551 |
apply simp |
|
552 |
apply (case_tac "b x") |
|
553 |
-- WhileTrue |
|
554 |
apply (erule rel_pow_E2) |
|
555 |
apply simp |
|
556 |
apply (clarify dest!: lemma2) |
|
18372 | 557 |
apply atomize |
12431 | 558 |
apply (erule allE, erule allE, erule impE, assumption) |
559 |
apply (erule_tac x=mb in allE, erule impE, fastsimp) |
|
560 |
apply blast |
|
18372 | 561 |
-- WhileFalse |
12431 | 562 |
apply (erule rel_pow_E2) |
563 |
apply simp |
|
564 |
apply (simp add: SKIP_n) |
|
565 |
done |
|
566 |
||
567 |
||
568 |
text {* proof of the equivalence of evalc and evalc1 *} |
|
569 |
lemma evalc1_eq_evalc: "(\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle>) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)" |
|
18372 | 570 |
by (fast elim!: evalc1_impl_evalc evalc_impl_evalc1) |
12431 | 571 |
|
572 |
||
573 |
subsection "A proof without n" |
|
574 |
||
575 |
text {* |
|
576 |
The inductions are a bit awkward to write in this section, |
|
577 |
because @{text None} as result statement in the small step |
|
578 |
semantics doesn't have a direct counterpart in the big step |
|
18372 | 579 |
semantics. |
1700 | 580 |
|
12431 | 581 |
Winskel's small step rule set (using the @{text "\<SKIP>"} statement |
582 |
to indicate termination) is better suited for this proof. |
|
583 |
*} |
|
584 |
||
18372 | 585 |
lemma my_lemma1: |
586 |
assumes "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>" |
|
587 |
and "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" |
|
588 |
shows "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" |
|
12431 | 589 |
proof - |
590 |
-- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *} |
|
18372 | 591 |
from prems |
592 |
have "\<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" |
|
593 |
apply (induct rule: converse_rtrancl_induct2) |
|
12431 | 594 |
apply simp |
595 |
apply (rename_tac c s') |
|
596 |
apply simp |
|
597 |
apply (rule conjI) |
|
18372 | 598 |
apply fast |
12431 | 599 |
apply clarify |
600 |
apply (case_tac c) |
|
12566
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12546
diff
changeset
|
601 |
apply (auto intro: converse_rtrancl_into_rtrancl) |
12431 | 602 |
done |
18372 | 603 |
then show ?thesis by simp |
12431 | 604 |
qed |
605 |
||
13524 | 606 |
lemma evalc_impl_evalc1': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>" |
18372 | 607 |
apply (induct set: evalc) |
12431 | 608 |
|
18372 | 609 |
-- SKIP |
12431 | 610 |
apply fast |
611 |
||
612 |
-- ASSIGN |
|
613 |
apply fast |
|
614 |
||
18372 | 615 |
-- SEMI |
12431 | 616 |
apply (fast intro: my_lemma1) |
617 |
||
618 |
-- IF |
|
12566
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12546
diff
changeset
|
619 |
apply (fast intro: converse_rtrancl_into_rtrancl) |
18372 | 620 |
apply (fast intro: converse_rtrancl_into_rtrancl) |
12431 | 621 |
|
18372 | 622 |
-- WHILE |
12431 | 623 |
apply fast |
12566
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12546
diff
changeset
|
624 |
apply (fast intro: converse_rtrancl_into_rtrancl my_lemma1) |
12431 | 625 |
|
626 |
done |
|
627 |
||
628 |
text {* |
|
629 |
The opposite direction is based on a Coq proof done by Ranan Fraer and |
|
630 |
Yves Bertot. The following sketch is from an email by Ranan Fraer. |
|
631 |
||
632 |
\begin{verbatim} |
|
633 |
First we've broke it into 2 lemmas: |
|
1700 | 634 |
|
12431 | 635 |
Lemma 1 |
636 |
((c,s) --> (SKIP,t)) => (<c,s> -c-> t) |
|
637 |
||
638 |
This is a quick one, dealing with the cases skip, assignment |
|
639 |
and while_false. |
|
640 |
||
641 |
Lemma 2 |
|
642 |
((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t |
|
18372 | 643 |
=> |
12431 | 644 |
<c,s> -c-> t |
645 |
||
646 |
This is proved by rule induction on the -*-> relation |
|
18372 | 647 |
and the induction step makes use of a third lemma: |
12431 | 648 |
|
649 |
Lemma 3 |
|
650 |
((c,s) --> (c',s')) /\ <c',s'> -c'-> t |
|
18372 | 651 |
=> |
12431 | 652 |
<c,s> -c-> t |
653 |
||
18372 | 654 |
This captures the essence of the proof, as it shows that <c',s'> |
12431 | 655 |
behaves as the continuation of <c,s> with respect to the natural |
656 |
semantics. |
|
657 |
The proof of Lemma 3 goes by rule induction on the --> relation, |
|
658 |
dealing with the cases sequence1, sequence2, if_true, if_false and |
|
659 |
while_true. In particular in the case (sequence1) we make use again |
|
660 |
of Lemma 1. |
|
661 |
\end{verbatim} |
|
662 |
*} |
|
663 |
||
664 |
inductive_cases evalc1_term_cases: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>" |
|
665 |
||
18372 | 666 |
lemma FB_lemma3: |
667 |
"(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow> |
|
668 |
\<langle>if c'=None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t" |
|
669 |
by (induct fixing: t set: evalc1) |
|
670 |
(auto elim!: evalc1_term_cases equivD2 [OF unfold_while]) |
|
12431 | 671 |
|
18372 | 672 |
lemma FB_lemma2: |
673 |
"(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow> |
|
674 |
\<langle>if c' = None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t" |
|
18447 | 675 |
apply (induct rule: converse_rtrancl_induct2, force) |
12434 | 676 |
apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3) |
12431 | 677 |
done |
678 |
||
13524 | 679 |
lemma evalc1_impl_evalc': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" |
18372 | 680 |
by (fastsimp dest: FB_lemma2) |
1700 | 681 |
|
682 |
end |