[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.