Isabelle termination of function on datatypes containing maps to themselves

Question

Is it possible in Isabelle to define a terminating recursive function f where

• f has a single parameter of type t such that values of type t may contain maps to values of type t, and
• f performs its recursive calls on all elements in the range of such a map?

For example consider the datatype trie defined in theory Trie_Fun:

datatype 'a trie = Nd bool "'a ⇒ 'a trie option"

and my attempt at a simple function height intended to compute the height of tries (with finitely many outgoing edges):

theory Scratch
  imports "HOL-Data_Structures.Trie_Fun"
begin

function height :: "'a trie ⇒ nat" where
  "height (Nd _ edges) = (if dom edges = Set.empty ∨ ¬ finite (dom edges)
    then 0
    else 1 + Max (height ` ran edges))"
  by pat_completeness auto
termination (* ??? *)

end

Here lexicographic_order does not suffice to prove the function to be terminating, but so far I have also not been able to formulate any measure on trie (for termination) that does not itself require a similar recursion. I must admit here that I am not sure whether I have understood datatypes in Isabelle/HOL correctly (i.e., whether a trie of the above definition is actually always of finite height).

Is it possible to show that height terminates?

Answer 1

Based to the comment by Peter Zeller, I was able to prove termination of height by adding (domintros) to the definition and then performing induction on the trie, using the fact height.domintros, resulting in the following termination proof:

function (domintros) height :: "'a trie ⇒ nat" where
  "height (Nd _ edges) = (if dom edges = Set.empty ∨ ¬ finite (dom edges)
    then 0
    else 1 + Max (height ` ran edges))"
  by pat_completeness auto
termination apply auto
proof -
  fix x :: "'a trie"
  show "height_dom x"
  proof (induction)
    case (Nd b edges)

    have "(⋀x. x ∈ ran edges ⟹ height_dom x)"
    proof -
      fix x assume "x ∈ ran edges" 
      then have "∃a. edges a = Some x"
        unfolding ran_def by blast
      then have "∃a. Some x = edges a"
        by (metis (no_types))
      then have "Some x ∈ range edges"
        by blast
      then show "height_dom x"
        using Nd by auto
    qed
    then show ?case
      using height.domintros by blast
  qed
qed