# Theory Hydra_Battle

theory Hydra_Battle
imports Syntactic_Ordinal
```(*  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
```