Cleaned up IntDiv and removed subsumed lemmas.
authornipkow
Tue Feb 17 18:48:17 2009 +0100 (2009-02-17)
changeset 29948cdf12a1cb963
parent 29947 0a51765d2084
child 29951 a70bc5190534
Cleaned up IntDiv and removed subsumed lemmas.
src/HOL/Algebra/IntRing.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Divides.thy
src/HOL/IntDiv.thy
src/HOL/NumberTheory/Chinese.thy
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/NumberTheory/Residues.thy
src/HOL/Tools/Qelim/presburger.ML
src/HOL/Word/Num_Lemmas.thy
src/HOL/Word/WordGenLib.thy
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Mon Feb 16 19:35:52 2009 -0800
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Tue Feb 17 18:48:17 2009 +0100
     1.3 @@ -407,7 +407,7 @@
     1.4  
     1.5    hence "b mod m = (x * m + a) mod m" by simp
     1.6    also
     1.7 -      have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq)
     1.8 +      have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: mod_add_eq)
     1.9    also
    1.10        have "\<dots> = a mod m" by simp
    1.11    finally
     2.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Mon Feb 16 19:35:52 2009 -0800
     2.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Tue Feb 17 18:48:17 2009 +0100
     2.3 @@ -30,7 +30,7 @@
     2.4  val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
     2.5  val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
     2.6  val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
     2.7 -val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
     2.8 +val int_mod_add_eq = @{thm mod_add_eq} RS sym;
     2.9  val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
    2.10  val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
    2.11  val nat_div_add_eq = @{thm div_add1_eq} RS sym;
     3.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Mon Feb 16 19:35:52 2009 -0800
     3.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Feb 17 18:48:17 2009 +0100
     3.3 @@ -34,7 +34,7 @@
     3.4  val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
     3.5  val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
     3.6  val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
     3.7 -val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
     3.8 +val int_mod_add_eq = @{thm mod_add_eq} RS sym;
     3.9  val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
    3.10  val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
    3.11  val nat_div_add_eq = @{thm div_add1_eq} RS sym;
     4.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Mon Feb 16 19:35:52 2009 -0800
     4.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Tue Feb 17 18:48:17 2009 +0100
     4.3 @@ -49,7 +49,7 @@
     4.4  val nat_mod_add_eq = @{thm "mod_add1_eq"} RS sym;
     4.5  val nat_mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
     4.6  val nat_mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
     4.7 -val int_mod_add_eq = @{thm "zmod_zadd1_eq"} RS sym;
     4.8 +val int_mod_add_eq = @{thm "mod_add_eq"} RS sym;
     4.9  val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
    4.10  val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
    4.11  val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
     5.1 --- a/src/HOL/Divides.thy	Mon Feb 16 19:35:52 2009 -0800
     5.2 +++ b/src/HOL/Divides.thy	Tue Feb 17 18:48:17 2009 +0100
     5.3 @@ -173,7 +173,7 @@
     5.4  qed
     5.5  
     5.6  lemma dvd_imp_mod_0: "a dvd b \<Longrightarrow> b mod a = 0"
     5.7 -by (unfold dvd_def, auto)
     5.8 +by (rule dvd_eq_mod_eq_0[THEN iffD1])
     5.9  
    5.10  lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
    5.11  by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)
     6.1 --- a/src/HOL/IntDiv.thy	Mon Feb 16 19:35:52 2009 -0800
     6.2 +++ b/src/HOL/IntDiv.thy	Tue Feb 17 18:48:17 2009 +0100
     6.3 @@ -451,9 +451,6 @@
     6.4  lemma zmod_zero [simp]: "(0::int) mod b = 0"
     6.5  by (simp add: mod_def divmod_def)
     6.6  
     6.7 -lemma zdiv_minus1: "(0::int) < b ==> -1 div b = -1"
     6.8 -by (simp add: div_def divmod_def)
     6.9 -
    6.10  lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
    6.11  by (simp add: mod_def divmod_def)
    6.12  
    6.13 @@ -729,18 +726,6 @@
    6.14  apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod])
    6.15  done
    6.16  
    6.17 -lemma zmod_zmult1_eq': "(a*b) mod (c::int) = ((a mod c) * b) mod c"
    6.18 -apply (rule trans)
    6.19 -apply (rule_tac s = "b*a mod c" in trans)
    6.20 -apply (rule_tac [2] zmod_zmult1_eq)
    6.21 -apply (simp_all add: mult_commute)
    6.22 -done
    6.23 -
    6.24 -lemma zmod_zmult_distrib: "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c"
    6.25 -apply (rule zmod_zmult1_eq' [THEN trans])
    6.26 -apply (rule zmod_zmult1_eq)
    6.27 -done
    6.28 -
    6.29  lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
    6.30  by (simp add: zdiv_zmult1_eq)
    6.31  
    6.32 @@ -749,11 +734,6 @@
    6.33  apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
    6.34  done
    6.35  
    6.36 -lemma zmod_zmod_trivial: "(a mod b) mod b = a mod (b::int)"
    6.37 -apply (case_tac "b = 0", simp)
    6.38 -apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
    6.39 -done
    6.40 -
    6.41  text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
    6.42  
    6.43  lemma zadd1_lemma:
    6.44 @@ -768,11 +748,6 @@
    6.45  apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_div)
    6.46  done
    6.47  
    6.48 -lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
    6.49 -apply (case_tac "c = 0", simp)
    6.50 -apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_mod)
    6.51 -done
    6.52 -
    6.53  instance int :: ring_div
    6.54  proof
    6.55    fix a b c :: int
    6.56 @@ -971,7 +946,7 @@
    6.57      P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
    6.58  apply (rule iffI, clarify)
    6.59   apply (erule_tac P="P ?x ?y" in rev_mp)  
    6.60 - apply (subst zmod_zadd1_eq) 
    6.61 + apply (subst mod_add_eq) 
    6.62   apply (subst zdiv_zadd1_eq) 
    6.63   apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)  
    6.64  txt{*converse direction*}
    6.65 @@ -984,7 +959,7 @@
    6.66      P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
    6.67  apply (rule iffI, clarify)
    6.68   apply (erule_tac P="P ?x ?y" in rev_mp)  
    6.69 - apply (subst zmod_zadd1_eq) 
    6.70 + apply (subst mod_add_eq) 
    6.71   apply (subst zdiv_zadd1_eq) 
    6.72   apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)  
    6.73  txt{*converse direction*}
    6.74 @@ -1057,11 +1032,6 @@
    6.75         simp) 
    6.76  done
    6.77  
    6.78 -(*Not clear why this must be proved separately; probably number_of causes
    6.79 -  simplification problems*)
    6.80 -lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)"
    6.81 -by auto
    6.82 -
    6.83  lemma zdiv_number_of_Bit0 [simp]:
    6.84       "number_of (Int.Bit0 v) div number_of (Int.Bit0 w) =  
    6.85            number_of v div (number_of w :: int)"
    6.86 @@ -1088,7 +1058,7 @@
    6.87   apply (rule_tac [2] mult_left_mono)
    6.88  apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq 
    6.89                        pos_mod_bound)
    6.90 -apply (subst zmod_zadd1_eq)
    6.91 +apply (subst mod_add_eq)
    6.92  apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
    6.93  apply (rule mod_pos_pos_trivial)
    6.94  apply (auto simp add: mod_pos_pos_trivial ring_distribs)
    6.95 @@ -1111,7 +1081,7 @@
    6.96        (2::int) * (number_of v mod number_of w)"
    6.97  apply (simp only: number_of_eq numeral_simps) 
    6.98  apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
    6.99 -                 not_0_le_lemma neg_zmod_mult_2 add_ac)
   6.100 +                 neg_zmod_mult_2 add_ac)
   6.101  done
   6.102  
   6.103  lemma zmod_number_of_Bit1 [simp]:
   6.104 @@ -1121,7 +1091,7 @@
   6.105                  else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
   6.106  apply (simp only: number_of_eq numeral_simps) 
   6.107  apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
   6.108 -                 not_0_le_lemma neg_zmod_mult_2 add_ac)
   6.109 +                 neg_zmod_mult_2 add_ac)
   6.110  done
   6.111  
   6.112  
   6.113 @@ -1131,7 +1101,7 @@
   6.114  apply (subgoal_tac "a div b \<le> -1", force)
   6.115  apply (rule order_trans)
   6.116  apply (rule_tac a' = "-1" in zdiv_mono1)
   6.117 -apply (auto simp add: zdiv_minus1)
   6.118 +apply (auto simp add: div_eq_minus1)
   6.119  done
   6.120  
   6.121  lemma div_nonneg_neg_le0: "[| (0::int) \<le> a;  b < 0 |] ==> a div b \<le> 0"
   6.122 @@ -1379,7 +1349,7 @@
   6.123  apply (induct "y", auto)
   6.124  apply (rule zmod_zmult1_eq [THEN trans])
   6.125  apply (simp (no_asm_simp))
   6.126 -apply (rule zmod_zmult_distrib [symmetric])
   6.127 +apply (rule mod_mult_eq [symmetric])
   6.128  done
   6.129  
   6.130  lemma zdiv_int: "int (a div b) = (int a) div (int b)"
   6.131 @@ -1420,7 +1390,7 @@
   6.132    IntDiv.zmod_zadd_left_eq  [symmetric]
   6.133    IntDiv.zmod_zadd_right_eq [symmetric]
   6.134    IntDiv.zmod_zmult1_eq     [symmetric]
   6.135 -  IntDiv.zmod_zmult1_eq'    [symmetric]
   6.136 +  mod_mult_left_eq          [symmetric]
   6.137    IntDiv.zpower_zmod
   6.138    zminus_zmod zdiff_zmod_left zdiff_zmod_right
   6.139  
     7.1 --- a/src/HOL/NumberTheory/Chinese.thy	Mon Feb 16 19:35:52 2009 -0800
     7.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Tue Feb 17 18:48:17 2009 +0100
     7.3 @@ -101,7 +101,7 @@
     7.4    apply (induct l)
     7.5     apply auto
     7.6    apply (rule trans)
     7.7 -   apply (rule zmod_zadd1_eq)
     7.8 +   apply (rule mod_add_eq)
     7.9    apply simp
    7.10    apply (rule zmod_zadd_right_eq [symmetric])
    7.11    done
    7.12 @@ -237,10 +237,10 @@
    7.13    apply (unfold lincong_sol_def)
    7.14    apply safe
    7.15      apply (tactic {* stac (thm "zcong_zmod") 3 *})
    7.16 -    apply (tactic {* stac (thm "zmod_zmult_distrib") 3 *})
    7.17 +    apply (tactic {* stac (thm "mod_mult_eq") 3 *})
    7.18      apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *})
    7.19        apply (tactic {* stac (thm "x_sol_lin") 5 *})
    7.20 -        apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *})
    7.21 +        apply (tactic {* stac (thm "mod_mult_eq" RS sym) 7 *})
    7.22          apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *})
    7.23          apply (subgoal_tac [7]
    7.24            "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
     8.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Mon Feb 16 19:35:52 2009 -0800
     8.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Tue Feb 17 18:48:17 2009 +0100
     8.3 @@ -88,7 +88,7 @@
     8.4  
     8.5  lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k) n = zgcd m n"
     8.6    apply (rule zgcd_eq [THEN trans])
     8.7 -  apply (simp add: zmod_zadd1_eq)
     8.8 +  apply (simp add: mod_add_eq)
     8.9    apply (rule zgcd_eq [symmetric])
    8.10    done
    8.11  
     9.1 --- a/src/HOL/NumberTheory/Residues.thy	Mon Feb 16 19:35:52 2009 -0800
     9.2 +++ b/src/HOL/NumberTheory/Residues.thy	Tue Feb 17 18:48:17 2009 +0100
     9.3 @@ -53,7 +53,7 @@
     9.4  lemma StandardRes_prop4: "2 < m 
     9.5       ==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)"
     9.6    by (auto simp add: StandardRes_def zcong_zmod_eq 
     9.7 -                     zmod_zmult_distrib [of x y m])
     9.8 +                     mod_mult_eq [of x y m])
     9.9  
    9.10  lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x"
    9.11    by (auto simp add: StandardRes_def pos_mod_sign)
    10.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Mon Feb 16 19:35:52 2009 -0800
    10.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Tue Feb 17 18:48:17 2009 +0100
    10.3 @@ -124,7 +124,7 @@
    10.4    @ map (symmetric o mk_meta_eq) 
    10.5      [@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"}, 
    10.6       @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
    10.7 -     @{thm "zmod_zadd1_eq"}, @{thm "zmod_zadd_left_eq"}, 
    10.8 +     @{thm "mod_add_eq"}, @{thm "zmod_zadd_left_eq"}, 
    10.9       @{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
   10.10    @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, 
   10.11       @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
    11.1 --- a/src/HOL/Word/Num_Lemmas.thy	Mon Feb 16 19:35:52 2009 -0800
    11.2 +++ b/src/HOL/Word/Num_Lemmas.thy	Tue Feb 17 18:48:17 2009 +0100
    11.3 @@ -121,8 +121,8 @@
    11.4  
    11.5  lemma zmod_zsub_distrib: "((a::int) - b) mod c = (a mod c - b mod c) mod c"
    11.6    apply (unfold diff_int_def)
    11.7 -  apply (rule trans [OF _ zmod_zadd1_eq [symmetric]])
    11.8 -  apply (simp add: zmod_uminus zmod_zadd1_eq [symmetric])
    11.9 +  apply (rule trans [OF _ mod_add_eq [symmetric]])
   11.10 +  apply (simp add: zmod_uminus mod_add_eq [symmetric])
   11.11    done
   11.12  
   11.13  lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c"
   11.14 @@ -162,8 +162,8 @@
   11.15  lemmas nat_minus_mod_plus_right = trans [OF nat_minus_mod mod_0 [symmetric],
   11.16    THEN mod_plus_right [THEN iffD2], standard, simplified]
   11.17  
   11.18 -lemmas push_mods' = zmod_zadd1_eq [standard]
   11.19 -  zmod_zmult_distrib [standard] zmod_zsub_distrib [standard]
   11.20 +lemmas push_mods' = mod_add_eq [standard]
   11.21 +  mod_mult_eq [standard] zmod_zsub_distrib [standard]
   11.22    zmod_uminus [symmetric, standard]
   11.23  
   11.24  lemmas push_mods = push_mods' [THEN eq_reflection, standard]
    12.1 --- a/src/HOL/Word/WordGenLib.thy	Mon Feb 16 19:35:52 2009 -0800
    12.2 +++ b/src/HOL/Word/WordGenLib.thy	Tue Feb 17 18:48:17 2009 +0100
    12.3 @@ -293,9 +293,9 @@
    12.4    shows "(x + y) mod b = z' mod b'"
    12.5  proof -
    12.6    from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
    12.7 -    by (simp add: zmod_zadd1_eq[symmetric])
    12.8 +    by (simp add: mod_add_eq[symmetric])
    12.9    also have "\<dots> = (x' + y') mod b'"
   12.10 -    by (simp add: zmod_zadd1_eq[symmetric])
   12.11 +    by (simp add: mod_add_eq[symmetric])
   12.12    finally show ?thesis by (simp add: 4)
   12.13  qed
   12.14