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 Option.map and my search for
constants used "'a option => ('a => 'b) => 'b option" instead of the
other way around for the arguments.

Thanks Lars!

-- 
cmr
http://octayn.net/

Attachment: signature.asc
Description: OpenPGP digital signature



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