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
have 1: "length ?tps = Suc k"
using assms(5) by simp
have 2: "?tps ! j1 = (\<lfloor>xs\<rfloor>, 1)"
by (simp add: assms(9) assms(2) assms(5) nth_append)
have 3: "?tps ! j2 = (\<lfloor>ys\<rfloor>, 1)"
by (simp add: assms(10) assms(3) assms(5) nth_append)
have 4: "last ?tps = \<lceil>\<triangleright>\<rceil>"
by simp
have 5: "k \<ge> 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
moreover have "?tps' = tps' @ [\<lceil>\<zero>\<rceil>]"
using assms by (simp add: list_update_append)
ultimately have "transforms (tm_plus j1 j2) (tps @ [\<lceil>\<triangleright>\<rceil>]) t (tps' @ [\<lceil>\<zero>\<rceil>])"
by simp
moreover have "turing_machine (Suc k) 4 ?M"
using tm_plus_tm assms by simp
moreover have "immobile ?M k (Suc k)"
using tm_plus_immobile assms by simp
moreover have "bounded_write (tm_plus j1 j2) k 4"
using tm_plus_bounded_write[of j1 "Suc k"] assms(2) by simp
ultimately have "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
then show ?thesis
using tm_plus'_def by simp
qed
text \<open>
The next Turing machine is the one we actually use to add two numbers. After
computing the sum by running @{const tm_plus'}, it removes trailing zeros
and performs a carriage return on the tapes $j_1$ and $j_2$. \<close>
lemma tm_add_tm:
assumes "j2 > 0" and "k \<ge> 2" and "G \<ge> 4" and "j2 < k"
shows "turing_machine k G (tm_add j1 j2)"
unfolding tm_add_def using tm_plus'_tm tm_lconst_until_tm tm_cr_tm assms by simp
locale turing_machine_add =
fixes j1 j2 :: tapeidx
begin
lemma contents_canlen:
assumes "bit_symbols zs"
shows "\<lfloor>zs\<rfloor> (canlen zs) \<in> {h. h \<noteq> \<zero> \<and> \<box> < 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 (\<lfloor>?zs\<rfloor>, Suc n) {h. h \<noteq> \<zero> \<and> \<box> < h} ?ln"
proof (rule lneighI)
have "\<lfloor>?zs\<rfloor> (canlen ?zs) \<in> {h. h \<noteq> \<zero> \<and> \<box> < h}"
using contents_canlen[OF `bit_symbols ?zs`] by simp
moreover have "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)
ultimately have "\<lfloor>?zs\<rfloor> (Suc n - ?ln) \<in> {h. h \<noteq> \<zero> \<and> \<box> < h}"
by simp
then show "fst (\<lfloor>?zs\<rfloor>, Suc n) (snd (\<lfloor>?zs\<rfloor>, Suc n) - ?ln) \<in> {h. h \<noteq> \<zero> \<and> \<box> < h}"
by simp
have "\<lfloor>?zs\<rfloor> (Suc n - n') \<in> {\<box>, \<zero>}" if "n' < ?ln" for n'
proof (cases "Suc n - n' \<le> n")
case True
moreover have 1: "Suc n - n' > 0"
using that by simp
ultimately have "\<lfloor>?zs\<rfloor> (Suc n - n') = ?zs ! (Suc n - n' - 1)"
using contents_def by simp
moreover have "Suc n - n' - 1 < length ?zs"
using that True by simp
moreover have "Suc n - n' - 1 \<ge> canlen ?zs"
using that by simp
ultimately show ?thesis
using canlen_at_ge[of ?zs] by simp
next
case False
then show ?thesis
by simp
qed
then have "\<lfloor>?zs\<rfloor> (Suc n - n') \<notin> {h. h \<noteq> \<zero> \<and> \<box> < h}" if "n' < ?ln" for n'
using that by fastforce
then show "fst (\<lfloor>?zs\<rfloor>, Suc n) (snd (\<lfloor>?zs\<rfloor>, Suc n) - n') \<notin> {h. h \<noteq> \<zero> \<and> \<box> < h}"
if "n' < ?ln" for n'
using that by simp
qed
then show "lneigh (tps1 ! j2) {h. h \<noteq> \<zero> \<and> h \<noteq> \<box>} ?ln"
using assms tps1_def jk by simp
show "Suc n - canlen (map (sumdigit xs ys) [0..<n]) \<le> tps1 :#: j2" "Suc n - canlen (map (sumdigit xs ys) [0..<n]) \<le> 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
then have 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 (\<lfloor>?zs\<rfloor>, Suc n) \<box> ?ln =
(\<lfloor>canrepr (num xs + num ys)\<rfloor>, m)"
(is "lconstplant ?tp \<box> ?ln = _")
proof -
have "(if Suc n - ?ln < i \<and> i \<le> Suc n then \<box> else \<lfloor>?zs\<rfloor> i) = \<lfloor>take (canlen ?zs) ?zs\<rfloor> i"
(is "?lhs = ?rhs")
for i
proof -
consider "i = 0"
| "i > 0 \<and> i \<le> canlen ?zs"
| "i > canlen ?zs \<and> i \<le> Suc n"
| "i > canlen ?zs \<and> i > Suc n"
by linarith
then show ?thesis
proof (cases)
case 1
then show ?thesis
by simp
next
case 2
then have "i \<le> 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)
then have lhs: "?lhs = \<lfloor>?zs\<rfloor> i"
by simp
have "take (canlen ?zs) ?zs ! (i - 1) = ?zs ! (i - 1)"
using 2 by (metis Suc_diff_1 Suc_less_eq le_imp_less_Suc nth_take)
then have "?rhs = \<lfloor>?zs\<rfloor> i"
using 2 contents_inbounds len_canrepr local.canrepr not_le canlen_le_length
by (metis add_diff_inverse_nat add_leE)
then show ?thesis
using lhs by simp
next
case 3
then have "Suc n - ?ln < i \<and> i \<le> Suc n"
by (metis diff_diff_cancel less_imp_le_nat less_le_trans)
then have "?lhs = 0"
by simp
moreover have "?rhs = 0"
using 3 contents_outofbounds len_canrepr canrepr by metis
ultimately show ?thesis
by simp
next
case 4
then have "?lhs = 0"
by simp
moreover have "?rhs = 0"
using 4 contents_outofbounds len_canrepr canrepr by metis
ultimately show ?thesis
by simp
qed
qed
then have "(\<lambda>i. if Suc n - ?ln < i \<and> i \<le> Suc n then \<box> else \<lfloor>?zs\<rfloor> i) = \<lfloor>canrepr (num xs + num ys)\<rfloor>"
using canrepr by simp
moreover have "fst ?tp = \<lfloor>?zs\<rfloor>"
by simp
ultimately have "(\<lambda>i. if Suc n - ?ln < i \<and> i \<le> Suc n then 0 else fst ?tp i) = \<lfloor>canrepr (num xs + num ys)\<rfloor>" by metis
moreover have "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)
ultimately show ?thesis
using lconstplant[of ?tp 0 ?ln] by simp
qed
then show "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
then have 1: "length (canrepr (num xs + num ys)) = canlen ?zs"
using length_canrepr_canlen sumdigit_bit_symbols by blast
moreover have "length ?zs = n"
by simp
ultimately have "m \<le> 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"
using 1 by simp
also have "... = n + Suc (Suc n - m) + Suc n + 4 + m"
by simp
also have "... = n + Suc (Suc n) - m + Suc n + 4 + m"
using `m \<le> n` by simp
also have "... = n + Suc (Suc n) + Suc n + 4"
using `m \<le> n` by simp
also have "... = 3 * n + 7"
by simp
also have "... = ttt"
using assms by simp
finally have "n + Suc (Suc n - canlen ?zs) + Suc n + 2 + m + 2 = ttt" .
then show ?thesis
using tm4 by simp
qed
text \<open>
In this section we construct a Turing machine that multiplies two numbers, each
on its own tape, and writes the result to another tape. It employs the common
algorithm for multiplication, which for binary numbers requires only doubling a number and adding two numbers. For the latter we already have a TM; for the
former we are going to construct one. \<close>
subsubsection \<open>The common algorithm\<close>
text \<open>
For two numbers given as symbol sequences @{term xs} and @{term ys}, the common
algorithm maintains an intermediate result, initialized with 0, and scans @{term
xs} starting from the most significant digit. In each step the intermediate
result is multiplied by two, and if the current digit of @{term xs} is @{text \<one>}, the value of @{term ys} is added to the intermediate result. \<close>
fun prod :: "symbol list \<Rightarrow> symbol list \<Rightarrow> nat \<Rightarrow> 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 \<open>
After $i$ steps of the algorithm, the intermediate result is the product of @{term ys}
and the $i$ most significant bits of @{term xs}. \<close>
lemma prod:
assumes "i \<le> length xs"
shows "prod xs ys i = num (drop (length xs - i) xs) * num ys"
using assms
proof (induction i)
case 0
then show ?case
using num_def by simp
next
case (Suc i)
then have "i < length xs"
by simp
then have "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))
then show ?case
using num_Cons Suc by simp
qed
text \<open>
After @{term "length xs"} steps, the intermediate result is the final result: \<close>
corollary prod_eq_prod: "prod xs ys (length xs) = num xs * num ys"
using prod by simp
definition prod' :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where "prod' x y i \<equiv> prod (canrepr x) (canrepr y) i"
lemma prod': "prod' x y (nlength x) = x * y"
using prod_eq_prod prod'_def by (simp add: canrepr)
subsubsection \<open>Multiplying by two\<close>
text \<open>
Since we represent numbers with the least significant bit at the left, a
rted astheleast
digit command the shiftIt scansjava.lang.StringIndexOutOfBoundsException: Index 76 out of bounds for length 76
tape $j$ and memorizes the current symbol on the last tape. It only writes the
symbols \textbf{0} and \textbf{1}. \<close>
definition cmd_double :: "tapeidx \<Rightarrow> command" where "cmd_double j rs \<equiv>
(if rs ! j = \<box> then 1 else 0,
(map (\<lambda>i.
if i = j then
if last rs = \<triangleright> \<and> rs ! j = \<box> 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 \<ge> 2" and "G \<ge> 4" and "j > 0" and "j < k - 1"
shows "turing_command k 1 G (cmd_double j)"
proof
show "\<And>gs. length gs = k \<Longrightarrow> length ([!!] cmd_double j gs) = length gs"
using cmd_double_def by simp
show "\<And>gs. length gs = k \<Longrightarrow> 0 < k \<Longrightarrow> 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""\<And>i. i < length gs \<Longrightarrow> gs ! i < G""j' < length gs"
for j' gs
proof -
consider "j' = j" | "j' = k - 1" | "j' \<noteq> j \<and> j' \<noteq> k - 1"
by auto
then show ?thesis
proof (cases)
case 1
then have "cmd_double j gs [!] j' =
(if last gs = \<triangleright> \<and> gs ! j = \<box> then (gs ! j, Right)
else (tosym (todigit (last gs)), Right))"
using cmd_double_def assms(1,4) that(1) by simp
then have "cmd_double j gs [.] j' =
(if last gs = \<triangleright> \<and> gs ! j = \<box> then gs ! j else tosym (todigit (last gs)))"
by simp
then show ?thesis
using that assms by simp
next
case 2
then have "cmd_double j gs [!] j' = (tosym (todigit (gs ! j)), Stay)"
using cmd_double_def assms(1,4) that(1) by simp
then show ?thesis
using assms by simp
next
case 3
then show ?thesis
using cmd_double_def assms that by simp
qed
qed
show "\<And>gs. length gs = k \<Longrightarrow> [*] (cmd_double j gs) \<le> 1"
using assms cmd_double_def by simp
qed
lemma sem_cmd_double_0:
assumes "j < k"
and "bit_symbols xs"
and "i \<le> length xs"
and "i > 0"
and "length tps = Suc k"
and "tps ! j = (\<lfloor>xs\<rfloor>, i)"
and "tps ! k = \<lceil>z\<rceil>"
and "tps' = tps [j := tps ! j |:=| tosym (todigit z) |+| 1, k := \<lceil>xs ! (i - 1)\<rceil>]"
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"
then have 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)
then have rs23: "rs ! j = \<zero> \<or> rs ! j = \<one>"
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' \<noteq> j \<and> j' \<noteq> k"
by auto
then show ?thesis
proof (cases)
case 1
then have "j' < length rs"
using lenrs that by simp
then have "cmd_double j rs [!] j' =
(if last rs = \<triangleright> \<and> rs ! j = \<box> then (rs ! j, Right)
else (tosym (todigit (last rs)), Right))"
using cmd_double_def that 1 by simp
then have "cmd_double j rs [!] j' = (tosym (todigit (last rs)), Right)"
using rs23 lenrs assms by auto
moreover have "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))
ultimately show ?thesis
using act_Right' rs_def 1 assms(1,5,8) by simp
next
case 2
then have "j' = length rs - 1""j' \<noteq> j""j' < length rs"
using lenrs that assms(1) by simp_all
then have "(cmd_double j rs) [!] j' = (tosym (todigit (rs ! j)), Stay)"
using cmd_double_def by simp
then have "(cmd_double j rs) [!] j' = (xs ! (i - 1), Stay)"
using rsj rs23 by auto
then show ?thesis
using act_onesie rs_def 2 assms that by simp
next
case 3
then have "j' \<noteq> length rs - 1""j' \<noteq> j""j' < length rs"
using lenrs that by simp_all
then have "(cmd_double j rs) [!] j' = (rs ! j', Stay)"
using cmd_double_def by simp
then show ?thesis
using act_Stay rs_def assms that 3 by 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 = (\<lfloor>xs\<rfloor>, i)"
and "tps ! k = \<lceil>z\<rceil>"
and "tps' = tps
[j := tps ! j |:=| (if z = \<triangleright> then \<box> else tosym (todigit z)) |+| 1,
k := \<lceil>\<zero>\<rceil>]"
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"
then have rsj: "rs ! j = \<box>"
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' \<noteq> j \<and> j' \<noteq> k"
by auto
then show ?thesis
proof (cases)
case 1
then have "j' < length rs"
using lenrs that by simp
then have "cmd_double j rs [!] j' =
(if last rs = \<triangleright> \<and> rs ! j = \<box> then (rs ! j, Right)
else (tosym (todigit (last rs)), Right))"
using cmd_double_def that 1 by simp
moreover have "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))
ultimately have "cmd_double j rs [!] j' =
(if z = \<triangleright> then (\<box>, Right) else (tosym (todigit z), Right))"
using rsj 1 by simp
then show ?thesis
using act_Right' rs_def 1 assms(1,4,7) by simp
next
case 2
then have "j' = length rs - 1""j' \<noteq> j""j' < length rs"
using lenrs that assms(1) by simp_all
then have "(cmd_double j rs) [!] j' = (tosym (todigit (rs ! j)), Stay)"
using cmd_double_def by simp
then have "(cmd_double j rs) [!] j' = (2, Stay)"
using rsj by auto
then show ?thesis
using act_onesie rs_def 2 assms that by simp
next
case 3
then have "j' \<noteq> length rs - 1""j' \<noteq> j""j' < length rs"
using lenrs that by simp_all
then have "(cmd_double j rs) [!] j' = (rs ! j', Stay)"
using cmd_double_def by simp
then show ?thesis
using act_Stay rs_def assms that 3 by simp
qed
qed
qed
text \<open>
The next Turing machine consists just of the command @{const cmd_double}. \<close>
lemma tm_double_tm:
assumes "k \<ge> 2" and "G \<ge> 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 = (\<lfloor>xs\<rfloor>, 1)"
and "tps ! k = \<lceil>\<triangleright>\<rceil>"
and "t \<ge> 1"
and "t \<le> length xs"
shows "execute (tm_double j) (0, tps) t =
(0, tps [j := (\<lfloor>\<zero> # take (t - 1) xs @ drop t xs\<rfloor>, Suc t), k := \<lceil>xs ! (t - 1)\<rceil>])"
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
also have "... = sem (cmd_double j) (execute (tm_double j) (0, tps) 0)"
using tm_double_def exe_lt_length by simp
also have "... = sem (cmd_double j) (0, tps)"
by simp
also have "... = (0, tps [j := tps ! j |:=| tosym (todigit 1) |+| 1, k := \<lceil>xs ! (1 - 1)\<rceil>])"
using assms(7,8) sem_cmd_double_0[OF assms(1-2) _ _ assms(4,5,6)] by simp
also have "... = (0, tps [j := (\<lfloor>\<zero> # take (1 - 1) xs @ drop 1 xs\<rfloor>, Suc 1), k := \<lceil>xs ! (1 - 1)\<rceil>])"
proof -
have "tps ! j |:=| tosym (todigit 1) |+| 1 = (\<lfloor>xs\<rfloor>, 1) |:=| tosym (todigit 1) |+| 1"
using assms(5) by simp
also have "... = (\<lfloor>xs\<rfloor>(1 := tosym (todigit 1)), Suc 1)"
by simp
also have "... = (\<lfloor>xs\<rfloor>(1 := \<zero>), Suc 1)"
by auto
also have "... = (\<lfloor>\<zero> # drop 1 xs\<rfloor>, Suc 1)"
proof -
have "\<lfloor>\<zero> # drop 1 xs\<rfloor> = \<lfloor>xs\<rfloor>(1 := \<zero>)"
proof
fix i :: nat
consider "i = 0" | "i = 1" | "i > 1 \<and> i \<le> length xs" | "i > length xs"
by linarith
then show "\<lfloor>\<zero> # drop 1 xs\<rfloor> i = (\<lfloor>xs\<rfloor>(1 := \<zero>)) i"
proof (cases)
case 1
then show ?thesis
by simp
next
case 2
then show ?thesis
by simp
next
case 3
then have "\<lfloor>\<zero> # drop 1 xs\<rfloor> i = (\<zero> # drop 1 xs) ! (i - 1)"
using assms(3) by simp
also have "... = (drop 1 xs) ! (i - 2)"
using 3 by (metis Suc_1 diff_Suc_eq_diff_pred nth_Cons_pos zero_less_diff)
also have "... = xs ! (Suc (i - 2))"
using 3 assms(5) by simp
also have "... = xs ! (i - 1)"
using 3 by (metis Suc_1 Suc_diff_Suc)
also have "... = \<lfloor>xs\<rfloor> i"
using 3 by simp
also have "... = (\<lfloor>xs\<rfloor>(1 := \<zero>)) i"
using 3 by simp
finally show ?thesis .
next
case 4
then show ?thesis
by simp
qed
qed
then show ?thesis
by simp
qed
also have "... = (\<lfloor>\<zero> # take (1 - 1) xs @ drop 1 xs\<rfloor>, Suc 1)"
by simp
finally show ?thesis
by auto
qed
finally show ?case .
next
case (Suc t)
let ?xs = "\<zero> # take (t - 1) xs @ drop t xs"
let ?z = "xs ! (t - 1)"
let ?tps = "tps
[j := (\<lfloor>?xs\<rfloor>, Suc t),
k := \<lceil>?z\<rceil>]"
have lenxs: "length ?xs = length xs"
using Suc by simp
have 0: "?xs ! t = xs ! t"
proof -
have "t > 0"
using Suc by simp
then have "length (\<zero> # take (t - 1) xs) = t"
using Suc by simp
moreover have "length (drop t xs) > 0"
using Suc by simp
moreover have "drop t xs ! 0 = xs ! t"
using Suc by simp
ultimately have "((\<zero> # take (t - 1) xs) @ drop t xs) ! t = xs ! t"
by (metis diff_self_eq_0 less_not_refl3 nth_append)
then show ?thesis
by simp
qed
have 1: "bit_symbols ?xs"
proof -
have "bit_symbols (take (t - 1) xs)"
using assms(2) by simp
moreover have "bit_symbols (drop t xs)"
using assms(2) by simp
moreover have "bit_symbols [\<zero>]"
by simp
ultimately have "bit_symbols ([\<zero>] @ take (t - 1) xs @ drop t xs)"
using bit_symbols_append by presburger
then show ?thesis
by simp
qed
have 2: "Suc t \<le> length ?xs"
using Suc by simp
have 3: "Suc t > 0"
using Suc by simp
have 4: "length ?tps = Suc k"
using assms by simp
have 5: "?tps ! j = (\<lfloor>?xs\<rfloor>, Suc t)"
by (simp add: Suc_lessD assms(1,4) nat_neq_iff)
have 6: "?tps ! k = \<lceil>?z\<rceil>"
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
also have "... = sem (cmd_double j) (execute (tm_double j) (0, tps) t)"
using tm_double_def exe_lt_length Suc by simp
also have "... = sem (cmd_double j) (0, ?tps)"
using Suc by simp
also have "... = (0, ?tps [j := ?tps ! j |:=| tosym (todigit ?z) |+| 1, k := \<lceil>?xs ! (Suc t - 1)\<rceil>])"
using sem_cmd_double_0[OF assms(1) 123456] by simp
also have "... = (0, ?tps [j := ?tps ! j |:=| tosym (todigit ?z) |+| 1, k := \<lceil>xs ! (Suc t - 1)\<rceil>])"
using 0 by simp
also have "... = (0, tps [j := ?tps ! j |:=| tosym (todigit ?z) |+| 1, k := \<lceil>xs ! (Suc t - 1)\<rceil>])"
using assms by (smt (verit) list_update_overwrite list_update_swap)
also have "... = (0, tps [j := (\<lfloor>?xs\<rfloor>, Suc t) |:=| tosym (todigit ?z) |+| 1, k := \<lceil>xs ! (Suc t - 1)\<rceil>])"
using 5 by simp
also have "... = (0, tps
[j := (\<lfloor>?xs\<rfloor>(Suc t := tosym (todigit ?z)), Suc (Suc t)),
k := \<lceil>xs ! (Suc t - 1)\<rceil>])"
by simp
also have "... = (0, tps
[j := (\<lfloor>2 # take (Suc t - 1) xs @ drop (Suc t) xs\<rfloor>, Suc (Suc t)),
k := \<lceil>xs ! (Suc t - 1)\<rceil>])"
proof -
have "\<lfloor>?xs\<rfloor>(Suc t := tosym (todigit ?z)) = \<lfloor>\<zero> # take (Suc t - 1) xs @ drop (Suc t) xs\<rfloor>"
proof
fix i :: nat
consider "i = 0" | "i > 0 \<and> i < Suc t" | "i = Suc t" | "i > Suc t \<and> i \<le> length xs" | "i > length xs"
by linarith
then show "(\<lfloor>?xs\<rfloor>(Suc t := tosym (todigit ?z))) i = \<lfloor>\<zero> # take (Suc t - 1) xs @ drop (Suc t) xs\<rfloor> i"
proof (cases)
case 1
then show ?thesis
by simp
next
case 2
then have lhs: "(\<lfloor>?xs\<rfloor>(Suc t := tosym (todigit ?z))) i = ?xs ! (i - 1)"
using lenxs Suc by simp
have "\<lfloor>\<zero> # take (Suc t - 1) xs @ drop (Suc t) xs\<rfloor> i =
(\<zero> # take (Suc t - 1) xs @ drop (Suc t) xs) ! (i - 1)"
using Suc 2 by auto
then have "\<lfloor>\<zero> # take (Suc t - 1) xs @ drop (Suc t) xs\<rfloor> i =
((\<zero> # take (Suc t - 1) xs) @ drop (Suc t) xs) ! (i - 1)"
by simp
moreover have "length (\<zero> # take (Suc t - 1) xs) = Suc t"
using Suc.prems by simp
ultimately have "\<lfloor>\<zero> # take (Suc t - 1) xs @ drop (Suc t) xs\<rfloor> i =
(\<zero> # take (Suc t - 1) xs) ! (i - 1)"
using 2 by (metis Suc_diff_1 Suc_lessD nth_append)
also have "... = (\<zero> # take t xs) ! (i - 1)"
by simp
also have "... = (\<zero> # 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)
also have "... = ((\<zero> # take (t - 1) xs) @ [xs ! (t - 1)]) ! (i - 1)"
by simp
also have "... = (\<zero> # take (t - 1) xs) ! (i - 1)"
using 2 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)
also have "... = ((\<zero> # take (t - 1) xs) @ drop t xs) ! (i - 1)"
using 2 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)
also have "... = ?xs ! (i - 1)"
by simp
finally have "\<lfloor>\<zero> # take (Suc t - 1) xs @ drop (Suc t) xs\<rfloor> i = ?xs ! (i - 1)" .
then show ?thesis
using lhs by simp
next
case 3
moreover have "?z = \<zero> \<or> ?z = \<one>"
using `bit_symbols ?xs` Suc assms(2) by (metis Suc_diff_le Suc_leD Suc_le_lessD diff_Suc_1)
ultimately have lhs: "(\<lfloor>?xs\<rfloor>(Suc t := tosym (todigit ?z))) i = ?z"
by auto
have "\<lfloor>\<zero> # take (Suc t - 1) xs @ drop (Suc t) xs\<rfloor> i = \<lfloor>(\<zero> # take t xs) @ drop (Suc t) xs\<rfloor> (Suc t)"
using 3 by simp
also have "... = ((\<zero> # take t xs) @ drop (Suc t) xs) ! t"
using 3 Suc by simp
also have "... = (\<zero> # take t xs) ! t"
using Suc by (metis Suc_leD length_Cons length_take lessI min_absorb2 nth_append)
also have "... = xs ! (t - 1)"
using Suc by simp
finally have "\<lfloor>\<zero> # take (Suc t - 1) xs @ drop (Suc t) xs\<rfloor> i = ?z" .
then show ?thesis
using lhs by simp
next
case 4
then have "(\<lfloor>?xs\<rfloor>(Suc t := tosym (todigit ?z))) i = \<lfloor>?xs\<rfloor> i"
by simp
also have "... = ?xs ! (i - 1)"
using 4 by auto
also have "... = ((\<zero> # take (t - 1) xs) @ drop t xs) ! (i - 1)"
by simp
also have "... = drop t xs ! (i - 1 - t)"
using 4 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)
also have "... = xs ! (i - 1)"
using 4 Suc by simp
finally have lhs: "(\<lfloor>?xs\<rfloor>(Suc t := tosym (todigit ?z))) i = xs ! (i - 1)" .
have "\<lfloor>\<zero> # take (Suc t - 1) xs @ drop (Suc t) xs\<rfloor> i =
(\<zero> # take (Suc t - 1) xs @ drop (Suc t) xs) ! (i - 1)"
using 4 by auto
also have "... = ((\<zero> # take t xs) @ drop (Suc t) xs) ! (i - 1)"
by simp
also have "... = (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)
also have "... = xs ! (i - 1)"
using Suc 4 Suc_lessE by fastforce
finally have "\<lfloor>\<zero> # take (Suc t - 1) xs @ drop (Suc t) xs\<rfloor> i = xs ! (i - 1)" .
then show ?thesis
using lhs by simp
next
case 5
then have "(\<lfloor>?xs\<rfloor>(Suc t := tosym (todigit ?z))) i = \<lfloor>?xs\<rfloor> i"
using Suc by simp
then have lhs: "(\<lfloor>?xs\<rfloor>(Suc t := tosym (todigit ?z))) i = \<box>"
using 5 contents_outofbounds lenxs by simp
have "length (\<zero> # take (Suc t - 1) xs @ drop (Suc t) xs) = length xs"
using Suc by simp
then have "\<lfloor>\<zero> # take (Suc t - 1) xs @ drop (Suc t) xs\<rfloor> i = \<box>"
using 5 contents_outofbounds by simp
then show ?thesis
using lhs by simp
qed
qed
then show ?thesis
by simp
qed
finally show ?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 = (\<lfloor>xs\<rfloor>, 1)"
and "tps ! k = \<lceil>\<triangleright>\<rceil>"
shows "execute (tm_double j) (0, tps) (Suc (length xs)) =
(1, tps [j := (\<lfloor>\<zero> # xs\<rfloor>, length xs + 2), k := \<lceil>\<zero>\<rceil>])"
proof -
let ?z = "xs ! (length xs - 1)"
let ?xs = "\<zero> # take (length xs - 1) xs"
have "?z \<noteq> \<triangleright>"
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 = \<zero> \<or> ?z = \<one>"
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)
have 0: "bit_symbols ?xs"
using assms(2) bit_symbols_append[of "[\<zero>]""take (length xs - 1) xs"] by simp
have "execute (tm_double j) (0, tps) (length xs) =
(0, tps
[j := (\<lfloor>\<zero> # take (length xs - 1) xs @ drop (length xs) xs\<rfloor>, Suc (length xs)),
k := \<lceil>?z\<rceil>])"
using execute_tm_double_0[OF assms(1-6), where ?t="length xs"] assms(3) by simp
then have *: "execute (tm_double j) (0, tps) (length xs) =
(0, tps [j := (\<lfloor>?xs\<rfloor>, Suc (length ?xs)), k := \<lceil>?z\<rceil>])"
(is "_ = (0, ?tps)")
using lenxs by simp
let ?i = "Suc (length ?xs)"
have 1: "?i > length ?xs"
by simp
have 2: "length ?tps = Suc k"
using assms(4) by simp
have 3: "?tps ! j = (\<lfloor>?xs\<rfloor>, ?i)"
using assms(1,4) by simp
have 4: "?tps ! k = \<lceil>?z\<rceil>"
using assms(4) by simp
have "execute (tm_double j) (0, tps) (Suc (length xs)) = exe (tm_double j) (0, ?tps)"
using * by simp
also have "... = sem (cmd_double j) (0, ?tps)"
using tm_double_def exe_lt_length by simp
also have "... = (1, ?tps
[j := ?tps ! j |:=| (if ?z = \<triangleright> then \<box> else tosym (todigit ?z)) |+| 1,
k := \<lceil>\<zero>\<rceil>])"
using sem_cmd_double_1[OF assms(1) 01234] by simp
also have "... = (1, ?tps
[j := ?tps ! j |:=| (tosym (todigit ?z)) |+| 1,
k := \<lceil>\<zero>\<rceil>])"
using `?z \<noteq> 1` by simp
also have "... = (1, ?tps
[j := (\<lfloor>?xs\<rfloor>, Suc (length ?xs)) |:=| (tosym (todigit ?z)) |+| 1,
k := \<lceil>\<zero>\<rceil>])"
using 3 by simp
also have "... = (1, ?tps
[j := (\<lfloor>?xs\<rfloor>, Suc (length ?xs)) |:=| ?z |+| 1,
k := \<lceil>\<zero>\<rceil>])"
using z23 One_nat_def Suc_1 add_2_eq_Suc' numeral_3_eq_3 by presburger
also have "... = (1, tps
[j := (\<lfloor>?xs\<rfloor>, Suc (length ?xs)) |:=| ?z |+| 1,
k := \<lceil>\<zero>\<rceil>])"
by (smt (verit) list_update_overwrite list_update_swap)
also have "... = (1, tps
[j := (\<lfloor>?xs\<rfloor>(Suc (length ?xs) := ?z), length ?xs + 2),
k := \<lceil>\<zero>\<rceil>])"
by simp
also have "... = (1, tps
[j := (\<lfloor>?xs\<rfloor>(Suc (length ?xs) := ?z), length xs + 2),
k := \<lceil>\<zero>\<rceil>])"
using lenxs by simp
also have "... = (1, tps [j := (\<lfloor>\<zero> # xs\<rfloor>, length xs + 2), k := \<lceil>\<zero>\<rceil>])"
proof -
have "\<lfloor>?xs\<rfloor>(Suc (length ?xs) := ?z) = \<lfloor>\<zero> # xs\<rfloor>"
proof
fix i
consider "i = 0" | "i > 0 \<and> i \<le> length xs" | "i = Suc (length xs)" | "i > Suc (length xs)"
by linarith
then show "(\<lfloor>?xs\<rfloor>(Suc (length ?xs) := ?z)) i = \<lfloor>\<zero> # xs\<rfloor> i"
proof (cases)
case 1
then show ?thesis
by simp
next
case 2
then have "(\<lfloor>?xs\<rfloor>(Suc (length ?xs) := ?z)) i = \<lfloor>?xs\<rfloor> i"
using lenxs by simp
also have "... = ?xs ! (i - 1)"
using 2 by auto
also have "... = (\<zero> # xs) ! (i - 1)"
using lenxs 2 assms(3) by (metis Suc_diff_1 Suc_le_lessD nth_take take_Suc_Cons)
also have "... = \<lfloor>\<zero> # xs\<rfloor> i"
using 2 by simp
finally show ?thesis .
next
case 3
then have lhs: "(\<lfloor>?xs\<rfloor>(Suc (length ?xs) := ?z)) i = ?z"
using lenxs by simp
have "\<lfloor>\<zero> # xs\<rfloor> i = (\<zero> # xs) ! (i - 1)"
using 3 lenxs by simp
also have "... = xs ! (i - 2)"
using 3 assms(3) by simp
also have "... = ?z"
using 3 by simp
finally have "\<lfloor>\<zero> # xs\<rfloor> i = ?z" .
then show ?thesis
using lhs by simp
next
case 4
then show ?thesis
using 4 lenxs by simp
qed
qed
then show ?thesis
by simp
qed
finally show ?thesis .
qed
lemma execute_tm_double_Nil:
assumes "j < k"
and "length tps = Suc k"
and "tps ! j = (\<lfloor>[]\<rfloor>, 1)"
and "tps ! k = \<lceil>\<triangleright>\<rceil>"
shows "execute (tm_double j) (0, tps) (Suc 0) =
(1, tps [j := (\<lfloor>[]\<rfloor>, 2), k := \<lceil>\<zero>\<rceil>])"
proof -
have "execute (tm_double j) (0, tps) (Suc 0) = exe (tm_double j) (execute (tm_double j) (0, tps) 0)"
by simp
also have "... = exe (tm_double j) (0, tps)"
by simp
also have "... = sem (cmd_double j) (0, tps)"
using tm_double_def exe_lt_length by simp
also have "... = (1, tps
[j := tps ! j |:=| (if (1::nat) = 1 then 0 else tosym (todigit 1)) |+| 1,
k := \<lceil>\<zero>\<rceil>])"
using sem_cmd_double_1[OF assms(1) _ _ assms(2-4)] by simp
also have "... = (1, tps [j := tps ! j |:=| \<box> |+| 1, k := \<lceil>\<zero>\<rceil>])"
by simp
also have "... = (1, tps [j := (\<lfloor>[]\<rfloor>, 1) |:=| \<box> |+| 1, k := \<lceil>\<zero>\<rceil>])"
using assms(3) by simp
also have "... = (1, tps [j := (\<lfloor>[]\<rfloor>(1 := \<box>), 2), k := \<lceil>\<zero>\<rceil>])"
by (metis fst_eqD one_add_one snd_eqD)
also have "... = (1, tps [j := (\<lfloor>[]\<rfloor>, 2), k := \<lceil>\<zero>\<rceil>])"
by (metis contents_outofbounds fun_upd_idem_iff list.size(3) zero_less_one)
finally show ?thesis .
qed
lemma execute_tm_double:
assumes "j < k"
and "length tps = Suc k"
and "tps ! j = (\<lfloor>canrepr n\<rfloor>, 1)"
and "tps ! k = \<lceil>\<triangleright>\<rceil>"
shows "execute (tm_double j) (0, tps) (Suc (length (canrepr n))) =
(1, tps [j := (\<lfloor>canrepr (2 * n)\<rfloor>, length (canrepr n) + 2), k := \<lceil>\<zero>\<rceil>])"
proof (cases "n = 0")
case True
then have "canrepr n = []"
using canrepr_0 by simp
then show ?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 (\<zero> # ?xs) = 2 * num ?xs"
using num_Cons by simp
then have "num (\<zero> # ?xs) = 2 * n"
using canrepr by simp
moreover have "canonical (\<zero> # ?xs)"
proof -
have "?xs \<noteq> []"
using False canrepr canrepr_0 by metis
then show ?thesis
using canonical_Cons canonical_canrepr by simp
qed
ultimately have "canrepr (2 * n) = \<zero> # ?xs"
using canreprI by blast
then show ?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 = (\<lfloor>canrepr n\<rfloor>, 1)"
shows "execute (tm_double j) (0, tps @ [\<lceil>\<triangleright>\<rceil>]) (Suc (length (canrepr n))) =
(1, tps [j := (\<lfloor>canrepr (2 * n)\<rfloor>, length (canrepr n) + 2)] @ [\<lceil>\<zero>\<rceil>])"
proof -
let ?tps = "tps @ [\<lceil>\<triangleright>\<rceil>]"
have "length ?tps = Suc k"
using assms(2) by simp
moreover have "?tps ! j = (\<lfloor>canrepr n\<rfloor>, 1)"
using assms(1,2,3) by (simp add: nth_append)
moreover have "?tps ! k = \<lceil>\<triangleright>\<rceil>"
using assms(2) by (simp add: nth_append)
moreover have "tps [j := (\<lfloor>canrepr (2 * n)\<rfloor>, length (canrepr n) + 2)] @ [\<lceil>\<zero>\<rceil>] =
?tps [j := (\<lfloor>canrepr (2 * n)\<rfloor>, length (canrepr n) + 2), k := \<lceil>\<zero>\<rceil>]"
using assms by (metis length_list_update list_update_append1 list_update_length)
ultimately show ?thesis
using assms execute_tm_double[OF assms(1), where ?tps="tps @ [\<lceil>\<triangleright>\<rceil>]"]
by simp
qed
lemma tm_double_immobile:
fixes k :: nat
assumes "j > 0" and "j < k"
shows "immobile (tm_double j) k (Suc k)"
proof -
let ?M = "tm_double j"
{ fix q :: nat and rs :: "symbol list"
assume q: "q < length ?M"
assume rs: "length rs = Suc k"
then have len: "length rs - 1 = k"
by simp
have neq: "k \<noteq> j"
using assms(2) by simp
have "?M ! q = cmd_double j"
using tm_double_def q by simp
moreover have "(cmd_double j) rs [!] k = (tosym (todigit (rs ! j)), Stay)"
using cmd_double_def rs len neq by fastforce
ultimately have "(cmd_double j) rs [~] k = Stay"
by simp
}
then show ?thesis
by (simp add: immobile_def tm_double_def)
qed
lemma tm_double_bounded_write:
assumes "j < k - 1"
shows "bounded_write (tm_double j) (k - 1) 4"
using assms cmd_double_def tm_double_def bounded_write_def by simp
text \<open>
The next Turing machine removes the memorization tape. \<close>
lemma tm_double'_tm:
assumes "j > 0" and "k \<ge> 2" and "G \<ge> 4" and "j < k"
shows "turing_machine k G (tm_double' j)"
unfolding tm_double'_def using assms cartesian_tm tm_double_tm by simp
lemma transforms_tm_double'I [transforms_intros]:
assumes "j > 0" and "j < k"
and "length tps = k"
and "tps ! j = (\<lfloor>canrepr n\<rfloor>, 1)"
and "t = (Suc (length (canrepr n)))"
and "tps' = tps [j := (\<lfloor>canrepr (2 * n)\<rfloor>, length (canrepr n) + 2)]"
shows "transforms (tm_double' j) tps t tps'"
unfolding tm_double'_def
proof (rule cartesian_transforms_onesie)
show "turing_machine (Suc k) 4 (tm_double j)"
using assms(1,2) tm_double_tm by simp
show "length tps = k""2 \<le> k""(1::nat) < 4"
using assms by simp_all
show "bounded_write (tm_double j) k 4"
by (metis assms(2) diff_Suc_1 tm_double_bounded_write)
show "immobile (tm_double j) k (Suc k)"
by (simp add: assms(1,2) tm_double_immobile)
show "transforms (tm_double j) (tps @ [\<lceil>\<triangleright>\<rceil>]) t (tps' @ [\<lceil>\<zero>\<rceil>])"
using assms transforms_tm_double by simp
qed
text \<open>
The next Turing machine is the one we actually use to double a number. It runs
@{const tm_double'} and performs a carriage return. \<close>
lemma tm_times2_tm:
assumes "k \<ge> 2" and "j > 0" and "j < k" and "G \<ge> 4"
shows "turing_machine k G (tm_times2 j)"
using assms by (simp add: assms(1) tm_cr_tm tm_double'_tm tm_times2_def)
lemma transforms_tm_times2I [transforms_intros]:
assumes "j > 0" and "j < k"
and "length tps = k"
and "tps ! j = (\<lfloor>n\<rfloor>\<^sub>N, 1)"
and "t = 5 + 2 * nlength n"
and "tps' = tps [j := (\<lfloor>2 * n\<rfloor>\<^sub>N, 1)]"
shows "transforms (tm_times2 j) tps t tps'"
unfolding tm_times2_def
proof (tform tps: assms)
show "clean_tape (tps[j := (\<lfloor>2 * n\<rfloor>\<^sub>N, nlength n + 2)] ! j)"
using clean_tape_ncontents assms by simp
show "t = Suc (nlength n) + (tps[j := (\<lfloor>2 * n\<rfloor>\<^sub>N, nlength n + 2)] :#: j + 2)"
using assms by simp
qed
text \<open>
Before we can multiply arbitrary numbers we need just a few more lemmas.
\null \<close>
lemma num_drop_le_nu: "num (drop j xs) \<le> num xs"
proof (cases "j \<le> length xs")
case True
let ?ys = "drop j xs"
have map_shift_upt: "map (\<lambda>i. f (j + i)) [0..<l] = map f [j..<j + l]"
for f :: "nat \<Rightarrow> nat" and j l
by (rule nth_equalityI) simp_all
have "num ?ys = (\<Sum>i\<leftarrow>[0..<length ?ys]. todigit (?ys ! i) * 2 ^ i)"
using num_def by simp
also have "... = (\<Sum>i\<leftarrow>[0..<length ?ys]. todigit (xs ! (j + i)) * 2 ^ i)"
by (simp add: True)
also have "... \<le> 2 ^ j * (\<Sum>i\<leftarrow>[0..<length ?ys]. todigit (xs ! (j + i)) * 2 ^ i)"
by simp
also have "... = (\<Sum>i\<leftarrow>[0..<length ?ys]. 2 ^ j * todigit (xs ! (j + i)) * 2 ^ i)"
by (simp add: mult.assoc sum_list_const_mult)
also have "... = (\<Sum>i\<leftarrow>[0..<length ?ys]. todigit (xs ! (j + i)) * 2 ^ (j + i))"
by (simp add: ab_semigroup_mult_class.mult_ac(1) mult.commute power_add)
also have "... = (\<Sum>i\<leftarrow>[j..<j + length ?ys]. todigit (xs ! i) * 2 ^ i)"
using map_shift_upt[of "\<lambda>i. todigit (xs ! i) * 2 ^ i" j "length ?ys"] by simp
also have "... \<le> (\<Sum>i\<leftarrow>[0..<j]. todigit (xs ! i) * 2 ^ i) +
(\<Sum>i\<leftarrow>[j..<j + length ?ys]. todigit (xs ! i) * 2 ^ i)"
by simp
also have "... = (\<Sum>i\<leftarrow>[0..<j + length ?ys]. todigit (xs ! i) * 2 ^ i)"
by (metis (no_types, lifting) le_add2 le_add_same_cancel2 map_append sum_list.append upt_add_eq_append)
also have "... = (\<Sum>i\<leftarrow>[0..<length xs]. todigit (xs ! i) * 2 ^ i)"
by (simp add: True)
also have "... = num xs"
using num_def by simp
finally show ?thesis .
next
case False
then show ?thesis
using canrepr canrepr_0 by (metis drop_all nat_le_linear zero_le)
qed
lemma nlength_prod_le_prod:
assumes "i \<le> length xs"
shows "nlength (prod xs ys i) \<le> 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 \<le> nlength x"
shows "nlength (prod' x y i) \<le> 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 \<le> num xs * num ys"
proof -
have "2 * prod xs ys i \<le> prod xs ys (Suc i)"
by simp
also have "... = num (drop (length xs - Suc i) xs) * num ys"
using prod[of "Suc i" xs] assms by simp
also have "... \<le> num xs * num ys"
using num_drop_le_nu by simp
finally show ?thesis .
qed
corollary two_times_prod':
assumes "i < nlength x"
shows "2 * prod' x y i \<le> x * y"
using assms two_times_prod prod'_def by (metis prod' prod_eq_prod)
text \<open>
The next Turing machine multiplies the numbers on tapes $j_1$ and $j_2$ and
writes the result to tape $j_3$. It iterates over the binary digits on $j_1$
starting from the most significant digit. In each iteration it doubles the
intermediate result on $j_3$. If the current digit is @{text \<one>}, the number on
$j_2$ is added to $j_3$. \<close>
lemma tm2 [transforms_intros]:
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> tps0
[j1 := (\<lfloor>x\<rfloor>\<^sub>N, nlength x - t),
j3 := (\<lfloor>prod' x y t\<rfloor>\<^sub>N, 1)]"
definition "tpsL1 t \<equiv> tps0
[j1 := (\<lfloor>x\<rfloor>\<^sub>N, nlength x - t),
j3 := (\<lfloor>2 * prod' x y t\<rfloor>\<^sub>N, 1)]"
definition "tpsL2 t \<equiv> tps0
[j1 := (\<lfloor>x\<rfloor>\<^sub>N, nlength x - t),
j3 := (\<lfloor>prod' x y (Suc t)\<rfloor>\<^sub>N, 1)]"
definition "tpsL3 t \<equiv> tps0
[j1 := (\<lfloor>x\<rfloor>\<^sub>N, nlength x - t - 1),
j3 := (\<lfloor>prod' x y (Suc t)\<rfloor>\<^sub>N, 1)]"
lemma tmIf [transforms_intros]:
assumes "t < nlength x" and "ttt = 12 + 3 * nlength (x * y)"
shows "transforms tmIf (tpsL1 t) ttt (tpsL2 t)"
unfolding tmIf_def
proof (tform tps: assms tpsL1_def tps0 jk)
have "nlength y \<le> nlength (x * y) \<and> nlength (2 * prod' x y t) \<le> nlength (x * y)"
proof
have "x > 0"
using assms(1) gr_implies_not_zero nlength_0 by auto
then have "y \<le> x * y"
by simp
then show "nlength y \<le> nlength (x * y)"
using nlength_mono by simp
show "nlength (2 * prod' x y t) \<le> nlength (x * y)"
using assms(1) by (simp add: nlength_mono two_times_prod')
qed
then show "3 * max (nlength y) (nlength (2 * Arithmetic.prod' x y t)) + 10 + 2 \<le> ttt"
using assms(2) by simp
let ?xs = "canrepr x" and ?ys = "canrepr y"
let ?r = "read (tpsL1 t) ! j1"
have "?r = (\<lfloor>x\<rfloor>\<^sub>N) (nlength x - t)"
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: "?r = canrepr x ! (nlength x - 1 - t)"
using assms contents_def by simp
have "prod' x y (Suc t) = 2 * prod' x y t + (if ?xs ! (length ?xs - 1 - t) = \<one> then num ?ys else 0)"
using prod'_def by simp
also have "... = 2 * prod' x y t + (if ?r = \<one> then num ?ys else 0)"
using r by simp
also have "... = 2 * prod' x y t + (if ?r = \<one> then y else 0)"
using canrepr by simp
finally have "prod' x y (Suc t) = 2 * prod' x y t + (if ?r = \<one> then y else 0)" .
then show "read (tpsL1 t) ! j1 \<noteq> \<one> \<Longrightarrow> tpsL2 t = tpsL1 t"
and "read (tpsL1 t) ! j1 = \<one> \<Longrightarrow>
tpsL2 t = (tpsL1 t) [j3 := (\<lfloor>y + 2 * Arithmetic.prod' x y t\<rfloor>\<^sub>N, 1)]"
by (simp_all add: add.commute tpsL1_def tpsL2_def)
qed
lemma tmBody1 [transforms_intros]:
assumes "t < nlength x"
and "ttt = 17 + 2 * nlength (Arithmetic.prod' x y t) + 3 * nlength (x * y)"
shows "transforms tmBody1 (tpsL t) ttt (tpsL2 t)"
unfolding tmBody1_def by (tform tps: jk tpsL_def tpsL1_def assms(1) time: assms(2))
lemma tmBody:
assumes "t < nlength x"
and "ttt = 6 + 2 * nlength (prod' x y t) + (12 + 3 * nlength (x * y))"
shows "transforms tmBody (tpsL t) ttt (tpsL (Suc t))"
unfolding tmBody_def by (tform tps: jk tpsL_def tpsL2_def assms(1) time: assms(2))
lemma tmBody' [transforms_intros]:
assumes "t < nlength x" and "ttt = 18 + 5 * nlength (x * y)"
shows "transforms tmBody (tpsL t) ttt (tpsL (Suc t))"
proof -
have "6 + 2 * nlength (prod' x y t) + (12 + 3 * nlength (x * y)) \<le> 18 + 5 * nlength (x * y)"
using assms nlength_prod'_le_prod by simp
then show ?thesis
using tmBody assms transforms_monotone by blast
qed
lemma read_contents:
fixes tps :: "tape list" and j :: tapeidx and zs :: "symbol list"
assumes "tps ! j = (\<lfloor>zs\<rfloor>, i)" and "i > 0" and "i \<le> length zs" and "j < length tps"
shows "read tps ! j = zs ! (i - 1)"
using assms tapes_at_read' by fastforce
lemma tmWhile [transforms_intros]:
assumes "ttt = 1 + 25 * (nlength x + nlength y) * (nlength x + nlength y)"
shows "transforms tmWhile (tpsL 0) ttt (tpsL (nlength x))"
unfolding tmWhile_def
proof (tform)
show "read (tpsL i) ! j1 \<noteq> \<triangleright>" if "i < nlength x" for i
proof -
have "(tpsL i) ! j1 = (\<lfloor>x\<rfloor>\<^sub>N, nlength x - i)"
using tpsL_def jk by simp
moreover have *: "nlength x - i > 0""nlength x - i \<le> length (canrepr x)"
using that by simp_all
moreover have "length (tpsL i) = k"
using tpsL_def jk by simp
ultimately have "read (tpsL i) ! j1 = canrepr x ! (nlength x - i - 1)"
using jk read_contents by simp
then show ?thesis
using * bit_symbols_canrepr
by (metis One_nat_def Suc_le_lessD Suc_pred less_numeral_extra(4) proper_symbols_canrepr)
qed
show "\<not> read (tpsL (nlength x)) ! j1 \<noteq> \<triangleright>"
proof -
have "(tpsL (nlength x)) ! j1 = (\<lfloor>x\<rfloor>\<^sub>N, nlength x - nlength x)"
using tpsL_def jk by simp
then have "(tpsL (nlength x)) ! j1 = (\<lfloor>x\<rfloor>\<^sub>N, 0)"
by simp
then have "read (tpsL (nlength x)) ! j1 = \<triangleright>"
using tapes_at_read' tpsL_def contents_at_0 jk by (metis fst_conv length_list_update snd_conv)
then show ?thesis
by simp
qed
show "nlength x * (18 + 5 * nlength (x * y) + 2) + 1 \<le> ttt"
proof (cases "x = 0")
case True
then show ?thesis
using assms by simp
next
case False
have "nlength x * (18 + 5 * nlength (x * y) + 2) + 1 = nlength x * (20 + 5 * nlength (x * y)) + 1"
by simp
also have "... \<le> nlength x * (20 + 5 * (nlength x + nlength y)) + 1"
using nlength_prod by (meson add_mono le_refl mult_le_mono)
also have "... \<le> nlength x * (20 * (nlength x + nlength y) + 5 * (nlength x + nlength y)) + 1"
proof -
have "1 \<le> nlength x + nlength y"
using False nlength_0 by (simp add: Suc_leI)
then show ?thesis
by simp
qed
also have "... \<le> nlength x * (25 * (nlength x + nlength y)) + 1"
by simp
also have "... \<le> (nlength x + nlength y) * (25 * (nlength x + nlength y)) + 1"
by simp
finally show ?thesis
using assms by linarith
qed
qed
lemma tm3:
assumes "ttt = Suc (Suc (nlength x)) +
Suc ((25 * nlength x + 25 * nlength y) * (nlength x + nlength y))"
shows "transforms tm3 tps0 ttt (tpsL (nlength x))"
unfolding tm3_def
proof (tform time: assms)
show "tpsL 0 = tps2"
proof -
have "prod' x y 0 = 0"
using prod'_def by simp
then show ?thesis
using tpsL_def tps2_def jk tps0 by (metis diff_zero list_update_id list_update_swap)
qed
qed
lemma tm4:
assumes "ttt = 4 + 26 * (nlength x + nlength y) * (nlength x + nlength y)"
shows "transforms tm4 tps0 ttt tps4"
unfolding tm4_def
proof (tform tps: tps3_def jk time: assms)
show "tps4 = tps3[j1 := tps3 ! j1 |+| 1]"
using tps4_def tps3_def jk tps0
by (metis One_nat_def add.right_neutral add_Suc_right fst_conv list_update_id list_update_overwrite
list_update_swap nth_list_update_eq nth_list_update_neq snd_conv)
qed
end (* context x y k tps0 *)
end (* locale turing_machine_mult *)
lemma transforms_tm_mult [transforms_intros]:
fixes j1 j2 j3 :: tapeidx and x y k ttt :: nat and tps tps' :: "tape list"
assumes "j1 \<noteq> j2""j2 \<noteq> j3""j3 \<noteq> j1""j3 > 0"
assumes "length tps = k"
and "j1 < k""j2 < k""j3 < k"
and "tps ! j1 = (\<lfloor>x\<rfloor>\<^sub>N, 1)"
and "tps ! j2 = (\<lfloor>y\<rfloor>\<^sub>N, 1)"
and "tps ! j3 = (\<lfloor>0\<rfloor>\<^sub>N, 1)"
and "ttt = 4 + 26 * (nlength x + nlength y) * (nlength x + nlength y)"
and "tps' = tps [j3 := (\<lfloor>x * y\<rfloor>\<^sub>N, 1)]"
shows "transforms (tm_mult j1 j2 j3) tps ttt tps'"
proof -
interpret loc: turing_machine_mult j1 j2 j3 .
show ?thesis
using assms loc.tps4_def loc.tm4 loc.tm4_eq_tm_mult by metis
qed
subsection \<open>Powers\<close>
text \<open>
In this section we construct for every $d \in\nat$ a Turing machine that
computes $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
intermediate values. The TMs initialize tape $j_3$ with~1 and then multiply this
value by $n$ for $d$ times using the TM @{const tm_mult}. \<close>
lemma tm3:
assumes "ttt = 38 + 7 * nlength y + (26 * nlength x + 26 * nlength y) * (nlength x + nlength y)"
shows "transforms tm3 tps0 ttt tps3"
unfolding tm3_def
proof (tform tps: jk tps2_def time: assms)
show "tps3 = tps2[j2 := (\<lfloor>0\<rfloor>\<^sub>N, 1)]"
using tps3_def tps2_def jk by (metis list_update_id list_update_overwrite list_update_swap tps0(2))
qed
lemma tm3':
assumes "ttt = 38 + 33 * (nlength x + nlength y) ^ 2"
shows "transforms tm3 tps0 ttt tps3"
proof -
have "38 + 7 * nlength y + (26 * nlength x + 26 * nlength y) * (nlength x + nlength y) = 38 + 7 * nlength y + 26 * (nlength x + nlength y) * (nlength x + nlength y)"
by simp
also have "... \<le> 38 + 33 * (nlength x + nlength y) * (nlength x + nlength y)"
proof -
have "nlength y \<le> (nlength x + nlength y) * (nlength x + nlength y)"
by (meson le_add2 le_square le_trans)
then show ?thesis
by linarith
qed
also have "... = 38 + 33 * (nlength x + nlength y) ^ 2"
by algebra
finally have "38 + 7 * nlength y + (26 * nlength x + 26 * nlength y) * (nlength x + nlength y) \<le> ttt"
using assms(1) by simp
then show ?thesis
using tm3 transforms_monotone assms by meson
qed
end (* context x y k tps0 *)
lemma tm3'' [transforms_intros]:
fixes x d k :: nat and tps0 :: "tape list"
assumes "k = length tps0"
and "j1 < k""j2 < k""j3 < k"
assumes j_neq [simp]: "j1 \<noteq> j2""j2 \<noteq> j3""j3 \<noteq> j1"
and j_gt [simp]: "0 < j2""0 < j3""0 < j1"
and "tps0 ! j1 = (\<lfloor>x\<rfloor>\<^sub>N, 1)"
and "tps0 ! j2 = (\<lfloor>0\<rfloor>\<^sub>N, 1)"
and "tps0 ! j3 = (\<lfloor>x ^ d\<rfloor>\<^sub>N, 1)"
and "ttt = 71 + 99 * (Suc d) ^ 2 * (nlength x) ^ 2"
and "tps' = tps0 [j3 := (\<lfloor>x ^ Suc d\<rfloor>\<^sub>N, 1)]"
shows "transforms tm3 tps0 ttt tps'"
proof -
let ?l = "nlength x"
have "transforms tm3 tps0 (38 + 33 * (nlength x + nlength (x ^ d)) ^ 2) tps'"
using tm3' assms tps3_def by simp
moreover have "38 + 33 * (nlength x + nlength (x ^ d)) ^ 2 \<le> 71 + 99 * (Suc d) ^ 2 * ?l ^ 2"
proof -
have "38 + 33 * (nlength x + nlength (x ^ d)) ^ 2 \<le> 38 + 33 * (Suc (Suc d * ?l)) ^ 2"
using nlength_pow by simp
also have "... = 38 + 33 * ((Suc d * ?l)^2 + 2 * (Suc d * ?l) * 1 + 1^2)"
by (metis Suc_eq_plus1 add_Suc one_power2 power2_sum)
also have "... = 38 + 33 * ((Suc d * ?l)^2 + 2 * (Suc d * ?l) + 1)"
by simp
also have "... \<le> 38 + 33 * ((Suc d * ?l)^2 + 2 * (Suc d * ?l)^2 + 1)"
proof -
have "(Suc d * ?l) \<le> (Suc d * ?l) ^ 2"
by (simp add: le_square power2_eq_square)
then show ?thesis
by simp
qed
also have "... \<le> 38 + 33 * (3 * (Suc d * ?l)^2 + 1)"
by simp
also have "... = 38 + 33 * (3 * (Suc d) ^ 2 * ?l^2 + 1)"
by algebra
also have "... = 71 + 99 * (Suc d) ^ 2 * ?l ^ 2"
by simp
finally show ?thesis .
qed
ultimately show ?thesis
using transforms_monotone assms(14) by blast
qed
lemma tm4:
fixes d :: nat
assumes "tps' = tps0 [j3 := (\<lfloor>x ^ d\<rfloor>\<^sub>N, 1)]"
and "ttt = 12 + 71 * d + 99 * d ^ 3 * (nlength x) ^ 2"
shows "transforms (tm4 d) tps0 ttt tps'"
using assms
proof (induction d arbitrary: tps' ttt)
case 0
have "tm4 0 = tm_setn j3 1"
by simp
let ?tps = "tps0 [j3 := (\<lfloor>1\<rfloor>\<^sub>N, 1)]"
let ?t = "10 + 2 * nlength 1"
have "transforms (tm_setn j3 1) tps0 ?t ?tps"
using transforms_tm_setnI[of j3 tps0 0 ?t 1 ?tps] jk tps0 by simp
then have "transforms (tm_setn j3 1) tps0 ?t tps'"
using 0 by simp
then show ?case
using 0 nlength_1_simp by simp
next
case (Suc d)
note Suc.IH [transforms_intros]
let ?l = "nlength x"
have "tm4 (Suc d) = tm4 d ;; tm3"
by simp
define t where "t = 12 + 71 * d + 99 * d ^ 3 * (nlength x)\<^sup>2 + (71 + 99 * (Suc d)\<^sup>2 * (nlength x)\<^sup>2)"
have "transforms (tm4 d ;; tm3) tps0 t tps'"
by (tform tps: jk tps0 Suc.prems(1) time: t_def)
moreover have "t \<le> 12 + 71 * Suc d + 99 * Suc d ^ 3 * ?l\<^sup>2"
proof -
have "t = 12 + d * 71 + 99 * d ^ 3 * ?l\<^sup>2 + (71 + 99 * (Suc d)\<^sup>2 * ?l\<^sup>2)"
using t_def by simp
also have "... = 12 + Suc d * 71 + 99 * d ^ 3 * ?l\<^sup>2 + 99 * (Suc d)\<^sup>2 * ?l\<^sup>2"
by simp
also have "... = 12 + Suc d * 71 + 99 * ?l^2 * (d ^ 3 + (Suc d)\<^sup>2)"
by algebra
also have "... \<le> 12 + Suc d * 71 + 99 * ?l^2 * Suc d ^ 3"
proof -
have "Suc d ^ 3 = Suc d * Suc d ^ 2"
by algebra
also have "... = Suc d * (d ^ 2 + 2 * d + 1)"
by (metis (no_types, lifting) Suc_1 add.commute add_Suc mult_2 one_power2 plus_1_eq_Suc power2_sum)
also have "... = (d + 1) * (d ^ 2 + 2 * d + 1)"
by simp
also have "... = d ^ 3 + 2 * d ^ 2 + d + d ^ 2 + 2 * d + 1"
by algebra
also have "... = d ^ 3 + (d + 1) ^ 2 + 2 * d ^ 2 + d"
by algebra
also have "... \<ge> d ^ 3 + (d + 1) ^ 2"
by simp
finally have "Suc d ^ 3 \<ge> d ^ 3 + Suc d ^ 2"
by simp
then show ?thesis
by simp
qed
also have "... = 12 + 71 * Suc d + 99 * Suc d ^ 3 * ?l^2"
by simp
finally show ?thesis .
qed
ultimately show ?case
using transforms_monotone Suc by simp
qed
text \<open>
A monomial is a power multiplied by a constant coefficient. The following Turing
machines have parameters $c$ and $d$ and expect a number $x$ on tape $j$. They
output $c\cdot x^d$ on tape $j + 3$. The tapes $j+1$ and $j+2$ are
scratch space for use by @{const tm_pow} and @{const tm_mult}. \<close>
lemma tm_monomial_tm:
assumes "k \<ge> 2" and "G \<ge> 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 \<open>
A polynomial is a sum of monomials. In this section we construct for every
polynomial function $p$ a Turing machine that on input $x\in\nat$ outputs
$p(x)$.
According to our definition of polynomials (see Section~\ref{s:tm-basic-bigoh}),
we can represent each polynomial by a list of coefficients. The value of such a
polynomial with coefficient list @{term cs} on input $x$ is given by the next
function. In the following definition, the coefficients of the polynomial are in
reverse order, which simplifies the Turing machine later. \<close>
definition polyvalue :: "nat list \<Rightarrow> nat \<Rightarrow> nat" where "polyvalue cs x \<equiv> (\<Sum>i\<leftarrow>[0..<length cs]. rev cs ! i * x ^ i)"
lemma polyvalue_Nil: "polyvalue [] x = 0"
using polyvalue_def by simp
lemma sum_upt_snoc: "(\<Sum>i\<leftarrow>[0..<length (zs @ [z])]. (zs @ [z]) ! i * x ^ i) =
(\<Sum>i\<leftarrow>[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 = (\<Sum>i\<leftarrow>[0..<Suc (length cs)]. (rev cs @ [c]) ! i * x ^ i)"
using polyvalue_def by simp
also have "... = (\<Sum>i\<leftarrow>[0..<length (rev cs @ [c])]. (rev cs @ [c]) ! i * x ^ i)"
by simp
also have "... = (\<Sum>i\<leftarrow>[0..<length (rev cs)]. (rev cs) ! i * x ^ i) + c * x ^ (length (rev cs))"
using sum_upt_snoc by blast
also have "... = (\<Sum>i\<leftarrow>[0..<length cs]. (rev cs) ! i * x ^ i) + c * x ^ (length cs)"
by simp
finally show ?thesis
using polyvalue_def by simp
qed
lemma polyvalue_Cons_ge: "polyvalue (c # cs) x \<ge> polyvalue cs x"
using polyvalue_Cons by simp
lemma polyvalue_Cons_ge2: "polyvalue (c # cs) x \<ge> c * x ^ (length cs)"
using polyvalue_Cons by simp
lemma sum_list_const: "(\<Sum>_\<leftarrow>ns. c) = c * length ns"
using sum_list_triv[of c ns] by simp
lemma polyvalue_le: "polyvalue cs x \<le> Max (set cs) * length cs * Suc x ^ length cs"
proof -
define cmax where "cmax = Max (set (rev cs))"
have "polyvalue cs x = (\<Sum>i\<leftarrow>[0..<length cs]. rev cs ! i * x ^ i)"
using polyvalue_def by simp
also have "... \<le> (\<Sum>i\<leftarrow>[0..<length cs]. cmax * x ^ i)"
proof -
have "rev cs ! i \<le> cmax" if "i < length cs" for i
using that cmax_def by (metis List.finite_set Max_ge length_rev nth_mem)
then show ?thesis
by (metis (no_types, lifting) atLeastLessThan_iff mult_le_mono1 set_upt sum_list_mono)
qed
also have "... = cmax * (\<Sum>i\<leftarrow>[0..<length cs]. x ^ i)"
using sum_list_const_mult by blast
also have "... \<le> cmax * (\<Sum>i\<leftarrow>[0..<length cs]. Suc x ^ i)"
by (simp add: power_mono sum_list_mono)
also have "... \<le> cmax * (\<Sum>i\<leftarrow>[0..<length cs]. Suc x ^ length cs)"
proof -
have "Suc x ^ i \<le> Suc x ^ length cs" if "i < length cs" for i
using that by (simp add: dual_order.strict_implies_order pow_mono)
then show ?thesis
by (metis atLeastLessThan_iff mult_le_mono2 set_upt sum_list_mono)
qed
also have "... = cmax * length cs * Suc x ^ length cs"
using sum_list_const[of _ "[0..<length cs]"] by simp
finally have "polyvalue cs x \<le> cmax * length cs * Suc x ^ length cs" .
moreover have "cmax = Max (set cs)"
using cmax_def by simp
ultimately show ?thesis
by simp
qed
lemma nlength_polyvalue: "nlength (polyvalue cs x) \<le> nlength (Max (set cs)) + nlength (length cs) + Suc (length cs * nlength (Suc x))"
proof -
have "nlength (polyvalue cs x) \<le> nlength (Max (set cs) * length cs * Suc x ^ length cs)"
using polyvalue_le nlength_mono by simp
also have "... \<le> nlength (Max (set cs) * length cs) + nlength (Suc x ^ length cs)"
using nlength_prod by simp
also have "... \<le> nlength (Max (set cs)) + nlength(length cs) + Suc (length cs * nlength (Suc x))"
by (meson add_mono nlength_pow nlength_prod)
finally show ?thesis .
qed
text \<open>
The following Turing machines compute polynomials given as lists of
coefficients. 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
tape $j + 4$. The tapes $j+1$, $j+2$, and $j + 3$ are auxiliary tapes for use by
@{const tm_monomial}. \<close>
lemma tm_polycoef_tm:
assumes "k \<ge> 2" and "G \<ge> 4" and "j + 4 < k" and "0 < j"
shows "turing_machine k G (tm_polycoef cs j)"
proof (induction cs)
case Nil
then show ?case
by (simp add: assms(1) assms(2) turing_machine_def)
next
case (Cons c cs)
moreover have "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
ultimately show ?case
by simp
qed
locale turing_machine_polycoef =
fixes j :: tapeidx
begin
definition "tm1 c cs \<equiv> tm_monomial c (length cs) j"
definition "tm2 c cs \<equiv> tm1 c cs ;; tm_add (j + 3) (j + 4)"
definition "tm3 c cs \<equiv> tm2 c cs ;; tm_setn (j + 3) 0"
fun tm4 :: "nat list \<Rightarrow> 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
then show ?case
by simp
next
case (Cons z zs)
then show ?case
by (simp add: tm1_def tm2_def tm3_def)
qed
lemma pow_le_pow_Suc:
fixes a b :: nat
shows "a ^ b \<le> Suc a ^ Suc b"
proof -
have "a ^ b \<le> Suc a ^ b"
by (simp add: power_mono)
then show ?thesis
by simp
qed
have tm4def: "tm4 (c # cs) = tm4 cs ;; tm3 c cs"
by simp
let ?t1 = "d cs *
(66 + 71 * d cs + 99 * d cs ^ 3 * (nlength x)\<^sup>2 + 32 * (Max (nlength ` set cs) + nlength (Suc x ^ d cs))\<^sup>2 + 5 * nlength (polyvalue cs x))"
let ?t2 = "66 + 71 * d cs + 99 * d cs ^ 3 * (nlength x)\<^sup>2 + 32 * (nlength c + nlength (x ^ d cs))\<^sup>2 + 5 * max (nlength (c * x ^ d cs)) (nlength (polyvalue cs x))"
define t where "t = ?t1 + ?t2"
have tm4: "transforms (tm4 (c # cs)) tps0 t (tps0[j + 4 := (\<lfloor>polyvalue (c # cs) x\<rfloor>\<^sub>N, 1)])"
unfolding tm4def by (tform tps: assms t_def)
have "?t1 \<le> d cs *
(66 + 71 * d (c#cs) + 99 * d cs ^ 3 * (nlength x)\<^sup>2 + 32 * (Max (nlength ` set cs) + nlength (Suc x ^d cs))\<^sup>2 + 5 * nlength (polyvalue cs x))"
by simp
also have "... \<le> d cs *
(66 + 71 * d (c#cs) + 99 * d (c#cs) ^ 3 * (nlength x)\<^sup>2 + 32 * (Max (nlength ` set cs) + nlength (Suc x ^d cs))\<^sup>2 + 5 * nlength (polyvalue cs x))"
by simp
also have "... \<le> d cs *
(66 + 71 * d (c#cs) + 99 * d (c#cs) ^ 3 * (nlength x)\<^sup>2 + 32 * (Max (nlength ` set (c#cs)) + nlength (Suc x ^d cs))\<^sup>2 + 5 * nlength (polyvalue cs x))"
by simp
also have "... \<le> d cs *
(66 + 71 * d (c#cs) + 99 * d (c#cs) ^ 3 * (nlength x)\<^sup>2 + 32 * (Max (nlength ` set (c#cs)) + nlength (Suc x ^d (c#cs)))\<^sup>2 + 5 * nlength (polyvalue cs x))"
using nlength_mono by simp
also have "... \<le> d cs *
(66 + 71 * d (c#cs) + 99 * d (c#cs) ^ 3 * (nlength x)\<^sup>2 + 32 * (Max (nlength ` set (c#cs)) + nlength (Suc x ^d (c#cs)))\<^sup>2 + 5 * nlength (polyvalue (c#cs) x))"
using nlength_mono polyvalue_Cons_ge by simp
finally have t1: "?t1 \<le> d cs *
(66 + 71 * d (c#cs) + 99 * d (c#cs) ^ 3 * (nlength x)\<^sup>2 + 32 * (Max (nlength ` set (c#cs)) + nlength (Suc x ^d (c#cs)))\<^sup>2 + 5 * nlength (polyvalue (c#cs) x))"
(is "?t1 \<le> d cs * ?t3") .
have "?t2 \<le> 66 + 71 * d (c # cs) + 99 * d cs ^ 3 * (nlength x)\<^sup>2 + 32 * (nlength c + nlength (x ^ d cs))\<^sup>2 + 5 * max (nlength (c * x ^ d cs)) (nlength (polyvalue cs x))"
by simp
also have "... \<le> 66 + 71 * d (c # cs) + 99 * d (c # cs) ^ 3 * (nlength x)\<^sup>2 + 32 * (nlength c + nlength (x ^ d cs))\<^sup>2 + 5 * max (nlength (c * x ^ d cs)) (nlength (polyvalue cs x))"
by simp
also have "... \<le> 66 + 71 * d (c # cs) + 99 * d (c # cs) ^ 3 * (nlength x)\<^sup>2 + 32 * (Max (set (map nlength (c # cs))) + nlength (x ^ d cs))\<^sup>2 + 5 * max (nlength (c * x ^ d cs)) (nlength (polyvalue cs x))"
by simp
also have "... \<le> 66 + 71 * d (c # cs) + 99 * d (c # cs) ^ 3 * (nlength x)\<^sup>2 + 32 * (Max (set (map nlength (c # cs))) + nlength (Suc x ^ d (c#cs)))\<^sup>2 + 5 * max (nlength (c * x ^ d cs)) (nlength (polyvalue cs x))"
using nlength_mono pow_le_pow_Suc by simp
also have "... \<le> 66 + 71 * d (c # cs) + 99 * d (c # cs) ^ 3 * (nlength x)\<^sup>2 + 32 * (Max (set (map nlength (c # cs))) + nlength (Suc x ^ d (c#cs)))\<^sup>2 + 5 * max (nlength (c * x ^ d cs)) (nlength (polyvalue (c#cs) x))"
proof -
have "nlength (polyvalue cs x) \<le> nlength (polyvalue (c#cs) x)"
using polyvalue_Cons by (simp add: nlength_mono)
then show ?thesis
by simp
qed
also have "... \<le> 66 + 71 * d (c # cs) + 99 * d (c # cs) ^ 3 * (nlength x)\<^sup>2 + 32 * (Max (set (map nlength (c # cs))) + nlength (Suc x ^ d (c#cs)))\<^sup>2 + 5 * max (nlength (polyvalue (c#cs) x)) (nlength (polyvalue (c#cs) x))"
using nlength_mono polyvalue_Cons_ge2 by simp
also have "... \<le> 66 + 71 * d (c # cs) + 99 * d (c # cs) ^ 3 * (nlength x)\<^sup>2 + 32 * (Max (set (map nlength (c # cs))) + nlength (Suc x ^ d (c#cs)))\<^sup>2 + 5 * nlength (polyvalue (c#cs) x)"
by simp
finally have t2: "?t2 \<le> ?t3"
by simp
have "t \<le> d cs * ?t3 + ?t3"
using t1 t2 t_def add_le_mono by blast
then have "t \<le> d (c#cs) * ?t3"
by simp
moreover have "ttt = d (c#cs) * ?t3"
using Cons by simp
ultimately have "t \<le> ttt"
by simp
then show ?case
using tm4 transforms_monotone by simp
qed
end (* locale turing_machine_polycoef *)
text \<open>
The time bound in the previous lemma for @{const tm_polycoef} is a bit unwieldy.
It depends not only on the length of the input $x$ but also on the list of
coefficients of the polynomial $p$ and on the value $p(x)$. Next we bound this
time bound by a simpler expression of the form $d + d\cdot|x|^2$ where $d$
depends only on the polynomial. This is accomplished by the next three lemmas. \<close>
lemma tm_polycoef_time_1: "\<exists>d. \<forall>x. nlength (polyvalue cs x) \<le> d + d * nlength x"
proof -
{ fix x
have "nlength (polyvalue cs x) \<le> nlength (Max (set cs)) + nlength (length cs) + Suc (length cs * nlength (Suc x))"
using nlength_polyvalue by simp
also have "... = nlength (Max (set cs)) + nlength (length cs) + 1 + length cs * nlength (Suc x)"
(is "_ = ?a + length cs * nlength (Suc x)")
by simp
also have "... \<le> ?a + length cs * (Suc (nlength x))"
using nlength_Suc by (meson add_mono_thms_linordered_semiring(2) mult_le_mono2)
also have "... = ?a + length cs + length cs * nlength x"
(is "_ = ?b + length cs * nlength x")
by simp
also have "... \<le> ?b + ?b * nlength x"
by (meson add_left_mono le_add2 mult_le_mono1)
finally have "nlength (polyvalue cs x) \<le> ?b + ?b * nlength x" .
}
then show ?thesis
by blast
qed
lemma tm_polycoef_time_2: "\<exists>d. \<forall>x. (Max (set (map nlength cs)) + nlength (Suc x ^ length cs))\<^sup>2 \<le> d + d * nlength x ^ 2"
proof -
{ fix x
have "(Max (set (map nlength cs)) + nlength (Suc x ^ length cs))\<^sup>2 \<le>
(Max (set (map nlength cs)) + Suc (nlength (Suc x) * length cs))\<^sup>2"
using nlength_pow by (simp add: mult.commute)
also have "... = (Suc (Max (set (map nlength cs))) + nlength (Suc x) * length cs)\<^sup>2"
(is "_ = (?a + ?b)^2")
by simp
also have "... = ?a ^ 2 + 2 * ?a * ?b + ?b ^ 2"
by algebra
also have "... \<le> ?a ^ 2 + 2 * ?a * ?b ^ 2 + ?b ^ 2"
by (meson add_le_mono dual_order.eq_iff mult_le_mono2 power2_nat_le_imp_le)
also have "... \<le> ?a ^ 2 + (2 * ?a + 1) * ?b ^ 2"
by simp
also have "... = ?a ^ 2 + (2 * ?a + 1) * (length cs) ^ 2 * nlength (Suc x) ^ 2"
by algebra
also have "... \<le> ?a ^ 2 + (2 * ?a + 1) * (length cs) ^ 2 * Suc (nlength x) ^ 2"
using nlength_Suc by simp
also have "... = ?a ^ 2 + (2 * ?a + 1) * (length cs) ^ 2 * (nlength x ^ 2 + 2 * nlength x + 1)"
by (smt (verit) Suc_eq_plus1 add.assoc mult_2 nat_1_add_1 one_power2 plus_1_eq_Suc power2_sum)
also have "... \<le> ?a ^ 2 + (2 * ?a + 1) * (length cs) ^ 2 * (nlength x ^ 2 + 2 * nlength x ^ 2 + 1)"
proof -
have "nlength x ^ 2 + 2 * nlength x + 1 \<le> nlength x ^ 2 + 2 * nlength x ^ 2 + 1"
by (metis add_le_mono1 add_mono_thms_linordered_semiring(2) le_square mult.commute
mult_le_mono1 numerals(1) power_add_numeral power_one_right semiring_norm(2))
then show ?thesis
by simp
qed
also have "... = ?a ^ 2 + (2 * ?a + 1) * (length cs) ^ 2 * (3 * nlength x ^ 2 + 1)"
by simp
also have "... = ?a ^ 2 + (2 * ?a + 1) * (length cs) ^ 2 + (2 * ?a + 1) * (length cs) ^ 2 * 3 * nlength x ^ 2"
(is "_ = _ + ?c * nlength x ^ 2")
by simp
also have "... \<le> ?a ^ 2 + ?c + ?c * nlength x ^ 2"
(is "_ \<le> ?d + ?c * nlength x ^ 2")
by simp
also have "... \<le> ?d + ?d * nlength x ^ 2"
by simp
finally have "(Max (set (map nlength cs)) + nlength (Suc x ^ length cs))\<^sup>2 \<le> ?d + ?d * nlength x ^ 2" .
}
then show ?thesis
by auto
qed
lemma tm_polycoef_time_3: "\<exists>d. \<forall>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" proof - obtain d1 where d1: "∀x. nlength (polyvalue cs x) ≤ d1 + d1 * nlength x" using tm_polycoef_time_1 by auto obtain d2 where d2: "∀x. (Max (set (map nlength cs)) + nlength (Suc x ^ length cs))2≤ d2 + d2 * nlength x ^ 2" using tm_polycoef_time_2 by auto { fix x let ?lhs = " 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))" let ?n = "nlength x" have "?lhs ≤ length cs *
(66 + 71 * length cs + 99 * length cs ^ 3 * ?n ^ 2 + 32 * (d2 + d2 * ?n ^ 2) + 5 * (d1 + d1 * ?n))" using d1 d2 add_le_mono mult_le_mono2 nat_add_left_cancel_le by presburger also have "... ≤ length cs *
(66 + 71 * length cs + 99 * length cs ^ 3 * ?n ^ 2 + 32 * (d2 + d2 * ?n ^ 2) + 5 * (d1 + d1 * ?n ^ 2))" by (simp add: le_square power2_eq_square) also have "... = length cs *
(66 + 71 * length cs + 99 * length cs ^ 3 * ?n ^ 2 + 32 * d2 + 32 * d2 * ?n ^ 2 + 5 * d1 + 5 * d1 * ?n ^ 2)" by simp also have "... = length cs *
(66 + 71 * length cs + 32 * d2 + 5 * d1 +
(99 * length cs ^ 3 + 32 * d2 + 5 * d1) * ?n ^ 2)" by algebra also have "... = length cs * (66 + 71 * length cs + 32 * d2 + 5 * d1) +
length cs * (99 * length cs ^ 3 + 32 * d2 + 5 * d1) * ?n ^ 2" (is "_ = ?a + ?b * ?n ^ 2") by algebra also have "... ≤ max ?a ?b + max ?a ?b * ?n ^ 2" by (simp add: add_mono_thms_linordered_semiring(1)) finally have "?lhs ≤ max ?a ?b + max ?a ?b * ?n ^ 2" . } then show ?thesis by auto qed
text ‹ According to our definition of @{const polynomial} (see Section~\ref{s:tm-basic-bigoh}) every polynomial has a list of coefficients. Therefore the next definition is well-defined for polynomials $p$. \<close>
definition coefficients :: " nat ==> nat) ==> nat list" where
"coefficients p ≡ SOME cs. ∀n. p n = (∑i←[0..<length cs]. cs ! i * n ^ i)"
‹
$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
: ›
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)"
‹
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. ›
tm_polynomial :: "(nat ==> nat) ==> tapeidx ==> machine" where
"tm_polynomial p j ≡ tm_polycoef (rev (coefficients p)) j"
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
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'"
-
let ?P = "λx. ∀n. p n = (∑i←[0..<length x]. x ! i * n ^ i)"
define cs where "cs = (SOME x. ?P x)"
moreover have ex: "∃cs. ?P cs"
using assms(4) polynomial_def by simp
ultimately have "?P cs"
using someI_ex[of ?P] by blast
then have 1: "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
then have *: "∀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
then have "transforms (loc.tm4 ?cs) tps ?ttt (tps[j + 4 := (⌊p x⌋N, 1)])"
using 1 by simp
then have "transforms (loc.tm4 ?cs) tps ?ttt tps'"
using assms(11) by simp
moreover have "loc.tm4 ?cs = tm_polynomial p j"
using tm_polynomial_def loc.tm4_eq_tm_polycoef coefficients_def cs_def by simp
ultimately have "transforms (tm_polynomial p j) tps ?ttt tps'"
by simp
then show "transforms (tm_polynomial p j) tps ttt tps'"
using * assms(10) transforms_monotone by simp
‹Division by two›
‹
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. ›
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]))"
turing_command_halve:
assumes "G ≥ 4" and "0 < j" and "j < k"
shows "turing_command (Suc k) 1 G (cmd_halve j)"
show "∧gs. length gs = Suc k ==> length ([!!] cmd_halve j gs) = length gs"
using cmd_halve_def by simp
moreover have "0 ≠ Suc k - 1"
using assms by simp
ultimately show "∧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
ultimately show ?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
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')"
(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"
then have 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)
then have rsj': "rs ! j > 1"
using assms Suc_1 Suc_diff_1 Suc_le_lessD by (metis eval_nat_numeral(3) less_Suc_eq)
then show "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" for j'
proof -
have "j' < length rs"
using that lenrs by simp
then have *: "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
then show ?thesis
proof (cases)
case 1
then have "cmd_halve j (read tps) [!] j' = (tosym (todigit (last rs)), Left)"
using rs_def rsj' lastrs * assms(6) by auto
then have "cmd_halve j (read tps) [!] j' = (z, Left)"
using lastrs assms(6) by auto
moreover have "tps' ! j' = tps ! j |:=| z |-| 1"
using 1 assms(1,3,9) by simp
ultimately show ?thesis
using act_Left' 1 that rs_def by metis
next
case 2
then have "cmd_halve j (read tps) [!] j' = (tosym (todigit (rs ! j)), Stay)"
using rs_def * lenrs assms(1) by simp
moreover have "tps' ! j' = ⌈xs ! (i - 1)⌉"
using assms 2 by simp
moreover have "tps ! j' = ⌈z⌉"
using assms 2 by simp
moreover have "tosym (todigit (rs ! j)) = xs ! (i - 1)"
proof -
have "xs ! (i - 1) = 0∨ xs ! (i - 1) = 1"
using rsj rs_def assms by simp
then show ?thesis
using One_nat_def add_2_eq_Suc' numeral_3_eq_3 rsj by presburger
qed
ultimately show ?thesis
using act_onesie by simp
next
case 3
then show ?thesis
using * act_Stay that assms lenrs rs_def by simp
qed
qed
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')"
(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"
then have 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)
then have 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)
then show "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" for j'
proof -
have "j' < length rs"
using that lenrs by simp
then have *: "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
then show ?thesis
proof (cases)
case 1
then have "cmd_halve j (read tps) [!] j' = (◻, Left)"
using rs_def rsj' lastrs * by simp
then show ?thesis
using act_Left' 1 that rs_def assms(1,3,7) by simp
next
case 2
then have "cmd_halve j (read tps) [!] j' = (tosym (todigit (rs ! j)), Stay)"
using rs_def * lenrs assms(1) by simp
moreover have "tps' ! j' = ⌈xs ! (length xs - 1)⌉"
using assms 2 by simp
moreover have "tps ! j' = ⌈▹⌉"
using assms 2 by simp
ultimately show ?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
case 3
then show ?thesis
using * act_Stay that assms lenrs rs_def by simp
qed
qed
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')"
(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" for j'
proof -
define gs where "gs = read tps"
then have "length gs = Suc k"
using assms by (simp add: read_length)
then have "j' < length gs"
using that by simp
then 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 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
then show ?thesis
proof (cases)
case 1
then have "cmd_halve j (read tps) [!] j' = (gs ! j', Right)"
using gs_def gsj * by simp
then show ?thesis
using act_Right assms 1 that gs_def by (metis length_list_update lessI nat_neq_iff nth_list_update)
next
case 2
then have "cmd_halve j (read tps) [!] j' = (tosym (todigit (gs ! j)), Stay)"
using gs_def * ‹length gs = Suc k› assms(1) by simp
moreover have "tps' ! j' = ⌈0⌉"
using assms 2 by simp
moreover have "tps ! j' = ⌈z⌉"
using assms 2 by simp
ultimately show ?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
case 3
then show ?thesis
using * act_Stay that assms(2,5) ‹length gs = Suc k› gs_def by simp
qed
qed
tm_halve_tm:
assumes "k ≥ 2" and "G ≥ 4" and "0 < j" and "j < k"
shows "turing_machine (Suc k) G (tm_halve j)"
using tm_halve_def turing_command_halve assms by auto
exe_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 "exe (tm_halve j) (0, tps) = (1, tps')"
using assms sem_cmd_halve_0 tm_halve_def exe_lt_length by simp
execute_cmd_halve_0:
assumes "j < k"
and "length tps = Suc k"
and "tps ! j = (⌊[]⌋, 0)"
and "tps ! k = ⌈▹⌉"
and "tps' = tps[j := tps ! j |+| 1, k := ⌈0⌉]"
shows "execute (tm_halve j) (0, tps) 1 = (1, tps')"
using tm_halve_def exe_lt_length sem_cmd_halve_0 assms by simp
shift :: "tape ==> nat ==> tape" where
"shift tp y ≡ (λx. if x ≤ y then (fst tp) x else (fst tp) (Suc x), y)"
shift_update: "y > 0 ==> shift tp y |:=| (fst tp) (Suc y) |-| 1 = shift tp (y - 1)"
unfolding shift_def by fastforce
shift_contents_0:
assumes "length xs > 0"
shows "shift (⌊xs⌋, length xs) 0 = (⌊tl xs⌋, 0)"
-
have "shift (⌊xs⌋, length xs) 0 = (⌊drop 1 xs⌋, 0)"
using shift_def contents_def by fastforce
then show ?thesis
by (simp add: drop_Suc)
proper_bit_symbols: "bit_symbols ws ==> proper_symbols ws"
by auto
bit_symbols_shift:
assumes "t < length ws" and "bit_symbols ws"
shows "|.| (shift (⌊ws⌋, length ws) (length ws - t)) ≠ 1"
using assms shift_def contents_def nat_neq_iff proper_bit_symbols by simp
exe_cmd_halve_1:
assumes "j < k"
and "length tps = Suc k"
and "bit_symbols xs"
and "length xs > 0"
and "tps ! j = (⌊xs⌋, length xs)"
and "tps ! k = ⌈▹⌉"
and "tps' = tps[j := tps ! j |:=| ◻ |-| 1, k := ⌈xs ! (length xs - 1)⌉]"
shows "exe (tm_halve j) (0, tps) = (0, tps')"
using tm_halve_def exe_lt_length sem_cmd_halve_1 assms by simp
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)"
-
have "shift (⌊xs⌋, length xs) i = (λx. if x ≤ i then ⌊xs⌋ x else ⌊xs⌋ (Suc x), i)"
using shift_def by auto
moreover have "(λ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
then show "?l x = ?r x"
proof (cases)
case 1
then show ?thesis
using assms contents_def by simp
next
case 2
then have "?l x = ⌊xs⌋ x"
by simp
then have lhs: "?l x = xs ! (x - 1)"
using assms 2 by simp
have "?r x = (take i xs @ drop (Suc i) xs) ! (x - 1)"
using assms 2 by auto
then have "?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)
then show ?thesis
using lhs by simp
next
case 3
then have "?l x = ⌊xs⌋ (Suc x)"
by simp
then have lhs: "?l x = xs ! x"
using 3 assms by auto
have "?r x = (take i xs @ drop (Suc i) xs) ! (x - 1)"
using assms 3 by auto
then have "?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)
then have "?r x = xs ! x"
using assms 3 by simp
then show ?thesis
using lhs by simp
next
case 4
then show ?thesis
using contents_def by auto
qed
qed
ultimately show ?thesis
using assms(2) by simp
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
bounded_write_tm_halve:
assumes "j < k"
shows "bounded_write (tm_halve j) k 4"
unfolding bounded_write_def
standard+
fix q :: nat and rs :: "symbol list"
assume q: "q < length (tm_halve j)" and lenrs: "length rs = Suc k"
have "k < length rs"
using lenrs by simp
then have "cmd_halve j rs [!] k =
(if k = j then
if rs ! j = ▹ then (rs ! k, Right)
else if last rs = ▹ then (◻, Left)
else (tosym (todigit (last rs)), Left)
else if k = length rs - 1 then (tosym (todigit (rs ! j)), Stay)
else (rs ! k, Stay))"
using cmd_halve_def by simp
then have "cmd_halve j rs [!] k = (tosym (todigit (rs ! j)), Stay)"
using assms lenrs by simp
then have "cmd_halve j rs [.] k = tosym (todigit (rs ! j))"
by simp
moreover have "(tm_halve j ! q) rs [.] k = cmd_halve j rs [.] k"
using tm_halve_def q by simp
ultimately show "(tm_halve j ! q) rs [.] k < 4"
by simp
immobile_tm_halve:
assumes "j < k"
shows "immobile (tm_halve j) k (Suc k)"
standard+
fix q :: nat and rs :: "symbol list"
assume q: "q < length (tm_halve j)" and lenrs: "length rs = Suc k"
have "k < length rs"
using lenrs by simp
then have "cmd_halve j rs [!] k =
(if k = j then
if rs ! j = ▹ then (rs ! k, Right)
else if last rs = ▹ then (◻, Left)
else (tosym (todigit (last rs)), Left)
else if k = length rs - 1 then (tosym (todigit (rs ! j)), Stay)
else (rs ! k, Stay))"
using cmd_halve_def by simp
then have "cmd_halve j rs [!] k = (tosym (todigit (rs ! j)), Stay)"
using assms lenrs by simp
then have "cmd_halve j rs [~] k = Stay"
by simp
moreover have "(tm_halve j ! q) rs [~] k = cmd_halve j rs [~] k"
using tm_halve_def q by simp
ultimately show "(tm_halve j ! q) rs [~] k = Stay"
by simp
tm_halve'_tm:
assumes "G ≥ 4" and "0 < j" and "j < k"
shows "turing_machine k G (tm_halve' j)"
using tm_halve'_def tm_halve_tm assms cartesian_tm by simp
transforms_tm_halve' [transforms_intros]:
assumes "j > 0" and "j < k"
and "length tps = k"
and "bit_symbols xs"
and "tps ! j = (⌊xs⌋, length xs)"
and "tps' = tps[j := (⌊tl xs⌋, 1)]"
shows "transforms (tm_halve' j) tps (Suc (length xs)) tps'"
unfolding tm_halve'_def
(rule cartesian_transforms_onesie[OF tm_halve_tm immobile_tm_halve _ _ bounded_write_tm_halve assms(3), where ?G=4];
(simp add: assms)?)
show "2 ≤ k" and "2 ≤ k"
using assms(1,2) by simp_all
show "transforms (tm_halve j) (tps @ [⌈Suc 0⌉]) (Suc (length xs))
(tps[j := (⌊tl xs⌋, Suc 0)] @ [⌈0⌉])"
using transforms_tm_halve2 assms by simp
num_tl_div_2: "num (tl xs) = num xs div 2"
(cases "xs = []")
case True
then show ?thesis
by (simp add: num_def)
case False
then have *: "xs = hd xs # tl xs"
by simp
then have "num xs = todigit (hd xs) + 2 * num (tl xs)"
using num_Cons by metis
then show ?thesis
by simp
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))
nlength_times2: "nlength (2 * n) ≤ Suc (nlength n)"
using canrepr_div_2[of "2 * n"] by simp
nlength_times2plus1: "nlength (2 * n + 1) ≤ Suc (nlength n)"
using canrepr_div_2[of "2 * n + 1"] by simp
‹
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'}. ›
tm_div2_tm:
assumes "G ≥ 4" and "0 < j" and "j < k"
shows "turing_machine k G (tm_div2 j)"
unfolding tm_div2_def using tm_right_until_tm tm_left_tm tm_halve'_tm assms by simp
tm3:
assumes "ttt = 2 * nlength n + 3"
shows "transforms tm3 tps0 ttt tps3"
unfolding tm3_def
(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
(* locale turing_machine_div2 *)
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'"
-
interpret loc: turing_machine_div2 j .
show ?thesis
using loc.tm3_eq_tm_div2 loc.tm3 loc.tps3_def assms by simp
‹Modulo two›
‹
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. ›
canrepr_odd: "odd n ==> canrepr n ! 0 = 1"
-
assume "odd n"
then have "0 < n"
by presburger
then have len: "length (canrepr n) > 0"
using nlength_0 by simp
then have "canrepr n ! 0 = 0∨ canrepr n ! 0 = 1"
using bit_symbols_canrepr by fastforce
then show "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)
canrepr_even: "even n ==> 0 < n ==> canrepr n ! 0 = 0"
-
assume "even n" "0 < n"
then have len: "length (canrepr n) > 0"
using nlength_0 by simp
then have "canrepr n ! 0 = 0∨ canrepr n ! 0 = 1"
using bit_symbols_canrepr by fastforce
then show "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)
"tm_mod2 j1 j2 ≡ tm_trans2 j1 j2 (λz. if z = 1 then 1 else ◻)"
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
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'"
-
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)
moreover have "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)
moreover have "tps :.: j1 = ◻" if "n = 0"
using that canrepr_even assms(5) contents_def
by simp
ultimately have "tps :.: j1 = 1⟷ odd n"
by linarith
then have 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
then have "tps ! j2 |:=| (?f (tps :.: j1)) = ((⌊b⌋N)(1 := 0), 1)"
using f tps_j2 by auto
also have "... = (⌊[]⌋, 1)"
proof (cases "b = 0")
case True
then have "⌊b⌋N = ⌊[]⌋"
using canrepr_0 by simp
then show ?thesis
by auto
next
case False
then have "⌊b⌋N = ⌊[1]⌋"
using canrepr_1 assms(4) by (metis One_nat_def bot_nat_0.extremum_uniqueI le_Suc_eq)
then show ?thesis
by (metis One_nat_def append.simps(1) append_Nil2 contents_append_update contents_blank_0 list.size(3))
qed
also have "... = (⌊0⌋N, 1)"
using canrepr_0 by simp
finally show ?thesis
using True by auto
next
case False
then have "tps ! j2 |:=| (?f (tps :.: j1)) = ((⌊b⌋N)(1 := 1), 1)"
using f tps_j2 by auto
also have "... = (⌊[1]⌋, 1)"
proof (cases "b = 0")
case True
then have "⌊b⌋N = ⌊[]⌋"
using canrepr_0 by simp
then show ?thesis
by (metis One_nat_def append.simps(1) contents_snoc list.size(3))
next
case False
then have "⌊b⌋N = ⌊[1]⌋"
using canrepr_1 assms(4) by (metis One_nat_def bot_nat_0.extremum_uniqueI le_Suc_eq)
then show ?thesis
by auto
qed
also have "... = (⌊1⌋N, 1)"
using canrepr_1 by simp
also have "... = (⌊n mod 2⌋N, 1)"
using False by (simp add: mod2_eq_if)
finally show ?thesis
by auto
qed
then show ?thesis
using * assms(7) by auto
‹Boolean operations›
‹
order to support Boolean operations, we represent the value True by the
~1 and False by~0. ›
bcontents :: "bool ==> (nat ==> symbol)" (‹⌊_⌋B›) where
"⌊b⌋B≡⌊if b then 1 else 0⌋N"
‹
tape containing a number contains the number~0 iff.\ there is a blank in cell
~1. ›
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))
‹And›
‹
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. ›
tm_and_tm:
assumes "k ≥ 2" and "G ≥ 4" and "0 < j1" and "j1 < k"
shows "turing_machine k G (tm_and j1 j2)"
using tm_and_def tm_write_tm Nil_tm assms turing_machine_branch_turing_machine by simp
turing_machine_and =
fixes j1 j2 :: tapeidx
fixes tps0 :: "tape list" and k :: nat and a b :: nat
assumes ab: "a < 2" "b < 2"
assumes jk: "j1 < k" "j2 < k" "j1 ≠ j2" "0 < j1" "length tps0 = k"
assumes tps0:
"tps0 ! j1 = (⌊a⌋N, 1)"
"tps0 ! j2 = (⌊b⌋N, 1)"
"tps1 ≡ tps0
[j1 := (⌊a = 1 ∧ b = 1⌋B, 1)]"
tm: "transforms (tm_and j1 j2) tps0 3 tps1"
unfolding tm_and_def
(tform)
have "read tps0 ! j1 = ⌊canrepr a⌋ 1"
using jk tps0 tapes_at_read'[of j1 tps0] by simp
then have 1: "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
then have 2: "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 1 2 ab jk by (metis One_nat_def less_2_cases_iff read_ncontents_eq_0 tps0(2))
then have "tps0 ! j1 = (⌊a = 1 ∧ b = 1⌋B, 1)"
using tps0 by simp
then show ?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 1 2 by simp
moreover have "tps0 ! j1 |:=| ◻ = (⌊0⌋N, 1)"
proof (cases "a = 0")
case True
then show ?thesis
using tps0 jk by auto
next
case False
then have "a = 1"
using ab by simp
then have "⌊a⌋N = ⌊[1]⌋"
using canrepr_1 by simp
moreover have "(⌊[1]⌋, 1) |:=| ◻ = (⌊[]⌋, 1)"
using contents_def by auto
ultimately have "(⌊a⌋N, 1) |:=| ◻ = (⌊0⌋N, 1)"
using ncontents_0 by presburger
then show ?thesis
using tps0 jk by simp
qed
ultimately have "tps0 ! j1 |:=| ◻ = (⌊a = 1 ∧ b = 1⌋B, 1)"
by (smt (verit, best))
then show ?thesis
unfolding tps1_def by auto
qed
(* context *)
(* locale *)
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'"
-
interpret loc: turing_machine_and j1 j2 .
show ?thesis
using assms loc.tps1_def loc.tm by simp
‹Not›
‹
next Turing machine turns the number~1 into~0 and vice versa. ›
tm_not :: "tapeidx ==> machine" where
"tm_not j ≡ IF λrs. rs ! j = ◻ THEN tm_write j 1 ELSE tm_write j ◻ ENDIF"
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
turing_machine_not =
fixes j :: tapeidx
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)"
"tps1 ≡ tps0
[j := (⌊a ≠ 1⌋B, 1)]"
tm: "transforms (tm_not j) tps0 3 tps1"
unfolding tm_not_def
(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
then have "(⌊if a = 1 then 0 else 1⌋N, 1) = (⌊1⌋N, 1)"
by simp
moreover have "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)
ultimately have "tps0[j := tps0 ! j |:=| 1] = tps0[j := (⌊a ≠ 1⌋B, 1)]"
by auto
then show ?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
then have "(⌊if a = 1 then 0 else 1⌋N, 1) = (⌊0⌋N, 1)"
by simp
moreover have "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)
ultimately have "tps0[j := tps0 ! j |:=| ◻] = tps0[j := (⌊a ≠ 1⌋B, 1)]"
by auto
then show ?thesis
using tps1_def by simp
qed
(* context *)
(* locale *)
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'"
-
interpret loc: turing_machine_not j .
show ?thesis
using assms loc.tps1_def loc.tm by simp
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.450Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-06-10)
¤
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.