transfer lifting rule for numeral
authorhaftmann
Wed Oct 12 21:48:53 2016 +0200 (2016-10-12)
changeset 6417812e6c3bbb488
parent 64177 006f303fb173
child 64179 ce205d1f8592
child 64182 857a335ac292
transfer lifting rule for numeral
src/HOL/Code_Numeral.thy
src/HOL/Num.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Wed Oct 12 21:48:52 2016 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Wed Oct 12 21:48:53 2016 +0200
     1.3 @@ -77,23 +77,19 @@
     1.4  
     1.5  lemma [transfer_rule]:
     1.6    "rel_fun HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
     1.7 -  by (unfold of_nat_def [abs_def]) transfer_prover
     1.8 +  by (rule transfer_rule_of_nat) transfer_prover+
     1.9  
    1.10  lemma [transfer_rule]:
    1.11    "rel_fun HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
    1.12  proof -
    1.13    have "rel_fun HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
    1.14 -    by (unfold of_int_of_nat [abs_def]) transfer_prover
    1.15 +    by (rule transfer_rule_of_int) transfer_prover+
    1.16    then show ?thesis by (simp add: id_def)
    1.17  qed
    1.18  
    1.19  lemma [transfer_rule]:
    1.20    "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
    1.21 -proof -
    1.22 -  have "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
    1.23 -    by transfer_prover
    1.24 -  then show ?thesis by simp
    1.25 -qed
    1.26 +  by (rule transfer_rule_numeral) transfer_prover+
    1.27  
    1.28  lemma [transfer_rule]:
    1.29    "rel_fun HOL.eq (rel_fun HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
     2.1 --- a/src/HOL/Num.thy	Wed Oct 12 21:48:52 2016 +0200
     2.2 +++ b/src/HOL/Num.thy	Wed Oct 12 21:48:53 2016 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  section \<open>Binary Numerals\<close>
     2.5  
     2.6  theory Num
     2.7 -  imports BNF_Least_Fixpoint
     2.8 +  imports BNF_Least_Fixpoint Transfer
     2.9  begin
    2.10  
    2.11  subsection \<open>The \<open>num\<close> type\<close>
    2.12 @@ -535,8 +535,22 @@
    2.13  lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n"
    2.14    by (induct n) (simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
    2.15  
    2.16 +lemma numeral_unfold_funpow:
    2.17 +  "numeral k = (op + 1 ^^ numeral k) 0"
    2.18 +  unfolding of_nat_def [symmetric] by simp
    2.19 +
    2.20  end
    2.21  
    2.22 +lemma transfer_rule_numeral:
    2.23 +  fixes R :: "'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool"
    2.24 +  assumes [transfer_rule]: "R 0 0" "R 1 1"
    2.25 +    "rel_fun R (rel_fun R R) plus plus"
    2.26 +  shows "rel_fun HOL.eq R numeral numeral"
    2.27 +  apply (subst (2) numeral_unfold_funpow [abs_def])
    2.28 +  apply (subst (1) numeral_unfold_funpow [abs_def])
    2.29 +  apply transfer_prover
    2.30 +  done
    2.31 +
    2.32  lemma nat_of_num_numeral [code_abbrev]: "nat_of_num = numeral"
    2.33  proof
    2.34    fix n