Re: [isabelle] Dealing with functions

Because fun generates the right induction principle, the proof is a one-liner:

by (induct n xs ys rule: sv2vl.induct) auto

See the documentation (eg Tutorial on Function Definitions or the new
Programming and Proving tutorial) for more info.

Of course you can also use this induction rule in more verbose Isar proofs.


Am 06/09/2012 01:13, schrieb Aaron W. Hsu:
> 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

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