Theory Hydra_Battle

theory Hydra_Battle
imports Syntactic_Ordinal
(*  Title:       Termination of the hydra battle
    Author:      Jasmin Blanchette <jasmin.blanchette at>, 2017
    Maintainer:  Jasmin Blanchette <jasmin.blanchette at>

section ‹Termination of the Hydra Battle›

theory Hydra_Battle
imports Syntactic_Ordinal

hide_const (open) Nil Cons

text ‹
The ‹h› function and its auxiliaries ‹f› and ‹d› represent the
hydra battle. The ‹encode› function converts a hydra (represented as a
Lisp-like tree) to a syntactic ordinal. The definitions follow Dershowitz and

datatype lisp =
| Cons (car: lisp) (cdr: lisp)
  "car Nil = Nil"
| "cdr Nil = Nil"

primrec encode :: "lisp ⇒ hmultiset" where
  "encode Nil = 0"
| "encode (Cons l r) = ω^(encode l) + encode r"

primrec f :: "nat ⇒ lisp ⇒ lisp ⇒ lisp" where
  "f 0 y x = x"
| "f (Suc m) y x = Cons y (f m y x)"

lemma encode_f: "encode (f n y x) = of_nat n * ω^(encode y) + encode x"
  unfolding of_nat_times_ω_exp by (induct n) (auto simp: HMSet_plus[symmetric])

function d :: "nat ⇒ lisp ⇒ lisp" where
  "d n x =
   (if car x = Nil then cdr x
    else if car (car x) = Nil then f n (cdr (car x)) (cdr x)
    else Cons (d n (car x)) (cdr x))"
  by pat_completeness auto
  by (relation "measure (λ(_, x). size x)", rule wf_measure, rename_tac n x, case_tac x, auto)

declare d.simps[simp del]

function h :: "nat ⇒ lisp ⇒ lisp" where
  "h n x = (if x = Nil then Nil else h (n + 1) (d n x))"
  by pat_completeness auto
proof -
  let ?R = "inv_image {(m, n). m < n} (λ(n, x). encode x)"

  show ?thesis
  proof (relation ?R)
    show "wf ?R"
      by (rule wf_inv_image) (rule wf)
    fix n x
    assume x_cons: "x ≠ Nil"
    thus "((n + 1, d n x), n, x) ∈ ?R"
      unfolding inv_image_def mem_Collect_eq
    proof (induct x)
      case (Cons l r)
      note ihl = this(1)
      show ?case
      proof (subst d.simps, simp, intro conjI impI)
        assume l_cons: "l ≠ Nil"
          assume "car l = Nil"
          show "encode (f n (cdr l) r) < ω^(encode l) + encode r"
            using l_cons by (cases l) (auto simp: encode_f[unfolded of_nat_times_ω_exp])
          show "encode (d n l) < encode l"
            by (rule ihl[OF l_cons])
    qed simp

declare h.simps[simp del]