# HG changeset patch
# User haftmann
# Date 1587017372 -7200
# Node ID e4e05fcd8937c8846e141c55fc5abb039e624d86
# Parent  816e52bbfa605581128b6232e12adba98cb4f6a8
generalized

diff -r 816e52bbfa60 -r e4e05fcd8937 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Thu Apr 16 08:09:31 2020 +0200
+++ b/src/HOL/Num.thy	Thu Apr 16 08:09:32 2020 +0200
@@ -543,28 +543,6 @@
 lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n"
   by (induct n) (simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
 
-lemma numeral_unfold_funpow:
-  "numeral k = ((+) 1 ^^ numeral k) 0"
-  unfolding of_nat_def [symmetric] by simp
-
-end
-
-context
-  includes lifting_syntax
-begin
-
-lemma transfer_rule_numeral:
-  "((=) ===> R) numeral numeral"
-    if [transfer_rule]: "R 0 0" "R 1 1"
-      "(R ===> R ===> R) (+) (+)"
-    for R :: "'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool"
-proof -
-  have "((=) ===> R) (\<lambda>k. ((+) 1 ^^ numeral k) 0) (\<lambda>k. ((+) 1 ^^ numeral k) 0)"
-    by transfer_prover
-  then show ?thesis
-    by (simp flip: numeral_unfold_funpow [abs_def])
-qed
-
 end
 
 lemma nat_of_num_numeral [code_abbrev]: "nat_of_num = numeral"
@@ -1136,6 +1114,60 @@
 
 lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *)
 
+context semiring_numeral
+begin
+
+lemma numeral_add_unfold_funpow:
+  \<open>numeral k + a = ((+) 1 ^^ numeral k) a\<close>
+proof (rule sym, induction k arbitrary: a)
+  case One
+  then show ?case
+    by (simp add: numeral_One Num.numeral_One)
+next
+  case (Bit0 k)
+  then show ?case
+    by (simp add: numeral_Bit0 Num.numeral_Bit0 ac_simps funpow_add)
+next
+  case (Bit1 k)
+  then show ?case
+    by (simp add: numeral_Bit1 Num.numeral_Bit1 ac_simps funpow_add)
+qed
+
+end
+
+context semiring_1
+begin
+
+lemma numeral_unfold_funpow:
+  \<open>numeral k = ((+) 1 ^^ numeral k) 0\<close>
+  using numeral_add_unfold_funpow [of k 0] by simp
+
+end
+
+context
+  includes lifting_syntax
+begin
+
+lemma transfer_rule_numeral:
+  \<open>((=) ===> R) numeral numeral\<close>
+    if [transfer_rule]: \<open>R 0 0\<close> \<open>R 1 1\<close>
+      \<open>(R ===> R ===> R) (+) (+)\<close>
+    for R :: \<open>'a::{semiring_numeral,monoid_add} \<Rightarrow> 'b::{semiring_numeral,monoid_add} \<Rightarrow> bool\<close>
+proof -
+  have "((=) ===> R) (\<lambda>k. ((+) 1 ^^ numeral k) 0) (\<lambda>k. ((+) 1 ^^ numeral k) 0)"
+    by transfer_prover
+  moreover have \<open>numeral = (\<lambda>k. ((+) (1::'a) ^^ numeral k) 0)\<close>
+    using numeral_add_unfold_funpow [where ?'a = 'a, of _ 0]
+    by (simp add: fun_eq_iff)
+  moreover have \<open>numeral = (\<lambda>k. ((+) (1::'b) ^^ numeral k) 0)\<close>
+    using numeral_add_unfold_funpow [where ?'a = 'b, of _ 0]
+    by (simp add: fun_eq_iff)
+  ultimately show ?thesis
+    by simp
+qed
+
+end
+
 
 subsection \<open>Particular lemmas concerning \<^term>\<open>2\<close>\<close>
 
diff -r 816e52bbfa60 -r e4e05fcd8937 src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Thu Apr 16 08:09:31 2020 +0200
+++ b/src/HOL/ex/Word.thy	Thu Apr 16 08:09:32 2020 +0200
@@ -157,7 +157,7 @@
   by transfer_prover
 
 lemma [transfer_rule]:
-  "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) numeral numeral"
+  "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len0 word \<Rightarrow> bool)) numeral numeral"
   by transfer_prover
 
 lemma [transfer_rule]: