Hi Corey,
let's start with the simple question:
> pat_completeness auto also doesn't show completeness of the pattern
> matches, which I do not understand. They seem complete to me at least!
They are overlapping as you have written them down. As opposed to "fun",
"function" by default does not consider pattern matches to be
sequential. That is, your sixth equation matches everything the others
matched, too. The fix is easy: use "function (sequential)" instead, and
"pat_completeness auto" will solve it.
> 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.
>
> 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.
"read_array" looks complicated, because the calls of the callback
function look quite irregular. Have you tried inlining the definition of
"read_array", i.e. remove the callback and define it as part of the
mutual bundle?
(In my personal experience, while this complicates some proofs because
of the now three-way-mutual definition, it greatly simplifies some others.)
Also, the "Option.bind ... (Some o ValArray)" looks suspicious. Why are
you "bind"ing if you're always feeding in a "Some"?
Cheers
Lars