# 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

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

Tobias

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.