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