*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Help defining a mutually recursive function*From*: Corey Richardson <corey at octayn.net>*Date*: Thu, 6 Oct 2016 05:38:18 -0400*In-reply-to*: <f2624f79-2802-2498-247a-8895c5e55cec@in.tum.de>*References*: <92645c8b-66d2-27f4-878b-4530199f4ea9@octayn.net> <f2624f79-2802-2498-247a-8895c5e55cec@in.tum.de>*User-agent*: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

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**

**References**:**[isabelle] Help defining a mutually recursive function***From:*Corey Richardson

**Re: [isabelle] Help defining a mutually recursive function***From:*Lars Hupel

- Previous by Date: Re: [isabelle] Help defining a mutually recursive function
- Next by Date: [isabelle] Using an assumption as a rule
- Previous by Thread: Re: [isabelle] Help defining a mutually recursive function
- Next by Thread: [isabelle] Using an assumption as a rule
- Cl-isabelle-users October 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list