Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Lemma suggestion to Function_Algebras

view this post on Zulip Email Gateway (Oct 05 2020 at 00:50):

From: "Yamada, Akihisa" <ayamada@trs.cm.is.nagoya-u.ac.jp>
Dear library developers,

I propose the following lemma in HOL-Library.Function_Algebras:

lemma numeral_fun_apply[simp]:
"numeral (num.Bit0 n) x = numeral n x + numeral n x"
"numeral (num.Bit1 n) x = numeral n x + numeral n x + 1"
by (simp_all only: numeral.simps plus_fun_apply one_fun_apply)

so that users wouldn't have to learn the internal representation for
trivial facts like: "2 = (λx. 2)"

Best,
Akihisa

view this post on Zulip Email Gateway (Oct 05 2020 at 01:05):

From: "Yamada, Akihisa" <ayamada@trs.cm.is.nagoya-u.ac.jp>
Dear list,

let me refine the suggestion by

lemma numeral_fun_apply[simp]: "numeral n x = numeral n"
by (induct n; simp only: numeral.simps plus_fun_apply one_fun_apply)

Best regards,
Akihisa

view this post on Zulip Email Gateway (Jan 14 2021 at 15:21):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Akihisa,

thanks for contributing this.

I will put it into the distribution after the upcoming Isabelle2021 release.

Cheers,
Florian
signature.asc

Last updated: Jan 04 2025 at 20:18 UTC