generalize some div/mod lemmas; remove type-specific proofs
authorhuffman
Thu Jan 08 08:24:08 2009 -0800 (2009-01-08)
changeset 29403fe17df4e4ab3
parent 29402 9610f3870d64
child 29404 ee15ccdeaa72
generalize some div/mod lemmas; remove type-specific proofs
src/HOL/Divides.thy
src/HOL/IntDiv.thy
     1.1 --- a/src/HOL/Divides.thy	Wed Jan 07 08:13:56 2009 -0800
     1.2 +++ b/src/HOL/Divides.thy	Thu Jan 08 08:24:08 2009 -0800
     1.3 @@ -33,6 +33,10 @@
     1.4    unfolding mult_commute [of b]
     1.5    by (rule mod_div_equality)
     1.6  
     1.7 +lemma mod_div_equality': "a mod b + a div b * b = a"
     1.8 +  using mod_div_equality [of a b]
     1.9 +  by (simp only: add_ac)
    1.10 +
    1.11  lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
    1.12    by (simp add: mod_div_equality)
    1.13  
    1.14 @@ -143,6 +147,107 @@
    1.15    then show "b mod a = 0" by simp
    1.16  qed
    1.17  
    1.18 +lemma mod_div_trivial [simp]: "a mod b div b = 0"
    1.19 +proof (cases "b = 0")
    1.20 +  assume "b = 0"
    1.21 +  thus ?thesis by simp
    1.22 +next
    1.23 +  assume "b \<noteq> 0"
    1.24 +  hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
    1.25 +    by (rule div_mult_self1 [symmetric])
    1.26 +  also have "\<dots> = a div b"
    1.27 +    by (simp only: mod_div_equality')
    1.28 +  also have "\<dots> = a div b + 0"
    1.29 +    by simp
    1.30 +  finally show ?thesis
    1.31 +    by (rule add_left_imp_eq)
    1.32 +qed
    1.33 +
    1.34 +lemma mod_mod_trivial [simp]: "a mod b mod b = a mod b"
    1.35 +proof -
    1.36 +  have "a mod b mod b = (a mod b + a div b * b) mod b"
    1.37 +    by (simp only: mod_mult_self1)
    1.38 +  also have "\<dots> = a mod b"
    1.39 +    by (simp only: mod_div_equality')
    1.40 +  finally show ?thesis .
    1.41 +qed
    1.42 +
    1.43 +text {* Addition respects modular equivalence. *}
    1.44 +
    1.45 +lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c"
    1.46 +proof -
    1.47 +  have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
    1.48 +    by (simp only: mod_div_equality)
    1.49 +  also have "\<dots> = (a mod c + b + a div c * c) mod c"
    1.50 +    by (simp only: add_ac)
    1.51 +  also have "\<dots> = (a mod c + b) mod c"
    1.52 +    by (rule mod_mult_self1)
    1.53 +  finally show ?thesis .
    1.54 +qed
    1.55 +
    1.56 +lemma mod_add_right_eq: "(a + b) mod c = (a + b mod c) mod c"
    1.57 +proof -
    1.58 +  have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
    1.59 +    by (simp only: mod_div_equality)
    1.60 +  also have "\<dots> = (a + b mod c + b div c * c) mod c"
    1.61 +    by (simp only: add_ac)
    1.62 +  also have "\<dots> = (a + b mod c) mod c"
    1.63 +    by (rule mod_mult_self1)
    1.64 +  finally show ?thesis .
    1.65 +qed
    1.66 +
    1.67 +lemma mod_add_eq: "(a + b) mod c = (a mod c + b mod c) mod c"
    1.68 +by (rule trans [OF mod_add_left_eq mod_add_right_eq])
    1.69 +
    1.70 +lemma mod_add_cong:
    1.71 +  assumes "a mod c = a' mod c"
    1.72 +  assumes "b mod c = b' mod c"
    1.73 +  shows "(a + b) mod c = (a' + b') mod c"
    1.74 +proof -
    1.75 +  have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
    1.76 +    unfolding assms ..
    1.77 +  thus ?thesis
    1.78 +    by (simp only: mod_add_eq [symmetric])
    1.79 +qed
    1.80 +
    1.81 +text {* Multiplication respects modular equivalence. *}
    1.82 +
    1.83 +lemma mod_mult_left_eq: "(a * b) mod c = ((a mod c) * b) mod c"
    1.84 +proof -
    1.85 +  have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
    1.86 +    by (simp only: mod_div_equality)
    1.87 +  also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
    1.88 +    by (simp only: left_distrib right_distrib add_ac mult_ac)
    1.89 +  also have "\<dots> = (a mod c * b) mod c"
    1.90 +    by (rule mod_mult_self1)
    1.91 +  finally show ?thesis .
    1.92 +qed
    1.93 +
    1.94 +lemma mod_mult_right_eq: "(a * b) mod c = (a * (b mod c)) mod c"
    1.95 +proof -
    1.96 +  have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
    1.97 +    by (simp only: mod_div_equality)
    1.98 +  also have "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c"
    1.99 +    by (simp only: left_distrib right_distrib add_ac mult_ac)
   1.100 +  also have "\<dots> = (a * (b mod c)) mod c"
   1.101 +    by (rule mod_mult_self1)
   1.102 +  finally show ?thesis .
   1.103 +qed
   1.104 +
   1.105 +lemma mod_mult_eq: "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
   1.106 +by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])
   1.107 +
   1.108 +lemma mod_mult_cong:
   1.109 +  assumes "a mod c = a' mod c"
   1.110 +  assumes "b mod c = b' mod c"
   1.111 +  shows "(a * b) mod c = (a' * b') mod c"
   1.112 +proof -
   1.113 +  have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
   1.114 +    unfolding assms ..
   1.115 +  thus ?thesis
   1.116 +    by (simp only: mod_mult_eq [symmetric])
   1.117 +qed
   1.118 +
   1.119  end
   1.120  
   1.121  
   1.122 @@ -467,22 +572,14 @@
   1.123  done
   1.124  
   1.125  lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
   1.126 -apply (cases "c = 0", simp)
   1.127 -apply (blast intro: divmod_rel [THEN divmod_rel_mult1_eq, THEN mod_eq])
   1.128 -done
   1.129 +  by (rule mod_mult_right_eq)
   1.130  
   1.131  lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
   1.132 -  apply (rule trans)
   1.133 -   apply (rule_tac s = "b*a mod c" in trans)
   1.134 -    apply (rule_tac [2] mod_mult1_eq)
   1.135 -   apply (simp_all add: mult_commute)
   1.136 -  done
   1.137 +  by (rule mod_mult_left_eq)
   1.138  
   1.139  lemma mod_mult_distrib_mod:
   1.140    "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
   1.141 -apply (rule mod_mult1_eq' [THEN trans])
   1.142 -apply (rule mod_mult1_eq)
   1.143 -done
   1.144 +  by (rule mod_mult_eq)
   1.145  
   1.146  lemma divmod_rel_add1_eq:
   1.147    "[| divmod_rel a c aq ar; divmod_rel b c bq br;  c > 0 |]
   1.148 @@ -497,9 +594,7 @@
   1.149  done
   1.150  
   1.151  lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
   1.152 -apply (cases "c = 0", simp)
   1.153 -apply (blast intro: divmod_rel_add1_eq [THEN mod_eq] divmod_rel)
   1.154 -done
   1.155 +  by (rule mod_add_eq)
   1.156  
   1.157  lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
   1.158    apply (cut_tac m = q and n = c in mod_less_divisor)
   1.159 @@ -618,11 +713,11 @@
   1.160  apply (auto simp add: Suc_diff_le le_mod_geq)
   1.161  done
   1.162  
   1.163 -lemma nat_mod_div_trivial [simp]: "m mod n div n = (0 :: nat)"
   1.164 -  by (cases "n = 0") auto
   1.165 +lemma nat_mod_div_trivial: "m mod n div n = (0 :: nat)"
   1.166 +  by simp
   1.167  
   1.168 -lemma nat_mod_mod_trivial [simp]: "m mod n mod n = (m mod n :: nat)"
   1.169 -  by (cases "n = 0") auto
   1.170 +lemma nat_mod_mod_trivial: "m mod n mod n = (m mod n :: nat)"
   1.171 +  by simp
   1.172  
   1.173  
   1.174  subsubsection {* The Divides Relation *}
   1.175 @@ -718,18 +813,6 @@
   1.176    apply (simp add: power_add)
   1.177    done
   1.178  
   1.179 -lemma mod_add_left_eq: "((a::nat) + b) mod c = (a mod c + b) mod c"
   1.180 -  apply (rule trans [symmetric])
   1.181 -   apply (rule mod_add1_eq, simp)
   1.182 -  apply (rule mod_add1_eq [symmetric])
   1.183 -  done
   1.184 -
   1.185 -lemma mod_add_right_eq: "(a+b) mod (c::nat) = (a + (b mod c)) mod c"
   1.186 -  apply (rule trans [symmetric])
   1.187 -   apply (rule mod_add1_eq, simp)
   1.188 -  apply (rule mod_add1_eq [symmetric])
   1.189 -  done
   1.190 -
   1.191  lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
   1.192    by (induct n) auto
   1.193  
     2.1 --- a/src/HOL/IntDiv.thy	Wed Jan 07 08:13:56 2009 -0800
     2.2 +++ b/src/HOL/IntDiv.thy	Thu Jan 08 08:24:08 2009 -0800
     2.3 @@ -747,12 +747,12 @@
     2.4  lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
     2.5  by (simp add: zdiv_zmult1_eq)
     2.6  
     2.7 -lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
     2.8 +lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
     2.9  apply (case_tac "b = 0", simp)
    2.10  apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
    2.11  done
    2.12  
    2.13 -lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
    2.14 +lemma zmod_zmod_trivial: "(a mod b) mod b = a mod (b::int)"
    2.15  apply (case_tac "b = 0", simp)
    2.16  apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
    2.17  done
    2.18 @@ -776,63 +776,47 @@
    2.19  apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
    2.20  done
    2.21  
    2.22 -lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
    2.23 -by (simp add: zdiv_zadd1_eq)
    2.24 -
    2.25 -lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
    2.26 -by (simp add: zdiv_zadd1_eq)
    2.27 -
    2.28  instance int :: semiring_div
    2.29  proof
    2.30    fix a b c :: int
    2.31    assume not0: "b \<noteq> 0"
    2.32    show "(a + c * b) div b = c + a div b"
    2.33      unfolding zdiv_zadd1_eq [of a "c * b"] using not0 
    2.34 -      by (simp add: zmod_zmult1_eq)
    2.35 +      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial)
    2.36  qed auto
    2.37  
    2.38 -lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
    2.39 -by (subst mult_commute, erule zdiv_zmult_self1)
    2.40 +lemma zdiv_zadd_self1: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
    2.41 +by (rule div_add_self1) (* already declared [simp] *)
    2.42 +
    2.43 +lemma zdiv_zadd_self2: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
    2.44 +by (rule div_add_self2) (* already declared [simp] *)
    2.45  
    2.46 -lemma zmod_zmult_self1 [simp]: "(a*b) mod b = (0::int)"
    2.47 -by (simp add: zmod_zmult1_eq)
    2.48 +lemma zdiv_zmult_self2: "b \<noteq> (0::int) ==> (b*a) div b = a"
    2.49 +by (rule div_mult_self1_is_id) (* already declared [simp] *)
    2.50  
    2.51 -lemma zmod_zmult_self2 [simp]: "(b*a) mod b = (0::int)"
    2.52 -by (simp add: mult_commute zmod_zmult1_eq)
    2.53 +lemma zmod_zmult_self1: "(a*b) mod b = (0::int)"
    2.54 +by (rule mod_mult_self2_is_0) (* already declared [simp] *)
    2.55 +
    2.56 +lemma zmod_zmult_self2: "(b*a) mod b = (0::int)"
    2.57 +by (rule mod_mult_self1_is_0) (* already declared [simp] *)
    2.58  
    2.59  lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
    2.60 -proof
    2.61 -  assume "m mod d = 0"
    2.62 -  with zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto
    2.63 -next
    2.64 -  assume "EX q::int. m = d*q"
    2.65 -  thus "m mod d = 0" by auto
    2.66 -qed
    2.67 +by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
    2.68  
    2.69 +(* REVISIT: should this be generalized to all semiring_div types? *)
    2.70  lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
    2.71  
    2.72  lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
    2.73 -apply (rule trans [symmetric])
    2.74 -apply (rule zmod_zadd1_eq, simp)
    2.75 -apply (rule zmod_zadd1_eq [symmetric])
    2.76 -done
    2.77 +by (rule mod_add_left_eq)
    2.78  
    2.79  lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c"
    2.80 -apply (rule trans [symmetric])
    2.81 -apply (rule zmod_zadd1_eq, simp)
    2.82 -apply (rule zmod_zadd1_eq [symmetric])
    2.83 -done
    2.84 +by (rule mod_add_right_eq)
    2.85  
    2.86 -lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)"
    2.87 -apply (case_tac "a = 0", simp)
    2.88 -apply (simp add: zmod_zadd1_eq)
    2.89 -done
    2.90 +lemma zmod_zadd_self1: "(a+b) mod a = b mod (a::int)"
    2.91 +by (rule mod_add_self1) (* already declared [simp] *)
    2.92  
    2.93 -lemma zmod_zadd_self2[simp]: "(b+a) mod a = b mod (a::int)"
    2.94 -apply (case_tac "a = 0", simp)
    2.95 -apply (simp add: zmod_zadd1_eq)
    2.96 -done
    2.97 -
    2.98 +lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)"
    2.99 +by (rule mod_add_self2) (* already declared [simp] *)
   2.100  
   2.101  lemma zmod_zdiff1_eq: fixes a::int
   2.102    shows "(a - b) mod c = (a mod c - b mod c) mod c" (is "?l = ?r")