tm: comparison thys/UTM.thy

equal deleted inserted replaced

-:7fa1b8e88d76
+:7cb94089324e
 thus "?thesis"
 apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
 done
 qed
+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))"
 apply(case_tac b, auto simp: fetch.simps nth_of.simps nth_map
 \<Longrightarrow>  fetch (turing_basic.adjust 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
+declare adjust.simps[simp del]
 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"
 by(case_tac st, simp_all add: step.simps fetch.simps)
 moreover hence "st \<le> (length ap) div 2"
 using assms
 apply(case_tac "st \<le> (length ap) div 2", simp)
 apply(case_tac st, auto simp: step.simps fetch.simps)
-apply(case_tac "read r", simp_all add: fetch.simps nth_of.simps)
+apply(case_tac "read r", simp_all add: fetch.simps
-done
+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)"
 using assms
 apply(case_tac "fetch ap st (read r)")
 apply(drule_tac adjust_fetch_norm, simp_all)
 apply(simp add: step.simps)
 using h
 apply(simp add: abc_fourtimes_def)
 done
 qed
 thus "?thesis"
-apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)
+apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
 done
 qed
 lemma wf_fourtimes[intro]: "tm_wf (t_fourtimes_compile, 0)"
 apply(simp only: t_fourtimes_compile_def)
 done
 lemma [simp]: "\<lbrakk>wprepare_add_one m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
 apply(simp only: wprepare_invs)
 apply(case_tac lm, simp_all add: tape_of_nl_abv
-tape_of_nat_list.simps, auto)
+tape_of_nat_list.simps tape_of_nat_abv, auto)
 done
 lemma [simp]: "\<lbrakk>lm \<noteq> [];  wprepare_goto_first_end m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
 apply(simp only: wprepare_invs, auto)
 apply(case_tac mr, simp_all)
 done
 lemma [simp]: "\<lbrakk>lm \<noteq> [];  wprepare_goto_start_pos m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
 apply(simp only: wprepare_invs, auto)
 apply(case_tac lm, simp, case_tac list)
