Theory Arithmetic

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 ::  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 ::  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 ::  where
"canrepr n  THE xs. num xs = n  canonical xs"

lemma canrepr_inj:
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:
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:
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]:
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]:
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
"nN  canrepr n"

lemma ncontents_0:
by (simp add: canrepr_0)

lemma clean_tape_ncontents: "clean_tape (xN, i)"
using bit_symbols_canrepr clean_contents_proper by fastforce

lemma ncontents_1_blank_iff_zero: "nN 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 ::  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)"
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 ::  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 = (n1N, 1)"
"tps ! j2 = (n2N, 1)"
"tps ! j3 = (bN, 1)"
assumes "ttt = (3 * nlength (min n1 n2) + 7)"
assumes "tps' = tps
[j3 := (if n1 = n2 then 1 else 0N, 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 "bN = []  bN = [𝟭]"
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 ::  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 = (xN, 1)"
and tps_j2 [simp]: "tps0 ! j2 = (yN, 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
using proper_symbols_canrepr by simp
qed

definition "tps2  tps0
[j1 := (xN, Suc (nlength x)),
j2 := (xN, 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 "(xN, 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 "(xN, 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 := (xN, 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 = (xN, 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 := (xN, 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 = (xN, 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 = (xN, 1)"
"tps ! j2 = (yN, 1)"
assumes "ttt = 14 + 3 * (nlength x + nlength y)"
assumes "tps' = tps
[j2 := (xN, 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 ::  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 = (xN, 1)"
assumes "t = 10 + 2 * nlength x + 2 * nlength n"
assumes "tps' = tps[j := (nN, 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 ::  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 ::  where "xs = replicate j 𝟭 @ [𝟬]"
define ys ::  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 ::  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 = (xN, 1)"
begin

lemma tm1 [transforms_intros]:
assumes "i0 = (LEAST i. i  nlength x  xN (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  xN (Suc i)  {, 𝟬}"
have 2: "i0  nlength x  xN (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  xN (Suc i)  {, 𝟬})"
and "ttt = Suc (Suc i0)"
and "tps' = tps[j := (Suc xN, 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  xN (Suc i)  {, 𝟬}"
have 1: "?P (nlength x)"
by simp
have 2: "i0  nlength x  xN (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  xN (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 (xN, Suc 0) 𝟬 i0 |:=| 𝟭]"
using jk assms(1) by simp
moreover have "(Suc xN, Suc i0) = constplant (xN, Suc 0) 2 i0 |:=| 𝟭"
(is "?l = ?r")
proof -
have "snd ?l = snd ?r"
by (simp add: transplant_def)
moreover have "Suc xN = fst ?r"
proof -
let ?zs = "canrepr x"
have l: "Suc xN = nincr ?zs"
by (simp add: nincr_canrepr)
have r: "fst ?r = (λi. if Suc 0  i  i < Suc i0 then 𝟬 else xN 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  xN (Suc (Least ?Q))  {, 𝟬}"
proof
show "Least ?Q  nlength x"
using True by (metis (mono_tags, lifting) LeastI_ex less_imp_le)
show "xN (Suc (Least ?Q))  {, 𝟬}"
using True by (simp add: Q1 Suc_leI)
qed
then show "y. y  nlength x  xN (Suc y)  {, 𝟬}  (Least ?Q)  y"
using True Q1 Q2 bit_symbols_canrepr contents_def
by (smt (z3) Least_le Suc_leI bot_nat_0.not_eq_extremum diff_Suc_1 insert_iff le_neq_implies_less
nat.simps(3) nlength_0_simp nlength_le_n nlength_less_n 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 xN 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 (smt (z3) Suc_leI append_Cons diff_Suc_1 fun_upd_apply le_trans length_replicate
nth_append_length zero_less_Suc)
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 = xN 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 xN i = fst (constplant (xN, 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  xN (Suc (nlength x))  {, 𝟬}"
by simp
show "y. y  nlength x  xN (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 xN 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 xN i = fst (constplant (xN, 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  xN (Suc i)  {, 𝟬})"
and "ttt = 5 + 2 * i0"
and "tps' = tps[j := (Suc xN, 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 xN, Suc (LEAST i. i  nlength x  xN (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 xN, Suc 0)]"
shows "transforms tm3 tps ttt tps'"
proof -
let ?P = "λi. i  nlength x  xN (Suc i)  {, 𝟬}"
define i0 where "i0 = Least ?P"
have "i0  nlength x  xN (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 = (xN, 1)"
and "ttt = 5 + 2 * nlength x"
and "tps' = tps[j := (Suc xN, 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 ::  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 = (xN, 1)"
and "ttt = c * (5 + 2 * nlength (x + c))"
and "tps' = tps[j := (x + cN, 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 + cN, 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 + cN, 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 ::  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 ::  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