# HG changeset patch
# User haftmann
# Date 1476301733 -7200
# Node ID 12e6c3bbb488499f5183de57b48c80e07eaf3596
# Parent  006f303fb173a231c715e85cecec9b98a5c35807
transfer lifting rule for numeral

diff -r 006f303fb173 -r 12e6c3bbb488 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Wed Oct 12 21:48:52 2016 +0200
+++ b/src/HOL/Code_Numeral.thy	Wed Oct 12 21:48:53 2016 +0200
@@ -77,23 +77,19 @@
 
 lemma [transfer_rule]:
   "rel_fun HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
-  by (unfold of_nat_def [abs_def]) transfer_prover
+  by (rule transfer_rule_of_nat) transfer_prover+
 
 lemma [transfer_rule]:
   "rel_fun HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
 proof -
   have "rel_fun HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
-    by (unfold of_int_of_nat [abs_def]) transfer_prover
+    by (rule transfer_rule_of_int) transfer_prover+
   then show ?thesis by (simp add: id_def)
 qed
 
 lemma [transfer_rule]:
   "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
-proof -
-  have "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
-    by transfer_prover
-  then show ?thesis by simp
-qed
+  by (rule transfer_rule_numeral) transfer_prover+
 
 lemma [transfer_rule]:
   "rel_fun HOL.eq (rel_fun HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
diff -r 006f303fb173 -r 12e6c3bbb488 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Wed Oct 12 21:48:52 2016 +0200
+++ b/src/HOL/Num.thy	Wed Oct 12 21:48:53 2016 +0200
@@ -6,7 +6,7 @@
 section \<open>Binary Numerals\<close>
 
 theory Num
-  imports BNF_Least_Fixpoint
+  imports BNF_Least_Fixpoint Transfer
 begin
 
 subsection \<open>The \<open>num\<close> type\<close>
@@ -535,8 +535,22 @@
 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 = (op + 1 ^^ numeral k) 0"
+  unfolding of_nat_def [symmetric] by simp
+
 end
 
+lemma transfer_rule_numeral:
+  fixes R :: "'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool"
+  assumes [transfer_rule]: "R 0 0" "R 1 1"
+    "rel_fun R (rel_fun R R) plus plus"
+  shows "rel_fun HOL.eq R numeral numeral"
+  apply (subst (2) numeral_unfold_funpow [abs_def])
+  apply (subst (1) numeral_unfold_funpow [abs_def])
+  apply transfer_prover
+  done
+
 lemma nat_of_num_numeral [code_abbrev]: "nat_of_num = numeral"
 proof
   fix n