A few theorems on integer divisibily.

--- a/src/HOL/Integ/IntDiv.thy	Fri Jan 05 17:38:05 2007 +0100
+++ b/src/HOL/Integ/IntDiv.thy	Sat Jan 06 20:47:09 2007 +0100
@@ -1076,6 +1076,24 @@
   apply (simp add: dvd_def, auto)
    apply (rule_tac [!] x = "-k" in exI, auto)
   done
+lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)" 
+  apply (cases "i > 0", simp)
+  apply (simp add: dvd_def)
+  apply (rule iffI)
+  apply (erule exE)
+  apply (rule_tac x="- k" in exI, simp)
+  apply (erule exE)
+  apply (rule_tac x="- k" in exI, simp)
+  done
+lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)" 
+  apply (cases "j > 0", simp)
+  apply (simp add: dvd_def)
+  apply (rule iffI)
+  apply (erule exE)
+  apply (rule_tac x="- k" in exI, simp)
+  apply (erule exE)
+  apply (rule_tac x="- k" in exI, simp)
+  done
 
 lemma zdvd_anti_sym:
     "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
@@ -1088,6 +1106,18 @@
   apply (blast intro: right_distrib [symmetric])
   done
 
+lemma zdvd_dvd_eq: assumes anz:"a \<noteq> 0" and ab: "(a::int) dvd b" and ba:"b dvd a" 
+  shows "\<bar>a\<bar> = \<bar>b\<bar>"
+proof-
+  from ab obtain k where k:"b = a*k" unfolding dvd_def by blast 
+  from ba obtain k' where k':"a = b*k'" unfolding dvd_def by blast 
+  from k k' have "a = a*k*k'" by simp
+  with mult_cancel_left1[where c="a" and b="k*k'"]
+  have kk':"k*k' = 1" using anz by (simp add: mult_assoc)
+  hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
+  thus ?thesis using k k' by auto
+qed
+
 lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)"
   apply (simp add: dvd_def)
   apply (blast intro: right_diff_distrib [symmetric])
@@ -1163,6 +1193,75 @@
   apply (subgoal_tac "n * k < n * 1")
    apply (drule mult_less_cancel_left [THEN iffD1], auto)
   done
+lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
+  using zmod_zdiv_equality[where a="m" and b="n"]
+  by (simp add: ring_eq_simps)
+
+lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
+apply (subgoal_tac "m mod n = 0")
+ apply (simp add: zmult_div_cancel)
+apply (simp only: zdvd_iff_zmod_eq_0)
+done
+
+lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
+  shows "m dvd n"
+proof-
+  from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
+  {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
+    with h have False by (simp add: mult_assoc)}
+  hence "n = m * h" by blast
+  thus ?thesis by blast
+qed
+
+theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
+  apply (simp split add: split_nat)
+  apply (rule iffI)
+  apply (erule exE)
+  apply (rule_tac x = "int x" in exI)
+  apply simp
+  apply (erule exE)
+  apply (rule_tac x = "nat x" in exI)
+  apply (erule conjE)
+  apply (erule_tac x = "nat x" in allE)
+  apply simp
+  done
+
+theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
+  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
+    nat_0_le cong add: conj_cong)
+  apply (rule iffI)
+  apply iprover
+  apply (erule exE)
+  apply (case_tac "x=0")
+  apply (rule_tac x=0 in exI)
+  apply simp
+  apply (case_tac "0 \<le> k")
+  apply iprover
+  apply (simp add: linorder_not_le)
+  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
+  apply assumption
+  apply (simp add: mult_ac)
+  done
+
+lemma zdvd1_eq: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
+proof
+  assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)
+  hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
+  hence "nat \<bar>x\<bar> = 1"  by simp
+  thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
+next
+  assume "\<bar>x\<bar>=1" thus "x dvd 1" 
+    by(cases "x < 0",simp_all add: minus_equation_iff zdvd_iff_zmod_eq_0)
+qed
+lemma zdvd_mult_cancel1: 
+  assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
+proof
+  assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 
+    by (cases "n >0", auto simp add: zdvd_zminus2_iff minus_equation_iff)
+next
+  assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
+  from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
+qed
 
 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
   apply (auto simp add: dvd_def nat_abs_mult_distrib)

--- a/src/HOL/Integ/Presburger.thy	Fri Jan 05 17:38:05 2007 +0100
+++ b/src/HOL/Integ/Presburger.thy	Sat Jan 06 20:47:09 2007 +0100
@@ -926,18 +926,6 @@
 theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
   by (simp split add: split_nat)
 
-theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
-  apply (simp split add: split_nat)
-  apply (rule iffI)
-  apply (erule exE)
-  apply (rule_tac x = "int x" in exI)
-  apply simp
-  apply (erule exE)
-  apply (rule_tac x = "nat x" in exI)
-  apply (erule conjE)
-  apply (erule_tac x = "nat x" in allE)
-  apply simp
-  done
 
 theorem zdiff_int_split: "P (int (x - y)) =
   ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
@@ -945,22 +933,6 @@
   apply (simp_all add: zdiff_int)
   done
 
-theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
-  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
-    nat_0_le cong add: conj_cong)
-  apply (rule iffI)
-  apply iprover
-  apply (erule exE)
-  apply (case_tac "x=0")
-  apply (rule_tac x=0 in exI)
-  apply simp
-  apply (case_tac "0 \<le> k")
-  apply iprover
-  apply (simp add: linorder_not_le)
-  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
-  apply assumption
-  apply (simp add: mult_ac)
-  done
 
 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
   by simp

--- a/src/HOL/Presburger.thy	Fri Jan 05 17:38:05 2007 +0100
+++ b/src/HOL/Presburger.thy	Sat Jan 06 20:47:09 2007 +0100
@@ -926,18 +926,6 @@
 theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
   by (simp split add: split_nat)
 
-theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
-  apply (simp split add: split_nat)
-  apply (rule iffI)
-  apply (erule exE)
-  apply (rule_tac x = "int x" in exI)
-  apply simp
-  apply (erule exE)
-  apply (rule_tac x = "nat x" in exI)
-  apply (erule conjE)
-  apply (erule_tac x = "nat x" in allE)
-  apply simp
-  done
 
 theorem zdiff_int_split: "P (int (x - y)) =
   ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
@@ -945,22 +933,6 @@
   apply (simp_all add: zdiff_int)
   done
 
-theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
-  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
-    nat_0_le cong add: conj_cong)
-  apply (rule iffI)
-  apply iprover
-  apply (erule exE)
-  apply (case_tac "x=0")
-  apply (rule_tac x=0 in exI)
-  apply simp
-  apply (case_tac "0 \<le> k")
-  apply iprover
-  apply (simp add: linorder_not_le)
-  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
-  apply assumption
-  apply (simp add: mult_ac)
-  done
 
 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
   by simp