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