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

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!
--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica
90619-900 -Porto Alegre - RS - Brasil

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