When dealing with custom termination proofs I tried using the "size" function, which counts the size of a datatype instance but not the things in it. I noticed this size function is also generated for each inductive type it seems? But then you need to supply a size function for the element type. This is okay but gets a bit annoying for nested types, such as nat list list. Is there also a version of "size_list" or maybe a typeclass that, pardon my naivety, does the obvious thing? So in this case I'd expect this naive_size function to also apply the proper size function for the inner type. So for the type nat list list, it would sum the sizes of all inner lists together, I think.

Or maybe the following question is better: what's the idiomatic way to write down a decreases relation? What form should simp rules added to "termination_simp" have? (Because the way I'm writing them now, with "size" and "size_list size_some_type", they don't seem to compose very well with the termination proofs)

I don't think something like this exists. I can see that it might be useful in some cases, but it does seem a bit ‘special purpose’. But I'm not an expert on datatypes, so it's possible that the thing you're looking for does exists somewhere and I just cannot find it.

You can create a typeclass of the form that you were suggesting quite easily, but of course you'll have to do all the instantiations by hand…

```
class full_size =
fixes full_size :: "'a ⇒ nat"
instantiation nat :: full_size
begin
definition "full_size (n :: nat) = n"
instance ..
end
instantiation list :: (full_size) full_size
begin
definition "full_size = size_list full_size"
instance ..
end
value "full_size [1,2,3::nat]"
```

That's too bad! I ended writing up small size functions for each of the datatypes where it mattered, e.g. "size_clause", "size_formula", etc. At least they were easy to write that way

Last updated: Nov 11 2024 at 04:22 UTC