2016-10-06 09:05:38 UTC
In a theory I'm working on, I'm having challenges defining a mutually
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.