[isabelle] Array and list



Hello,

I have an questions pertinent to the natural numbers type.

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"



Thanks,
Hong Zhang.







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