# Re: [isabelle] Termination for ordinal-like datatypes

```Dear Eddy,

> I was wondering if someone could help me figure out an easy way to prove termination for functions over ordinal-like datatypes. What I mean by this is datatypes T where one of the constructors for T takes a function that returns type T. The classic one is the ordinals:
>
> datatype ord
>  = Zero
>  | Succ ord
>  | Limit "(nat => ord)”
>
> My question is, what is the easiest and best way to write termination proofs for recursive functions over the type ord? Are there some mechanisms already available, or do I have to define my own inductive proposition or something similar? It looks like all the default mechanisms for proving termination rely on types that satisfy “size”, which ord does not because of the Limit constructor.
>
> For example, I want to define functions like these, which should be terminating:
>
> function ord_plus :: "ord => ord => ord"
> where
>  "ord_plus x Zero = x"
>  | "ord_plus x (Succ y) = Succ (ord_plus x y)"
>  | "ord_plus x (Limit f) = Limit (\<lambda> n . ord_plus x (f n))"
>  by pat_completeness auto
>
> function ord_leq :: "ord ⇒ ord ⇒ bool"
> where
>  "ord_leq Zero x = True"
>  | "ord_leq (Succ x) Zero = False"
>  | "ord_leq (Succ x) (Succ y) = ord_leq x y"
>  | "ord_leq (Succ x) (Limit f) = (\<exists> n. ord_leq (Succ x) (f n))"
>  | "ord_leq (Limit f) y = (\<forall>n . ord_leq (f n) y)"
>  by pat_completeness auto

In your case (recursion via "nat => _") it might be best to use primrec instead of fun/function:

primrec ord_plus :: "ord => ord => ord"
where
"ord_plus x Zero = x"
| "ord_plus x (Succ y) = Succ (ord_plus x y)"
| "ord_plus x (Limit f) = Limit (λ n . ord_plus x (f n))"

is accepted without having to prove anything.

Hope this helps,
René

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.