text‹
this section we define a representation of natural numbers and some reusable
machines for elementary arithmetical operations. All Turing machines
the operations assume that the tape heads on the tapes containing
operands and the result(s) contain one natural number each. In programming
terms we could say that such a tape corresponds to a variable of type
{typ nat}. Furthermore, initially the tape heads are on cell number~1, that is,
to the right of the start symbol. The Turing machines will halt with the
heads in that position as well. In that way operations can be concatenated
. ›
text‹
represent binary numbers as sequences of the symbols \textbf{0} and
textbf{1}. Slightly unusually the least significant bit will be on the left.
every sequence over these symbols represents a natural number, the
is not unique due to leading (or rather, trailing) zeros. The
emph{canonical} representation is unique and has no trailing zeros, not even for
number zero, which is thus represented by the empty symbol sequence. As a
effect empty tapes can be thought of as being initialized with zero.
the binary digits 0 and 1 are represented by the symbols \textbf{0} \textbf{1}, respectively. For example, the decimal number $14$,
written $1100_2$ in binary, is represented by the symbol sequence
textbf{0011}. The next two functions map between symbols and binary digits: ›
abbreviation (input) tosym :: "nat ==> symbol"where "tosym z ≡ z + 2"
abbreviation todigit :: "symbol ==> nat"where "todigit z ≡ if z = 1 then 1 else 0"
text‹
numerical value of a symbol sequence: ›
definition num :: "symbol list ==> nat"where "num xs ≡∑i←[0..<length xs]. todigit (xs ! i) * 2 ^ i"
text‹
$i$-th digit of a symbol sequence, where digits out of bounds are considered
zeros: ›
definition digit :: "symbol list ==> nat ==> nat"where "digit xs i ≡ if i < length xs then xs ! i else 0"
text‹
properties of $num$: ›
lemma num_ge_pow: assumes"i < length xs"and"xs ! i = 1" shows"num xs ≥ 2 ^ i" proof - let ?ys = "map (λi. todigit (xs ! i) * 2 ^ i) [0..<length xs]" have"?ys ! i = 2 ^ i" using assms by simp moreoverhave"i < length ?ys" using assms(1) by simp ultimatelyshow"num xs ≥ 2 ^ i" unfolding num_def using elem_le_sum_list by (metis (no_types, lifting)) qed
lemma num_trailing_zero: assumes"todigit z = 0" shows"num xs = num (xs @ [z])" proof - let ?xs = "xs @ [z]" let ?ys = "map (λi. todigit (?xs ! i) * 2 ^ i) [0..<length ?xs]" have *: "?ys = map (λi. todigit (xs ! i) * 2 ^ i) [0..<length xs] @ [0]" using assms by (simp add: nth_append) have"num ?xs = sum_list ?ys" using num_def by simp thenhave"num ?xs = sum_list (map (λi. todigit (xs ! i) * 2 ^ i) [0..<length xs] @ [0])" using * by metis thenhave"num ?xs = sum_list (map (λi. todigit (xs ! i) * 2 ^ i) [0..<length xs])" by simp thenshow ?thesis using num_def by simp qed
have"map (λi. f i) [1..<Suc m] = map (λi. f (Suc i)) [0..<m]"for f :: "nat ==> nat"and m proof (rule nth_equalityI) show"length (map f [1..<Suc m]) = length (map (λi. f (Suc i)) [0..<m])" by simp thenshow"∧i. i < length (map f [1..<Suc m]) ==> map f [1..<Suc m] ! i = map (λi. f (Suc i)) [0..<m] ! i" by (metis add.left_neutral length_map length_upt nth_map_upt plus_1_eq_Suc) qed thenhave2: "(∑i←[1..<Suc m]. f i) = (∑i←[0..<m]. f (Suc i))" for f :: "nat ==> nat"and m by simp
lemma num_append: "num (xs @ ys) = num xs + 2 ^ length xs * num ys" proof (induction"length xs" arbitrary: xs) case0 thenshow ?case using num_def by simp next case (Suc n) thenhave xs: "xs = hd xs # tl xs" by (metis hd_Cons_tl list.size(3) nat.simps(3)) thenhave"xs @ ys = hd xs # (tl xs @ ys)" by simp thenhave"num (xs @ ys) = todigit (hd xs) + 2 * num (tl xs @ ys)" using num_Cons by presburger alsohave"... = todigit (hd xs) + 2 * (num (tl xs) + 2 ^ length (tl xs) * num ys)" using Suc by simp alsohave"... = todigit (hd xs) + 2 * num (tl xs) + 2 ^ Suc (length (tl xs)) * num ys" by simp alsohave"... = num xs + 2 ^ Suc (length (tl xs)) * num ys" using num_Cons xs by metis alsohave"... = num xs + 2 ^ length xs * num ys" using xs by (metis length_Cons) finallyshow ?case . qed
lemma num_drop: "num (drop t zs) = todigit (digit zs t) + 2 * num (drop (Suc t) zs)" proof (cases "t < length zs") case True thenhave"drop t zs = zs ! t # drop (Suc t) zs" by (simp add: Cons_nth_drop_Suc) thenhave"num (drop t zs) = todigit (zs ! t) + 2 * num (drop (Suc t) zs)" using num_Cons by simp thenshow ?thesis using digit_def True by simp next case False thenshow ?thesis using digit_def num_def by simp qed
lemma num_take_Suc: "num (take (Suc t) zs) = num (take t zs) + 2 ^ t * todigit (digit zs t)" proof (cases "t < length zs") case True let ?zs = "take (Suc t) zs" have1: "?zs ! i = zs ! i"if"i < Suc t"for i using that by simp have2: "take t zs ! i = zs ! i"if"i < t"for i using that by simp have"num ?zs = (∑i←[0..<length ?zs]. todigit (?zs ! i) * 2 ^ i)" using num_def by simp alsohave"... = (∑i←[0..<Suc t]. todigit (?zs ! i) * 2 ^ i)" by (simp add: Suc_leI True min_absorb2) alsohave"... = (∑i←[0..<Suc t]. todigit (zs ! i) * 2 ^ i)" using1by (smt (verit, best) atLeastLessThan_iff map_eq_conv set_upt) alsohave"... = (∑i←[0..<t]. todigit (zs ! i) * 2 ^ i) + todigit (zs ! t) * 2 ^ t" by simp alsohave"... = (∑i←[0..<t]. todigit (take t zs ! i) * 2 ^ i) + todigit (zs ! t) * 2 ^ t" using2by (metis (no_types, lifting) atLeastLessThan_iff map_eq_conv set_upt) alsohave"... = num (take t zs) + todigit (zs ! t) * 2 ^ t" using num_def True by simp alsohave"... = num (take t zs) + todigit (digit zs t) * 2 ^ t" using digit_def True by simp finallyshow ?thesis by simp next case False thenshow ?thesis using digit_def by simp qed
text‹
symbol sequence is a canonical representation of a natural number if the
contains only the symbols \textbf{0} and \textbf{1} and is either empty
ends in \textbf{1}. ›
lemma canonical_Cons: assumes"canonical xs"and"xs ≠ []"and"x = 0∨ x = 1" shows"canonical (x # xs)" using assms canonical_def less_Suc_eq_0_disj by auto
lemma canonical_Cons_3: "canonical xs ==> canonical (1 # xs)" using canonical_def less_Suc_eq_0_disj by auto
lemma canonical_tl: "canonical (x # xs) ==> canonical xs" using canonical_def by fastforce
lemma prepend_2_even: "x = 0==> even (num (x # xs))" using num_Cons by simp
lemma prepend_3_odd: "x = 1==> odd (num (x # xs))" using num_Cons by simp
text‹
number has exactly one canonical representation. ›
lemma canonical_ex1: fixes n :: nat shows"∃!xs. num xs = n ∧ canonical xs" proof (induction n rule: nat_less_induct) case IH: (1 n) show ?case proof (cases "n = 0") case True have"num [] = 0" using num_def by simp moreoverhave"canonical xs ==> num xs = 0 ==> xs = []"for xs proof (rule ccontr) fix xs assume"canonical xs""num xs = 0""xs ≠ []" thenhave"length xs > 0""last xs = 1" using canonical_def by simp_all thenhave"xs ! (length xs - 1) = 1" by (metis Suc_diff_1 last_length) thenhave"num xs ≥ 2 ^ (length xs - 1)" using num_ge_pow by (meson ‹0 < length xs› diff_less zero_less_one) thenhave"num xs > 0" by (meson dual_order.strict_trans1 le0 le_less_trans less_exp) thenshow False using‹num xs = 0›by auto qed ultimatelyshow ?thesis using IH True canonical_def by (metis less_nat_zero_code list.size(3)) next case False thenhave gt: "n > 0" by simp define m where"m = n div 2" define r where"r = n mod 2" have n: "n = 2 * m + r" using m_def r_def by simp have"m < n" using gt m_def by simp thenobtain xs where"num xs = m""canonical xs" using IH by auto thenhave"num (tosym r # xs) = n"
(is"num ?xs = n") using num_Cons n add.commute r_def by simp have"canonical ?xs" proof (cases "r = 0") case True thenhave"m > 0" using gt n by simp thenhave"xs ≠ []" using `num xs = m` num_def by auto thenshow ?thesis using canonical_Cons[of xs] `canonical xs` r_def True by simp next case False thenshow ?thesis using `canonical xs` canonical_Cons_3 r_def by (metis One_nat_def not_mod_2_eq_1_eq_0 numeral_3_eq_3 one_add_one plus_1_eq_Suc) qed moreoverhave"xs1 = xs2"if"canonical xs1""num xs1 = n""canonical xs2""num xs2 = n"for xs1 xs2 proof - have"xs1 ≠ []" using gt that(2) num_def by auto thenobtain x1 ys1 where1: "xs1 = x1 # ys1" by (meson neq_Nil_conv) thenhave x1: "x1 = 0∨ x1 = 1" using canonical_def that(1) by auto have"xs2 ≠ []" using gt that(4) num_def by auto thenobtain x2 ys2 where2: "xs2 = x2 # ys2" by (meson neq_Nil_conv) thenhave x2: "x2 = 0∨ x2 = 1" using canonical_def that(3) by auto have"x1 = x2" using prepend_2_even prepend_3_odd that 12 x1 x2 by metis moreoverhave"n = todigit x1 + 2 * num ys1" using that(2) num_Cons 1by simp moreoverhave"n = todigit x2 + 2 * num ys2" using that(4) num_Cons 2by simp ultimatelyhave"num ys1 = num ys2" by simp moreoverhave"num ys1 < n" using that(2) num_Cons 1 gt by simp moreoverhave"num ys2 < n" using that(4) num_Cons 2 gt by simp ultimatelyhave"ys1 = ys2" using IH 12 that(1,3) by (metis canonical_tl) thenshow"xs1 = xs2" using `x1 = x2` 12by simp qed ultimatelyshow ?thesis using‹num (tosym r # xs) = n›by auto qed qed
text‹
canonical representation of a natural number as symbol sequence: ›
definition canrepr :: "nat ==> symbol list"where "canrepr n ≡ THE xs. num xs = n ∧ canonical xs"
lemma canrepr_inj: "inj canrepr" using canrepr_def canonical_ex1 by (smt (verit, del_insts) inj_def the_equality)
lemma canonical_canrepr: "canonical (canrepr n)" using theI'[OF canonical_ex1] canrepr_def by simp
lemma canrepr: "num (canrepr n) = n" using theI'[OF canonical_ex1] canrepr_def by simp
lemma bit_symbols_canrepr: "bit_symbols (canrepr n)" using canonical_canrepr canonical_def by simp
lemma proper_symbols_canrepr: "proper_symbols (canrepr n)" using bit_symbols_canrepr by fastforce
lemma canreprI: "num xs = n ==> canonical xs ==> canrepr n = xs" using canrepr canonical_canrepr canonical_ex1 by blast
lemma canrepr_0: "canrepr 0 = []" using num_def canonical_def by (intro canreprI) simp_all
lemma canrepr_1: "canrepr 1 = [1]" using num_def canonical_def by (intro canreprI) simp_all
text‹
length of the canonical representation of a number $n$: ›
lemma nlength_0: "nlength n = 0 ⟷ n = 0" by (metis canrepr canrepr_0 length_0_conv)
corollary nlength_0_simp [simp]: "nlength 0 = 0" using nlength_0 by simp
lemma num_replicate2_eq_pow: "num (replicate j 0 @ [1]) = 2 ^ j" proof (induction j) case0 thenshow ?case using num_def by simp next case (Suc j) thenshow ?case using num_Cons by simp qed
lemma num_replicate3_eq_pow_minus_1: "num (replicate j 1) = 2 ^ j - 1" proof (induction j) case0 thenshow ?case using num_def by simp next case (Suc j) thenhave"num (replicate (Suc j) 1) = num (1 # replicate j 1)" by simp alsohave"... = 1 + 2 * (2 ^ j - 1)" using Suc num_Cons by simp alsohave"... = 1 + 2 * 2 ^ j - 2" by (metis Nat.add_diff_assoc diff_mult_distrib2 mult_2 mult_le_mono2 nat_1_add_1 one_le_numeral one_le_power) alsohave"... = 2 ^ Suc j - 1" by simp finallyshow ?case . qed
lemma nlength_pow2: "nlength (2 ^ j) = Suc j" proof - define xs :: "nat list"where"xs = replicate j 2 @ [3]" thenhave"length xs = Suc j" by simp moreoverhave"num xs = 2 ^ j" using num_replicate2_eq_pow xs_def by simp moreoverhave"canonical xs" using xs_def bit_symbols_append canonical_def by simp ultimatelyshow ?thesis using canreprI by blast qed
corollary nlength_1_simp [simp]: "nlength 1 = 1" using nlength_pow2[of 0] by simp
corollary nlength_2: "nlength 2 = 2" using nlength_pow2[of 1] by simp
lemma nlength_pow_minus_1: "nlength (2 ^ j - 1) = j" proof - define xs :: "nat list"where"xs = replicate j 1" thenhave"length xs = j" by simp moreoverhave"num xs = 2 ^ j - 1" using num_replicate3_eq_pow_minus_1 xs_def by simp moreoverhave"canonical xs" proof - have"bit_symbols xs" using xs_def by simp moreoverhave"last xs = 3 ∨ xs = []" by (cases "j = 0") (simp_all add: xs_def) ultimatelyshow ?thesis using canonical_def by auto qed ultimatelyshow ?thesis using canreprI by metis qed
corollary nlength_3: "nlength 3 = 2" using nlength_pow_minus_1[of 2] by simp
text‹
handling natural numbers, Turing machines will usually have tape contents
the following form: ›
lemma ncontents_0: "⌊0⌋N = ⌊[]⌋" by (simp add: canrepr_0)
lemma clean_tape_ncontents: "clean_tape (⌊x⌋N, i)" using bit_symbols_canrepr clean_contents_proper by fastforce
lemma ncontents_1_blank_iff_zero: "⌊n⌋N 1 = ◻⟷ n = 0" using bit_symbols_canrepr contents_def nlength_0 by (metis contents_outofbounds diff_is_0_eq' leI length_0_conv length_greater_0_conv less_one zero_neq_numeral)
text‹
bit symbol sequence can be turned into a canonical representation of some
by stripping trailing zeros. The length of the prefix without trailing
is given by the next function: ›
definition canlen :: "symbol list ==> nat"where "canlen zs ≡ LEAST m. ∀i<length zs. i ≥ m ⟶ zs ! i = 0"
lemma canlen_at_ge: "∀i<length zs. i ≥ canlen zs ⟶ zs ! i = 0" proof - let ?P = "λm. ∀i<length zs. i ≥ m ⟶ zs ! i = 0" have"?P (length zs)" by simp thenshow ?thesis unfolding canlen_def using LeastI[of ?P "length zs"] by fast qed
lemma canlen_eqI: assumes"∀i<length zs. i ≥ m ⟶ zs ! i = 0" and"∧y. ∀i<length zs. i ≥ y ⟶ zs ! i = 0==> m ≤ y" shows"canlen zs = m" unfolding canlen_def using assms Least_equality[of _ m, OF _ assms(2)] by presburger
lemma canlen_le_length: "canlen zs ≤ length zs" proof - let ?P = "λm. ∀i<length zs. i ≥ m ⟶ zs ! i = 0" have"?P (length zs)" by simp thenshow ?thesis unfolding canlen_def using Least_le[of _ "length zs"] by simp qed
lemma canlen_le: assumes"∀i<length zs. i ≥ m ⟶ zs ! i = 0" shows"m ≥ canlen zs" unfolding canlen_def using Least_le[of _ m] assms by simp
lemma canlen_one: assumes"bit_symbols zs"and"canlen zs > 0" shows"zs ! (canlen zs - 1) = 1" proof (rule ccontr) assume"zs ! (canlen zs - 1) ≠1" thenhave"zs ! (canlen zs - 1) = 0" using assms canlen_le_length by (metis One_nat_def Suc_pred lessI less_le_trans) thenhave"∀i<length zs. i ≥ canlen zs - 1 ⟶ zs ! i = 2" using canlen_at_ge assms(2) by (metis One_nat_def Suc_leI Suc_pred le_eq_less_or_eq) thenhave"canlen zs - 1 ≥ canlen zs" using canlen_le by auto thenshow False using assms(2) by simp qed
lemma canonical_take_canlen: assumes"bit_symbols zs" shows"canonical (take (canlen zs) zs)" proof (cases "canlen zs = 0") case True thenshow ?thesis using canonical_def by simp next case False thenshow ?thesis using canonical_def assms canlen_le_length canlen_one by (smt (verit, ccfv_SIG) One_nat_def Suc_pred append_take_drop_id diff_less last_length
length_take less_le_trans min_absorb2 neq0_conv nth_append zero_less_one) qed
lemma num_take_canlen_eq: "num (take (canlen zs) zs) = num zs" proof (induction"length zs - canlen zs" arbitrary: zs) case0 thenshow ?case by simp next case (Suc x) let ?m = "canlen zs" have *: "∀i<length zs. i ≥ ?m ⟶ zs ! i = 0" using canlen_at_ge by auto have"canlen zs < length zs" using Suc by simp thenhave"zs ! (length zs - 1) = 0" using Suc canlen_at_ge canlen_le_length by (metis One_nat_def Suc_pred diff_less le_Suc_eq less_nat_zero_code nat_neq_iff zero_less_one) thenhave"todigit (zs ! (length zs - 1)) = 0" by simp moreoverhave ys: "zs = take (length zs - 1) zs @ [zs ! (length zs - 1)]"
(is"zs = ?ys @ _") by (metis Suc_diff_1 ‹canlen zs < length zs› append_butlast_last_id butlast_conv_take
gr_implies_not0 last_length length_0_conv length_greater_0_conv) ultimatelyhave"num ?ys = num zs" using num_trailing_zero by metis have canlen_ys: "canlen ?ys = canlen zs" proof (rule canlen_eqI) show"∀i<length ?ys. canlen zs ≤ i ⟶ ?ys ! i = 0" by (simp add: canlen_at_ge) show"∧y. ∀i<length ?ys. y ≤ i ⟶ ?ys ! i = 0==> canlen zs ≤ y" using * Suc.hyps(2) canlen_le by (smt (verit, del_insts) One_nat_def Suc_pred append_take_drop_id diff_le_self length_take
length_upt less_Suc_eq less_nat_zero_code list.size(3) min_absorb2 nth_append upt.simps(2) zero_less_Suc) qed thenhave"length ?ys - canlen ?ys = x" using ys Suc.hyps(2) by (metis butlast_snoc diff_Suc_1 diff_commute length_butlast) thenhave"num (take (canlen ?ys) ?ys) = num ?ys" using Suc by blast thenhave"num (take (canlen zs) ?ys) = num ?ys" using canlen_ys by simp thenhave"num (take (canlen zs) zs) = num ?ys" by (metis ‹canlen zs < length zs› butlast_snoc take_butlast ys) thenshow ?case using‹num ?ys = num zs›by presburger qed
lemma canrepr_take_canlen: assumes"num zs = n"and"bit_symbols zs" shows"canrepr n = take (canlen zs) zs" using assms canrepr canonical_canrepr canonical_ex1 canonical_take_canlen num_take_canlen_eq by blast
lemma length_canrepr_canlen: assumes"num zs = n"and"bit_symbols zs" shows"nlength n = canlen zs" using canrepr_take_canlen assms canlen_le_length by (metis length_take min_absorb2)
lemma nlength_ge_pow: assumes"nlength n = Suc j" shows"n ≥ 2 ^ j" proof - let ?xs = "canrepr n" have"?xs ! (length ?xs - 1) = 1" using canonical_def assms canonical_canrepr by (metis Suc_neq_Zero diff_Suc_1 last_length length_0_conv) moreoverhave"(∑i←[0..<length ?xs]. todigit (?xs ! i) * 2 ^ i) ≥ todigit (?xs ! (length ?xs - 1)) * 2 ^ (length ?xs - 1)" using assms by simp ultimatelyhave"num ?xs ≥ 2 ^ (length ?xs - 1)" using num_def by simp moreoverhave"num ?xs = n" using canrepr by simp ultimatelyshow ?thesis using assms by simp qed
lemma nlength_less_pow: "n < 2 ^ (nlength n)" proof (induction"nlength n" arbitrary: n) case0 thenshow ?case by (metis canrepr canrepr_0 length_0_conv nat_zero_less_power_iff) next case (Suc j) let ?xs = "canrepr n" have lenxs: "length ?xs = Suc j" using Suc by simp have hdtl: "?xs = hd ?xs # tl ?xs" using Suc by (metis hd_Cons_tl list.size(3) nat.simps(3)) have len: "length (tl ?xs) = j" using Suc by simp have can: "canonical (tl ?xs)" using hdtl canonical_canrepr canonical_tl by metis define n' where"n' = num (tl ?xs)" thenhave"nlength n' = j" using len can canreprI by simp thenhave n'_less: "n' < 2 ^ j" using Suc by auto have"num ?xs = todigit (hd ?xs) + 2 * num (tl ?xs)" by (metis hdtl num_Cons) thenhave"n = todigit (hd ?xs) + 2 * num (tl ?xs)" using canrepr by simp alsohave"... ≤ 1 + 2 * num (tl ?xs)" by simp alsohave"... = 1 + 2 * n'" using n'_defby simp alsohave"... ≤ 1 + 2 * (2 ^ j - 1)" using n'_less by simp alsohave"... = 2 ^ (Suc j) - 1" by (metis (no_types, lifting) add_Suc_right le_add_diff_inverse mult_2 one_le_numeral
one_le_power plus_1_eq_Suc sum.op_ivl_Suc sum_power2 zero_order(3)) alsohave"... < 2 ^ (Suc j)" by simp alsohave"... = 2 ^ (nlength n)" using lenxs by simp finallyshow ?case . qed
lemma pow_nlength: assumes"2 ^ j ≤ n"and"n < 2 ^ (Suc j)" shows"nlength n = Suc j" proof (rule ccontr) assume"nlength n ≠ Suc j" thenhave"nlength n < Suc j ∨ nlength n > Suc j" by auto thenshow False proof assume"nlength n < Suc j" thenhave"nlength n ≤ j" by simp moreoverhave"n < 2 ^ (nlength n)" using nlength_less_pow by simp ultimatelyhave"n < 2 ^ j" by (metis le_less_trans nat_power_less_imp_less not_less numeral_2_eq_2 zero_less_Suc) thenshow False using assms(1) by simp next assume *: "nlength n > Suc j" thenhave"n ≥ 2 ^ (nlength n - 1)" using nlength_ge_pow by simp moreoverhave"nlength n - 1 ≥ Suc j" using * by simp ultimatelyhave"n ≥ 2 ^ (Suc j)" by (metis One_nat_def le_less_trans less_2_cases_iff linorder_not_less power_less_imp_less_exp) thenshow False using assms(2) by simp qed qed
lemma nlength_le_n: "nlength n ≤ n" proof (cases "n = 0") case True thenshow ?thesis using canrepr_0 by simp next case False thenhave"nlength n > 0" using nlength_0 by simp moreoverfrom this have"n ≥ 2 ^ (nlength n - 1)" using nlength_0 nlength_ge_pow by auto ultimatelyshow ?thesis using nlength_ge_pow by (metis Suc_diff_1 Suc_leI dual_order.trans less_exp) qed
lemma nlength_Suc_le: "nlength n ≤ nlength (Suc n)" proof (cases "n = 0") case True thenshow ?thesis by (simp add: canrepr_0) next case False thenobtain j where j: "nlength n = Suc j" by (metis canrepr canrepr_0 gr0_implies_Suc length_greater_0_conv) thenhave"n ≥ 2 ^ j" using nlength_ge_pow by simp show ?thesis proof (cases "Suc n ≥ 2 ^ (Suc j)") case True have"n < 2 ^ (Suc j)" using j nlength_less_pow by metis thenhave"Suc n < 2 ^ (Suc (Suc j))" by simp thenhave"nlength (Suc n) = Suc (Suc j)" using True pow_nlength by simp thenshow ?thesis using j by simp next case False thenhave"Suc n < 2 ^ (Suc j)" by simp thenhave"nlength (Suc n) = Suc j" using `n ≥2 ^ j` pow_nlength by simp thenshow ?thesis using j by simp qed qed
lemma nlength_mono: assumes"n1 ≤ n2" shows"nlength n1 ≤ nlength n2" proof - have"nlength n ≤ nlength (n + d)"for n d proof (induction d) case0 thenshow ?case by simp next case (Suc d) thenshow ?case using nlength_Suc_le by (metis nat_arith.suc1 order_trans) qed thenshow ?thesis using assms by (metis le_add_diff_inverse) qed
lemma nlength_even_le: "n > 0 ==> nlength (2 * n) = Suc (nlength n)" proof - assume"n > 0" thenhave"nlength n > 0" by (metis canrepr canrepr_0 length_greater_0_conv less_numeral_extra(3)) thenhave"n ≥ 2 ^ (nlength n - 1)" using Suc_diff_1 nlength_ge_pow by simp thenhave"2 * n ≥ 2 ^ (nlength n)" by (metis Suc_diff_1 ‹0 < nlength n› mult_le_mono2 power_Suc) moreoverhave"2 * n < 2 ^ (Suc (nlength n))" using nlength_less_pow by simp ultimatelyshow ?thesis using pow_nlength by simp qed
lemma nlength_prod: "nlength (n1 * n2) ≤ nlength n1 + nlength n2" proof - let ?j1 = "nlength n1"and ?j2 = "nlength n2" have"n1 < 2 ^ ?j1""n2 < 2 ^ ?j2" using nlength_less_pow by simp_all thenhave"n1 * n2 < 2 ^ ?j1 * 2 ^ ?j2" by (simp add: mult_strict_mono) thenhave"n1 * n2 < 2 ^ (?j1 + ?j2)" by (simp add: power_add) thenhave"n1 * n2 ≤ 2 ^ (?j1 + ?j2) - 1" by simp thenhave"nlength (n1 * n2) ≤ nlength (2 ^ (?j1 + ?j2) - 1)" using nlength_mono by simp thenshow"nlength (n1 * n2) ≤ ?j1 + ?j2" using nlength_pow_minus_1 by simp qed
text‹
the following lemma @{const Suc} is needed because $n^0 = 1$. ›
lemma nlength_pow: "nlength (n ^ d) ≤ Suc (d * nlength n)" proof (induction d) case0 thenshow ?case by (metis less_or_eq_imp_le mult_not_zero nat_power_eq_Suc_0_iff nlength_pow2) next case (Suc d) have"nlength (n ^ Suc d) = nlength (n ^ d * n)" by (simp add: mult.commute) thenhave"nlength (n ^ Suc d) ≤ nlength (n ^ d) + nlength n" using nlength_prod by simp thenshow ?case using Suc by simp qed
lemma nlength_sum: "nlength (n1 + n2) ≤ Suc (max (nlength n1) (nlength n2))" proof - let ?m = "max n1 n2" have"n1 + n2 ≤ 2 * ?m" by simp thenhave"nlength (n1 + n2) ≤ nlength (2 * ?m)" using nlength_mono by simp moreoverhave"nlength ?m = max (nlength n1) (nlength n2)" using nlength_mono by (metis max.absorb1 max.cobounded2 max_def) ultimatelyshow ?thesis using nlength_even_le by (metis canrepr_0 le_SucI le_zero_eq list.size(3) max_nat.neutr_eq_iff not_gr_zero zero_eq_add_iff_both_eq_0) qed
lemma nlength_less_n: "n ≥ 3 ==> nlength n < n" proof (induction n rule: nat_induct_at_least) case base thenshow ?case by (simp add: nlength_3) next case (Suc n) thenshow ?case using nlength_Suc by (metis Suc_le_eq le_neq_implies_less nlength_le_n not_less_eq) qed
subsubsection‹Comparing two numbers›
text‹
order to compare two numbers in canonical representation, we can use the
machine @{const tm_equals}, which works for arbitrary proper symbol
.
lemma tm_setn_tm: assumes"k ≥ 2"and"G ≥ 4"and"j < k"and"0 < j " shows"turing_machine k G (tm_setn j n)" proof - have"symbols_lt G (canrepr n)" using assms(2) bit_symbols_canrepr by fastforce thenshow ?thesis unfolding tm_setn_def using tm_set_tm assms by simp qed
lemma transforms_tm_setnI [transforms_intros]: fixes j :: tapeidx fixes tps tps' :: "tape list"and x k n :: nat assumes"j < length tps" assumes"tps ! j = (⌊x⌋N, 1)" assumes"t = 10 + 2 * nlength x + 2 * nlength n" assumes"tps' = tps[j := (⌊n⌋N, 1)]" shows"transforms (tm_setn j n) tps t tps'" unfolding tm_setn_def using transforms_tm_setI[OF assms(1), of "canrepr x""canrepr n" t tps'] assms
canonical_canrepr canonical_def contents_clean_tape' by (simp add: eval_nat_numeral(3) numeral_Bit0 proper_symbols_canrepr)
subsection‹Incrementing›
text‹
this section we devise a Turing machine that increments a number. The next
describes how the symbol sequence of the incremented number looks like.
one has to flip all @{text 1} symbols starting at the least
digit until one reaches a @{text 0}, which is then replaced by a
{text 1}. If there is no @{text 0}, a @{text 1} is appended. Here we
that the most significant digit is to the right. ›
definition nincr :: "symbol list ==> symbol list"where "nincr zs ≡ if ∃i<length zs. zs ! i = 0 then replicate (LEAST i. i < length zs ∧ zs ! i = 0) 0 @ [1] @ drop (Suc (LEAST i. i < length zs ∧ zs ! i = 0)) zs else replicate (length zs) 0 @ [1]"
lemma canonical_nincr: assumes"canonical zs" shows"canonical (nincr zs)" proof - have1: "bit_symbols zs" using canonical_def assms by simp let ?j = "LEAST i. i < length zs ∧ zs ! i = 0" have"bit_symbols (nincr zs)" proof (cases "∃i<length zs. zs ! i = 0") case True thenhave"nincr zs = replicate ?j 0 @ [1] @ drop (Suc ?j) zs" using nincr_def by simp moreoverhave"bit_symbols (replicate ?j 0)" by simp moreoverhave"bit_symbols [1]" by simp moreoverhave"bit_symbols (drop (Suc ?j) zs)" using1by simp ultimatelyshow ?thesis using bit_symbols_append by presburger next case False thenshow ?thesis using nincr_def bit_symbols_append by auto qed moreoverhave"last (nincr zs) = 1" proof (cases "∃i<length zs. zs ! i = 0") case True thenshow ?thesis using nincr_def assms canonical_def by auto next case False thenshow ?thesis using nincr_def by auto qed ultimatelyshow ?thesis using canonical_def by simp qed
lemma nincr: assumes"bit_symbols zs" shows"num (nincr zs) = Suc (num zs)" proof (cases "∃i<length zs. zs ! i = 0") case True define j where"j = (LEAST i. i < length zs ∧ zs ! i = 0)" thenhave1: "j < length zs ∧ zs ! j = 0" using LeastI_ex[OF True] by simp have2: "zs ! i = 1"if"i < j"for i using that True j_def assms "1" less_trans not_less_Least by blast
define xs :: "symbol list"where"xs = replicate j 1 @ [0]" define ys :: "symbol list"where"ys = drop (Suc j) zs" have"zs = xs @ ys" proof - have"xs = take (Suc j) zs" using xs_def 12 by (smt (verit, best) le_eq_less_or_eq length_replicate length_take min_absorb2 nth_equalityI
nth_replicate nth_take take_Suc_conv_app_nth) thenshow ?thesis using ys_def by simp qed
have"nincr zs = replicate j 0 @ [1] @ drop (Suc j) zs" using nincr_def True j_def by simp thenhave"num (nincr zs) = num (replicate j 0 @ [1] @ ys)" using ys_def by simp alsohave"... = num (replicate j 0 @ [1]) + 2 ^ Suc j * num ys" using num_append by (metis append_assoc length_append_singleton length_replicate) alsohave"... = Suc (num xs) + 2 ^ Suc j * num ys" proof - have"num (replicate j 0 @ [1]) = 2 ^ j" using num_replicate2_eq_pow by simp alsohave"... = Suc (2 ^ j - 1)" by simp alsohave"... = Suc (num (replicate j 1))" using num_replicate3_eq_pow_minus_1 by simp alsohave"... = Suc (num (replicate j 1 @ [0]))" using num_trailing_zero by simp finallyhave"num (replicate j 0 @ [1]) = Suc (num xs)" using xs_def by simp thenshow ?thesis by simp qed alsohave"... = Suc (num xs + 2 ^ Suc j * num ys)" by simp alsohave"... = Suc (num zs)" using `zs = xs @ ys` num_append xs_def by (metis length_append_singleton length_replicate) finallyshow ?thesis . next case False thenhave"∀i<length zs. zs ! i = 1" using assms by simp thenhave zs: "zs = replicate (length zs) 1" by (simp add: nth_equalityI) thenhave num_zs: "num zs = 2 ^ length zs - 1" by (metis num_replicate3_eq_pow_minus_1) have"nincr zs = replicate (length zs) 0 @ [1]" using nincr_def False by auto thenhave"num (nincr zs) = 2 ^ length zs" by (simp add: num_replicate2_eq_pow) thenshow ?thesis using num_zs by simp qed
lemma nincr_canrepr: "nincr (canrepr n) = canrepr (Suc n)" using canrepr canonical_canrepr canreprI bit_symbols_canrepr canonical_nincr nincr by metis
text‹
next Turing machine performs the incrementing. Starting from the left of the
sequence on tape $j$, it writes the symbol \textbf{0} until it reaches a
or the symbol \textbf{1}. Then it writes a \textbf{1} and returns the tape
to the beginning. ›
text‹
a constant by iteratively incrementing is not exactly efficient, but it
only takes constant time and thus does not endanger any time bounds. ›
fun tm_plus_const :: "nat ==> tapeidx ==> machine"where "tm_plus_const 0 j = []" | "tm_plus_const (Suc c) j = tm_plus_const c j ;; tm_incr j"
lemma tm_plus_const_tm: assumes"k ≥ 2"and"G ≥ 4"and"0 < j"and"j < k" shows"turing_machine k G (tm_plus_const c j)" using assms Nil_tm tm_incr_tm by (induction c) simp_all
lemma transforms_tm_plus_constI [transforms_intros]: fixes c :: nat assumes"j < k" and"j > 0" and"length tps = k" and"tps ! j = (⌊x⌋N, 1)" and"ttt = c * (5 + 2 * nlength (x + c))" and"tps' = tps[j := (⌊x + c⌋N, 1)]" shows"transforms (tm_plus_const c j) tps ttt tps'" using assms(5,6,4) proof (induction c arbitrary: ttt tps') case0 thenshow ?case using transforms_Nil assms by (metis add_cancel_left_right list_update_id mult_eq_0_iff tm_plus_const.simps(1)) next case (Suc c) define tpsA where"tpsA = tps[j := (⌊x + c⌋N, 1)]" let ?ttt = "c * (5 + 2 * nlength (x + c)) + (5 + 2 * nlength (x + c))" have"transforms (tm_plus_const c j ;; tm_incr j) tps ?ttt tps'" proof (tform tps: assms) show"transforms (tm_plus_const c j) tps (c * (5 + 2 * nlength (x + c))) tpsA" using tpsA_def assms Suc by simp show"j < length tpsA" using tpsA_def assms(1,3) by simp show"tpsA ! j = (⌊x + c⌋N, 1)" using tpsA_def assms(1,3) by simp show"tps' = tpsA[j := (⌊Suc (x + c)⌋N, 1)]" using tpsA_def assms Suc by (metis add_Suc_right list_update_overwrite) qed moreoverhave"?ttt ≤ ttt" proof - have"?ttt = Suc c * (5 + 2 * nlength (x + c))" by simp alsohave"... ≤ Suc c * (5 + 2 * nlength (x + Suc c))" using nlength_mono Suc_mult_le_cancel1 by auto finallyshow"?ttt ≤ ttt" using Suc by simp qed ultimatelyhave"transforms (tm_plus_const c j ;; tm_incr j) tps ttt tps'" using transforms_monotone by simp thenshow ?case by simp qed
subsection‹Decrementing›
text‹
a number is almost like incrementing but with the symbols
textbf{0} and \textbf{1} swapped. One difference is that in order to get a
symbol sequence, a trailing zero must be removed, whereas incrementing
result in a trailing zero. Another difference is that decrementing the
zero yields zero.
next function returns the leftmost symbol~\textbf{1}, that is, the one
needs to be flipped. ›
definition first1 :: "symbol list ==> nat"where "first1 zs ≡ LEAST i. i < length zs ∧ zs ! i = 1"
lemma canonical_ex_3: assumes"canonical zs"and"zs ≠ []" shows"∃i<length zs. zs ! i = 1" using assms canonical_def by (metis One_nat_def Suc_pred last_conv_nth length_greater_0_conv lessI)
lemma canonical_first1_less: assumes"canonical zs"and"zs ≠ []" shows"∀i<first1 zs. zs ! i = 0" proof - have"∀i<first1 zs. zs ! i ≠1" using assms first1_def canonical_first1 not_less_Least by fastforce thenshow ?thesis using assms canonical_def by (meson canonical_first1 less_trans) qed
text‹
next function describes how the canonical representation of the decremented
sequence looks like. It has special cases for the empty sequence and for
whose only \textbf{1} is the most significant digit. ›
definition ndecr :: "symbol list ==> symbol list"where "ndecr zs ≡ if zs = [] then [] else if first1 zs = length zs - 1 then replicate (first1 zs) 1 else replicate (first1 zs) 1 @ [0] @ drop (Suc (first1 zs)) zs"
lemma canonical_ndecr: assumes"canonical zs" shows"canonical (ndecr zs)" proof - let ?i = "first1 zs"
consider "zs = []"
| "zs ≠ [] ∧ first1 zs = length zs - 1"
| "zs ≠ [] ∧ first1 zs < length zs - 1" using canonical_first1 assms by fastforce thenshow ?thesis proof (cases) case1 thenshow ?thesis using ndecr_def canonical_def by simp next case2 thenshow ?thesis using canonical_def ndecr_def not_less_eq by fastforce next case3 thenhave"Suc (first1 zs) < length zs" by auto thenhave"last (drop (Suc (first1 zs)) zs) = 1" using assms canonical_def 3by simp moreoverhave"bit_symbols (replicate (first1 zs) 1 @ [0] @ drop (Suc (first1 zs)) zs)" proof - have"bit_symbols (replicate (first1 zs) 1)" by simp moreoverhave"bit_symbols [0]" by simp moreoverhave"bit_symbols (drop (Suc (first1 zs)) zs)" using assms canonical_def by simp ultimatelyshow ?thesis using bit_symbols_append by presburger qed ultimatelyshow ?thesis using canonical_def ndecr_def 3by auto qed qed
lemma ndecr: assumes"canonical zs" shows"num (ndecr zs) = num zs - 1" proof - let ?i = "first1 zs"
consider "zs = []" | "zs ≠ [] ∧ first1 zs = length zs - 1" | "zs ≠ [] ∧ first1 zs < length zs - 1" using canonical_first1 assms by fastforce thenshow ?thesis proof (cases) case1 thenshow ?thesis using ndecr_def canrepr_0 canrepr by (metis zero_diff) next case2 thenhave less: "zs ! i = 0"if"i < first1 zs"for i using that assms canonical_first1_less by simp have at: "zs ! (first1 zs) = 1" using2 canonical_first1 assms by blast have"zs = replicate (first1 zs) 0 @ [1]" (is"zs = ?zs") proof (rule nth_equalityI) show len: "length zs = length ?zs" using2by simp show"zs ! i = ?zs ! i"if"i < length zs"for i proof (cases "i < first1 zs") case True thenshow ?thesis by (simp add: less nth_append) next case False thenshow ?thesis using len that at by (metis Suc_leI leD length_append_singleton length_replicate linorder_neqE_nat nth_append_length) qed qed moreoverfrom this have"ndecr zs = replicate (first1 zs) 3" using ndecr_def 2by simp ultimatelyshow ?thesis using num_replicate2_eq_pow num_replicate3_eq_pow_minus_1 by metis next case3 thenhave less: "zs ! i = 0"if"i < ?i"for i using that assms canonical_first1_less by simp have at: "zs ! ?i = 1" using3 canonical_first1 assms by simp have zs: "zs = replicate ?i 0 @ [1] @ drop (Suc ?i) zs" (is"zs = ?zs") proof (rule nth_equalityI) show len: "length zs = length ?zs" using3by auto show"zs ! i = ?zs ! i"if"i < length zs"for i proof -
consider "i < ?i" | "i = ?i" | "i > ?i" by linarith thenshow ?thesis proof (cases) case1 thenshow ?thesis using less by (metis length_replicate nth_append nth_replicate) next case2 thenshow ?thesis using at by (metis append_Cons length_replicate nth_append_length) next case3 have"?zs = (replicate ?i 0 @ [1]) @ drop (Suc ?i) zs" by simp thenhave"?zs ! i = drop (Suc ?i) zs ! (i - Suc ?i)" using3by (simp add: nth_append) thenhave"?zs ! i = zs ! i" using3 that by simp thenshow ?thesis by simp qed qed qed thenhave"ndecr zs = replicate ?i 1 @ [0] @ drop (Suc ?i) zs" using ndecr_def 3by simp thenhave"Suc (num (ndecr zs)) = Suc (num ((replicate ?i 1 @ [0]) @ drop (Suc ?i) zs))"
(is"_ = Suc (num (?xs @ ?ys))") by simp alsohave"... = Suc (num ?xs + 2 ^ length ?xs * num ?ys)" using num_append by blast alsohave"... = Suc (num ?xs + 2 ^ Suc ?i * num ?ys)" by simp alsohave"... = Suc (2 ^ ?i - 1 + 2 ^ Suc ?i * num ?ys)" using num_replicate3_eq_pow_minus_1 num_trailing_zero[of 2"replicate ?i 1"] by simp alsohave"... = 2 ^ ?i + 2 ^ Suc ?i * num ?ys" by simp alsohave"... = num (replicate ?i 0 @ [1]) + 2 ^ Suc ?i * num ?ys" using num_replicate2_eq_pow by simp alsohave"... = num ((replicate ?i 0 @ [1]) @ ?ys)" using num_append by (metis length_append_singleton length_replicate) alsohave"... = num (replicate ?i 0 @ [1] @ ?ys)" by simp alsohave"... = num zs" using zs by simp finallyhave"Suc (num (ndecr zs)) = num zs" . thenshow ?thesis by simp qed qed
text‹
next Turing machine implements the function @{const ndecr}. It does nothing
the empty input, which represents zero. On other inputs it writes symbols
textbf{1} going right until it reaches a \textbf{1} symbol, which is guaranteed
happen for non-empty canonical representations. It then overwrites this
textbf{1} with \textbf{0}. If there is a blank symbol to the right of this
textbf{0}, the \textbf{0} is removed again. ›
context fixes tps0 :: "tape list"and xs :: "symbol list"and k :: nat assumes jk: "length tps0 = k""j < k" and can: "canonical xs" and tps0: "tps0 ! j = (⌊xs⌋, 1)" begin
lemma bs: "bit_symbols xs" using can canonical_def by simp
context assumes read_tps0: "read tps0 ! j = ◻" begin
lemma xs_Nil: "xs = []" using tps0 jk tapes_at_read' read_tps0 bs contents_inbounds by (metis can canreprI canrepr_0 fst_conv ncontents_1_blank_iff_zero snd_conv)
have"tps2 ! j = (⌊replicate (first1 xs) 1 @ [0] @ drop (Suc (first1 xs)) xs⌋, Suc (Suc (first1 xs)))"
(is"_ = (⌊?zs⌋, ?i)") using tps2_def jk by simp have"length ?zs = length xs" using first1 by simp thenhave"Suc (Suc (first1 xs)) = Suc (length ?zs)" using xs eq by simp thenhave *: "⌊?zs⌋ ?i = 0" using contents_outofbounds by simp
have"read tps2 ! j = ⌊?zs⌋ ?i" using tps2_def jk tapes_at_read'[of j tps2] by simp thenhave"⌊?zs⌋ ?i ≠◻" using read_tps2' by simp thenshow False using * by simp qed
lemma tps2: "tps2 = tps0[j := (⌊ndecr xs⌋, Suc (Suc (first1 xs)))]" using tps2_def ndecr_def first1_neq xs by simp
lemma tm6: assumes"ttt = first1 xs + 2 + (if read tps2 ! j = ◻ then 4 else 1) + (tps5 :#: j + 2)" shows"transforms tm6 tps0 ttt tps6" unfolding tm6_def proof (tform tps: tps5_def tps6_def jk time: assms) show"clean_tape (tps5 ! j)" proof - have"tps5 ::: j = ⌊ndecr xs⌋" using tps5_def jk by simp moreoverhave"bit_symbols (ndecr xs)" using canonical_ndecr can canonical_def by simp ultimatelyshow ?thesis using One_nat_def Suc_1 Suc_le_lessD clean_contents_proper by (metis contents_clean_tape' lessI one_less_numeral_iff semiring_norm(77)) qed qed
lemma tm6' [transforms_intros]: assumes"ttt = 2 * first1 xs + 9" shows"transforms tm6 tps0 ttt tps6" proof - let ?ttt = "first1 xs + 2 + (if read tps2 ! j = ◻ then 4 else 1) + (tps5 :#: j + 2)" have"tps5 :#: j = (if read tps2 ! j = ◻ then Suc (first1 xs) else Suc (Suc (first1 xs)))" using tps5_def jk by simp thenhave"?ttt ≤ ttt" using assms by simp thenshow ?thesis using tm6 transforms_monotone assms by simp qed
end(* context read tps0 ! j \<noteq> 0 *)
definition"tps7 ≡ tps0[j := (⌊ndecr xs⌋, 1)]"
lemma tm7: assumes"ttt = 8 + 2 * length xs" shows"transforms tm7 tps0 ttt tps7" unfolding tm7_def proof (tform tps: tps6_def tps7_def time: assms) show"tps7 = tps0"if"read tps0 ! j = ◻" using that ndecr_def tps0 tps7_def xs_Nil jk by (simp add: list_update_same_conv) show"2 * first1 xs + 9 + 1 ≤ ttt"if"read tps0 ! j ≠◻" proof - have"length xs > 0" using that xs by simp thenshow ?thesis using first1(1) that assms by simp qed qed
end(* context *)
end(* locale *)
lemma transforms_tm_decrI [transforms_intros]: fixes tps tps' :: "tape list"and n :: nat and k ttt :: nat assumes"j < k""length tps = k" assumes"tps ! j = (⌊n⌋N, 1)" assumes"ttt = 8 + 2 * nlength n" assumes"tps' = tps[j := (⌊n - 1⌋N, 1)]" shows"transforms (tm_decr j) tps ttt tps'" proof - let ?xs = "canrepr n" have can: "canonical ?xs" using canonical_canrepr by simp have tps0: "tps ! j = (⌊?xs⌋, 1)" using assms by simp have tps': "tps' = tps[j := (⌊ndecr ?xs⌋, 1)]" using ndecr assms(5) by (metis canrepr canreprI can canonical_ndecr) interpret loc: turing_machine_decr j . have"transforms loc.tm7 tps ttt tps'" using loc.tm7 loc.tps7_def by (metis assms(1,2,4) can tps' tps0) thenshow ?thesis using loc.tm7_eq_tm_decr by simp qed
subsection‹Addition›
text‹
this section we construct a Turing machine that adds two numbers in canonical
each given on a separate tape and overwrites the second number
the sum. The TM implements the common algorithm with carry starting from
least significant digit.
two symbol sequences @{term xs} and @{term ys} representing numbers, the
function computes the carry bit that occurs in the $i$-th position. For the
significant position, 0, there is no carry (that is, it is 0); for
$i + 1$ the carry is the sum of the bits of @{term xs} and @{term ys}
position $i$ and the carry for position $i$. The function gives the carry as \textbf{0} or \textbf{1}, except for position 0, where it is the start
~$\triangleright$. The start symbol represents the same bit as the
~\textbf{0} as defined by @{const todigit}. The reason for this special
is that the TM will store the carry on a memorization tape
see~Section~\ref{s:tm-memorizing}), which initially contains the start symbol. ›
fun carry :: "symbol list ==> symbol list ==> nat ==> symbol"where "carry xs ys 0 = 1" | "carry xs ys (Suc i) = tosym ((todigit (digit xs i) + todigit (digit ys i) + todigit (carry xs ys i)) div 2)"
text‹
next function specifies the $i$-th digit of the sum. ›
definition sumdigit :: "symbol list ==> symbol list ==> nat ==> symbol"where "sumdigit xs ys i ≡ tosym ((todigit (digit xs i) + todigit (digit ys i) + todigit (carry xs ys i)) mod 2)"
lemma carry_sumdigit_eq_sum: "num xs + num ys = num (map (sumdigit xs ys) [0..<t]) + 2 ^ t * todigit (carry xs ys t) + 2 ^ t * num (drop t xs) + 2 ^ t * num (drop t ys)" proof (induction t) case0 thenshow ?case using num_def by simp next case (Suc t) let ?z = "sumdigit xs ys" let ?c = "carry xs ys" let ?zzz = "map ?z [0..<Suc t]" have"num (take (Suc t) ?zzz) = num (take t ?zzz) + 2 ^ t * todigit (digit ?zzz t)" using num_take_Suc by blast moreoverhave"take (Suc t) ?zzz = map (sumdigit xs ys) [0..<Suc t]" by simp moreoverhave"take t ?zzz = map (sumdigit xs ys) [0..<t]" by simp ultimatelyhave1: "num (map ?z [0..<Suc t]) = num (map ?z [0..<t]) + 2 ^ t * todigit (digit ?zzz t)" by simp
have2: "digit ?zzz t = sumdigit xs ys t" using digit_def by (metis One_nat_def add_Suc diff_add_inverse length_map length_upt lessI nth_map_upt plus_1_eq_Suc)
have"todigit (?z t) + 2 * (todigit (carry xs ys (Suc t))) = todigit (carry xs ys t) + todigit (digit xs t) + todigit (digit ys t)" using carry_sumdigit . thenhave"2 ^ t * (todigit (?z t) + 2 * (todigit (?c (Suc t)))) = 2 ^ t * (todigit (?c t) + todigit (digit xs t) + todigit (digit ys t))" by simp thenhave"2 ^ t * todigit (?z t) + 2 ^ t * 2 * todigit (?c (Suc t)) = 2 ^ t * todigit (?c t) + 2 ^ t * todigit (digit xs t) + 2 ^ t * todigit (digit ys t)" using add_mult_distrib2 by simp thenhave"num (map ?z [0..<t]) + 2 ^ t * (todigit (?z t)) + 2 ^ Suc t * (todigit (?c (Suc t))) = num (map ?z [0..<t]) + 2 ^ t * (todigit (?c t)) + 2 ^ t * (todigit (digit xs t)) + 2^t * (todigit (digit ys t))" by simp thenhave"num (map ?z [0..<Suc t]) + 2 ^ Suc t * (todigit (?c (Suc t))) = num (map ?z [0..<t]) + 2 ^ t * todigit (?c t) + 2 ^ t * todigit (digit xs t) + 2 ^ t * todigit (digit ys t)" using12by simp thenhave"num (map ?z [0..<Suc t]) + 2 ^ Suc t * (todigit (?c (Suc t))) + 2 ^ Suc t * num (drop (Suc t) xs) + 2 ^ Suc t * num (drop (Suc t) ys) = num (map ?z [0..<t]) + 2 ^ t * todigit (?c t) + 2 ^ t * todigit (digit xs t) + 2 ^ t * todigit (digit ys t) + 2 ^ Suc t * num (drop (Suc t) xs) + 2 ^ Suc t * num (drop (Suc t) ys)" by simp alsohave"... = num (map ?z [0..<t]) + 2 ^ t * (todigit (?c t)) + 2 ^ t * (todigit (digit xs t) + 2 * num (drop (Suc t) xs)) + 2 ^ t * (todigit (digit ys t) + 2 * num (drop (Suc t) ys))" by (simp add: add_mult_distrib2) alsohave"... = num (map ?z [0..<t]) + 2 ^ t * (todigit (?c t)) + 2 ^ t * num (drop t xs) + 2 ^ t * num (drop t ys)" using num_drop by metis alsohave"... = num xs + num ys" using Suc by simp finallyshow ?case by simp qed
lemma carry_le: assumes"symbols_lt 4 xs"and"symbols_lt 4 ys" shows"carry xs ys t ≤1" proof (induction t) case0 thenshow ?case by simp next case (Suc t) thenhave"todigit (carry xs ys t) ≤ 1" by simp moreoverhave"todigit (digit xs t) ≤ 1" using assms(1) digit_def by auto moreoverhave"todigit (digit ys t) ≤ 1" using assms(2) digit_def by auto ultimatelyshow ?case by simp qed
lemma num_sumdigit_eq_sum: assumes"length xs ≤ n" and"length ys ≤ n" and"symbols_lt 4 xs" and"symbols_lt 4 ys" shows"num xs + num ys = num (map (sumdigit xs ys) [0..<Suc n])" proof - have"num xs + num ys = num (map (sumdigit xs ys) [0..<Suc n]) + 2 ^ Suc n * todigit (carry xs ys (Suc n)) + 2 ^ Suc n * num (drop (Suc n) xs) + 2 ^ Suc n * num (drop (Suc n) ys)" using carry_sumdigit_eq_sum by blast alsohave"... = num (map (sumdigit xs ys) [0..<Suc n]) + 2 ^ Suc n * todigit (carry xs ys (Suc n))" using assms(1,2) by (simp add: num_def) alsohave"... = num (map (sumdigit xs ys) [0..<Suc n])" proof - have"digit xs n = 0" using assms(1) digit_def by simp moreoverhave"digit ys n = 0" using assms(2) digit_def by simp ultimatelyhave"(digit xs n + digit ys n + todigit (carry xs ys n)) div 2 = 0" using carry_le[OF assms(3,4), of n] by simp thenshow ?thesis by auto qed finallyshow ?thesis . qed
lemma num_sumdigit_eq_sum': assumes"symbols_lt 4 xs"and"symbols_lt 4 ys" shows"num xs + num ys = num (map (sumdigit xs ys) [0..<Suc (max (length xs) (length ys))])" using assms num_sumdigit_eq_sum by simp
lemma num_sumdigit_eq_sum'': assumes"bit_symbols xs"and"bit_symbols ys" shows"num xs + num ys = num (map (sumdigit xs ys) [0..<Suc (max (length xs) (length ys))])" proof - have"symbols_lt 4 xs" using assms(1) by auto moreoverhave"symbols_lt 4 ys" using assms(2) by auto ultimatelyshow ?thesis using num_sumdigit_eq_sum' by simp qed
lemma sumdigit_bit_symbols: "bit_symbols (map (sumdigit xs ys) [0..<t])" using sumdigit_def by auto
text‹
core of the addition Turing machine is the following command. It scans the
on tape $j_1$ and $j_2$ in lockstep until it reaches blanks on both
. In every step it adds the symbols on both tapes and the symbol on the
tape, which is a memorization tape storing the carry bit. The sum of these
bits modulo~2 is written to tape $j_2$ and the new carry to the
tape. ›
lemma sem_cmd_plus: assumes"j1 ≠ j2" and"j1 < k - 1" and"j2 < k - 1" and"j2 > 0" and"length tps = k" and"bit_symbols xs" and"bit_symbols ys" and"tps ! j1 = (⌊xs⌋, Suc t)" and"tps ! j2 = (⌊map (sumdigit xs ys) [0..<t] @ drop t ys⌋, Suc t)" and"last tps = ⌈carry xs ys t⌉" and"rs = read tps" and"tps' = tps [j1 := tps!j1 |+| 1, j2 := tps!j2 |:=| sumdigit xs ys t |+| 1, length tps - 1 := ⌈carry xs ys (Suc t)⌉]" shows"sem (cmd_plus j1 j2) (0, tps) = (if t < max (length xs) (length ys) then 0 else 1, tps')" proof have"k ≥ 2" using assms(3,4) by simp have rs1: "rs ! j1 = digit xs t" using assms(2,5,8,11) digit_def read_def contents_def by simp let ?zs = "map (sumdigit xs ys) [0..<t] @ drop t ys" have rs2: "rs ! j2 = digit ys t" proof (cases "t < length ys") case True thenhave"?zs ! t = ys ! t" by (simp add: nth_append) thenshow ?thesis using assms(3,5,9,11) digit_def read_def contents_def by simp next case False thenhave"length ?zs = t" by simp thenhave"⌊?zs⌋ (Suc t) = ◻" using False contents_def by simp thenshow ?thesis using digit_def read_def contents_def False assms(3,5,9,11) by simp qed have rs3: "last rs = carry xs ys t" using `k ≥2` assms onesie_read onesie_def read_def read_length tapes_at_read' by (metis (no_types, lifting) diff_less last_conv_nth length_greater_0_conv less_one list.size(3) not_numeral_le_zero) have *: "tosym ((todigit (rs ! j1) + todigit (rs ! j2) + todigit (last rs)) mod 2) = sumdigit xs ys t" using rs1 rs2 rs3 sumdigit_def by simp
have"¬ (digit xs t = 0 ∧ digit ys t = 0)"if"t < max (length xs) (length ys)" using assms(6,7) digit_def that by auto thenhave4: "¬ (rs ! j1 = 0 ∧ rs ! j2 = 0)"if"t < max (length xs) (length ys)" using rs1 rs2 that by simp thenhave fst1: "fst (sem (cmd_plus j1 j2) (0, tps)) = fst (0, tps')"if"t < max (length xs) (length ys)" using that cmd_plus_def assms(11) by (smt (verit, ccfv_threshold) fst_conv prod.sel(2) sem)
have"digit xs t = 0 ∧ digit ys t = 0"if"t ≥ max (length xs) (length ys)" using that digit_def by simp thenhave5: "rs ! j1 = ◻∧ rs ! j2 = ◻"if"t ≥ max (length xs) (length ys)" using rs1 rs2 that by simp thenhave"fst (sem (cmd_plus j1 j2) (0, tps)) = fst (1, tps')"if"t ≥ max (length xs) (length ys)" using that cmd_plus_def assms(11) by (smt (verit, ccfv_threshold) fst_conv prod.sel(2) sem) thenshow"fst (sem (cmd_plus j1 j2) (0, tps)) = fst (if t < max (length xs) (length ys) then 0 else 1, tps')" using fst1 by (simp add: not_less)
show"snd (sem (cmd_plus j1 j2) (0, tps)) = snd (if t < max (length xs) (length ys) then 0 else 1, tps')" proof (rule snd_semI) show"proper_command k (cmd_plus j1 j2)" using cmd_plus_def by simp show"length tps = k" using assms(5) . show"length tps' = k" using assms(5,12) by simp have len: "length (read tps) = k" by (simp add: assms read_length) show"act (cmd_plus j1 j2 (read tps) [!] j) (tps ! j) = tps' ! j" if"j < k"for j proof - have j: "j < length tps" using len that assms(5) by simp
consider "j = j1"
| "j ≠ j1 ∧ j = j2"
| "j ≠ j1 ∧ j ≠ j2 ∧ j = length rs - 1"
| "j ≠ j1 ∧ j ≠ j2 ∧ j ≠ length rs - 1" by auto thenshow ?thesis proof (cases) case1 thenhave"cmd_plus j1 j2 (read tps) [!] j = (read tps ! j, Right)" using that len cmd_plus_def by simp thenhave"act (cmd_plus j1 j2 (read tps) [!] j) (tps ! j) = tps ! j |+| 1" using act_Right[OF j] by simp moreoverhave"tps' ! j = tps ! j |+| 1" using assms(1,2,5,12) that 1by simp ultimatelyshow ?thesis by simp next case2 thenhave"cmd_plus j1 j2 (read tps) [!] j = (tosym ((todigit (rs ! j1) + todigit (rs ! j2) + todigit (last rs)) mod 2), Right)" using that len cmd_plus_def assms(11) by simp thenhave"cmd_plus j1 j2 (read tps) [!] j = (sumdigit xs ys t, Right)" using * by simp moreoverhave"tps' ! j2 = tps!j2 |:=| sumdigit xs ys t |+| 1" using assms(3,5,12) by simp ultimatelyshow ?thesis using act_Right' 2by simp next case3 thenhave"cmd_plus j1 j2 (read tps) [!] j = (tosym ((todigit (rs ! j1) + todigit (rs ! j2) + todigit (last rs)) div 2), Stay)" using that len cmd_plus_def assms(11) by simp thenhave"cmd_plus j1 j2 (read tps) [!] j = (carry xs ys (Suc t), Stay)" using rs1 rs2 rs3 by simp moreoverhave"tps' ! (length tps - 1) = ⌈carry xs ys (Suc t)⌉" using3 assms(5,11,12) len that by simp ultimatelyshow ?thesis using3 act_onesie assms(3,5,10,11) len by (metis add_diff_inverse_nat last_length less_nat_zero_code nat_diff_split_asm plus_1_eq_Suc) next case4 thenhave"cmd_plus j1 j2 (read tps) [!] j = (read tps ! j, Stay)" using that len cmd_plus_def assms(11) by simp thenhave"act (cmd_plus j1 j2 (read tps) [!] j) (tps ! j) = tps ! j" using act_Stay[OF j] by simp moreoverhave"tps' ! j = tps ! j" using that 4 len assms(5,11,12) by simp ultimatelyshow ?thesis by simp qed qed qed qed
lemma contents_map_append_drop: "⌊map f [0..<t] @ drop t zs⌋(Suc t := f t) = ⌊map f [0..<Suc t] @ drop (Suc t) zs⌋" proof (cases "t < length zs") case lt: True thenhave t_lt: "t < length (map f [0..<t] @ drop t zs)" by simp show ?thesis proof fix x
consider "x = 0"
| "x > 0 ∧ x < Suc t"
| "x = Suc t"
| "x > Suc t ∧ x ≤ length zs"
| "x > Suc t ∧ x > length zs" by linarith thenshow"(⌊map f [0..<t] @ drop t zs⌋(Suc t := f t)) x = ⌊map f [0..<Suc t] @ drop (Suc t) zs⌋ x"
(is"?lhs x = ?rhs x") proof (cases) case1 thenshow ?thesis using contents_def by simp next case2 thenhave"?lhs x = (map f [0..<t] @ drop t zs) ! (x - 1)" using contents_def by simp moreoverhave"x - 1 < t" using2by auto ultimatelyhave left: "?lhs x = f (x - 1)" by (metis add.left_neutral diff_zero length_map length_upt nth_append nth_map_upt) have"?rhs x = (map f [0..<Suc t] @ drop (Suc t) zs) ! (x - 1)" using2 contents_def by simp moreoverhave"x - 1 < Suc t" using2by auto ultimatelyhave"?rhs x = f (x - 1)" by (metis diff_add_inverse diff_zero length_map length_upt nth_append nth_map_upt) thenshow ?thesis using left by simp next case3 thenshow ?thesis using contents_def lt by (smt (verit, ccfv_threshold) One_nat_def Suc_leI add_Suc append_take_drop_id diff_Suc_1 diff_zero fun_upd_same
length_append length_map length_take length_upt lessI min_absorb2 nat.simps(3) nth_append nth_map_upt plus_1_eq_Suc) next case4 thenhave"?lhs x = ⌊map f [0..<t] @ drop t zs⌋ x" using contents_def by simp thenhave"?lhs x = (map f [0..<t] @ drop t zs) ! (x - 1)" using4 contents_def by simp thenhave left: "?lhs x = drop t zs ! (x - 1 - t)" using4 by (metis Suc_lessE diff_Suc_1 length_map length_upt less_Suc_eq_le less_or_eq_imp_le minus_nat.diff_0 not_less_eq nth_append) have"x ≤ length (map f [0..<Suc t] @ drop (Suc t) zs)" using4 lt by auto moreoverhave"x > 0" using4by simp ultimatelyhave"?rhs x = (map f [0..<Suc t] @ drop (Suc t) zs) ! (x - 1)" using4 contents_inbounds by simp moreoverhave"x - 1 ≥ Suc t" using4by auto ultimatelyhave"?rhs x = drop (Suc t) zs ! (x - 1 - Suc t)" by (metis diff_zero leD length_map length_upt nth_append) thenshow ?thesis using left 4by (metis Cons_nth_drop_Suc Suc_diff_Suc diff_Suc_eq_diff_pred lt nth_Cons_Suc) next case5 thenshow ?thesis using lt contents_def by auto qed qed next case False moreoverhave"⌊map f [0..<t]⌋(Suc t := f t) = ⌊map f [0..<Suc t]⌋" proof fix x show"(⌊map f [0..<t]⌋(Suc t := f t)) x = ⌊map f [0..<Suc t]⌋ x" proof (cases "x < Suc t") case True thenshow ?thesis using contents_def by (smt (verit, del_insts) diff_Suc_1 diff_zero fun_upd_apply length_map length_upt less_Suc_eq_0_disj
less_Suc_eq_le less_imp_le_nat nat_neq_iff nth_map_upt) next case ge: False show ?thesis proof (cases "x = Suc t") case True thenshow ?thesis using contents_def by (metis One_nat_def add_Suc diff_Suc_1 diff_zero fun_upd_same ge le_eq_less_or_eq length_map
length_upt lessI less_Suc_eq_0_disj nth_map_upt plus_1_eq_Suc) next case False thenhave"x > Suc t" using ge by simp thenshow ?thesis using contents_def by simp qed qed qed ultimatelyshow ?thesis by simp qed
corollary sem_cmd_plus': assumes"j1 ≠ j2" and"j1 < k - 1" and"j2 < k - 1" and"j2 > 0" and"length tps = k" and"bit_symbols xs" and"bit_symbols ys" and"tps ! j1 = (⌊xs⌋, Suc t)" and"tps ! j2 = (⌊map (sumdigit xs ys) [0..<t] @ drop t ys⌋, Suc t)" and"last tps = ⌈carry xs ys t⌉" and"tps' = tps [j1 := (⌊xs⌋, Suc (Suc t)), j2 := (⌊map (sumdigit xs ys) [0..<Suc t] @ drop (Suc t) ys⌋, Suc (Suc t)), length tps - 1 := ⌈carry xs ys (Suc t)⌉]" shows"sem (cmd_plus j1 j2) (0, tps) = (if Suc t ≤ max (length xs) (length ys) then 0 else 1, tps')" proof - have"tps ! j1 |+| 1 = (⌊xs⌋, Suc (Suc t))" using assms(8) by simp moreoverhave"tps ! j2 |:=| sumdigit xs ys t |+| 1 = (⌊map (sumdigit xs ys) [0..<Suc t] @ drop (Suc t) ys⌋, Suc (Suc t))" using contents_map_append_drop assms(9) by simp ultimatelyshow ?thesis using sem_cmd_plus[OF assms(1-10)] assms(11) by auto qed
text‹
next Turing machine comprises just the command @{const cmd_plus}. It
tape $j_2$ with the sum of the numbers on tape $j_1$ and $j_2$. The
bit is maintained on the last tape. ›
lemma tm_plus_tm: assumes"j2 > 0"and"k ≥ 2"and"G ≥ 4" shows"turing_machine k G (tm_plus j1 j2)" unfolding tm_plus_def using assms(1-3) cmd_plus_def turing_machine_def by auto
lemma tm_plus_immobile: fixes k :: nat assumes"j1 < k"and"j2 < k" shows"immobile (tm_plus j1 j2) k (Suc k)" proof - let ?M = "tm_plus j1 j2"
{ fix q :: nat and rs :: "symbol list" assume q: "q < length ?M" assume rs: "length rs = Suc k" thenhave len: "length rs - 1 = k" by simp have neq: "k ≠ j1""k ≠ j2" using assms by simp_all have"?M ! q = cmd_plus j1 j2" using tm_plus_def q by simp moreoverhave"(cmd_plus j1 j2) rs [!] k = (tosym ((todigit (rs ! j1) + todigit (rs ! j2) + todigit (last rs)) div 2), Stay)" using cmd_plus_def rs len neq by fastforce ultimatelyhave"(cmd_plus j1 j2) rs [~] k = Stay" by simp
} thenshow ?thesis by (simp add: immobile_def tm_plus_def) qed
lemma execute_tm_plus: assumes"j1 ≠ j2" and"j1 < k - 1" and"j2 < k - 1" and"j2 > 0" and"length tps = k" and"bit_symbols xs" and"bit_symbols ys" and"t ≤ Suc (max (length xs) (length ys))" and"tps ! j1 = (⌊xs⌋, 1)" and"tps ! j2 = (⌊ys⌋, 1)" and"last tps = ⌈▹⌉" shows"execute (tm_plus j1 j2) (0, tps) t = (if t ≤ max (length xs) (length ys) then 0 else 1, tps [j1 := (⌊xs⌋, Suc t), j2 := (⌊map (sumdigit xs ys) [0..<t] @ drop t ys⌋, Suc t), length tps - 1 := ⌈carry xs ys t⌉])" using assms(8) proof (induction t) case0 have"carry xs ys 0 = 1" by simp moreoverhave"map (sumdigit xs ys) [0..<0] @ drop 0 ys = ys" by simp ultimatelyhave"tps = tps [j1 := (⌊xs⌋, Suc 0), j2 := (⌊map (sumdigit xs ys) [0..<0] @ drop 0 ys⌋, Suc 0), length tps - 1 := ⌈carry xs ys 0⌉]" using assms by (metis One_nat_def add_diff_inverse_nat last_length less_nat_zero_code
list_update_id nat_diff_split_asm plus_1_eq_Suc) thenshow ?case by simp next case (Suc t) let ?M = "tm_plus j1 j2" have"execute ?M (0, tps) (Suc t) = exe ?M (execute ?M (0, tps) t)"
(is"_ = exe ?M ?cfg") by simp alsohave"... = sem (cmd_plus j1 j2) ?cfg" using Suc tm_plus_def exe_lt_length by simp alsohave"... = (if Suc t ≤ max (length xs) (length ys) then 0 else 1, tps [j1 := (⌊xs⌋, Suc (Suc t)), j2 := (⌊map (sumdigit xs ys) [0..<Suc t] @ drop (Suc t) ys⌋, Suc (Suc t)), length tps - 1 := ⌈carry xs ys (Suc t)⌉])" proof - let ?tps = "tps [j1 := (⌊xs⌋, Suc t), j2 := (⌊map (sumdigit xs ys) [0..<t] @ drop t ys⌋, Suc t), length tps - 1 := ⌈carry xs ys t⌉]" let ?tps' = "?tps [j1 := (⌊xs⌋, Suc (Suc t)), j2 := (⌊map (sumdigit xs ys) [0..<Suc t] @ drop (Suc t) ys⌋, Suc (Suc t)), length tps - 1 := ⌈carry xs ys (Suc t)⌉]" have cfg: "?cfg = (0, ?tps)" using Suc by simp have tps_k: "length ?tps = k" using assms(2,3,5) by simp have tps_j1: "?tps ! j1 = (⌊xs⌋, Suc t)" using assms(1-3,5) by simp have tps_j2: "?tps ! j2 = (⌊map (sumdigit xs ys) [0..<t] @ drop t ys⌋, Suc t)" using assms(1-3,5) by simp have tps_last: "last ?tps = ⌈carry xs ys t⌉" using assms by (metis One_nat_def carry.simps(1) diff_Suc_1 last_list_update length_list_update list_update_nonempty prod.sel(2) tps_j1) thenhave"sem (cmd_plus j1 j2) (0, ?tps) = (if Suc t ≤ max (length xs) (length ys) then 0 else 1, ?tps')" using sem_cmd_plus'[OF assms(1-4) tps_k assms(6,7) tps_j1 tps_j2 tps_last] assms(1-3) by (smt (verit, best) Suc.prems Suc_lessD assms(5) tps_k) thenhave"sem (cmd_plus j1 j2) ?cfg = (if Suc t ≤ max (length xs) (length ys) then 0 else 1, ?tps')" using cfg by simp moreoverhave"?tps' = tps [j1 := (⌊xs⌋, Suc (Suc t)), j2 := (⌊map (sumdigit xs ys) [0..<Suc t] @ drop (Suc t) ys⌋, Suc (Suc t)), length tps - 1 := ⌈carry xs ys (Suc t)⌉]" using assms by (smt (verit) list_update_overwrite list_update_swap) ultimatelyshow ?thesis by simp qed finallyshow ?case by simp qed
lemma tm_plus_bounded_write: assumes"j1 < k - 1" shows"bounded_write (tm_plus j1 j2) (k - 1) 4" using assms cmd_plus_def tm_plus_def bounded_write_def by simp
lemma carry_max_length: assumes"bit_symbols xs"and"bit_symbols ys" shows"carry xs ys (Suc (max (length xs) (length ys))) = 0" proof - let ?t = "max (length xs) (length ys)" have"carry xs ys (Suc ?t) = tosym ((todigit (digit xs ?t) + todigit (digit ys ?t) + todigit (carry xs ys ?t)) div 2)" by simp thenhave"carry xs ys (Suc ?t) = tosym (todigit (carry xs ys ?t) div 2)" using digit_def by simp moreoverhave"carry xs ys ?t ≤1" using carry_le assms by fastforce ultimatelyshow ?thesis by simp qed
have1: "length ?tps = Suc k" using assms(5) by simp have2: "?tps ! j1 = (⌊xs⌋, 1)" by (simp add: assms(9) assms(2) assms(5) nth_append) have3: "?tps ! j2 = (⌊ys⌋, 1)" by (simp add: assms(10) assms(3) assms(5) nth_append) have4: "last ?tps = ⌈▹⌉" by simp have5: "k ≥ 2" using assms(3,4) by simp have"transforms (tm_plus j1 j2) ?tps t ?tps'" using transforms_tm_plusI[OF assms(1) _ _ assms(4) 1 assms(6,7,8) 234, of ?tps'] assms(2,3) by simp moreoverhave"?tps' = tps' @ [⌈0⌉]" using assms by (simp add: list_update_append) ultimatelyhave"transforms (tm_plus j1 j2) (tps @ [⌈▹⌉]) t (tps' @ [⌈0⌉])" by simp moreoverhave"turing_machine (Suc k) 4 ?M" using tm_plus_tm assms by simp moreoverhave"immobile ?M k (Suc k)" using tm_plus_immobile assms by simp moreoverhave"bounded_write (tm_plus j1 j2) k 4" using tm_plus_bounded_write[of j1 "Suc k"] assms(2) by simp ultimatelyhave"transforms (cartesian (tm_plus j1 j2) 4) tps t tps'" using cartesian_transforms_onesie[where ?M="?M"and ?b=4] assms(5) 5 by simp thenshow ?thesis using tm_plus'_defby simp qed
text‹
next Turing machine is the one we actually use to add two numbers. After
the sum by running @{const tm_plus'}, it removes trailing zeros
performs a carriage return on the tapes $j_1$ and $j_2$. ›
lemma contents_canlen: assumes"bit_symbols zs" shows"⌊zs⌋ (canlen zs) ∈ {h. h ≠0∧◻ < h}" using assms contents_def canlen_le_length canlen_one by auto
lemma tm2 [transforms_intros]: assumes"ttt = n + Suc (Suc n - canlen (map (sumdigit xs ys) [0..<n]))" shows"transforms tm2 tps0 ttt tps2" unfolding tm2_def proof (tform tps: tps1_def jk xs ys tps0) let ?zs = "map (sumdigit xs ys) [0..<n]" have"bit_symbols ?zs" using sumdigit_bit_symbols by blast let ?ln = "Suc n - canlen ?zs" have"lneigh (⌊?zs⌋, Suc n) {h. h ≠0∧◻ < h} ?ln" proof (rule lneighI) have"⌊?zs⌋ (canlen ?zs) ∈ {h. h ≠0∧◻ < h}" using contents_canlen[OF `bit_symbols ?zs`] by simp moreoverhave"Suc n - ?ln = canlen ?zs" by (metis One_nat_def diff_Suc_1 diff_Suc_Suc diff_diff_cancel le_imp_less_Suc
length_map length_upt less_imp_le_nat canlen_le_length) ultimatelyhave"⌊?zs⌋ (Suc n - ?ln) ∈ {h. h ≠0∧◻ < h}" by simp thenshow"fst (⌊?zs⌋, Suc n) (snd (⌊?zs⌋, Suc n) - ?ln) ∈ {h. h ≠0∧◻ < h}" by simp
have"⌊?zs⌋ (Suc n - n') ∈ {◻, 0}"if"n' < ?ln"for n' proof (cases "Suc n - n' ≤ n") case True moreoverhave1: "Suc n - n' > 0" using that by simp ultimatelyhave"⌊?zs⌋ (Suc n - n') = ?zs ! (Suc n - n' - 1)" using contents_def by simp moreoverhave"Suc n - n' - 1 < length ?zs" using that True by simp moreoverhave"Suc n - n' - 1 ≥ canlen ?zs" using that by simp ultimatelyshow ?thesis using canlen_at_ge[of ?zs] by simp next case False thenshow ?thesis by simp qed thenhave"⌊?zs⌋ (Suc n - n') ∉ {h. h ≠0∧◻ < h}"if"n' < ?ln"for n' using that by fastforce thenshow"fst (⌊?zs⌋, Suc n) (snd (⌊?zs⌋, Suc n) - n') ∉ {h. h ≠0∧◻ < h}" if"n' < ?ln"for n' using that by simp qed thenshow"lneigh (tps1 ! j2) {h. h ≠0∧ h ≠◻} ?ln" using assms tps1_def jk by simp show"Suc n - canlen (map (sumdigit xs ys) [0..<n]) ≤ tps1 :#: j2" "Suc n - canlen (map (sumdigit xs ys) [0..<n]) ≤ tps1 :#: j2" using assms tps1_def jk by simp_all
have num_zs: "num ?zs = num xs + num ys" using assms num_sumdigit_eq_sum'' xs ys by simp thenhave canrepr: "canrepr (num xs + num ys) = take (canlen ?zs) ?zs" using canrepr_take_canlen `bit_symbols ?zs` by blast have len_canrepr: "length (canrepr (num xs + num ys)) = canlen ?zs" using num_zs length_canrepr_canlen sumdigit_bit_symbols by blast
have"lconstplant (⌊?zs⌋, Suc n) ◻ ?ln = (⌊canrepr (num xs + num ys)⌋, m)"
(is"lconstplant ?tp ◻ ?ln = _") proof - have"(if Suc n - ?ln < i ∧ i ≤ Suc n then ◻ else ⌊?zs⌋ i) = ⌊take (canlen ?zs) ?zs⌋ i"
(is"?lhs = ?rhs") for i proof -
consider "i = 0"
| "i > 0 ∧ i ≤ canlen ?zs"
| "i > canlen ?zs ∧ i ≤ Suc n"
| "i > canlen ?zs ∧ i > Suc n" by linarith thenshow ?thesis proof (cases) case1 thenshow ?thesis by simp next case2 thenhave"i ≤ Suc n - ?ln" using canlen_le_length by (metis diff_diff_cancel diff_zero le_imp_less_Suc length_map length_upt less_imp_le_nat) thenhave lhs: "?lhs = ⌊?zs⌋ i" by simp have"take (canlen ?zs) ?zs ! (i - 1) = ?zs ! (i - 1)" using2by (metis Suc_diff_1 Suc_less_eq le_imp_less_Suc nth_take) thenhave"?rhs = ⌊?zs⌋ i" using2 contents_inbounds len_canrepr local.canrepr not_le canlen_le_length by (metis add_diff_inverse_nat add_leE) thenshow ?thesis using lhs by simp next case3 thenhave"Suc n - ?ln < i ∧ i ≤ Suc n" by (metis diff_diff_cancel less_imp_le_nat less_le_trans) thenhave"?lhs = 0" by simp moreoverhave"?rhs = 0" using3 contents_outofbounds len_canrepr canrepr by metis ultimatelyshow ?thesis by simp next case4 thenhave"?lhs = 0" by simp moreoverhave"?rhs = 0" using4 contents_outofbounds len_canrepr canrepr by metis ultimatelyshow ?thesis by simp qed qed thenhave"(λi. if Suc n - ?ln < i ∧ i ≤ Suc n then ◻ else ⌊?zs⌋ i) = ⌊canrepr (num xs + num ys)⌋" using canrepr by simp moreoverhave"fst ?tp = ⌊?zs⌋" by simp ultimatelyhave"(λi. if Suc n - ?ln < i ∧ i ≤ Suc n then 0 else fst ?tp i) = ⌊canrepr (num xs + num ys)⌋"by metis moreoverhave"Suc n - ?ln = m" using len_canrepr by (metis add_diff_inverse_nat diff_add_inverse2 diff_is_0_eq diff_zero le_imp_less_Suc length_map
length_upt less_imp_le_nat less_numeral_extra(3) canlen_le_length zero_less_diff) ultimatelyshow ?thesis using lconstplant[of ?tp 0 ?ln] by simp qed thenshow"tps2 = tps1 [j2 := tps1 ! j2 |-| ?ln, j2 := lconstplant (tps1 ! j2) 0 ?ln]" using tps2_def tps1_def jk by simp
lemma tm4: assumes"ttt = n + Suc (Suc n - canlen (map (sumdigit xs ys) [0..<n])) + Suc n + 2 + m + 2" shows"transforms tm4 tps0 ttt tps4" unfolding tm4_def proof (tform tps: tps3_def jk xs ys tps0 time: assms tps3_def jk) show"clean_tape (tps3 ! j2)" using tps3_def tps2_def jk tps0(1) by (metis clean_tape_ncontents list_update_id nth_list_update_eq) show"tps4 = tps3[j2 := tps3 ! j2 |#=| 1]" using tps4_def tps3_def jk by simp qed
lemma tm4': assumes"ttt = 3 * max (length xs) (length ys) + 10" shows"transforms tm4 tps0 ttt tps4" proof - let ?zs = "map (sumdigit xs ys) [0..<n]" have"num ?zs = num xs + num ys" using num_sumdigit_eq_sum'' xs ys by simp thenhave1: "length (canrepr (num xs + num ys)) = canlen ?zs" using length_canrepr_canlen sumdigit_bit_symbols by blast moreoverhave"length ?zs = n" by simp ultimatelyhave"m ≤ n" by (metis canlen_le_length)
have"n + Suc (Suc n - canlen ?zs) + Suc n + 2 + m + 2 = n + Suc (Suc n - m) + Suc n + 2 + m + 2" using1by simp alsohave"... = n + Suc (Suc n - m) + Suc n + 4 + m" by simp alsohave"... = n + Suc (Suc n) - m + Suc n + 4 + m" using `m ≤ n` by simp alsohave"... = n + Suc (Suc n) + Suc n + 4" using `m ≤ n` by simp alsohave"... = 3 * n + 7" by simp alsohave"... = ttt" using assms by simp finallyhave"n + Suc (Suc n - canlen ?zs) + Suc n + 2 + m + 2 = ttt" . thenshow ?thesis using tm4 by simp qed
definition"tps4' ≡ tps0 [j2 := (⌊x + y⌋N, 1)]"
lemma tm4'': assumes"ttt = 3 * max (nlength x) (nlength y) + 10" shows"transforms tm4 tps0 ttt tps4'" proof - have"canrepr (num xs + num ys) = canrepr (x + y)" by (simp add: canrepr) thenshow ?thesis using assms tps0(1) tps4'_def tps4_def tm4' by (metis list_update_id) qed
text‹
this section we construct a Turing machine that multiplies two numbers, each
its own tape, and writes the result to another tape. It employs the common
for multiplication, which for binary numbers requires only doubling a
and adding two numbers. For the latter we already have a TM; for the
we are going to construct one. ›
subsubsection‹The common algorithm›
text‹
two numbers given as symbol sequences @{term xs} and @{term ys}, the common
maintains an intermediate result, initialized with 0, and scans @{term
} starting from the most significant digit. In each step the intermediate
is multiplied by two, and if the current digit of @{term xs} is @{text 1}, the value of @{term ys} is added to the intermediate result. ›
fun prod :: "symbol list ==> symbol list ==> nat ==> nat"where "prod xs ys 0 = 0" | "prod xs ys (Suc i) = 2 * prod xs ys i + (if xs ! (length xs - 1 - i) = 3 then num ys else 0)"
text‹
$i$ steps of the algorithm, the intermediate result is the product of @{term ys}
the $i$ most significant bits of @{term xs}. ›
lemma prod: assumes"i ≤ length xs" shows"prod xs ys i = num (drop (length xs - i) xs) * num ys" using assms proof (induction i) case0 thenshow ?case using num_def by simp next case (Suc i) thenhave"i < length xs" by simp thenhave"drop (length xs - Suc i) xs = (xs ! (length xs - 1 - i)) # drop (length xs - i) xs" by (metis Cons_nth_drop_Suc Suc_diff_Suc diff_Suc_eq_diff_pred
diff_Suc_less gr_implies_not0 length_greater_0_conv list.size(3)) thenshow ?case using num_Cons Suc by simp qed
text‹
@{term "length xs"} steps, the intermediate result is the final result: ›
corollary prod_eq_prod: "prod xs ys (length xs) = num xs * num ys" using prod by simp
definition prod' :: "nat ==> nat ==> nat ==> nat"where "prod' x y i ≡ prod (canrepr x) (canrepr y) i"
lemma prod': "prod' x y (nlength x) = x * y" using prod_eq_prod prod'_defby (simp add: canrepr)
subsubsection‹Multiplying by two›
text‹
we represent numbers with the least significant bit at the left, a
by two is a right shift with a \textbf{0} inserted as the least
digit. The next command implements the right shift. It scans the
$j$ and memorizes the current symbol on the last tape. It only writes the \textbf{0} and \textbf{1}. ›
definition cmd_double :: "tapeidx ==> command"where "cmd_double j rs ≡ (if rs ! j = ◻ then 1 else 0, (map (λi. if i = j then if last rs = ▹∧ rs ! j = ◻ then (rs ! i, Right) else (tosym (todigit (last rs)), Right) else if i = length rs - 1 then (tosym (todigit (rs ! j)), Stay) else (rs ! i, Stay)) [0..<length rs]))"
lemma turing_command_double: assumes"k ≥ 2"and"G ≥ 4"and"j > 0"and"j < k - 1" shows"turing_command k 1 G (cmd_double j)" proof show"∧gs. length gs = k ==> length ([!!] cmd_double j gs) = length gs" using cmd_double_def by simp show"∧gs. length gs = k ==> 0 < k ==> cmd_double j gs [.] 0 = gs ! 0" using assms cmd_double_def by simp show"cmd_double j gs [.] j' < G" if"length gs = k""∧i. i < length gs ==> gs ! i < G""j' < length gs" for j' gs proof -
consider "j' = j" | "j' = k - 1" | "j' ≠ j ∧ j' ≠ k - 1" by auto thenshow ?thesis proof (cases) case1 thenhave"cmd_double j gs [!] j' = (if last gs = ▹∧ gs ! j = ◻ then (gs ! j, Right) else (tosym (todigit (last gs)), Right))" using cmd_double_def assms(1,4) that(1) by simp thenhave"cmd_double j gs [.] j' = (if last gs = ▹∧ gs ! j = ◻ then gs ! j else tosym (todigit (last gs)))" by simp thenshow ?thesis using that assms by simp next case2 thenhave"cmd_double j gs [!] j' = (tosym (todigit (gs ! j)), Stay)" using cmd_double_def assms(1,4) that(1) by simp thenshow ?thesis using assms by simp next case3 thenshow ?thesis using cmd_double_def assms that by simp qed qed show"∧gs. length gs = k ==> [*] (cmd_double j gs) ≤ 1" using assms cmd_double_def by simp qed
lemma sem_cmd_double_0: assumes"j < k" and"bit_symbols xs" and"i ≤ length xs" and"i > 0" and"length tps = Suc k" and"tps ! j = (⌊xs⌋, i)" and"tps ! k = ⌈z⌉" and"tps' = tps [j := tps ! j |:=| tosym (todigit z) |+| 1, k := ⌈xs ! (i - 1)⌉]" shows"sem (cmd_double j) (0, tps) = (0, tps')" proof (rule semI) show"proper_command (Suc k) (cmd_double j)" using cmd_double_def by simp show"length tps = Suc k" using assms(5) . show"length tps' = Suc k" using assms(5,8) by simp show"fst (cmd_double j (read tps)) = 0" using assms contents_def cmd_double_def tapes_at_read'[of j tps] by (smt (verit, del_insts) One_nat_def Suc_le_lessD Suc_le_mono Suc_pred fst_conv
less_imp_le_nat snd_conv zero_neq_numeral) show"act (cmd_double j (read tps) [!] j') (tps ! j') = tps' ! j'" if"j' < Suc k"for j' proof - define rs where"rs = read tps" thenhave rsj: "rs ! j = xs ! (i - 1)" using assms tapes_at_read' contents_inbounds by (metis fst_conv le_imp_less_Suc less_imp_le_nat snd_conv) thenhave rs23: "rs ! j = 0∨ rs ! j = 1" using assms by simp have lenrs: "length rs = Suc k" by (simp add: rs_def assms(5) read_length)
consider "j' = j" | "j' = k" | "j' ≠ j ∧ j' ≠ k" by auto thenshow ?thesis proof (cases) case1 thenhave"j' < length rs" using lenrs that by simp thenhave"cmd_double j rs [!] j' = (if last rs = ▹∧ rs ! j = ◻ then (rs ! j, Right) else (tosym (todigit (last rs)), Right))" using cmd_double_def that 1by simp thenhave"cmd_double j rs [!] j' = (tosym (todigit (last rs)), Right)" using rs23 lenrs assms by auto moreoverhave"last rs = z" using lenrs assms(5,7) rs_def onesie_read[of z] tapes_at_read'[of _ tps] by (metis diff_Suc_1 last_conv_nth length_0_conv lessI old.nat.distinct(2)) ultimatelyshow ?thesis using act_Right' rs_def 1 assms(1,5,8) by simp next case2 thenhave"j' = length rs - 1""j' ≠ j""j' < length rs" using lenrs that assms(1) by simp_all thenhave"(cmd_double j rs) [!] j' = (tosym (todigit (rs ! j)), Stay)" using cmd_double_def by simp thenhave"(cmd_double j rs) [!] j' = (xs ! (i - 1), Stay)" using rsj rs23 by auto thenshow ?thesis using act_onesie rs_def 2 assms that by simp next case3 thenhave"j' ≠ length rs - 1""j' ≠ j""j' < length rs" using lenrs that by simp_all thenhave"(cmd_double j rs) [!] j' = (rs ! j', Stay)" using cmd_double_def by simp thenshow ?thesis using act_Stay rs_def assms that 3by simp qed qed qed
lemma sem_cmd_double_1: assumes"j < k" and"bit_symbols xs" and"i > length xs" and"length tps = Suc k" and"tps ! j = (⌊xs⌋, i)" and"tps ! k = ⌈z⌉" and"tps' = tps [j := tps ! j |:=| (if z = ▹ then ◻ else tosym (todigit z)) |+| 1, k := ⌈0⌉]" shows"sem (cmd_double j) (0, tps) = (1, tps')" proof (rule semI) show"proper_command (Suc k) (cmd_double j)" using cmd_double_def by simp show"length tps = Suc k" using assms(4) . show"length tps' = Suc k" using assms(4,7) by simp show"fst (cmd_double j (read tps)) = 1" using assms contents_def cmd_double_def tapes_at_read'[of j tps] by simp have"j < length tps" using assms by simp show"act (cmd_double j (read tps) [!] j') (tps ! j') = tps' ! j'" if"j' < Suc k"for j' proof - define rs where"rs = read tps" thenhave rsj: "rs ! j = ◻" using tapes_at_read'[OF `j < length tps`] assms(1,3,4,5) by simp have lenrs: "length rs = Suc k" by (simp add: rs_def assms(4) read_length)
consider "j' = j" | "j' = k" | "j' ≠ j ∧ j' ≠ k" by auto thenshow ?thesis proof (cases) case1 thenhave"j' < length rs" using lenrs that by simp thenhave"cmd_double j rs [!] j' = (if last rs = ▹∧ rs ! j = ◻ then (rs ! j, Right) else (tosym (todigit (last rs)), Right))" using cmd_double_def that 1by simp moreoverhave"last rs = z" using assms onesie_read rs_def tapes_at_read' by (metis diff_Suc_1 last_conv_nth length_0_conv lenrs lessI nat.simps(3)) ultimatelyhave"cmd_double j rs [!] j' = (if z = ▹ then (◻, Right) else (tosym (todigit z), Right))" using rsj 1by simp thenshow ?thesis using act_Right' rs_def 1 assms(1,4,7) by simp next case2 thenhave"j' = length rs - 1""j' ≠ j""j' < length rs" using lenrs that assms(1) by simp_all thenhave"(cmd_double j rs) [!] j' = (tosym (todigit (rs ! j)), Stay)" using cmd_double_def by simp thenhave"(cmd_double j rs) [!] j' = (2, Stay)" using rsj by auto thenshow ?thesis using act_onesie rs_def 2 assms that by simp next case3 thenhave"j' ≠ length rs - 1""j' ≠ j""j' < length rs" using lenrs that by simp_all thenhave"(cmd_double j rs) [!] j' = (rs ! j', Stay)" using cmd_double_def by simp thenshow ?thesis using act_Stay rs_def assms that 3by simp qed qed qed
text‹
next Turing machine consists just of the command @{const cmd_double}. ›
lemma tm_double_tm: assumes"k ≥ 2"and"G ≥ 4"and"j > 0"and"j < k - 1" shows"turing_machine k G (tm_double j)" using assms tm_double_def turing_command_double by auto
lemma execute_tm_double_0: assumes"j < k" and"bit_symbols xs" and"length xs > 0" and"length tps = Suc k" and"tps ! j = (⌊xs⌋, 1)" and"tps ! k = ⌈▹⌉" and"t ≥ 1" and"t ≤ length xs" shows"execute (tm_double j) (0, tps) t = (0, tps [j := (⌊0 # take (t - 1) xs @ drop t xs⌋, Suc t), k := ⌈xs ! (t - 1)⌉])" using assms(7,8) proof (induction t rule: nat_induct_at_least) case base have"execute (tm_double j) (0, tps) 1 = exe (tm_double j) (execute (tm_double j) (0, tps) 0)" by simp alsohave"... = sem (cmd_double j) (execute (tm_double j) (0, tps) 0)" using tm_double_def exe_lt_length by simp alsohave"... = sem (cmd_double j) (0, tps)" by simp alsohave"... = (0, tps [j := tps ! j |:=| tosym (todigit 1) |+| 1, k := ⌈xs ! (1 - 1)⌉])" using assms(7,8) sem_cmd_double_0[OF assms(1-2) _ _ assms(4,5,6)] by simp alsohave"... = (0, tps [j := (⌊0 # take (1 - 1) xs @ drop 1 xs⌋, Suc 1), k := ⌈xs ! (1 - 1)⌉])" proof - have"tps ! j |:=| tosym (todigit 1) |+| 1 = (⌊xs⌋, 1) |:=| tosym (todigit 1) |+| 1" using assms(5) by simp alsohave"... = (⌊xs⌋(1 := tosym (todigit 1)), Suc 1)" by simp alsohave"... = (⌊xs⌋(1 := 0), Suc 1)" by auto alsohave"... = (⌊0 # drop 1 xs⌋, Suc 1)" proof - have"⌊0 # drop 1 xs⌋ = ⌊xs⌋(1 := 0)" proof fix i :: nat
consider "i = 0" | "i = 1" | "i > 1 ∧ i ≤ length xs" | "i > length xs" by linarith thenshow"⌊0 # drop 1 xs⌋ i = (⌊xs⌋(1 := 0)) i" proof (cases) case1 thenshow ?thesis by simp next case2 thenshow ?thesis by simp next case3 thenhave"⌊0 # drop 1 xs⌋ i = (0 # drop 1 xs) ! (i - 1)" using assms(3) by simp alsohave"... = (drop 1 xs) ! (i - 2)" using3by (metis Suc_1 diff_Suc_eq_diff_pred nth_Cons_pos zero_less_diff) alsohave"... = xs ! (Suc (i - 2))" using3 assms(5) by simp alsohave"... = xs ! (i - 1)" using3by (metis Suc_1 Suc_diff_Suc) alsohave"... = ⌊xs⌋ i" using3by simp alsohave"... = (⌊xs⌋(1 := 0)) i" using3by simp finallyshow ?thesis . next case4 thenshow ?thesis by simp qed qed thenshow ?thesis by simp qed alsohave"... = (⌊0 # take (1 - 1) xs @ drop 1 xs⌋, Suc 1)" by simp finallyshow ?thesis by auto qed finallyshow ?case . next case (Suc t) let ?xs = "0 # take (t - 1) xs @ drop t xs" let ?z = "xs ! (t - 1)" let ?tps = "tps [j := (⌊?xs⌋, Suc t), k := ⌈?z⌉]" have lenxs: "length ?xs = length xs" using Suc by simp have0: "?xs ! t = xs ! t" proof - have"t > 0" using Suc by simp thenhave"length (0 # take (t - 1) xs) = t" using Suc by simp moreoverhave"length (drop t xs) > 0" using Suc by simp moreoverhave"drop t xs ! 0 = xs ! t" using Suc by simp ultimatelyhave"((0 # take (t - 1) xs) @ drop t xs) ! t = xs ! t" by (metis diff_self_eq_0 less_not_refl3 nth_append) thenshow ?thesis by simp qed have1: "bit_symbols ?xs" proof - have"bit_symbols (take (t - 1) xs)" using assms(2) by simp moreoverhave"bit_symbols (drop t xs)" using assms(2) by simp moreoverhave"bit_symbols [0]" by simp ultimatelyhave"bit_symbols ([0] @ take (t - 1) xs @ drop t xs)" using bit_symbols_append by presburger thenshow ?thesis by simp qed have2: "Suc t ≤ length ?xs" using Suc by simp have3: "Suc t > 0" using Suc by simp have4: "length ?tps = Suc k" using assms by simp have5: "?tps ! j = (⌊?xs⌋, Suc t)" by (simp add: Suc_lessD assms(1,4) nat_neq_iff) have6: "?tps ! k = ⌈?z⌉" by (simp add: assms(4)) have"execute (tm_double j) (0, tps) (Suc t) = exe (tm_double j) (execute (tm_double j) (0, tps) t)" by simp alsohave"... = sem (cmd_double j) (execute (tm_double j) (0, tps) t)" using tm_double_def exe_lt_length Suc by simp alsohave"... = sem (cmd_double j) (0, ?tps)" using Suc by simp alsohave"... = (0, ?tps [j := ?tps ! j |:=| tosym (todigit ?z) |+| 1, k := ⌈?xs ! (Suc t - 1)⌉])" using sem_cmd_double_0[OF assms(1) 123456] by simp alsohave"... = (0, ?tps [j := ?tps ! j |:=| tosym (todigit ?z) |+| 1, k := ⌈xs ! (Suc t - 1)⌉])" using0by simp alsohave"... = (0, tps [j := ?tps ! j |:=| tosym (todigit ?z) |+| 1, k := ⌈xs ! (Suc t - 1)⌉])" using assms by (smt (verit) list_update_overwrite list_update_swap) alsohave"... = (0, tps [j := (⌊?xs⌋, Suc t) |:=| tosym (todigit ?z) |+| 1, k := ⌈xs ! (Suc t - 1)⌉])" using5by simp alsohave"... = (0, tps [j := (⌊?xs⌋(Suc t := tosym (todigit ?z)), Suc (Suc t)), k := ⌈xs ! (Suc t - 1)⌉])" by simp alsohave"... = (0, tps [j := (⌊2 # take (Suc t - 1) xs @ drop (Suc t) xs⌋, Suc (Suc t)), k := ⌈xs ! (Suc t - 1)⌉])" proof - have"⌊?xs⌋(Suc t := tosym (todigit ?z)) = ⌊0 # take (Suc t - 1) xs @ drop (Suc t) xs⌋" proof fix i :: nat
consider "i = 0" | "i > 0 ∧ i < Suc t" | "i = Suc t" | "i > Suc t ∧ i ≤ length xs" | "i > length xs" by linarith thenshow"(⌊?xs⌋(Suc t := tosym (todigit ?z))) i = ⌊0 # take (Suc t - 1) xs @ drop (Suc t) xs⌋ i" proof (cases) case1 thenshow ?thesis by simp next case2 thenhave lhs: "(⌊?xs⌋(Suc t := tosym (todigit ?z))) i = ?xs ! (i - 1)" using lenxs Suc by simp have"⌊0 # take (Suc t - 1) xs @ drop (Suc t) xs⌋ i = (0 # take (Suc t - 1) xs @ drop (Suc t) xs) ! (i - 1)" using Suc 2by auto thenhave"⌊0 # take (Suc t - 1) xs @ drop (Suc t) xs⌋ i = ((0 # take (Suc t - 1) xs) @ drop (Suc t) xs) ! (i - 1)" by simp moreoverhave"length (0 # take (Suc t - 1) xs) = Suc t" using Suc.prems by simp ultimatelyhave"⌊0 # take (Suc t - 1) xs @ drop (Suc t) xs⌋ i = (0 # take (Suc t - 1) xs) ! (i - 1)" using2by (metis Suc_diff_1 Suc_lessD nth_append) alsohave"... = (0 # take t xs) ! (i - 1)" by simp alsohave"... = (0 # take (t - 1) xs @ [xs ! (t - 1)]) ! (i - 1)" using Suc by (metis Suc_diff_le Suc_le_lessD Suc_lessD diff_Suc_1 take_Suc_conv_app_nth) alsohave"... = ((0 # take (t - 1) xs) @ [xs ! (t - 1)]) ! (i - 1)" by simp alsohave"... = (0 # take (t - 1) xs) ! (i - 1)" using2 Suc by (metis One_nat_def Suc_leD Suc_le_eq Suc_pred length_Cons length_take less_Suc_eq_le
min_absorb2 nth_append) alsohave"... = ((0 # take (t - 1) xs) @ drop t xs) ! (i - 1)" using2 Suc by (metis Suc_diff_1 Suc_diff_le Suc_leD Suc_lessD diff_Suc_1 length_Cons length_take
less_Suc_eq min_absorb2 nth_append) alsohave"... = ?xs ! (i - 1)" by simp finallyhave"⌊0 # take (Suc t - 1) xs @ drop (Suc t) xs⌋ i = ?xs ! (i - 1)" . thenshow ?thesis using lhs by simp next case3 moreoverhave"?z = 0∨ ?z = 1" using `bit_symbols ?xs` Suc assms(2) by (metis Suc_diff_le Suc_leD Suc_le_lessD diff_Suc_1) ultimatelyhave lhs: "(⌊?xs⌋(Suc t := tosym (todigit ?z))) i = ?z" by auto have"⌊0 # take (Suc t - 1) xs @ drop (Suc t) xs⌋ i = ⌊(0 # take t xs) @ drop (Suc t) xs⌋ (Suc t)" using3by simp alsohave"... = ((0 # take t xs) @ drop (Suc t) xs) ! t" using3 Suc by simp alsohave"... = (0 # take t xs) ! t" using Suc by (metis Suc_leD length_Cons length_take lessI min_absorb2 nth_append) alsohave"... = xs ! (t - 1)" using Suc by simp finallyhave"⌊0 # take (Suc t - 1) xs @ drop (Suc t) xs⌋ i = ?z" . thenshow ?thesis using lhs by simp next case4 thenhave"(⌊?xs⌋(Suc t := tosym (todigit ?z))) i = ⌊?xs⌋ i" by simp alsohave"... = ?xs ! (i - 1)" using4by auto alsohave"... = ((0 # take (t - 1) xs) @ drop t xs) ! (i - 1)" by simp alsohave"... = drop t xs ! (i - 1 - t)" using4 Suc by (smt (verit, ccfv_threshold) Cons_eq_appendI Suc_diff_1 Suc_leD
add_diff_cancel_right' bot_nat_0.extremum_uniqueI diff_diff_cancel
length_append length_drop lenxs not_le not_less_eq nth_append) alsohave"... = xs ! (i - 1)" using4 Suc by simp finallyhave lhs: "(⌊?xs⌋(Suc t := tosym (todigit ?z))) i = xs ! (i - 1)" . have"⌊0 # take (Suc t - 1) xs @ drop (Suc t) xs⌋ i = (0 # take (Suc t - 1) xs @ drop (Suc t) xs) ! (i - 1)" using4by auto alsohave"... = ((0 # take t xs) @ drop (Suc t) xs) ! (i - 1)" by simp alsohave"... = (drop (Suc t) xs) ! (i - 1 - Suc t)" using Suc 4 by (smt (verit) Suc_diff_1 Suc_leD Suc_leI bot_nat_0.extremum_uniqueI length_Cons length_take
min_absorb2 not_le nth_append) alsohave"... = xs ! (i - 1)" using Suc 4 Suc_lessE by fastforce finallyhave"⌊0 # take (Suc t - 1) xs @ drop (Suc t) xs⌋ i = xs ! (i - 1)" . thenshow ?thesis using lhs by simp next case5 thenhave"(⌊?xs⌋(Suc t := tosym (todigit ?z))) i = ⌊?xs⌋ i" using Suc by simp thenhave lhs: "(⌊?xs⌋(Suc t := tosym (todigit ?z))) i = ◻" using5 contents_outofbounds lenxs by simp have"length (0 # take (Suc t - 1) xs @ drop (Suc t) xs) = length xs" using Suc by simp thenhave"⌊0 # take (Suc t - 1) xs @ drop (Suc t) xs⌋ i = ◻" using5 contents_outofbounds by simp thenshow ?thesis using lhs by simp qed qed thenshow ?thesis by simp qed finallyshow ?case . qed
lemma execute_tm_double_1: assumes"j < k" and"bit_symbols xs" and"length xs > 0" and"length tps = Suc k" and"tps ! j = (⌊xs⌋, 1)" and"tps ! k = ⌈▹⌉" shows"execute (tm_double j) (0, tps) (Suc (length xs)) = (1, tps [j := (⌊0 # xs⌋, length xs + 2), k := ⌈0⌉])" proof - let ?z = "xs ! (length xs - 1)" let ?xs = "0 # take (length xs - 1) xs" have"?z ≠▹" using assms(2,3) by (metis One_nat_def Suc_1 diff_less less_Suc_eq not_less_eq numeral_3_eq_3) have z23: "?z = 0∨ ?z = 1" using assms(2,3) by (meson diff_less zero_less_one) have lenxs: "length ?xs = length xs" using assms(3) by (metis Suc_diff_1 diff_le_self length_Cons length_take min_absorb2) have0: "bit_symbols ?xs" using assms(2) bit_symbols_append[of "[0]""take (length xs - 1) xs"] by simp
have"execute (tm_double j) (0, tps) (length xs) = (0, tps [j := (⌊0 # take (length xs - 1) xs @ drop (length xs) xs⌋, Suc (length xs)), k := ⌈?z⌉])" using execute_tm_double_0[OF assms(1-6), where ?t="length xs"] assms(3) by simp thenhave *: "execute (tm_double j) (0, tps) (length xs) = (0, tps [j := (⌊?xs⌋, Suc (length ?xs)), k := ⌈?z⌉])"
(is"_ = (0, ?tps)") using lenxs by simp
let ?i = "Suc (length ?xs)" have1: "?i > length ?xs" by simp have2: "length ?tps = Suc k" using assms(4) by simp have3: "?tps ! j = (⌊?xs⌋, ?i)" using assms(1,4) by simp have4: "?tps ! k = ⌈?z⌉" using assms(4) by simp
have"execute (tm_double j) (0, tps) (Suc (length xs)) = exe (tm_double j) (0, ?tps)" using * by simp alsohave"... = sem (cmd_double j) (0, ?tps)" using tm_double_def exe_lt_length by simp alsohave"... = (1, ?tps [j := ?tps ! j |:=| (if ?z = ▹ then ◻ else tosym (todigit ?z)) |+| 1, k := ⌈0⌉])" using sem_cmd_double_1[OF assms(1) 01234] by simp alsohave"... = (1, ?tps [j := ?tps ! j |:=| (tosym (todigit ?z)) |+| 1, k := ⌈0⌉])" using `?z ≠1` by simp alsohave"... = (1, ?tps [j := (⌊?xs⌋, Suc (length ?xs)) |:=| (tosym (todigit ?z)) |+| 1, k := ⌈0⌉])" using3by simp alsohave"... = (1, ?tps [j := (⌊?xs⌋, Suc (length ?xs)) |:=| ?z |+| 1, k := ⌈0⌉])" using z23 One_nat_def Suc_1 add_2_eq_Suc' numeral_3_eq_3 by presburger alsohave"... = (1, tps [j := (⌊?xs⌋, Suc (length ?xs)) |:=| ?z |+| 1, k := ⌈0⌉])" by (smt (verit) list_update_overwrite list_update_swap) alsohave"... = (1, tps [j := (⌊?xs⌋(Suc (length ?xs) := ?z), length ?xs + 2), k := ⌈0⌉])" by simp alsohave"... = (1, tps [j := (⌊?xs⌋(Suc (length ?xs) := ?z), length xs + 2), k := ⌈0⌉])" using lenxs by simp alsohave"... = (1, tps [j := (⌊0 # xs⌋, length xs + 2), k := ⌈0⌉])" proof - have"⌊?xs⌋(Suc (length ?xs) := ?z) = ⌊0 # xs⌋" proof fix i
consider "i = 0" | "i > 0 ∧ i ≤ length xs" | "i = Suc (length xs)" | "i > Suc (length xs)" by linarith thenshow"(⌊?xs⌋(Suc (length ?xs) := ?z)) i = ⌊0 # xs⌋ i" proof (cases) case1 thenshow ?thesis by simp next case2 thenhave"(⌊?xs⌋(Suc (length ?xs) := ?z)) i = ⌊?xs⌋ i" using lenxs by simp alsohave"... = ?xs ! (i - 1)" using2by auto alsohave"... = (0 # xs) ! (i - 1)" using lenxs 2 assms(3) by (metis Suc_diff_1 Suc_le_lessD nth_take take_Suc_Cons) alsohave"... = ⌊0 # xs⌋ i" using2by simp finallyshow ?thesis . next case3 thenhave lhs: "(⌊?xs⌋(Suc (length ?xs) := ?z)) i = ?z" using lenxs by simp have"⌊0 # xs⌋ i = (0 # xs) ! (i - 1)" using3 lenxs by simp alsohave"... = xs ! (i - 2)" using3 assms(3) by simp alsohave"... = ?z" using3by simp finallyhave"⌊0 # xs⌋ i = ?z" . thenshow ?thesis using lhs by simp next case4 thenshow ?thesis using4 lenxs by simp qed qed thenshow ?thesis by simp qed finallyshow ?thesis . qed
lemma execute_tm_double_Nil: assumes"j < k" and"length tps = Suc k" and"tps ! j = (⌊[]⌋, 1)" and"tps ! k = ⌈▹⌉" shows"execute (tm_double j) (0, tps) (Suc 0) = (1, tps [j := (⌊[]⌋, 2), k := ⌈0⌉])" proof - have"execute (tm_double j) (0, tps) (Suc 0) = exe (tm_double j) (execute (tm_double j) (0, tps) 0)" by simp alsohave"... = exe (tm_double j) (0, tps)" by simp alsohave"... = sem (cmd_double j) (0, tps)" using tm_double_def exe_lt_length by simp alsohave"... = (1, tps [j := tps ! j |:=| (if (1::nat) = 1 then 0 else tosym (todigit 1)) |+| 1, k := ⌈0⌉])" using sem_cmd_double_1[OF assms(1) _ _ assms(2-4)] by simp alsohave"... = (1, tps [j := tps ! j |:=| ◻ |+| 1, k := ⌈0⌉])" by simp alsohave"... = (1, tps [j := (⌊[]⌋, 1) |:=| ◻ |+| 1, k := ⌈0⌉])" using assms(3) by simp alsohave"... = (1, tps [j := (⌊[]⌋(1 := ◻), 2), k := ⌈0⌉])" by (metis fst_eqD one_add_one snd_eqD) alsohave"... = (1, tps [j := (⌊[]⌋, 2), k := ⌈0⌉])" by (metis contents_outofbounds fun_upd_idem_iff list.size(3) zero_less_one) finallyshow ?thesis . qed
lemma execute_tm_double: assumes"j < k" and"length tps = Suc k" and"tps ! j = (⌊canrepr n⌋, 1)" and"tps ! k = ⌈▹⌉" shows"execute (tm_double j) (0, tps) (Suc (length (canrepr n))) = (1, tps [j := (⌊canrepr (2 * n)⌋, length (canrepr n) + 2), k := ⌈0⌉])" proof (cases "n = 0") case True thenhave"canrepr n = []" using canrepr_0 by simp thenshow ?thesis using execute_tm_double_Nil[OF assms(1-2) _ assms(4)] assms(3) True by (metis add_2_eq_Suc' list.size(3) mult_0_right numeral_2_eq_2) next case False let ?xs = "canrepr n" have"num (0 # ?xs) = 2 * num ?xs" using num_Cons by simp thenhave"num (0 # ?xs) = 2 * n" using canrepr by simp moreoverhave"canonical (0 # ?xs)" proof - have"?xs ≠ []" using False canrepr canrepr_0 by metis thenshow ?thesis using canonical_Cons canonical_canrepr by simp qed ultimatelyhave"canrepr (2 * n) = 0 # ?xs" using canreprI by blast thenshow ?thesis using execute_tm_double_1[OF assms(1) _ _ assms(2) _ assms(4)] assms(3) False canrepr canrepr_0 bit_symbols_canrepr by (metis length_greater_0_conv) qed
lemma execute_tm_double_app: assumes"j < k" and"length tps = k" and"tps ! j = (⌊canrepr n⌋, 1)" shows"execute (tm_double j) (0, tps @ [⌈▹⌉]) (Suc (length (canrepr n))) = (1, tps [j := (⌊canrepr (2 * n)⌋, length (canrepr n) + 2)] @ [⌈0⌉])" proof - let ?tps = "tps @ [⌈▹⌉]" have"length ?tps = Suc k" using assms(2) by simp moreoverhave"?tps ! j = (⌊canrepr n⌋, 1)" using assms(1,2,3) by (simp add: nth_append) moreoverhave"?tps ! k = ⌈▹⌉" using assms(2) by (simp add: nth_append) moreoverhave"tps [j := (⌊canrepr (2 * n)⌋, length (canrepr n) + 2)] @ [⌈0⌉] = ?tps [j := (⌊canrepr (2 * n)⌋, length (canrepr n) + 2), k := ⌈0⌉]" using assms by (metis length_list_update list_update_append1 list_update_length) ultimatelyshow ?thesis using assms execute_tm_double[OF assms(1), where ?tps="tps @ [⌈▹⌉]"] by simp qed
text‹
we can multiply arbitrary numbers we need just a few more lemmas.
null ›
lemma num_drop_le_nu: "num (drop j xs) ≤ num xs" proof (cases "j ≤ length xs") case True let ?ys = "drop j xs" have map_shift_upt: "map (λi. f (j + i)) [0..<l] = map f [j..<j + l]" for f :: "nat ==> nat"and j l by (rule nth_equalityI) simp_all
lemma nlength_prod_le_prod: assumes"i ≤ length xs" shows"nlength (prod xs ys i) ≤ nlength (num xs * num ys)" using prod[OF assms] num_drop_le_nu mult_le_mono1 nlength_mono by simp
corollary nlength_prod'_le_prod: assumes"i ≤ nlength x" shows"nlength (prod' x y i) ≤ nlength (x * y)" using assms prod'_def nlength_prod_le_prod by (metis prod' prod_eq_prod)
lemma two_times_prod: assumes"i < length xs" shows"2 * prod xs ys i ≤ num xs * num ys" proof - have"2 * prod xs ys i ≤ prod xs ys (Suc i)" by simp alsohave"... = num (drop (length xs - Suc i) xs) * num ys" using prod[of "Suc i" xs] assms by simp alsohave"... ≤ num xs * num ys" using num_drop_le_nu by simp finallyshow ?thesis . qed
corollary two_times_prod': assumes"i < nlength x" shows"2 * prod' x y i ≤ x * y" using assms two_times_prod prod'_defby (metis prod' prod_eq_prod)
text‹
next Turing machine multiplies the numbers on tapes $j_1$ and $j_2$ and
the result to tape $j_3$. It iterates over the binary digits on $j_1$
from the most significant digit. In each iteration it doubles the
result on $j_3$. If the current digit is @{text 1}, the number on
j_2$ is added to $j_3$. ›
lemma tm4_eq_tm_mult: "tm4 = tm_mult j1 j2 j3" using tm1_def tm2_def tm3_def tm4_def tm_mult_def tmIf_def tmBody_def tmBody1_def tmWhile_def by simp
context
x :and tps0 :: "tape list" assumes jk: "j1 ≠ j3""j3 <1 3 0" k" "j2 < k" "j3 < k" "length tps0 = k"
java.lang.StringIndexOutOfBoundsException: Index 32 out of bounds for length 15 "tps0j1x⌋N, 1)" "tps0 ! j2lfloory⌋N, 1)" "tps0 ! j3 \lfloor🚫 begin
inition <> N, Suc (nlength)]java.lang.StringIndexOutOfBoundsException: Index 86 out of bounds for length 86
[transforms_intros
nlength shows"transforms tm1 tps0 t tps1" unfoldingarbitrary proof : assmstps1_defjk) showtps0} (nlength x)" proof (rule rneighI) show "(tps0 ::: j1) (tps0 :#: j1 + nlength x) ∈java.lang.StringIndexOutOfBoundsException: Index 65 out of bounds for length 65
dd show usingewhe
ed qed
definition java.lang.NullPointerException
m2 [transforms_intro]: assumes "t = Suc (Suc (nlength x))" and "tps' = tps2" shows "transforms tm2 tps0 t tps'" unfolding tm2_def by (tform tps: assms tps1_def tps2_def jk)
definition "tpsL t <equiv
[j1bpT ∪n
j3 := (⌊java.lang.NullPointerException
definitionT represents T" [j1 := (⌊isis tht te
java.lang.NullPointerException
definition"tpsL3 t ≡ [j1 := (⌊x⌋N, nlength x - t - 1), j3 := (⌊prod' x y (Suc t)⌋MCn:: "==>KripkeStructure(*<*)(\<open>MC\<^bsub>_\<^esub>\<close>)(*>*) where
lemmalemma[intro assumes"t < nlength x"andttt 123 * nlength (x * y)" shows "transforms tmIf (tpsL1 unfolding
( tps tpsL1_def jk) have"nlength y ≤ jkbpC_def proof x> " using assms1)gr_implies_not_zeronlength_0 by auto then>jkbpC ⟷ set envInit" by simp show "nlength \> nlengthy" using nlength_mono by imp show "nlength using assms(1 y( ength_mono qed thenshow"3 * max (nlength y y) (nlength (2 * Arithmetic.prod' x y t)) + 10 + 2 \le ttt" using assms let ?xs = "canrepr x"and ?ys = "canrepr y" let ?r = "read (tpsL1 ssumes r repT: "represents have"?r = (⌊ using tpsL1_def jk tapes_at_read' by (metis fst_conv length_list_update list_update_swap nth_list_update_eq snd_conv) then have r: "? x ! (nlength1 - t" using assms contents_def by simp have "prod+ usingtext🚫‹ in "FHMV:1995"› alsohave"...=2*prod'xyt+(if?r=\<one>thennum?yselse0)" using alsohave"...=2*prod'xyt+(if?r=\<one>thenyelse0)" usingcanreprbysimp finallyhave"prod'xy(Suct)=2*prod'xyt+(if?r=\<one>thenyelse0)". thenshow"read(tpsL1t)!j1\<noteq>\<one>\<Longrightarrow>tpsL2t=tpsL1t" and"read(tpsL1t)!j1=\<one>\<Longrightarrow> tpsL2t=(tpsL1t)[j3:=(\<lfloor>y+2*Arithmetic.prod'xyt\<rfloor>\<^sub>N,1)]" by(simp_alladd:add.commutetpsL1_deftpsL2_def) qed
text‹
this section we construct for every $d \in\nat$ a Turing machine that
$n^d$. The following TMs expect a number $n$ on tape $j_1$ and output
n^d$ on tape $j_3$. Another tape, $j_2$, is used as scratch space to hold
values. The TMs initialize tape $j_3$ with~1 and then multiply this
by $n$ for $d$ times using the TM @{const tm_mult}. ›
text‹
monomial is a power multiplied by a constant coefficient. The following Turing
have parameters $c$ and $d$ and expect a number $x$ on tape $j$. They
$c\cdot x^d$ on tape $j + 3$. The tapes $j+1$ and $j+2$ are
space for use by @{const tm_pow} and @{const tm_mult}. ›
lemma tm_monomial_tm: assumes"k ≥ 2"and"G ≥ 4"and"j + 3 < k"and"0 < j" shows"turing_machine k G (tm_monomial c d j)" unfolding tm_monomial_def using assms tm_setn_tm tm_mult_tm tm_pow_tm turing_machine_sequential_turing_machine by simp
locale turing_machine_monomial = fixes c d :: nat and j :: tapeidx begin
text‹
polynomial is a sum of monomials. In this section we construct for every
function $p$ a Turing machine that on input $x\in\nat$ outputs
p(x)$.
to our definition of polynomials (see Section~\ref{s:tm-basic-bigoh}),
can represent each polynomial by a list of coefficients. The value of such a
with coefficient list @{term cs} on input $x$ is given by the next
. In the following definition, the coefficients of the polynomial are in
order, which simplifies the Turing machine later. ›
definition polyvalue :: "nat list ==> nat ==> nat"where "polyvalue cs x ≡ (∑i←[0..<length cs]. rev cs ! i * x ^ i)"
lemma polyvalue_Nil: "polyvalue [] x = 0" using polyvalue_def by simp
lemma sum_upt_snoc: "(∑i←[0..<length (zs @ [z])]. (zs @ [z]) ! i * x ^ i) = (∑i←[0..<length zs]. zs ! i * x ^ i) + z * x ^ (length zs)" by simp (smt (verit, ccfv_SIG) length_map less_diff_conv map_equality_iff map_nth nth_append nth_upt zero_less_diff)
lemma polyvalue_Cons: "polyvalue (c # cs) x = c * x ^ (length cs) + polyvalue cs x" proof - have"polyvalue (c # cs) x = (∑i←[0..<Suc (length cs)]. (rev cs @ [c]) ! i * x ^ i)" using polyvalue_def by simp alsohave"... = (∑i←[0..<length (rev cs @ [c])]. (rev cs @ [c]) ! i * x ^ i)" by simp alsohave"... = (∑i←[0..<length (rev cs)]. (rev cs) ! i * x ^ i) + c * x ^ (length (rev cs))" using sum_upt_snoc by blast alsohave"... = (∑i←[0..<length cs]. (rev cs) ! i * x ^ i) + c * x ^ (length cs)" by simp finallyshow ?thesis using polyvalue_def by simp qed
lemma polyvalue_Cons_ge: "polyvalue (c # cs) x ≥ polyvalue cs x" using polyvalue_Cons by simp
lemma polyvalue_Cons_ge2: "polyvalue (c # cs) x ≥ c * x ^ (length cs)" using polyvalue_Cons by simp
lemma sum_list_const: "(∑_←ns. c) = c * length ns" using sum_list_triv[of c ns] by simp
lemma polyvalue_le: "polyvalue cs x ≤ Max (set cs) * length cs * Suc x ^ length cs" proof - define cmax where"cmax = Max (set (rev cs))" have"polyvalue cs x = (∑i←[0..<length cs]. rev cs ! i * x ^ i)" using polyvalue_def by simp alsohave"... ≤ (∑i←[0..<length cs]. cmax * x ^ i)" proof - have"rev cs ! i ≤ cmax"if"i < length cs"for i using that cmax_def by (metis List.finite_set Max_ge length_rev nth_mem) thenshow ?thesis by (metis (no_types, lifting) atLeastLessThan_iff mult_le_mono1 set_upt sum_list_mono) qed alsohave"... = cmax * (∑i←[0..<length cs]. x ^ i)" using sum_list_const_mult by blast alsohave"... ≤ cmax * (∑i←[0..<length cs]. Suc x ^ i)" by (simp add: power_mono sum_list_mono) alsohave"... ≤ cmax * (∑i←[0..<length cs]. Suc x ^ length cs)" proof - have"Suc x ^ i ≤ Suc x ^ length cs"if"i < length cs"for i using that by (simp add: dual_order.strict_implies_order pow_mono) thenshow ?thesis by (metis atLeastLessThan_iff mult_le_mono2 set_upt sum_list_mono) qed alsohave"... = cmax * length cs * Suc x ^ length cs" using sum_list_const[of _ "[0..<length cs]"] by simp finallyhave"polyvalue cs x ≤ cmax * length cs * Suc x ^ length cs" . moreoverhave"cmax = Max (set cs)" using cmax_def by simp ultimatelyshow ?thesis by simp qed
text‹
following Turing machines compute polynomials given as lists of
. If the polynomial is given by coefficients @{term cs}, the TM
{term "tm_polycoef cs j"} expect a number $n$ on tape $j$ and writes $p(n)$ to
$j + 4$. The tapes $j+1$, $j+2$, and $j + 3$ are auxiliary tapes for use by
{const tm_monomial}. ›
lemma tm_polycoef_tm: assumes"k ≥ 2"and"G ≥ 4"and"j + 4 < k"and"0 < j" shows"turing_machine k G (tm_polycoef cs j)" proof (induction cs) case Nil thenshow ?case by (simp add: assms(1) assms(2) turing_machine_def) next case (Cons c cs) moreoverhave "turing_machine k G (tm_monomial c (length cs) j ;; tm_add (j + 3) (j + 4) ;; tm_setn (j + 3) 0)" using tm_monomial_tm tm_add_tm tm_setn_tm assms by simp ultimatelyshow ?case by simp qed
locale turing_machine_polycoef = fixes j :: tapeidx begin
definition"tm1 c cs ≡ tm_monomial c (length cs) j" definition"tm2 c cs ≡ tm1 c cs ;; tm_add (j + 3) (j + 4)" definition"tm3 c cs ≡ tm2 c cs ;; tm_setn (j + 3) 0"
fun tm4 :: "nat list ==> machine"where "tm4 [] = []" | "tm4 (c # cs) = tm4 cs ;; tm3 c cs"
lemma tm4_eq_tm_polycoef: "tm4 zs = tm_polycoef zs j" proof (induction zs) case Nil thenshow ?case by simp next case (Cons z zs) thenshow ?case by (simp add: tm1_def tm2_def tm3_def) qed
text‹
time bound in the previous lemma for @{const tm_polycoef} is a bit unwieldy.
depends not only on the length of the input $x$ but also on the list of
of the polynomial $p$ and on the value $p(x)$. Next we bound this
bound by a simpler expression of the form $d + d\cdot|x|^2$ where $d$
only on the polynomial. This is accomplished by the next three lemmas. ›
text‹
to our definition of @{const polynomial} (see
~\ref{s:tm-basic-bigoh}) every polynomial has a list of coefficients.
the next definition is well-defined for polynomials $p$. ›
definition coefficients :: "(nat ==> nat) ==> nat list"where "coefficients p ≡ SOME cs. ∀n. p n = (∑i←[0..<length cs]. cs ! i * n ^ i)"
text‹
$d$ in our upper bound of the form $d + d\cdot|x|^2$ for the running time of
{const tm_polycoef} depends on the polynomial. It is given by the next
: ›
definition d_polynomial :: "(nat ==> nat) ==> nat"where "d_polynomial p ≡ (let cs = rev (coefficients p) in SOME d. ∀x. length cs * (66 + 71 * length cs + 99 * length cs ^ 3 * (nlength x)2 + 32 * (Max (set (map nlength cs)) + nlength (Suc x ^ length cs))2 + 5 * nlength (polyvalue cs x)) ≤ d + d * nlength x ^ 2)"
text‹
Turing machine @{const tm_polycoef} has the coefficients of a polynomial
parameter. Next we devise a similar Turing machine that has the polynomial,
a function $\nat\to\nat$, as parameter. ›
lemma tm_polynomial_tm: assumes"k ≥ 2"and"G ≥ 4"and"0 < j"and"j + 4 < k" shows"turing_machine k G (tm_polynomial p j)" using assms tm_polynomial_def tm_polycoef_tm by simp
lemma transforms_tm_polynomialI [transforms_intros]: fixes p :: "nat ==> nat"and j :: tapeidx fixes k x :: nat and tps tps' :: "tape list" assumes"0 < j"and"k = length tps"and"j + 4 < k" and"polynomial p" assumes "tps ! j = (⌊x⌋N, 1)" "tps ! (j + 1) = (⌊0⌋N, 1)" "tps ! (j + 2) = (⌊0⌋N, 1)" "tps ! (j + 3) = (⌊0⌋N, 1)" "tps ! (j + 4) = (⌊0⌋N, 1)" assumes"ttt = d_polynomial p + d_polynomial p * nlength x ^ 2" assumes"tps' = tps [j + 4 := (⌊p x⌋N, 1)]" shows"transforms (tm_polynomial p j) tps ttt tps'" proof - let ?P = "λx. ∀n. p n = (∑i←[0..<length x]. x ! i * n ^ i)" define cs where"cs = (SOME x. ?P x)" moreoverhave ex: "∃cs. ?P cs" using assms(4) polynomial_def by simp ultimatelyhave"?P cs" using someI_ex[of ?P] by blast thenhave1: "polyvalue (rev cs) x = p x" using polyvalue_def by simp
let ?cs = "rev cs" have"d_polynomial p = (SOME d. ∀x. length ?cs * (66 + 71 * length ?cs + 99 * length ?cs ^ 3 * (nlength x)2 + 32 * (Max (set (map nlength ?cs)) + nlength (Suc x ^ length ?cs))2 + 5 * nlength (polyvalue ?cs x)) ≤ d + d * nlength x ^ 2)" using cs_def coefficients_def d_polynomial_def by simp thenhave *: "∀x. length ?cs * (66 + 71 * length ?cs + 99 * length ?cs ^ 3 * (nlength x)2 + 32 * (Max (set (map nlength ?cs)) + nlength (Suc x ^ length ?cs))2 + 5 * nlength (polyvalue ?cs x)) ≤ (d_polynomial p) + (d_polynomial p) * nlength x ^ 2" using tm_polycoef_time_3 someI_ex[OF tm_polycoef_time_3] by presburger
have"transforms (loc.tm4 ?cs) tps ?ttt (tps[j + 4 := (⌊polyvalue ?cs x⌋N, 1)])" using loc.tm4 assms * by blast thenhave"transforms (loc.tm4 ?cs) tps ?ttt (tps[j + 4 := (⌊p x⌋N, 1)])" using1by simp thenhave"transforms (loc.tm4 ?cs) tps ?ttt tps'" using assms(11) by simp moreoverhave"loc.tm4 ?cs = tm_polynomial p j" using tm_polynomial_def loc.tm4_eq_tm_polycoef coefficients_def cs_def by simp ultimatelyhave"transforms (tm_polynomial p j) tps ?ttt tps'" by simp thenshow"transforms (tm_polynomial p j) tps ttt tps'" using * assms(10) transforms_monotone by simp qed
subsection‹Division by two›
text‹
order to divide a number by two, a Turing machine can shift all symbols on
tape containing the number to the left, of course without overwriting
start symbol.
next command implements the left shift. It scans the tape $j$ from right to
and memorizes the current symbol on the last tape. It works very similar to
{const cmd_double} only in the opposite direction. Upon reaching the start
, it moves the head one cell to the right. ›
definition cmd_halve :: "tapeidx ==> command"where "cmd_halve j rs ≡ (if rs ! j = 1 then 1 else 0, (map (λi. if i = j then if rs ! j = ▹ then (rs ! i, Right) else if last rs = ▹ then (◻, Left) else (tosym (todigit (last rs)), Left) else if i = length rs - 1 then (tosym (todigit (rs ! j)), Stay) else (rs ! i, Stay)) [0..<length rs]))"
lemma turing_command_halve: assumes"G ≥ 4"and"0 < j"and"j < k" shows"turing_command (Suc k) 1 G (cmd_halve j)" proof show"∧gs. length gs = Suc k ==> length ([!!] cmd_halve j gs) = length gs" using cmd_halve_def by simp moreoverhave"0 ≠ Suc k - 1" using assms by simp ultimatelyshow"∧gs. length gs = Suc k ==> 0 < Suc k ==> cmd_halve j gs [.] 0 = gs ! 0" using assms cmd_halve_def by (smt (verit) One_nat_def ab_semigroup_add_class.add_ac(1) diff_Suc_1
length_map neq0_conv nth_map nth_upt plus_1_eq_Suc prod.sel(1) prod.sel(2)) show"cmd_halve j gs [.] j' < G" if"length gs = Suc k""(∧i. i < length gs ==> gs ! i < G)""j' < length gs" for gs j' proof - have"cmd_halve j gs [!] j' = (if j' = j then if gs ! j = ▹ then (gs ! j', Right) else if last gs = ▹ then (◻, Left) else (tosym (todigit (last gs)), Left) else if j' = length gs - 1 then (tosym (todigit (gs ! j)), Stay) else (gs ! j', Stay))" using cmd_halve_def that(3) by simp moreover consider "j' = j" | "j' = k" | "j' ≠ j ∧ j' ≠ k" by auto ultimatelyshow ?thesis using that assms by (cases) simp_all qed show"∧gs. length gs = Suc k ==> [*] (cmd_halve j gs) ≤ 1" using cmd_halve_def by simp qed
lemma sem_cmd_halve_2: assumes"j < k" and"bit_symbols xs" and"length tps = Suc k" and"i ≤ length xs" and"i > 0" and"z = 0∨ z = 1" and"tps ! j = (⌊xs⌋, i)" and"tps ! k = ⌈z⌉" and"tps' = tps[j := tps ! j |:=| z |-| 1, k := ⌈xs ! (i - 1)⌉]" shows"sem (cmd_halve j) (0, tps) = (0, tps')" proof (rule semI) show"proper_command (Suc k) (cmd_halve j)" using cmd_halve_def by simp show"length tps = Suc k""length tps' = Suc k" using assms(3,9) by simp_all define rs where"rs = read tps" thenhave lenrs: "length rs = Suc k" using assms(3) read_length by simp have rsj: "rs ! j = xs ! (i - 1)" using rs_def assms tapes_at_read' contents_inbounds by (metis fst_conv le_imp_less_Suc less_imp_le_nat snd_conv) thenhave rsj': "rs ! j > 1" using assms Suc_1 Suc_diff_1 Suc_le_lessD by (metis eval_nat_numeral(3) less_Suc_eq) thenshow"fst (cmd_halve j (read tps)) = 0" using cmd_halve_def rs_def by simp have lastrs: "last rs = z" using assms rs_def onesie_read tapes_at_read' by (metis diff_Suc_1 last_conv_nth length_0_conv lenrs lessI nat.simps(3)) show"act (cmd_halve j (read tps) [!] j') (tps ! j') = tps' ! j'"if"j' < Suc k"forj' proof - have"j' < length rs" using that lenrs by simp thenhave *: "cmd_halve j rs [!] j' = (if j' = j then if rs ! j = ▹ then (rs ! j', Right) else if last rs = ▹ then (◻, Left) else (tosym (todigit (last rs)), Left) else if j' = length rs - 1 then (tosym (todigit (rs ! j)), Stay) else (rs ! j', Stay))" using cmd_halve_def by simp
consider "j' = j" | "j' = k" | "j' ≠ j ∧ j' ≠ k" by auto thenshow ?thesis proof (cases) case1 thenhave"cmd_halve j (read tps) [!] j' = (tosym (todigit (last rs)), Left)" using rs_def rsj' lastrs * assms(6) by auto thenhave"cmd_halve j (read tps) [!] j' = (z, Left)" using lastrs assms(6) by auto moreoverhave"tps' ! j' = tps ! j |:=| z |-| 1" using1 assms(1,3,9) by simp ultimatelyshow ?thesis using act_Left' 1 that rs_def by metis next case2 thenhave"cmd_halve j (read tps) [!] j' = (tosym (todigit (rs ! j)), Stay)" using rs_def * lenrs assms(1) by simp moreoverhave"tps' ! j' = ⌈xs ! (i - 1)⌉" using assms 2by simp moreoverhave"tps ! j' = ⌈z⌉" using assms 2by simp moreoverhave"tosym (todigit (rs ! j)) = xs ! (i - 1)" proof - have"xs ! (i - 1) = 0∨ xs ! (i - 1) = 1" using rsj rs_def assms by simp thenshow ?thesis using One_nat_def add_2_eq_Suc' numeral_3_eq_3 rsj by presburger qed ultimatelyshow ?thesis using act_onesie by simp next case3 thenshow ?thesis using * act_Stay that assms lenrs rs_def by simp qed qed qed
lemma sem_cmd_halve_1: assumes"j < k" and"bit_symbols xs" and"length tps = Suc k" and"0 < length xs" and"tps ! j = (⌊xs⌋, length xs)" and"tps ! k = ⌈▹⌉" and"tps' = tps[j := tps ! j |:=| ◻ |-| 1, k := ⌈xs ! (length xs - 1)⌉]" shows"sem (cmd_halve j) (0, tps) = (0, tps')" proof (rule semI) show"proper_command (Suc k) (cmd_halve j)" using cmd_halve_def by simp show"length tps = Suc k""length tps' = Suc k" using assms(3,7) by simp_all define rs where"rs = read tps" thenhave lenrs: "length rs = Suc k" using assms(3) read_length by simp have rsj: "rs ! j = xs ! (length xs - 1)" using rs_def assms tapes_at_read' contents_inbounds by (metis One_nat_def fst_conv le_eq_less_or_eq le_imp_less_Suc snd_conv) thenhave rsj': "rs ! j > 1" using assms(2,4) by (metis One_nat_def Suc_1 diff_less lessI less_add_Suc2 numeral_3_eq_3 plus_1_eq_Suc) thenshow"fst (cmd_halve j (read tps)) = ◻" using cmd_halve_def rs_def by simp have lastrs: "last rs = ▹" using assms rs_def onesie_read tapes_at_read' by (metis diff_Suc_1 last_conv_nth length_0_conv lenrs lessI nat.simps(3)) show"act (cmd_halve j (read tps) [!] j') (tps ! j') = tps' ! j'"if"j' < Suc k"forj' proof - have"j' < length rs" using that lenrs by simp thenhave *: "cmd_halve j rs [!] j' = (if j' = j then if rs ! j = ▹ then (rs ! j', Right) else if last rs = ▹ then (◻, Left) else (tosym (todigit (last rs)), Left) else if j' = length rs - 1 then (tosym (todigit (rs ! j)), Stay) else (rs ! j', Stay))" using cmd_halve_def by simp
consider "j' = j" | "j' = k" | "j' ≠ j ∧ j' ≠ k" by auto thenshow ?thesis proof (cases) case1 thenhave"cmd_halve j (read tps) [!] j' = (◻, Left)" using rs_def rsj' lastrs * by simp thenshow ?thesis using act_Left' 1 that rs_def assms(1,3,7) by simp next case2 thenhave"cmd_halve j (read tps) [!] j' = (tosym (todigit (rs ! j)), Stay)" using rs_def * lenrs assms(1) by simp moreoverhave"tps' ! j' = ⌈xs ! (length xs - 1)⌉" using assms 2by simp moreoverhave"tps ! j' = ⌈▹⌉" using assms 2by simp ultimatelyshow ?thesis using act_onesie assms 2 that rs_def rsj by (smt (verit) One_nat_def Suc_1 add_2_eq_Suc' diff_less numeral_3_eq_3 zero_less_one) next case3 thenshow ?thesis using * act_Stay that assms lenrs rs_def by simp qed qed qed
lemma sem_cmd_halve_0: assumes"j < k" and"length tps = Suc k" and"tps ! j = (⌊xs⌋, 0)" and"tps ! k = ⌈z⌉" and"tps' = tps[j := tps ! j |+| 1, k := ⌈0⌉]" shows"sem (cmd_halve j) (0, tps) = (1, tps')" proof (rule semI) show"proper_command (Suc k) (cmd_halve j)" using cmd_halve_def by simp show"length tps = Suc k""length tps' = Suc k" using assms(2,5) by simp_all show"fst (cmd_halve j (read tps)) = 1" using cmd_halve_def assms contents_at_0 tapes_at_read' by (smt (verit) fst_conv le_eq_less_or_eq not_less not_less_eq snd_conv) show"act (cmd_halve j (read tps) [!] j') (tps ! j') = tps' ! j'"if"j' < Suc k"forj' proof - define gs where"gs = read tps" thenhave"length gs = Suc k" using assms by (simp add: read_length) thenhave"j' < length gs" using that by simp thenhave *: "cmd_halve j gs [!] j' = (if j' = j then if gs ! j = ▹ then (gs ! j', Right) else if last gs = ▹ then (◻, Left) else (tosym (todigit (last gs)), Left) else if j' = length gs - 1 then (tosym (todigit (gs ! j)), Stay) else (gs ! j', Stay))" using cmd_halve_def by simp have gsj: "gs ! j = ▹" using gs_def assms(1,2,3) by (metis contents_at_0 fstI less_Suc_eq sndI tapes_at_read')
consider "j' = j" | "j' = k" | "j' ≠ j ∧ j' ≠ k" by auto thenshow ?thesis proof (cases) case1 thenhave"cmd_halve j (read tps) [!] j' = (gs ! j', Right)" using gs_def gsj * by simp thenshow ?thesis using act_Right assms 1 that gs_def by (metis length_list_update lessI nat_neq_iff nth_list_update) next case2 thenhave"cmd_halve j (read tps) [!] j' = (tosym (todigit (gs ! j)), Stay)" using gs_def * ‹length gs = Suc k› assms(1) by simp moreoverhave"tps' ! j' = ⌈0⌉" using assms 2by simp moreoverhave"tps ! j' = ⌈z⌉" using assms 2by simp ultimatelyshow ?thesis using act_onesie assms 2 that gs_def gsj by (smt (verit, best) One_nat_def Suc_1 add_2_eq_Suc' less_Suc_eq_0_disj less_numeral_extra(3) nat.inject numeral_3_eq_3) next case3 thenshow ?thesis using * act_Stay that assms(2,5) ‹length gs = Suc k› gs_def by simp qed qed qed
lemma execute_cmd_halve_0 assumes" k" and tps k" and "tps ! j = \lfloor\rfloor,0 and"tps ! k = ⌈⌉
java.lang.StringIndexOutOfBoundsException: Index 96 out of bounds for length 96 shows "execute (tm_halve j) (0, tps) 1 = (1, tps')" using tm_halve_def exe_lt_length
definition shift :: "tape nat ==>
< (λx. if x ≤ y then (fst tp) x else (fst tp) (Suc x), y)"
lemma shift_update: "y > 0 <Longrightarrow ) (Suc 1 = shift ( - ) unfolding shift_def by fastforce
lemma shift_contents_0: assumes"length xs > 0" shows"shift (⌊xs⌋, length xs) 0 = (⌊tl xs⌋, 0)" proof - have"shift (⌊xs⌋, length xs) 0 = (⌊drop 1 xs⌋, 0)" using shift_def contents_def by fastforce thenshow ?thesis by (simp add: drop_Suc) qed
lemma proper_bit_symbols: "bit_symbols ws ==> proper_symbols ws" by auto
lemma shift_contents_eq_take_drop: assumes"length xs > 0" and"ys = take i xs @ drop (Suc i) xs" and"i > 0" and"i < length xs" shows"shift (⌊xs⌋, length xs) i = (⌊ys⌋, i)" proof - have"shift (⌊xs⌋, length xs) i = (λx. if x ≤ i then ⌊xs⌋ x else ⌊xs⌋ (Suc x), i)" using shift_def by auto moreoverhave"(λx. if x ≤ i then ⌊xs⌋ x else ⌊xs⌋ (Suc x)) = ⌊take i xs @ drop (Suc i) xs⌋"
(is"?l = ?r") proof fix x
consider "x = 0" | "0 < x ∧ x ≤ i" | "i < x ∧ x ≤ length xs - 1" | "length xs - 1 < x" by linarith thenshow"?l x = ?r x" proof (cases) case1 thenshow ?thesis using assms contents_def by simp next case2 thenhave"?l x = ⌊xs⌋ x" by simp thenhave lhs: "?l x = xs ! (x - 1)" using assms 2by simp have"?r x = (take i xs @ drop (Suc i) xs) ! (x - 1)" using assms 2by auto thenhave"?r x = xs ! (x - 1)" using assms(4) 2 by (metis diff_less le_eq_less_or_eq length_take less_trans min_absorb2 nth_append nth_take zero_less_one) thenshow ?thesis using lhs by simp next case3 thenhave"?l x = ⌊xs⌋ (Suc x)" by simp thenhave lhs: "?l x = xs ! x" using3 assms by auto have"?r x = (take i xs @ drop (Suc i) xs) ! (x - 1)" using assms 3by auto thenhave"?r x = drop (Suc i) xs ! (x - 1 - i)" using assms(3,4) 3 by (smt (verit) Suc_diff_1 dual_order.strict_trans length_take less_Suc_eq min_absorb2 nat_less_le nth_append) thenhave"?r x = xs ! x" using assms 3by simp thenshow ?thesis using lhs by simp next case4 thenshow ?thesis using contents_def by auto qed qed ultimatelyshow ?thesis using assms(2) by simp qed
lemma exe_cmd_halve_2: assumes"j < k" and"bit_symbols xs" and"length tps = Suc k" and"i ≤ length xs" and"i > 0" and"z = 0∨ z = 1" and"tps ! j = (⌊xs⌋, i)" and"tps ! k = ⌈z⌉" and"tps' = tps[j := tps ! j |:=| z |-| 1, k := ⌈xs ! (i - 1)⌉]" shows"exe (tm_halve j) (0, tps) = (0, tps')" using tm_halve_def exe_lt_length sem_cmd_halve_2 assms by simp
lemma num_tl_div_2: "num (tl xs) = num xs div 2" proof (cases "xs = []") case True thenshow ?thesis by (simp add: num_def) next case False thenhave *: "xs = hd xs # tl xs" by simp thenhave"num xs = todigit (hd xs) + 2 * num (tl xs)" using num_Cons by metis thenshow ?thesis by simp qed
lemma canrepr_div_2: "canrepr (n div 2) = tl (canrepr n)" using canreprI canrepr canonical_canrepr num_tl_div_2 canonical_tl by (metis hd_Cons_tl list.sel(2))
corollary nlength_times2: "nlength (2 * n) ≤ Suc (nlength n)" using canrepr_div_2[of "2 * n"] by simp
corollary nlength_times2plus1: "nlength (2 * n + 1) ≤ Suc (nlength n)" using canrepr_div_2[of "2 * n + 1"] by simp
text‹
next Turing machine is the one we actually use to divide a number by two.
it moves to the end of the symbol sequence representing the number, then
applies @{const tm_halve'}. ›
lemma tm3: assumes"ttt = 2 * nlength n + 3" shows"transforms tm3 tps0 ttt tps3" unfolding tm3_def proof (tform tps: tps3_def tps2_def tps0 jk time: assms) show"bit_symbols (canrepr n)" using bit_symbols_canrepr . show"tps3 = tps2[j := (⌊tl (canrepr n)⌋, 1)]" using tps3_def tps2_def jk tps0 canrepr_div_2 by simp qed
end
end(* locale turing_machine_div2 *)
lemma transforms_tm_div2I [transforms_intros]: fixes tps tps' :: "tape list"and ttt k n :: nat and j :: tapeidx assumes"0 < j""j < k" and"length tps = k" and"tps ! j = (⌊n⌋N, 1)" assumes"ttt = 2 * nlength n + 3" assumes"tps' = tps[j := (⌊n div 2⌋N, 1)]" shows"transforms (tm_div2 j) tps ttt tps'" proof - interpret loc: turing_machine_div2 j . show ?thesis using loc.tm3_eq_tm_div2 loc.tm3 loc.tps3_def assms by simp qed
subsection‹Modulo two›
text‹
this section we construct a Turing machine that writes to tape $j_2$ the
@{text 1} or @{text ◻} depending on whether the number on tape $j_1$ is
or even. If initially tape $j_2$ contained at most one symbol, it will
the numbers~1 or~0. ›
lemma canrepr_odd: "odd n ==> canrepr n ! 0 = 1" proof - assume"odd n" thenhave"0 < n" by presburger thenhave len: "length (canrepr n) > 0" using nlength_0 by simp thenhave"canrepr n ! 0 = 0∨ canrepr n ! 0 = 1" using bit_symbols_canrepr by fastforce thenshow"canrepr n ! 0 = 1" using prepend_2_even len canrepr `odd n` `0 < n` by (metis gr0_implies_Suc length_Suc_conv nth_Cons_0) qed
lemma canrepr_even: "even n ==> 0 < n ==> canrepr n ! 0 = 0" proof - assume"even n""0 < n" thenhave len: "length (canrepr n) > 0" using nlength_0 by simp thenhave"canrepr n ! 0 = 0∨ canrepr n ! 0 = 1" using bit_symbols_canrepr by fastforce thenshow"canrepr n ! 0 = 0" using prepend_3_odd len canrepr `even n` `0 < n` by (metis gr0_implies_Suc length_Suc_conv nth_Cons_0) qed
definition"tm_mod2 j1 j2 ≡ tm_trans2 j1 j2 (λz. if z = 1 then 1 else ◻)"
lemma tm_mod2_tm: assumes"k ≥ 2"and"G ≥ 4"and"0 < j2"and"j1 < k"and"j2 < k" shows"turing_machine k G (tm_mod2 j1 j2)" unfolding tm_mod2_def using assms tm_trans2_tm by simp
lemma transforms_tm_mod2I [transforms_intros]: assumes"j1 < length tps"and"0 < j2"and"j2 < length tps" and"b ≤ 1" assumes"tps ! j1 = (⌊n⌋N, 1)" and"tps ! j2 = (⌊b⌋N, 1)" assumes"tps' = tps[j2 := (⌊n mod 2⌋N, 1)]" shows"transforms (tm_mod2 j1 j2) tps 1 tps'" proof - let ?f = "λz::symbol. if z = 1 then 1 else ◻" let ?tps = "tps[j2 := tps ! j2 |:=| (?f (tps :.: j1))]" have *: "transforms (tm_mod2 j1 j2) tps 1 ?tps" using transforms_tm_trans2I assms tm_mod2_def by metis
have"tps :.: j1 = 1"if"odd n" using that canrepr_odd assms(5) contents_def by (metis One_nat_def diff_Suc_1 fst_conv gr_implies_not0 ncontents_1_blank_iff_zero odd_pos snd_conv) moreoverhave"tps :.: j1 = 0"if"even n"and"n > 0" using that canrepr_even assms(5) contents_def by (metis One_nat_def diff_Suc_1 fst_conv gr_implies_not0 ncontents_1_blank_iff_zero snd_conv) moreoverhave"tps :.: j1 = ◻"if"n = 0" using that canrepr_even assms(5) contents_def by simp ultimatelyhave"tps :.: j1 = 1⟷ odd n" by linarith thenhave f: "?f (tps :.: j1) = 1⟷ odd n" by simp
have tps_j2: "tps ! j2 |:=| (?f (tps :.: j1)) = ((⌊b⌋N)(1 := (?f (tps :.: j1))), 1)" using assms by simp
have"tps ! j2 |:=| (?f (tps :.: j1)) = (⌊n mod 2⌋N, 1)" proof (cases "even n") case True thenhave"tps ! j2 |:=| (?f (tps :.: j1)) = ((⌊b⌋N)(1 := 0), 1)" using f tps_j2 by auto alsohave"... = (⌊[]⌋, 1)" proof (cases "b = 0") case True thenhave"⌊b⌋N = ⌊[]⌋" using canrepr_0 by simp thenshow ?thesis by auto next case False thenhave"⌊b⌋N = ⌊[1]⌋" using canrepr_1 assms(4) by (metis One_nat_def bot_nat_0.extremum_uniqueI le_Suc_eq) thenshow ?thesis by (metis One_nat_def append.simps(1) append_Nil2 contents_append_update contents_blank_0 list.size(3)) qed alsohave"... = (⌊0⌋N, 1)" using canrepr_0 by simp finallyshow ?thesis using True by auto next case False thenhave"tps ! j2 |:=| (?f (tps :.: j1)) = ((⌊b⌋N)(1 := 1), 1)" using f tps_j2 by auto alsohave"... = (⌊[1]⌋, 1)" proof (cases "b = 0") case True thenhave"⌊b⌋N = ⌊[]⌋" using canrepr_0 by simp thenshow ?thesis by (metis One_nat_def append.simps(1) contents_snoc list.size(3)) next case False thenhave"⌊b⌋N = ⌊[1]⌋" using canrepr_1 assms(4) by (metis One_nat_def bot_nat_0.extremum_uniqueI le_Suc_eq) thenshow ?thesis by auto qed alsohave"... = (⌊1⌋N, 1)" using canrepr_1 by simp alsohave"... = (⌊n mod 2⌋N, 1)" using False by (simp add: mod2_eq_if) finallyshow ?thesis by auto qed thenshow ?thesis using * assms(7) by auto qed
subsection‹Boolean operations›
text‹
order to support Boolean operations, we represent the value True by the
~1 and False by~0. ›
abbreviation bcontents :: "bool ==> (nat ==> symbol)" (java.lang.NullPointerException
"⌊if b then 1 else 0⌋N"
java.lang.NullPointerException
tape containing a ber ains enumber~0 iff.\ heei ban in cell
~1. ›
lemma read_ncontents_eq_0: assumes"tps ! j = (⌊n⌋N, 1)"and"j < length tps" shows"(read tps) ! j = ◻⟷ n = 0" using assms tapes_at_read'[of j tps] ncontents_1_blank_iff_zero by (metis prod.sel(1) prod.sel(2))
subsubsection‹And›
text‹
next Turing machine, when given two numbers $a, b \in\{0, 1\}$ on tapes
j_1$ and $j_2$, writes to tape $j_1$ the number~1 if $a = b = 1$; otherwise it
the number~0. In other words, it overwrites tape $j_1$ with the logical
of the two tapes. ›
lemma tm: "transforms (tm_and j1 j2) tps0 3 tps1" unfolding tm_and_def proof (tform) have"read tps0 ! j1 = ⌊canrepr a⌋ 1" using jk tps0 tapes_at_read'[of j1 tps0] by simp thenhave1: "read tps0 ! j1 = 1⟷ a = 1" using ab canrepr_odd contents_def ncontents_1_blank_iff_zero by (metis (mono_tags, lifting) One_nat_def diff_Suc_1 less_2_cases_iff odd_one) have"read tps0 ! j2 = ⌊canrepr b⌋ 1" using jk tps0 tapes_at_read'[of j2 tps0] by simp thenhave2: "read tps0 ! j2 = 1⟷ b = 1" using ab canrepr_odd contents_def ncontents_1_blank_iff_zero by (metis (mono_tags, lifting) One_nat_def diff_Suc_1 less_2_cases_iff odd_one)
show"tps1 = tps0"if"¬ (read tps0 ! j1 = 1∧ read tps0 ! j2 = ◻)" proof - have"a = (if a = 1 ∧ b = 1 then 1 else 0)" using that 12 ab jk by (metis One_nat_def less_2_cases_iff read_ncontents_eq_0 tps0(2)) thenhave"tps0 ! j1 = (⌊a = 1 ∧ b = 1⌋B, 1)" using tps0 by simp thenshow ?thesis unfolding tps1_def using list_update_id[of tps0 j1] by simp qed show"tps1 = tps0[j1 := tps0 ! j1 |:=| ◻]"if"read tps0 ! j1 = 1∧ read tps0 ! j2 = ◻" proof - have"(if a = 1 ∧ b = 1 then 1 else 0) = 0" using that 12by simp moreoverhave"tps0 ! j1 |:=| ◻ = (⌊0⌋N, 1)" proof (cases "a = 0") case True thenshow ?thesis using tps0 jk by auto next case False thenhave"a = 1" using ab by simp thenhave"⌊a⌋N = ⌊[1]⌋" using canrepr_1 by simp moreoverhave"(⌊[1]⌋, 1) |:=| ◻ = (⌊[]⌋, 1)" using contents_def by auto ultimatelyhave"(⌊a⌋N, 1) |:=| ◻ = (⌊0⌋N, 1)" using ncontents_0 by presburger thenshow ?thesis using tps0 jk by simp qed ultimatelyhave"tps0 ! j1 |:=| ◻ = (⌊a = 1 ∧ b = 1⌋B, 1)" by (smt (verit, best)) thenshow ?thesis unfolding tps1_def by auto qed qed
end(* context *)
end(* locale *)
lemma transforms_tm_andI [transforms_intros]: fixes j1 j2 :: tapeidx fixes tps :: "tape list"and k :: nat and a b :: nat assumes"a < 2""b < 2" assumes"length tps = k" assumes"j1 < k""j2 < k""j1 ≠ j2""0 < j1" assumes "tps ! j1 = (⌊a⌋N, 1)" "tps ! j2 = (⌊b⌋N, 1)" assumes"tps' = tps [j1 := (⌊a = 1 ∧ b = 1⌋B, 1)]" shows"transforms (tm_and j1 j2) tps 3 tps'" proof - interpret loc: turing_machine_and j1 j2 . show ?thesis using assms loc.tps1_def loc.tm by simp qed
subsubsection‹Not›
text‹
next Turing machine turns the number~1 into~0 and vice versa. ›
lemma tm_not_tm: assumes"k ≥ 2"and"G ≥ 4"and"0 < j"and"j < k" shows"turing_machine k G (tm_not j)" using tm_not_def tm_write_tm assms turing_machine_branch_turing_machine by simp
locale turing_machine_not = fixes j :: tapeidx begin
context fixes tps0 :: "tape list"and k :: nat and a :: nat assumes a: "a < 2" assumes jk: "j < k""length tps0 = k" assumes tps0: "tps0 ! j = (⌊a⌋N, 1)" begin
definition"tps1 ≡ tps0 [j := (⌊a ≠ 1⌋B, 1)]"
lemma tm: "transforms (tm_not j) tps0 3 tps1" unfolding tm_not_def proof (tform) have *: "read tps0 ! j = ◻⟷ a = 0" using read_ncontents_eq_0 jk tps0 by simp show"tps1 = tps0[j := tps0 ! j |:=| 1]"if"read tps0 ! j = ◻" proof - have"a = 0" using a that * by simp thenhave"(⌊if a = 1 then 0 else 1⌋N, 1) = (⌊1⌋N, 1)" by simp moreoverhave"tps0 ! j |:=| 1 = (⌊1⌋N, 1)" using tps0 canrepr_0 canrepr_1 `a = 0` contents_snoc by (metis One_nat_def append.simps(1) fst_conv list.size(3) snd_conv) ultimatelyhave"tps0[j := tps0 ! j |:=| 1] = tps0[j := (⌊a ≠ 1⌋B, 1)]" by auto thenshow ?thesis using tps1_def by simp qed show"tps1 = tps0[j := tps0 ! j |:=| ◻]"if"read tps0 ! j ≠◻" proof - have"a = 1" using a that * by simp thenhave"(⌊if a = 1 then 0 else 1⌋N, 1) = (⌊0⌋N, 1)" by simp moreoverhave"tps0 ! j |:=| ◻ = (⌊0⌋N, 1)" using tps0 canrepr_0 canrepr_1 `a = 1` contents_snoc by (metis Suc_1 append_self_conv2 contents_blank_0 fst_eqD fun_upd_upd nat.inject nlength_0_simp numeral_2_eq_2 snd_eqD) ultimatelyhave"tps0[j := tps0 ! j |:=| ◻] = tps0[j := (⌊a ≠ 1⌋B, 1)]" by auto thenshow ?thesis using tps1_def by simp qed qed
end(* context *)
end(* locale *)
lemma transforms_tm_notI [transforms_intros]: fixes j :: tapeidx fixes tps tps' :: "tape list"and k :: nat and a :: nat assumes"j < k""length tps = k" and"a < 2" assumes"tps ! j = (⌊a⌋N, 1)" assumes"tps' = tps [j := (⌊a ≠ 1⌋B, 1)]" shows"transforms (tm_not j) tps 3 tps'" proof - interpret loc: turing_machine_not j . show ?thesis using assms loc.tps1_def loc.tm by simp qed
end
Messung V0.5 in Prozent
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.521Bemerkung:
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.