author | wenzelm |
Sun, 28 Nov 2010 14:01:20 +0100 | |
changeset 40781 | ba5be5c3d477 |
parent 34990 | 81e8fdfeb849 |
child 41529 | ba60efa2fd08 |
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 |
|
34990 | 208 |
from `co = Some c2` and `\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'''\<rangle>` and 1 n |
209 |
have "?Q 1 n s'''" by simp |
|
18372 | 210 |
thus ?thesis by blast |
211 |
next |
|
34990 | 212 |
case (Semi2 c1') |
213 |
note c1 = `\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'''\<rangle>` |
|
214 |
with `co = Some (c1'; c2)` and n |
|
215 |
have "\<langle>c1'; c2, s'''\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp |
|
18372 | 216 |
with Suc.hyps obtain i j s0 where |
34990 | 217 |
c1': "\<langle>c1',s'''\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and |
12431 | 218 |
c2: "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and |
219 |
i: "n = i+j" |
|
18372 | 220 |
by fast |
221 |
||
222 |
from c1 c1' |
|
223 |
have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto intro: rel_pow_Suc_I2) |
|
224 |
with c2 i |
|
225 |
have "?Q (i+1) j s0" by simp |
|
226 |
thus ?thesis by blast |
|
34990 | 227 |
qed |
12431 | 228 |
qed |
1700 | 229 |
|
230 |
||
18372 | 231 |
lemma semiI: |
232 |
"\<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 | 233 |
proof (induct n arbitrary: c0 s s'') |
18372 | 234 |
case 0 |
235 |
from `\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>` |
|
236 |
have False by simp |
|
237 |
thus ?case .. |
|
12431 | 238 |
next |
18372 | 239 |
case (Suc n) |
240 |
note c0 = `\<langle>c0,s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>` |
|
241 |
note c1 = `\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>` |
|
242 |
note IH = `\<And>c0 s s''. |
|
243 |
\<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>` |
|
244 |
from c0 obtain y where |
|
12431 | 245 |
1: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 y" and n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast |
246 |
from 1 obtain c0' s0' where |
|
18372 | 247 |
"y = \<langle>s0'\<rangle> \<or> y = \<langle>c0', s0'\<rangle>" |
248 |
by (cases y, cases "fst y") auto |
|
12431 | 249 |
moreover |
250 |
{ assume y: "y = \<langle>s0'\<rangle>" |
|
251 |
with n have "s'' = s0'" by simp |
|
252 |
with y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1, s''\<rangle>" by blast |
|
253 |
with c1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans) |
|
254 |
} |
|
255 |
moreover |
|
256 |
{ assume y: "y = \<langle>c0', s0'\<rangle>" |
|
257 |
with n have "\<langle>c0', s0'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast |
|
258 |
with IH c1 have "\<langle>c0'; c1,s0'\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast |
|
259 |
moreover |
|
260 |
from y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0'; c1,s0'\<rangle>" by blast |
|
261 |
hence "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c0'; c1,s0'\<rangle>" by blast |
|
262 |
ultimately |
|
263 |
have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans) |
|
264 |
} |
|
265 |
ultimately |
|
266 |
show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast |
|
267 |
qed |
|
268 |
||
269 |
text {* |
|
270 |
The easy direction of the equivalence proof: |
|
271 |
*} |
|
18372 | 272 |
lemma evalc_imp_evalc1: |
273 |
assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
274 |
shows "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" |
|
275 |
using prems |
|
276 |
proof induct |
|
277 |
fix s show "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" by auto |
|
278 |
next |
|
279 |
fix x a s show "\<langle>x :== a ,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x\<mapsto>a s]\<rangle>" by auto |
|
280 |
next |
|
281 |
fix c0 c1 s s'' s' |
|
282 |
assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>" |
|
283 |
then obtain n where "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow) |
|
284 |
moreover |
|
285 |
assume "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" |
|
286 |
ultimately |
|
287 |
show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule semiI) |
|
288 |
next |
|
289 |
fix s::state and b c0 c1 s' |
|
290 |
assume "b s" |
|
291 |
hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0,s\<rangle>" by simp |
|
292 |
also assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" |
|
293 |
finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" . |
|
294 |
next |
|
295 |
fix s::state and b c0 c1 s' |
|
296 |
assume "\<not>b s" |
|
297 |
hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>" by simp |
|
298 |
also assume "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" |
|
299 |
finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" . |
|
300 |
next |
|
301 |
fix b c and s::state |
|
302 |
assume b: "\<not>b s" |
|
303 |
let ?if = "\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>" |
|
304 |
have "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast |
|
305 |
also have "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" by (simp add: b) |
|
306 |
also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" by blast |
|
307 |
finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" .. |
|
308 |
next |
|
309 |
fix b c s s'' s' |
|
310 |
let ?w = "\<WHILE> b \<DO> c" |
|
311 |
let ?if = "\<IF> b \<THEN> c; ?w \<ELSE> \<SKIP>" |
|
312 |
assume w: "\<langle>?w,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" |
|
313 |
assume c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>" |
|
314 |
assume b: "b s" |
|
315 |
have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast |
|
316 |
also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c; ?w, s\<rangle>" by (simp add: b) |
|
317 |
also |
|
318 |
from c obtain n where "\<langle>c,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow) |
|
319 |
with w have "\<langle>c; ?w,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by - (rule semiI) |
|
320 |
finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .. |
|
12431 | 321 |
qed |
322 |
||
323 |
text {* |
|
324 |
Finally, the equivalence theorem: |
|
325 |
*} |
|
326 |
theorem evalc_equiv_evalc1: |
|
327 |
"\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" |
|
328 |
proof |
|
329 |
assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
23373 | 330 |
then show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1) |
18372 | 331 |
next |
12431 | 332 |
assume "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" |
333 |
then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow) |
|
334 |
moreover |
|
18372 | 335 |
have "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" |
20503 | 336 |
proof (induct arbitrary: c s s' rule: less_induct) |
12431 | 337 |
fix n |
18372 | 338 |
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 | 339 |
fix c s s' |
340 |
assume c: "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" |
|
341 |
then obtain m where n: "n = Suc m" by (cases n) auto |
|
18372 | 342 |
with c obtain y where |
12431 | 343 |
c': "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1 y" and m: "y -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by blast |
18372 | 344 |
show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" |
12431 | 345 |
proof (cases c) |
346 |
case SKIP |
|
347 |
with c n show ?thesis by auto |
|
18372 | 348 |
next |
12431 | 349 |
case Assign |
350 |
with c n show ?thesis by auto |
|
351 |
next |
|
352 |
fix c1 c2 assume semi: "c = (c1; c2)" |
|
353 |
with c obtain i j s'' where |
|
18372 | 354 |
c1: "\<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and |
355 |
c2: "\<langle>c2, s''\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" and |
|
356 |
ij: "n = i+j" |
|
12431 | 357 |
by (blast dest: semiD) |
18372 | 358 |
from c1 c2 obtain |
12431 | 359 |
"0 < i" and "0 < j" by (cases i, auto, cases j, auto) |
360 |
with ij obtain |
|
361 |
i: "i < n" and j: "j < n" by simp |
|
18372 | 362 |
from IH i c1 |
363 |
have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" . |
|
12431 | 364 |
moreover |
18372 | 365 |
from IH j c2 |
366 |
have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" . |
|
12431 | 367 |
moreover |
368 |
note semi |
|
369 |
ultimately |
|
370 |
show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
371 |
next |
|
372 |
fix b c1 c2 assume If: "c = \<IF> b \<THEN> c1 \<ELSE> c2" |
|
373 |
{ assume True: "b s = True" |
|
374 |
with If c n |
|
18372 | 375 |
have "\<langle>c1,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto |
12431 | 376 |
with n IH |
377 |
have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
378 |
with If True |
|
34055 | 379 |
have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
12431 | 380 |
} |
381 |
moreover |
|
382 |
{ assume False: "b s = False" |
|
383 |
with If c n |
|
18372 | 384 |
have "\<langle>c2,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto |
12431 | 385 |
with n IH |
386 |
have "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
387 |
with If False |
|
34055 | 388 |
have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
12431 | 389 |
} |
390 |
ultimately |
|
391 |
show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases "b s") auto |
|
392 |
next |
|
393 |
fix b c' assume w: "c = \<WHILE> b \<DO> c'" |
|
18372 | 394 |
with c n |
12431 | 395 |
have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" |
396 |
(is "\<langle>?if,_\<rangle> -m\<rightarrow>\<^sub>1 _") by auto |
|
397 |
with n IH |
|
398 |
have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
399 |
moreover note unfold_while [of b c'] |
|
400 |
-- {* @{thm unfold_while [of b c']} *} |
|
18372 | 401 |
ultimately |
12431 | 402 |
have "\<langle>\<WHILE> b \<DO> c',s\<rangle> \<longrightarrow>\<^sub>c s'" by (blast dest: equivD2) |
403 |
with w show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp |
|
404 |
qed |
|
405 |
qed |
|
406 |
ultimately |
|
407 |
show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
408 |
qed |
|
409 |
||
410 |
||
411 |
subsection "Winskel's Proof" |
|
412 |
||
413 |
declare rel_pow_0_E [elim!] |
|
414 |
||
415 |
text {* |
|
18372 | 416 |
Winskel's small step rules are a bit different \cite{Winskel}; |
12431 | 417 |
we introduce their equivalents as derived rules: |
418 |
*} |
|
419 |
lemma whileFalse1 [intro]: |
|
18372 | 420 |
"\<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 | 421 |
proof - |
422 |
assume "\<not>b s" |
|
423 |
have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" .. |
|
23373 | 424 |
also from `\<not>b s` have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" .. |
12431 | 425 |
also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" .. |
426 |
finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" .. |
|
427 |
qed |
|
428 |
||
429 |
lemma whileTrue1 [intro]: |
|
18372 | 430 |
"b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;\<WHILE> b \<DO> c, s\<rangle>" |
12431 | 431 |
(is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>") |
432 |
proof - |
|
433 |
assume "b s" |
|
434 |
have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" .. |
|
23373 | 435 |
also from `b s` have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c;?w, s\<rangle>" .. |
12431 | 436 |
finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>" .. |
437 |
qed |
|
1700 | 438 |
|
18372 | 439 |
inductive_cases evalc1_SEs: |
23746 | 440 |
"\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1 (co, s')" |
441 |
"\<langle>x:==a,s\<rangle> \<longrightarrow>\<^sub>1 (co, s')" |
|
442 |
"\<langle>c1;c2, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')" |
|
443 |
"\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')" |
|
444 |
"\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')" |
|
12431 | 445 |
|
23746 | 446 |
inductive_cases evalc1_E: "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')" |
12431 | 447 |
|
448 |
declare evalc1_SEs [elim!] |
|
449 |
||
450 |
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 | 451 |
apply (induct set: evalc) |
12431 | 452 |
|
18372 | 453 |
-- SKIP |
12431 | 454 |
apply blast |
455 |
||
18372 | 456 |
-- ASSIGN |
12431 | 457 |
apply fast |
458 |
||
18372 | 459 |
-- SEMI |
12431 | 460 |
apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI) |
461 |
||
18372 | 462 |
-- IF |
12566
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12546
diff
changeset
|
463 |
apply (fast intro: converse_rtrancl_into_rtrancl) |
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12546
diff
changeset
|
464 |
apply (fast intro: converse_rtrancl_into_rtrancl) |
12431 | 465 |
|
18372 | 466 |
-- WHILE |
34055 | 467 |
apply blast |
468 |
apply (blast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI) |
|
12431 | 469 |
|
470 |
done |
|
471 |
||
472 |
||
18372 | 473 |
lemma lemma2: |
474 |
"\<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 | 475 |
apply (induct n arbitrary: c d s u) |
12431 | 476 |
-- "case n = 0" |
477 |
apply fastsimp |
|
478 |
-- "induction step" |
|
18372 | 479 |
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
|
480 |
elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl) |
12431 | 481 |
done |
482 |
||
18372 | 483 |
lemma evalc1_impl_evalc: |
484 |
"\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" |
|
20503 | 485 |
apply (induct c arbitrary: s t) |
12431 | 486 |
apply (safe dest!: rtrancl_imp_UN_rel_pow) |
487 |
||
488 |
-- SKIP |
|
489 |
apply (simp add: SKIP_n) |
|
490 |
||
18372 | 491 |
-- ASSIGN |
12431 | 492 |
apply (fastsimp elim: rel_pow_E2) |
493 |
||
494 |
-- SEMI |
|
495 |
apply (fast dest!: rel_pow_imp_rtrancl lemma2) |
|
496 |
||
18372 | 497 |
-- IF |
12431 | 498 |
apply (erule rel_pow_E2) |
499 |
apply simp |
|
500 |
apply (fast dest!: rel_pow_imp_rtrancl) |
|
501 |
||
502 |
-- "WHILE, induction on the length of the computation" |
|
503 |
apply (rename_tac b c s t n) |
|
504 |
apply (erule_tac P = "?X -n\<rightarrow>\<^sub>1 ?Y" in rev_mp) |
|
505 |
apply (rule_tac x = "s" in spec) |
|
18372 | 506 |
apply (induct_tac n rule: nat_less_induct) |
12431 | 507 |
apply (intro strip) |
508 |
apply (erule rel_pow_E2) |
|
509 |
apply simp |
|
23746 | 510 |
apply (simp only: split_paired_all) |
12431 | 511 |
apply (erule evalc1_E) |
512 |
||
513 |
apply simp |
|
514 |
apply (case_tac "b x") |
|
515 |
-- WhileTrue |
|
516 |
apply (erule rel_pow_E2) |
|
517 |
apply simp |
|
518 |
apply (clarify dest!: lemma2) |
|
18372 | 519 |
apply atomize |
12431 | 520 |
apply (erule allE, erule allE, erule impE, assumption) |
521 |
apply (erule_tac x=mb in allE, erule impE, fastsimp) |
|
522 |
apply blast |
|
18372 | 523 |
-- WhileFalse |
12431 | 524 |
apply (erule rel_pow_E2) |
525 |
apply simp |
|
526 |
apply (simp add: SKIP_n) |
|
527 |
done |
|
528 |
||
529 |
||
530 |
text {* proof of the equivalence of evalc and evalc1 *} |
|
531 |
lemma evalc1_eq_evalc: "(\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle>) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)" |
|
18372 | 532 |
by (fast elim!: evalc1_impl_evalc evalc_impl_evalc1) |
12431 | 533 |
|
534 |
||
535 |
subsection "A proof without n" |
|
536 |
||
537 |
text {* |
|
538 |
The inductions are a bit awkward to write in this section, |
|
539 |
because @{text None} as result statement in the small step |
|
540 |
semantics doesn't have a direct counterpart in the big step |
|
18372 | 541 |
semantics. |
1700 | 542 |
|
12431 | 543 |
Winskel's small step rule set (using the @{text "\<SKIP>"} statement |
544 |
to indicate termination) is better suited for this proof. |
|
545 |
*} |
|
546 |
||
18372 | 547 |
lemma my_lemma1: |
548 |
assumes "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>" |
|
549 |
and "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" |
|
550 |
shows "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" |
|
12431 | 551 |
proof - |
552 |
-- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *} |
|
18372 | 553 |
from prems |
554 |
have "\<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" |
|
555 |
apply (induct rule: converse_rtrancl_induct2) |
|
12431 | 556 |
apply simp |
557 |
apply (rename_tac c s') |
|
558 |
apply simp |
|
559 |
apply (rule conjI) |
|
18372 | 560 |
apply fast |
12431 | 561 |
apply clarify |
562 |
apply (case_tac c) |
|
12566
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12546
diff
changeset
|
563 |
apply (auto intro: converse_rtrancl_into_rtrancl) |
12431 | 564 |
done |
18372 | 565 |
then show ?thesis by simp |
12431 | 566 |
qed |
567 |
||
13524 | 568 |
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 | 569 |
apply (induct set: evalc) |
12431 | 570 |
|
18372 | 571 |
-- SKIP |
12431 | 572 |
apply fast |
573 |
||
574 |
-- ASSIGN |
|
575 |
apply fast |
|
576 |
||
18372 | 577 |
-- SEMI |
12431 | 578 |
apply (fast intro: my_lemma1) |
579 |
||
580 |
-- IF |
|
12566
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12546
diff
changeset
|
581 |
apply (fast intro: converse_rtrancl_into_rtrancl) |
18372 | 582 |
apply (fast intro: converse_rtrancl_into_rtrancl) |
12431 | 583 |
|
18372 | 584 |
-- WHILE |
12431 | 585 |
apply fast |
12566
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12546
diff
changeset
|
586 |
apply (fast intro: converse_rtrancl_into_rtrancl my_lemma1) |
12431 | 587 |
|
588 |
done |
|
589 |
||
590 |
text {* |
|
591 |
The opposite direction is based on a Coq proof done by Ranan Fraer and |
|
592 |
Yves Bertot. The following sketch is from an email by Ranan Fraer. |
|
593 |
||
594 |
\begin{verbatim} |
|
595 |
First we've broke it into 2 lemmas: |
|
1700 | 596 |
|
12431 | 597 |
Lemma 1 |
598 |
((c,s) --> (SKIP,t)) => (<c,s> -c-> t) |
|
599 |
||
600 |
This is a quick one, dealing with the cases skip, assignment |
|
601 |
and while_false. |
|
602 |
||
603 |
Lemma 2 |
|
604 |
((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t |
|
18372 | 605 |
=> |
12431 | 606 |
<c,s> -c-> t |
607 |
||
608 |
This is proved by rule induction on the -*-> relation |
|
18372 | 609 |
and the induction step makes use of a third lemma: |
12431 | 610 |
|
611 |
Lemma 3 |
|
612 |
((c,s) --> (c',s')) /\ <c',s'> -c'-> t |
|
18372 | 613 |
=> |
12431 | 614 |
<c,s> -c-> t |
615 |
||
18372 | 616 |
This captures the essence of the proof, as it shows that <c',s'> |
12431 | 617 |
behaves as the continuation of <c,s> with respect to the natural |
618 |
semantics. |
|
619 |
The proof of Lemma 3 goes by rule induction on the --> relation, |
|
620 |
dealing with the cases sequence1, sequence2, if_true, if_false and |
|
621 |
while_true. In particular in the case (sequence1) we make use again |
|
622 |
of Lemma 1. |
|
623 |
\end{verbatim} |
|
624 |
*} |
|
625 |
||
626 |
inductive_cases evalc1_term_cases: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>" |
|
627 |
||
18372 | 628 |
lemma FB_lemma3: |
629 |
"(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow> |
|
630 |
\<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 | 631 |
by (induct arbitrary: t set: evalc1) |
18372 | 632 |
(auto elim!: evalc1_term_cases equivD2 [OF unfold_while]) |
12431 | 633 |
|
18372 | 634 |
lemma FB_lemma2: |
635 |
"(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow> |
|
636 |
\<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 | 637 |
apply (induct rule: converse_rtrancl_induct2, force) |
12434 | 638 |
apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3) |
12431 | 639 |
done |
640 |
||
13524 | 641 |
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 | 642 |
by (fastsimp dest: FB_lemma2) |
1700 | 643 |
|
644 |
end |