section ‹Arithmetic\label{s:tm-arithmetic}› theory Arithmetic imports Memorizing begin text ‹ In this section we define a representation of natural numbers and some reusable Turing machines for elementary arithmetical operations. All Turing machines implementing the operations assume that the tape heads on the tapes containing the operands and the result(s) contain one natural number each. In programming language 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, one to the right of the start symbol. The Turing machines will halt with the tape heads in that position as well. In that way operations can be concatenated seamlessly. › subsection ‹Binary numbers\label{s:tm-arithmetic-binary}› text ‹ We represent binary numbers as sequences of the symbols \textbf{0} and \textbf{1}. Slightly unusually the least significant bit will be on the left. While every sequence over these symbols represents a natural number, the representation is not unique due to leading (or rather, trailing) zeros. The \emph{canonical} representation is unique and has no trailing zeros, not even for the number zero, which is thus represented by the empty symbol sequence. As a side effect empty tapes can be thought of as being initialized with zero. Naturally the binary digits 0 and 1 are represented by the symbols \textbf{0} and \textbf{1}, respectively. For example, the decimal number $14$, conventionally 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 = 𝟭 then 1 else 0" text ‹ The numerical value of a symbol sequence: › definition num :: "symbol list ⇒ nat" where "num xs ≡ ∑i←[0..<length xs]. todigit (xs ! i) * 2 ^ i" text ‹ The $i$-th digit of a symbol sequence, where digits out of bounds are considered trailing zeros: › definition digit :: "symbol list ⇒ nat ⇒ nat" where "digit xs i ≡ if i < length xs then xs ! i else 0" text ‹ Some properties of $num$: › lemma num_ge_pow: assumes "i < length xs" and "xs ! i = 𝟭" 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 moreover have "i < length ?ys" using assms(1) by simp ultimately show "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 then have "num ?xs = sum_list (map (λi. todigit (xs ! i) * 2 ^ i) [0..<length xs] @ [0])" using * by metis then have "num ?xs = sum_list (map (λi. todigit (xs ! i) * 2 ^ i) [0..<length xs])" by simp then show ?thesis using num_def by simp qed lemma num_Cons: "num (x # xs) = todigit x + 2 * num xs" proof - have "[0..<length (x # xs)] = [0..<1] @ [1..<length (x # xs)]" by (metis length_Cons less_imp_le_nat plus_1_eq_Suc upt_add_eq_append zero_less_one) then have 1: "(map (λi. todigit ((x # xs) ! i) * 2 ^ i) [0..<length (x # xs)]) = (map (λi. todigit ((x # xs) ! i) * 2 ^ i) [0..<1]) @ (map (λi. todigit ((x # xs) ! i) * 2 ^ i) [1..<length (x # xs)])" by simp 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 then show "⋀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 then have 2: "(∑i←[1..<Suc m]. f i) = (∑i←[0..<m]. f (Suc i))" for f :: "nat ⇒ nat" and m by simp have "num (x # xs) = (∑i←[0..<length (x # xs)]. todigit ((x # xs) ! i) * 2 ^ i)" using num_def by simp also have "... = (∑i←[0..<1]. (todigit ((x # xs) ! i) * 2 ^ i)) + (∑i←[1..<length (x # xs)]. todigit ((x # xs) ! i) * 2 ^ i)" using 1 by simp also have "... = todigit x + (∑i←[1..<length (x # xs)]. todigit ((x # xs) ! i) * 2 ^ i)" by simp also have "... = todigit x + (∑i←[0..<length (x # xs) - 1]. todigit ((x # xs) ! (Suc i)) * 2 ^ (Suc i))" using 2 by simp also have "... = todigit x + (∑i←[0..<length xs]. todigit (xs ! i) * 2 ^ (Suc i))" by simp also have "... = todigit x + (∑i←[0..<length xs]. todigit (xs ! i) * (2 * 2 ^ i))" by simp also have "... = todigit x + (∑i←[0..<length xs]. (todigit (xs ! i) * 2 * 2 ^ i))" by (simp add: mult.assoc) also have "... = todigit x + (∑i←[0..<length xs]. (2 * (todigit (xs ! i) * 2 ^ i)))" by (metis (mono_tags, opaque_lifting) ab_semigroup_mult_class.mult_ac(1) mult.commute) also have "... = todigit x + 2 * (∑i←[0..<length xs]. (todigit (xs ! i) * 2 ^ i))" using sum_list_const_mult by fastforce also have "... = todigit x + 2 * num xs" using num_def by simp finally show ?thesis . qed lemma num_append: "num (xs @ ys) = num xs + 2 ^ length xs * num ys" proof (induction "length xs" arbitrary: xs) case 0 then show ?case using num_def by simp next case (Suc n) then have xs: "xs = hd xs # tl xs" by (metis hd_Cons_tl list.size(3) nat.simps(3)) then have "xs @ ys = hd xs # (tl xs @ ys)" by simp then have "num (xs @ ys) = todigit (hd xs) + 2 * num (tl xs @ ys)" using num_Cons by presburger also have "... = todigit (hd xs) + 2 * (num (tl xs) + 2 ^ length (tl xs) * num ys)" using Suc by simp also have "... = todigit (hd xs) + 2 * num (tl xs) + 2 ^ Suc (length (tl xs)) * num ys" by simp also have "... = num xs + 2 ^ Suc (length (tl xs)) * num ys" using num_Cons xs by metis also have "... = num xs + 2 ^ length xs * num ys" using xs by (metis length_Cons) finally show ?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 then have "drop t zs = zs ! t # drop (Suc t) zs" by (simp add: Cons_nth_drop_Suc) then have "num (drop t zs) = todigit (zs ! t) + 2 * num (drop (Suc t) zs)" using num_Cons by simp then show ?thesis using digit_def True by simp next case False then show ?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" have 1: "?zs ! i = zs ! i" if "i < Suc t" for i using that by simp have 2: "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 also have "... = (∑i←[0..<Suc t]. todigit (?zs ! i) * 2 ^ i)" by (simp add: Suc_leI True min_absorb2) also have "... = (∑i←[0..<Suc t]. todigit (zs ! i) * 2 ^ i)" using 1 by (smt (verit, best) atLeastLessThan_iff map_eq_conv set_upt) also have "... = (∑i←[0..<t]. todigit (zs ! i) * 2 ^ i) + todigit (zs ! t) * 2 ^ t" by simp also have "... = (∑i←[0..<t]. todigit (take t zs ! i) * 2 ^ i) + todigit (zs ! t) * 2 ^ t" using 2 by (metis (no_types, lifting) atLeastLessThan_iff map_eq_conv set_upt) also have "... = num (take t zs) + todigit (zs ! t) * 2 ^ t" using num_def True by simp also have "... = num (take t zs) + todigit (digit zs t) * 2 ^ t" using digit_def True by simp finally show ?thesis by simp next case False then show ?thesis using digit_def by simp qed text ‹ A symbol sequence is a canonical representation of a natural number if the sequence contains only the symbols \textbf{0} and \textbf{1} and is either empty or ends in \textbf{1}. › definition canonical :: "symbol list ⇒ bool" where "canonical xs ≡ bit_symbols xs ∧ (xs = [] ∨ last xs = 𝟭)" lemma canonical_Cons: assumes "canonical xs" and "xs ≠ []" and "x = 𝟬 ∨ x = 𝟭" shows "canonical (x # xs)" using assms canonical_def less_Suc_eq_0_disj by auto lemma canonical_Cons_3: "canonical xs ⟹ canonical (𝟭 # 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 = 𝟬 ⟹ even (num (x # xs))" using num_Cons by simp lemma prepend_3_odd: "x = 𝟭 ⟹ odd (num (x # xs))" using num_Cons by simp text ‹ Every 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 moreover have "canonical xs ⟹ num xs = 0 ⟹ xs = []" for xs proof (rule ccontr) fix xs assume "canonical xs" "num xs = 0" "xs ≠ []" then have "length xs > 0" "last xs = 𝟭" using canonical_def by simp_all then have "xs ! (length xs - 1) = 𝟭" by (metis Suc_diff_1 last_length) then have "num xs ≥ 2 ^ (length xs - 1)" using num_ge_pow by (meson ‹0 < length xs› diff_less zero_less_one) then have "num xs > 0" by (meson dual_order.strict_trans1 le0 le_less_trans less_exp) then show False using ‹num xs = 0› by auto qed ultimately show ?thesis using IH True canonical_def by (metis less_nat_zero_code list.size(3)) next case False then have 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 then obtain xs where "num xs = m" "canonical xs" using IH by auto then have "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 then have "m > 0" using gt n by simp then have "xs ≠ []" using `num xs = m` num_def by auto then show ?thesis using canonical_Cons[of xs] `canonical xs` r_def True by simp next case False then show ?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 moreover have "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 then obtain x1 ys1 where 1: "xs1 = x1 # ys1" by (meson neq_Nil_conv) then have x1: "x1 = 𝟬 ∨ x1 = 𝟭" using canonical_def that(1) by auto have "xs2 ≠ []" using gt that(4) num_def by auto then obtain x2 ys2 where 2: "xs2 = x2 # ys2" by (meson neq_Nil_conv) then have x2: "x2 = 𝟬 ∨ x2 = 𝟭" using canonical_def that(3) by auto have "x1 = x2" using prepend_2_even prepend_3_odd that 1 2 x1 x2 by metis moreover have "n = todigit x1 + 2 * num ys1" using that(2) num_Cons 1 by simp moreover have "n = todigit x2 + 2 * num ys2" using that(4) num_Cons 2 by simp ultimately have "num ys1 = num ys2" by simp moreover have "num ys1 < n" using that(2) num_Cons 1 gt by simp moreover have "num ys2 < n" using that(4) num_Cons 2 gt by simp ultimately have "ys1 = ys2" using IH 1 2 that(1,3) by (metis canonical_tl) then show "xs1 = xs2" using `x1 = x2` 1 2 by simp qed ultimately show ?thesis using ‹num (tosym r # xs) = n› by auto qed qed text ‹ The 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 = [𝟭]" using num_def canonical_def by (intro canreprI) simp_all text ‹ The length of the canonical representation of a number $n$: › abbreviation nlength :: "nat ⇒ nat" where "nlength n ≡ length (canrepr 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 𝟬 @ [𝟭]) = 2 ^ j" proof (induction j) case 0 then show ?case using num_def by simp next case (Suc j) then show ?case using num_Cons by simp qed lemma num_replicate3_eq_pow_minus_1: "num (replicate j 𝟭) = 2 ^ j - 1" proof (induction j) case 0 then show ?case using num_def by simp next case (Suc j) then have "num (replicate (Suc j) 𝟭) = num (𝟭 # replicate j 𝟭)" by simp also have "... = 1 + 2 * (2 ^ j - 1)" using Suc num_Cons by simp also have "... = 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) also have "... = 2 ^ Suc j - 1" by simp finally show ?case . qed lemma nlength_pow2: "nlength (2 ^ j) = Suc j" proof - define xs :: "nat list" where "xs = replicate j 2 @ [3]" then have "length xs = Suc j" by simp moreover have "num xs = 2 ^ j" using num_replicate2_eq_pow xs_def by simp moreover have "canonical xs" using xs_def bit_symbols_append canonical_def by simp ultimately show ?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 𝟭" then have "length xs = j" by simp moreover have "num xs = 2 ^ j - 1" using num_replicate3_eq_pow_minus_1 xs_def by simp moreover have "canonical xs" proof - have "bit_symbols xs" using xs_def by simp moreover have "last xs = 3 ∨ xs = []" by (cases "j = 0") (simp_all add: xs_def) ultimately show ?thesis using canonical_def by auto qed ultimately show ?thesis using canreprI by metis qed corollary nlength_3: "nlength 3 = 2" using nlength_pow_minus_1[of 2] by simp text ‹ When handling natural numbers, Turing machines will usually have tape contents of the following form: › abbreviation ncontents :: "nat ⇒ (nat ⇒ symbol)" ("⌊_⌋⇩_{N}") where "⌊n⌋⇩_{N}≡ ⌊canrepr n⌋" 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 ‹ Every bit symbol sequence can be turned into a canonical representation of some number by stripping trailing zeros. The length of the prefix without trailing zeros is given by the next function: › definition canlen :: "symbol list ⇒ nat" where "canlen zs ≡ LEAST m. ∀i<length zs. i ≥ m ⟶ zs ! i = 𝟬" lemma canlen_at_ge: "∀i<length zs. i ≥ canlen zs ⟶ zs ! i = 𝟬" proof - let ?P = "λm. ∀i<length zs. i ≥ m ⟶ zs ! i = 𝟬" have "?P (length zs)" by simp then show ?thesis unfolding canlen_def using LeastI[of ?P "length zs"] by fast qed lemma canlen_eqI: assumes "∀i<length zs. i ≥ m ⟶ zs ! i = 𝟬" and "⋀y. ∀i<length zs. i ≥ y ⟶ zs ! i = 𝟬 ⟹ 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 = 𝟬" have "?P (length zs)" by simp then show ?thesis unfolding canlen_def using Least_le[of _ "length zs"] by simp qed lemma canlen_le: assumes "∀i<length zs. i ≥ m ⟶ zs ! i = 𝟬" 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) = 𝟭" proof (rule ccontr) assume "zs ! (canlen zs - 1) ≠ 𝟭" then have "zs ! (canlen zs - 1) = 𝟬" using assms canlen_le_length by (metis One_nat_def Suc_pred lessI less_le_trans) then have "∀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) then have "canlen zs - 1 ≥ canlen zs" using canlen_le by auto then show 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 then show ?thesis using canonical_def by simp next case False then show ?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) case 0 then show ?case by simp next case (Suc x) let ?m = "canlen zs" have *: "∀i<length zs. i ≥ ?m ⟶ zs ! i = 𝟬" using canlen_at_ge by auto have "canlen zs < length zs" using Suc by simp then have "zs ! (length zs - 1) = 𝟬" 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) then have "todigit (zs ! (length zs - 1)) = 0" by simp moreover have 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) ultimately have "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 = 𝟬" by (simp add: canlen_at_ge) show "⋀y. ∀i<length ?ys. y ≤ i ⟶ ?ys ! i = 𝟬 ⟹ 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 then have "length ?ys - canlen ?ys = x" using ys Suc.hyps(2) by (metis butlast_snoc diff_Suc_1 diff_commute length_butlast) then have "num (take (canlen ?ys) ?ys) = num ?ys" using Suc by blast then have "num (take (canlen zs) ?ys) = num ?ys" using canlen_ys by simp then have "num (take (canlen zs) zs) = num ?ys" by (metis ‹canlen zs < length zs› butlast_snoc take_butlast ys) then show ?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) = 𝟭" using canonical_def assms canonical_canrepr by (metis Suc_neq_Zero diff_Suc_1 last_length length_0_conv) moreover have "(∑i←[0..<length ?xs]. todigit (?xs ! i) * 2 ^ i) ≥ todigit (?xs ! (length ?xs - 1)) * 2 ^ (length ?xs - 1)" using assms by simp ultimately have "num ?xs ≥ 2 ^ (length ?xs - 1)" using num_def by simp moreover have "num ?xs = n" using canrepr by simp ultimately show ?thesis using assms by simp qed lemma nlength_less_pow: "n < 2 ^ (nlength n)" proof (induction "nlength n" arbitrary: n) case 0 then show ?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)" then have "nlength n' = j" using len can canreprI by simp then have n'_less: "n' < 2 ^ j" using Suc by auto have "num ?xs = todigit (hd ?xs) + 2 * num (tl ?xs)" by (metis hdtl num_Cons) then have "n = todigit (hd ?xs) + 2 * num (tl ?xs)" using canrepr by simp also have "... ≤ 1 + 2 * num (tl ?xs)" by simp also have "... = 1 + 2 * n'" using n'_def by simp also have "... ≤ 1 + 2 * (2 ^ j - 1)" using n'_less by simp also have "... = 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)) also have "... < 2 ^ (Suc j)" by simp also have "... = 2 ^ (nlength n)" using lenxs by simp finally show ?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" then have "nlength n < Suc j ∨ nlength n > Suc j" by auto then show False proof assume "nlength n < Suc j" then have "nlength n ≤ j" by simp moreover have "n < 2 ^ (nlength n)" using nlength_less_pow by simp ultimately have "n < 2 ^ j" by (metis le_less_trans nat_power_less_imp_less not_less numeral_2_eq_2 zero_less_Suc) then show False using assms(1) by simp next assume *: "nlength n > Suc j" then have "n ≥ 2 ^ (nlength n - 1)" using nlength_ge_pow by simp moreover have "nlength n - 1 ≥ Suc j" using * by simp ultimately have "n ≥ 2 ^ (Suc j)" by (metis One_nat_def le_less_trans less_2_cases_iff linorder_not_less power_less_imp_less_exp) then show False using assms(2) by simp qed qed lemma nlength_le_n: "nlength n ≤ n" proof (cases "n = 0") case True then show ?thesis using canrepr_0 by simp next case False then have "nlength n > 0" using nlength_0 by simp moreover from this have "n ≥ 2 ^ (nlength n - 1)" using nlength_0 nlength_ge_pow by auto ultimately show ?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 then show ?thesis by (simp add: canrepr_0) next case False then obtain j where j: "nlength n = Suc j" by (metis canrepr canrepr_0 gr0_implies_Suc length_greater_0_conv) then have "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 then have "Suc n < 2 ^ (Suc (Suc j))" by simp then have "nlength (Suc n) = Suc (Suc j)" using True pow_nlength by simp then show ?thesis using j by simp next case False then have "Suc n < 2 ^ (Suc j)" by simp then have "nlength (Suc n) = Suc j" using `n ≥ 2 ^ j` pow_nlength by simp then show ?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) case 0 then show ?case by simp next case (Suc d) then show ?case using nlength_Suc_le by (metis nat_arith.suc1 order_trans) qed then show ?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" then have "nlength n > 0" by (metis canrepr canrepr_0 length_greater_0_conv less_numeral_extra(3)) then have "n ≥ 2 ^ (nlength n - 1)" using Suc_diff_1 nlength_ge_pow by simp then have "2 * n ≥ 2 ^ (nlength n)" by (metis Suc_diff_1 ‹0 < nlength n› mult_le_mono2 power_Suc) moreover have "2 * n < 2 ^ (Suc (nlength n))" using nlength_less_pow by simp ultimately show ?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 then have "n1 * n2 < 2 ^ ?j1 * 2 ^ ?j2" by (simp add: mult_strict_mono) then have "n1 * n2 < 2 ^ (?j1 + ?j2)" by (simp add: power_add) then have "n1 * n2 ≤ 2 ^ (?j1 + ?j2) - 1" by simp then have "nlength (n1 * n2) ≤ nlength (2 ^ (?j1 + ?j2) - 1)" using nlength_mono by simp then show "nlength (n1 * n2) ≤ ?j1 + ?j2" using nlength_pow_minus_1 by simp qed text ‹ In the following lemma @{const Suc} is needed because $n^0 = 1$. › lemma nlength_pow: "nlength (n ^ d) ≤ Suc (d * nlength n)" proof (induction d) case 0 then show ?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) then have "nlength (n ^ Suc d) ≤ nlength (n ^ d) + nlength n" using nlength_prod by simp then show ?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 then have "nlength (n1 + n2) ≤ nlength (2 * ?m)" using nlength_mono by simp moreover have "nlength ?m = max (nlength n1) (nlength n2)" using nlength_mono by (metis max.absorb1 max.cobounded2 max_def) ultimately show ?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_Suc: "nlength (Suc n) ≤ Suc (nlength n)" using nlength_sum nlength_1_simp by (metis One_nat_def Suc_leI add_Suc diff_Suc_1 length_greater_0_conv max.absorb_iff2 max.commute max_def nlength_0 plus_1_eq_Suc) lemma nlength_less_n: "n ≥ 3 ⟹ nlength n < n" proof (induction n rule: nat_induct_at_least) case base then show ?case by (simp add: nlength_3) next case (Suc n) then show ?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 ‹ In order to compare two numbers in canonical representation, we can use the Turing machine @{const tm_equals}, which works for arbitrary proper symbol sequences. \null › lemma min_nlength: "min (nlength n1) (nlength n2) = nlength (min n1 n2)" by (metis min_absorb2 min_def nat_le_linear nlength_mono) lemma max_nlength: "max (nlength n1) (nlength n2) = nlength (max n1 n2)" using nlength_mono by (metis max.absorb1 max.cobounded2 max_def) lemma contents_blank_0: "⌊[□]⌋ = ⌊[]⌋" using contents_def by auto definition tm_equalsn :: "tapeidx ⇒ tapeidx ⇒ tapeidx ⇒ machine" where "tm_equalsn ≡ tm_equals" lemma tm_equalsn_tm: assumes "k ≥ 2" and "G ≥ 4" and "0 < j3" shows "turing_machine k G (tm_equalsn j1 j2 j3)" unfolding tm_equalsn_def using assms tm_equals_tm by simp lemma transforms_tm_equalsnI [transforms_intros]: fixes j1 j2 j3 :: tapeidx fixes tps tps' :: "tape list" and k b n1 n2 :: nat assumes "length tps = k" "j1 ≠ j2" "j2 ≠ j3" "j1 ≠ j3" "j1 < k" "j2 < k" "j3 < k" and "b ≤ 1" assumes "tps ! j1 = (⌊n1⌋⇩_{N}, 1)" "tps ! j2 = (⌊n2⌋⇩_{N}, 1)" "tps ! j3 = (⌊b⌋⇩_{N}, 1)" assumes "ttt = (3 * nlength (min n1 n2) + 7)" assumes "tps' = tps [j3 := (⌊if n1 = n2 then 1 else 0⌋⇩_{N}, 1)]" shows "transforms (tm_equalsn j1 j2 j3) tps ttt tps'" unfolding tm_equalsn_def proof (tform tps: assms) show "proper_symbols (canrepr n1)" using proper_symbols_canrepr by simp show "proper_symbols (canrepr n2)" using proper_symbols_canrepr by simp show "ttt = 3 * min (nlength n1) (nlength n2) + 7" using assms(12) min_nlength by simp let ?v = "if canrepr n1 = canrepr n2 then 3::nat else 0::nat" have "b = 0 ∨ b = 1" using assms(8) by auto then have "⌊b⌋⇩_{N}= ⌊[]⌋ ∨ ⌊b⌋⇩_{N}= ⌊[𝟭]⌋" using canrepr_0 canrepr_1 by auto then have "tps ! j3 = (⌊[]⌋, 1) ∨ tps ! j3 = (⌊[𝟭]⌋, 1)" using assms(11) by simp then have v: "tps ! j3 |:=| ?v = (⌊[?v]⌋, 1)" using contents_def by auto show "tps' = tps[j3 := tps ! j3 |:=| ?v]" proof (cases "n1 = n2") case True then show ?thesis using canrepr_1 v assms(13) by auto next case False then have "?v = 0" by (metis canrepr) then show ?thesis using canrepr_0 v assms(13) contents_blank_0 by auto qed qed subsubsection ‹Copying a number between tapes› text ‹ The next Turing machine overwrites the contents of tape $j_2$ with the contents of tape $j_1$ and performs a carriage return on both tapes. › definition tm_copyn :: "tapeidx ⇒ tapeidx ⇒ machine" where "tm_copyn j1 j2 ≡ tm_erase_cr j2 ;; tm_cp_until j1 j2 {□} ;; tm_cr j1 ;; tm_cr j2" lemma tm_copyn_tm: assumes "k ≥ 2" and "G ≥ 4" and "j1 < k" "j2 < k" "j1 ≠ j2" "0 < j2" shows "turing_machine k G (tm_copyn j1 j2)" unfolding tm_copyn_def using assms tm_cp_until_tm tm_cr_tm tm_erase_cr_tm by simp locale turing_machine_move = fixes j1 j2 :: tapeidx begin definition "tm1 ≡ tm_erase_cr j2" definition "tm2 ≡ tm1 ;; tm_cp_until j1 j2 {□}" definition "tm3 ≡ tm2 ;; tm_cr j1" definition "tm4 ≡ tm3 ;; tm_cr j2" lemma tm4_eq_tm_copyn: "tm4 = tm_copyn j1 j2" unfolding tm4_def tm3_def tm2_def tm1_def tm_copyn_def by simp context fixes x y :: nat and tps0 :: "tape list" assumes j_less [simp]: "j1 < length tps0" "j2 < length tps0" assumes j [simp]: "j1 ≠ j2" and tps_j1 [simp]: "tps0 ! j1 = (⌊x⌋⇩_{N}, 1)" and tps_j2 [simp]: "tps0 ! j2 = (⌊y⌋⇩_{N}, 1)" begin definition "tps1 ≡ tps0 [j2 := (⌊[]⌋, 1)]" lemma tm1 [transforms_intros]: assumes "t = 7 + 2 * nlength y" shows "transforms tm1 tps0 t tps1" unfolding tm1_def proof (tform tps: tps1_def time: assms) show "proper_symbols (canrepr y)" using proper_symbols_canrepr by simp qed definition "tps2 ≡ tps0 [j1 := (⌊x⌋⇩_{N}, Suc (nlength x)), j2 := (⌊x⌋⇩_{N}, Suc (nlength x))]" lemma tm2 [transforms_intros]: assumes "t = 8 + (2 * nlength y + nlength x)" shows "transforms tm2 tps0 t tps2" unfolding tm2_def proof (tform tps: tps1_def time: assms) show "rneigh (tps1 ! j1) {□} (nlength x)" proof (rule rneighI) show "(tps1 ::: j1) (tps1 :#: j1 + nlength x) ∈ {□}" using tps1_def canrepr_0 contents_outofbounds j(1) nlength_0_simp tps_j1 by (metis fst_eqD lessI nth_list_update_neq plus_1_eq_Suc singleton_iff snd_eqD) show "⋀n'. n' < nlength x ⟹ (tps1 ::: j1) (tps1 :#: j1 + n') ∉ {□}" using tps1_def tps_j1 j j_less contents_inbounds proper_symbols_canrepr by (metis Suc_leI add_diff_cancel_left' fst_eqD not_add_less2 nth_list_update_neq plus_1_eq_Suc singletonD snd_eqD zero_less_Suc) qed have "(⌊x⌋⇩_{N}, Suc (nlength x)) = tps0[j2 := (⌊[]⌋, 1)] ! j1 |+| nlength x" using tps_j1 tps_j2 by (metis fst_eqD j(1) j_less(2) nth_list_update plus_1_eq_Suc snd_eqD) moreover have "(⌊x⌋⇩_{N}, Suc (nlength x)) = implant (tps0[j2 := (⌊[]⌋, 1)] ! j1) (tps0[j2 := (⌊[]⌋, 1)] ! j2) (nlength x)" using tps_j1 tps_j2 j j_less implant_contents nlength_0_simp by (metis add.right_neutral append.simps(1) canrepr_0 diff_Suc_1 drop0 le_eq_less_or_eq nth_list_update_eq nth_list_update_neq plus_1_eq_Suc take_all zero_less_one) ultimately show "tps2 = tps1 [j1 := tps1 ! j1 |+| nlength x, j2 := implant (tps1 ! j1) (tps1 ! j2) (nlength x)]" unfolding tps2_def tps1_def by (simp add: list_update_swap[of j1]) qed definition "tps3 ≡ tps0[j2 := (⌊x⌋⇩_{N}, Suc (nlength x))]" lemma tm3 [transforms_intros]: assumes "t = 11 + (2 * nlength y + 2 * nlength x)" shows "transforms tm3 tps0 t tps3" unfolding tm3_def proof (tform tps: tps2_def) have "tps2 :#: j1 = Suc (nlength x)" using assms tps2_def by (metis j(1) j_less(1) nth_list_update_eq nth_list_update_neq snd_conv) then show "t = 8 + (2 * nlength y + nlength x) + (tps2 :#: j1 + 2)" using assms by simp show "clean_tape (tps2 ! j1)" using tps2_def by (simp add: clean_tape_ncontents nth_list_update_neq') have "tps2 ! j1 |#=| 1 = (⌊x⌋⇩_{N}, 1)" using tps2_def by (simp add: nth_list_update_neq') then show "tps3 = tps2[j1 := tps2 ! j1 |#=| 1]" using tps3_def tps2_def by (metis j(1) list_update_id list_update_overwrite list_update_swap tps_j1) qed definition "tps4 ≡ tps0[j2 := (⌊x⌋⇩_{N}, 1)]" lemma tm4: assumes "t = 14 + (3 * nlength x + 2 * nlength y)" shows "transforms tm4 tps0 t tps4" unfolding tm4_def proof (tform tps: tps3_def time: tps3_def assms) show "clean_tape (tps3 ! j2)" using tps3_def clean_tape_ncontents by simp have "tps3 ! j2 |#=| 1 = (⌊x⌋⇩_{N}, 1)" using tps3_def by (simp add: nth_list_update_neq') then show "tps4 = tps3[j2 := tps3 ! j2 |#=| 1]" using tps4_def tps3_def by (metis list_update_overwrite tps_j1) qed lemma tm4': assumes "t = 14 + 3 * (nlength x + nlength y)" shows "transforms tm4 tps0 t tps4" using tm4 transforms_monotone assms by simp end end (* locale turing_machine_move *) lemma transforms_tm_copynI [transforms_intros]: fixes j1 j2 :: tapeidx fixes tps tps' :: "tape list" and k x y :: nat assumes "j1 ≠ j2" "j1 < length tps" "j2 < length tps" assumes "tps ! j1 = (⌊x⌋⇩_{N}, 1)" "tps ! j2 = (⌊y⌋⇩_{N}, 1)" assumes "ttt = 14 + 3 * (nlength x + nlength y)" assumes "tps' = tps [j2 := (⌊x⌋⇩_{N}, 1)]" shows "transforms (tm_copyn j1 j2) tps ttt tps'" proof - interpret loc: turing_machine_move j1 j2 . show ?thesis using assms loc.tm4' loc.tps4_def loc.tm4_eq_tm_copyn by simp qed subsubsection ‹Setting the tape contents to a number› text ‹ The Turing machine in this section writes a hard-coded number to a tape. › definition tm_setn :: "tapeidx ⇒ nat ⇒ machine" where "tm_setn j n ≡ tm_set j (canrepr n)" 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 then show ?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 ‹ In this section we devise a Turing machine that increments a number. The next function describes how the symbol sequence of the incremented number looks like. Basically one has to flip all @{text 𝟭} symbols starting at the least significant digit until one reaches a @{text 𝟬}, which is then replaced by a @{text 𝟭}. If there is no @{text 𝟬}, a @{text 𝟭} is appended. Here we exploit that the most significant digit is to the right. › definition nincr :: "symbol list ⇒ symbol list" where "nincr zs ≡ if ∃i<length zs. zs ! i = 𝟬 then replicate (LEAST i. i < length zs ∧ zs ! i = 𝟬) 𝟬 @ [𝟭] @ drop (Suc (LEAST i. i < length zs ∧ zs ! i = 𝟬)) zs else replicate (length zs) 𝟬 @ [𝟭]" lemma canonical_nincr: assumes "canonical zs" shows "canonical (nincr zs)" proof - have 1: "bit_symbols zs" using canonical_def assms by simp let ?j = "LEAST i. i < length zs ∧ zs ! i = 𝟬" have "bit_symbols (nincr zs)" proof (cases "∃i<length zs. zs ! i = 𝟬") case True then have "nincr zs = replicate ?j 𝟬 @ [𝟭] @ drop (Suc ?j) zs" using nincr_def by simp moreover have "bit_symbols (replicate ?j 𝟬)" by simp moreover have "bit_symbols [𝟭]" by simp moreover have "bit_symbols (drop (Suc ?j) zs)" using 1 by simp ultimately show ?thesis using bit_symbols_append by presburger next case False then show ?thesis using nincr_def bit_symbols_append by auto qed moreover have "last (nincr zs) = 𝟭" proof (cases "∃i<length zs. zs ! i = 𝟬") case True then show ?thesis using nincr_def assms canonical_def by auto next case False then show ?thesis using nincr_def by auto qed ultimately show ?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 = 𝟬") case True define j where "j = (LEAST i. i < length zs ∧ zs ! i = 𝟬)" then have 1: "j < length zs ∧ zs ! j = 𝟬" using LeastI_ex[OF True] by simp have 2: "zs ! i = 𝟭" 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 𝟭 @ [𝟬]" define ys :: "symbol list" where "ys = drop (Suc j) zs" have "zs = xs @ ys" proof - have "xs = take (Suc j) zs" using xs_def 1 2 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) then show ?thesis using ys_def by simp qed have "nincr zs = replicate j 𝟬 @ [𝟭] @ drop (Suc j) zs" using nincr_def True j_def by simp then have "num (nincr zs) = num (replicate j 𝟬 @ [𝟭] @ ys)" using ys_def by simp also have "... = num (replicate j 𝟬 @ [𝟭]) + 2 ^ Suc j * num ys" using num_append by (metis append_assoc length_append_singleton length_replicate) also have "... = Suc (num xs) + 2 ^ Suc j * num ys" proof - have "num (replicate j 𝟬 @ [𝟭]) = 2 ^ j" using num_replicate2_eq_pow by simp also have "... = Suc (2 ^ j - 1)" by simp also have "... = Suc (num (replicate j 𝟭))" using num_replicate3_eq_pow_minus_1 by simp also have "... = Suc (num (replicate j 𝟭 @ [𝟬]))" using num_trailing_zero by simp finally have "num (replicate j 𝟬 @ [𝟭]) = Suc (num xs)" using xs_def by simp then show ?thesis by simp qed also have "... = Suc (num xs + 2 ^ Suc j * num ys)" by simp also have "... = Suc (num zs)" using `zs = xs @ ys` num_append xs_def by (metis length_append_singleton length_replicate) finally show ?thesis . next case False then have "∀i<length zs. zs ! i = 𝟭" using assms by simp then have zs: "zs = replicate (length zs) 𝟭" by (simp add: nth_equalityI) then have num_zs: "num zs = 2 ^ length zs - 1" by (metis num_replicate3_eq_pow_minus_1) have "nincr zs = replicate (length zs) 𝟬 @ [𝟭]" using nincr_def False by auto then have "num (nincr zs) = 2 ^ length zs" by (simp add: num_replicate2_eq_pow) then show ?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 ‹ The next Turing machine performs the incrementing. Starting from the left of the symbol sequence on tape $j$, it writes the symbol \textbf{0} until it reaches a blank or the symbol \textbf{1}. Then it writes a \textbf{1} and returns the tape head to the beginning. › definition tm_incr :: "tapeidx ⇒ machine" where "tm_incr j ≡ tm_const_until j j {□, 𝟬} 𝟬 ;; tm_write j 𝟭 ;; tm_cr j" lemma tm_incr_tm: assumes "G ≥ 4" and "k ≥ 2" and "j < k" and "j > 0" shows "turing_machine k G (tm_incr j)" unfolding tm_incr_def using assms tm_const_until_tm tm_write_tm tm_cr_tm by simp locale turing_machine_incr = fixes j :: tapeidx begin definition "tm1 ≡ tm_const_until j j {□, 𝟬} 𝟬" definition "tm2 ≡ tm1 ;; tm_write j 𝟭" definition "tm3 ≡ tm2 ;; tm_cr j" lemma tm3_eq_tm_incr: "tm3 = tm_incr j" unfolding tm3_def tm2_def tm1_def tm_incr_def by simp context fixes x k :: nat and tps :: "tape list" assumes jk [simp]: "j < k" "length tps = k" and tps0 [simp]: "tps ! j = (⌊x⌋⇩_{N}, 1)" begin lemma tm1 [transforms_intros]: assumes "i0 = (LEAST i. i ≤ nlength x ∧ ⌊x⌋⇩_{N}(Suc i) ∈ {□, 𝟬})" and "tps' = tps[j := constplant (tps ! j) 𝟬 i0]" shows "transforms tm1 tps (Suc i0) tps'" unfolding tm1_def proof (tform tps: assms(2)) let ?P = "λi. i ≤ nlength x ∧ ⌊x⌋⇩_{N}(Suc i) ∈ {□, 𝟬}" have 2: "i0 ≤ nlength x ∧ ⌊x⌋⇩_{N}(Suc i0) ∈ {□, 𝟬}" using LeastI[of ?P "nlength x"] jk(1) assms(1) by simp have 3: "¬ ?P i" if "i < i0" for i using not_less_Least[of i ?P] jk(1) assms(1) that by simp show "rneigh (tps ! j) {□, 𝟬} i0" proof (rule rneighI) show "(tps ::: j) (tps :#: j + i0) ∈ {□, 𝟬}" using tps0 2 jk(1) assms(1) by simp show "⋀n'. n' < i0 ⟹ (tps ::: j) (tps :#: j + n') ∉ {□, 𝟬}" using tps0 2 3 jk(1) assms(1) by simp qed qed lemma tm2 [transforms_intros]: assumes "i0 = (LEAST i. i ≤ nlength x ∧ ⌊x⌋⇩_{N}(Suc i) ∈ {□, 𝟬})" and "ttt = Suc (Suc i0)" and "tps' = tps[j := (⌊Suc x⌋⇩_{N}, Suc i0)]" shows "transforms tm2 tps ttt tps'" unfolding tm2_def proof (tform tps: assms(1,3) time: assms(1,2)) let ?P = "λi. i ≤ nlength x ∧ ⌊x⌋⇩_{N}(Suc i) ∈ {□, 𝟬}" have 1: "?P (nlength x)" by simp have 2: "i0 ≤ nlength x ∧ ⌊x⌋⇩_{N}(Suc i0) ∈ {□, 𝟬}" using LeastI[of ?P "nlength x"] assms(1) by simp have 3: "¬ ?P i" if "i < i0" for i using not_less_Least[of i ?P] assms(1) that by simp let ?i = "LEAST i. i ≤ nlength x ∧ ⌊x⌋⇩_{N}(Suc i) ∈ {□, 𝟬}" show "tps' = tps [j := constplant (tps ! j) 2 ?i, j := tps[j := constplant (tps ! j) 𝟬 ?i] ! j |:=| 𝟭]" (is "tps' = ?rhs") proof - have "?rhs = tps [j := constplant (⌊x⌋⇩_{N}, Suc 0) 𝟬 i0 |:=| 𝟭]" using jk assms(1) by simp moreover have "(⌊Suc x⌋⇩_{N}, Suc i0) = constplant (⌊x⌋⇩_{N}, Suc 0) 2 i0 |:=| 𝟭" (is "?l = ?r") proof - have "snd ?l = snd ?r" by (simp add: transplant_def) moreover have "⌊Suc x⌋⇩_{N}= fst ?r" proof - let ?zs = "canrepr x" have l: "⌊Suc x⌋⇩_{N}= ⌊nincr ?zs⌋" by (simp add: nincr_canrepr) have r: "fst ?r = (λi. if Suc 0 ≤ i ∧ i < Suc i0 then 𝟬 else ⌊x⌋⇩_{N}i)(Suc i0 := 𝟭)" using constplant by auto show ?thesis proof (cases "∃i<length ?zs. ?zs ! i = 𝟬") case True let ?Q = "λi. i < length ?zs ∧ ?zs ! i = 𝟬" have Q1: "?Q (Least ?Q)" using True by (metis (mono_tags, lifting) LeastI_ex) have Q2: "¬ ?Q i" if "i < Least ?Q" for i using True not_less_Least that by blast have "Least ?P = Least ?Q" proof (rule Least_equality) show "Least ?Q ≤ nlength x ∧ ⌊x⌋⇩_{N}(Suc (Least ?Q)) ∈ {□, 𝟬}" proof show "Least ?Q ≤ nlength x" using True by (metis (mono_tags, lifting) LeastI_ex less_imp_le) show "⌊x⌋⇩_{N}(Suc (Least ?Q)) ∈ {□, 𝟬}" using True by (simp add: Q1 Suc_leI) qed then show "⋀y. y ≤ nlength x ∧ ⌊x⌋⇩_{N}(Suc y) ∈ {□, 𝟬} ⟹ (Least ?Q) ≤ y" using True Q1 Q2 bit_symbols_canrepr contents_def by (metis (no_types, lifting) Least_le antisym_conv2 diff_Suc_1 insert_iff le_less_Suc_eq less_nat_zero_code nat_le_linear proper_symbols_canrepr singletonD) qed then have i0: "i0 = Least ?Q" using assms(1) by simp then have nincr_zs: "nincr ?zs = replicate i0 𝟬 @ [𝟭] @ drop (Suc i0) ?zs" using nincr_def True by simp show ?thesis proof fix i consider "i = 0" | "Suc 0 ≤ i ∧ i < Suc i0" | "i = Suc i0" | "i > Suc i0 ∧ i ≤ length ?zs" | "i > Suc i0 ∧ i > length ?zs" by linarith then have "⌊replicate i0 𝟬 @ [𝟭] @ drop (Suc i0) ?zs⌋ i = ((λi. if Suc 0 ≤ i ∧ i < Suc i0 then 𝟬 else ⌊x⌋⇩_{N}i)(Suc i0 := 𝟭)) i" (is "?A i = ?B i") proof (cases) case 1 then show ?thesis by (simp add: transplant_def) next case 2 then have "i - 1 < i0" by auto then have "(replicate i0 𝟬 @ [𝟭] @ drop (Suc i0) ?zs) ! (i - 1) = 𝟬" by (metis length_replicate nth_append nth_replicate) then have "?A i = 𝟬" using contents_def i0 "2" Q1 nincr_canrepr nincr_zs by (metis Suc_le_lessD le_trans less_Suc_eq_le less_imp_le_nat less_numeral_extra(3) nlength_Suc_le) moreover have "?B i = 𝟬" using i0 2 by simp ultimately show ?thesis by simp next case 3 then show ?thesis using i0 Q1 canrepr_0 contents_inbounds nincr_canrepr nincr_zs nlength_0_simp nlength_Suc nlength_Suc_le by (metis (no_types, lifting) contents_append_update fun_upd_apply length_replicate) next case 4 then have "?A i = (replicate i0 𝟬 @ [𝟭] @ drop (Suc i0) ?zs) ! (i - 1)" by auto then have "?A i = ((replicate i0 𝟬 @ [𝟭]) @ drop (Suc i0) ?zs) ! (i - 1)" by simp moreover have "length (replicate i0 𝟬 @ [𝟭]) = Suc i0" by simp moreover have "i - 1 < length ?zs" using 4 by auto moreover have "i - 1 >= Suc i0" using 4 by auto ultimately have "?A i = ?zs ! (i - 1)" using i0 Q1 by (metis (no_types, lifting) Suc_leI append_take_drop_id length_take min_absorb2 not_le nth_append) moreover have "?B i = ⌊x⌋⇩_{N}i" using 4 by simp ultimately show ?thesis using i0 4 contents_def by simp next case 5 then show ?thesis by auto qed then show "⌊Suc x⌋⇩_{N}i = fst (constplant (⌊x⌋⇩_{N}, Suc 0) 𝟬 i0 |:=| 𝟭) i" using nincr_zs l r by simp qed next case False then have nincr_zs: "nincr ?zs = replicate (length ?zs) 𝟬 @ [𝟭]" using nincr_def by auto have "Least ?P = length ?zs" proof (rule Least_equality) show "nlength x ≤ nlength x ∧ ⌊x⌋⇩_{N}(Suc (nlength x)) ∈ {□, 𝟬}" by simp show "⋀y. y ≤ nlength x ∧ ⌊x⌋⇩_{N}(Suc y) ∈ {□, 𝟬} ⟹ nlength x ≤ y" using False contents_def bit_symbols_canrepr by (metis diff_Suc_1 insert_iff le_neq_implies_less nat.simps(3) not_less_eq_eq numeral_3_eq_3 singletonD) qed then have i0: "i0 = length ?zs" using assms(1) by simp show ?thesis proof fix i consider "i = 0" | "Suc 0 ≤ i ∧ i < Suc (length ?zs)" | "i = Suc (length ?zs)" | "i > Suc (length ?zs)" by linarith then have "⌊replicate (length ?zs) 𝟬 @ [𝟭]⌋ i = ((λi. if Suc 0 ≤ i ∧ i < Suc i0 then 𝟬 else ⌊x⌋⇩_{N}i)(Suc i0 := 𝟭)) i" (is "?A i = ?B i") proof (cases) case 1 then show ?thesis by (simp add: transplant_def) next case 2 then have "?A i = 𝟬" by (metis One_nat_def Suc_le_lessD add.commute contents_def diff_Suc_1 length_Cons length_append length_replicate less_Suc_eq_0_disj less_imp_le_nat less_numeral_extra(3) list.size(3) nth_append nth_replicate plus_1_eq_Suc) moreover have "?B i = 𝟬" using i0 2 by simp ultimately show ?thesis by simp next case 3 then show ?thesis using i0 canrepr_0 contents_inbounds nincr_canrepr nincr_zs nlength_0_simp nlength_Suc by (metis One_nat_def add.commute diff_Suc_1 fun_upd_apply length_Cons length_append length_replicate nth_append_length plus_1_eq_Suc zero_less_Suc) next case 4 then show ?thesis using i0 by simp qed then show "⌊Suc x⌋⇩_{N}i = fst (constplant (⌊x⌋⇩_{N}, Suc 0) 𝟬 i0 |:=| 𝟭) i" using nincr_zs l r by simp qed qed qed ultimately show ?thesis by simp qed ultimately show ?thesis using assms(3) by simp qed qed lemma tm3: assumes "i0 = (LEAST i. i ≤ nlength x ∧ ⌊x⌋⇩_{N}(Suc i) ∈ {□, 𝟬})" and "ttt = 5 + 2 * i0" and "tps' = tps[j := (⌊Suc x⌋⇩_{N}, Suc 0)]" shows "transforms tm3 tps ttt tps'" unfolding tm3_def proof (tform tps: assms(1,3) time: assms(1,2)) let ?tps = "tps[j := (⌊Suc x⌋⇩_{N}, Suc (LEAST i. i ≤ nlength x ∧ ⌊x⌋⇩_{N}(Suc i) ∈ {□, 𝟬}))]" show "clean_tape (?tps ! j)" using clean_tape_ncontents by (simp add: assms(1,3)) qed lemma tm3': assumes "ttt = 5 + 2 * nlength x" and "tps' = tps[j := (⌊Suc x⌋⇩_{N}, Suc 0)]" shows "transforms tm3 tps ttt tps'" proof - let ?P = "λi. i ≤ nlength x ∧ ⌊x⌋⇩_{N}(Suc i) ∈ {□, 𝟬}" define i0 where "i0 = Least ?P" have "i0 ≤ nlength x ∧ ⌊x⌋⇩_{N}(Suc i0) ∈ {□, 𝟬}" using LeastI[of ?P "nlength x"] i0_def by simp then have "5 + 2 * i0 ≤ 5 + 2 * nlength x" by simp moreover have "transforms tm3 tps (5 + 2 * i0) tps'" using assms tm3 i0_def by simp ultimately show ?thesis using transforms_monotone assms(1) by simp qed end (* context *) end (* locale *) lemma transforms_tm_incrI [transforms_intros]: assumes "j < k" and "length tps = k" and "tps ! j = (⌊x⌋⇩_{N}, 1)" and "ttt = 5 + 2 * nlength x" and "tps' = tps[j := (⌊Suc x⌋⇩_{N}, 1)]" shows "transforms (tm_incr j) tps ttt tps'" proof - interpret loc: turing_machine_incr j . show ?thesis using assms loc.tm3' loc.tm3_eq_tm_incr by simp qed subsubsection ‹Incrementing multiple times› text ‹ Adding a constant by iteratively incrementing is not exactly efficient, but it still 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') case 0 then show ?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 moreover have "?ttt ≤ ttt" proof - have "?ttt = Suc c * (5 + 2 * nlength (x + c))" by simp also have "... ≤ Suc c * (5 + 2 * nlength (x + Suc c))" using nlength_mono Suc_mult_le_cancel1 by auto finally show "?ttt ≤ ttt" using Suc by simp qed ultimately have "transforms (tm_plus_const c j ;; tm_incr j) tps ttt tps'" using transforms_monotone by simp then show ?case by simp qed subsection ‹Decrementing› text ‹ Decrementing 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 canonical symbol sequence, a trailing zero must be removed, whereas incrementing cannot result in a trailing zero. Another difference is that decrementing the number zero yields zero. The next function returns the leftmost symbol~\textbf{1}, that is, the one that needs to be flipped. › definition first1 :: "symbol list ⇒ nat" where "first1 zs ≡ LEAST i. i < length zs ∧ zs ! i = 𝟭" lemma canonical_ex_3: assumes "canonical zs" and "zs ≠ []" shows "∃i<length zs. zs ! i = 𝟭" using assms canonical_def by (metis One_nat_def Suc_pred last_conv_nth length_greater_0_conv lessI) lemma canonical_first1: assumes "canonical zs" and "zs ≠ []" shows "first1 zs < length zs ∧ zs ! first1 zs = 𝟭" using assms canonical_ex_3 by (metis (mono_tags, lifting) LeastI first1_def) lemma canonical_first1_less: assumes "canonical zs" and "zs ≠ []" shows "∀i<first1 zs. zs ! i = 𝟬" proof - have "∀i<first1 zs. zs ! i ≠ 𝟭" using assms first1_def canonical_first1 not_less_Least by fastforce then show ?thesis using assms canonical_def by (meson canonical_first1 less_trans) qed text ‹ The next function describes how the canonical representation of the decremented symbol sequence looks like. It has special cases for the empty sequence and for sequences 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) 𝟭 else replicate (first1 zs) 𝟭 @ [𝟬] @ 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 then show ?thesis proof (cases) case 1 then show ?thesis using ndecr_def canonical_def by simp next case 2 then show ?thesis using canonical_def ndecr_def not_less_eq by fastforce next case 3 then have "Suc (first1 zs) < length zs" by auto then have "last (drop (Suc (first1 zs)) zs) = 𝟭" using assms canonical_def 3 by simp moreover have "bit_symbols (replicate (first1 zs) 𝟭 @ [𝟬] @ drop (Suc (first1 zs)) zs)" proof - have "bit_symbols (replicate (first1 zs) 𝟭)" by simp moreover have "bit_symbols [𝟬]" by simp moreover have "bit_symbols (drop (Suc (first1 zs)) zs)" using assms canonical_def by simp ultimately show ?thesis using bit_symbols_append by presburger qed ultimately show ?thesis using canonical_def ndecr_def 3 by 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