[isabelle] Array and list
I have an questions pertinent to the natural numbers type.
Given the following definition:
--"translate an array into a natural list "
elems :: "nat => (nat => nat) => nat list"
"elems 0 arr = "
"elems (Suc n) arr = (arr n) # elems n arr"
Can someone please explain how can I prove the following lemma?
lemma "\<forall>ua uc. elems n (ua(n:=uc)) = elems n ua"
This archive was generated by a fusion of
Pipermail (Mailman edition) and