Re: [isabelle] Array and list



Zhang Hong wrote:

> Given the following definition:
>    --"translate an array into a natural list "
>    consts
>      elems :: "nat => (nat => nat) => nat list"
>    primrec
>      "elems 0 arr = []"
>      "elems (Suc n) arr = (arr n) # elems n arr"
>
> Question:
> Can someone please explain how can I prove the following lemma?
>     lemma "\<forall>ua uc. elems n (ua(n:=uc)) = elems n ua"


Generalize your lemma first:

lemma "m <= n --> elems m (ua(n:=uc)) = elems m ua"

Unlike the original, you can easily prove this by induction on m. (This
is because you get a stronger induction hypothesis here...)

Hope this helps.

Alex


-- 
Alexander Krauss                   E-Mail: krauss at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17300
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.060
85748 Garching, GERMANY            http://www4.in.tum.de/~krauss





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