--- 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)"
--- 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