src/HOL/Code_Numeral.thy
changeset 64241 430d74089d4d
parent 64178 12e6c3bbb488
child 64246 15d1ee6e847b
     1.1 --- a/src/HOL/Code_Numeral.thy	Sun Oct 16 09:31:04 2016 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sun Oct 16 09:31:04 2016 +0200
     1.3 @@ -75,6 +75,12 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instance integer :: Rings.dvd ..
     1.8 +
     1.9 +lemma [transfer_rule]:
    1.10 +  "rel_fun pcr_integer (rel_fun pcr_integer HOL.iff) Rings.dvd Rings.dvd"
    1.11 +  unfolding dvd_def by transfer_prover
    1.12 +
    1.13  lemma [transfer_rule]:
    1.14    "rel_fun HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
    1.15    by (rule transfer_rule_of_nat) transfer_prover+
    1.16 @@ -716,6 +722,12 @@
    1.17  
    1.18  end
    1.19  
    1.20 +instance natural :: Rings.dvd ..
    1.21 +
    1.22 +lemma [transfer_rule]:
    1.23 +  "rel_fun pcr_natural (rel_fun pcr_natural HOL.iff) Rings.dvd Rings.dvd"
    1.24 +  unfolding dvd_def by transfer_prover
    1.25 +
    1.26  lemma [transfer_rule]:
    1.27    "rel_fun HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
    1.28  proof -