Theory Karatsuba.Nat_LSBF

theory Nat_LSBF
  imports Main "../Preliminaries/Karatsuba_Sum_Lemmas" Abstract_Representations "HOL-Library.Log_Nat"
begin

section "Representing @{type nat} in LSBF"

text "In this theory, a representation of @{type nat} is chosen and simple algorithms implemented
thereon."

lemma list_isolate_nth: "i < length xs  xs1 xs2. xs = xs1 @ (xs ! i) # xs2  length xs1 = i"
  using id_take_nth_drop by fastforce

lemma list_is_replicate_iff: "xs = replicate (length xs) x  (i  {0..<length xs}. xs ! i = x)"
proof
  assume 1: "xs = replicate (length xs) x"
  show "i  {0..<length xs}. xs ! i = x"
    using 1 nth_replicate[of _ "length xs" x] by auto
next
  assume "i  {0..<length xs}. xs ! i = x"
  then have "i  {0..<length xs}. xs ! i = (replicate (length xs) x) ! i"
    using nth_replicate by auto
  then show "xs = replicate (length xs) x"
    using nth_equalityI[of xs "replicate (length xs) x"] by simp
qed

lemma list_is_replicate_iff2: "xs = replicate (length xs) x  set xs = {x}  xs = []"
  by (metis empty_replicate length_0_conv replicate_eqI set_replicate singleton_iff)

lemma set_bool_list: "set xs  {True, False}"
  by auto
lemma bool_list_is_replicate_if:
  assumes "a  set xs" shows "xs = replicate (length xs) (¬ a)"
proof (intro iffD2[OF list_is_replicate_iff2])
  from assms set_bool_list have "set xs  {¬ a}" by fastforce
  then have "set xs = {¬ a}  set xs = {}" by (meson subset_singletonD)
  then show "set xs = {¬ a}  xs = []" by simp
qed

lemma bit_strong_decomp_2: "ys zs. xs = ys @ a # zs  ys' n. xs = ys' @ a # (replicate n (¬ a))"
proof -
  assume "ys zs. xs = ys @ a # zs"
  then have "a  set xs" by auto
  from split_list_last[OF this] obtain ys zs where "xs = ys @ a # zs" "a  set zs" by blast
  from this(2) have "zs = replicate (length zs) (¬a)"
    by (intro bool_list_is_replicate_if)
  with xs = ys @ a # zs show ?thesis by blast
qed

lemma bit_strong_decomp_1: "ys zs. xs = ys @ a # zs  ys' n. xs = (replicate n (¬ a) @ a # ys')"
proof -
  assume "ys zs. xs = ys @ a # zs"
  then obtain ys zs where "xs = ys @ a # zs" by blast
  then have "rev xs = rev zs @ [a] @ rev ys" by simp
  then obtain n ys' where "rev xs = ys' @ [a] @ replicate n (¬ a)"
    using bit_strong_decomp_2[of "rev xs" a] by auto
  then have "xs = replicate n (¬ a) @ [a] @ rev ys'"
    by (metis append_assoc rev_append rev_replicate rev_rev_ident rev_singleton_conv)
  thus ?thesis by auto
qed

subsection "Type definition"

type_synonym nat_lsbf = "bool list"

subsection "Conversions"

fun eval_bool :: "bool  nat" where
"eval_bool True = 1"
| "eval_bool False = 0"

lemma eval_bool_is_of_bool[simp]: "eval_bool = of_bool"
  by auto

lemma eval_bool_leq_1: "eval_bool a  1"
  by (cases a) simp_all

lemma eval_bool_inj: "eval_bool a = eval_bool b  a = b"
  by (cases a; cases b) simp_all

fun to_nat :: "nat_lsbf  nat" where
"to_nat [] = 0"
| "to_nat (x#xs) = (eval_bool x) + 2 * to_nat xs"

fun from_nat :: "nat  nat_lsbf" where
"from_nat 0 = []"
| "from_nat x = (if x mod 2 = 0 then False else True)#(from_nat (x div 2))"

value "from_nat 103"
value "to_nat (from_nat 103)"

lemma to_nat_from_nat[simp]: "to_nat (from_nat x) = x"
proof (induction x rule: less_induct)
  case (less x)
  consider "x = 0" | "x > 0" by auto
  then show ?case
  proof (cases)
    case 1
    then show ?thesis by simp
  next
    case 2
    then have "to_nat (from_nat x) = eval_bool (if x mod 2 = 0 then False else True) + 2 * to_nat (from_nat (x div 2))"
      by (metis from_nat.elims nat_less_le to_nat.simps(2))
    also have "... = (x mod 2) + 2 * to_nat (from_nat (x div 2))"
      by simp
    also have "... = (x mod 2) + 2 * (x div 2)"
      using less 2 by simp
    also have "... = x" by simp
    finally show ?thesis .
  qed
qed

lemma to_nat_explicitly: "to_nat xs = (i  [0..<length xs]. eval_bool (xs ! i) * 2 ^ i)"
proof (induction xs rule: to_nat.induct)
  case 1
  then show ?case by simp
