1 (* Title: HOL/IMP/Transition.thy |
|
2 Author: Tobias Nipkow & Robert Sandner, TUM |
|
3 Isar Version: Gerwin Klein, 2001 |
|
4 Copyright 1996 TUM |
|
5 *) |
|
6 |
|
7 header "Transition Semantics of Commands" |
|
8 |
|
9 theory Transition imports Natural begin |
|
10 |
|
11 subsection "The transition relation" |
|
12 |
|
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. |
|
17 |
|
18 Since configurations that have terminated are written without |
|
19 a statement, the transition relation is not |
|
20 @{typ "((com \<times> state) \<times> (com \<times> state)) set"} |
|
21 but instead: |
|
22 @{typ "((com option \<times> state) \<times> (com option \<times> state)) set"} |
|
23 |
|
24 Some syntactic sugar that we will use to hide the |
|
25 @{text option} part in configurations: |
|
26 *} |
|
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)" |
|
33 |
|
34 notation (xsymbols) |
|
35 angle ("\<langle>_,_\<rangle>") and |
|
36 angle2 ("\<langle>_\<rangle>") |
|
37 |
|
38 notation (HTML output) |
|
39 angle ("\<langle>_,_\<rangle>") and |
|
40 angle2 ("\<langle>_\<rangle>") |
|
41 |
|
42 text {* |
|
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 {* |
|
65 More syntactic sugar for the transition relation, and its |
|
66 iteration. |
|
67 *} |
|
68 abbreviation |
|
69 evalcn :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool" |
|
70 ("_ -_\<rightarrow>\<^sub>1 _" [60,60,60] 60) where |
|
71 "cs -n\<rightarrow>\<^sub>1 cs' == (cs,cs') \<in> evalc1^^n" |
|
72 |
|
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^*" |
|
77 |
|
78 (*<*) |
|
79 declare rel_pow_Suc_E2 [elim!] |
|
80 (*>*) |
|
81 |
|
82 text {* |
|
83 As for the big step semantics you can read these rules in a |
|
84 syntax directed way: |
|
85 *} |
|
86 lemma SKIP_1: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s\<rangle>)" |
|
87 by (induct y, rule, cases set: evalc1, auto) |
|
88 |
|
89 lemma Assign_1: "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s[x \<mapsto> a s]\<rangle>)" |
|
90 by (induct y, rule, cases set: evalc1, auto) |
|
91 |
|
92 lemma Cond_1: |
|
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>))" |
|
94 by (induct y, rule, cases set: evalc1, auto) |
|
95 |
|
96 lemma While_1: |
|
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>)" |
|
98 by (induct y, rule, cases set: evalc1, auto) |
|
99 |
|
100 lemmas [simp] = SKIP_1 Assign_1 Cond_1 While_1 |
|
101 |
|
102 |
|
103 subsection "Examples" |
|
104 |
|
105 lemma |
|
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>" |
|
107 (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* _") |
|
108 proof - |
|
109 let ?c = "x:== \<lambda>s. s x+1" |
|
110 let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>" |
|
111 assume [simp]: "s x = 0" |
|
112 have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" .. |
|
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 |
|
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 |
|
120 |
|
121 lemma |
|
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'" |
|
123 (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'") |
|
124 proof - |
|
125 let ?c = "x:== \<lambda>s. s x+1" |
|
126 let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>" |
|
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 |
|
131 also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 3]\<rangle>" by (rule Semi1) simp |
|
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 |
|
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 |
|
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 |
|
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 |
|
138 oops |
|
139 |
|
140 subsection "Basic properties" |
|
141 |
|
142 text {* |
|
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:" |
|
148 fix c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" |
|
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>" |
|
151 by (cases y, cases "fst y") auto |
|
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 *} |
|
163 lemma stuck [elim!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1 y \<Longrightarrow> P" |
|
164 by (induct y, auto elim: evalc1.cases) |
|
165 |
|
166 lemma evalc_None_retrancl [simp, dest!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = \<langle>s\<rangle>" |
|
167 by (induct set: rtrancl) auto |
|
168 |
|
169 (*<*) |
|
170 (* FIXME: relpow.simps don't work *) |
|
171 lemmas [simp del] = relpow.simps |
|
172 lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R ^^ 0 = Id" by (simp add: relpow.simps) |
|
173 lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R ^^ Suc 0 = R" by (simp add: relpow.simps) |
|
174 |
|
175 (*>*) |
|
176 lemma evalc1_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)" |
|
177 by (cases n) auto |
|
178 |
|
179 lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1" |
|
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: |
|
189 "\<langle>c1; c2, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> |
|
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" |
|
191 proof (induct n arbitrary: c1 c2 s s'') |
|
192 case 0 |
|
193 then show ?case by simp |
|
194 next |
|
195 case (Suc n) |
|
196 |
|
197 from `\<langle>c1; c2, s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>` |
|
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 |
|
202 |
|
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 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 |
|
210 thus ?thesis by blast |
|
211 next |
|
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 |
|
216 with Suc.hyps obtain i j s0 where |
|
217 c1': "\<langle>c1',s'''\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and |
|
218 c2: "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and |
|
219 i: "n = i+j" |
|
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 |
|
227 qed |
|
228 qed |
|
229 |
|
230 |
|
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>" |
|
233 proof (induct n arbitrary: c0 s s'') |
|
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 .. |
|
238 next |
|
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 |
|
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 |
|
247 "y = \<langle>s0'\<rangle> \<or> y = \<langle>c0', s0'\<rangle>" |
|
248 by (cases y, cases "fst y") auto |
|
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 *} |
|
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 assms |
|
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>" .. |
|
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'" |
|
330 then show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1) |
|
331 next |
|
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 |
|
335 have "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
336 proof (induct arbitrary: c s s' rule: less_induct) |
|
337 fix n |
|
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'" |
|
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 |
|
342 with c obtain y where |
|
343 c': "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1 y" and m: "y -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by blast |
|
344 show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" |
|
345 proof (cases c) |
|
346 case SKIP |
|
347 with c n show ?thesis by auto |
|
348 next |
|
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 |
|
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" |
|
357 by (blast dest: semiD) |
|
358 from c1 c2 obtain |
|
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 |
|
362 from IH i c1 |
|
363 have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" . |
|
364 moreover |
|
365 from IH j c2 |
|
366 have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" . |
|
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 |
|
375 have "\<langle>c1,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto |
|
376 with n IH |
|
377 have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
378 with If True |
|
379 have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
380 } |
|
381 moreover |
|
382 { assume False: "b s = False" |
|
383 with If c n |
|
384 have "\<langle>c2,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto |
|
385 with n IH |
|
386 have "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
387 with If False |
|
388 have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast |
|
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'" |
|
394 with c n |
|
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']} *} |
|
401 ultimately |
|
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 {* |
|
416 Winskel's small step rules are a bit different \cite{Winskel}; |
|
417 we introduce their equivalents as derived rules: |
|
418 *} |
|
419 lemma whileFalse1 [intro]: |
|
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>") |
|
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>" .. |
|
424 also from `\<not>b s` have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" .. |
|
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]: |
|
430 "b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;\<WHILE> b \<DO> c, s\<rangle>" |
|
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>" .. |
|
435 also from `b s` have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c;?w, s\<rangle>" .. |
|
436 finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>" .. |
|
437 qed |
|
438 |
|
439 inductive_cases evalc1_SEs: |
|
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')" |
|
445 |
|
446 inductive_cases evalc1_E: "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')" |
|
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>" |
|
451 apply (induct set: evalc) |
|
452 |
|
453 -- SKIP |
|
454 apply blast |
|
455 |
|
456 -- ASSIGN |
|
457 apply fast |
|
458 |
|
459 -- SEMI |
|
460 apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI) |
|
461 |
|
462 -- IF |
|
463 apply (fast intro: converse_rtrancl_into_rtrancl) |
|
464 apply (fast intro: converse_rtrancl_into_rtrancl) |
|
465 |
|
466 -- WHILE |
|
467 apply blast |
|
468 apply (blast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI) |
|
469 |
|
470 done |
|
471 |
|
472 |
|
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" |
|
475 apply (induct n arbitrary: c d s u) |
|
476 -- "case n = 0" |
|
477 apply fastsimp |
|
478 -- "induction step" |
|
479 apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2 |
|
480 elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl) |
|
481 done |
|
482 |
|
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" |
|
485 apply (induct c arbitrary: s t) |
|
486 apply (safe dest!: rtrancl_imp_UN_rel_pow) |
|
487 |
|
488 -- SKIP |
|
489 apply (simp add: SKIP_n) |
|
490 |
|
491 -- ASSIGN |
|
492 apply (fastsimp elim: rel_pow_E2) |
|
493 |
|
494 -- SEMI |
|
495 apply (fast dest!: rel_pow_imp_rtrancl lemma2) |
|
496 |
|
497 -- IF |
|
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) |
|
506 apply (induct_tac n rule: nat_less_induct) |
|
507 apply (intro strip) |
|
508 apply (erule rel_pow_E2) |
|
509 apply simp |
|
510 apply (simp only: split_paired_all) |
|
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) |
|
519 apply atomize |
|
520 apply (erule allE, erule allE, erule impE, assumption) |
|
521 apply (erule_tac x=mb in allE, erule impE, fastsimp) |
|
522 apply blast |
|
523 -- WhileFalse |
|
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)" |
|
532 by (fast elim!: evalc1_impl_evalc evalc_impl_evalc1) |
|
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 |
|
541 semantics. |
|
542 |
|
543 Winskel's small step rule set (using the @{text "\<SKIP>"} statement |
|
544 to indicate termination) is better suited for this proof. |
|
545 *} |
|
546 |
|
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" |
|
551 proof - |
|
552 -- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *} |
|
553 from assms |
|
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) |
|
556 apply simp |
|
557 apply (rename_tac c s') |
|
558 apply simp |
|
559 apply (rule conjI) |
|
560 apply fast |
|
561 apply clarify |
|
562 apply (case_tac c) |
|
563 apply (auto intro: converse_rtrancl_into_rtrancl) |
|
564 done |
|
565 then show ?thesis by simp |
|
566 qed |
|
567 |
|
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>" |
|
569 apply (induct set: evalc) |
|
570 |
|
571 -- SKIP |
|
572 apply fast |
|
573 |
|
574 -- ASSIGN |
|
575 apply fast |
|
576 |
|
577 -- SEMI |
|
578 apply (fast intro: my_lemma1) |
|
579 |
|
580 -- IF |
|
581 apply (fast intro: converse_rtrancl_into_rtrancl) |
|
582 apply (fast intro: converse_rtrancl_into_rtrancl) |
|
583 |
|
584 -- WHILE |
|
585 apply fast |
|
586 apply (fast intro: converse_rtrancl_into_rtrancl my_lemma1) |
|
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: |
|
596 |
|
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 |
|
605 => |
|
606 <c,s> -c-> t |
|
607 |
|
608 This is proved by rule induction on the -*-> relation |
|
609 and the induction step makes use of a third lemma: |
|
610 |
|
611 Lemma 3 |
|
612 ((c,s) --> (c',s')) /\ <c',s'> -c'-> t |
|
613 => |
|
614 <c,s> -c-> t |
|
615 |
|
616 This captures the essence of the proof, as it shows that <c',s'> |
|
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 |
|
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" |
|
631 by (induct arbitrary: t set: evalc1) |
|
632 (auto elim!: evalc1_term_cases equivD2 [OF unfold_while]) |
|
633 |
|
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" |
|
637 apply (induct rule: converse_rtrancl_induct2, force) |
|
638 apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3) |
|
639 done |
|
640 |
|
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" |
|
642 by (fastsimp dest: FB_lemma2) |
|
643 |
|
644 end |
|