--- 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