# HG changeset patch
# User haftmann
# Date 1614112908 0
# Node ID 2ac92ba88d6bb1ded2db0a87f0b25bf2893b099e
# Parent  6c4c37a3ebec0d763eb8317952e95f5c097a9ae7
more lemmas

diff -r 6c4c37a3ebec -r 2ac92ba88d6b src/HOL/Library/Function_Algebras.thy
--- 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))"