--- a/utm/abacus.thy Sat Sep 29 12:38:12 2012 +0000
+++ b/utm/abacus.thy Mon Oct 15 13:23:52 2012 +0000
@@ -1,5 +1,5 @@
header {*
- {\em Abacus} (a kind of register machine)
+ {\em abacus} a kind of register machine
*}
theory abacus
@@ -935,14 +935,15 @@
apply(erule_tac t_split, auto simp: tm_of.simps)
done
-subsubsection {* The compilation of @{text "Inc n"} *}
+(*
+subsection {* The compilation of @{text "Inc n"} *}
+*)
text {*
The lemmas in this section lead to the correctness of
the compilation of @{text "Inc n"} instruction.
*}
-(*****Begin: inc crsp*******)
fun at_begin_fst_bwtn :: "inc_inv_t"
where
"at_begin_fst_bwtn (as, lm) (s, l, r) ires =
@@ -2568,12 +2569,9 @@
from inc_crsp_ex_pre [OF layout corresponds inc] show ?thesis .
qed
-(*******End: inc crsp********)
-
-(*******Begin: dec crsp******)
-
-subsubsection {* The compilation of @{text "Dec n e"} *}
-
+(*
+subsection {* The compilation of @{text "Dec n e"} *}
+*)
text {*
The lemmas in this section lead to the correctness of the compilation
@@ -4834,14 +4832,10 @@
from dec_crsp_ex_pre layout dec correspond show ?thesis by blast
qed
-
-(*******End: dec crsp********)
-
-
-subsubsection {* Compilation of @{text "Goto n"}*}
-
-
-(*******Begin: goto crsp********)
+(*
+subsection {* Compilation of @{text "Goto n"}*}
+*)
+
lemma goto_fetch:
"fetch (ci (layout_of aprog)
(start_of (layout_of aprog) as) (Goto n)) (Suc 0) b
@@ -4880,9 +4874,8 @@
proof -
from goto_crsp_ex_pre and layout goto correspondence show "?thesis" by blast
qed
-(*******End : goto crsp*********)
-
-subsubsection {*
+
+subsection {*
The correctness of the compiler
*}
@@ -5158,8 +5151,7 @@
from steps_crsp_pre [OF layout compiled correspond execution] show ?thesis .
qed
-
-subsubsection {* The Mop-up machine *}
+subsection {* The Mop-up machine *}
fun mop_bef :: "nat \<Rightarrow> tprog"
where
@@ -6001,7 +5993,6 @@
apply(erule_tac x = rn in allE, simp_all)
done
-(***Begin: mopup stop***)
fun abc_mopup_stage1 :: "t_conf \<Rightarrow> nat \<Rightarrow> nat"
where
"abc_mopup_stage1 (s, l, r) n =
@@ -6107,26 +6098,6 @@
apply(rule_tac mopup_init, auto)
done
(***End: mopup stop****)
-(*
-lemma mopup_stop_cond: "mopup_inv (0, l, r) lm n ires \<Longrightarrow>
- (\<exists>ln rn. ?l = Bk\<^bsup>ln\<^esup> @ Bk # Bk # ?ires \<and> ?r = <abc_lm_v ?lm ?n> @ Bk\<^bsup>rn\<^esup>) "
- t_halt_conf (0, l, r) \<and> t_result r = Suc (abc_lm_v lm n)"
-apply(simp add: mopup_inv.simps mopup_stop.simps t_halt_conf.simps
- t_result.simps, auto simp: tape_of_nat_abv)
-apply(rule_tac x = rn in exI,
- rule_tac x = "Suc (abc_lm_v lm n)" in exI,
- simp add: tape_of_nat_abv)
-apply(simp add: tape_of_nat_abv exponent_def)
-apply(subgoal_tac "takeWhile (\<lambda>a. a = Oc)
- (replicate (abc_lm_v lm n) Oc @ replicate rn Bk)
- = replicate (abc_lm_v lm n) Oc @ takeWhile (\<lambda>a. a = Oc)
- (replicate rn Bk)", simp)
-apply(case_tac rn, simp, simp)
-apply(rule takeWhile_append2)
-apply(case_tac x, auto)
-done
-*)
-
lemma mopup_halt_conf_pre:
"\<lbrakk>n < length lm; crsp_l ly (as, lm) (s, l, r) ires\<rbrakk>
@@ -6148,24 +6119,20 @@
apply(rule_tac mopup_halt, simp, simp)
done
-thm mopup_stop.simps
-
lemma mopup_halt_conf:
assumes len: "n < length lm"
and correspond: "crsp_l ly (as, lm) (s, l, r) ires"
shows
- "\<exists> na. (\<lambda> (s', l', r'). ((\<exists>ln rn. s' = 0 \<and> l' = Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires \<and> r' = Oc\<^bsup>Suc (abc_lm_v lm n)\<^esup> @ Bk\<^bsup>rn\<^esup>)))
+ "\<exists> na. (\<lambda> (s', l', r'). ((\<exists>ln rn. s' = 0 \<and> l' = Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires
+ \<and> r' = Oc\<^bsup>Suc (abc_lm_v lm n)\<^esup> @ Bk\<^bsup>rn\<^esup>)))
(t_steps (Suc 0, l, r)
((mop_bef n @ tshift mp_up (2 * n)), 0) na)"
using len correspond mopup_halt_conf_pre[of n lm ly as s l r ires]
apply(simp add: mopup_stop.simps tape_of_nat_abv tape_of_nat_list.simps)
done
-(*********End: mop_up****************************)
-
-
-subsubsection {* Final results about Abacus machine *}
-
-thm mopup_halt
+
+subsection {* Final results about Abacus machine *}
+
lemma mopup_halt_bef: "\<lbrakk>n < length lm; crsp_l ly (as, lm) (s, l, r) ires\<rbrakk>
\<Longrightarrow> \<exists>stp. (\<lambda>(s, l, r). s \<noteq> 0 \<and> ((\<lambda> (s', l', r'). s' = 0)
(t_step (s, l, r) (mop_bef n @ tshift mp_up (2 * n), 0))))
@@ -6293,29 +6260,6 @@
apply(rule startof_not0, auto)
done
-(*
-lemma stop_conf: "mopup_inv (0, aca, bc) am n
- \<Longrightarrow> t_halt_conf (0, aca, bc) \<and> t_result bc = Suc (abc_lm_v am n)"
-apply(case_tac n,
- auto simp: mopup_inv.simps mopup_stop.simps t_halt_conf.simps
- t_result.simps tape_of_nl_abv tape_of_nat_abv )
-apply(rule_tac x = "rn" in exI,
- rule_tac x = "Suc (abc_lm_v am 0)" in exI, simp)
-apply(subgoal_tac "takeWhile (\<lambda>a. a = Oc) (Oc\<^bsup>abc_lm_v am 0\<^esup> @ Bk\<^bsup>rn\<^esup>)
- = Oc\<^bsup>abc_lm_v am 0\<^esup> @ takeWhile (\<lambda>a. a = Oc) (Bk\<^bsup>rn\<^esup>)", simp)
-apply(simp add: exponent_def, case_tac rn, simp, simp)
-apply(rule_tac takeWhile_append2, simp add: exponent_def)
-apply(rule_tac x = rn in exI,
- rule_tac x = "Suc (abc_lm_v am (Suc nat))" in exI, simp)
-apply(subgoal_tac
- "takeWhile (\<lambda>a. a = Oc) (Oc\<^bsup>abc_lm_v am (Suc nat)\<^esup> @ Bk\<^bsup>rn\<^esup>) =
- Oc\<^bsup>abc_lm_v am (Suc nat)\<^esup> @ takeWhile (\<lambda>a. a = Oc) (Bk\<^bsup>rn\<^esup>)", simp)
-apply(simp add: exponent_def, case_tac rn, simp, simp)
-apply(rule_tac takeWhile_append2, simp add: exponent_def)
-done
-*)
-
-
lemma start_of_out_range:
"as \<ge> length aprog \<Longrightarrow>
start_of (layout_of aprog) as =
@@ -6448,7 +6392,8 @@
TM @{text "(tMp n (mop_ss - 1))"} will halt and gives rise to a configuration which
only hold the content of memory cell @{text "n"}:
*}
- "\<exists> stp. (\<lambda> (s, l, r). \<exists> ln rn. s = 0 \<and> l = Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires \<and> r = Oc\<^bsup>Suc (abc_lm_v am n)\<^esup> @ Bk\<^bsup>rn\<^esup>)
+ "\<exists> stp. (\<lambda> (s, l, r). \<exists> ln rn. s = 0 \<and> l = Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires
+ \<and> r = Oc\<^bsup>Suc (abc_lm_v am n)\<^esup> @ Bk\<^bsup>rn\<^esup>)
(t_steps tc (tprog @ (tMp n (mop_ss - 1)), 0) stp)"
proof -
from layout complied correspond halt_state abc_exec rs_len mopup_start
@@ -6656,6 +6601,7 @@
apply(rule_tac abacus_turing_eq_unhalt_case_pre, auto)
done
+
definition abc_list_crsp:: "nat list \<Rightarrow> nat list \<Rightarrow> bool"
where
"abc_list_crsp xs ys = (\<exists> n. xs = ys @ 0\<^bsup>n\<^esup> \<or> ys = xs @ 0\<^bsup>n\<^esup>)"
@@ -6663,7 +6609,6 @@
apply(auto simp: abc_list_crsp_def)
done
-thm abc_lm_v.simps
lemma abc_list_crsp_lm_v:
"abc_list_crsp lma lmb \<Longrightarrow> abc_lm_v lma n = abc_lm_v lmb n"
apply(auto simp: abc_list_crsp_def abc_lm_v.simps
@@ -6748,8 +6693,6 @@
split: abc_inst.splits if_splits)
done
-thm abc_step_l.simps
-
lemma abc_steps_red:
"abc_steps_l ac aprog stp = (as, am) \<Longrightarrow>
abc_steps_l ac aprog (Suc stp) =
@@ -6799,13 +6742,10 @@
done
qed
-text {* Begin: equvilence between steps and t_steps*}
lemma [simp]: "(case ca of [] \<Rightarrow> Bk | Bk # xs \<Rightarrow> Bk | Oc # xs \<Rightarrow> Oc) =
(case ca of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x)"
by(case_tac ca, simp_all, case_tac a, simp, simp)
-text {* needed to interpret*}
-
lemma steps_eq: "length t mod 2 = 0 \<Longrightarrow>
t_steps c (t, 0) stp = steps c t stp"
apply(induct stp)
@@ -6815,8 +6755,6 @@
apply(auto simp: t_step.simps tstep.simps)
done
-text{* end: equvilence between steps and t_steps*}
-
lemma crsp_l_start: "crsp_l ly (0, lm) (Suc 0, Bk # Bk # ires, <lm> @ Bk\<^bsup>rn\<^esup>) ires"
apply(simp add: crsp_l.simps, auto simp: start_of.simps)
done
@@ -6867,7 +6805,6 @@
done
-thm tinres_steps
lemma list_length: "xs = ys \<Longrightarrow> length xs = length ys"
by simp
lemma [elim]: "tinres (Bk\<^bsup>m\<^esup>) b \<Longrightarrow> \<exists>m. b = Bk\<^bsup>m\<^esup>"
@@ -6903,6 +6840,7 @@
text {*
Main theorem for the case when the original Abacus program does halt.
*}
+
lemma abacus_turing_eq_halt:
assumes layout:
"ly = layout_of aprog"
@@ -6952,26 +6890,7 @@
(start_of ly (length aprog) - Suc 0)) mod 2 = 0")
apply(simp add: steps_eq, auto simp: isS0_def)
done
-(*
-lemma abacus_turing_eq_uhalt_pre:
- "\<lbrakk>ly = layout_of aprog;
- tprog = tm_of aprog;
- \<forall> stp. ((\<lambda> (as, am). as < length aprog)
- (abc_steps_l (0, lm) aprog stp));
- mop_ss = start_of ly (length aprog)\<rbrakk>
- \<Longrightarrow> (\<not> (\<exists> stp. isS0 (steps (Suc 0, [Bk, Bk], <lm>)
- (tprog @ (tMp n (mop_ss - 1))) stp)))"
-apply(drule_tac k = 0 and n = n in abacus_turing_eq_uhalt', auto)
-apply(erule_tac x = stp in allE, erule_tac x = stp in allE)
-apply(subgoal_tac "tinres ([Bk]) (Bk\<^bsup>k\<^esup>)")
-apply(case_tac "steps (Suc 0, Bk\<^bsup>k\<^esup>, <lm>)
- (tm_of aprog @ tMp n (start_of ly (length aprog) - Suc 0)) stp")
-apply(case_tac
- "steps (Suc 0, [Bk], <lm>)
- (tm_of aprog @ tMp n (start_of ly (length aprog) - Suc 0)) stp")
-apply(drule_tac tinres_steps, auto simp: isS0_def)
-done
-*)
+
text {*
Main theorem for the case when the original Abacus program does not halt.
*}
@@ -7000,6 +6919,5 @@
layout compiled abc_unhalt mop_start
by(auto)
-
end