
diff -r 582916f289ea -r 99a180fd4194 thys/UTM.thy
--- a/thys/UTM.thy	Mon Feb 11 00:08:54 2013 +0000
+++ b/thys/UTM.thy	Mon Feb 11 08:31:48 2013 +0000
@@ -5,17 +5,27 @@
 section {* Wang coding of input arguments *}
 
 text {*
-  The direct compilation of the universal function @{text "rec_F"} can not give us UTM, because @{text "rec_F"} is of arity 2,
-  where the first argument represents the Godel coding of the TM being simulated and the second argument represents the right number (in Wang's coding) of the TM tape. 
-  (Notice, left number is always @{text "0"} at the very beginning). However, UTM needs to simulate the execution of any TM which may
-  very well take many input arguments. Therefore, a initialization TM needs to run before the TM compiled from @{text "rec_F"}, and the sequential 
-  composition of these two TMs will give rise to the UTM we are seeking. The purpose of this initialization TM is to transform the multiple 
-  input arguments of the TM being simulated into Wang's coding, so that it can be consumed by the TM compiled from @{text "rec_F"} as the second
-  argument. 
-
-  However, this initialization TM (named @{text "t_wcode"}) can not be constructed by compiling from any resurve function, because every recursive 
-  function takes a fixed number of input arguments, while @{text "t_wcode"} needs to take varying number of arguments and tranform them into 
-  Wang's coding. Therefore, this section give a direct construction of @{text "t_wcode"} with just some parts being obtained from recursive functions.
+  The direct compilation of the universal function @{text "rec_F"} can
+  not give us UTM, because @{text "rec_F"} is of arity 2, where the
+  first argument represents the Godel coding of the TM being simulated
+  and the second argument represents the right number (in Wang's
+  coding) of the TM tape.  (Notice, left number is always @{text "0"}
+  at the very beginning). However, UTM needs to simulate the execution
+  of any TM which may very well take many input arguments. Therefore,
+  a initialization TM needs to run before the TM compiled from @{text
+  "rec_F"}, and the sequential composition of these two TMs will give
+  rise to the UTM we are seeking. The purpose of this initialization
+  TM is to transform the multiple input arguments of the TM being
+  simulated into Wang's coding, so that it can be consumed by the TM
+  compiled from @{text "rec_F"} as the second argument.
+
+  However, this initialization TM (named @{text "t_wcode"}) can not be
+  constructed by compiling from any resurve function, because every
+  recursive function takes a fixed number of input arguments, while
+  @{text "t_wcode"} needs to take varying number of arguments and
+  tranform them into Wang's coding. Therefore, this section give a
+  direct construction of @{text "t_wcode"} with just some parts being
+  obtained from recursive functions.
 
 \newlength{\basewidth}
 \settowidth{\basewidth}{xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx}
@@ -71,10 +81,22 @@
 \caption{The output of TM $prepare$} \label{prepare_output}
 \end{figure}
 
-As shown in Figure \ref{prepare_input}, the input of $prepare$ is the same as the the input
-of UTM, where $m$ is the Godel coding of the TM being interpreted and $a_1$ through $a_n$ are the $n$ input arguments of the TM under interpretation. The purpose of $purpose$ is to transform this initial tape layout to the one shown in Figure \ref{prepare_output},
-which is convenient for the generation of Wang's codding of $a_1, \ldots, a_n$. The coding procedure starts from $a_n$ and ends after $a_1$ is encoded. The coding result is stored in an accumulator at the end of the tape (initially represented by the $1$ two blanks right to $a_n$ in Figure \ref{prepare_output}). In Figure \ref{prepare_output}, arguments $a_1, \ldots, a_n$ are separated by two blanks on both ends with the rest so that movement conditions can be implemented conveniently in subsequent TMs, because, by convention,
-two consecutive blanks are usually used to signal the end or start of a large chunk of data. The diagram of $prepare$ is given in Figure \ref{prepare_diag}.
+As shown in Figure \ref{prepare_input}, the input of $prepare$ is the
+same as the the input of UTM, where $m$ is the Godel coding of the TM
+being interpreted and $a_1$ through $a_n$ are the $n$ input arguments
+of the TM under interpretation. The purpose of $purpose$ is to
+transform this initial tape layout to the one shown in Figure
+\ref{prepare_output}, which is convenient for the generation of Wang's
+codding of $a_1, \ldots, a_n$. The coding procedure starts from $a_n$
+and ends after $a_1$ is encoded. The coding result is stored in an
+accumulator at the end of the tape (initially represented by the $1$
+two blanks right to $a_n$ in Figure \ref{prepare_output}). In Figure
+\ref{prepare_output}, arguments $a_1, \ldots, a_n$ are separated by
+two blanks on both ends with the rest so that movement conditions can
+be implemented conveniently in subsequent TMs, because, by convention,
+two consecutive blanks are usually used to signal the end or start of
+a large chunk of data. The diagram of $prepare$ is given in Figure
+\ref{prepare_diag}.
 
 
 \begin{figure}[h!]
@@ -840,7 +862,6 @@
 
 lemma wf_wcode_double_case_le[intro]: "wf wcode_double_case_le"
 by(auto intro:wf_inv_image simp: wcode_double_case_le_def )
-term fetch
 
 lemma [simp]: "fetch t_wcode_main (Suc 0) Bk = (L, Suc 0)"
 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def
@@ -1326,7 +1347,7 @@
         (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'))"
-    thm before_final using exec
+    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'))" ..
@@ -1377,7 +1398,6 @@
   hence "\<exists> stp. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
     (adjust 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))"
-    thm adjust_halt_eq
     apply(rule_tac stp = stp in adjust_halt_eq)
     apply(simp add: t_twice_compile_def, auto)
     done
@@ -3310,15 +3330,6 @@
 apply(simp add:tm_wf.simps t_wcode_prepare_def)
 done
    
-(* 
-lemma t_correct_termi: "t_correct tp \<Longrightarrow> 
-      list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (change_termi_state tp)"
-apply(auto simp: t_correct.simps List.list_all_length)
-apply(erule_tac x = n in allE, simp)
-apply(case_tac "tp!n", auto simp: change_termi_state.simps split: if_splits)
-done
-*)
-
 lemma t_correct_shift:
          "list_all (\<lambda>(acn, st). (st \<le> y)) tp \<Longrightarrow>
           list_all (\<lambda>(acn, st). (st \<le> y + off)) (shift tp off) "
@@ -3326,20 +3337,6 @@
 apply(erule_tac x = n in allE, simp add: length_shift)
 apply(case_tac "tp!n", auto simp: shift.simps)
 done
-(*
-lemma [intro]: 
-  "t_correct (tm_of abc_twice @ tMp (Suc 0) 
-        (start_of twice_ly (length abc_twice) - Suc 0))"
-apply(rule_tac t_compiled_correct, simp_all)
-apply(simp add: twice_ly_def)
-done
-
-lemma [intro]: "t_correct (tm_of abc_fourtimes @ tMp (Suc 0) 
-   (start_of fourtimes_ly (length abc_fourtimes) - Suc 0))"
-apply(rule_tac t_compiled_correct, simp_all)
-apply(simp add: fourtimes_ly_def)
-done
-*)
 
 lemma [intro]: "(28 + (length t_twice_compile + length t_fourtimes_compile)) mod 2 = 0"
 apply(auto simp: t_twice_compile_def t_fourtimes_compile_def)
