Theory Goodstein_Lambda

section ‹Specification›

theory Goodstein_Lambda
  imports Main
begin

subsection ‹Hereditary base representation›

text ‹We define a data type of trees and an evaluation function that sums siblings and
  exponentiates with respect to the given base on nesting.›

datatype C = C (unC: "C list")

fun evalC where
  "evalC b (C []) = 0"
| "evalC b (C (x # xs)) = b^evalC b x + evalC b (C xs)"

value "evalC 2 (C [])" ― ‹$0$›
value "evalC 2 (C [C []])" ― ‹$2^0 = 1$›
value "evalC 2 (C [C [C []]])" ― ‹$2^1 = 2$›
value "evalC 2 (C [C [], C []])" ― ‹$2^0 + 2^0 = 2^0 \cdot 2 = 2$; not in hereditary base $2$›

text ‹The hereditary base representation is characterized as trees (i.e., nested lists) whose
  lists have monotonically increasing evaluations, with fewer than @{term "b"} repetitions for
  each value. We will show later that this representation is unique.›

inductive_set hbase for b where
  "C [] ∈ hbase b"
| "i ≠ 0 ⟹ i < b ⟹ n ∈ hbase b ⟹
   C ms ∈ hbase b ⟹ (⋀m'. m' ∈ set ms ⟹ evalC b n < evalC b m') ⟹
   C (replicate i n @ ms) ∈ hbase b"

text ‹We can convert to and from natural numbers as follows.›

definition H2N where
  "H2N b n = evalC b n"

text ‹As we will show later, @{term "H2N b"} restricted to @{term "hbase n"} is bijective
  if @{prop "b ≥ (2 :: nat)"}, so we can convert from natural numbers by taking the inverse.›

definition N2H where
  "N2H b n = inv_into (hbase b) (H2N b) n"

subsection ‹The Goodstein function›

text ‹We define a function that computes the length of the Goodstein sequence whose $c$-th element
  is $g_c = n$. Termination will be shown later, thereby establishing Goodstein's theorem.›

function (sequential) goodstein :: "nat ⇒ nat ⇒ nat" where
  "goodstein 0 n = 0"
  ― ‹we start counting at 1; also note that the initial base is @{term "c+1 :: nat"} and›
  ― ‹hereditary base 1 makes no sense, so we have to avoid this case›
| "goodstein c 0 = c"
| "goodstein c n = goodstein (c+1) (H2N (c+2) (N2H (c+1) n) - 1)"
  by pat_completeness auto

abbreviation 𝒢 where
  "𝒢 n ≡ goodstein (Suc 0) n"

section ‹Ordinals›

text ‹The following type contains countable ordinals, by the usual case distinction into 0,
  successor ordinal, or limit ordinal; limit ordinals are given by their fundamental sequence.
  Hereditary base @{term "b"} representations carry over to such ordinals by replacing each
  occurrence of the base by @{term "ω"}.›

datatype Ord = Z | S Ord | L "nat ⇒ Ord"

text ‹Note that the following arithmetic operations are not correct for all ordinals. However, they
  will only be used in cases where they actually correspond to the ordinal arithmetic operations.›

primrec addO where
  "addO n Z = n"
| "addO n (S m) = S (addO n m)"
| "addO n (L f) = L (λi. addO n (f i))"

primrec mulO where
  "mulO n Z = Z"
| "mulO n (S m) = addO (mulO n m) n"
| "mulO n (L f) = L (λi. mulO n (f i))"

definition ω where
  "ω = L (λn. (S ^^ n) Z)"

primrec expω where
  "expω Z = S Z"
| "expω (S n) = mulO (expω n) ω"
| "expω (L f) = L (λi. expω (f i))"

subsection ‹Evaluation›

text ‹Evaluating an ordinal number at base $b$ is accomplished by taking the $b$-th element of
  all fundamental sequences and interpreting zero and successor over the natural numbers.›

primrec evalO where
  "evalO b Z = 0"
| "evalO b (S n) = Suc (evalO b n)"
| "evalO b (L f) = evalO b (f b)"

subsection ‹Goodstein function and sequence›

text ‹We can define the Goodstein function very easily, but proving correctness will take a while.›

primrec goodsteinO where
  "goodsteinO c Z = c"
| "goodsteinO c (S n) = goodsteinO (c+1) n"
| "goodsteinO c (L f) = goodsteinO c (f (c+2))"

primrec stepO where
  "stepO c Z = Z"
| "stepO c (S n) = n"
| "stepO c (L f) = stepO c (f (c+2))"

text ‹We can compute a few values of the Goodstein sequence starting at $4$.›

definition g4O where
  "g4O n = fold stepO [1..<Suc n] ((expω ^^ 3) Z)"

value "map (λn. evalO (n+2) (g4O n)) [0..<10]"
― ‹@{value "[4, 26, 41, 60, 83, 109, 139, 173, 211, 253] :: nat list"}›

subsection ‹Properties of evaluation›

lemma evalO_addO [simp]:
  "evalO b (addO n m) = evalO b n + evalO b m"
  by (induct m) auto

lemma evalO_mulO [simp]:
  "evalO b (mulO n m) = evalO b n * evalO b m"
  by (induct m) auto

lemma evalO_n [simp]:
  "evalO b ((S ^^ n) Z) = n"
  by (induct n) auto

lemma evalO_ω [simp]:
  "evalO b ω = b"
  by (auto simp: ω_def)

lemma evalO_expω [simp]:
  "evalO b (expω n) = b^(evalO b n)"
  by (induct n) auto

text ‹Note that evaluation is useful for proving that @{type "Ord"} values are distinct:›
notepad begin
  have "addO n (expω m) ≠ n" for n m by (auto dest: arg_cong[of _ _ "evalO 1"])
end

subsection ‹Arithmetic properties›

lemma addO_Z [simp]:
  "addO Z n = n"
  by (induct n) auto

lemma addO_assoc [simp]:
  "addO n (addO m p) = addO (addO n m) p"
  by (induct p) auto

lemma mul0_distrib [simp]:
  "mulO n (addO p q) = addO (mulO n p) (mulO n q)"
  by (induct q) auto

lemma mulO_assoc [simp]:
  "mulO n (mulO m p) = mulO (mulO n m) p"
  by (induct p) auto

lemma expω_addO [simp]:
  "expω (addO n m) = mulO (expω n) (expω m)"
  by (induct m) auto


section ‹Cantor normal form›

text ‹The previously introduced tree type @{type C} can be used to represent Cantor normal forms;
  they are trees (evaluated at base @{term ω}) such that siblings are in non-decreasing order.
  One can think of this as hereditary base @{term ω}. The plan is to mirror selected operations on
  ordinals in Cantor normal forms.›

subsection ‹Conversion to and from the ordinal type @{type Ord}›

fun C2O where
  "C2O (C []) = Z"
| "C2O (C (n # ns)) = addO (C2O (C ns)) (expω (C2O n))"

definition O2C where
  "O2C = inv C2O"

text ‹We show that @{term C2O} is injective, meaning the inverse is unique.›

lemma addO_expω_inj:
  assumes "addO n (expω m) = addO n' (expω m')"
  shows "n = n'" and "m = m'"
proof -
  have "addO n (expω m) = addO n' (expω m') ⟹ n = n'"
    by (induct m arbitrary: m'; case_tac m';
      force simp: ω_def dest!: fun_cong[of _ _ 1])
  moreover have "addO n (expω m) = addO n (expω m') ⟹ m = m'"
    apply (induct m arbitrary: n m'; case_tac m')
    apply (auto 0 3 simp: ω_def intro: rangeI
      dest: arg_cong[of _ _ "evalO 1"] fun_cong[of _ _ 0] fun_cong[of _ _ 1])[8] (* 1 left *)
    by simp (meson ext rangeI)
  ultimately show "n = n'" and "m = m'" using assms by simp_all
qed

lemma C2O_inj:
  "C2O n = C2O m ⟹ n = m"
  by (induct n arbitrary: m rule: C2O.induct; case_tac m rule: C2O.cases)
    (auto dest: addO_expω_inj arg_cong[of _ _ "evalO 1"])

lemma O2C_C2O [simp]:
  "O2C (C2O n) = n"
  by (auto intro!: inv_f_f simp: O2C_def inj_def C2O_inj)

lemma O2C_Z [simp]:
  "O2C Z = C []"
  using O2C_C2O[of "C []", unfolded C2O.simps] .

lemma C2O_replicate:
  "C2O (C (replicate i n)) = mulO (expω (C2O n)) ((S ^^ i) Z)"
  by (induct i) auto

lemma C2O_app:
  "C2O (C (xs @ ys)) = addO (C2O (C ys)) (C2O (C xs))"
  by (induct xs arbitrary: ys) auto

subsection ‹Evaluation›

lemma evalC_def':
  "evalC b n = evalO b (C2O n)"
  by (induct n rule: C2O.induct) auto

lemma evalC_app [simp]:
  "evalC b (C (ns @ ms)) = evalC b (C ns) + evalC b (C ms)"
  by (induct ns) auto

lemma evalC_replicate [simp]:
  "evalC b (C (replicate c n)) = c * evalC b (C [n])"
  by (induct c) auto

subsection ‹Transfer of the @{type Ord} induction principle to @{type C}›

fun funC where ― ‹@{term funC} computes the fundamental sequence on @{type C}›
  "funC (C []) = (λi. [C []])"
| "funC (C (C [] # ns)) = (λi. replicate i (C ns))"
| "funC (C (n # ns)) = (λi. [C (funC n i @ ns)])"

lemma C2O_cons:
  "C2O (C (n # ns)) =
    (if n = C [] then S (C2O (C ns)) else L (λi. C2O (C (funC n i @ ns))))"
  by (induct n arbitrary: ns rule: funC.induct)
    (simp_all add: ω_def C2O_replicate C2O_app flip: expω_addO)

lemma C_Ord_induct:
  assumes "P (C [])"
  and "⋀ns. P (C ns) ⟹ P (C (C [] # ns))"
  and "⋀n ns ms. (⋀i. P (C (funC (C (n # ns)) i @ ms))) ⟹
    P (C (C (n # ns) # ms))"
  shows "P n"
proof -
  have "∀n. C2O n = m ⟶ P n" for m
    by (induct m; intro allI; case_tac n rule: funC.cases)
      (auto simp: C2O_cons simp del: C2O.simps(2) intro: assms)
  then show ?thesis by simp
qed

subsection ‹Goodstein function and sequence on @{type C}›

function (domintros) goodsteinC where
  "goodsteinC c (C []) = c"
| "goodsteinC c (C (C [] # ns)) = goodsteinC (c+1) (C ns)"
| "goodsteinC c (C (C (n # ns) # ms)) =
    goodsteinC c (C (funC (C (n # ns)) (c+2) @ ms))"
  by pat_completeness auto

termination
proof -
  have "goodsteinC_dom (c, n)" for c n
    by (induct n arbitrary: c rule: C_Ord_induct) (auto intro: goodsteinC.domintros)
  then show ?thesis by simp
qed

lemma goodsteinC_def':
  "goodsteinC c n = goodsteinO c (C2O n)"
  by (induct c n rule: goodsteinC.induct) (simp_all add: C2O_cons del: C2O.simps(2))

function (domintros) stepC where
  "stepC c (C []) = C []"
| "stepC c (C (C [] # ns)) = C ns"
| "stepC c (C (C (n # ns) # ms)) =
    stepC c (C (funC (C (n # ns)) (Suc (Suc c)) @ ms))"
  by pat_completeness auto

termination
proof -
  have "stepC_dom (c, n)" for c n
    by (induct n arbitrary: c rule: C_Ord_induct) (auto intro: stepC.domintros)
  then show ?thesis by simp
qed

definition g4C where
  "g4C n = fold stepC [1..<Suc n] (C [C [C [C []]]])"

value "map (λn. evalC (n+2) (g4C n)) [0..<10]"
― ‹@{value "[4, 26, 41, 60, 83, 109, 139, 173, 211, 253] :: nat list"}›

subsection ‹Properties›

lemma stepC_def':
  "stepC c n = O2C (stepO c (C2O n))"
  by (induct c n rule: stepC.induct) (simp_all add: C2O_cons del: C2O.simps(2))

lemma funC_ne [simp]:
  "funC m (Suc n) ≠ []"
  by (cases m rule: funC.cases) simp_all

lemma evalC_funC [simp]:
  "evalC b (C (funC n b)) = evalC b (C [n])"
  by (induct n rule: funC.induct) simp_all

lemma stepC_app [simp]:
  "n ≠ C [] ⟹ stepC c (C (unC n @ ns)) = C (unC (stepC c n) @ ns)"
  by (induct n arbitrary: ns rule: stepC.induct) simp_all

lemma stepC_cons [simp]:
  "ns ≠ [] ⟹ stepC c (C (n # ns)) = C (unC (stepC c (C [n])) @ ns)"
  using stepC_app[of "C[n]" c ns] by simp

lemma stepC_dec:
  "n ≠ C [] ⟹ Suc (evalC (Suc (Suc c)) (stepC c n)) = evalC (Suc (Suc c)) n"
  by (induct c n rule: stepC.induct) simp_all

lemma stepC_dec':
  "n ≠ C [] ⟹ evalC (c+3) (stepC c n) < evalC (c+3) n"
proof (induct c n rule: stepC.induct)
  case (3 c n ns ms)
  have "evalC (c+3) (C (funC (C (n # ns)) (Suc (Suc c)))) ≤
      (c+3) ^ ((c+3) ^ evalC (c+3) n + evalC (c+3) (C ns))"
    by (induct n rule: funC.induct) (simp_all add: distrib_right)
  then show ?case using 3 by simp
qed simp_all


section ‹Hereditary base @{term b} representation›

text ‹We now turn to properties of the @{term "hbase b"} subset of trees.›

subsection ‹Uniqueness›

text ‹We show uniqueness of the hereditary base representation by showing that @{term "evalC b"}
  restricted to @{term "hbase b"} is injective.›

lemma hbaseI2:
  "i < b ⟹ n ∈ hbase b ⟹ C m ∈ hbase b ⟹
    (⋀m'. m' ∈ set m ⟹ evalC b n < evalC b m') ⟹
    C (replicate i n @ m) ∈ hbase b"
  by (cases i) (auto intro: hbase.intros simp del: replicate.simps(2))

lemmas hbase_singletonI =
  hbase.intros(2)[of 1 "Suc (Suc b)" for b, OF _ _ _ hbase.intros(1), simplified]

lemma hbase_hd:
  "C ns ∈ hbase b ⟹ ns ≠ [] ⟹ hd ns ∈ hbase b"
  by (cases rule: hbase.cases) auto

lemmas hbase_hd' [dest] = hbase_hd[of "n # ns" for n ns, simplified]

lemma hbase_tl:
  "C ns ∈ hbase b ⟹ ns ≠ [] ⟹ C (tl ns) ∈ hbase b"
  by (cases "C ns" b rule: hbase.cases) (auto intro: hbaseI2)

lemmas hbase_tl' [dest] = hbase_tl[of "n # ns" for n ns, simplified]

lemma hbase_elt [dest]:
  "C ns ∈ hbase b ⟹ n ∈ set ns ⟹ n ∈ hbase b"
  by (induct ns) auto

lemma evalC_sum_list:
  "evalC b (C ns) = sum_list (map (λn. b^evalC b n) ns)"
  by (induct ns) auto

lemma sum_list_replicate:
  "sum_list (replicate n x) = n * x"
  by (induct n) auto

lemma base_red:
  fixes b :: nat
  assumes n: "⋀n'. n' ∈ set ns ⟹ n < n'" "i < b" "i ≠ 0"
  and m: "⋀m'. m' ∈ set ms ⟹ m < m'" "j < b" "j ≠ 0"
  and s: "i * b^n + sum_list (map (λn. b^n) ns) = j * b^m + sum_list (map (λn. b^n) ms)"
  shows "i = j ∧ n = m"
  using n(1) m(1) s
proof (induct n arbitrary: m ns ms)
  { fix ns ms :: "nat list" and i j m :: nat
    assume n': "⋀n'. n' ∈ set ns ⟹ 0 < n'" "i < b" "i ≠ 0"
    assume m': "⋀m'. m' ∈ set ms ⟹ m < m'" "j < b" "j ≠ 0"
    assume s': "i * b^0 + sum_list (map (λn. b^n) ns) = j * b^m + sum_list (map (λn. b^n) ms)"
    obtain x where [simp]: "sum_list (map ((^) b) ns) = x*b"
      using n'(1)
      by (intro that[of "sum_list (map (λn. b^(n-1)) ns)"])
        (simp add: ac_simps flip: sum_list_const_mult power_Suc cong: map_cong)
    obtain y where [simp]: "sum_list (map ((^) b) ms) = y*b"
      using order.strict_trans1[OF le0 m'(1)]
      by (intro that[of "sum_list (map (λn. b^(n-1)) ms)"])
        (simp add: ac_simps flip: sum_list_const_mult power_Suc cong: map_cong)
    have [simp]: "m = 0"
      using s' n'(2,3)
      by (cases m, simp_all)
        (metis Groups.mult_ac(2) Groups.mult_ac(3) Suc_pred div_less mod_div_mult_eq
          mod_mult_self2 mod_mult_self2_is_0 mult_zero_right nat.simps(3))
    have "i = j ∧ 0 = m" using s' n'(2,3) m'(2,3)
      by simp (metis div_less mod_div_mult_eq mod_mult_self1)
  } note BASE = this
  {
    case 0 show ?case by (rule BASE; fact)
  next
    case (Suc n m')
    have "j = i ∧ 0 = Suc n" if "m' = 0" using Suc(2-4)
      by (intro BASE[of ms j ns "Suc n" i]) (simp_all add: ac_simps that n(2,3) m(2,3))
    then obtain m where m' [simp]: "m' = Suc m"
      by (cases m') auto
    obtain ns' where [simp]: "ns = map Suc ns'" "⋀n'. n' ∈ set ns' ⟹ n < n'"
      using Suc(2) less_trans[OF zero_less_Suc Suc(2)]
      by (intro that[of "map (λn. n-1) ns"]; force cong: map_cong)
    obtain ms' where [simp]: "ms = map Suc ms'" "⋀m'. m' ∈ set ms' ⟹ m < m'"
      using Suc(3)[unfolded m'] less_trans[OF zero_less_Suc Suc(3)[unfolded m']]
      by (intro that[of "map (λn. n-1) ms"]; force cong: map_cong)
    have *: "b * x = b * y ⟹ x = y" for x y using n(2) by simp
    have "i = j ∧ n = m"
    proof (rule Suc(1)[of "map (λn. n-1) ns" "map (λn. n-1) ms" m, OF _ _ *], goal_cases)
      case 3 show ?case using Suc(4) unfolding add_mult_distrib2
        by (simp add: comp_def ac_simps flip: sum_list_const_mult)
    qed simp_all
    then show ?case by simp
  }
qed

lemma evalC_inj_on_hbase:
  "n ∈ hbase b ⟹ m ∈ hbase b ⟹ evalC b n = evalC b m ⟹ n = m"
proof (induct n arbitrary: m rule: hbase.induct)
  case 1
  then show ?case by (cases m rule: hbase.cases) simp_all
next
  case (2 i n ns m')
  obtain j m ms where [simp]: "m' = C (replicate j m @ ms)" and
    m: "j ≠ 0" "j < b" "m ∈ hbase b" "C ms ∈ hbase b" "⋀m'. m' ∈ set ms ⟹ evalC b m < evalC b m'"
    using 2(8,1,2,9) by (cases m' rule: hbase.cases) simp_all
  have "i = j ∧ evalC b n = evalC b m" using 2(1,2,7,9) m(1,2,5)
    by (intro base_red[of "map (evalC b) ns" _ _ b "map (evalC b) ms"])
      (auto simp: comp_def evalC_sum_list sum_list_replicate)
  then show ?case
    using 2(4)[OF m(3)] 2(6)[OF m(4)] 2(9) by simp
qed

subsection ‹Correctness of @{const stepC}›

text ‹We show that @{term "stepC c"} preserves hereditary base @{term "c + 2 :: nat"}
  representations. In order to cover intermediate results produced by @{const stepC}, we extend
  the hereditary base representation to allow the least significant digit to be equal to @{term b},
  which essentially means that we may have an extra sibling in front on every level.›

inductive_set hbase_ext for b where
  "n ∈ hbase b ⟹ n ∈ hbase_ext b"
| "n ∈ hbase_ext b ⟹
   C m ∈ hbase b ⟹ (⋀m'. m' ∈ set m ⟹ evalC b n ≤ evalC b m') ⟹
   C (n # m) ∈ hbase_ext b"

lemma hbase_ext_hd' [dest]:
  "C (n # ns) ∈ hbase_ext b ⟹ n ∈ hbase_ext b"
  by (cases rule: hbase_ext.cases) (auto intro: hbase_ext.intros(1))

lemma hbase_ext_tl:
  "C ns ∈ hbase_ext b ⟹ ns ≠ [] ⟹ C (tl ns) ∈ hbase b"
  by (cases "C ns" b rule: hbase_ext.cases; cases ns) (simp_all add: hbase_tl')

lemmas hbase_ext_tl' [dest] = hbase_ext_tl[of "n # ns" for n ns, simplified]

lemma hbase_funC:
  "c ≠ 0 ⟹ C (n # ns) ∈ hbase_ext (Suc c) ⟹
    C (funC n (Suc c) @ ns) ∈ hbase_ext (Suc c)"
proof (induct n arbitrary: ns rule: funC.induct)
  case (2 ms)
  have [simp]: "evalC (Suc c) (C ms) < evalC (Suc c) m'" if "m' ∈ set ns" for m'
    using 2(2)
  proof (cases rule: hbase_ext.cases)
    case 1 then show ?thesis using that
      by (cases rule: hbase.cases, case_tac i) (auto intro: Suc_lessD)
  qed (auto simp: Suc_le_eq that)
  show ?case using 2
    by (auto 0 4 intro: hbase_ext.intros hbase.intros(2) order.strict_implies_order)
next
  case (3 m ms ms')
  show ?case
    unfolding funC.simps append_Cons append_Nil
  proof (rule hbase_ext.intros(2), goal_cases 31 32 33)
    case (33 m')
    show ?case using 3(3)
    proof (cases rule: hbase_ext.cases)
      case 1 show ?thesis using 1 3(1,2) 33
        by (cases rule: hbase.cases, case_tac i) (auto intro: less_or_eq_imp_le)
    qed (insert 33, simp)
  qed (insert 3, blast+)
qed auto

lemma stepC_sound:
  "n ∈ hbase_ext (Suc (Suc c)) ⟹ stepC c n ∈ hbase (Suc (Suc c))"
proof (induct c n rule: stepC.induct)
  case (3 c n ns ms)
  show ?case using 3(2,1)
    by (cases rule: hbase_ext.cases; unfold stepC.simps) (auto intro: hbase_funC)
qed (auto intro: hbase.intros)

subsection ‹Surjectivity of @{const evalC}›

text ‹Note that the base must be at least @{term "2 :: nat"}.›

lemma evalC_surjective:
  "∃n' ∈ hbase (Suc (Suc b)). evalC (Suc (Suc b)) n' = n"
proof (induct n)
  case 0 then show ?case by (auto intro: bexI[of _ "C []"] hbase.intros)
next
  have [simp]: "Suc x ≤ Suc (Suc b)^x" for x by (induct x) auto
  case (Suc n)
  then obtain n' where "n' ∈ hbase (Suc (Suc b))" "evalC (Suc (Suc b)) n' = n" by blast
  then obtain n' j where n': "Suc n ≤ j" "j = evalC (Suc (Suc b)) n'" "n' ∈ hbase (Suc (Suc b))"
    by (intro that[of _ "C [n']"])
      (auto intro!: intro: hbase.intros(1) dest!: hbaseI2[of 1 "b+2" n' "[]", simplified])
  then show ?case
  proof (induct rule: inc_induct)
    case (step m)
    obtain n' where "n' ∈ hbase (Suc (Suc b))" "evalC (Suc (Suc b)) n' = Suc m"
      using step(3)[OF step(4,5)] by blast
    then show ?case using stepC_dec[of n' "b"]
      by (cases n' rule: C2O.cases) (auto intro: stepC_sound hbase_ext.intros(1))
  qed blast
qed

subsection ‹Monotonicity of @{const hbase}›

text ‹Here we show that every hereditary base @{term "b :: nat"} number is also a valid hereditary
  base @{term "b+1 :: nat"} number. This is not immediate because we have to show that monotonicity
  of siblings is preserved.›

lemma hbase_evalC_mono:
  assumes "n ∈ hbase b" "m ∈ hbase b" "evalC b n < evalC b m"
  shows "evalC (Suc b) n < evalC (Suc b) m"
proof (cases "b < 2")
  case True show ?thesis using assms(2,3) True by (cases rule: hbase.cases) simp_all
next
  case False
  then obtain b' where [simp]: "b = Suc (Suc b')"
    by (auto simp: numeral_2_eq_2 not_less_eq dest: less_imp_Suc_add)
  show ?thesis using assms(3,1,2)
  proof (induct "evalC b n" "evalC b m" arbitrary: n m rule: less_Suc_induct)
    case 1 then show ?case using stepC_sound[of m b', OF hbase_ext.intros(1)]
      stepC_dec[of m b'] stepC_dec'[of m b'] evalC_inj_on_hbase
      by (cases m rule: C2O.cases) (fastforce simp: eval_nat_numeral)+
  next
    case (2 j) then show ?case
      using evalC_surjective[of b' j] less_trans by fastforce
  qed
qed

lemma hbase_mono:
  "n ∈ hbase b ⟹ n ∈ hbase (Suc b)"
  by (induct n rule: hbase.induct) (auto 0 3 intro: hbase.intros hbase_evalC_mono)

subsection ‹Conversion to and from @{type nat}›

text ‹We have previously defined @{term "H2N b = evalC b"} and @{term "N2H b"} as its inverse.
  So we can use the injectivity and surjectivity of @{term "evalC b"} for simplification.›

lemma N2H_inv:
  "n ∈ hbase b ⟹ N2H b (H2N b n) = n"
  using evalC_inj_on_hbase
  by (auto simp: N2H_def H2N_def[abs_def] inj_on_def intro!: inv_into_f_f)

lemma H2N_inv:
  "H2N (Suc (Suc b)) (N2H (Suc (Suc b)) n) = n"
  using evalC_surjective[of "b" n]
  by (auto simp: N2H_def H2N_def[abs_def] intro: f_inv_into_f)

lemma N2H_eqI:
  "n ∈ hbase (Suc (Suc b)) ⟹
   H2N (Suc (Suc b)) n = m ⟹ N2H (Suc (Suc b)) m = n"
  using N2H_inv by blast

lemma N2H_neI:
  "n ∈ hbase (Suc (Suc b)) ⟹
   H2N (Suc (Suc b)) n ≠ m ⟹ N2H (Suc (Suc b)) m ≠ n"
  using H2N_inv by blast

lemma N2H_0 [simp]:
  "N2H (Suc (Suc c)) 0 = C []"
  using H2N_def N2H_inv hbase.intros(1) by fastforce

lemma N2H_nz [simp]:
  "0 < n ⟹ N2H (Suc (Suc c)) n ≠ C []"
  by (metis N2H_0 H2N_inv neq0_conv)


section ‹The Goodstein function revisited›

text ‹We are now ready to prove termination of the Goodstein function @{const goodstein} as well
  as its relation to @{const goodsteinC} and @{const goodsteinO}.›

lemma goodstein_aux:
  "goodsteinC (Suc c) (N2H (Suc (Suc c)) (Suc n)) =
    goodsteinC (c+2) (N2H (c+3) (H2N (c+3) (N2H (c+2) (n+1)) - 1))"
proof -
  have [simp]: "n ≠ C [] ⟹ goodsteinC c n = goodsteinC (c+1) (stepC c n)" for c n
    by (induct c n rule: stepC.induct) simp_all
  have [simp]: "stepC (Suc c) (N2H (Suc (Suc c)) (Suc n)) ∈ hbase (Suc (Suc (Suc c)))"
    by (metis H2N_def N2H_inv evalC_surjective hbase_ext.intros(1) hbase_mono stepC_sound)
  show ?thesis
    using arg_cong[OF stepC_dec[of "N2H (c+2) (n+1)" "c+1", folded H2N_def], of "λn. N2H (c+3) (n-1)"]
    by (simp add: eval_nat_numeral N2H_inv)
qed

termination goodstein
proof (relation "measure (λ(c, n). goodsteinC c (N2H (c+1) n) - c)", goal_cases _ 1)
  case (1 c n)
  have *: "goodsteinC c n ≥ c" for c n
    by (induct c n rule: goodsteinC.induct) simp_all
  show ?case by (simp add: goodstein_aux eval_nat_numeral) (meson Suc_le_eq diff_less_mono2 lessI *)
qed simp

lemma goodstein_def':
  "c ≠ 0 ⟹ goodstein c n = goodsteinC c (N2H (c+1) n)"
  by (induct c n rule: goodstein.induct) (simp_all add: goodstein_aux eval_nat_numeral)

lemma goodstein_impl:
  "c ≠ 0 ⟹ goodstein c n = goodsteinO c (C2O (N2H (c+1) n))"
  ― ‹but note that @{term N2H} is not executable as currently defined›
  using goodstein_def'[unfolded goodsteinC_def'] .

lemma goodstein_16:
  "𝒢 16 = goodsteinO 1 (expω (expω (expω (expω Z))))"
proof -
  have "N2H (Suc (Suc 0)) 16 = C [C [C [C [C []]]]]"
    by (auto simp: H2N_def intro!: N2H_eqI hbase_singletonI hbase.intros(1))
  then show ?thesis by (simp add: goodstein_impl)
qed


section ‹Translation to $\lambda$-calculus›

text ‹We define Church encodings for @{type nat} and @{type Ord}. Note that we are basically in a
  Hindley-Milner type system, so we cannot use a proper polymorphic type. We can still express
  Church encodings as folds over values of the original type.›

abbreviation Z⇩N where "Z⇩N ≡ (λs z. z)"
abbreviation S⇩N where "S⇩N ≡ (λn s z. s (n s z))"

primrec fold_nat ("⟨_⟩⇩N") where
  "⟨0⟩⇩N = Z⇩N"
| "⟨Suc n⟩⇩N = S⇩N ⟨n⟩⇩N"

lemma one⇩N:
  "⟨1⟩⇩N = (λx. x)"
  by simp

abbreviation Z⇩O where "Z⇩O ≡ (λz s l. z)"
abbreviation S⇩O where "S⇩O ≡ (λn z s l. s (n z s l))"
abbreviation L⇩O where "L⇩O ≡ (λf z s l. l (λi. f i z s l))"

primrec fold_Ord ("⟨_⟩⇩O") where
  "⟨Z⟩⇩O = Z⇩O"
| "⟨S n⟩⇩O = S⇩O ⟨n⟩⇩O"
| "⟨L f⟩⇩O = L⇩O (λi. ⟨f i⟩⇩O)"

text ‹The following abbreviations and lemmas show how to implement the arithmetic functions and
  the Goodstein function on a Church-encoded @{type Ord} in lambda calculus.›

abbreviation (input) add⇩O where
  "add⇩O n m ≡ (λz s l. m (n z s l) s l)"

lemma add⇩O:
  "⟨addO n m⟩⇩O = add⇩O ⟨n⟩⇩O ⟨m⟩⇩O"
  by (induct m) simp_all

abbreviation (input) mul⇩O where
  "mul⇩O n m ≡ (λz s l. m z (λm. n m s l) l)"

lemma mul⇩O:
  "⟨mulO n m⟩⇩O = mul⇩O ⟨n⟩⇩O ⟨m⟩⇩O"
  by (induct m) (simp_all add: add⇩O)

abbreviation (input) ω⇩O where
  "ω⇩O ≡ (λz s l. l (λn. ⟨n⟩⇩N s z))"

lemma ω⇩O:
  "⟨ω⟩⇩O = ω⇩O"
proof -
  have [simp]: "⟨(S ^^ i) Z⟩⇩O z s l = ⟨i⟩⇩N s z" for i z s l by (induct i) simp_all
  show ?thesis by (simp add: ω_def)
qed

abbreviation (input) expω⇩O where
  "expω⇩O n ≡ (λz s l. n s (λx z. l (λn. ⟨n⟩⇩N x z)) (λf z. l (λn. f n z)) z)"

lemma expω⇩O:
  "⟨expω n⟩⇩O = expω⇩O ⟨n⟩⇩O"
  by (induct n) (simp_all add: mul⇩O ω⇩O)

abbreviation (input) goodstein⇩O where
  "goodstein⇩O ≡ (λc n. n (λx. x) (λn m. n (m + 1)) (λf m. f (m + 2) m) c)"

lemma goodstein⇩O:
  "goodsteinO c n = goodstein⇩O c ⟨n⟩⇩O"
  by (induct n arbitrary: c) simp_all

text ‹Note that modeling Church encodings with folds is still limited. For example, the meaningful
  expression @{text "⟨n⟩⇩N expω⇩O Z⇩O"} cannot be typed in Isabelle/HOL, as that would require rank-2
  polymorphism.›

subsection ‹Alternative: free theorems›

text ‹The following is essentially the free theorem for Church-encoded @{type Ord} values.›

lemma freeOrd:
  assumes "⋀n. h (s n) = s' (h n)" and "⋀f. h (l f) = l' (λi. h (f i))"
  shows "h (⟨n⟩⇩O z s l) = ⟨n⟩⇩O (h z) s' l'"
  by (induct n) (simp_all add: assms)

text ‹Each of the following proofs first states a naive definition of the corresponding function
  (which is proved correct by induction), from which we then derive the optimized version using
  the free theorem, by (conditional) rewriting (without induction).›

lemma add⇩O':
  "⟨addO n m⟩⇩O = add⇩O ⟨n⟩⇩O ⟨m⟩⇩O"
proof -
  have [simp]: "⟨addO n m⟩⇩O = ⟨m⟩⇩O ⟨n⟩⇩O S⇩O L⇩O"
    by (induct m) simp_all
  show ?thesis
    by (intro ext) (simp add: freeOrd[where h = "λn. n _ _ _"])
qed

lemma mul⇩O':
  "⟨mulO n m⟩⇩O = mul⇩O ⟨n⟩⇩O ⟨m⟩⇩O"
proof -
  have [simp]: "⟨mulO n m⟩⇩O = ⟨m⟩⇩O Z⇩O (λm. add⇩O m ⟨n⟩⇩O) L⇩O"
    by (induct m) (simp_all add: add⇩O)
  show ?thesis
    by (intro ext) (simp add: freeOrd[where h = "λn. n _ _ _"])
qed

lemma expω⇩O':
  "⟨expω n⟩⇩O = expω⇩O ⟨n⟩⇩O"
proof -
  have [simp]: "⟨expω n⟩⇩O = ⟨n⟩⇩O (S⇩O Z⇩O) (λm. mul⇩O m ω⇩O) L⇩O"
    by (induct n) (simp_all add: mul⇩O ω⇩O)
  show ?thesis
    by (intro ext) (simp add: fun_cong[OF freeOrd[where h = "λn z. n z _ _"]])
qed

end