[isabelle] Dealing with functions



Hello all:

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? 

	Yours truly,

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