author chaieb Sat Jan 06 20:47:09 2007 +0100 (2007-01-06) changeset 22026 cc60e54aa7cb parent 22025 7c5896919eb8 child 22027 e4a08629c4bd
A few theorems on integer divisibily.
 src/HOL/Integ/IntDiv.thy file | annotate | diff | revisions src/HOL/Integ/Presburger.thy file | annotate | diff | revisions src/HOL/Presburger.thy file | annotate | diff | revisions
```     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.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.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.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
```