# HG changeset patch
# User haftmann
# Date 1439472131 -7200
# Node ID dd8ab7252ba270cf69cee73ce5c4eebedc016eac
# Parent  bb3610d34e2e78439df253d5732f4566dfbea6fb
qualified adjust_*

diff -r bb3610d34e2e -r dd8ab7252ba2 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Aug 13 10:05:58 2015 +0200
+++ b/src/HOL/Divides.thy	Thu Aug 13 15:22:11 2015 +0200
@@ -2311,15 +2311,18 @@
     pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial
     zmod_zmult2_eq zdiv_zmult2_eq)
 
-definition adjust_div :: "int \<times> int \<Rightarrow> int"
+context
+begin
+  
+qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
 where
   "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
 
-lemma adjust_div_eq [simp, code]:
+qualified lemma adjust_div_eq [simp, code]:
   "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
   by (simp add: adjust_div_def)
 
-definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
+qualified definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
 where
   [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)"
 
@@ -2375,6 +2378,8 @@
   "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
   using numeral_mod_minus_numeral [of Num.One n] by simp
 
+end
+
 
 subsubsection \<open>Further properties\<close>
 
@@ -2574,10 +2579,10 @@
         one_div_minus_numeral one_mod_minus_numeral
         numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
         numeral_div_minus_numeral numeral_mod_minus_numeral
-        div_minus_minus mod_minus_minus adjust_div_eq of_bool_eq one_neq_zero
+        div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
         numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
         divmod_cancel divmod_steps divmod_step_eq fst_conv snd_conv numeral_One
-        case_prod_beta rel_simps adjust_mod_def div_minus1_right mod_minus1_right
+        case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
         minus_minus numeral_times_numeral mult_zero_right mult_1_right}
         @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
       fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
@@ -2602,10 +2607,10 @@
     "k mod Int.Neg Num.One = 0"
     "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 = - (adjust_div (divmod m n) :: int)"
-    "Int.Neg m mod Int.Pos n = adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
-    "Int.Pos m div Int.Neg n = - (adjust_div (divmod m n) :: int)"
-    "Int.Pos m mod Int.Neg n = - adjust_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.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.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
diff -r bb3610d34e2e -r dd8ab7252ba2 src/HOL/Matrix_LP/ComputeNumeral.thy
--- a/src/HOL/Matrix_LP/ComputeNumeral.thy	Thu Aug 13 10:05:58 2015 +0200
+++ b/src/HOL/Matrix_LP/ComputeNumeral.thy	Thu Aug 13 15:22:11 2015 +0200
@@ -51,10 +51,10 @@
   one_div_minus_numeral one_mod_minus_numeral
   numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
   numeral_div_minus_numeral numeral_mod_minus_numeral
-  div_minus_minus mod_minus_minus adjust_div_eq of_bool_eq one_neq_zero
+  div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
   numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
   divmod_steps divmod_cancel divmod_step_eq fst_conv snd_conv numeral_One
-  case_prod_beta rel_simps adjust_mod_def div_minus1_right mod_minus1_right
+  case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
   minus_minus numeral_times_numeral mult_zero_right mult_1_right