Theory Hydra_Battle

(*  Title:       Termination of the hydra battle
    Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2017
    Maintainer:  Jasmin Blanchette <jasmin.blanchette at inria.fr>
*)

section ‹Termination of the Hydra Battle›

theory Hydra_Battle
imports Syntactic_Ordinal
begin

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
Moser.
›

datatype lisp =
  Nil
| Cons (car: lisp) (cdr: lisp)
where
  "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
termination
  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
termination
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)
  next
    fix n x
    assume x_cons: "x ≠ Nil"
    thus "((n + 1, d n x), n, x) ∈ ?R"
      unfolding inv_image_def mem_Collect_eq prod.case
    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
    qed simp
  qed
qed

declare h.simps[simp del]

end