src/HOL/Num.thy
 changeset 64178 12e6c3bbb488 parent 63913 6b886cadba7c child 64238 b60a9752b6d0
```     1.1 --- a/src/HOL/Num.thy	Wed Oct 12 21:48:52 2016 +0200
1.2 +++ b/src/HOL/Num.thy	Wed Oct 12 21:48:53 2016 +0200
1.3 @@ -6,7 +6,7 @@
1.4  section \<open>Binary Numerals\<close>
1.5
1.6  theory Num
1.7 -  imports BNF_Least_Fixpoint
1.8 +  imports BNF_Least_Fixpoint Transfer
1.9  begin
1.10
1.11  subsection \<open>The \<open>num\<close> type\<close>
1.12 @@ -535,8 +535,22 @@
1.13  lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n"
1.14    by (induct n) (simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
1.15
1.16 +lemma numeral_unfold_funpow:
1.17 +  "numeral k = (op + 1 ^^ numeral k) 0"
1.18 +  unfolding of_nat_def [symmetric] by simp
1.19 +
1.20  end
1.21
1.22 +lemma transfer_rule_numeral:
1.23 +  fixes R :: "'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool"
1.24 +  assumes [transfer_rule]: "R 0 0" "R 1 1"
1.25 +    "rel_fun R (rel_fun R R) plus plus"
1.26 +  shows "rel_fun HOL.eq R numeral numeral"
1.27 +  apply (subst (2) numeral_unfold_funpow [abs_def])
1.28 +  apply (subst (1) numeral_unfold_funpow [abs_def])
1.29 +  apply transfer_prover
1.30 +  done
1.31 +
1.32  lemma nat_of_num_numeral [code_abbrev]: "nat_of_num = numeral"
1.33  proof
1.34    fix n
```