CODEWITHSUNDEEP
isabelletermination
Peter Zeller
Peter Zeller

Reputation: 2296

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?

Upvotes: 4

Views: 163

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5078

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.

Upvotes: 4

Related Questions