src/HOL/IntDiv.thy
changeset 29951 a70bc5190534
parent 29950 32db77615915
parent 29948 cdf12a1cb963
child 29981 7d0ed261b712
child 30240 5b25fee0362c
     1.1 --- a/src/HOL/IntDiv.thy	Tue Feb 17 07:13:29 2009 -0800
     1.2 +++ b/src/HOL/IntDiv.thy	Tue Feb 17 10:52:55 2009 -0800
     1.3 @@ -451,9 +451,6 @@
     1.4  lemma zmod_zero [simp]: "(0::int) mod b = 0"
     1.5  by (simp add: mod_def divmod_def)
     1.6  
     1.7 -lemma zdiv_minus1: "(0::int) < b ==> -1 div b = -1"
     1.8 -by (simp add: div_def divmod_def)
     1.9 -
    1.10  lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
    1.11  by (simp add: mod_def divmod_def)
    1.12  
    1.13 @@ -729,18 +726,6 @@
    1.14  apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod])
    1.15  done
    1.16  
    1.17 -lemma zmod_zmult1_eq': "(a*b) mod (c::int) = ((a mod c) * b) mod c"
    1.18 -apply (rule trans)
    1.19 -apply (rule_tac s = "b*a mod c" in trans)
    1.20 -apply (rule_tac [2] zmod_zmult1_eq)
    1.21 -apply (simp_all add: mult_commute)
    1.22 -done
    1.23 -
    1.24 -lemma zmod_zmult_distrib: "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c"
    1.25 -apply (rule zmod_zmult1_eq' [THEN trans])
    1.26 -apply (rule zmod_zmult1_eq)
    1.27 -done
    1.28 -
    1.29  lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
    1.30  by (simp add: zdiv_zmult1_eq)
    1.31  
    1.32 @@ -749,11 +734,6 @@
    1.33  apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
    1.34  done
    1.35  
    1.36 -lemma zmod_zmod_trivial: "(a mod b) mod b = a mod (b::int)"
    1.37 -apply (case_tac "b = 0", simp)
    1.38 -apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
    1.39 -done
    1.40 -
    1.41  text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
    1.42  
    1.43  lemma zadd1_lemma:
    1.44 @@ -768,11 +748,6 @@
    1.45  apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_div)
    1.46  done
    1.47  
    1.48 -lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
    1.49 -apply (case_tac "c = 0", simp)
    1.50 -apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_mod)
    1.51 -done
    1.52 -
    1.53  instance int :: ring_div
    1.54  proof
    1.55    fix a b c :: int
    1.56 @@ -971,7 +946,7 @@
    1.57      P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
    1.58  apply (rule iffI, clarify)
    1.59   apply (erule_tac P="P ?x ?y" in rev_mp)  
    1.60 - apply (subst zmod_zadd1_eq) 
    1.61 + apply (subst mod_add_eq) 
    1.62   apply (subst zdiv_zadd1_eq) 
    1.63   apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)  
    1.64  txt{*converse direction*}
    1.65 @@ -984,7 +959,7 @@
    1.66      P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
    1.67  apply (rule iffI, clarify)
    1.68   apply (erule_tac P="P ?x ?y" in rev_mp)  
    1.69 - apply (subst zmod_zadd1_eq) 
    1.70 + apply (subst mod_add_eq) 
    1.71   apply (subst zdiv_zadd1_eq) 
    1.72   apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)  
    1.73  txt{*converse direction*}
    1.74 @@ -1057,11 +1032,6 @@
    1.75         simp) 
    1.76  done
    1.77  
    1.78 -(*Not clear why this must be proved separately; probably number_of causes
    1.79 -  simplification problems*)
    1.80 -lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)"
    1.81 -by auto
    1.82 -
    1.83  lemma zdiv_number_of_Bit0 [simp]:
    1.84       "number_of (Int.Bit0 v) div number_of (Int.Bit0 w) =  
    1.85            number_of v div (number_of w :: int)"
    1.86 @@ -1088,7 +1058,7 @@
    1.87   apply (rule_tac [2] mult_left_mono)
    1.88  apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq 
    1.89                        pos_mod_bound)
    1.90 -apply (subst zmod_zadd1_eq)
    1.91 +apply (subst mod_add_eq)
    1.92  apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
    1.93  apply (rule mod_pos_pos_trivial)
    1.94  apply (auto simp add: mod_pos_pos_trivial ring_distribs)
    1.95 @@ -1111,7 +1081,7 @@
    1.96        (2::int) * (number_of v mod number_of w)"
    1.97  apply (simp only: number_of_eq numeral_simps) 
    1.98  apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
    1.99 -                 not_0_le_lemma neg_zmod_mult_2 add_ac)
   1.100 +                 neg_zmod_mult_2 add_ac)
   1.101  done
   1.102  
   1.103  lemma zmod_number_of_Bit1 [simp]:
   1.104 @@ -1121,7 +1091,7 @@
   1.105                  else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
   1.106  apply (simp only: number_of_eq numeral_simps) 
   1.107  apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
   1.108 -                 not_0_le_lemma neg_zmod_mult_2 add_ac)
   1.109 +                 neg_zmod_mult_2 add_ac)
   1.110  done
   1.111  
   1.112  
   1.113 @@ -1131,7 +1101,7 @@
   1.114  apply (subgoal_tac "a div b \<le> -1", force)
   1.115  apply (rule order_trans)
   1.116  apply (rule_tac a' = "-1" in zdiv_mono1)
   1.117 -apply (auto simp add: zdiv_minus1)
   1.118 +apply (auto simp add: div_eq_minus1)
   1.119  done
   1.120  
   1.121  lemma div_nonneg_neg_le0: "[| (0::int) \<le> a;  b < 0 |] ==> a div b \<le> 0"
   1.122 @@ -1379,7 +1349,7 @@
   1.123  apply (induct "y", auto)
   1.124  apply (rule zmod_zmult1_eq [THEN trans])
   1.125  apply (simp (no_asm_simp))
   1.126 -apply (rule zmod_zmult_distrib [symmetric])
   1.127 +apply (rule mod_mult_eq [symmetric])
   1.128  done
   1.129  
   1.130  lemma zdiv_int: "int (a div b) = (int a) div (int b)"
   1.131 @@ -1420,7 +1390,7 @@
   1.132    IntDiv.zmod_zadd_left_eq  [symmetric]
   1.133    IntDiv.zmod_zadd_right_eq [symmetric]
   1.134    IntDiv.zmod_zmult1_eq     [symmetric]
   1.135 -  IntDiv.zmod_zmult1_eq'    [symmetric]
   1.136 +  mod_mult_left_eq          [symmetric]
   1.137    IntDiv.zpower_zmod
   1.138    zminus_zmod zdiff_zmod_left zdiff_zmod_right
   1.139