tm: comparison thys/UTM.thy

equal deleted inserted replaced

-:5974111de158
+:f1ecb4a68a54
 where
 "t_twice_compile= (tm_of abc_twice @ (shift (mopup 1) (length (tm_of abc_twice) div 2)))"
 definition t_twice :: "instr list"
 where
-"t_twice = adjust t_twice_compile"
+"t_twice = adjust0 t_twice_compile"
 definition t_fourtimes_compile :: "instr list"
 where
 "t_fourtimes_compile= (tm_of abc_fourtimes @ (shift (mopup 1) (length (tm_of abc_fourtimes) div 2)))"
 definition t_fourtimes :: "instr list"
 where
-"t_fourtimes = adjust t_fourtimes_compile"
+"t_fourtimes = adjust0 t_fourtimes_compile"
 definition t_twice_len :: "nat"
 where
 "t_twice_len = length t_twice div 2"
 declare adjust.simps[simp]
 lemma adjust_fetch0:
 "\<lbrakk>0 < a; a \<le> length ap div 2;  fetch ap a b = (aa, 0)\<rbrakk>
-\<Longrightarrow> fetch (adjust ap) a b = (aa, Suc (length ap div 2))"
+\<Longrightarrow> fetch (adjust0 ap) a b = (aa, Suc (length ap div 2))"
 apply(case_tac b, auto simp: fetch.simps nth_of.simps nth_map
 split: if_splits)
 apply(case_tac [!] a, auto simp: fetch.simps nth_of.simps)
 done
 lemma adjust_fetch_norm:
 "\<lbrakk>st > 0;  st \<le> length tp div 2; fetch ap st b = (aa, ns); ns \<noteq> 0\<rbrakk>
-\<Longrightarrow>  fetch (Turing.adjust ap) st b = (aa, ns)"
+\<Longrightarrow>  fetch (adjust0 ap) st b = (aa, ns)"
 apply(case_tac b, auto simp: fetch.simps nth_of.simps nth_map
 split: if_splits)
 apply(case_tac [!] st, auto simp: fetch.simps nth_of.simps)
 done
 lemma adjust_step_eq:
 assumes exec: "step0 (st,l,r) ap = (st', l', r')"
 and wf_tm: "tm_wf (ap, 0)"
 and notfinal: "st' > 0"
-shows "step0 (st, l, r) (adjust ap) = (st', l', r')"
+shows "step0 (st, l, r) (adjust0 ap) = (st', l', r')"
 using assms
 proof -
 have "st > 0"
 using assms
 by(case_tac st, simp_all add: step.simps fetch.simps)
 apply(case_tac st, auto simp: step.simps fetch.simps)
 apply(case_tac "read r", simp_all add: fetch.simps
 nth_of.simps adjust.simps tm_wf.simps split: if_splits)
 apply(auto simp: mod_ex2)
 done
-ultimately have "fetch (adjust ap) st (read r) = fetch ap st (read r)"
+ultimately have "fetch (adjust0 ap) st (read r) = fetch ap st (read r)"
 using assms
 apply(case_tac "fetch ap st (read r)")
 apply(drule_tac adjust_fetch_norm, simp_all)
 apply(simp add: step.simps)
 done
 lemma adjust_steps_eq:
 assumes exec: "steps0 (st,l,r) ap stp = (st', l', r')"
 and wf_tm: "tm_wf (ap, 0)"
 and notfinal: "st' > 0"
