# Re: [isabelle] Induction on the length of computation sequences (in Isabelle)

```Hi Alfio,

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

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.