src/HOL/Integ/IntDiv.thy
changeset 14378 69c4d5997669
parent 14353 79f9fbef9106
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Integ/IntDiv.thy	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Integ/IntDiv.thy	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -531,7 +531,7 @@
     1.4   prefer 2 apply simp
     1.5  apply (simp (no_asm_simp) add: zadd_zmult_distrib2)
     1.6  apply (subst zadd_commute, rule zadd_zless_mono, arith)
     1.7 -apply (rule zmult_zle_mono1, auto)
     1.8 +apply (rule mult_right_mono, auto)
     1.9  done
    1.10  
    1.11  lemma zdiv_mono2:
    1.12 @@ -561,7 +561,7 @@
    1.13   apply (simp add: zmult_zless_cancel1)
    1.14  apply (simp add: zadd_zmult_distrib2)
    1.15  apply (subgoal_tac "b*q' \<le> b'*q'")
    1.16 - prefer 2 apply (simp add: zmult_zle_mono1_neg)
    1.17 + prefer 2 apply (simp add: mult_right_mono_neg)
    1.18  apply (subgoal_tac "b'*q' < b + b*q")
    1.19   apply arith
    1.20  apply simp 
    1.21 @@ -702,8 +702,8 @@
    1.22  apply (subgoal_tac "b * (c - q mod c) < r * 1")
    1.23  apply (simp add: zdiff_zmult_distrib2)
    1.24  apply (rule order_le_less_trans)
    1.25 -apply (erule_tac [2] zmult_zless_mono1)
    1.26 -apply (rule zmult_zle_mono2_neg)
    1.27 +apply (erule_tac [2] mult_strict_right_mono)
    1.28 +apply (rule mult_left_mono_neg)
    1.29  apply (auto simp add: compare_rls zadd_commute [of 1]
    1.30                        add1_zle_eq pos_mod_bound)
    1.31  done
    1.32 @@ -724,7 +724,7 @@
    1.33  apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
    1.34  apply (simp add: zdiff_zmult_distrib2)
    1.35  apply (rule order_less_le_trans)
    1.36 -apply (erule zmult_zless_mono1)
    1.37 +apply (erule mult_strict_right_mono)
    1.38  apply (rule_tac [2] zmult_zle_mono2)
    1.39  apply (auto simp add: compare_rls zadd_commute [of 1]
    1.40                        add1_zle_eq pos_mod_bound)
    1.41 @@ -1111,7 +1111,7 @@
    1.42    apply (unfold dvd_def, auto)
    1.43    apply (subgoal_tac "0 < n")
    1.44     prefer 2
    1.45 -   apply (blast intro: zless_trans)
    1.46 +   apply (blast intro: order_less_trans)
    1.47    apply (simp add: zero_less_mult_iff)
    1.48    apply (subgoal_tac "n * k < n * 1")
    1.49     apply (drule zmult_zless_cancel1 [THEN iffD1], auto)
    1.50 @@ -1150,7 +1150,7 @@
    1.51  
    1.52  lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
    1.53    apply (auto simp add: dvd_def)
    1.54 -   apply (drule zminus_equation [THEN iffD1])
    1.55 +   apply (drule minus_equation_iff [THEN iffD1])
    1.56     apply (rule_tac [!] x = "-k" in exI, auto)
    1.57    done
    1.58