1.1 --- a/src/HOL/Integ/IntDiv.thy Fri Jan 05 17:38:05 2007 +0100
1.2 +++ b/src/HOL/Integ/IntDiv.thy Sat Jan 06 20:47:09 2007 +0100
1.3 @@ -1076,6 +1076,24 @@
1.4 apply (simp add: dvd_def, auto)
1.5 apply (rule_tac [!] x = "-k" in exI, auto)
1.6 done
1.7 +lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
1.8 + apply (cases "i > 0", simp)
1.9 + apply (simp add: dvd_def)
1.10 + apply (rule iffI)
1.11 + apply (erule exE)
1.12 + apply (rule_tac x="- k" in exI, simp)
1.13 + apply (erule exE)
1.14 + apply (rule_tac x="- k" in exI, simp)
1.15 + done
1.16 +lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)"
1.17 + apply (cases "j > 0", simp)
1.18 + apply (simp add: dvd_def)
1.19 + apply (rule iffI)
1.20 + apply (erule exE)
1.21 + apply (rule_tac x="- k" in exI, simp)
1.22 + apply (erule exE)
1.23 + apply (rule_tac x="- k" in exI, simp)
1.24 + done
1.25
1.26 lemma zdvd_anti_sym:
1.27 "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
1.28 @@ -1088,6 +1106,18 @@
1.29 apply (blast intro: right_distrib [symmetric])
1.30 done
1.31
1.32 +lemma zdvd_dvd_eq: assumes anz:"a \<noteq> 0" and ab: "(a::int) dvd b" and ba:"b dvd a"
1.33 + shows "\<bar>a\<bar> = \<bar>b\<bar>"
1.34 +proof-
1.35 + from ab obtain k where k:"b = a*k" unfolding dvd_def by blast
1.36 + from ba obtain k' where k':"a = b*k'" unfolding dvd_def by blast
1.37 + from k k' have "a = a*k*k'" by simp
1.38 + with mult_cancel_left1[where c="a" and b="k*k'"]
1.39 + have kk':"k*k' = 1" using anz by (simp add: mult_assoc)
1.40 + hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
1.41 + thus ?thesis using k k' by auto
1.42 +qed
1.43 +
1.44 lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)"
1.45 apply (simp add: dvd_def)
1.46 apply (blast intro: right_diff_distrib [symmetric])
1.47 @@ -1163,6 +1193,75 @@
1.48 apply (subgoal_tac "n * k < n * 1")
1.49 apply (drule mult_less_cancel_left [THEN iffD1], auto)
1.50 done
1.51 +lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
1.52 + using zmod_zdiv_equality[where a="m" and b="n"]
1.53 + by (simp add: ring_eq_simps)
1.54 +
1.55 +lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
1.56 +apply (subgoal_tac "m mod n = 0")
1.57 + apply (simp add: zmult_div_cancel)
1.58 +apply (simp only: zdvd_iff_zmod_eq_0)
1.59 +done
1.60 +
1.61 +lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
1.62 + shows "m dvd n"
1.63 +proof-
1.64 + from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
1.65 + {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
1.66 + with h have False by (simp add: mult_assoc)}
1.67 + hence "n = m * h" by blast
1.68 + thus ?thesis by blast
1.69 +qed
1.70 +
1.71 +theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
1.72 + apply (simp split add: split_nat)
1.73 + apply (rule iffI)
1.74 + apply (erule exE)
1.75 + apply (rule_tac x = "int x" in exI)
1.76 + apply simp
1.77 + apply (erule exE)
1.78 + apply (rule_tac x = "nat x" in exI)
1.79 + apply (erule conjE)
1.80 + apply (erule_tac x = "nat x" in allE)
1.81 + apply simp
1.82 + done
1.83 +
1.84 +theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
1.85 + apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
1.86 + nat_0_le cong add: conj_cong)
1.87 + apply (rule iffI)
1.88 + apply iprover
1.89 + apply (erule exE)
1.90 + apply (case_tac "x=0")
1.91 + apply (rule_tac x=0 in exI)
1.92 + apply simp
1.93 + apply (case_tac "0 \<le> k")
1.94 + apply iprover
1.95 + apply (simp add: linorder_not_le)
1.96 + apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
1.97 + apply assumption
1.98 + apply (simp add: mult_ac)
1.99 + done
1.100 +
1.101 +lemma zdvd1_eq: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
1.102 +proof
1.103 + assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)
1.104 + hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
1.105 + hence "nat \<bar>x\<bar> = 1" by simp
1.106 + thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
1.107 +next
1.108 + assume "\<bar>x\<bar>=1" thus "x dvd 1"
1.109 + by(cases "x < 0",simp_all add: minus_equation_iff zdvd_iff_zmod_eq_0)
1.110 +qed
1.111 +lemma zdvd_mult_cancel1:
1.112 + assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
1.113 +proof
1.114 + assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
1.115 + by (cases "n >0", auto simp add: zdvd_zminus2_iff minus_equation_iff)
1.116 +next
1.117 + assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
1.118 + from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
1.119 +qed
1.120
1.121 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
1.122 apply (auto simp add: dvd_def nat_abs_mult_distrib)
2.1 --- a/src/HOL/Integ/Presburger.thy Fri Jan 05 17:38:05 2007 +0100
2.2 +++ b/src/HOL/Integ/Presburger.thy Sat Jan 06 20:47:09 2007 +0100
2.3 @@ -926,18 +926,6 @@
2.4 theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
2.5 by (simp split add: split_nat)
2.6
2.7 -theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
2.8 - apply (simp split add: split_nat)
2.9 - apply (rule iffI)
2.10 - apply (erule exE)
2.11 - apply (rule_tac x = "int x" in exI)
2.12 - apply simp
2.13 - apply (erule exE)
2.14 - apply (rule_tac x = "nat x" in exI)
2.15 - apply (erule conjE)
2.16 - apply (erule_tac x = "nat x" in allE)
2.17 - apply simp
2.18 - done
2.19
2.20 theorem zdiff_int_split: "P (int (x - y)) =
2.21 ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
2.22 @@ -945,22 +933,6 @@
2.23 apply (simp_all add: zdiff_int)
2.24 done
2.25
2.26 -theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
2.27 - apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
2.28 - nat_0_le cong add: conj_cong)
2.29 - apply (rule iffI)
2.30 - apply iprover
2.31 - apply (erule exE)
2.32 - apply (case_tac "x=0")
2.33 - apply (rule_tac x=0 in exI)
2.34 - apply simp
2.35 - apply (case_tac "0 \<le> k")
2.36 - apply iprover
2.37 - apply (simp add: linorder_not_le)
2.38 - apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
2.39 - apply assumption
2.40 - apply (simp add: mult_ac)
2.41 - done
2.42
2.43 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
2.44 by simp
3.1 --- a/src/HOL/Presburger.thy Fri Jan 05 17:38:05 2007 +0100
3.2 +++ b/src/HOL/Presburger.thy Sat Jan 06 20:47:09 2007 +0100
3.3 @@ -926,18 +926,6 @@
3.4 theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
3.5 by (simp split add: split_nat)
3.6
3.7 -theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
3.8 - apply (simp split add: split_nat)
3.9 - apply (rule iffI)
3.10 - apply (erule exE)
3.11 - apply (rule_tac x = "int x" in exI)
3.12 - apply simp
3.13 - apply (erule exE)
3.14 - apply (rule_tac x = "nat x" in exI)
3.15 - apply (erule conjE)
3.16 - apply (erule_tac x = "nat x" in allE)
3.17 - apply simp
3.18 - done
3.19
3.20 theorem zdiff_int_split: "P (int (x - y)) =
3.21 ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
3.22 @@ -945,22 +933,6 @@
3.23 apply (simp_all add: zdiff_int)
3.24 done
3.25
3.26 -theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
3.27 - apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
3.28 - nat_0_le cong add: conj_cong)
3.29 - apply (rule iffI)
3.30 - apply iprover
3.31 - apply (erule exE)
3.32 - apply (case_tac "x=0")
3.33 - apply (rule_tac x=0 in exI)
3.34 - apply simp
3.35 - apply (case_tac "0 \<le> k")
3.36 - apply iprover
3.37 - apply (simp add: linorder_not_le)
3.38 - apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
3.39 - apply assumption
3.40 - apply (simp add: mult_ac)
3.41 - done
3.42
3.43 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
3.44 by simp