--- a/src/HOL/Library/Function_Algebras.thy Tue Feb 23 20:41:48 2021 +0000
+++ b/src/HOL/Library/Function_Algebras.thy Tue Feb 23 20:41:48 2021 +0000
@@ -132,6 +132,14 @@
instance "fun" :: (type, semiring_1) semiring_1 ..
+lemma numeral_fun: \<^marker>\<open>contributor \<open>Akihisa Yamada\<close>\<close>
+ \<open>numeral n = (\<lambda>x::'a. numeral n)\<close>
+ by (induction n) (simp_all only: numeral.simps plus_fun_def, simp_all)
+
+lemma numeral_fun_apply [simp]: \<^marker>\<open>contributor \<open>Akihisa Yamada\<close>\<close>
+ \<open>numeral n x = numeral n\<close>
+ by (simp add: numeral_fun)
+
lemma of_nat_fun: "of_nat n = (\<lambda>x::'a. of_nat n)"
proof -
have comp: "comp = (\<lambda>f g x. f (g x))"