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 "\ stp. \ is_final (steps0 (1, l, r) ap stp) \ (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: "\ is_final (steps0 (1, l, r) ap stpa) \ (steps0 (1, l, r) ap (Suc stpa) = (0, l', r'))" .. @@ -1377,7 +1398,6 @@ hence "\ stp. steps0 (Suc 0, Bk # Bk # ires, Oc\(Suc rs) @ Bk\(n)) (adjust t_twice_compile) stp = (Suc (length t_twice_compile div 2), Bk\(ln) @ Bk # Bk # ires, Oc\(Suc (2 * rs)) @ Bk\(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 \ - list_all (\(acn, st). (st \ 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 (\(acn, st). (st \ y)) tp \ list_all (\(acn, st). (st \ 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: - "\Turing.t_correct tp; - length lm = k; - steps (Suc 0, Bk\(l), ) tp stp = (0, Bk\(m), Oc\(rs)@Bk\(n)); - rs > 0\ - \ \ stp m. abc_steps_l (0, [code tp, bl2wc ()]) (F_aprog) stp = - (length (F_aprog), code tp # bl2wc () # (rs - 1) # 0\(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: - "\rs > 0; - abc_steps_l (0, [code tp, bl2wc ()]) F_aprog stp = - (length F_aprog, code tp # bl2wc () # (rs - 1) # 0\(m))\ - \ \stp m n.(steps (Suc 0, [Bk, Bk], <[code tp, bl2wc ()]>) t_utm stp = - (0, Bk\(m), Oc\(rs) @ Bk\(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 ()]" stp "code tp # bl2wc () # (rs - 1) # 0\(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': - "\Turing.t_correct tp; - 0 < rs; - steps (Suc 0, Bk\(l), ) tp stp = (0, Bk\(m), Oc\(rs)@Bk\(n))\ - \ \stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc ()]>) t_utm stp = - (0, Bk\(m), Oc\(rs) @ Bk\(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\(i))" -apply(auto simp: tinres_def) -done - -lemma [elim]: "\rs > 0; Oc\(rs) @ Bk\(na) = c @ Bk\(n)\ - \ \n. c = Oc\(rs) @ Bk\(n)" -apply(case_tac "na > n") -apply(subgoal_tac "\ d. na = d + n", auto simp: exp_add) -apply(rule_tac x = "na - n" in exI, simp) -apply(subgoal_tac "\ 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'': - "\Turing.t_correct tp; - 0 < rs; - steps (Suc 0, Bk\(l), ) tp stp = (0, Bk\(m), Oc\(rs)@Bk\(n))\ - \ \stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc ()]> @ Bk\(i)) t_utm stp = - (0, Bk\(m), Oc\(rs) @ Bk\(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 ()]>) t_utm stpa = (0, Bk\(ma), Oc\(rs) @ Bk\(na))" - and gr: "rs > 0" - thus "\stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc ()]> @ Bk\(i)) t_utm stp = (0, Bk\(m), Oc\(rs) @ Bk\(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 ()]> @ Bk\(i)) t_utm stpa", simp) - fix a b c - assume "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc ()]>) t_utm stpa = (0, Bk\(ma), Oc\(rs) @ Bk\(na))" - "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc ()]> @ Bk\(i)) t_utm stpa = (a, b, c)" - thus " a = 0 \ b = Bk\(ma) \ (\n. c = Oc\(rs) @ Bk\(n))" - using tinres_steps2[of "<[code tp, bl2wc ()]>" "<[code tp, bl2wc ()]> @ Bk\(i)" - "Suc 0" " [Bk, Bk]" t_utm stpa 0 "Bk\(ma)" "Oc\(rs) @ Bk\(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\(ma) = b @ Bk\(n) \ \m. b = Bk\(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: "\tinres l l'; step (ss, l, r) (t, 0) = (sa, la, ra); step (ss, l', r) (t, 0) = (sb, lb, rb)\ @@ -5083,15 +4973,6 @@ apply(rule_tac nonstop_t_uhalt_eq, simp_all) done -(* -lemma [simp]: - "\j \ stp. case abc_steps_l (0, [code tp, bl2wc ()]) F_aprog stp of (ss, e) \ 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