diff -r 1ce04eb1c8ad -r 48b231495281 utm/abacus.thy
--- 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