Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Array and list

view this post on Zulip Email Gateway (Aug 17 2022 at 13:27):

From: Alexander Krauss <krauss@in.tum.de>
Zhang Hong wrote:

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

view this post on Zulip Email Gateway (Aug 17 2022 at 13:27):

From: Zhang Hong <hong@ercist.iscas.ac.cn>
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.

Last updated: May 03 2024 at 12:27 UTC