[isabelle] Induction on the length of computation sequences (in Isabelle)
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
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
after reading carefully the presentation of this material in "Programming
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)
1) Is this a correct way to encode a proof of an invariant of a tail
2) Is there a more elegant way to approach this problem?
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
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