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