1080 |
1080 |
1081 fun inv_stop :: "inc_inv_t" |
1081 fun inv_stop :: "inc_inv_t" |
1082 where "inv_stop (as, lm) (s, l, r) ires= |
1082 where "inv_stop (as, lm) (s, l, r) ires= |
1083 (\<exists> rn. l = Bk # Bk # ires \<and> r = <lm> @ Bk\<up>rn)" |
1083 (\<exists> rn. l = Bk # Bk # ires \<and> r = <lm> @ Bk\<up>rn)" |
1084 |
1084 |
1085 |
|
1086 lemma halt_lemma2': |
1085 lemma halt_lemma2': |
1087 "\<lbrakk>wf LE; \<forall> n. ((\<not> P (f n) \<and> Q (f n)) \<longrightarrow> |
1086 "\<lbrakk>wf LE; \<forall> n. ((\<not> P (f n) \<and> Q (f n)) \<longrightarrow> |
1088 (Q (f (Suc n)) \<and> (f (Suc n), (f n)) \<in> LE)); Q (f 0)\<rbrakk> |
1087 (Q (f (Suc n)) \<and> (f (Suc n), (f n)) \<in> LE)); Q (f 0)\<rbrakk> |
1089 \<Longrightarrow> \<exists> n. P (f n)" |
1088 \<Longrightarrow> \<exists> n. P (f n)" |
|
1089 |
1090 apply(intro exCI, simp) |
1090 apply(intro exCI, simp) |
1091 apply(subgoal_tac "\<forall> n. Q (f n)", simp) |
1091 apply(subgoal_tac "\<forall> n. Q (f n)", simp) |
1092 apply(drule_tac f = f in wf_inv_image) |
1092 apply(drule_tac f = f in wf_inv_image) |
1093 apply(simp add: inv_image_def) |
1093 apply(simp add: inv_image_def) |
1094 apply(erule wf_induct, simp) |
1094 apply(erule wf_induct, simp) |
1316 apply(rule_tac x = "Suc ml" in exI, rule_tac x = "mr - 1" in exI, |
1316 apply(rule_tac x = "Suc ml" in exI, rule_tac x = "mr - 1" in exI, |
1317 rule_tac x = rn in exI) |
1317 rule_tac x = rn in exI) |
1318 apply(case_tac mr, simp_all, auto) |
1318 apply(case_tac mr, simp_all, auto) |
1319 done |
1319 done |
1320 |
1320 |
1321 (* |
|
1322 lemma zero_and_nil[intro]: "(Bk # Bk\<^bsup>n\<^esup> = Oc\<^bsup>mr\<^esup> @ Bk # <lm::nat list> @ |
|
1323 Bk\<^bsup>rn \<^esup>) \<or> (lm2 = [] \<and> Bk # Bk\<^bsup>n\<^esup> = Oc\<^bsup>mr\<^esup>) |
|
1324 \<Longrightarrow> mr = 0 \<and> lm = []" |
|
1325 apply(rule context_conjI) |
|
1326 apply(case_tac mr, auto simp:exponent_def) |
|
1327 apply(insert BkCons_nil[of "replicate (n - 1) Bk" lm rn]) |
|
1328 apply(case_tac n, auto simp: exponent_def Bk_def tape_of_nl_nil_eq) |
|
1329 done |
|
1330 |
|
1331 lemma tape_of_nat_def: "<[m::nat]> = Oc # Oc\<^bsup>m\<^esup>" |
|
1332 apply(simp add: tape_of_nl_abv tape_of_nat_list.simps) |
|
1333 done |
|
1334 *) |
|
1335 lemma [simp]: "<[x::nat]> = Oc\<up>(Suc x)" |
1321 lemma [simp]: "<[x::nat]> = Oc\<up>(Suc x)" |
1336 apply(simp add: tape_of_nat_abv tape_of_nl_abv) |
1322 apply(simp add: tape_of_nat_abv tape_of_nl_abv) |
1337 done |
1323 done |
1338 |
1324 |
1339 lemma [simp]: " <([]::nat list)> = []" |
1325 lemma [simp]: " <([]::nat list)> = []" |
4452 else if s = 2*n + 2 then 1 |
4438 else if s = 2*n + 2 then 1 |
4453 else if s = 2*n + 3 then 0 |
4439 else if s = 2*n + 3 then 0 |
4454 else if s = 2*n + 4 then 2 |
4440 else if s = 2*n + 4 then 2 |
4455 else 0)" |
4441 else 0)" |
4456 |
4442 |
4457 fun abc_mopup_measure :: "(config \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat)" |
4443 definition |
4458 where |
4444 "abc_mopup_measure = measures [\<lambda>(c, n). abc_mopup_stage1 c n, |
4459 "abc_mopup_measure (c, n) = |
4445 \<lambda>(c, n). abc_mopup_stage2 c n, |
4460 (abc_mopup_stage1 c n, abc_mopup_stage2 c n, |
4446 \<lambda>(c, n). abc_mopup_stage3 c n]" |
4461 abc_mopup_stage3 c n)" |
4447 |
4462 |
4448 lemma wf_abc_mopup_measure: |
4463 definition abc_mopup_LE :: |
4449 shows "wf abc_mopup_measure" |
4464 "(((nat \<times> cell list \<times> cell list) \<times> nat) \<times> |
4450 unfolding abc_mopup_measure_def |
4465 ((nat \<times> cell list \<times> cell list) \<times> nat)) set" |
4451 by auto |
4466 where |
4452 |
4467 "abc_mopup_LE \<equiv> (inv_image lex_triple abc_mopup_measure)" |
4453 lemma abc_mopup_measure_induct [case_names Step]: |
4468 |
4454 "\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> abc_mopup_measure\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" |
4469 lemma wf_abc_mopup_le[intro]: "wf abc_mopup_LE" |
4455 using wf_abc_mopup_measure |
4470 by(auto intro:wf_inv_image simp:abc_mopup_LE_def lex_triple_def lex_pair_def) |
4456 by (metis wf_iff_no_infinite_down_chain) |
4471 |
4457 |
4472 lemma [simp]: "mopup_bef_erase_a (a, aa, []) lm n ires = False" |
4458 lemma [simp]: "mopup_bef_erase_a (a, aa, []) lm n ires = False" |
4473 apply(auto simp: mopup_bef_erase_a.simps) |
4459 apply(auto simp: mopup_bef_erase_a.simps) |
4474 done |
4460 done |
4475 |
4461 |
4492 mopup_a (Suc nat) ! ((4 * nat) + 2)", |
4478 mopup_a (Suc nat) ! ((4 * nat) + 2)", |
4493 simp add: mopup_a.simps nth_append) |
4479 simp add: mopup_a.simps nth_append) |
4494 apply(rule mopup_a_nth, auto) |
4480 apply(rule mopup_a_nth, auto) |
4495 done |
4481 done |
4496 |
4482 |
4497 (* FIXME: is also in uncomputable *) |
|
4498 lemma halt_lemma: |
|
4499 "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" |
|
4500 by (metis wf_iff_no_infinite_down_chain) |
|
4501 |
|
4502 |
|
4503 lemma mopup_halt: |
4483 lemma mopup_halt: |
4504 assumes |
4484 assumes |
4505 less: "n < length lm" |
4485 less: "n < length lm" |
4506 and inv: "mopup_inv (Suc 0, l, r) lm n ires" |
4486 and inv: "mopup_inv (Suc 0, l, r) lm n ires" |
4507 and f: "f = (\<lambda> stp. (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))" |
4487 and f: "f = (\<lambda> stp. (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))" |
4508 and P: "P = (\<lambda> (c, n). is_final c)" |
4488 and P: "P = (\<lambda> (c, n). is_final c)" |
4509 shows "\<exists> stp. P (f stp)" |
4489 shows "\<exists> stp. P (f stp)" |
4510 proof(rule_tac LE = abc_mopup_LE in halt_lemma) |
4490 proof (induct rule: abc_mopup_measure_induct) |
4511 show "wf abc_mopup_LE" by(auto) |
4491 case (Step na) |
4512 next |
4492 have h: "\<not> P (f na)" by fact |
4513 show "\<forall>n. \<not> P (f n) \<longrightarrow> (f (Suc n), f n) \<in> abc_mopup_LE" |
4493 show "(f (Suc na), f na) \<in> abc_mopup_measure" |
4514 proof(rule_tac allI, rule_tac impI) |
4494 proof(simp add: f) |
4515 fix na |
4495 obtain a b c where g:"steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na = (a, b, c)" |
4516 assume h: "\<not> P (f na)" |
4496 apply(case_tac "steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na", auto) |
4517 show "(f (Suc na), f na) \<in> abc_mopup_LE" |
4497 done |
4518 proof(simp add: f) |
4498 then have "mopup_inv (a, b, c) lm n ires" |
4519 obtain a b c where g:"steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na = (a, b, c)" |
4499 using inv less mopup_inv_steps[of n lm "Suc 0" l r ires na] |
4520 apply(case_tac "steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na", auto) |
4500 apply(simp) |
4521 done |
4501 done |
4522 then have "mopup_inv (a, b, c) lm n ires" |
4502 moreover have "a > 0" |
4523 using inv less mopup_inv_steps[of n lm "Suc 0" l r ires na] |
4503 using h g |
4524 apply(simp) |
4504 apply(simp add: f P) |
4525 done |
4505 done |
4526 moreover have "a > 0" |
4506 ultimately |
4527 using h g |
4507 have "((step (a, b, c) (mopup_a n @ shift mopup_b (2 * n), 0), n), (a, b, c), n) \<in> abc_mopup_measure" |
4528 apply(simp add: f P) |
4508 apply(case_tac c, case_tac [2] aa) |
4529 done |
4509 apply(auto split:if_splits simp add:step.simps mopup_inv.simps) |
4530 ultimately have "((step (a, b, c) (mopup_a n @ shift mopup_b (2 * n), 0), n), (a, b, c), n) \<in> abc_mopup_LE" |
4510 apply(simp_all add: mopupfetchs abc_mopup_measure_def lex_triple_def lex_pair_def ) |
4531 apply(case_tac c, case_tac [2] aa) |
4511 done |
4532 apply(auto split:if_splits simp add:step.simps mopup_inv.simps) |
4512 thus "((step (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na) |
4533 apply(simp_all add: mopupfetchs abc_mopup_LE_def lex_triple_def lex_pair_def ) |
4513 (mopup_a n @ shift mopup_b (2 * n), 0), n), |
4534 done |
4514 steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na, n) |
4535 thus "((step (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na) |
4515 \<in> abc_mopup_measure" |
4536 (mopup_a n @ shift mopup_b (2 * n), 0), n), |
4516 using g by simp |
4537 steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na, n) |
|
4538 \<in> abc_mopup_LE" |
|
4539 using g by simp |
|
4540 qed |
|
4541 qed |
4517 qed |
4542 qed |
4518 qed |
4543 |
4519 |
4544 lemma mopup_inv_start: |
4520 lemma mopup_inv_start: |
4545 "n < length am \<Longrightarrow> mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires" |
4521 "n < length am \<Longrightarrow> mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires" |
4546 apply(auto simp: mopup_inv.simps mopup_bef_erase_a.simps mopup_jump_over1.simps) |
4522 apply(auto simp: mopup_inv.simps mopup_bef_erase_a.simps mopup_jump_over1.simps) |
4547 apply(case_tac [!] am, auto split: if_splits simp: tape_of_nl_cons) |
4523 apply(case_tac [!] am, auto split: if_splits simp: tape_of_nl_cons) |
4687 qed |
4663 qed |
4688 |
4664 |
4689 lemma compile_correct_unhalt: |
4665 lemma compile_correct_unhalt: |
4690 assumes layout: "ly = layout_of ap" |
4666 assumes layout: "ly = layout_of ap" |
4691 and compile: "tp = tm_of ap" |
4667 and compile: "tp = tm_of ap" |
4692 and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires" |
4668 and crsp: "crsp ly (0, lm) (1, l, r) ires" |
4693 and off: "off = length tp div 2" |
4669 and off: "off = length tp div 2" |
4694 and abc_unhalt: "\<forall> stp. (\<lambda> (as, am). as < length ap) (abc_steps_l (0, lm) ap stp)" |
4670 and abc_unhalt: "\<forall> stp. (\<lambda> (as, am). as < length ap) (abc_steps_l (0, lm) ap stp)" |
4695 shows "\<forall> stp.\<not> is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp)" |
4671 shows "\<forall> stp.\<not> is_final (steps (1, l, r) (tp @ shift (mopup n) off, 0) stp)" |
4696 using assms |
4672 using assms |
4697 proof(rule_tac allI, rule_tac notI) |
4673 proof(rule_tac allI, rule_tac notI) |
4698 fix stp |
4674 fix stp |
4699 assume h: "is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp)" |
4675 assume h: "is_final (steps (1, l, r) (tp @ shift (mopup n) off, 0) stp)" |
4700 obtain as am where a: "abc_steps_l (0, lm) ap stp = (as, am)" |
4676 obtain as am where a: "abc_steps_l (0, lm) ap stp = (as, am)" |
4701 by(case_tac "abc_steps_l (0, lm) ap stp", auto) |
4677 by(case_tac "abc_steps_l (0, lm) ap stp", auto) |
4702 then have b: "as < length ap" |
4678 then have b: "as < length ap" |
4703 using abc_unhalt |
4679 using abc_unhalt |
4704 by(erule_tac x = stp in allE, simp) |
4680 by(erule_tac x = stp in allE, simp) |
4705 have "\<exists> stpa\<ge>stp. crsp ly (as, am) (steps (Suc 0, l, r) (tp, 0) stpa) ires " |
4681 have "\<exists> stpa\<ge>stp. crsp ly (as, am) (steps (1, l, r) (tp, 0) stpa) ires " |
4706 using assms b a |
4682 using assms b a |
4707 apply(rule_tac crsp_steps2, simp_all) |
4683 apply(simp add: numeral) |
|
4684 apply(rule_tac crsp_steps2) |
|
4685 apply(simp_all) |
4708 done |
4686 done |
4709 then obtain stpa where |
4687 then obtain stpa where |
4710 "stpa\<ge>stp \<and> crsp ly (as, am) (steps (Suc 0, l, r) (tp, 0) stpa) ires" .. |
4688 "stpa\<ge>stp \<and> crsp ly (as, am) (steps (1, l, r) (tp, 0) stpa) ires" .. |
4711 then obtain s' l' r' where b: "(steps (Suc 0, l, r) (tp, 0) stpa) = (s', l', r') \<and> |
4689 then obtain s' l' r' where b: "(steps (1, l, r) (tp, 0) stpa) = (s', l', r') \<and> |
4712 stpa\<ge>stp \<and> crsp ly (as, am) (s', l', r') ires" |
4690 stpa\<ge>stp \<and> crsp ly (as, am) (s', l', r') ires" |
4713 by(case_tac "steps (Suc 0, l, r) (tp, 0) stpa", auto) |
4691 by(case_tac "steps (1, l, r) (tp, 0) stpa", auto) |
4714 hence c: |
4692 hence c: |
4715 "(steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stpa) = (s', l', r')" |
4693 "(steps (1, l, r) (tp @ shift (mopup n) off, 0) stpa) = (s', l', r')" |
4716 by(rule_tac tm_append_first_steps_eq, simp_all add: crsp.simps) |
4694 by(rule_tac tm_append_first_steps_eq, simp_all add: crsp.simps) |
4717 from b have d: "s' > 0 \<and> stpa \<ge> stp" |
4695 from b have d: "s' > 0 \<and> stpa \<ge> stp" |
4718 by(simp add: crsp.simps) |
4696 by(simp add: crsp.simps) |
4719 then obtain diff where e: "stpa = stp + diff" by (metis le_iff_add) |
4697 then obtain diff where e: "stpa = stp + diff" by (metis le_iff_add) |
4720 obtain s'' l'' r'' where f: |
4698 obtain s'' l'' r'' where f: |
4721 "steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp = (s'', l'', r'') \<and> is_final (s'', l'', r'')" |
4699 "steps (1, l, r) (tp @ shift (mopup n) off, 0) stp = (s'', l'', r'') \<and> is_final (s'', l'', r'')" |
4722 using h |
4700 using h |
4723 by(case_tac "steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp", auto) |
4701 by(case_tac "steps (1, l, r) (tp @ shift (mopup n) off, 0) stp", auto) |
4724 |
4702 |
4725 then have "is_final (steps (s'', l'', r'') (tp @ shift (mopup n) off, 0) diff)" |
4703 then have "is_final (steps (s'', l'', r'') (tp @ shift (mopup n) off, 0) diff)" |
4726 by(auto intro: after_is_final) |
4704 by(auto intro: after_is_final) |
4727 then have "is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stpa)" |
4705 then have "is_final (steps (1, l, r) (tp @ shift (mopup n) off, 0) stpa)" |
4728 using e |
4706 using e f by simp |
4729 by(simp add: steps_add f) |
|
4730 from this and c d show "False" by simp |
4707 from this and c d show "False" by simp |
4731 qed |
4708 qed |
4732 |
4709 |
4733 end |
4710 end |
4734 |
4711 |