@@ -3664,7 +3661,6 @@
 apply(simp only: fetch.simps t_wcode_adjust_def nth_of.simps numeral_5_eq_5, auto)
 done
 
-thm numeral_6_eq_6
 lemma [simp]: "fetch t_wcode_adjust 6 Oc = (R, 7)"
 apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_6_eq_6)
 done
@@ -4665,112 +4661,6 @@
   where
   "UTM_pre = t_wcode |+| t_utm"
 
-(*
-lemma F_abc_halt_eq:
-  "\<lbrakk>Turing.t_correct tp; 
-    length lm = k;
-    steps (Suc 0, Bk\<up>(l), <lm>) tp stp = (0, Bk\<up>(m), Oc\<up>(rs)@Bk\<up>(n));
-    rs > 0\<rbrakk>
-    \<Longrightarrow> \<exists> stp m. abc_steps_l (0, [code tp, bl2wc (<lm>)]) (F_aprog) stp =
-                       (length (F_aprog), code tp # bl2wc (<lm>) # (rs - 1) # 0\<up>(m))"
-apply(drule_tac  F_t_halt_eq, simp, simp, simp)
-apply(case_tac "rec_ci rec_F")
-apply(frule_tac abc_append_dummy_complie, simp, simp, erule_tac exE,
-      erule_tac exE)
-apply(rule_tac x = stp in exI, rule_tac x = m in exI)
-apply(simp add: F_aprog_def dummy_abc_def)
-done
-
-lemma F_abc_utm_halt_eq: 
-  "\<lbrakk>rs > 0; 
-  abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog stp =
-        (length F_aprog, code tp #  bl2wc (<lm>) # (rs - 1) # 0\<up>(m))\<rbrakk>
-  \<Longrightarrow> \<exists>stp m n.(steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp =
-                                             (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n)))"
-  thm abacus_turing_eq_halt
-  using abacus_turing_eq_halt
-  [of "layout_of F_aprog" "F_aprog" "F_tprog" "length (F_aprog)" 
-    "[code tp, bl2wc (<lm>)]" stp "code tp # bl2wc (<lm>) # (rs - 1) # 0\<up>(m)" "Suc (Suc 0)"
-    "start_of (layout_of (F_aprog)) (length (F_aprog))" "[]" 0]
-apply(simp add: F_tprog_def t_utm_def abc_lm_v.simps nth_append)
-apply(erule_tac exE)+
-apply(rule_tac x = stpa in exI, rule_tac x = "Suc (Suc ma)" in exI, 
-       rule_tac x = l in exI, simp add: exp_ind)
-done
-
-declare tape_of_nl_abv_cons[simp del]
-
-lemma t_utm_halt_eq': 
-  "\<lbrakk>Turing.t_correct tp;
-   0 < rs;
-  steps (Suc 0, Bk\<up>(l), <lm::nat list>) tp stp = (0, Bk\<up>(m), Oc\<up>(rs)@Bk\<up>(n))\<rbrakk>
-  \<Longrightarrow>  \<exists>stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp = 
-                                                (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))"
-apply(drule_tac  l = l in F_abc_halt_eq, simp, simp, simp)
-apply(erule_tac exE, erule_tac exE)
-apply(rule_tac F_abc_utm_halt_eq, simp_all)
-done
-*)
-(*
-lemma [simp]: "tinres xs (xs @ Bk\<up>(i))"
-apply(auto simp: tinres_def)
-done
-
-lemma [elim]: "\<lbrakk>rs > 0; Oc\<up>(rs) @ Bk\<up>(na) = c @ Bk\<up>(n)\<rbrakk>
-        \<Longrightarrow> \<exists>n. c = Oc\<up>(rs) @ Bk\<up>(n)"
-apply(case_tac "na > n")
-apply(subgoal_tac "\<exists> d. na = d + n", auto simp: exp_add)
-apply(rule_tac x = "na - n" in exI, simp)
-apply(subgoal_tac "\<exists> d. n = d + na", auto simp: exp_add)
-apply(case_tac rs, simp_all add: exp_ind, case_tac d, 
-           simp_all add: exp_ind)
-apply(rule_tac x = "n - na" in exI, simp)
-done
-*)
-(*
-lemma t_utm_halt_eq'': 
-  "\<lbrakk>Turing.t_correct tp;
-   0 < rs;
-   steps (Suc 0, Bk\<up>(l), <lm::nat list>) tp stp = (0, Bk\<up>(m), Oc\<up>(rs)@Bk\<up>(n))\<rbrakk>
-  \<Longrightarrow>  \<exists>stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stp = 
-                                                (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))"
-apply(drule_tac t_utm_halt_eq', simp_all)
-apply(erule_tac exE)+
-proof -
-  fix stpa ma na
-  assume "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stpa = (0, Bk\<up>(ma), Oc\<up>(rs) @ Bk\<up>(na))"
-  and gr: "rs > 0"
-  thus "\<exists>stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stp = (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))"
-    apply(rule_tac x = stpa in exI, rule_tac x = ma in exI,  simp)
-  proof(case_tac "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stpa", simp)
-    fix a b c
-    assume "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stpa = (0, Bk\<up>(ma), Oc\<up>(rs) @ Bk\<up>(na))"
-            "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stpa = (a, b, c)"
-    thus " a = 0 \<and> b = Bk\<up>(ma) \<and> (\<exists>n. c = Oc\<up>(rs) @ Bk\<up>(n))"
-      using tinres_steps2[of "<[code tp, bl2wc (<lm>)]>" "<[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)" 
-                           "Suc 0" " [Bk, Bk]" t_utm stpa 0 "Bk\<up>(ma)" "Oc\<up>(rs) @ Bk\<up>(na)" a b c]
-      apply(simp)
-      using gr
-      apply(simp only: tinres_def, auto)
-      apply(rule_tac x = "na + n" in exI, simp add: exp_add)
-      done
-  qed
-qed
-
-lemma [simp]: "tinres [Bk, Bk] [Bk]"
-apply(auto simp: tinres_def)
-done
-
-lemma [elim]: "Bk\<up>(ma) = b @ Bk\<up>(n)  \<Longrightarrow> \<exists>m. b = Bk\<up>(m)"
-apply(subgoal_tac "ma = length b + n")
-apply(rule_tac x = "ma - n" in exI, simp add: exp_add)
-apply(drule_tac length_equal)
-apply(simp)
-done
-*)
-
-
-
 lemma tinres_step1: 
   "\<lbrakk>tinres l l'; step (ss, l, r) (t, 0) = (sa, la, ra); 
                  step (ss, l', r) (t, 0) = (sb, lb, rb)\<rbrakk>
@@ -5083,15 +4973,6 @@
 apply(rule_tac nonstop_t_uhalt_eq, simp_all)
 done
 
-(*
-lemma [simp]: 
-  "\<forall>j<Suc k. Ex (rec_calc_rel (get_fstn_args (Suc k) (Suc k) ! j)
-                                                     (code tp # lm))"
-apply(auto simp: get_fstn_args_nth)
-apply(rule_tac x = "(code tp # lm) ! j" in exI)
-apply(rule_tac calc_id, simp_all)
-done
-*)
 declare ci_cn_para_eq[simp]
 
 lemma F_aprog_uhalt: 
@@ -5180,7 +5061,6 @@
   \<Longrightarrow> \<forall> stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog 
        stp of (ss, e) \<Rightarrow> ss < length F_aprog"
 apply(case_tac "rec_ci rec_F", simp add: F_aprog_def)
-thm uabc_uhalt'
 apply(drule_tac ap = a and pos = b and md = c in uabc_uhalt', simp_all)
 proof -
   fix a b c




