*To*: Corey Richardson <corey at octayn.net>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Help defining a mutually recursive function*From*: Lars Hupel <hupel at in.tum.de>*Date*: Thu, 6 Oct 2016 11:29:09 +0200*In-reply-to*: <92645c8b-66d2-27f4-878b-4530199f4ea9@octayn.net>*References*: <92645c8b-66d2-27f4-878b-4530199f4ea9@octayn.net>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

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

**Follow-Ups**:**Re: [isabelle] Help defining a mutually recursive function***From:*Corey Richardson

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

- Previous by Date: [isabelle] Help defining a mutually recursive function
- Next by Date: Re: [isabelle] Help defining a mutually recursive function
- Previous by Thread: [isabelle] Help defining a mutually recursive function
- Next by Thread: Re: [isabelle] Help defining a mutually recursive function
- 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