225 

   225 

   226 text {*

   226 text {*

   227   @{text "start_of layout n"} looks out the starting state of @{text "n"}-th

   227   @{text "start_of layout n"} looks out the starting state of @{text "n"}-th

   228   TM in the finall TM.

   228   TM in the finall TM.

   229 *}

   229 *}

   231 

   230 

   232 fun start_of :: "nat list \<Rightarrow> nat \<Rightarrow> nat"

   231 fun start_of :: "nat list \<Rightarrow> nat \<Rightarrow> nat"

   233   where

   232   where

   234   "start_of ly x = (Suc (listsum (take x ly))) "

   233   "start_of ly x = (Suc (listsum (take x ly))) "

   235 

   234 

   875     using h k

   874     using h k

   876     by(rule_tac notI, auto simp: step_red)

   875     by(rule_tac notI, auto simp: step_red)

   877   from a b have c: "steps0 (s + off, l, r) (A @ shift B off) stp = (s'' + off, l'', r'')"

   876   from a b have c: "steps0 (s + off, l, r) (A @ shift B off) stp = (s'' + off, l'', r'')"

   878     by(erule_tac ind, simp)

   877     by(erule_tac ind, simp)

   879   from c b h a k assms show "?case"

   878   from c b h a k assms show "?case"

   881     apply(simp add: step_red) by(rule tm_append_second_step_eq, simp_all)

   879     apply(simp add: step_red) by(rule tm_append_second_step_eq, simp_all)

   882 qed

   880 qed

   883 

   881 

   884 lemma tm_append_second_fetch0_eq:

   882 lemma tm_append_second_fetch0_eq:

   885   assumes

   883   assumes

   900   and wf_B: "tm_wf (B, 0)"

   898   and wf_B: "tm_wf (B, 0)"

   901   and off: "off = length A div 2"

   899   and off: "off = length A div 2"

   902   and even: "length A mod 2 = 0"

   900   and even: "length A mod 2 = 0"

   903   shows "steps (Suc off, l, r) (A @ shift B off, 0) stp = (0, l', r')"

   901   shows "steps (Suc off, l, r) (A @ shift B off, 0) stp = (0, l', r')"

   904 proof -

   902 proof -

   906   have "\<exists>n. \<not> is_final (steps0 (1, l, r) B n) \<and> steps0 (1, l, r) B (Suc n) = (0, l', r')"

   903   have "\<exists>n. \<not> is_final (steps0 (1, l, r) B n) \<and> steps0 (1, l, r) B (Suc n) = (0, l', r')"

   907     using exec by(rule_tac before_final, simp)

   904     using exec by(rule_tac before_final, simp)

   908  then obtain n where a: 

   905  then obtain n where a: 

   909    "\<not> is_final (steps0 (1, l, r) B n) \<and> steps0 (1, l, r) B (Suc n) = (0, l', r')" ..

   906    "\<not> is_final (steps0 (1, l, r) B n) \<and> steps0 (1, l, r) B (Suc n) = (0, l', r')" ..

   910  obtain s'' l'' r'' where b: "steps0 (1, l, r) B n = (s'', l'', r'') \<and> s'' >0"

   907  obtain s'' l'' r'' where b: "steps0 (1, l, r) B n = (s'', l'', r'') \<and> s'' >0"

  1506   and not0: "n > 0"

  1503   and not0: "n > 0"

  1507   and f: "f = (\<lambda> stp. (steps (Suc 0, l, r) (findnth n, 0) stp, n))"

  1504   and f: "f = (\<lambda> stp. (steps (Suc 0, l, r) (findnth n, 0) stp, n))"

  1508   and P: "P = (\<lambda> ((s, l, r), n). s = Suc (2 * n))"

  1505   and P: "P = (\<lambda> ((s, l, r), n). s = Suc (2 * n))"

  1509   and Q: "Q = (\<lambda> ((s, l, r), n). findnth_inv ly n (as, lm) (s, l, r) ires)"

  1506   and Q: "Q = (\<lambda> ((s, l, r), n). findnth_inv ly n (as, lm) (s, l, r) ires)"

  1510   shows "\<exists> stp. P (f stp) \<and> Q (f stp)"

  1507   shows "\<exists> stp. P (f stp) \<and> Q (f stp)"

  1512 proof(rule_tac LE = findnth_LE in halt_lemma2)

  1508 proof(rule_tac LE = findnth_LE in halt_lemma2)

  1513   show "wf findnth_LE"  by(intro wf_findnth_LE)

  1509   show "wf findnth_LE"  by(intro wf_findnth_LE)

  1514 next

  1510 next

  1515   show "Q (f 0)"

  1511   show "Q (f 0)"

  1516     using crsp layout

  1512     using crsp layout

  2099   and crsp: "crsp ly (as, lm) (s, l, r) ires"

  2095   and crsp: "crsp ly (as, lm) (s, l, r) ires"

  2100   and aexec: "abc_step_l (as, lm) (Some (Inc n)) = (asa, lma)"

  2096   and aexec: "abc_step_l (as, lm) (Some (Inc n)) = (asa, lma)"

  2101   shows "\<exists> stp k. steps (Suc 0, l, r) (findnth n @ shift tinc_b (2 * n), 0) stp 

  2097   shows "\<exists> stp k. steps (Suc 0, l, r) (findnth n @ shift tinc_b (2 * n), 0) stp 

  2102         = (2*n + 10, Bk # Bk # ires, <lma> @ Bk\<up>k) \<and> stp > 0"

  2098         = (2*n + 10, Bk # Bk # ires, <lma> @ Bk\<up>k) \<and> stp > 0"

  2103 proof -

  2099 proof -

  2105   have "\<exists> stp l' r'. steps (Suc 0, l, r) (findnth n, 0) stp = (Suc (2 * n), l', r')

  2100   have "\<exists> stp l' r'. steps (Suc 0, l, r) (findnth n, 0) stp = (Suc (2 * n), l', r')

  2106     \<and> inv_locate_a (as, lm) (n, l', r') ires"

  2101     \<and> inv_locate_a (as, lm) (n, l', r') ires"

  2107     using assms

  2102     using assms

  2108     apply(rule_tac findnth_correct, simp_all add: crsp layout)

  2103     apply(rule_tac findnth_correct, simp_all add: crsp layout)

  2109     done

  2104     done

  2347                  take_Suc_conv_app_nth split: if_splits)

  2342                  take_Suc_conv_app_nth split: if_splits)

  2348 done

  2343 done

  2349 

  2344 

  2350 lemma start_of_less_2: 

  2345 lemma start_of_less_2: 

  2351   "start_of ly e \<le> start_of ly (Suc e)"

  2346   "start_of ly e \<le> start_of ly (Suc e)"

  2353 apply(case_tac "e < length ly")

  2347 apply(case_tac "e < length ly")

  2354 apply(auto simp: start_of.simps take_Suc take_Suc_conv_app_nth)

  2348 apply(auto simp: start_of.simps take_Suc take_Suc_conv_app_nth)

  2355 done

  2349 done

  2356 

  2350 

  2357 lemma start_of_less_1: "start_of ly e \<le> start_of ly (e + d)"

  2351 lemma start_of_less_1: "start_of ly e \<le> start_of ly (e + d)"

  3232     apply(case_tac "r = [] \<or> hd r = Bk", simp_all)

  3226     apply(case_tac "r = [] \<or> hd r = Bk", simp_all)

  3233     done

  3227     done

  3234   from this obtain stpa la ra where a:

  3228   from this obtain stpa la ra where a:

  3235     "steps (start_of ly as + 2 * n, l, r) (?P, ?off) stpa = (Suc (start_of ly as) + 2*n, la, ra)

  3229     "steps (start_of ly as + 2 * n, l, r) (?P, ?off) stpa = (Suc (start_of ly as) + 2*n, la, ra)

  3236              \<and>  inv_locate_b (as, lm) (n, la, ra) ires" by blast

  3230              \<and>  inv_locate_b (as, lm) (n, la, ra) ires" by blast

  3238   have "\<exists> stp lb rb. steps (Suc (start_of ly as) + 2 * n, la, ra) (?P, ?off) stp = (start_of ly e, lb, rb)

  3231   have "\<exists> stp lb rb. steps (Suc (start_of ly as) + 2 * n, la, ra) (?P, ?off) stp = (start_of ly e, lb, rb)

  3239              \<and>  dec_inv_1 ly n e (as, lm) (start_of ly e, lb, rb) ires"

  3232              \<and>  dec_inv_1 ly n e (as, lm) (start_of ly e, lb, rb) ires"

  3240     using assms a

  3233     using assms a

  3241     apply(rule_tac crsp_step_dec_b_e_pre, auto)

  3234     apply(rule_tac crsp_step_dec_b_e_pre, auto)

  3242     done

  3235     done

  3712   apply(case_tac "steps (Suc 0, l, r) (tm_of ap, 0) stpa", simp add: crsp.simps)

  3705   apply(case_tac "steps (Suc 0, l, r) (tm_of ap, 0) stpa", simp add: crsp.simps)

  3713   done

  3706   done

  3714 

  3707 

  3715 text{*The tp @ [(Nop, 0), (Nop, 0)] is nomoral turing machines, so we can use Hoare_plus when composing with Mop machine*}

  3708 text{*The tp @ [(Nop, 0), (Nop, 0)] is nomoral turing machines, so we can use Hoare_plus when composing with Mop machine*}

  3716 

  3709 

  3718 lemma layout_id_cons: "layout_of (ap @ [p]) = layout_of ap @ [length_of p]"

  3710 lemma layout_id_cons: "layout_of (ap @ [p]) = layout_of ap @ [length_of p]"

  3719 apply(simp add: layout_of.simps)

  3711 apply(simp add: layout_of.simps)

  3720 done

  3712 done

  3721 

  3713 

  3722 lemma [simp]: "length (layout_of xs) = length xs"

  3714 lemma [simp]: "length (layout_of xs) = length xs"

  3723 by(simp add: layout_of.simps)

  3715 by(simp add: layout_of.simps)

  3729 

  3716 

  3730 lemma [simp]:  

  3717 lemma [simp]:  

  3731   "map (start_of (layout_of xs @ [length_of x])) [0..<length xs] =  (map (start_of (layout_of xs)) [0..<length xs])"

  3718   "map (start_of (layout_of xs @ [length_of x])) [0..<length xs] =  (map (start_of (layout_of xs)) [0..<length xs])"

  3732 apply(auto)

  3719 apply(auto)

  3733 apply(simp add: layout_of.simps start_of.simps)

  3720 apply(simp add: layout_of.simps start_of.simps)

  4493 lemma [simp]: "mopup_aft_erase_b (2 * n + 3, aa, []) lm n ires = False"

  4480 lemma [simp]: "mopup_aft_erase_b (2 * n + 3, aa, []) lm n ires = False"

  4494 apply(auto simp: mopup_aft_erase_b.simps)

  4481 apply(auto simp: mopup_aft_erase_b.simps)

  4495 done

  4482 done

  4496 

  4483 

  4497 declare mopup_inv.simps[simp del]

  4484 declare mopup_inv.simps[simp del]

  4499 

  4485 

  4500 lemma [simp]: 

  4486 lemma [simp]: 

  4501   "\<lbrakk>0 < q; q \<le> n\<rbrakk> \<Longrightarrow> 

  4487   "\<lbrakk>0 < q; q \<le> n\<rbrakk> \<Longrightarrow> 

  4502      (fetch (mopup_a n @ shift mopup_b (2 * n)) (2*q) Bk) = (R, 2*q - 1)"

  4488      (fetch (mopup_a n @ shift mopup_b (2 * n)) (2*q) Bk) = (R, 2*q - 1)"

  4503 apply(case_tac q, simp, simp)

  4489 apply(case_tac q, simp, simp)

  4532     proof(simp add: f)

  4518     proof(simp add: f)

  4533       obtain a b c where g:"steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na = (a, b, c)"

  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)"

  4534         apply(case_tac "steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na", auto)

  4520         apply(case_tac "steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na", auto)

  4535         done

  4521         done

  4536       then have "mopup_inv (a, b, c) lm n ires"

  4522       then have "mopup_inv (a, b, c) lm n ires"

  4538         using inv less mopup_inv_steps[of n lm "Suc 0" l r ires na]

  4523         using inv less mopup_inv_steps[of n lm "Suc 0" l r ires na]

  4539         apply(simp)

  4524         apply(simp)

  4540         done

  4525         done

  4541       moreover have "a > 0"

  4526       moreover have "a > 0"

  4542         using h g

  4527         using h g

  4639     "steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stpb

  4624     "steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stpb

  4640     = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)" by blast

  4625     = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)" by blast

  4641   then have b: "steps (Suc 0 + off, Bk # Bk # ires, <am> @ Bk \<up> k) (tp @ shift (mopup n) off, 0) stpb

  4626   then have b: "steps (Suc 0 + off, Bk # Bk # ires, <am> @ Bk \<up> k) (tp @ shift (mopup n) off, 0) stpb

  4642     = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)"

  4627     = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)"

  4643     using assms wf_mopup

  4628     using assms wf_mopup

  4645     apply(drule_tac tm_append_second_halt_eq, auto)

  4629     apply(drule_tac tm_append_second_halt_eq, auto)

  4646     done

  4630     done

  4647   from a b show "?thesis"

  4631   from a b show "?thesis"

  4648     by(rule_tac x = "stp + stpb" in exI, simp add: steps_add)

  4632     by(rule_tac x = "stp + stpb" in exI, simp add: steps_add)

  4649 qed

  4633 qed