[isabelle] Lemma suggestion to Function_Algebras



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.