[isabelle] Help defining a mutually recursive function


In a theory I'm working on, I'm having challenges defining a mutually
recursive function.

Here's the repository and the particular function:


I think I need to prove that read_array does not make a larger "t" for
the higher-order function passed in. I'm not sure how to do this either.

pat_completeness auto also doesn't show completeness of the pattern
matches, which I do not understand. They seem complete to me at least!

I also suspect I'll need some congruence rule for read_array, but even
after studying examples of congruence rules from the functions.pdf and
the Isabelle libraries, I'm not sure what it should be.

Thanks for any help.


Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.