Re: [isabelle] Lemma suggestion to Function_Algebras



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

On 2020/10/05 9:49, Yamada, Akihisa wrote:
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


--
このEメールはアバスト アンチウイルスによりウイルススキャンされています。
https://www.avast.com/antivirus





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