next
  case (2 x xs)
  let ?xs = "λi. eval_bool ((x # xs) ! i)"
  have "(i[0..<length (x # xs)]. ?xs i * 2 ^ i)
    = ?xs 0 + (i[1..<length (x # xs)]. ?xs i * 2 ^ i)"
    by (simp add: upt_rec)
  also have "... = ?xs 0 + (i[0..<length xs]. ?xs (i + 1) * 2 ^ (i + 1))"
    using list_sum_index_shift[of _ "length xs" 0 "λi. ?xs i * 2 ^ i"] by simp
  also have "... = ?xs 0 + 2 * (i[0..<length xs]. ?xs (i + 1) * 2 ^ i)"
    by (simp add: sum_list_const_mult mult.left_commute)
  also have "... = ?xs 0 + 2 * to_nat xs"
    using 2 by simp
  also have "... = to_nat (x # xs)" by simp
  finally show ?case by simp
qed

lemma to_nat_app: "to_nat (xs @ ys) = to_nat xs + (2 ^ length xs) * to_nat ys"
  by (induction xs) auto

lemma to_nat_length_upper_bound: "to_nat xs  2 ^ (length xs) - 1"
proof (induction xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then have "to_nat (a # xs) = eval_bool a + 2 * to_nat xs" by simp
  also have "...  eval_bool a + 2 * (2 ^ (length xs) - 1)" using Cons.IH by simp
  also have "...  1 + 2 * (2 ^ (length xs) - 1)" using eval_bool_leq_1[of a] by simp
  also have "... = 1 + (2 ^ (length xs + 1) - 1 - 1)" by simp
  also have "... = 2 ^ (length xs + 1) - 1"
    apply (intro add_diff_inverse_nat)
    using power_increasing[of 1 "length xs + 1" "2::nat"]
    by (simp add: add.commute)
  finally show ?case by simp
qed
lemma to_nat_length_bound: "to_nat xs < 2 ^ length xs"
  using to_nat_length_upper_bound[of xs]
  using le_eq_less_or_eq by fastforce
lemma to_nat_length_lower_bound: "to_nat (xs @ [True])  2 ^ length xs"
  by (induction xs) auto

lemma to_nat_replicate_false[simp]: "to_nat (replicate n False) = 0"
  by (induction n) simp_all

lemma to_nat_one_bit[simp]: "to_nat (replicate n False @ [True]) = 2 ^ n"
  by (simp add: to_nat_app)

lemma to_nat_replicate_true[simp]: "to_nat (replicate n True) = 2 ^ n - 1"
proof (induction n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  have "2 ^ (Suc n)  (2 :: nat)" by simp
  hence 1: "2 ^ (Suc n) - 1  (1 :: nat)" by linarith
  have "to_nat (replicate (Suc n) True) = 1 + 2 * to_nat (replicate n True)"
    by simp
  also have "... = 1 + 2 * (2 ^ n - 1)"
    using Suc.IH by simp
  also have "... = 2 ^ (Suc n) - 1"
    using le_add_diff_inverse[of 1 "2 ^ (Suc n) - 1"]
    using 1 by simp
  finally show ?case .
qed

lemma "to_nat xs = 0  (n. xs = replicate n False)"
proof
  show "to_nat xs = 0  n. xs = replicate n False"
  proof (induction xs)
    case Nil
    then show ?case by simp
  next
    case (Cons a xs)
    then have "a = False" "to_nat xs = 0" by auto
    then obtain n where "xs = replicate n False" using Cons.IH by auto
    hence "a # xs = replicate (Suc n) False" using a = False by simp
    then show ?case by blast
  qed
  show "n. xs = replicate n False  to_nat xs = 0"
    using to_nat_replicate_false by auto
qed

lemma to_nat_app_replicate[simp]: "to_nat (xs @ replicate n False) = to_nat xs"
  by (induction xs) auto

lemma change_bit_ineq: "length xs = length ys  to_nat (xs @ False # zs) < to_nat (ys @ True # zs)"
proof -
  assume "length xs = length ys"
  have "to_nat (xs @ False # zs) = to_nat xs + 2 ^ (length xs + 1) * to_nat zs"
    using to_nat_app_replicate[of xs 1] to_nat_app by simp
  also have "...  2 ^ (length xs) - 1 + 2 ^ (length xs + 1) * to_nat zs"
    using to_nat_length_upper_bound[of xs] by linarith
  also have "... < 2 ^ (length xs) + 2 ^ (length xs + 1) * to_nat zs" by simp
  also have "... = 2 ^ (length ys) + 2 ^ (length ys + 1) * to_nat zs"
    using length xs = length ys by simp
  also have "...  to_nat (ys @ [True]) + 2 ^ (length ys + 1) * to_nat zs"
    using to_nat_length_lower_bound[of ys] by simp
  also have "... = to_nat (ys @ True # zs)"
    using to_nat_app by simp
  finally show ?thesis .
qed

lemma to_nat_ineq_imp_False_bit: "to_nat xs < 2 ^ length xs - 1  ys zs. xs = ys @ False # zs"
proof (rule ccontr)
  assume "ys zs. xs = ys @ False # zs"
  then have "i{0..<length xs}. xs ! i = True"
    by (metis(full_types) atLeastLessThan_iff in_set_conv_decomp_first in_set_conv_nth)
  then have "xs = replicate (length xs) True" using list_is_replicate_iff by fast
  then have "to_nat xs = 2 ^ length xs - 1" using to_nat_replicate_true by metis
  thus "to_nat xs < 2 ^ length xs - 1  False" by simp
qed

lemma to_nat_bound_to_length_bound: "to_nat xs  2 ^ n  length xs  n + 1"
proof (rule ccontr)
  assume "to_nat xs  2 ^ n"
  assume "¬ n + 1  length xs"
  then have "n  length xs" by simp
  then have "to_nat xs  2 ^ length xs" using to_nat xs  2 ^ n
    using power_increasing le_trans one_le_numeral by meson
  then show False using to_nat_length_bound[of xs] by simp
qed

lemma to_nat_drop_take: "to_nat xs = to_nat (take k xs) + 2 ^ k * to_nat (drop k xs)"
proof -
  have "xs = take k xs @ drop k xs" by simp
  then have "to_nat xs = to_nat (take k xs) + 2 ^ (length (take k xs)) * to_nat (drop k xs)"
    using to_nat_app by metis
  also have "2 ^ (length (take k xs)) * to_nat (drop k xs) = 2 ^ k * to_nat (drop k xs)"
    by (cases "length xs < k") simp_all
  finally show ?thesis .
qed

lemma to_nat_take: "to_nat (take k xs) = to_nat xs mod 2 ^ k"
proof -
  have "to_nat xs = to_nat (take k xs) + 2 ^ k * to_nat (drop k xs)"
    by (simp add: to_nat_drop_take)
  then have "to_nat xs mod 2 ^ k = to_nat (take k xs) mod 2 ^ k" by simp
  moreover have "to_nat (take k xs) < 2 ^ k"
    using to_nat_length_bound[of "take k xs"] length_take[of k xs]
    by (metis add_leD1 leI min_absorb2 min_def to_nat_bound_to_length_bound)
  ultimately show ?thesis by simp
qed

lemma to_nat_drop: "to_nat (drop k xs) = to_nat xs div 2 ^ k"
proof -
  have "to_nat xs = to_nat xs mod 2 ^ k + 2 ^ k * to_nat (drop k xs)"
    using to_nat_drop_take[of xs k] to_nat_take[of k xs] by argo
  then have "to_nat xs div 2 ^ k = to_nat (drop k xs)"
    by (metis add.right_neutral bits_mod_div_trivial div_mult_self2 power_not_zero zero_neq_numeral)
  thus ?thesis by rule
qed

lemma to_nat_nth_True_bound:
  assumes "i < length xs"
  assumes "xs ! i = True"
  shows "to_nat xs  2 ^ i"
proof -
  from assms have "xs = (take i xs @ [True]) @ drop (Suc i) xs"
    using id_take_nth_drop by fastforce
  then show "to_nat xs  2 ^ i"
    using to_nat_app[of _ "drop (Suc i) xs"] to_nat_length_lower_bound[of "take i xs"] i < length xs
    by (metis append_eq_conv_conj le_add1 le_eq_less_or_eq list_isolate_nth trans_less_add1)
qed

subsection "Truncating and filling"

fun truncate_reversed :: "bool list  bool list" where
"truncate_reversed [] = []"
| "truncate_reversed (x#xs) = (if x then x#xs else truncate_reversed xs)"

definition truncate :: "nat_lsbf  nat_lsbf" where
"truncate xs = rev (truncate_reversed (rev xs))"

abbreviation truncated where "truncated x  truncate x = x"

lemma truncate_reversed_eqI[simp]: "xs = (replicate n False) @ ys  truncate_reversed xs = truncate_reversed ys"
  by (induction n arbitrary: xs ys) auto
corollary truncate_eqI[simp]: "xs = ys @ (replicate n False)  truncate xs = truncate ys"
  by (simp add: truncate_def)

lemma replicate_truncate_reversed: "n. (replicate n False) @ truncate_reversed xs = xs"
proof (induction xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then obtain n where 1: "replicate n False @ truncate_reversed xs = xs" by blast
  hence "a # xs = a # replicate n False @ truncate_reversed xs" by simp
  show ?case
  proof (cases a)
    case True
    then have "truncate_reversed (a # xs) = a # xs" by simp
    also have "... = replicate 0 False @ a # xs" by simp
    finally show ?thesis by simp
  next
    case False
    then have "truncate_reversed (a # xs) = truncate_reversed xs" by simp
    hence "replicate (Suc n) False @ truncate_reversed (a # xs) = False # replicate n False @ truncate_reversed xs"
      by simp
    with 1 False have "replicate (Suc n) False @ truncate_reversed (a # xs) = a # xs" by simp
    then show ?thesis by blast
  qed
qed
corollary truncate_replicate: "n. truncate xs @ (replicate n False) = xs"
proof -
  from replicate_truncate_reversed[of "rev xs"]
  obtain n where "replicate n False @ truncate_reversed (rev xs) = rev xs" by blast
  hence "rev (truncate_reversed (rev xs)) @ rev (replicate n False) = xs"
    using rev_append[symmetric, of "truncate_reversed (rev xs)" "replicate n False"]
    using rev_rev_ident[of xs]
    by simp
  hence "truncate xs @ replicate n False = xs" by (simp add: truncate_def)
  thus ?thesis by blast
qed
lemma decompose_trailing_zeros: "xs = truncate xs @ (replicate (length xs - length (truncate xs)) False)"
  using truncate_replicate[of xs]
  by (metis add_diff_cancel_left' length_append length_replicate)

lemma truncate_reversed_length_ineq: "length (truncate_reversed xs)  length xs"
  by (induction xs) simp_all
lemma truncate_length_ineq: "length (truncate xs)  length xs"
  by (metis Nat_LSBF.truncate_def length_rev truncate_reversed_length_ineq)

lemma truncate_reversed_fixed_point_iff: "truncate_reversed x = x  (x = []  hd x = True)"
proof (induction x)
  case Nil
  then show ?case by simp
next
  case (Cons a x)
  then have "(a # x = []  hd (a # x) = True) = a" by simp
  moreover have "a  truncate_reversed (a # x) = a # x" by simp
  moreover have "¬ a  truncate_reversed (a # x) = truncate_reversed x" by simp
  hence "¬ a  length (truncate_reversed (a # x))  length x"
    using truncate_reversed_length_ineq[of "x"] by simp
  hence "¬ a  truncate_reversed (a # x)  (a # x)"
    using neq_if_length_neq[of "a#x" x] by force
  ultimately show ?case by simp
qed

lemma truncated_iff: "truncated x  (x = []  last x = True)"
proof -
  have "truncated x  truncate_reversed (rev x) = rev x"
    by (simp add: truncate_def rev_swap)
  also have "...  rev x = []  hd (rev x) = True"
    using truncate_reversed_fixed_point_iff[of "rev x"] .
  also have "...  x = []  last x = True"
    by (simp add: hd_rev)
  finally show ?thesis .
qed

lemma hd_truncate_reversed: "truncate_reversed xs  []  hd (truncate_reversed xs) = True"
proof (induction xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  show ?case
  proof (rule ccontr)
    assume 1: "hd (truncate_reversed (a # xs))  True"
    then have "a = False" by auto
    with 1 have "hd (truncate_reversed xs)  True" by simp
    hence "truncate_reversed xs = []" using Cons.IH by blast
    hence "truncate_reversed (a # xs) = []" using a = False by simp
    thus "False" using Cons.prems by simp
  qed
qed

lemma last_truncate: "truncate xs  []  last (truncate xs) = True"
  using hd_truncate_reversed last_rev by (auto simp: truncate_def)

lemma truncate_truncate[simp]: "truncate (truncate xs) = truncate xs"
  using truncated_iff[of "truncate xs"] last_truncate by auto


lemma truncate_reversed_Nil_iff: "truncate_reversed xs = []  (n. xs = replicate n False)"
proof
  show "truncate_reversed xs = []  n. xs = replicate n False"
  proof (induction xs)
    case Nil
    then show ?case by simp
  next
    case (Cons a xs)
    then have "a = False" "truncate_reversed (a#xs) = truncate_reversed xs"
      by (auto split: if_splits)
    then obtain n where "xs = replicate n False" using Cons by auto
    hence "a # xs = replicate (Suc n) False" using a = False by simp
    thus ?case by blast
  qed
next
  show "n. xs = replicate n False  truncate_reversed xs = []"
  proof (induction xs)
    case Nil
    then show ?case by simp
  next
    case (Cons a xs)
    then show ?case
      by (metis Cons_replicate_eq truncate_reversed.simps(2))
  qed
qed

lemma truncate_Nil_iff: "truncate xs = []  (n. xs = replicate n False)"
  using truncate_reversed_Nil_iff[of "rev xs"]
  by (auto simp: truncate_def) (metis rev_replicate rev_rev_ident)

corollary truncate_neq_Nil: "truncate xs  []  ys zs. xs = ys @ True # zs"
  using truncate_Nil_iff[of xs]
  by (metis (full_types) hd_Cons_tl hd_truncate_reversed replicate_truncate_reversed truncate_reversed_Nil_iff)

lemma truncate_Cons: "truncate (a # xs) = (if ¬a  (truncate xs = []) then [] else a # truncate xs)"
proof (cases "truncate xs = []")
  case True
  then obtain n where "xs = replicate n False" using truncate_Nil_iff by blast
  then have "truncate (a # xs) = truncate [a]" by simp
  then show ?thesis using True by (simp add: truncate_def)
next
  case False
  then obtain ys n where "xs = ys @ True # (replicate n False)"
    using truncate_neq_Nil[of xs] bit_strong_decomp_2[of xs True] by auto
  then have "truncate xs = ys @ [True]" by (auto simp: truncate_def)
  moreover have "truncate (a # xs) = a # ys @ [True]"
    using xs = ys @ True # (replicate n False) by (auto simp: truncate_def)
  ultimately show ?thesis by simp
qed

lemma truncate_eq_Cons: "truncate xs = truncate ys  truncate (a # xs) = truncate (a # ys)"
  using truncate_Cons by simp

lemma truncate_as_take: "xs. n. truncate xs = take n xs"
  using truncate_replicate append_eq_conv_conj by blast

lemma to_nat_zero_iff: "to_nat xs = 0  truncate xs = []"
proof (induction xs)
  case Nil
  then show ?case by (simp add: truncate_def)
next
  case (Cons a xs)
  have "to_nat (a # xs) = 0  (eval_bool a = 0  to_nat xs = 0)" by simp
  also have "...  (a = False  to_nat xs = 0)" using eval_bool_inj[of a "False"] by auto
  also have "...  (a = False  truncate xs = [])" using Cons.IH by simp
  also have "...  (truncate (a # xs) = [])" using truncate_Cons by simp
  finally show ?case .
qed

lemma to_nat_eq_imp_truncate_eq: "to_nat xs = to_nat ys  truncate xs = truncate ys"
proof (induction xs arbitrary: ys)
  case Nil
  then show ?case using to_nat_zero_iff by (simp add: truncate_def)
next
  case (Cons a xs)
  show ?case
  proof (cases "ys = []")
    case True
    then have "to_nat ys = 0" by simp
    hence "to_nat (a # xs) = 0" using Cons.prems by simp
    with to_nat ys = 0 show "truncate (a # xs) = truncate ys"
      using to_nat_zero_iff[of "a # xs"] to_nat_zero_iff[of ys] by simp
  next
    case False
    then obtain b zs where "ys = b # zs" by (meson neq_Nil_conv)
    then have "to_nat (a # xs) = to_nat (b # zs)" using Cons.prems by simp
    then have 1: "eval_bool a + 2 * to_nat xs = eval_bool b + 2 * to_nat zs" by simp
    then have "eval_bool a = eval_bool b"
      by (metis add_cancel_right_left double_not_eq_Suc_double eval_bool.elims plus_1_eq_Suc)
    hence "a = b" using eval_bool_inj by simp
    from 1 have "to_nat xs = to_nat zs"
      using eval_bool a = eval_bool b by auto
    hence "truncate xs = truncate zs" using Cons.IH by simp
    hence "truncate (a # xs) = truncate (b # zs)" using a = b
      using truncate_eq_Cons[of xs zs a] by simp
    thus ?thesis using ys = b # zs by simp
  qed
qed

lemma truncate_from_nat[simp]: "truncate (from_nat x) = from_nat x"
  unfolding truncated_iff
  by (induction x rule: from_nat.induct) auto

lemma truncate_and_length_eq_imp_eq:
  assumes "truncate xs = truncate ys" "length xs = length ys"
  shows "xs = ys"
proof -
  obtain n where 1: "xs = truncate xs @ replicate n False"
    by (metis truncate_replicate)
  then have 2: "length xs = length (truncate xs) + n"
    by (metis length_append length_replicate)
  obtain m where 3: "ys = truncate ys @ replicate m False"
    by (metis truncate_replicate)
  then have "length ys = length (truncate ys) + m"
    by (metis length_append length_replicate)
  with 2 assms have "n = m" by simp
  with 1 3 assms show ?thesis by algebra
qed

lemma nat_lsbf_eqI:
  assumes "to_nat xs = to_nat ys"
  assumes "length xs = length ys"
  shows "xs = ys"
  using assms 
  using to_nat_eq_imp_truncate_eq truncate_and_length_eq_imp_eq by blast

interpretation nat_lsbf: abstract_representation from_nat to_nat truncate
proof
  show "to_nat  from_nat = id"
    using to_nat_from_nat comp_apply by fastforce
next
  show "from_nat  to_nat = truncate"
    using from_to_f_criterion[of to_nat from_nat truncate]
    using to_nat_from_nat truncate_from_nat to_nat_eq_imp_truncate_eq
    using comp_apply
    by fastforce
qed
    
lemma truncated_Cons_imp_truncated_tl: "truncated (x # xs)  truncated xs"
  using truncated_iff by fastforce

(* ensures that the number has at least n bits *)
definition fill where "fill n xs = xs @ replicate (n - length xs) False"

lemma to_nat_fill[simp]: "to_nat (fill n xs) = to_nat xs"
  by (simp add: fill_def)

lemma length_fill[intro]: "length xs  n  length (fill n xs) = n"
  by (simp add: fill_def)

lemma take_id: "length xs = k  take k xs = xs"
  by simp
lemma fill_id: "length xs  k  fill k xs = xs"
  unfolding fill_def by simp

lemma length_fill': "length (fill n xs) = max n (length xs)"
  by (simp add: fill_def)

lemma length_fill_max[simp]:
  "length (fill (max (length xs) (length ys)) xs) = max (length xs) (length ys)"
  "length (fill (max (length xs) (length ys)) ys) = max (length xs) (length ys)"
  by (intro length_fill, simp)+


lemma truncate_fill: "truncate (fill k xs) = truncate xs"
  by (simp add: fill_def)

lemma fill_truncate: "length xs  k  fill k (truncate xs) = fill k xs"
proof -
  assume "length xs  k"
  obtain n where n_def: "xs = truncate xs @ replicate n False"
    using truncate_replicate by metis
  then have "length xs = length (truncate xs) + n" by (metis length_append length_replicate)
  then have "length (truncate xs) + n  k" using length xs  k by simp
  from n_def have "fill k xs = (truncate xs @ replicate n False) @ replicate (k - length (truncate xs @ replicate n False)) False"
    using fill_def by presburger
  also have "... = truncate xs @ replicate (n + (k - length (truncate xs @ replicate n False))) False"
    by (simp add: replicate_add)
  also have "... = truncate xs @ replicate (n + (k - (length (truncate xs) + n))) False"
    by simp
  also have "... = truncate xs @ replicate (k - (length (truncate xs))) False"
    using length (truncate xs) + n  k by simp
  also have "... = fill k (truncate xs)" by (simp add: fill_def)
  finally show ?thesis by simp
qed
  
lemma fill_take_com: "fill k (take k xs) = take k (fill k xs)"
  using fill_def by fastforce

lemma to_nat_length_lower_bound_truncated: "xs  []  truncated xs  to_nat xs  2 ^ (length xs - 1)"
proof -
  assume "xs  []" "truncated xs"
  then obtain xs' where "xs = xs' @ [True]"
    by (metis(full_types) append_butlast_last_id last_truncate)
  then show ?thesis using to_nat_length_lower_bound[of xs'] by simp
qed

lemma to_nat_length_bound_truncated: "truncated xs  to_nat xs < 2 ^ n  length xs  n"
proof (rule ccontr)
  assume "truncated xs" "to_nat xs < 2 ^ n" "¬ length xs  n"
  show False
  proof (cases "xs = []")
    case True
    then show ?thesis using ¬ length xs  n by simp
  next
    case False
    have "length xs  n + 1" using ¬ length xs  n by simp
    then have "to_nat xs  2 ^ n"
      using to_nat_length_lower_bound_truncated[of xs]
      using False truncated xs
      by (meson add_le_imp_le_diff dual_order.trans one_le_numeral power_increasing)
    then show ?thesis using to_nat xs < 2 ^ n by simp
  qed
qed

subsection "Right-shifts"

definition shift_right :: "nat  nat_lsbf  nat_lsbf" where
  "shift_right n xs = (replicate n False) @ xs"

lemma to_nat_shift_right[simp]: "to_nat (shift_right n xs) = 2 ^ n * to_nat xs"
  unfolding shift_right_def using to_nat_app by simp

lemma length_shift_right[simp]: "length (shift_right n xs) = n + length xs"
  unfolding shift_right_def by simp

subsection "Subdividing lists"

subsubsection "Splitting a list in two blocks"

fun split_at :: "nat  'a list  'a list × 'a list" where
  "split_at m xs = (take m xs, drop m xs)"

definition split :: "nat_lsbf  nat_lsbf × nat_lsbf" where
  "split xs = (let n = length xs div (2::nat) in split_at n xs)"

lemma app_split: "split xs = (x0, x1)  xs = x0 @ x1"
  unfolding split_def Let_def using append_take_drop_id[of "length xs div 2" xs] by simp

lemma length_split: "length xs mod 2 = 0  split xs = (x0, x1)  length x0 = length xs div 2  length x1 = length xs div 2"
  unfolding split_def by fastforce

lemma length_split_le:
  assumes "split xs = (x0, x1)"
  shows "length x0  length xs" and "length x1  length xs"
  using app_split[OF assms] by simp_all

subsubsection "Splitting a list in multiple blocks"

text "@{term subdivide n xs} divides the list @{term xs} into blocks of size @{term n}."

fun subdivide :: "nat  'a list  'a list list" where
"subdivide 0 xs = undefined"
| "subdivide n [] = []"
| "subdivide n xs = take n xs # subdivide n (drop n xs)"

value "concat [[0..<2], [4..<7], [1..<5]]"

value "subdivide 2 [0..<6]"
value "subdivide 3 [0..<6]"
value "subdivide (2 ^ 2) [0..<2 ^ 6]"

lemma concat_subdivide: "n > 0  concat (subdivide n xs) = xs"
  by (induction n xs rule: subdivide.induct) simp_all

lemma subdivide_step:
  assumes "n > 0"
  assumes "xs  []"
  assumes "length xs = n * k"
  obtains ys zs where "xs = ys @ zs" "length ys = n" "length zs = n * (k - 1)"
    "subdivide n xs = ys # subdivide n zs"
proof -
  from assms obtain a xs' where "xs = a # xs'" using list.exhaust by blast
  from assms have "k > 0"
    using zero_less_iff_neq_zero by fastforce
  then obtain k' where "k = Suc k'" using gr0_implies_Suc by auto
  then have "length xs = n + n * k'" using assms(3) by simp
  define ys zs where "ys = take n xs" "zs = drop n xs"
  with length xs = n + n * k' have "xs = ys @ zs" "length ys = n" "length zs = n * k'" by simp_all
  moreover have "subdivide n xs = ys # subdivide n zs" using ys_zs_def assms(1) assms(2) Suc_diff_1 subdivide.simps(3)
    xs = a # xs' by metis
  ultimately show "(ys zs.
        xs = ys @ zs 
        length ys = n 
        length zs = n * (k - 1) 
        subdivide n xs = ys # subdivide n zs  thesis) 
    thesis"
    by (simp add: k = Suc k')
qed

lemma subdivide_step':
  assumes "n > 0"
  assumes "xs  []"
  shows "subdivide n xs = (take n xs) # subdivide n (drop n xs)"
  using assms
  by (cases n; cases xs; simp_all)

lemma subdivide_correct:
  assumes "n > 0"
  assumes "length xs = n * k"
  shows "length (subdivide n xs) = k  (x  set (subdivide n xs)  length x = n)"
  using assms
proof (induction k arbitrary: xs n x)
  case 0
  then have "subdivide n xs = []" using 0 gr0_conv_Suc by force
  then show ?case by simp
next
  case (Suc k)
  then have "xs  []" by force
  from subdivide_step[OF n > 0 this length xs = n * Suc k] obtain ys zs where ys_zs:
    "xs = ys @ zs"
    "length ys = n"
    "length zs = n * (Suc k - 1)"
    "subdivide n xs = ys # subdivide n zs"
    by blast
  then have "length zs = n * k" by simp
  note IH = Suc.IH[OF n > 0 this]
  from IH show ?case using ys_zs by simp
qed

lemma nth_nth_subdivide:
  assumes "n > 0"
  assumes "length xs = n * k"
  assumes "i < k" "j < n"
  shows "subdivide n xs ! i ! j = xs ! (i * n + j)"
  using assms
proof (induction k arbitrary: xs i)
  case 0
  then show ?case by simp
next
  case (Suc k)
  then have "xs  []" by auto
  with Suc subdivide_step obtain ys zs where "xs = ys @ zs" "length ys = n" "length zs = n * (Suc k - 1)"
    "subdivide n xs = ys # subdivide n zs" by blast
  then have "length zs = n * k" by simp
  show ?case
  proof (cases i)
    case 0
    then have "subdivide n xs ! i ! j = ys ! (i * n + j)" using subdivide n xs = ys # subdivide n zs by simp
    then show ?thesis using xs = ys @ zs 0 j < n length ys = n
      by (simp add: nth_append)
  next
    case (Suc i')
    then have "subdivide n xs ! i ! j = subdivide n zs ! i' ! j"
      using subdivide n xs = ys # subdivide n zs by simp
    also have "... = zs ! (i' * n + j)"
      apply (intro Suc.IH[of zs i'])
      subgoal using n > 0 .
      subgoal using length zs = n * k .
      subgoal using i < Suc k i = Suc i' by simp
      subgoal using j < n .
      done
    also have "... = xs ! (i * n + j)"
      using i = Suc i' xs = ys @ zs length ys = n
      by (metis ab_semigroup_add_class.add_ac(1) mult_Suc nth_append_length_plus)
    finally show ?thesis .
  qed
qed

lemma subdivide_concat:
  assumes "n > 0"
  assumes "i. i < length xs  length (xs ! i) = n"
  shows "subdivide n (concat xs) = xs"
proof (intro iffD1[OF concat_eq_concat_iff])
  show "concat (subdivide n (concat xs)) = concat xs"
    using concat_subdivide[OF n > 0] .
  have "map length xs = replicate (length xs) n"
    apply (intro replicate_eqI)
    subgoal by simp
    subgoal using assms by (metis in_set_conv_nth length_map nth_map)
    done
  then have "length (concat xs) = length xs * n"
    by (simp add: length_concat sum_list_replicate)
  then show "length (subdivide n (concat xs)) = length xs"
    apply (intro conjunct1[OF subdivide_correct] n > 0) by simp
  show "(x, y)set (zip (subdivide n (concat xs)) xs). length x = length y"
  proof
    fix z
    assume a: "z  set (zip (subdivide n (concat xs)) xs)"
    then obtain x y where "z = (x, y)" by fastforce
    from a obtain i where "i < length xs" "z = zip (subdivide n (concat xs)) xs ! i"
      using length (subdivide n (concat xs)) = length xs
      by (metis (no_types, lifting) gen_length_def in_set_conv_nth length_code length_zip min_0R min_add_distrib_left)
    then have "subdivide n (concat xs) ! i = x" "xs ! i = y"
      using z = (x, y) length (subdivide n (concat xs)) = length xs by simp_all
    then have "length x = n" using i < length xs length (subdivide n (concat xs)) = length xs
      using length (concat xs) = length xs * n
      n > 0 mult.commute[of n "length xs"]
      by (metis nth_mem subdivide_correct)
    moreover from xs ! i = y i < length xs have "length y = n" using assms by blast
    ultimately show "case z of (x, y)  length x = length y" using z = (x, y) by simp
  qed
qed

lemma to_nat_subdivide:
  assumes "n > 0"
  assumes "length xs = n * k"
  shows "to_nat xs = (i  [0..<k]. to_nat (subdivide n xs ! i) * 2 ^ (i * n))"
  using assms
proof (induction k arbitrary: xs)
  case 0
  then show ?case by simp
next
  case (Suc k)
  then have "length (take n xs) = n" "length (drop n xs) = n * k" by simp_all
  from Suc have "xs  []" by auto
  have "(i  [0..<Suc k]. to_nat (subdivide n xs ! i) * 2 ^ (i * n))
      = to_nat (subdivide n xs ! 0) * 2 ^ (0 * n) + (i  [1..<Suc k]. to_nat (subdivide n xs ! i) * 2 ^ (i * n))"
    by (intro sum_list_split_0)
  also have "subdivide n xs ! 0 = take n xs"
    using Suc xs  [] subdivide_step'[OF 0 < n xs  []] by simp
  also have "(i  [1..<Suc k]. to_nat (subdivide n xs ! i) * 2 ^ (i * n))
           = (i  [0..<k]. to_nat (subdivide n xs ! (i + 1)) * 2 ^ ((i + 1) * n))"
    using sum_list_index_shift[of "λi. to_nat (subdivide n xs ! i) * 2 ^ (i * n)" 1 0 k]
    by simp
  also have "... = (i  [0..<k]. to_nat (subdivide n (drop n xs) ! i) * 2 ^ ((i + 1) * n))"
    using subdivide_step'[OF 0 < n xs  []] by simp
  also have "... = (i  [0..<k]. (to_nat (subdivide n (drop n xs) ! i) * (2 ^ n * 2 ^ (i * n))))"
    by (simp add: power_add)
  also have "... = (i  [0..<k]. 2 ^ n * (to_nat (subdivide n (drop n xs) ! i) * 2 ^ (i * n)))"
    by (simp add: mult.left_commute)
  also have "... = 2 ^ n * (i  [0..<k]. to_nat (subdivide n (drop n xs) ! i) * 2 ^ (i * n))"
    by (simp add: sum_list_const_mult)
  also have "... = 2 ^ n * to_nat (drop n xs)"
    using Suc.IH[OF 0 < n length (drop n xs) = n * k] by argo
  finally have "(i  [0..<Suc k]. to_nat (subdivide n xs ! i) * 2 ^ (i * n))
    = to_nat (take n xs) + 2 ^ n * to_nat (drop n xs)"
    by simp
  also have "... = to_nat (take n xs @ drop n xs)"
    by (simp only: to_nat_app length (take n xs) = n)
  also have "... = to_nat xs" by simp
  finally show "to_nat xs = (i  [0..<Suc k]. to_nat (subdivide n xs ! i) * 2 ^ (i * n))"
    by simp
qed

subsection "The @{term bitsize} function"

text "@{term bitsize n} calculates how many bits are needed in the LSBF encoding of @{term n}."

fun bitsize :: "nat  nat" where
"bitsize 0 = 0"
| "bitsize n = 1 + bitsize (n div 2)"

lemma bitsize_is_floorlog: "bitsize = floorlog 2"
  apply (intro ext)
  subgoal for n
    apply (induction n rule: bitsize.induct)
    by (auto simp add: floorlog_eq_zero_iff compute_floorlog)
  done

corollary bitsize_bitlen: "int (bitsize n) = bitlen (int n)"
  unfolding bitsize_is_floorlog bitlen_def by simp

lemma bitsize_eq: "bitsize n = length (from_nat n)"
proof (induction n rule: less_induct)
  case (less n)
  then show ?case
  proof (cases "n = 0")
    case True
    then show ?thesis by simp
  next
    case False
    then have 1: "bitsize n = 1 + bitsize (n div 2)"
      by (metis bitsize.elims)
    from False have "length (from_nat n) = length ((if n mod 2 = 0 then False else True) # from_nat (n div 2))"
      by (metis from_nat.elims)
    also have "... = 1 + bitsize (n div 2)" using less[of "n div 2"] False by simp
    finally show "bitsize n = length (from_nat n)" using 1 by simp
  qed
qed

lemma bitsize_zero_iff: "bitsize n = 0  n = 0"
  by (simp add: bitsize_is_floorlog floorlog_eq_zero_iff)

lemma truncated_iff': "truncated x  length x = bitsize (to_nat x)"
proof
  assume "truncated x"
  then have "x = from_nat (to_nat x)" unfolding nat_lsbf.f_fixed_point_iff' .
  then show "length x = bitsize (to_nat x)" unfolding bitsize_eq by simp
next
  assume "length x = bitsize (to_nat x)"
  then have "length x = length (from_nat (to_nat x))" unfolding bitsize_eq .
  moreover have "to_nat x = to_nat (from_nat (to_nat x))" by simp
  ultimately show "truncated x" unfolding nat_lsbf.f_fixed_point_iff'
    by (intro nat_lsbf_eqI; argo)
qed

lemma bitsize_length: "bitsize n  k  n < 2 ^ k"
  unfolding bitsize_is_floorlog floorlog_le_iff by simp

lemma two_pow_bitsize_pos_bound: "n > 0  2 ^ bitsize n  2 * n"
proof -
  assume "n > 0"
  then have "2 ^ (bitsize n - 1)  n"
    using bitsize_length[of n "bitsize n - 1"] by fastforce
  then have "2 ^ (bitsize n - 1 + 1)  2 * n" by simp
  also have "bitsize n - 1 + 1 = bitsize n" using bitsize_zero_iff[of n] n > 0 by simp
  finally show ?thesis .
qed

lemma two_pow_bitsize_bound: "2 ^ bitsize n  2 * n + 1"
  using two_pow_bitsize_pos_bound[of n] by (cases n) simp_all

lemma bitsize_mono: "n1  n2  bitsize n1  bitsize n2"
  unfolding bitsize_is_floorlog by (rule floorlog_mono)

subsubsection "The @{term next_power_of_2} function"

lemma power_of_2_recursion: "(k. (n::nat) = 2 ^ k)  (n = 1  (n mod 2 = 0  (k. n div 2 = 2 ^ k)))"
proof
  assume "k. n = 2 ^ k"
  then obtain k where k_def: "n = 2 ^ k" by blast
  show "n = 1  (n mod 2 = 0  (k. n div 2 = 2 ^ k))"
    using k_def by (cases k) simp_all
next
  assume "n = 1  (n mod 2 = 0  (k. n div 2 = 2 ^ k))"
  then consider "n = 1" | "n mod 2 = 0  (k. n div 2 = 2 ^ k)" by argo
  then show "k. n = 2 ^ k"
  proof cases
    case 1
    then have "n = 2 ^ 0" by simp
    then show ?thesis by blast
  next
    case 2
    then obtain k where "n div 2 = 2 ^ k" by blast
    with 2 have "n = 2 ^ Suc k" by auto
    then show ?thesis by blast
  qed
qed

fun is_power_of_2 :: "nat  bool" where
"is_power_of_2 0 = False"
| "is_power_of_2 (Suc 0) = True"
| "is_power_of_2 n = ((n mod 2 = 0)  is_power_of_2 (n div 2))"

lemma is_power_of_2_correct: "is_power_of_2 n  (k. n = 2 ^ k)"
proof (induction n rule: is_power_of_2.induct)
  case 1
  then show ?case by simp
next
  case 2
  then show ?case by (metis is_power_of_2.simps(2) nat_power_eq_Suc_0_iff)
next
  case (3 va)
  let ?n = "Suc (Suc va)"
  have "is_power_of_2 ?n = ((?n mod 2 = 0)  is_power_of_2 (?n div 2))"
    by simp
  also have "... = ((?n mod 2 = 0)  (k. (?n div 2) = 2 ^ k))"
    using 3 by argo
  also have "... = (k. ?n = 2 ^ k)"
    using power_of_2_recursion[of ?n] by simp
  finally show ?case .
qed


fun next_power_of_2 :: "nat  nat" where
"next_power_of_2 n = (if is_power_of_2 n then n else 2 ^ (bitsize n))"

lemma next_power_of_2_lower_bound: "next_power_of_2 k  k"
  apply (cases "is_power_of_2 k")
  subgoal by simp
  subgoal premises prems
  proof -
    from prems have "next_power_of_2 k - 1 = 2 ^ bitsize k - 1" by simp
    also have "... = 2 ^ (length (from_nat k)) - 1" using bitsize_eq by simp
    also have "...  k" using to_nat_length_upper_bound[of "from_nat k"] by simp
    finally show ?thesis by simp
  qed
  done

lemma next_power_of_2_upper_bound:
  assumes "k  0"
  shows "next_power_of_2 k  2 * k"
  apply (cases "is_power_of_2 k")
  subgoal by simp
  subgoal premises prems
  proof -
    have "2 ^ (length (from_nat k) - 1)  to_nat (from_nat k)"
      apply (intro to_nat_length_lower_bound_truncated)
      subgoal using assms by (cases k; simp)
      subgoal by simp
      done
    then have "2 ^ length (from_nat k)  2 * to_nat (from_nat k)"
      using assms by (cases k; simp)
    also have "... = 2 * k" by simp
    also have "2 ^ length (from_nat k) = next_power_of_2 k"
      using prems bitsize_eq by simp
    finally show ?thesis .
  qed
  done

lemma next_power_of_2_upper_bound': "next_power_of_2 k  2 * k + 1"
  apply (cases k)
  subgoal by simp
  subgoal using next_power_of_2_upper_bound[of k] by simp
  done

lemma next_power_of_2_is_power_of_2: "k. next_power_of_2 n = 2 ^ k"
  using is_power_of_2_correct by simp

subsection "Addition"

(* second entry: carry bit *)
fun bit_add_carry :: "bool  bool  bool  bool × bool" where
"bit_add_carry False False False = (False, False)"
| "bit_add_carry False False True = (True, False)"
| "bit_add_carry False True False = (True, False)"
| "bit_add_carry False True True = (False, True)"
| "bit_add_carry True False False = (True, False)"
| "bit_add_carry True False True = (False, True)"
| "bit_add_carry True True False = (False, True)"
| "bit_add_carry True True True = (True, True)"

lemma bit_add_carry_correct: "bit_add_carry c x y = (a, b)  eval_bool c + eval_bool x + eval_bool y = eval_bool a + 2 * eval_bool b"
  by (cases c; cases x; cases y) auto

subsubsection "Increment operation"

(* increases a number by 1 *)
fun inc_nat :: "nat_lsbf  nat_lsbf" where
"inc_nat [] = [True]"
| "inc_nat (False # xs) = True # xs"
| "inc_nat (True # xs) = False # (inc_nat xs)"

lemma length_inc_nat': "length (inc_nat xs) = length xs + of_bool (to_nat xs + 1  2 ^ length xs)"
proof (induction xs rule: inc_nat.induct)
  case 1
  then show ?case by simp
next
  case (2 xs)
  then show ?case using to_nat_length_bound[of xs] by simp
next
  case (3 xs)
  then show ?case by simp
qed

lemma length_inc_nat_lower: "length (inc_nat xs)  length xs"
  unfolding length_inc_nat' by simp

lemma length_inc_nat_upper: "length (inc_nat xs)  length xs + 1"
  unfolding length_inc_nat' by simp

lemma inc_nat_nonempty: "inc_nat xs  []"
  by (induction xs rule: inc_nat.induct) simp_all

lemma inc_nat_replicate_True: "inc_nat (replicate m True) = replicate m False @ [True]"
  by (induction m) simp_all

lemma inc_nat_replicate_True_2: "inc_nat (replicate m True @ False # ys) = replicate m False @ True # ys"
  by (induction m) simp_all

lemma length_inc_nat_iff: "length (inc_nat xs) = length xs  (ys zs. xs = ys @ False # zs)"
proof (intro iffI, rule ccontr)
  assume "ys zs. xs = ys @ False # zs"
  then have "i  {0..<length xs}. xs!i = True"
    by (metis(full_types) atLeastLessThan_iff in_set_conv_nth split_list)
  then have "xs = replicate (length xs) True"
    by (simp only: list_is_replicate_iff)
  then show "length (inc_nat xs) = length xs  False"
    using inc_nat_replicate_True
    by (metis length_append_singleton length_replicate n_not_Suc_n)
next
  assume "ys zs. xs = ys @ False # zs"
  then have "n zs'. xs = replicate n True @ False # zs'"
    using bit_strong_decomp_1 by fastforce
  then show "length (inc_nat xs) = length xs"
    using inc_nat_replicate_True_2 by fastforce
qed

lemma inc_nat_last_bit_True: "length (inc_nat xs) = Suc (length xs)  zs. inc_nat xs = zs @ [True]"
  by (induction xs rule: inc_nat.induct) auto

lemma inc_nat_truncated: "truncated xs  truncated (inc_nat xs)"
proof (induction xs rule: inc_nat.induct)
  case 1
  then show ?case using truncate_def by simp
next
  case (2 xs)
  then show ?case by (simp add: truncated_iff)
next
  case (3 xs)
  then show ?case by (simp add: truncated_iff inc_nat_nonempty split: if_splits)
qed

lemma inc_nat_correct: "to_nat (inc_nat xs) = to_nat xs + 1"
  by (induction xs rule: inc_nat.induct) simp_all

lemma length_inc_nat: "length (inc_nat xs) = max (length xs) (floorlog 2 (to_nat xs + 1))"
proof (induction xs rule: inc_nat.induct)
  case 1
  then show ?case by (simp add: compute_floorlog)
next
  case (2 xs)
  then show ?case using to_nat_length_bound[of "False # xs"]
    by (simp add: floorlog_leI)
next
  case (3 xs)
  then have "length (inc_nat (True # xs)) = Suc (max (length xs) (floorlog 2 (Suc (to_nat xs))))"
    by simp
  also have "... = max (length (True # xs)) (Suc (floorlog 2 (Suc (to_nat xs))))"
    by simp
  also have "... = max (length (True # xs)) (floorlog 2 (2 * Suc (to_nat xs)))"
    apply (intro arg_cong2[where f = max] refl)
    by (simp add: compute_floorlog)
  finally show ?case by simp 
qed

subsubsection "Addition with a carry bit"

(* performs addition with a carry bit *)
fun add_carry :: "bool  nat_lsbf  nat_lsbf  nat_lsbf" where
"add_carry False [] y = y"
| "add_carry False x [] = x"
| "add_carry True [] y = inc_nat y"
| "add_carry True x [] = inc_nat x"
| "add_carry c (x#xs) (y#ys) = (let (a, b) = bit_add_carry c x y in a#(add_carry b xs ys))"

lemma add_carry_correct: "to_nat (add_carry c x y) = eval_bool c + to_nat x + to_nat y"
proof (induction c x y rule: add_carry.induct)
  case (1 y)
  then show ?case by simp
next
  case (2 v va)
  then show ?case by simp
next
  case (3 y)
  then show ?case using inc_nat_correct by simp
next
  case (4 v va)
  then show ?case using inc_nat_correct by simp
next
  case (5 c x xs y ys)
  define a b where "a = fst (bit_add_carry c x y)" "b = snd (bit_add_carry c x y)"
  then have "to_nat (add_carry c (x#xs) (y#ys)) = to_nat (a # add_carry b xs ys)"
    by (simp add: case_prod_beta' Let_def)
  also have "... = eval_bool a + 2 * to_nat (add_carry b xs ys)" by simp
  also have "... = eval_bool a + 2 * (eval_bool b + to_nat xs + to_nat ys)"
    using 5 a_b_def prod.collapse[of "bit_add_carry c x y"] by algebra
  also have "... = eval_bool c + eval_bool x + eval_bool y + 2 * (to_nat xs + to_nat ys)"
    using bit_add_carry_correct a_b_def by (simp add: prod_eq_iff)
  also have "... = eval_bool c + to_nat (x#xs) + to_nat (y#ys)" by simp
  finally show ?case .
qed

lemma length_add_carry': "length (add_carry c xs ys) = max (length xs) (length ys) + of_bool (to_nat xs + to_nat ys + of_bool c  2 ^ max (length xs) (length ys))"
proof (induction c xs ys rule: add_carry.induct)
  case (1 y)
  then show ?case using to_nat_length_bound[of y] by simp
next
  case (2 v va)
  then show ?case
    using to_nat_length_bound[of va] by simp
next
  case (3 y)
  then show ?case by (simp add: length_inc_nat')
next
  case (4 v va)
  then show ?case by (simp add: length_inc_nat')
next
  case (5 c x xs y ys)

  have l: "2 ^ Suc a  2 * b + 1  2 ^ Suc a  2 * b" for a b :: nat
    by fastforce

  obtain a b where "bit_add_carry c x y = (a, b)" by fastforce
  then have "add_carry c (x # xs) (y # ys) = a # (add_carry b xs ys)" by simp
  then have "length (add_carry c (x # xs) (y # ys)) = 1 + max (length xs) (length ys) + of_bool (2 ^ max (length xs) (length ys)  to_nat xs + to_nat ys + of_bool b)"
    using "5.IH"[OF bit_add_carry c x y = (a, b)[symmetric] refl] by (simp only: length_Cons)
  also have "... = max (length (x # xs)) (length (y # ys)) + of_bool (2 ^ max (length xs) (length ys)  to_nat xs + to_nat ys + of_bool b)"
    by simp
  also have "... = max (length (x # xs)) (length (y # ys)) + of_bool (2 ^ max (length (x # xs)) (length (y # ys))  to_nat (x # xs) + to_nat (y # ys) + of_bool c)"
  proof (intro arg_cong2[where f = "(+)"] refl arg_cong[where f = of_bool])
    have "to_nat (x # xs) + to_nat (y # ys) + of_bool c =
        2 * to_nat xs + 2 * to_nat ys + of_bool x + of_bool y + of_bool c"
      by simp
    also have "... = 2 * to_nat xs + 2 * to_nat ys + of_bool a + 2 * of_bool b"
      using bit_add_carry_correct[OF bit_add_carry c x y = (a, b)] by simp
    finally have r: "to_nat (x # xs) + to_nat (y # ys) + of_bool c = ..." .
    show "(2 ^ max (length xs) (length ys)  to_nat xs + to_nat ys + of_bool b) =
    (2 ^ max (length (x # xs)) (length (y # ys))  to_nat (x # xs) + to_nat (y # ys) + of_bool c)"
      unfolding r using l[of "max (length xs) (length ys)" "to_nat xs + to_nat ys + of_bool b"]
      by auto
  qed
  finally show ?case .
qed

lemma length_add_carry: "length (add_carry c xs ys) = max (max (length xs) (length ys)) (floorlog 2 (of_bool c + to_nat xs + to_nat ys))"
proof (induction c xs ys rule: add_carry.induct)
  case (1 y)
  then show ?case using to_nat_length_bound[of y]
    by (simp add: floorlog_leI)
next
  case (2 v va)
  then show ?case using to_nat_length_bound[of "v # va"]
    by (simp add: floorlog_leI)
next
  case (3 y)
  then show ?case by (simp add: length_inc_nat)
next
  case (4 v va)
  then show ?case by (simp add: length_inc_nat)
next
  case (5 c x xs y ys)
  obtain a b where "bit_add_carry c x y = (a, b)" by fastforce
  then have "add_carry c (x # xs) (y # ys) = a # (add_carry b xs ys)" by simp
  then have "length (add_carry c (x # xs) (y # ys)) = Suc (max (max (length xs) (length ys)) (floorlog 2 (of_bool b + to_nat xs + to_nat ys)))"
    using 5 bit_add_carry c x y = (a, b) by (simp only: length_Cons)
  also have "... = max (max (length (x # xs)) (length (y # ys))) (1 + floorlog 2 (of_bool b + to_nat xs + to_nat ys))"
    by simp
  also have "... = max (max (length (x # xs)) (length (y # ys))) (floorlog 2 (of_bool c + to_nat (x # xs) + to_nat (y # ys)))"
  proof (cases "of_bool a + 2 * (of_bool b + to_nat xs + to_nat ys) > 0")
    case True
    then show ?thesis
    proof (intro arg_cong2[where f = max] refl)
      have "floorlog 2 (of_bool c + to_nat (x # xs) + to_nat (y # ys)) =
          floorlog 2 ((of_bool c + of_bool x + of_bool y) + 2 * (to_nat xs + to_nat ys))"
        by simp
      also have "... = floorlog 2 ((of_bool a + 2 * of_bool b) + 2 * (to_nat xs + to_nat ys))"
        using bit_add_carry_correct[OF bit_add_carry c x y = (a, b)] by simp
      also have "... = floorlog 2 (of_bool a + 2 * (of_bool b + to_nat xs + to_nat ys))"
        by simp
      also have "... = 1 + floorlog 2 (of_bool b + to_nat xs + to_nat ys)"
        using compute_floorlog[of 2 "of_bool a + 2 * (of_bool b + to_nat xs + to_nat ys)"] True
        by simp
      finally show "... = floorlog 2 (of_bool c + to_nat (x # xs) + to_nat (y # ys))" by simp
    qed
  next
    case False
    then have 01: "of_bool a = 0" "of_bool b = 0" "to_nat xs = 0" "to_nat ys = 0" by simp_all
    then have 02: "of_bool c = 0" "of_bool x = 0" "of_bool y = 0"
      using bit_add_carry_correct[OF bit_add_carry c x y = (a, b)] by simp_all
    from 01 02 show ?thesis by (simp add: floorlog_def)
  qed
  finally show ?case .
qed

lemma length_add_carry_lower: "length (add_carry c xs ys)  max (length xs) (length ys)"
  unfolding length_add_carry' by simp

lemma length_add_carry_upper: "length (add_carry c xs ys)  max (length xs) (length ys) + 1"
  unfolding length_add_carry' by simp

lemma add_carry_last_bit_True: "length (add_carry c xs ys) = max (length xs) (length ys) + 1  zs. add_carry c xs ys = zs @ [True]"
proof (induction c xs ys rule: add_carry.induct)
  case (1 y)
  then show ?case by simp
next
  case (2 v va)
  then show ?case by simp
next
  case (3 y)
  then show ?case by (simp add: inc_nat_last_bit_True)
next
  case (4 v va)
  then show ?case by (simp add: inc_nat_last_bit_True)
next
  case (5 c x xs y ys)
  obtain a b where "bit_add_carry c x y = (a, b)" by fastforce
  then have 1: "add_carry c (x # xs) (y # ys) = a # (add_carry b xs ys)"
    by simp
  from 5 have "length (add_carry b xs ys) = max (length (x # xs)) (length (y # ys))"
    using bit_add_carry c x y = (a, b) by auto
  also have "... = max (length xs) (length ys) + 1" by simp
  finally obtain zs where "add_carry b xs ys = zs @ [True]" using 5 bit_add_carry c x y = (a, b)
    by presburger
  then show ?case using 1 by simp
qed

(* Note that this is even stronger than the commutative law obtained by the correctness of
add_carry, since it even holds for non-truncated inputs *)
lemma add_carry_com: "add_carry c xs ys = add_carry c ys xs"
  apply (intro nat_lsbf_eqI)
  subgoal by (simp add: add_carry_correct)
  subgoal by (simp only: length_add_carry' max.commute add.commute)
  done

lemma add_carry_rNil[simp]: "add_carry True y [] = inc_nat y"
  by (cases y; simp)
lemma add_carry_rNil_nocarry[simp]: "add_carry False y [] = y"
  by (cases y; simp)

lemma add_carry_True_inc_nat:
"add_carry True xs ys = inc_nat (add_carry False xs ys) 
 add_carry True xs ys = add_carry False (inc_nat xs) ys 
 add_carry True xs ys = add_carry False xs (inc_nat ys)"
proof (induction xs arbitrary: ys)
  case Nil
  then show ?case
    apply (intro conjI)
    subgoal by simp
    subgoal
      apply (cases ys)
      subgoal by simp
      subgoal for a ys'
        by (cases a) simp_all
      done
    subgoal by simp
    done
next
  case (Cons a xs)
  then show ?case
    apply (cases a; cases ys)
    subgoal by simp
    subgoal for b ys'
      apply (cases b)
      subgoal by fastforce
      subgoal by simp
      done
    subgoal by (simp add: add_carry_com)
    subgoal for b ys'
      apply (cases b)
      subgoal by fastforce
      subgoal by simp
      done
    done
qed

lemma inc_nat_add_carry:
  "inc_nat (add_carry c xs ys) = add_carry c (inc_nat xs) ys 
   inc_nat (add_carry c xs ys) = add_carry c xs (inc_nat ys)"
proof (cases c)
  case True
  then have
    "add_carry c (inc_nat xs) ys = inc_nat (add_carry False (inc_nat xs) ys)"
    "add_carry c xs (inc_nat ys) = inc_nat (add_carry False xs (inc_nat ys))"
    using add_carry_True_inc_nat by simp_all
  moreover have
    "add_carry False (inc_nat xs) ys = inc_nat (add_carry False xs ys)"
    using add_carry_True_inc_nat[of xs ys] by argo
  moreover have "add_carry False xs (inc_nat ys) = inc_nat (add_carry False xs ys)"
    using add_carry_True_inc_nat[of xs ys] by argo
  ultimately show ?thesis using add_carry_True_inc_nat True by simp
next
  case False
  then show ?thesis using add_carry_True_inc_nat[of xs ys] by auto
qed

lemma add_carry_inc_nat_simps:
  "add_carry True xs ys = inc_nat (add_carry False xs ys)"
  "add_carry False (inc_nat xs) ys = inc_nat (add_carry False xs ys)"
  "add_carry False xs (inc_nat ys) = inc_nat (add_carry False xs ys)"
  using inc_nat_add_carry[of _ xs ys] add_carry_True_inc_nat[of xs ys]
  by argo+

lemma add_carry_assoc: "add_carry c2 (add_carry c1 xs ys) zs = add_carry c1 xs (add_carry c2 ys zs)"
  apply (intro nat_lsbf_eqI)
  subgoal by (simp add: add_carry_correct)
  subgoal
  proof -
    let ?t1 = "of_bool c1 + to_nat xs + to_nat ys"
    let ?t2 = "of_bool c2 + to_nat ys + to_nat zs"
    let ?t3 = "of_bool c1 + of_bool c2 + to_nat xs + to_nat ys + to_nat zs"

    have "length (add_carry c2 (add_carry c1 xs ys) zs) = max (max (max (max (length xs) (length ys)) (floorlog 2 ?t1)) (length zs))
     (floorlog 2 ?t3)"
      unfolding length_add_carry add_carry_correct eval_bool_is_of_bool
      by (intro arg_cong2[where f = max] refl arg_cong2[where f = floorlog]) simp
    also have "... = max (max (max (max (floorlog 2 ?t1) (floorlog 2 ?t3)) (length xs)) (length ys)) (length zs)"
      using max.commute max.assoc by presburger
    also have "... = max (max (max (floorlog 2 ?t3) (length xs)) (length ys)) (length zs)" (is "... = ?t4")
      by (intro arg_cong2[where f = max] refl max.absorb2 floorlog_mono) simp
    finally have 1: "length (add_carry c2 (add_carry c1 xs ys) zs) = ?t4" .

    have "length (add_carry c1 xs (add_carry c2 ys zs)) = max (max (length xs) (max (max (length ys) (length zs)) (floorlog 2 ?t2)))
     (floorlog 2 ?t3)"
      unfolding length_add_carry add_carry_correct eval_bool_is_of_bool
      by (intro arg_cong2[where f = max] refl arg_cong2[where f = floorlog]) simp
    also have "... = max (max (max (max (floorlog 2 ?t2) (floorlog 2 ?t3)) (length xs)) (length ys)) (length zs)"
      using max.commute max.assoc by presburger
    also have "... = max (max (max (floorlog 2 ?t3) (length xs)) (length ys)) (length zs)"
      by (intro arg_cong2[where f = max] refl max.absorb2 floorlog_mono) simp
    finally have 2: "length (add_carry c1 xs (add_carry c2 ys zs)) = ?t4" .

    show ?thesis unfolding 1 2 by (rule refl)
  qed
  done

lemma truncated_add_carry:
  assumes "truncated xs" "truncated ys"
  shows "truncated (add_carry c xs ys)"
proof -
  have "length (add_carry c xs ys) =
      max (max (length xs) (length ys)) (bitsize (of_bool c + to_nat xs + to_nat ys))"
    unfolding length_add_carry bitsize_is_floorlog by argo
  also have "... = max (max (bitsize (to_nat xs)) (bitsize (to_nat ys))) (bitsize (of_bool c + to_nat xs + to_nat ys))"
    using truncated_iff' assms by algebra
  also have "... = bitsize (of_bool c + to_nat xs + to_nat ys)"
    using bitsize_mono by simp
  also have "... = bitsize (to_nat (add_carry c xs ys))"
    by (simp add: add_carry_correct)
  finally show ?thesis unfolding truncated_iff' .
qed

subsubsection "Addition"

definition add_nat :: "nat_lsbf  nat_lsbf  nat_lsbf" where
"add_nat x y = add_carry False x y"

corollary length_add_nat_lower: "length (add_nat xs ys)  max (length xs) (length ys)"
  unfolding add_nat_def by (simp only: length_add_carry_lower)

corollary length_add_nat_upper: "length (add_nat xs ys)  max (length xs) (length ys) + 1"
  unfolding add_nat_def using length_add_carry_upper[of False xs ys] by simp

corollary add_nat_last_bit_True: "length (add_nat xs ys) = max (length xs) (length ys) + 1  zs. add_nat xs ys = zs @ [True]"
  unfolding add_nat_def by (simp add: add_carry_last_bit_True)

lemma add_nat_correct: "to_nat (add_nat x y) = to_nat x + to_nat y"
  unfolding add_nat_def using add_carry_correct by simp

corollary add_nat_com: "add_nat xs ys = add_nat ys xs"
  unfolding add_nat_def by (simp add: add_carry_com)

corollary add_nat_assoc: "add_nat xs (add_nat ys zs) = add_nat (add_nat xs ys) zs"
  unfolding add_nat_def using add_carry_assoc by simp

corollary truncated_add_nat:
  assumes "truncated xs" "truncated ys"
  shows "truncated (add_nat xs ys)"
  unfolding add_nat_def
  by (intro truncated_add_carry assms)

subsection "Comparison and subtraction"

subsubsection "Comparison"

fun compare_nat_same_length_reversed :: "bool list  bool list  bool" where
"compare_nat_same_length_reversed [] [] = True"
| "compare_nat_same_length_reversed (False#xs) (False#ys) = compare_nat_same_length_reversed xs ys"
| "compare_nat_same_length_reversed (True#xs) (False#ys) = False"
| "compare_nat_same_length_reversed (False#xs) (True#ys) = True"
| "compare_nat_same_length_reversed (True#xs) (True#ys) = compare_nat_same_length_reversed xs ys"
| "compare_nat_same_length_reversed _ _ = undefined"

lemma compare_nat_same_length_reversed_correct:
  "length xs = length ys  compare_nat_same_length_reversed xs ys  to_nat (rev xs)  to_nat (rev ys)"
proof (induction xs ys rule: compare_nat_same_length_reversed.induct)
  case 1
  then show ?case by simp
next
  case (2 xs ys)
  have "to_nat (rev (False # xs)) = to_nat (rev xs)" "to_nat (rev (False # ys)) = to_nat (rev ys)"
    using to_nat_app by simp_all
  then have "to_nat (rev (False # xs))  to_nat (rev (False # ys))  to_nat (rev xs)  to_nat (rev ys)"
    by simp
  then show ?case using 2 by simp
next
  case (3 xs ys)
  have "to_nat (rev (True # xs)) = 2 ^ (length xs) + to_nat (rev xs)"
    using to_nat_app by simp
  also have "... > to_nat (rev ys)"
    using 3 to_nat_length_upper_bound[of "rev ys"] leI le_add_diff_inverse2 by fastforce
  also have "to_nat (rev ys) = to_nat (rev (False # ys))"
    using to_nat_app by simp
  finally have "to_nat (rev (True # xs)) > to_nat (rev (False # ys))" .
  thus ?case using 3 by simp
next
  case (4 xs ys)
  have "to_nat (rev (False # xs)) = to_nat (rev xs)"
    using to_nat_app by simp
  also have "...  2 ^ (length xs)"
    using to_nat_length_upper_bound[of "rev xs"] by simp
  also have "...  to_nat (rev (True # ys))"
    using to_nat_app 4 by simp
  finally have "to_nat (rev (False # xs))  to_nat (rev (True # ys))" .
  thus ?case using 4 by simp
next
  case (5 xs ys)
  have "to_nat (rev (True # xs)) = 2 ^ (length xs) + to_nat (rev xs)" "to_nat (rev (True # ys)) = 2 ^ (length ys) + to_nat (rev ys)"
    using to_nat_app by simp_all
  then have "to_nat (rev (True # xs))  to_nat (rev (True # ys))  to_nat (rev xs)  to_nat (rev ys)"
    using 5 by simp
  then show ?case using 5 by simp
next
  case ("6_1" va)
  then show ?case by simp
next
  case ("6_2" v va)
  then show ?case by simp
next
  case ("6_3" v va)
  then show ?case by simp
next
  case ("6_4" va)
  then show ?case by simp
qed

fun compare_nat_same_length :: "nat_lsbf  nat_lsbf  bool" where
"compare_nat_same_length xs ys = compare_nat_same_length_reversed (rev xs) (rev ys)"

lemma compare_nat_same_length_correct:
  "length xs = length ys  compare_nat_same_length xs ys = (to_nat xs  to_nat ys)"
  using compare_nat_same_length_reversed_correct by simp

definition make_same_length :: "nat_lsbf  nat_lsbf  nat_lsbf × nat_lsbf" where
"make_same_length xs ys = (let n = max (length xs) (length ys) in ((fill n xs), (fill n ys)))"

lemma make_same_length_correct:
  assumes "(fill_xs, fill_ys) = make_same_length xs ys"
  shows "length fill_ys = length fill_xs"
  "length fill_xs = max (length xs) (length ys)"
  "to_nat fill_xs = to_nat xs"
  "to_nat fill_ys = to_nat ys"
  using assms by (simp_all add: Let_def make_same_length_def)

definition compare_nat :: "nat_lsbf  nat_lsbf  bool" where
"compare_nat xs ys = (let (fill_xs, fill_ys) = make_same_length xs ys in compare_nat_same_length fill_xs fill_ys)"

lemma compare_nat_correct: "compare_nat xs ys = (to_nat xs  to_nat ys)"
proof -
  obtain fill_xs fill_ys where fills_def: "make_same_length xs ys = (fill_xs, fill_ys)"
    by fastforce
  then show ?thesis unfolding compare_nat_def Let_def
    using make_same_length_correct[OF fills_def[symmetric]]
    using compare_nat_same_length_reversed_correct[of "rev fill_xs" "rev fill_ys"]
    by simp
qed

subsubsection "Subtraction"

definition subtract_nat :: "nat_lsbf  nat_lsbf  nat_lsbf" where
  "subtract_nat xs ys = (if compare_nat xs ys then [] else
    let (fill_xs, fill_ys) = make_same_length xs ys in
    butlast (add_carry True fill_xs (map Not fill_ys)))"

lemma add_complement: "add_nat xs (map Not xs) = replicate (length xs) True"
proof (induction xs)
  case Nil
  then show ?case unfolding add_nat_def by simp
next
  case (Cons a xs)
  have "add_nat (a # xs) (map Not (a # xs)) = True # (add_carry False xs (map Not xs))"
    unfolding add_nat_def by (cases a) simp_all
  also have "... = True # (replicate (length xs) True)"
    using Cons.IH by (simp add: add_nat_def)
  finally show ?case by simp
qed

lemma to_nat_complement: "to_nat (map Not xs) = 2 ^ (length xs) - 1 - to_nat xs"
  using add_complement[of xs] to_nat_replicate_true[of "length xs"] add_nat_correct[of xs "map Not xs"]
  by simp

lemma to_nat_butlast: "zs = xs @ [True]  to_nat (butlast zs) = to_nat zs - 2 ^ length xs"
  using to_nat_app[of xs "[True]"] by simp

lemma inc_nat_true_prefix[simp]: "inc_nat (replicate n True @ [False] @ ys) = replicate n False @ [True] @ ys"
  by (induction n arbitrary: ys) simp_all

lemma length_inc_nat_aux: "zs = replicate n True @ [False] @ ys  length (inc_nat zs) = length zs"
  using inc_nat_true_prefix[of n ys] by simp

lemma length_inc_nat_aux_2: "length (inc_nat (xs @ [False] @ ys)) = length (xs @ [False] @ ys)"
proof -
  define zs where "zs = xs @ [False] @ ys"
  with bit_strong_decomp_1[of zs False] obtain ys' n where "zs = replicate n True @ [False] @ ys'"
    by auto
  then show ?thesis using length_inc_nat_aux zs_def by simp
qed

lemma subtract_nat_aux: "to_nat (subtract_nat xs ys) = (to_nat xs) - (to_nat ys)  length (subtract_nat xs ys)  max (length xs) (length ys)"
proof (cases "compare_nat xs ys")
  case True
  then show ?thesis using compare_nat_correct unfolding subtract_nat_def by simp
next
  case False

  obtain fill_xs fill_ys where fills_def: "make_same_length xs ys = (fill_xs, fill_ys)"
    by fastforce
  note fills_props = make_same_length_correct[OF fills_def[symmetric]]
  define n where "n = max (length xs) (length ys)"
  then have "length fill_xs = n" "length fill_ys = n" using fills_props by auto

  from False have "to_nat fill_xs > to_nat fill_ys"
    using fills_props compare_nat_correct by simp
  then have "n > 0" using length fill_xs = n by auto

  let ?add = "add_carry True fill_xs (map Not fill_ys)"

  have subtract_nat_xs_ys: "subtract_nat xs ys = butlast ?add"
    unfolding subtract_nat_def using False fills_def by simp

  have "to_nat fill_ys  2 ^ n - 1" "to_nat fill_xs  2 ^ n - 1" "to_nat (map Not fill_ys)  2 ^ n - 1"
    subgoal using to_nat_length_upper_bound[of fill_ys] length fill_ys = n by argo
    subgoal using to_nat_length_upper_bound[of fill_xs] length fill_xs = n by argo
    subgoal using to_nat_length_upper_bound[of "map Not fill_ys"] length fill_ys = n by simp
    done
  then have "to_nat ?add  (2 ^ n - 1) + (2 ^ n - 1) + 1" unfolding add_carry_correct by simp
  also have "... = 2 ^ (n + 1) - 2 + 1" by simp
  also have "... = 2 ^ (n + 1) - 1"
    using Nat.diff_diff_right[of 1 2 "2 ^ (n + 1)"] Nat.diff_add_assoc2[of 2 "2 ^ (n + 1)" 1]
    by simp
  finally have "to_nat ?add  ..." .

  from to_nat fill_xs > to_nat fill_ys have "to_nat fill_xs  to_nat fill_ys + 1" by simp
  then have "to_nat fill_xs + 2 ^ n  2 ^ n + to_nat fill_ys + 1" by simp
  then have "to_nat fill_xs + (2 ^ n - 1 - to_nat fill_ys)  2 ^ n" by simp
  then have "to_nat fill_xs + to_nat (map Not fill_ys)  2 ^ n"
    using to_nat_complement[of fill_ys] length fill_ys = n by simp
  then have "to_nat ?add  2 ^ n"
    using add_carry_correct fills_props by simp
  then have "length ?add  n + 1"
    using to_nat_bound_to_length_bound by simp
  then have "length ?add = n + 1"
    using length_add_carry_upper[of True fill_xs "map Not fill_ys"] length fill_xs = n length fill_ys = n
    by simp

  then obtain zs where "?add = zs @ [True]" "length zs = n"
    using add_carry_last_bit_True[of True fill_xs "map Not fill_ys"] length fill_xs = n length fill_ys = n
    by auto
  then have 1: "to_nat (butlast ?add) = to_nat fill_xs + to_nat (map Not fill_ys) + 1 - 2 ^ n"
    unfolding to_nat_butlast[OF ?add = zs @ [True]]
    using add_carry_correct by (metis Suc_eq_plus1 add.assoc eval_bool.simps(1) plus_1_eq_Suc)
  also have "... = to_nat fill_xs + (2 ^ n - 1 - to_nat fill_ys) + 1 - 2 ^ n"
    unfolding to_nat_complement[of fill_ys] length fill_ys = n by (rule refl)
  also have "... = to_nat fill_xs + (2 ^ n - 1) - to_nat fill_ys + 1 - 2 ^ n"
    using le_add_diff_inverse[OF to_nat fill_ys  2 ^ n - 1] by linarith
  also have "... = to_nat fill_xs - to_nat fill_ys + (2 ^ n - 1) - (2 ^ n - 1)"
    using to_nat fill_xs > to_nat fill_ys by simp
  also have "... = to_nat fill_xs - to_nat fill_ys" by simp
  finally have 2: "to_nat (subtract_nat xs ys) = to_nat xs - to_nat ys"
    unfolding subtract_nat_xs_ys fills_props .

  have 3: "length (butlast ?add) = n"
    using length ?add = n + 1 by simp

  show ?thesis
    apply (intro conjI)
    subgoal by (fact 2)
    subgoal using 3 unfolding subtract_nat_xs_ys n_def[symmetric] by simp
    done
qed

corollary subtract_nat_correct: "to_nat (subtract_nat xs ys) = (to_nat xs) - (to_nat ys)"
  using subtract_nat_aux by simp

corollary length_subtract_nat_le: "length (subtract_nat xs ys)  max (length xs) (length ys)"
  using subtract_nat_aux by simp

subsection "(Grid) Multiplication"

fun grid_mul_nat :: "nat_lsbf  nat_lsbf  nat_lsbf" where
"grid_mul_nat [] _ = []"
| "grid_mul_nat (False#xs) y = False # (grid_mul_nat xs y)"
| "grid_mul_nat (True#xs) y = add_nat (False # (grid_mul_nat xs y)) y"

lemma grid_mul_nat_correct: "to_nat (grid_mul_nat x y) = to_nat x * to_nat y"
  by (induction x y rule: grid_mul_nat.induct) (simp_all add: add_nat_correct)

lemma length_grid_mul_nat: "length (grid_mul_nat xs ys)  length xs + length ys"
proof (induction xs ys rule: grid_mul_nat.induct)
  case (1 uu)
  then show ?case by simp
next
  case (2 xs y)
  then show ?case by simp
next
  case (3 xs y)
  show ?case
  proof (rule ccontr)
    assume "¬ length (grid_mul_nat (True # xs) y)  length (True # xs) + length y"
    then have l: "length (grid_mul_nat (True # xs) y) = length xs + length y + 2"
      using length_add_nat_upper[of "False # grid_mul_nat xs y" y] 3 by simp

    then have "length (add_nat (False # grid_mul_nat xs y) y) = max (length (False # grid_mul_nat xs y)) (length y) + 1"
      using length_add_nat_upper[of "False # grid_mul_nat xs y" y] 3 by simp
    then obtain as where "add_nat (False # grid_mul_nat xs y) y = as @ [True]"
      using add_nat_last_bit_True[of "False # grid_mul_nat xs y" y] by auto
    then have as_def: "grid_mul_nat (True # xs) y = as @ [True]" by simp
    then have length_as: "length as = length xs + length y + 1" using l by simp

    from as_def have m: "to_nat (True # xs) * to_nat y = to_nat (as @ [True])"
      using grid_mul_nat_correct by metis
    also have "to_nat (as @ [True])  2 ^ length as"
      using to_nat_length_lower_bound by simp
    also have "2 ^ length as = 2 ^ (length xs + length y + 1)" using length_as by simp
    also have "to_nat (True # xs) * to_nat y < 2 ^ (length xs + 1) * 2 ^ length y"
      apply (intro mult_less_le_imp_less)
      subgoal using to_nat_length_upper_bound[of "True # xs"] by simp
      subgoal using to_nat_length_upper_bound[of y] by simp
      subgoal by simp
      subgoal
        apply (rule ccontr)
        using m to_nat_length_lower_bound[of as] by simp
      done
    finally show "False" by (simp add: power_add)
  qed
qed

subsection "Syntax bundles"


abbreviation "shift_right_flip xs n  shift_right n xs"
bundle nat_lsbf_syntax
begin
  notation add_nat (infixl "+n" 65)
  notation compare_nat (infixl "n" 50)
  notation subtract_nat (infixl "-n" 65)
  notation grid_mul_nat (infixl "*n" 70)
  notation shift_right_flip (infixl ">>n" 55)
end

bundle no_nat_lsbf_syntax
begin
  no_notation add_nat (infixl "+n" 65)
  no_notation compare_nat (infixl "n" 50)
  no_notation subtract_nat (infixl "-n" 65)
  no_notation grid_mul_nat (infixl "*n" 70)
  no_notation shift_right_flip (infixl ">>n" 55)
end

unbundle nat_lsbf_syntax

end