src/HOL/Code_Numeral.thy
changeset 64178 12e6c3bbb488
parent 63950 cdc1e59aa513
child 64241 430d74089d4d
     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)"