*To*: e.a.pierzchalski at gmail.com, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Function definition*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Tue, 27 Sep 2016 13:45:01 +0200*In-reply-to*: <d234e92f-9b22-0e15-f5fb-57eadfee4af7@in.tum.de>*References*: <CADBMspKbPobfFuis3n10UvLNkEuJJew1Qy+3o6BWnx56dsTHRw@mail.gmail.com> <d234e92f-9b22-0e15-f5fb-57eadfee4af7@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0

Dear Ed, as Manuel indicated, you'll likely have to define your function in another way. One way would be to use mutual recursion: function (sequential) interesting :: "nat â t â t" and boring :: "nat â t â t" where "interesting k (N n) = N (n + k)" | "interesting k (A t) = A (interesting (k + 1) t)" | "interesting k t = boring k t" | "boring k (N n) = N n" | "boring k (A t) = A (interesting k (boring k t))" | "boring k (B t1 t2) = B (interesting k (boring k t1)) (interesting k (boring k t2))" by (pat_completeness) auto where your "boring" is replaced by a variant that only takes "k" as parameter. Then we can prove that both functions are size-preserving, as already suggested by Manuel. lemma [termination_simp]: shows "interesting_boring_dom (Inl (k, t)) â size (interesting k t) = size t" and "interesting_boring_dom (Inr (k, t)) â size (boring k t) = size t" by (induct k t and k t rule: interesting_boring.pinduct) (simp_all add: interesting.psimps boring.psimps) Which incidentally suffices for termination: termination by (lexicographic_order) It remains to show that this actually corresponds to your original function specification. Here, I use "boring'" for your "boring". fun boring' :: "(t â t) â t â t" where "boring' f (N n) = N n" | "boring' f (A t) = A (f (boring' f t))" | "boring' f (B t1 t2) = B (f (boring' f t1)) (f (boring' f t2))" Your definition of "interesting" (modulo "case" on the right vs. pattern-matching on the left) can be obtained by mutual induction: lemma shows "interesting k s = (case s of N n â N (n + k) | A t â A (interesting (k + 1) t) | t â boring' (interesting k) t)" and "boring k s = boring' (interesting k) s" by (induct k s and k s rule: interesting_boring.induct) auto cheers chris PS: For those who care and know what I'm talking about: termination of the TRS corresponding to "interesting" and "boring" is trivial for modern termination tools. Maybe a reason to revive IsaFoR/TermFun? ;) On 09/27/2016 10:52 AM, Manuel Eberl wrote: > 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:*Thomas.Sewell

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

**Re: [isabelle] Function definition***From:*Manuel Eberl

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