# HG changeset patch
# User haftmann
# Date 1660888156 0
# Node ID 96d5fa32f0f72e4aecbe43a50fa9d921fc4bff43
# Parent  83e4b6a5e7de0b243e91f9392dd530ef77c784b5
tuned type signature

diff -r 83e4b6a5e7de -r 96d5fa32f0f7 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Aug 19 05:49:12 2022 +0000
+++ b/src/HOL/Divides.thy	Fri Aug 19 05:49:16 2022 +0000
@@ -879,9 +879,9 @@
   "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
   by (simp add: adjust_div_def)
 
-qualified definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
+qualified definition adjust_mod :: "num \<Rightarrow> int \<Rightarrow> int"
 where
-  [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)"
+  [simp]: "adjust_mod l r = (if r = 0 then 0 else numeral l - r)"
 
 lemma minus_numeral_div_numeral [simp]:
   "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
@@ -893,7 +893,7 @@
 qed
 
 lemma minus_numeral_mod_numeral [simp]:
-  "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
+  "- numeral m mod numeral n = adjust_mod n (snd (divmod m n) :: int)"
 proof (cases "snd (divmod m n) = (0::int)")
   case True
   then show ?thesis
@@ -917,7 +917,7 @@
 qed
   
 lemma numeral_mod_minus_numeral [simp]:
-  "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
+  "numeral m mod - numeral n = - adjust_mod n (snd (divmod m n) :: int)"
 proof (cases "snd (divmod m n) = (0::int)")
   case True
   then show ?thesis
@@ -936,7 +936,7 @@
   using minus_numeral_div_numeral [of Num.One n] by simp  
 
 lemma minus_one_mod_numeral [simp]:
-  "- 1 mod numeral n = adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
+  "- 1 mod numeral n = adjust_mod n (snd (divmod Num.One n) :: int)"
   using minus_numeral_mod_numeral [of Num.One n] by simp
 
 lemma one_div_minus_numeral [simp]:
@@ -944,7 +944,7 @@
   using numeral_div_minus_numeral [of Num.One n] by simp
   
 lemma one_mod_minus_numeral [simp]:
-  "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
+  "1 mod - numeral n = - adjust_mod n (snd (divmod Num.One n) :: int)"
   using numeral_mod_minus_numeral [of Num.One n] by simp
 
 end
@@ -1053,9 +1053,9 @@
     "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
     "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
     "Int.Neg m div Int.Pos n = - (Divides.adjust_div (divmod m n) :: int)"
-    "Int.Neg m mod Int.Pos n = Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
+    "Int.Neg m mod Int.Pos n = Divides.adjust_mod n (snd (divmod m n) :: int)"
     "Int.Pos m div Int.Neg n = - (Divides.adjust_div (divmod m n) :: int)"
-    "Int.Pos m mod Int.Neg n = - Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
+    "Int.Pos m mod Int.Neg n = - Divides.adjust_mod n (snd (divmod m n) :: int)"
     "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
     "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
   by simp_all