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