*To*: Alfio Martini <alfio.martini at acm.org>*Subject*: Re: [isabelle] Induction on the length of computation sequences (in Isabelle)*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Mon, 12 Oct 2015 11:11:21 +0200*Cc*: Isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAAPnxw1+xhX7NG5EK8pbqrWo6chi0h-vcOUeLUZ1-fNdKDNhmQ@mail.gmail.com>*Organization*: TU München*References*: <CAAPnxw1+xhX7NG5EK8pbqrWo6chi0h-vcOUeLUZ1-fNdKDNhmQ@mail.gmail.com>

Hi Alfio, To answer your two questions: > 1) Is this a correct way to encode a proof of an invariant of a tail > recursive function? Yes, to use the induction-scheme by the function method is the usual way in Isabelle/HOL. of course, the induction-scheme is independent of the function itself: you can use other induction-schemes (like nat_induct), and you can also use the induction scheme tail_multn.induct to prove theorems no involving tail_multn. > 2) Is there a more elegant way to approach this problem? I find it quite elegant. Do you have anything more elegant in mind? Obviously, if you have more specific theorems to prove you might use a different approach. Btw, sometimes when defining tail-recursive functions the function-package is not enough and you might want to use partial_function. Greetings, - Johannes Am Freitag, den 09.10.2015, 14:46 -0300 schrieb Alfio Martini: > Dear Users, > > Whenever I want to (manually) prove that an invariant of a tail recursive > function is true, > I perform induction on the length of computation sequences. For instance, > consider the following > example: > > fun tail_multn::"nat => nat => nat => nat" where > "tail_multn 0 n a = a" | > "tail_multn (Suc m) n a = tail_multn m n (a+n)" > > Thus, a state s_ k (0<=k<=n) for a computation of this function is a triple > s_k=(m_k,n_k,a_k) in nat x nat x nat. > Now, using induction on k, I can prove that > > P(k)=def all m,n,a:nat. tail_multn m n a = m_k*n_k+ a_k > > The only way I was able to encode this proof in Isabelle was using > computation induction, > after reading carefully the presentation of this material in "Programming > and Proving". > > So, my proof in Isabelle is given by: > > lemma "tail_inv": "tail_multn x y a = x*y +a" > apply (induction x y a rule: tail_multn.induct) > apply (simp_all) > done > > Two questions: > > 1) Is this a correct way to encode a proof of an invariant of a tail > recursive function? > 2) Is there a more elegant way to approach this problem? > > Best! >

**Follow-Ups**:**Re: [isabelle] Induction on the length of computation sequences (in Isabelle)***From:*Alfio Martini

**References**:**[isabelle] Induction on the length of computation sequences (in Isabelle)***From:*Alfio Martini

- Previous by Date: Re: [isabelle] Getting an induction theorem from a type-name in an ML function
- Next by Date: [isabelle] Mathematics: Algorithms and Proofs 2016: Call for Participation
- Previous by Thread: [isabelle] Induction on the length of computation sequences (in Isabelle)
- Next by Thread: Re: [isabelle] Induction on the length of computation sequences (in Isabelle)
- Cl-isabelle-users October 2015 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