*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Function definition*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 27 Sep 2016 10:52:47 +0200*In-reply-to*: <CADBMspKbPobfFuis3n10UvLNkEuJJew1Qy+3o6BWnx56dsTHRw@mail.gmail.com>*References*: <CADBMspKbPobfFuis3n10UvLNkEuJJew1Qy+3o6BWnx56dsTHRw@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0

Unfortunately, it's not that easy. You pass the "interesting" function to the "boring" function as a parameter, and the "boring" function applies that function that it is given to things. In order for this to work, you need to essentially show that the "interesting" function that you are defining is only called on values for which it terminates (i.e. that are smaller than the original argument that it got) Normally, this is done with a fundef_cong rule, but in this case, I don't see how that is possible, because the values that "interesting" is called on by "boring" are "boring f t1" and "boring f t2" â that means that you are relying on the fact that the "interesting" function does not increase the size of its argument. Showing that "interesting" is size-preserving is actually straightforward: lemma same_size_boring: assumes "ây. size (f y) = size y" shows "size (boring f x) = size x" using assms by (induction x) simp_all lemma size_interesting_aux: assumes "interesting_dom (k, t)" shows "size (interesting k t) = size t" using assms by (induction rule: interesting.pinduct) (simp_all add: interesting.psimps same_size_boring) However, I have no idea how you would then go on and prove termination. Termination proofs depend on the call graph that is computed for the recursive definition, and if you don't have a fundef_cong rule for boring, that call graph â as you discovered yourself â will be too coarse (i.e. you will not have the information that you need in your termination proof). However, as I see it, any cong rule for "boring" would have to be conditional, which is, as far as I am aware, not possible for fundef_cong rules. What you are trying to do may therefore very well be outside of what the function package can do. (although I'm not 100% sure about that â still, even if it is possible, I would bet it will be ugly) My advice would be: try to define your functions in a simpler way. Proofs involving nested recursion tend to get very ugly very quickly, because the termination of your function depends on the semantics of your function, and semantic properties are difficult to use without a full termination proof. Cheers, Manuel

**Follow-Ups**:**Re: [isabelle] Function definition***From:*Christian Sternagel

**References**:**[isabelle] Function definition***From:*Edward Pierzchalski

- Previous by Date: [isabelle] Function definition
- Next by Date: Re: [isabelle] Function definition
- Previous by Thread: [isabelle] Function definition
- Next by Thread: Re: [isabelle] Function definition
- Cl-isabelle-users September 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