[isabelle] Dealing with functions
I have a function that I have defined like this:
fun sv2vl :: "nat â?? 'a::scalar list â?? 'a::scalar list â?? 'a::scalar list" where
"sv2vl 0 orig lst = "
| "sv2vl cnt   = (replicate cnt fill)"
| "sv2vl (Suc cnt) (oel # ors)  = (oel # (sv2vl cnt (oel # ors) ors))"
| "sv2vl (Suc cnt) orig (elm # rst) = (elm # (sv2vl cnt orig rst))"
And I am trying to prove that the length of the result of this function
is equal to the first argument. However, unlike with primrec or
some other elements, I am having a hard time figuring out how to
express the various cases of the body to Isabelle. That is, I am thinking
that you would prove this inductively by showing the base case
trivially, and then showing that for the case (Suc n) you have three
cases where this could be true, and in each one of them, the length
is what I want.
However, how do I say this in Isar or whatever else I am doing?
Aaron W. Hsu
Aaron W. Hsu | arcfide at sacrideo.us | http://www.sacrideo.us
Programming is just another word for the lost art of thinking.
This archive was generated by a fusion of
Pipermail (Mailman edition) and