--- a/thys/UTM.thy Wed Feb 06 14:06:18 2013 +0000
+++ b/thys/UTM.thy Wed Feb 06 14:09:35 2013 +0000
@@ -1235,6 +1235,7 @@
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>
@@ -1252,6 +1253,8 @@
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)"
@@ -1266,8 +1269,10 @@
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)
- done
+ 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)"
using assms
apply(case_tac "fetch ap st (read r)")
@@ -2025,7 +2030,7 @@
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
@@ -2957,7 +2962,7 @@
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> []"
@@ -2980,7 +2985,7 @@
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> []"
@@ -3055,7 +3060,7 @@
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"
@@ -3088,7 +3093,6 @@
\<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>
@@ -3123,7 +3127,7 @@
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>
@@ -3188,6 +3192,7 @@
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)"
@@ -3469,14 +3474,8 @@
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
@@ -3486,7 +3485,7 @@
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>
@@ -3505,15 +3504,22 @@
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) =
@@ -3650,8 +3656,6 @@
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
@@ -4533,15 +4537,13 @@
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>
@@ -4555,7 +4557,7 @@
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>
@@ -4570,7 +4572,7 @@
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)
@@ -4603,7 +4605,7 @@
\<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 *}
@@ -4876,7 +4878,7 @@
lemma [intro]: "tm_wf (t_utm, 0)"
apply(simp only: t_utm_def F_tprog_def)
apply(rule_tac t_compiled_correct, auto)
-done
+done
lemma UTM_halt_lemma_pre:
assumes wf_tm: "tm_wf (tp, 0)"
@@ -4894,20 +4896,17 @@
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>
@@ -4915,12 +4914,12 @@
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
@@ -5259,20 +5258,17 @@
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)"
@@ -5282,7 +5278,7 @@
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