# HG changeset patch
# User haftmann
# Date 1476603064 -7200
# Node ID 430d74089d4d1db75494c63ebdf80ba9af6a7c25
# Parent  eabf80376aab5f687048e64e5b83fcd6a72e5474
transfer rules for divides relation on integer and natural

diff -r eabf80376aab -r 430d74089d4d src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sun Oct 16 09:31:04 2016 +0200
+++ b/src/HOL/Code_Numeral.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -75,6 +75,12 @@
 
 end
 
+instance integer :: Rings.dvd ..
+
+lemma [transfer_rule]:
+  "rel_fun pcr_integer (rel_fun pcr_integer HOL.iff) Rings.dvd Rings.dvd"
+  unfolding dvd_def by transfer_prover
+
 lemma [transfer_rule]:
   "rel_fun HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
   by (rule transfer_rule_of_nat) transfer_prover+
@@ -716,6 +722,12 @@
 
 end
 
+instance natural :: Rings.dvd ..
+
+lemma [transfer_rule]:
+  "rel_fun pcr_natural (rel_fun pcr_natural HOL.iff) Rings.dvd Rings.dvd"
+  unfolding dvd_def by transfer_prover
+
 lemma [transfer_rule]:
   "rel_fun HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
 proof -