|
1 (* Title: Turing machines |
|
2 Author: Xu Jian <xujian817@hotmail.com> |
|
3 Maintainer: Xu Jian |
|
4 *) |
|
5 |
|
6 theory turing_basic |
|
7 imports Main |
|
8 begin |
|
9 |
|
10 section {* Basic definitions of Turing machine *} |
|
11 |
|
12 datatype action = W0 | W1 | L | R | Nop |
|
13 |
|
14 datatype cell = Bk | Oc |
|
15 |
|
16 type_synonym tape = "cell list \<times> cell list" |
|
17 |
|
18 type_synonym state = nat |
|
19 |
|
20 type_synonym instr = "action \<times> state" |
|
21 |
|
22 type_synonym tprog = "instr list \<times> nat" |
|
23 |
|
24 type_synonym config = "state \<times> tape" |
|
25 |
|
26 fun nth_of where |
|
27 "nth_of xs i = (if i \<ge> length xs then None |
|
28 else Some (xs ! i))" |
|
29 |
|
30 lemma nth_of_map [simp]: |
|
31 shows "nth_of (map f p) n = (case (nth_of p n) of None \<Rightarrow> None | Some x \<Rightarrow> Some (f x))" |
|
32 apply(induct p arbitrary: n) |
|
33 apply(auto) |
|
34 apply(case_tac n) |
|
35 apply(auto) |
|
36 done |
|
37 |
|
38 fun |
|
39 fetch :: "instr list \<Rightarrow> state \<Rightarrow> cell \<Rightarrow> instr" |
|
40 where |
|
41 "fetch p 0 b = (Nop, 0)" |
|
42 | "fetch p (Suc s) Bk = |
|
43 (case nth_of p (2 * s) of |
|
44 Some i \<Rightarrow> i |
|
45 | None \<Rightarrow> (Nop, 0))" |
|
46 |"fetch p (Suc s) Oc = |
|
47 (case nth_of p ((2 * s) + 1) of |
|
48 Some i \<Rightarrow> i |
|
49 | None \<Rightarrow> (Nop, 0))" |
|
50 |
|
51 lemma fetch_Nil [simp]: |
|
52 shows "fetch [] s b = (Nop, 0)" |
|
53 apply(case_tac s) |
|
54 apply(auto) |
|
55 apply(case_tac b) |
|
56 apply(auto) |
|
57 done |
|
58 |
|
59 fun |
|
60 update :: "action \<Rightarrow> tape \<Rightarrow> tape" |
|
61 where |
|
62 "update W0 (l, r) = (l, Bk # (tl r))" |
|
63 | "update W1 (l, r) = (l, Oc # (tl r))" |
|
64 | "update L (l, r) = (if l = [] then ([], Bk # r) else (tl l, (hd l) # r))" |
|
65 | "update R (l, r) = (if r = [] then (Bk # l, []) else ((hd r) # l, tl r))" |
|
66 | "update Nop (l, r) = (l, r)" |
|
67 |
|
68 abbreviation |
|
69 "read r == if (r = []) then Bk else hd r" |
|
70 |
|
71 fun step :: "config \<Rightarrow> tprog \<Rightarrow> config" |
|
72 where |
|
73 "step (s, l, r) (p, off) = |
|
74 (let (a, s') = fetch p (s - off) (read r) in (s', update a (l, r)))" |
|
75 |
|
76 fun steps :: "config \<Rightarrow> tprog \<Rightarrow> nat \<Rightarrow> config" |
|
77 where |
|
78 "steps c p 0 = c" | |
|
79 "steps c p (Suc n) = steps (step c p) p n" |
|
80 |
|
81 lemma step_red [simp]: |
|
82 shows "steps c p (Suc n) = step (steps c p n) p" |
|
83 by (induct n arbitrary: c) (auto) |
|
84 |
|
85 lemma steps_add [simp]: |
|
86 shows "steps c p (m + n) = steps (steps c p m) p n" |
|
87 by (induct m arbitrary: c) (auto) |
|
88 |
|
89 fun |
|
90 tm_wf :: "tprog \<Rightarrow> bool" |
|
91 where |
|
92 "tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and> |
|
93 (\<forall>(a, s) \<in> set p. s \<le> length p div 2 |
|
94 + off \<and> s \<ge> off))" |
|
95 |
|
96 (* FIXME: needed? *) |
|
97 lemma halt_lemma: |
|
98 "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" |
|
99 by (metis wf_iff_no_infinite_down_chain) |
|
100 |
|
101 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100) |
|
102 where "x \<up> n == replicate n x" |
|
103 |
|
104 consts tape_of :: "'a \<Rightarrow> cell list" ("<_>" 100) |
|
105 |
|
106 fun tape_of_nat_list :: "nat list \<Rightarrow> cell list" |
|
107 where |
|
108 "tape_of_nat_list [] = []" | |
|
109 "tape_of_nat_list [n] = Oc\<up>(Suc n)" | |
|
110 "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)" |
|
111 |
|
112 defs (overloaded) |
|
113 tape_of_nl_abv: "<am> \<equiv> tape_of_nat_list am" |
|
114 tape_of_nat_abv : "<(n::nat)> \<equiv> Oc\<up>(Suc n)" |
|
115 |
|
116 definition tinres :: "cell list \<Rightarrow> cell list \<Rightarrow> bool" |
|
117 where |
|
118 "tinres xs ys = (\<exists>n. xs = ys @ Bk \<up> n \<or> ys = xs @ Bk \<up> n)" |
|
119 |
|
120 fun |
|
121 shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list" |
|
122 where |
|
123 "shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)" |
|
124 |
|
125 |
|
126 lemma length_shift [simp]: |
|
127 "length (shift p n) = length p" |
|
128 by (simp) |
|
129 |
|
130 fun |
|
131 adjust :: "instr list \<Rightarrow> instr list" |
|
132 where |
|
133 "adjust p = map (\<lambda> (a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p" |
|
134 |
|
135 lemma length_adjust[simp]: |
|
136 shows "length (adjust p) = length p" |
|
137 by (induct p) (auto) |
|
138 |
|
139 fun |
|
140 tm_comp :: "instr list \<Rightarrow> instr list \<Rightarrow> instr list" ("_ |+| _" [0, 0] 100) |
|
141 where |
|
142 "tm_comp p1 p2 = ((adjust p1) @ (shift p2 ((length p1) div 2)))" |
|
143 |
|
144 fun |
|
145 is_final :: "config \<Rightarrow> bool" |
|
146 where |
|
147 "is_final (s, l, r) = (s = 0)" |
|
148 |
|
149 lemma is_final_steps: |
|
150 assumes "is_final (s, l, r)" |
|
151 shows "is_final (steps (s, l, r) (p, off) n)" |
|
152 using assms by (induct n) (auto) |
|
153 |
|
154 fun |
|
155 holds_for :: "(tape \<Rightarrow> bool) \<Rightarrow> config \<Rightarrow> bool" ("_ holds'_for _" [100, 99] 100) |
|
156 where |
|
157 "P holds_for (s, l, r) = P (l, r)" |
|
158 |
|
159 (* |
|
160 lemma step_0 [simp]: |
|
161 shows "step (0, (l, r)) p = (0, (l, r))" |
|
162 by simp |
|
163 |
|
164 lemma steps_0 [simp]: |
|
165 shows "steps (0, (l, r)) p n = (0, (l, r))" |
|
166 by (induct n) (simp_all) |
|
167 *) |
|
168 |
|
169 lemma is_final_holds[simp]: |
|
170 assumes "is_final c" |
|
171 shows "Q holds_for (steps c (p, off) n) = Q holds_for c" |
|
172 using assms |
|
173 apply(induct n) |
|
174 apply(case_tac [!] c) |
|
175 apply(auto) |
|
176 done |
|
177 |
|
178 type_synonym assert = "tape \<Rightarrow> bool" |
|
179 |
|
180 definition assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100) |
|
181 where |
|
182 "assert_imp P Q = (\<forall>l r. P (l, r) \<longrightarrow> Q (l, r))" |
|
183 |
|
184 lemma holds_for_imp: |
|
185 assumes "P holds_for c" |
|
186 and "P \<mapsto> Q" |
|
187 shows "Q holds_for c" |
|
188 using assms unfolding assert_imp_def by (case_tac c, auto) |
|
189 |
|
190 lemma test: |
|
191 assumes "is_final (steps (1, (l, r)) p n1)" |
|
192 and "is_final (steps (1, (l, r)) p n2)" |
|
193 shows "Q holds_for (steps (1, (l, r)) p n1) \<longleftrightarrow> Q holds_for (steps (1, (l, r)) p n2)" |
|
194 proof - |
|
195 obtain n3 where "n1 = n2 + n3 \<or> n2 = n1 + n3" |
|
196 by (metis le_iff_add nat_le_linear) |
|
197 with assms show "Q holds_for (steps (1, (l, r)) p n1) \<longleftrightarrow> Q holds_for (steps (1, (l, r)) p n2)" |
|
198 by(case_tac p) (auto) |
|
199 qed |
|
200 |
|
201 definition |
|
202 Hoare :: "assert \<Rightarrow> tprog \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50) |
|
203 where |
|
204 "{P} p {Q} \<equiv> |
|
205 (\<forall>l r. P (l, r) \<longrightarrow> (\<exists>n. is_final (steps (1, (l, r)) p n) \<and> Q holds_for (steps (1, (l, r)) p n)))" |
|
206 |
|
207 lemma HoareI: |
|
208 assumes "\<And>l r. P (l, r) \<Longrightarrow> \<exists>n. is_final (steps (1, (l, r)) p n) \<and> Q holds_for (steps (1, (l, r)) p n)" |
|
209 shows "{P} p {Q}" |
|
210 unfolding Hoare_def using assms by auto |
|
211 |
|
212 text {* |
|
213 {P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2 |
|
214 ----------------------------------- |
|
215 {P1} A |+| B {Q2} |
|
216 *} |
|
217 |
|
218 lemma step_0 [simp]: |
|
219 shows "step (0, (l, r)) p = (0, (l, r))" |
|
220 by (case_tac p, simp) |
|
221 |
|
222 lemma steps_0 [simp]: |
|
223 shows "steps (0, (l, r)) p n = (0, (l, r))" |
|
224 by (induct n) (simp_all) |
|
225 |
|
226 declare steps.simps[simp del] |
|
227 |
|
228 lemma before_final: |
|
229 assumes "steps (1, tp) A n = (0, tp')" |
|
230 obtains n' where "\<not> is_final (steps (1, tp) A n')" |
|
231 and "steps (1, tp) A (Suc n') = (0, tp')" |
|
232 proof - |
|
233 from assms have "\<exists> n'. \<not> is_final (steps (1, tp) A n') \<and> |
|
234 steps (1, tp) A (Suc n') = (0, tp')" |
|
235 proof(induct n arbitrary: tp', simp add: steps.simps) |
|
236 fix n tp' |
|
237 assume ind: |
|
238 "\<And>tp'. steps (1, tp) A n = (0, tp') \<Longrightarrow> |
|
239 \<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" |
|
240 and h: " steps (1, tp) A (Suc n) = (0, tp')" |
|
241 from h show "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" |
|
242 proof(simp add: step_red del: steps.simps, |
|
243 case_tac "(steps (Suc 0, tp) A n)", case_tac "a = 0", simp) |
|
244 fix a b c |
|
245 assume " steps (Suc 0, tp) A n = (0, tp')" |
|
246 hence "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" |
|
247 apply(rule_tac ind, simp) |
|
248 done |
|
249 thus "\<exists>n'. \<not> is_final (steps (Suc 0, tp) A n') \<and> step (steps (Suc 0, tp) A n') A = (0, tp')" |
|
250 apply(simp) |
|
251 done |
|
252 next |
|
253 fix a b c |
|
254 assume "steps (Suc 0, tp) A n = (a, b, c)" |
|
255 "step (steps (Suc 0, tp) A n) A = (0, tp')" |
|
256 "a \<noteq> 0" |
|
257 thus "\<exists>n'. \<not> is_final (steps (Suc 0, tp) A n') \<and> |
|
258 step (steps (Suc 0, tp) A n') A = (0, tp')" |
|
259 apply(rule_tac x = n in exI, simp) |
|
260 done |
|
261 qed |
|
262 qed |
|
263 thus "(\<And>n'. \<lbrakk>\<not> is_final (steps (1, tp) A n'); |
|
264 steps (1, tp) A (Suc n') = (0, tp')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis" |
|
265 by auto |
|
266 qed |
|
267 |
|
268 declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] |
|
269 |
|
270 lemma length_comp: |
|
271 "length (A |+| B) = length A + length B" |
|
272 apply(auto simp: tm_comp.simps) |
|
273 done |
|
274 |
|
275 lemma tmcomp_fetch_in_first: |
|
276 assumes "case (fetch A a x) of (ac, ns) \<Rightarrow> ns \<noteq> 0" |
|
277 shows "fetch (A |+| B) a x = fetch A a x" |
|
278 using assms |
|
279 apply(case_tac a, case_tac [!] x, |
|
280 auto simp: length_comp tm_comp.simps length_adjust nth_append) |
|
281 apply(simp_all add: adjust.simps) |
|
282 done |
|
283 |
|
284 |
|
285 lemma is_final_eq: "is_final (ba, tp) = (ba = 0)" |
|
286 apply(case_tac tp, simp add: is_final.simps) |
|
287 done |
|
288 |
|
289 lemma t_merge_pre_eq_step: |
|
290 assumes step: "step (a, b, c) (A, 0) = cf" |
|
291 and tm_wf: "tm_wf (A, 0)" |
|
292 and unfinal: "\<not> is_final cf" |
|
293 shows "step (a, b, c) (A |+| B, 0) = cf" |
|
294 proof - |
|
295 have "fetch (A |+| B) a (read c) = fetch A a (read c)" |
|
296 proof(rule_tac tmcomp_fetch_in_first) |
|
297 from step and unfinal show "case fetch A a (read c) of (ac, ns) \<Rightarrow> ns \<noteq> 0" |
|
298 apply(auto simp: is_final.simps) |
|
299 apply(case_tac "fetch A a (read c)", simp_all add: is_final_eq) |
|
300 done |
|
301 qed |
|
302 thus "?thesis" |
|
303 using step |
|
304 apply(auto simp: step.simps is_final.simps) |
|
305 done |
|
306 qed |
|
307 |
|
308 declare tm_wf.simps[simp del] step.simps[simp del] |
|
309 |
|
310 lemma t_merge_pre_eq: |
|
311 "\<lbrakk>steps (Suc 0, tp) (A, 0) stp = cf; \<not> is_final cf; tm_wf (A, 0)\<rbrakk> |
|
312 \<Longrightarrow> steps (Suc 0, tp) (A |+| B, 0) stp = cf" |
|
313 proof(induct stp arbitrary: cf, simp add: steps.simps) |
|
314 fix stp cf |
|
315 assume ind: "\<And>cf. \<lbrakk>steps (Suc 0, tp) (A, 0) stp = cf; \<not> is_final cf; tm_wf (A, 0)\<rbrakk> |
|
316 \<Longrightarrow> steps (Suc 0, tp) (A |+| B, 0) stp = cf" |
|
317 and h: "steps (Suc 0, tp) (A, 0) (Suc stp) = cf" |
|
318 "\<not> is_final cf" "tm_wf (A, 0)" |
|
319 from h show "steps (Suc 0, tp) (A |+| B, 0) (Suc stp) = cf" |
|
320 proof(simp add: step_red, case_tac "(steps (Suc 0, tp) (A, 0) stp)", simp) |
|
321 fix a b c |
|
322 assume g: "steps (Suc 0, tp) (A, 0) stp = (a, b, c)" |
|
323 "step (a, b, c) (A, 0) = cf" |
|
324 have "(steps (Suc 0, tp) (A |+| B, 0) stp) = (a, b, c)" |
|
325 proof(rule ind, simp_all add: h g) |
|
326 show "0 < a" |
|
327 using g h |
|
328 apply(simp add: step_red) |
|
329 apply(case_tac a, auto simp: step_0) |
|
330 apply(case_tac "steps (Suc 0, tp) (A, 0) stp", simp) |
|
331 done |
|
332 qed |
|
333 thus "step (steps (Suc 0, tp) (A |+| B, 0) stp) (A |+| B, 0) = cf" |
|
334 apply(simp) |
|
335 apply(rule_tac t_merge_pre_eq_step, simp_all add: g h) |
|
336 done |
|
337 qed |
|
338 qed |
|
339 |
|
340 lemma tmcomp_fetch_in_first2: |
|
341 assumes "fetch A a x = (ac, 0)" |
|
342 "tm_wf (A, 0)" |
|
343 "a \<le> length A div 2" "a > 0" |
|
344 shows "fetch (A |+| B) a x = (ac, Suc (length A div 2))" |
|
345 using assms |
|
346 apply(case_tac a, case_tac [!] x, |
|
347 auto simp: length_comp tm_comp.simps length_adjust nth_append) |
|
348 apply(simp_all add: adjust.simps) |
|
349 done |
|
350 |
|
351 lemma tmcomp_exec_after_first: |
|
352 "\<lbrakk>0 < a; step (a, b, c) (A, 0) = (0, tp'); tm_wf (A, 0); |
|
353 a \<le> length A div 2\<rbrakk> |
|
354 \<Longrightarrow> step (a, b, c) (A |+| B, 0) = (Suc (length A div 2), tp')" |
|
355 apply(simp add: step.simps, auto) |
|
356 apply(case_tac "fetch A a Bk", simp add: tmcomp_fetch_in_first2) |
|
357 apply(case_tac "fetch A a (hd c)", simp add: tmcomp_fetch_in_first2) |
|
358 done |
|
359 |
|
360 lemma step_nothalt_pre: "\<lbrakk>step (aa, ba, ca) (A, 0) = (a, b, c); 0 < a\<rbrakk> \<Longrightarrow> 0 < aa" |
|
361 apply(case_tac "aa = 0", simp add: step_0, simp) |
|
362 done |
|
363 |
|
364 lemma nth_in_set: |
|
365 "\<lbrakk> A ! i = x; i < length A\<rbrakk> \<Longrightarrow> x \<in> set A" |
|
366 by auto |
|
367 |
|
368 lemma step_nothalt: |
|
369 "\<lbrakk>step (aa, ba, ca) (A, 0) = (a, b, c); 0 < a; tm_wf (A, 0)\<rbrakk> \<Longrightarrow> |
|
370 a \<le> length A div 2" |
|
371 apply(simp add: step.simps) |
|
372 apply(case_tac aa, case_tac [!] aa, auto split: if_splits simp: tm_wf.simps) |
|
373 apply(case_tac "A ! (2 * nat)", simp) |
|
374 apply(erule_tac x = "(aa, a)" in ballE, simp_all add: nth_in_set) |
|
375 apply(case_tac "hd ca", auto split: if_splits simp: tm_wf.simps) |
|
376 apply(case_tac "A ! (2 * nat)", simp) |
|
377 apply(erule_tac x = "(aa, a)" in ballE, simp_all add: nth_in_set) |
|
378 apply(case_tac "A ! (Suc (2 * nat))") |
|
379 apply(erule_tac x = "(aa,bb)" in ballE, simp_all add: nth_in_set) |
|
380 done |
|
381 |
|
382 lemma steps_in_range: |
|
383 " \<lbrakk>0 < a; steps (Suc 0, tp) (A, 0) stp = (a, b, c); tm_wf (A, 0)\<rbrakk> |
|
384 \<Longrightarrow> a \<le> length A div 2" |
|
385 proof(induct stp arbitrary: a b c) |
|
386 fix a b c |
|
387 assume h: "0 < a" "steps (Suc 0, tp) (A, 0) 0 = (a, b, c)" |
|
388 "tm_wf (A, 0)" |
|
389 thus "a \<le> length A div 2" |
|
390 apply(simp add: steps.simps tm_wf.simps, auto) |
|
391 done |
|
392 next |
|
393 fix stp a b c |
|
394 assume ind: "\<And>a b c. \<lbrakk>0 < a; steps (Suc 0, tp) (A, 0) stp = (a, b, c); |
|
395 tm_wf (A, 0)\<rbrakk> \<Longrightarrow> a \<le> length A div 2" |
|
396 and h: "0 < a" "steps (Suc 0, tp) (A, 0) (Suc stp) = (a, b, c)" "tm_wf (A, 0)" |
|
397 from h show "a \<le> length A div 2" |
|
398 proof(simp add: step_red, case_tac "(steps (Suc 0, tp) (A, 0) stp)", simp) |
|
399 fix aa ba ca |
|
400 assume g: "step (aa, ba, ca) (A, 0) = (a, b, c)" |
|
401 "steps (Suc 0, tp) (A, 0) stp = (aa, ba, ca)" |
|
402 hence "aa \<le> length A div 2" |
|
403 apply(rule_tac ind, auto simp: h step_nothalt_pre) |
|
404 done |
|
405 thus "?thesis" |
|
406 using g h |
|
407 apply(rule_tac step_nothalt, auto) |
|
408 done |
|
409 qed |
|
410 qed |
|
411 |
|
412 lemma t_merge_pre_halt_same: |
|
413 assumes a_ht: "steps (1, tp) (A, 0) n = (0, tp')" |
|
414 and a_wf: "tm_wf (A, 0)" |
|
415 obtains n' where "steps (1, tp) (A |+| B, 0) n' = (Suc (length A div 2), tp')" |
|
416 proof - |
|
417 assume a: "\<And>n. steps (1, tp) (A |+| B, 0) n = (Suc (length A div 2), tp') \<Longrightarrow> thesis" |
|
418 obtain stp' where "\<not> is_final (steps (1, tp) (A, 0) stp')" and |
|
419 "steps (1, tp) (A, 0) (Suc stp') = (0, tp')" |
|
420 using a_ht before_final by blast |
|
421 then have "steps (1, tp) (A |+| B, 0) (Suc stp') = (Suc (length A div 2), tp')" |
|
422 proof(simp add: step_red) |
|
423 assume "\<not> is_final (steps (Suc 0, tp) (A, 0) stp')" |
|
424 " step (steps (Suc 0, tp) (A, 0) stp') (A, 0) = (0, tp')" |
|
425 moreover hence "(steps (Suc 0, tp) (A |+| B, 0) stp') = (steps (Suc 0, tp) (A, 0) stp')" |
|
426 apply(rule_tac t_merge_pre_eq) |
|
427 apply(simp_all add: a_wf a_ht) |
|
428 done |
|
429 ultimately show "step (steps (Suc 0, tp) (A |+| B, 0) stp') (A |+| B, 0) = (Suc (length A div 2), tp')" |
|
430 apply(case_tac " steps (Suc 0, tp) (A, 0) stp'", simp) |
|
431 apply(rule tmcomp_exec_after_first, simp_all add: a_wf) |
|
432 apply(erule_tac steps_in_range, auto simp: a_wf) |
|
433 done |
|
434 qed |
|
435 with a show thesis by blast |
|
436 qed |
|
437 |
|
438 lemma tm_comp_fetch_second_zero: |
|
439 "\<lbrakk>fetch B sa' x = (a, 0); tm_wf (A, 0); tm_wf (B, 0); sa' > 0\<rbrakk> |
|
440 \<Longrightarrow> fetch (A |+| B) (sa' + (length A div 2)) x = (a, 0)" |
|
441 apply(case_tac x) |
|
442 apply(case_tac [!] sa', |
|
443 auto simp: fetch.simps length_comp length_adjust nth_append tm_comp.simps |
|
444 tm_wf.simps shift.simps split: if_splits) |
|
445 done |
|
446 |
|
447 lemma tm_comp_fetch_second_inst: |
|
448 "\<lbrakk>sa > 0; s > 0; tm_wf (A, 0); tm_wf (B, 0); fetch B sa x = (a, s)\<rbrakk> |
|
449 \<Longrightarrow> fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)" |
|
450 apply(case_tac x) |
|
451 apply(case_tac [!] sa, |
|
452 auto simp: fetch.simps length_comp length_adjust nth_append tm_comp.simps |
|
453 tm_wf.simps shift.simps split: if_splits) |
|
454 done |
|
455 |
|
456 lemma t_merge_second_same: |
|
457 assumes a_wf: "tm_wf (A, 0)" |
|
458 and b_wf: "tm_wf (B, 0)" |
|
459 and steps: "steps (Suc 0, l, r) (B, 0) stp = (s, l', r')" |
|
460 shows "steps (Suc (length A div 2), l, r) (A |+| B, 0) stp |
|
461 = (if s = 0 then 0 |
|
462 else s + length A div 2, l', r')" |
|
463 using a_wf b_wf steps |
|
464 proof(induct stp arbitrary: s l' r', simp add: steps.simps, simp) |
|
465 fix stpa sa l'a r'a |
|
466 assume ind: "\<And>s l' r'. steps (Suc 0, l, r) (B, 0) stpa = (s, l', r') \<Longrightarrow> |
|
467 steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa = |
|
468 (if s = 0 then 0 else s + length A div 2, l', r')" |
|
469 and h: "step (steps (Suc 0, l, r) (B, 0) stpa) (B, 0) = (sa, l'a, r'a)" |
|
470 obtain sa' l'' r'' where a: "(steps (Suc 0, l, r) (B, 0) stpa) = (sa', l'', r'')" |
|
471 apply(case_tac "steps (Suc 0, l, r) (B, 0) stpa", auto) |
|
472 done |
|
473 from this have b: "steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa = |
|
474 (if sa' = 0 then 0 else sa' + length A div 2, l'', r'')" |
|
475 apply(erule_tac ind) |
|
476 done |
|
477 from a b h show |
|
478 "(sa = 0 \<longrightarrow> step (steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa) (A |+| B, 0) = (0, l'a, r'a)) \<and> |
|
479 (0 < sa \<longrightarrow> step (steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa) (A |+| B, 0) = (sa + length A div 2, l'a, r'a))" |
|
480 proof(case_tac "sa' = 0", auto) |
|
481 assume "step (sa', l'', r'') (B, 0) = (0, l'a, r'a)" "0 < sa'" |
|
482 thus "step (sa' + length A div 2, l'', r'') (A |+| B, 0) = (0, l'a, r'a)" |
|
483 using a_wf b_wf |
|
484 apply(simp add: step.simps) |
|
485 apply(case_tac "fetch B sa' (read r'')", auto) |
|
486 apply(simp_all add: step.simps tm_comp_fetch_second_zero) |
|
487 done |
|
488 next |
|
489 assume "step (sa', l'', r'') (B, 0) = (sa, l'a, r'a)" "0 < sa'" "0 < sa" |
|
490 thus "step (sa' + length A div 2, l'', r'') (A |+| B, 0) = (sa + length A div 2, l'a, r'a)" |
|
491 using a_wf b_wf |
|
492 apply(simp add: step.simps) |
|
493 apply(case_tac "fetch B sa' (read r'')", auto) |
|
494 apply(simp_all add: step.simps tm_comp_fetch_second_inst) |
|
495 done |
|
496 qed |
|
497 qed |
|
498 |
|
499 lemma t_merge_second_halt_same: |
|
500 "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0); |
|
501 steps (1, l, r) (B, 0) stp = (0, l', r')\<rbrakk> |
|
502 \<Longrightarrow> steps (Suc (length A div 2), l, r) (A |+| B, 0) stp |
|
503 = (0, l', r')" |
|
504 using t_merge_second_same[where s = "0"] |
|
505 apply(auto) |
|
506 done |
|
507 |
|
508 lemma Hoare_plus_halt: |
|
509 assumes aimpb: "Q1 \<mapsto> P2" |
|
510 and A_wf : "tm_wf (A, 0)" |
|
511 and B_wf : "tm_wf (B, 0)" |
|
512 and A_halt : "{P1} (A, 0) {Q1}" |
|
513 and B_halt : "{P2} (B, 0) {Q2}" |
|
514 shows "{P1} (A |+| B, 0) {Q2}" |
|
515 proof(rule HoareI) |
|
516 fix l r |
|
517 assume h: "P1 (l, r)" |
|
518 then obtain n1 where a: "is_final (steps (1, l, r) (A, 0) n1)" and b: "Q1 holds_for (steps (1, l, r) (A, 0) n1)" |
|
519 using A_halt unfolding Hoare_def by auto |
|
520 then obtain l' r' where "steps (1, l, r) (A, 0) n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" |
|
521 by(case_tac "steps (1, l, r) (A, 0) n1", auto) |
|
522 then obtain stpa where d: "steps (1, l, r) (A |+| B, 0) stpa = (Suc (length A div 2), l', r')" |
|
523 using A_wf |
|
524 by(rule_tac t_merge_pre_halt_same, auto) |
|
525 from c aimpb have "P2 holds_for (0, l', r')" |
|
526 by(rule holds_for_imp) |
|
527 from this have "P2 (l', r')" by auto |
|
528 from this obtain n2 where e: "is_final (steps (1, l', r') (B, 0) n2)" and f: "Q2 holds_for (steps (1, l', r') (B, 0) n2)" |
|
529 using B_halt unfolding Hoare_def |
|
530 by auto |
|
531 then obtain l'' r'' where "steps (1, l', r') (B, 0) n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')" |
|
532 by(case_tac "steps (1, l', r') (B, 0) n2", auto) |
|
533 from this have "steps (Suc (length A div 2), l', r') (A |+| B, 0) n2 |
|
534 = (0, l'', r'')" |
|
535 apply(rule_tac t_merge_second_halt_same, auto simp: A_wf B_wf) |
|
536 done |
|
537 thus "\<exists>n. is_final (steps (1, l, r) (A |+| B, 0) n) \<and> Q2 holds_for (steps (1, l, r) (A |+| B, 0) n)" |
|
538 using d g |
|
539 apply(rule_tac x = "stpa + n2" in exI) |
|
540 apply(simp add: steps_add) |
|
541 done |
|
542 qed |
|
543 |
|
544 definition |
|
545 Hoare_unhalt :: "assert \<Rightarrow> tprog \<Rightarrow> bool" ("({(1_)}/ (_))" 50) |
|
546 where |
|
547 "{P} p \<equiv> |
|
548 (\<forall>l r. P (l, r) \<longrightarrow> (\<forall> n . \<not> (is_final (steps (1, (l, r)) p n))))" |
|
549 |
|
550 lemma Hoare_unhalt_I: |
|
551 assumes "\<And>l r. P (l, r) \<Longrightarrow> \<forall> n. \<not> is_final (steps (1, (l, r)) p n)" |
|
552 shows "{P} p" |
|
553 unfolding Hoare_unhalt_def using assms by auto |
|
554 |
|
555 lemma Hoare_plus_unhalt: |
|
556 assumes aimpb: "Q1 \<mapsto> P2" |
|
557 and A_wf : "tm_wf (A, 0)" |
|
558 and B_wf : "tm_wf (B, 0)" |
|
559 and A_halt : "{P1} (A, 0) {Q1}" |
|
560 and B_uhalt : "{P2} (B, 0)" |
|
561 shows "{P1} (A |+| B, 0)" |
|
562 proof(rule_tac Hoare_unhalt_I) |
|
563 fix l r |
|
564 assume h: "P1 (l, r)" |
|
565 then obtain n1 where a: "is_final (steps (1, l, r) (A, 0) n1)" and b: "Q1 holds_for (steps (1, l, r) (A, 0) n1)" |
|
566 using A_halt unfolding Hoare_def by auto |
|
567 then obtain l' r' where "steps (1, l, r) (A, 0) n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" |
|
568 by(case_tac "steps (1, l, r) (A, 0) n1", auto) |
|
569 then obtain stpa where d: "steps (1, l, r) (A |+| B, 0) stpa = (Suc (length A div 2), l', r')" |
|
570 using A_wf |
|
571 by(rule_tac t_merge_pre_halt_same, auto) |
|
572 from c aimpb have "P2 holds_for (0, l', r')" |
|
573 by(rule holds_for_imp) |
|
574 from this have "P2 (l', r')" by auto |
|
575 from this have e: "\<forall> n. \<not> is_final (steps (Suc 0, l', r') (B, 0) n) " |
|
576 using B_uhalt unfolding Hoare_unhalt_def |
|
577 by auto |
|
578 from e show "\<forall>n. \<not> is_final (steps (1, l, r) (A |+| B, 0) n)" |
|
579 proof(rule_tac allI, case_tac "n > stpa") |
|
580 fix n |
|
581 assume h2: "stpa < n" |
|
582 hence "\<not> is_final (steps (Suc 0, l', r') (B, 0) (n - stpa))" |
|
583 using e |
|
584 apply(erule_tac x = "n - stpa" in allE) by simp |
|
585 then obtain s'' l'' r'' where f: "steps (Suc 0, l', r') (B, 0) (n - stpa) = (s'', l'', r'')" and g: "s'' \<noteq> 0" |
|
586 apply(case_tac "steps (Suc 0, l', r') (B, 0) (n - stpa)", auto) |
|
587 done |
|
588 have k: "steps (Suc (length A div 2), l', r') (A |+| B, 0) (n - stpa) = (s''+ length A div 2, l'', r'') " |
|
589 using A_wf B_wf f g |
|
590 apply(drule_tac t_merge_second_same, auto) |
|
591 done |
|
592 show "\<not> is_final (steps (1, l, r) (A |+| B, 0) n)" |
|
593 proof - |
|
594 have "\<not> is_final (steps (1, l, r) (A |+| B, 0) (stpa + (n - stpa)))" |
|
595 using d k A_wf |
|
596 apply(simp only: steps_add d, simp add: tm_wf.simps) |
|
597 done |
|
598 thus "\<not> is_final (steps (1, l, r) (A |+| B, 0) n)" |
|
599 using h2 by simp |
|
600 qed |
|
601 next |
|
602 fix n |
|
603 assume h2: "\<not> stpa < n" |
|
604 with d show "\<not> is_final (steps (1, l, r) (A |+| B, 0) n)" |
|
605 apply(auto) |
|
606 apply(subgoal_tac "\<exists> d. stpa = n + d", auto) |
|
607 apply(case_tac "(steps (Suc 0, l, r) (A |+| B, 0) n)", simp) |
|
608 apply(rule_tac x = "stpa - n" in exI, simp) |
|
609 done |
|
610 qed |
|
611 qed |
|
612 |
|
613 end |
|
614 |