4468 apply(auto) |
4468 apply(auto) |
4469 apply(simp add: dropWhile_exp1 takeWhile_exp1) |
4469 apply(simp add: dropWhile_exp1 takeWhile_exp1) |
4470 done |
4470 done |
4471 |
4471 |
4472 declare numeral_2_eq_2[simp del] |
4472 declare numeral_2_eq_2[simp del] |
|
4473 |
|
4474 lemma [simp]: "wadjust_start m rs (c, Bk # list) |
|
4475 \<Longrightarrow> wadjust_start m rs (c, Oc # list)" |
|
4476 apply(auto simp: wadjust_start.simps) |
|
4477 done |
|
4478 |
|
4479 lemma [simp]: "wadjust_backto_standard_pos m rs (c, Bk # list) |
|
4480 \<Longrightarrow> wadjust_stop m rs (Bk # c, list)" |
|
4481 apply(auto simp: wadjust_backto_standard_pos.simps |
|
4482 wadjust_stop.simps wadjust_backto_standard_pos_B.simps) |
|
4483 done |
|
4484 |
|
4485 lemma [simp]: "wadjust_start m rs (c, Oc # list) |
|
4486 \<Longrightarrow> wadjust_loop_start m rs (Oc # c, list)" |
|
4487 apply(auto simp: wadjust_start.simps wadjust_loop_start.simps) |
|
4488 apply(rule_tac x = ln in exI, simp) |
|
4489 apply(rule_tac x = "rn" in exI, simp) |
|
4490 apply(rule_tac x = 1 in exI, simp) |
|
4491 done |
|
4492 |
|
4493 lemma [simp]:" wadjust_erase2 m rs (c, Oc # list) |
|
4494 \<Longrightarrow> wadjust_erase2 m rs (c, Bk # list)" |
|
4495 apply(auto simp: wadjust_erase2.simps) |
|
4496 done |
4473 |
4497 |
4474 lemma wadjust_correctness: |
4498 lemma wadjust_correctness: |
4475 shows "let P = (\<lambda> (len, st, l, r). st = 0) in |
4499 shows "let P = (\<lambda> (len, st, l, r). st = 0) in |
4476 let Q = (\<lambda> (len, st, l, r). wadjust_inv st m rs (l, r)) in |
4500 let Q = (\<lambda> (len, st, l, r). wadjust_inv st m rs (l, r)) in |
4477 let f = (\<lambda> stp. (Suc (Suc rs), steps0 (Suc 0, Bk # Oc\<up>(Suc m), |
4501 let f = (\<lambda> stp. (Suc (Suc rs), steps0 (Suc 0, Bk # Oc\<up>(Suc m), |
4489 show "\<forall> n. \<not> ?P (?f n) \<and> ?Q (?f n) \<longrightarrow> |
4513 show "\<forall> n. \<not> ?P (?f n) \<and> ?Q (?f n) \<longrightarrow> |
4490 ?Q (?f (Suc n)) \<and> (?f (Suc n), ?f n) \<in> wadjust_le" |
4514 ?Q (?f (Suc n)) \<and> (?f (Suc n), ?f n) \<in> wadjust_le" |
4491 apply(rule_tac allI, rule_tac impI, case_tac "?f n", simp) |
4515 apply(rule_tac allI, rule_tac impI, case_tac "?f n", simp) |
4492 apply(simp add: step.simps) |
4516 apply(simp add: step.simps) |
4493 apply(case_tac d, case_tac [2] aa, simp_all) |
4517 apply(case_tac d, case_tac [2] aa, simp_all) |
|
4518 apply(simp_all only: wadjust_inv.simps split: if_splits) |
|
4519 apply(simp_all) |
4494 apply(simp_all add: wadjust_inv.simps wadjust_le_def |
4520 apply(simp_all add: wadjust_inv.simps wadjust_le_def |
4495 abacus.lex_triple_def abacus.lex_pair_def lex_square_def numeral_4_eq_4 |
4521 abacus.lex_triple_def abacus.lex_pair_def lex_square_def split: if_splits) |
4496 split: if_splits) |
|
4497 done |
4522 done |
4498 next |
4523 next |
4499 show "?Q (?f 0)" |
4524 show "?Q (?f 0)" |
4500 apply(simp add: steps.simps wadjust_inv.simps wadjust_start.simps, auto) |
4525 apply(simp add: steps.simps wadjust_inv.simps wadjust_start.simps, auto) |
4501 done |
4526 done |
5289 |
5314 |
5290 text {* |
5315 text {* |
5291 The correctness of @{text "UTM"}, the unhalt case. |
5316 The correctness of @{text "UTM"}, the unhalt case. |
5292 *} |
5317 *} |
5293 |
5318 |
5294 lemma UTM_uhalt_lemma: |
5319 lemma UTM_uhalt_lemma': |
5295 assumes tm_wf: "tm_wf (tp, 0)" |
5320 assumes tm_wf: "tm_wf (tp, 0)" |
5296 and unhalt: "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <args>) tp stp))" |
5321 and unhalt: "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <args>) tp stp))" |
5297 and args: "args \<noteq> []" |
5322 and args: "args \<noteq> []" |
5298 shows " \<forall> stp. \<not> is_final (steps0 (Suc 0, [], <code tp # args>) UTM stp)" |
5323 shows " \<forall> stp. \<not> is_final (steps0 (Suc 0, [], <code tp # args>) UTM stp)" |
5299 using UTM_uhalt_lemma_pre[of tp l args] assms |
5324 using UTM_uhalt_lemma_pre[of tp l args] assms |
5300 apply(simp add: UTM_pre_def t_utm_def UTM_def F_aprog_def F_tprog_def) |
5325 apply(simp add: UTM_pre_def t_utm_def UTM_def F_aprog_def F_tprog_def) |
5301 apply(case_tac "rec_ci rec_F", simp) |
5326 apply(case_tac "rec_ci rec_F", simp) |
5302 done |
5327 done |
5303 |
5328 |
|
5329 lemma UTM_halt_lemma: |
|
5330 assumes tm_wf: "tm_wf (p, 0)" |
|
5331 and resut: "rs > 0" |
|
5332 and args: "(args::nat list) \<noteq> []" |
|
5333 and exec: "{(\<lambda>tp. tp = (Bk\<up>i, <args>))} p {(\<lambda>tp. tp = (Bk\<up>m, Oc\<up>rs @ Bk\<up>k))}" |
|
5334 shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM {(\<lambda>tp. (\<exists> m n. tp = (Bk\<up>m, Oc\<up>rs @ Bk\<up>n)))}" |
|
5335 proof - |
|
5336 have "{(\<lambda> (l, r). l = [] \<and> r = <code p # args>)} (t_wcode |+| t_utm) |
|
5337 {(\<lambda> (l, r). (\<exists> m. l = Bk\<up>m) \<and> (\<exists> n. r = Oc\<up>rs @ Bk\<up>n))}" |
|
5338 proof(rule_tac Hoare_plus_halt) |
|
5339 show "{\<lambda>(l, r). l = [] \<and> r = <code p # args>} t_wcode {\<lambda> (l, r). (l = [Bk] \<and> |
|
5340 (\<exists> rn. r = Oc\<up>(Suc (code p)) @ Bk # Oc\<up>(Suc (bl_bin (<args>))) @ Bk\<up>(rn)))}" |
|
5341 apply(rule_tac Hoare_haltI, auto) |
|
5342 using wcode_lemma_1[of args "code p"] args |
|
5343 apply(auto) |
|
5344 apply(rule_tac x = stp in exI, simp) |
|
5345 done |
|
5346 next |
|
5347 have "\<exists> stp. steps0 (Suc 0, Bk\<up>i, <args>) p stp = (0, Bk\<up>m, Oc\<up>rs @ Bk\<up>k)" |
|
5348 using exec |
|
5349 apply(simp add: Hoare_halt_def, auto) |
|
5350 apply(case_tac "steps0 (Suc 0, Bk \<up> i, <args>) p n", simp) |
|
5351 apply(rule_tac x = n in exI, simp) |
|
5352 done |
|
5353 then obtain stp where k: "steps0 (Suc 0, Bk\<up>i, <args>) p stp = (0, Bk\<up>m, Oc\<up>rs @ Bk\<up>k)" |
|
5354 .. |
|
5355 thus "{\<lambda>(l, r). l = [Bk] \<and> (\<exists>rn. r = Oc \<up> Suc (code p) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> rn)} |
|
5356 t_utm {\<lambda>(l, r). (\<exists>m. l = Bk \<up> m) \<and> (\<exists>n. r = Oc \<up> rs @ Bk \<up> n)}" |
|
5357 proof(rule_tac Hoare_haltI, auto) |
|
5358 fix rn |
|
5359 show "\<exists>n. is_final (steps0 (Suc 0, [Bk], Oc \<up> Suc (code p) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> rn) t_utm n) \<and> |
|
5360 (\<lambda>(l, r). (\<exists>m. l = Bk \<up> m) \<and> (\<exists>n. r = Oc \<up> rs @ Bk \<up> n)) holds_for steps0 |
|
5361 (Suc 0, [Bk], Oc \<up> Suc (code p) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> rn) t_utm n" |
|
5362 using t_utm_halt_eq[of p i "args" stp m rs k rn] assms k |
|
5363 apply(auto simp: bin_wc_eq, auto) |
|
5364 apply(rule_tac x = stpa in exI, simp add: tape_of_nl_abv tape_of_nat_abv) |
|
5365 done |
|
5366 qed |
|
5367 next |
|
5368 show "tm_wf0 t_wcode" by auto |
|
5369 qed |
|
5370 thus "?thesis" |
|
5371 apply(case_tac "rec_ci rec_F") |
|
5372 apply(simp add: UTM_def t_utm_def F_aprog_def F_tprog_def) |
|
5373 apply(auto simp add: Hoare_halt_def) |
|
5374 apply(rule_tac x="n" in exI) |
|
5375 apply(auto) |
|
5376 apply(case_tac "(steps0 (Suc 0, [], <code p # args>) |
|
5377 (t_wcode |+| ((tm_of (a [+] dummy_abc (Suc (Suc 0)))) @ |
|
5378 shift (mopup (Suc (Suc 0))) |
|
5379 (length (tm_of (a [+] dummy_abc (Suc (Suc 0)))) div |
|
5380 2))) n)") |
|
5381 apply(simp) |
|
5382 done |
|
5383 qed |
|
5384 |
|
5385 lemma UTM_halt_lemma2: |
|
5386 assumes tm_wf: "tm_wf (p, 0)" |
|
5387 and args: "(args::nat list) \<noteq> []" |
|
5388 and exec: "{(\<lambda>tp. tp = ([], <args>))} p {(\<lambda>tp. tp = (Bk\<up>m, <(n::nat)> @ Bk\<up>k))}" |
|
5389 shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM {(\<lambda>tp. (\<exists> m k. tp = (Bk\<up>m, <n> @ Bk\<up>k)))}" |
|
5390 using UTM_halt_lemma[OF assms(1) _ assms(2), where i="0"] |
|
5391 using assms(3) |
|
5392 apply(simp add: tape_of_nat_abv) |
|
5393 done |
|
5394 |
|
5395 |
|
5396 lemma UTM_unhalt_lemma: |
|
5397 assumes tm_wf: "tm_wf (p, 0)" |
|
5398 and unhalt: "{(\<lambda>tp. tp = (Bk\<up>i, <args>))} p \<up>" |
|
5399 and args: "args \<noteq> []" |
|
5400 shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM \<up>" |
|
5401 proof - |
|
5402 have "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(i), <args>) p stp))" |
|
5403 using unhalt |
|
5404 apply(auto simp: Hoare_unhalt_def) |
|
5405 apply(case_tac "steps0 (Suc 0, Bk \<up> i, <args>) p stp", simp) |
|
5406 apply(erule_tac x = stp in allE, simp add: TSTD_def) |
|
5407 done |
|
5408 then have "\<forall> stp. \<not> is_final (steps0 (Suc 0, [], <code p # args>) UTM stp)" |
|
5409 using assms |
|
5410 apply(rule_tac UTM_uhalt_lemma', simp_all) |
|
5411 done |
|
5412 thus "?thesis" |
|
5413 apply(simp add: Hoare_unhalt_def) |
|
5414 done |
|
5415 qed |
|
5416 |
|
5417 lemma UTM_unhalt_lemma2: |
|
5418 assumes tm_wf: "tm_wf (p, 0)" |
|
5419 and unhalt: "{(\<lambda>tp. tp = ([], <args>))} p \<up>" |
|
5420 and args: "args \<noteq> []" |
|
5421 shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM \<up>" |
|
5422 using UTM_unhalt_lemma[OF assms(1), where i="0"] |
|
5423 using assms(2-3) |
|
5424 apply(simp add: tape_of_nat_abv) |
|
5425 done |
5304 end |
5426 end |