-apply(simp_all add: tape_of_nl_abv tape_of_nat_list.simps)
+apply(simp_all add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
 done
 lemma [simp]: "\<lbrakk>lm \<noteq> [];  wprepare_goto_start_pos m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> b \<noteq> []"
 apply(simp only: wprepare_invs)
 apply(auto)
 lemma tape_of_nl_false1:
 "lm \<noteq> [] \<Longrightarrow> rev b @ [Bk] \<noteq> Bk\<up>(ln) @ Oc # Oc\<up>(m) @ Bk # Bk # <lm::nat list>"
 apply(auto)
 apply(drule_tac rev_equal_iff, simp add: tape_of_nl_rev)
 apply(case_tac "rev lm")
-apply(case_tac [2] list, auto simp: tape_of_nl_abv tape_of_nat_list.simps )
+apply(case_tac [2] list, auto simp: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
 done
 lemma [simp]: "wprepare_loop_start_in_middle m lm (b, [Bk]) = False"
 apply(simp add: wprepare_loop_start_in_middle.simps, auto)
 apply(case_tac mr, simp_all add: )
 lemma [simp]: "wprepare_loop_start_on_rightmost m lm (b, Bk # a # lista)
 \<Longrightarrow> wprepare_loop_goon_in_middle m lm (Bk # b, a # lista) = False"
 apply(auto simp: wprepare_loop_start_on_rightmost.simps
 wprepare_loop_goon_in_middle.simps)
-apply(case_tac [!] mr, simp_all)
 done
 lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start_on_rightmost m lm (b, Bk # a # lista)\<rbrakk>
 \<Longrightarrow> wprepare_loop_goon_on_rightmost m lm (Bk # b, a # lista)"
 apply(simp only: wprepare_loop_start_on_rightmost.simps
 apply(rule_tac x = rn in exI, simp)
 apply(case_tac mr, simp_all add: )
 apply(case_tac lm1, simp)
 apply(rule_tac x = "Suc aa" in exI, simp)
 apply(rule_tac x = list in exI)
-apply(case_tac list, simp_all add: tape_of_nl_abv tape_of_nat_list.simps)
+apply(case_tac list, simp_all add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
 done
 lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, Bk # a # lista)\<rbrakk> \<Longrightarrow>
 wprepare_loop_goon m lm (Bk # b, a # lista)"
 apply(simp add: wprepare_loop_start.simps
 done
 lemma [simp]: "wprepare_loop_goon_on_rightmost m lm (b, Oc # list) = False"
 apply(simp add: wprepare_loop_goon_on_rightmost.simps)
 done
 lemma wprepare_loop1: "\<lbrakk>rev b @ Oc\<up>(mr) =  Oc\<up>(Suc m) @ Bk # Bk # <lm>;
 b \<noteq> []; 0 < mr; Oc # list = Oc\<up>(mr) @ Bk\<up>(rn)\<rbrakk>
 \<Longrightarrow> wprepare_loop_start_on_rightmost m lm (Oc # b, list)"
 apply(simp add: wprepare_loop_start_on_rightmost.simps)
 apply(rule_tac x = rn in exI, simp)
 r =  Bk # Oc # Bk\<up>(ln) @ Bk # Bk # Oc\<up>(bl_bin (<args>)) @ Bk\<up>(rn)))"
 let ?P3 = "\<lambda> tp. False"
 assume h: "args \<noteq> []"
 have "{?P1} t_wcode_prepare |+| t_wcode_main {?Q2}"
 proof(rule_tac Hoare_plus_halt)
-show "?Q1 \<mapsto> ?P2"
-by(simp add: assert_imp_def)
-next
-show "tm_wf (t_wcode_prepare, 0)"
-by auto
-next
 show "{?P1} t_wcode_prepare {?Q1}"
-proof(rule_tac HoareI, auto)
+proof(rule_tac Hoare_haltI, auto)
 show "\<exists>n. is_final (steps0 (Suc 0, [], <m # args>) t_wcode_prepare n) \<and>
 wprepare_stop m args holds_for steps0 (Suc 0, [], <m # args>) t_wcode_prepare n"
 using wprepare_correctness[of args m] h
 apply(auto)
 apply(rule_tac x = n in exI, simp add: wprepare_inv.simps)
 done
 qed
 next
 show "{?P2} t_wcode_main {?Q2}"
-proof(rule_tac HoareI, auto)
+proof(rule_tac Hoare_haltI, auto)
 fix l r
 assume "wprepare_stop m args (l, r)"
 thus "\<exists>n. is_final (steps0 (Suc 0, l, r) t_wcode_main n) \<and>
 (\<lambda>(l, r). l = Bk # Oc # Oc \<up> m \<and> (\<exists>ln rn. r = Bk # Oc # Bk \<up> ln @
 Bk # Bk # Oc \<up> bl_bin (<args>) @ Bk \<up> rn)) holds_for steps0 (Suc 0, l, r) t_wcode_main n"
 apply(auto simp: tape_of_nl_rev)
 apply(rule_tac x = stp in exI, auto)
 done
 qed
 qed
+next
+show "tm_wf0 t_wcode_prepare"
+by auto
 qed
 thus "?thesis"
-apply(auto simp: Hoare_def)
+apply(auto simp: Hoare_halt_def)
 apply(rule_tac x = n in exI)
 apply(case_tac "(steps0 (Suc 0, [], <m # args>)
 (turing_basic.adjust 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"
+where
+"tinres xs ys = (\<exists>n. xs = ys @ Bk \<up> n \<or> ys = xs @ Bk \<up> n)"
 lemma [simp]:  "tinres r r' \<Longrightarrow>
 fetch t ss (read r) =
 fetch t ss (read r')"
 apply(simp add: fetch.simps, auto split: if_splits simp: tinres_def)
 done
 lemma [simp]: "fetch t_wcode_adjust (Suc (Suc (Suc (Suc 0)))) Oc = (L, 5)"
 apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_4_eq_4)
 done
-thm numeral_5_eq_5
 lemma [simp]: "fetch t_wcode_adjust 5 Oc = (W0, 5)"
 apply(simp only: fetch.simps t_wcode_adjust_def nth_of.simps numeral_5_eq_5, simp)
 done
 assume h: "args \<noteq> []"
 hence a: "bl_bin (<args>) > 0"
 using h by simp
 hence "{?P1} (t_wcode_prepare |+| t_wcode_main) |+| t_wcode_adjust {?Q2}"
 proof(rule_tac Hoare_plus_halt)
-show "?Q1 \<mapsto> ?P2"
-by(simp add: assert_imp_def)
 next
 show "tm_wf (t_wcode_prepare |+| t_wcode_main, 0)"
 apply(rule_tac tm_wf_comp, auto)
 done
 next
 show "{?P1} t_wcode_prepare |+| t_wcode_main {?Q1}"
-proof(rule_tac HoareI, auto)
+proof(rule_tac Hoare_haltI, auto)
 show
 "\<exists>n. is_final (steps0 (Suc 0, [], <m # args>) (t_wcode_prepare |+| t_wcode_main) n) \<and>
 (\<lambda>(l, r). l = Bk # Oc # Oc \<up> m \<and>
 (\<exists>ln rn. r = Bk # Oc # Bk \<up> ln @ Bk # Bk # Oc \<up> bl_bin (<args>) @ Bk \<up> rn))
 holds_for steps0 (Suc 0, [], <m # args>) (t_wcode_prepare |+| t_wcode_main) n"
 apply(rule_tac x = ln in exI, auto)
 done
 qed
 next
 show "{?P2} t_wcode_adjust {?Q2}"
-proof(rule_tac HoareI, auto del: replicate_Suc)
+proof(rule_tac Hoare_haltI, auto del: replicate_Suc)
 fix ln rn
 show "\<exists>n. is_final (steps0 (Suc 0, Bk # Oc # Oc \<up> m,
 Bk # Oc # Bk \<up> ln @ Bk # Bk # Oc \<up> bl_bin (<args>) @ Bk \<up> rn) t_wcode_adjust n) \<and>
 wadjust_stop m (bl_bin (<args>) - Suc 0) holds_for steps0
 (Suc 0, Bk # Oc # Oc \<up> m, Bk # Oc # Bk \<up> ln @ Bk # Bk # Oc \<up> bl_bin (<args>) @ Bk \<up> rn) t_wcode_adjust n"
 apply(case_tac "bl_bin (<args>)", simp, simp del: replicate_Suc add: exp_ind wadjust_inv.simps)
 done
 qed
 qed
 thus "?thesis"
-apply(simp add: Hoare_def, auto)
+apply(simp add: Hoare_halt_def, auto)
 apply(case_tac "(steps0 (Suc 0, [], <(m::nat) # args>)
 ((t_wcode_prepare |+| t_wcode_main) |+| t_wcode_adjust) n)")
 apply(rule_tac x = n in exI, auto simp: wadjust_stop.simps)
 using a
 apply(case_tac "bl_bin (<args>)", simp_all)
 lemma wcode_lemma:
 "args \<noteq> [] \<Longrightarrow>
 \<exists> stp ln rn. steps0 (Suc 0, [], <m # args>)  (t_wcode) stp =
 (0,  [Bk],  <[m ,bl_bin (<args>)]> @ Bk\<up>(rn))"
 using wcode_lemma_1[of args m]
-apply(simp add: t_wcode_def tape_of_nl_abv tape_of_nat_list.simps)
+apply(simp add: t_wcode_def tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
 done
 section {* The universal TM *}
 text {*
 done
 lemma [intro]: "tm_wf (t_utm, 0)"
 apply(simp only: t_utm_def F_tprog_def)
 apply(rule_tac t_compiled_correct, auto)
 done
 lemma UTM_halt_lemma_pre:
 assumes wf_tm: "tm_wf (tp, 0)"
 and result: "0 < rs"
 and args: "args \<noteq> []"
 (\<exists> rn. r = Oc\<up>(Suc (code tp)) @ Bk # Oc\<up>(Suc (bl_bin (<args>))) @ Bk\<up>(rn)))"
 let ?P2 = ?Q1
 let ?P3 = "\<lambda> (l, r). False"
 have "{?P1} (t_wcode |+| t_utm) {?Q2}"
 proof(rule_tac Hoare_plus_halt)
-show "?Q1 \<mapsto> ?P2"
-by(simp add: assert_imp_def)
-next
 show "tm_wf (t_wcode, 0)" by auto
 next
 show "{?P1} t_wcode {?Q1}"
-apply(rule_tac HoareI, auto)
+apply(rule_tac Hoare_haltI, auto)
 using wcode_lemma_1[of args "code tp"] args
 apply(auto)
 apply(rule_tac x = stp in exI, simp)
 done
 next
 show "{?P2} t_utm {?Q2}"
-proof(rule_tac HoareI, auto)
+proof(rule_tac Hoare_haltI, auto)
 fix rn
 show "\<exists>n. is_final (steps0 (Suc 0, [Bk], Oc # Oc \<up> code tp @ Bk # Oc # Oc \<up> bl_bin (<args>) @ Bk \<up> rn) t_utm n) \<and>
 (\<lambda>(l, r). (\<exists>ln. l = Bk \<up> ln) \<and>
 (\<exists>rn. r = Oc \<up> rs @ Bk \<up> rn)) holds_for steps0 (Suc 0, [Bk],
 Oc # Oc \<up> code tp @ Bk # Oc # Oc \<up> bl_bin (<args>) @ Bk \<up> rn) t_utm n"
 using t_utm_halt_eq[of tp i "args" stp m rs k rn] assms
 apply(auto simp: bin_wc_eq)
-apply(rule_tac x = stpa in exI, simp add: tape_of_nl_abv)
+apply(rule_tac x = stpa in exI, simp add: tape_of_nl_abv tape_of_nat_abv)
 done
 qed
 qed
 thus "?thesis"
-apply(auto simp: Hoare_def UTM_pre_def)
+apply(auto simp: Hoare_halt_def UTM_pre_def)
 apply(case_tac "steps0 (Suc 0, [], <code tp # args>) (t_wcode |+| t_utm) n")
 apply(rule_tac x = n in exI, simp)
 done
 qed
 let ?Q1 = "\<lambda> (l, r). (l = [Bk] \<and>
 (\<exists> rn. r = Oc\<up>(Suc (code tp)) @ Bk # Oc\<up>(Suc (bl_bin (<args>))) @ Bk\<up>(rn)))"
 let ?P2 = ?Q1
 have "{?P1} (t_wcode |+| t_utm) \<up>"
 proof(rule_tac Hoare_plus_unhalt)
-show "?Q1 \<mapsto> ?P2"
-by(simp add: assert_imp_def)
-next
 show "tm_wf (t_wcode, 0)" by auto
 next
 show "{?P1} t_wcode {?Q1}"
-apply(rule_tac HoareI, auto)
+apply(rule_tac Hoare_haltI, auto)
 using wcode_lemma_1[of args "code tp"] args
 apply(auto)
 apply(rule_tac x = stp in exI, simp)
 done
 next
 show "{?P2} t_utm \<up>"
-proof(rule_tac Hoare_unhalt_I, auto)
+proof(rule_tac Hoare_unhaltI, auto)
 fix n rn
 assume h: "is_final (steps0 (Suc 0, [Bk], Oc \<up> Suc (code tp) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> rn) t_utm n)"
 have "\<forall> stp. \<not> is_final (steps0 (Suc 0, Bk\<up>(Suc 0), <[code tp, bl2wc (<args>)]> @ Bk\<up>(rn)) t_utm stp)"
 using assms
 apply(rule_tac tutm_uhalt, simp_all)
 done
 thus "False"
 using h
 apply(erule_tac x = n in allE)
-apply(simp add: tape_of_nl_abv bin_wc_eq)
+apply(simp add: tape_of_nl_abv bin_wc_eq tape_of_nat_abv)
 done
 qed
 qed
 thus "?thesis"
 apply(simp add: Hoare_unhalt_def UTM_pre_def)

changeset 139	7cb94089324e
parent 133	ca7fb6848715
child 145	38d8e0e37b7d