Search code examples
isabelletermination

Make automatic termination proof use different size function

I have written a custom size function size2 for my datatype. Using this function I can manually prove the termination of my function:

termination 
apply (relation "measure (λ(a,b,c). size2 c)")
apply auto
done

Is there a way to make fun use my alternative size function for the automatic termination proof?

Solution

  • A function f can be registered as a measure function for the termination prover by declaring the lemma is_measure f with the attribute measure_function. In your case, this looks as follows.

    lemma is_measure_size2 [measure_function]: "is_measure size2" ..

    Then, lexicographic_order, which fun uses, and size_change try size2, too.