Automatically complete evidence using a different size function

Question

I wrote a custom size function size2for my data type. Using this function, I can manually confirm the termination of my function:

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

Is there any way to make funuse of my alternative size function to automatically confirm completion?

Answer 1

A function fcan be registered as a dimension function to verify completion by declaring the lemma an is_measure fattribute measure_function. In your case, it looks like this.

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

lexicographic_order, fun, size_change size2 .