--- a/src/HOL/IntDiv.thy Sun Mar 22 11:56:32 2009 +0100
+++ b/src/HOL/IntDiv.thy Sun Mar 22 20:46:10 2009 +0100
@@ -8,6 +8,10 @@
theory IntDiv
imports Int Divides FunDef
+uses
+ "~~/src/Provers/Arith/cancel_numeral_factor.ML"
+ "~~/src/Provers/Arith/extract_common_term.ML"
+ ("Tools/int_factor_simprocs.ML")
begin
definition divmod_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
@@ -920,9 +924,10 @@
next
assume "a\<noteq>0" and le_a: "0\<le>a"
hence a_pos: "1 \<le> a" by arith
- hence one_less_a2: "1 < 2*a" by arith
+ hence one_less_a2: "1 < 2 * a" by arith
hence le_2a: "2 * (1 + b mod a) \<le> 2 * a"
- by (simp add: mult_le_cancel_left add_commute [of 1] add1_zle_eq)
+ unfolding mult_le_cancel_left
+ by (simp add: add1_zle_eq add_commute [of 1])
with a_pos have "0 \<le> b mod a" by simp
hence le_addm: "0 \<le> 1 mod (2*a) + 2*(b mod a)"
by (simp add: mod_pos_pos_trivial one_less_a2)
@@ -1357,6 +1362,11 @@
qed
+subsection {* Simproc setup *}
+
+use "Tools/int_factor_simprocs.ML"
+
+
subsection {* Code generation *}
definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where