-shows "steps0 (st, l, r) (adjust ap) stp = (st', l', r')"
+shows "steps0 (st, l, r) (adjust0 ap) stp = (st', l', r')"
 using exec notfinal
 proof(induct stp arbitrary: st' l' r')
 case 0
 thus "?case"
 by(simp add: steps.simps)
 next
 case (Suc stp st' l' r')
 have ind: "\<And>st' l' r'. \<lbrakk>steps0 (st, l, r) ap stp = (st', l', r'); 0 < st'\<rbrakk>
-\<Longrightarrow> steps0 (st, l, r) (Turing.adjust ap) stp = (st', l', r')" by fact
+\<Longrightarrow> steps0 (st, l, r) (adjust0 ap) stp = (st', l', r')" by fact
 have h: "steps0 (st, l, r) ap (Suc stp) = (st', l', r')" by fact
 have g:   "0 < st'" by fact
 obtain st'' l'' r'' where a: "steps0 (st, l, r) ap stp = (st'', l'', r'')"
 by (metis prod_cases3)
 hence c:"0 < st''"
 using h g
 apply(simp add: step_red)
 apply(case_tac st'', auto)
 done
-hence b: "steps0 (st, l, r) (Turing.adjust ap) stp = (st'', l'', r'')"
+hence b: "steps0 (st, l, r) (adjust0 ap) stp = (st'', l'', r'')"
 using a
 by(rule_tac ind, simp_all)
 thus "?case"
 using assms a b h g
 apply(simp add: step_red)
 qed
 lemma adjust_halt_eq:
 assumes exec: "steps0 (1, l, r) ap stp = (0, l', r')"
 and tm_wf: "tm_wf (ap, 0)"
-shows "\<exists> stp. steps0 (Suc 0, l, r) (adjust ap) stp =
+shows "\<exists> stp. steps0 (Suc 0, l, r) (adjust0 ap) stp =
 (Suc (length ap div 2), l', r')"
 proof -
 have "\<exists> stp. \<not> is_final (steps0 (1, l, r) ap stp) \<and> (steps0 (1, l, r) ap (Suc stp) = (0, l', r'))"
 using exec
 by(erule_tac before_final)
 then obtain stpa where a:
 "\<not> is_final (steps0 (1, l, r) ap stpa) \<and> (steps0 (1, l, r) ap (Suc stpa) = (0, l', r'))" ..
 obtain sa la ra where b:"steps0 (1, l, r) ap stpa = (sa, la, ra)"  by (metis prod_cases3)
-hence c: "steps0 (Suc 0, l, r) (adjust ap) stpa = (sa, la, ra)"
+hence c: "steps0 (Suc 0, l, r) (adjust0 ap) stpa = (sa, la, ra)"
 using assms a
 apply(rule_tac adjust_steps_eq, simp_all)
 done
 have d: "sa \<le> length ap div 2"
 using steps_in_range[of  "(l, r)" ap stpa] a tm_wf b
 by (metis prod.exhaust)
 hence f: "ns = 0"
 using b a
 apply(simp add: step_red step.simps)
 done
-have k: "fetch (adjust ap) sa (read ra) = (ac, Suc (length ap div 2))"
+have k: "fetch (adjust0 ap) sa (read ra) = (ac, Suc (length ap div 2))"
 using a b c d e f
 apply(rule_tac adjust_fetch0, simp_all)
 done
 from a b e f k and c show "?thesis"
 apply(rule_tac x = "Suc stpa" in exI)
 by(rule_tac t_twice_correct)
 then obtain stp ln rn where " steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
 (tm_of abc_twice @ shift (mopup (Suc 0)) ((length (tm_of abc_twice) div 2))) stp =
 (0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))" by blast
 hence "\<exists> stp. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
-(adjust t_twice_compile) stp
+(adjust0 t_twice_compile) stp
 = (Suc (length t_twice_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))"
 apply(rule_tac stp = stp in adjust_halt_eq)
 apply(simp add: t_twice_compile_def, auto)
 done
 then obtain stpb where
 "steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
-(adjust t_twice_compile) stpb
+(adjust0 t_twice_compile) stpb
 = (Suc (length t_twice_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))" ..
 thus "?thesis"
 apply(simp add: t_twice_def t_twice_len_def)
 by metis
 qed
 then obtain stp ln rn where
 "steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
 (tm_of abc_fourtimes @ shift (mopup 1) ((length (tm_of abc_fourtimes) div 2))) stp =
 (0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))" by blast
 hence "\<exists> stp. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
-(adjust t_fourtimes_compile) stp
+(adjust0 t_fourtimes_compile) stp
 = (Suc (length t_fourtimes_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))"
 apply(rule_tac stp = stp in adjust_halt_eq)
 apply(simp add: t_fourtimes_compile_def, auto)
 done
 then obtain stpb where
 "steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
-(adjust t_fourtimes_compile) stpb
+(adjust0 t_fourtimes_compile) stpb
 = (Suc (length t_fourtimes_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))" ..
 thus "?thesis"
 apply(simp add: t_fourtimes_def t_fourtimes_len_def)
 by metis
 qed
 done
 lemma tm_wf_change_termi: "tm_wf (tp, 0) \<Longrightarrow>
-list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (adjust tp)"
+list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (adjust0 tp)"
 apply(auto simp: tm_wf.simps List.list_all_length)
 apply(case_tac "tp!n", auto simp: adjust.simps split: if_splits)
 apply(erule_tac x = "(a, b)" in ballE, auto)
 by (metis in_set_conv_nth)
 lemma [simp]: "length (mopup (Suc 0)) = 16"
 apply(auto simp: mopup.simps)
 done
-lemma [elim]: "(a, b) \<in> set (shift (Turing.adjust t_twice_compile) 12) \<Longrightarrow>
+lemma [elim]: "(a, b) \<in> set (shift (adjust0 t_twice_compile) 12) \<Longrightarrow>
 b \<le> (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2"
 apply(simp add: t_twice_compile_def t_fourtimes_compile_def)
 proof -
-assume g: "(a, b) \<in> set (shift (Turing.adjust (tm_of abc_twice @ shift (mopup (Suc 0)) (length (tm_of abc_twice) div 2))) 12)"
+assume g: "(a, b)
+\<in> set (shift
+(adjust
+(tm_of abc_twice @
+shift (mopup (Suc 0)) (length (tm_of abc_twice) div 2))
+(Suc ((length (tm_of abc_twice) + 16) div 2)))
+12)"
 moreover have "length (tm_of abc_twice) mod 2 = 0" by auto
 moreover have "length (tm_of abc_fourtimes) mod 2 = 0" by auto
 ultimately have "list_all (\<lambda>(acn, st). (st \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2))
-(shift (Turing.adjust t_twice_compile) 12)"
+(shift (adjust0 t_twice_compile) 12)"
-proof(auto simp: mod_ex1)
+proof(auto simp add: mod_ex1 del: adjust.simps)
 fix q qa
 assume h: "length (tm_of abc_twice) = 2 * q" "length (tm_of abc_fourtimes) = 2 * qa"
-hence "list_all (\<lambda>(acn, st). st \<le> (18 + (q + qa)) + 12) (shift (Turing.adjust t_twice_compile) 12)"
+hence "list_all (\<lambda>(acn, st). st \<le> (18 + (q + qa)) + 12) (shift (adjust0 t_twice_compile) 12)"
 proof(rule_tac tm_wf_shift t_twice_compile_def)
-have "list_all (\<lambda>(acn, st). st \<le> Suc (length t_twice_compile div 2)) (adjust t_twice_compile)"
+have "list_all (\<lambda>(acn, st). st \<le> Suc (length t_twice_compile div 2)) (adjust0 t_twice_compile)"
 by(rule_tac tm_wf_change_termi, auto)
-thus "list_all (\<lambda>(acn, st). st \<le> 18 + (q + qa)) (Turing.adjust t_twice_compile)"
+thus "list_all (\<lambda>(acn, st). st \<le> 18 + (q + qa)) (adjust0 t_twice_compile)"
 using h
 apply(simp add: t_twice_compile_def, auto simp: List.list_all_length)
 done
 qed
-thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa)) (shift (Turing.adjust t_twice_compile) 12)"
+thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa))
+(shift
+(adjust t_twice_compile (Suc (length t_twice_compile div 2))) 12)"
 by simp
 qed
 thus "b \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2"
 using g
 apply(auto simp:t_twice_compile_def)
 apply(simp add: Ball_set[THEN sym])
 apply(erule_tac x = "(a, b)" in ballE, simp, simp)
 done
 qed
