src/HOL/Int.thy
changeset 64014 ca1239a3277b
parent 63652 804b80a80016
child 64267 b9a1486e79be
     1.1 --- a/src/HOL/Int.thy	Mon Oct 03 14:34:31 2016 +0200
     1.2 +++ b/src/HOL/Int.thy	Mon Oct 03 14:34:32 2016 +0200
     1.3 @@ -983,6 +983,20 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma transfer_rule_of_int:
     1.8 +  fixes R :: "'a::ring_1 \<Rightarrow> 'b::ring_1 \<Rightarrow> bool"
     1.9 +  assumes [transfer_rule]: "R 0 0" "R 1 1"
    1.10 +    "rel_fun R (rel_fun R R) plus plus"
    1.11 +    "rel_fun R R uminus uminus"
    1.12 +  shows "rel_fun HOL.eq R of_int of_int"
    1.13 +proof -
    1.14 +  note transfer_rule_of_nat [transfer_rule]
    1.15 +  have [transfer_rule]: "rel_fun HOL.eq R of_nat of_nat"
    1.16 +    by transfer_prover
    1.17 +  show ?thesis
    1.18 +    by (unfold of_int_of_nat [abs_def]) transfer_prover
    1.19 +qed
    1.20 +
    1.21  lemma nat_mult_distrib:
    1.22    fixes z z' :: int
    1.23    assumes "0 \<le> z"