Re: [isabelle] Help defining a mutually recursive function

On 2016-10-06 5:29, Lars Hupel wrote:
> 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.

Ah, that's simple. Thanks!

>> 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.)

I was avoiding it for the complication you mention. Adding it as another
mutually recursive function indeed makes all my problems go away (for now).

> Also, the "Option.bind ... (Some o ValArray)" looks suspicious. Why are
> you "bind"ing if you're always feeding in a "Some"?

I was using it as a poor-man's map_option, before I noticed that
map_option existed! I was looking for and my search for
constants used "'a option => ('a => 'b) => 'b option" instead of the
other way around for the arguments.

Thanks Lars!


Attachment: signature.asc
Description: OpenPGP digital signature

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