-lemma [elim]: "(a, b) \<in> set (shift (Turing.adjust t_fourtimes_compile) (t_twice_len + 13))
+lemma [elim]: "(a, b) \<in> set (shift (adjust0 t_fourtimes_compile) (t_twice_len + 13))
 \<Longrightarrow> b \<le> (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2"
 apply(simp add: t_twice_compile_def t_fourtimes_compile_def t_twice_len_def)
 proof -
-assume g: "(a, b) \<in> set (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0))
+assume g: "(a, b)
-(length (tm_of abc_fourtimes) div 2))) (length t_twice div 2 + 13))"
+\<in> set (shift
+(adjust
+(tm_of abc_fourtimes @
+shift (mopup (Suc 0)) (length (tm_of abc_fourtimes) div 2))
+(Suc ((length (tm_of abc_fourtimes) + 16) div 2)))
+(length t_twice div 2 + 13))"
 moreover have "length (tm_of abc_twice) mod 2 = 0" by auto
 moreover have "length (tm_of abc_fourtimes) mod 2 = 0" by auto
 ultimately have "list_all (\<lambda>(acn, st). (st \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2))
-(shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0))
+(shift (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0))
 (length (tm_of abc_fourtimes) div 2))) (length t_twice div 2 + 13))"
 proof(auto simp: mod_ex1 t_twice_def t_twice_compile_def)
 fix q qa
 assume h: "length (tm_of abc_twice) = 2 * q" "length (tm_of abc_fourtimes) = 2 * qa"
 hence "list_all (\<lambda>(acn, st). st \<le> (9 + qa + (21 + q)))
-(shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
+(shift (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
 proof(rule_tac tm_wf_shift t_twice_compile_def)
 have "list_all (\<lambda>(acn, st). st \<le> Suc (length (tm_of abc_fourtimes @ shift
-(mopup (Suc 0)) qa) div 2)) (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa))"
+(mopup (Suc 0)) qa) div 2)) (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa))"
 apply(rule_tac tm_wf_change_termi)
 using wf_fourtimes h
 apply(simp add: t_fourtimes_compile_def)
 done
-thus "list_all (\<lambda>(acn, st). st \<le> 9 + qa) ((Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)))"
+thus "list_all (\<lambda>(acn, st). st \<le> 9 + qa)
+(adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)
+(Suc (length (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa) div
+2)))"
 using h
 apply(simp)
 done
 qed
-thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa)) (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
+thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa))
+(shift
+(adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)
+(9 + qa))
+(21 + q))"
 apply(subgoal_tac "qa + q = q + qa")
-apply(simp, simp)
+apply(simp add: h)
+apply(simp)
 done
 qed
 thus "b \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2"
 using g
 apply(simp add: Ball_set[THEN sym])
 qed
 thus "?thesis"
 apply(auto simp: Hoare_halt_def)
 apply(rule_tac x = n in exI)
 apply(case_tac "(steps0 (Suc 0, [], <m # args>)
-(Turing.adjust t_wcode_prepare @ shift t_wcode_main (length t_wcode_prepare div 2)) n)")
+(adjust0 t_wcode_prepare @ shift t_wcode_main (length t_wcode_prepare div 2)) n)")
 apply(auto simp: tm_comp.simps)
 done
 qed
 definition tinres :: "cell list \<Rightarrow> cell list \<Rightarrow> bool"
 text {*
 The initialization TM @{text "t_wcode"}.
 *}
 definition t_wcode :: "instr list"
 where
-"t_wcode = (t_wcode_prepare |+| t_wcode_main) |+| t_wcode_adjust"
+"t_wcode = (t_wcode_prepare |+| t_wcode_main) |+| t_wcode_adjust        "
 text {*
 The correctness of @{text "t_wcode"}.
 *}

changeset 190	f1ecb4a68a54
parent 170	eccd79a974ae
child 229	d8e6f0798e23