src/HOL/NumberTheory/Quadratic_Reciprocity.thy
changeset 14387 e96d5c42c4b0
parent 14353 79f9fbef9106
child 14434 5f14c1207499
     1.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Sat Feb 14 02:06:12 2004 +0100
     1.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Sun Feb 15 10:46:37 2004 +0100
     1.3 @@ -320,7 +320,7 @@
     1.4    proof -;
     1.5      assume "b \<le> q * a div p";
     1.6      then have "p * b \<le> p * ((q * a) div p)";
     1.7 -      by (insert p_g_2, auto simp add: zmult_zle_cancel1)
     1.8 +      by (insert p_g_2, auto simp add: mult_le_cancel_left)
     1.9      also have "... \<le> q * a";
    1.10        by (rule zdiv_leq_prop, insert p_g_2, auto)
    1.11      finally have "p * b \<le> q * a" .;
    1.12 @@ -353,7 +353,7 @@
    1.13    proof -;
    1.14      assume "a \<le> p * b div q";
    1.15      then have "q * a \<le> q * ((p * b) div q)";
    1.16 -      by (insert q_g_2, auto simp add: zmult_zle_cancel1)
    1.17 +      by (insert q_g_2, auto simp add: mult_le_cancel_left)
    1.18      also have "... \<le> p * b";
    1.19        by (rule zdiv_leq_prop, insert q_g_2, auto)
    1.20      finally have "q * a \<le> p * b" .;
    1.21 @@ -425,7 +425,7 @@
    1.22          assume "0 < x" and "x \<le> q * j div p";
    1.23          with j_fact P_set_def  have "j \<le> (p - 1) div 2"; by auto
    1.24          with q_g_2; have "q * j \<le> q * ((p - 1) div 2)";
    1.25 -          by (auto simp add: zmult_zle_cancel1)
    1.26 +          by (auto simp add: mult_le_cancel_left)
    1.27          with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p";
    1.28            by (auto simp add: zdiv_mono1)
    1.29          also from prems have "... \<le> (q - 1) div 2";
    1.30 @@ -437,7 +437,7 @@
    1.31    also have "... = (q * j) div p";
    1.32    proof -;
    1.33      from j_fact P_set_def have "0 \<le> j" by auto
    1.34 -    with q_g_2 have "q * 0 \<le> q * j" by (auto simp only: zmult_zle_mono2)
    1.35 +    with q_g_2 have "q * 0 \<le> q * j" by (auto simp only: mult_left_mono)
    1.36      then have "0 \<le> q * j" by auto
    1.37      then have "0 div p \<le> (q * j) div p";
    1.38        apply (rule_tac a = 0 in zdiv_mono1)
    1.39 @@ -478,7 +478,7 @@
    1.40          assume "0 < x" and "x \<le> p * j div q";
    1.41          with j_fact Q_set_def  have "j \<le> (q - 1) div 2"; by auto
    1.42          with p_g_2; have "p * j \<le> p * ((q - 1) div 2)";
    1.43 -          by (auto simp add: zmult_zle_cancel1)
    1.44 +          by (auto simp add: mult_le_cancel_left)
    1.45          with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q";
    1.46            by (auto simp add: zdiv_mono1)
    1.47          also from prems have "... \<le> (p - 1) div 2";
    1.48 @@ -490,7 +490,7 @@
    1.49    also have "... = (p * j) div q";
    1.50    proof -;
    1.51      from j_fact Q_set_def have "0 \<le> j" by auto
    1.52 -    with p_g_2 have "p * 0 \<le> p * j" by (auto simp only: zmult_zle_mono2)
    1.53 +    with p_g_2 have "p * 0 \<le> p * j" by (auto simp only: mult_left_mono)
    1.54      then have "0 \<le> p * j" by auto
    1.55      then have "0 div q \<le> (p * j) div q";
    1.56        apply (rule_tac a = 0 in zdiv_mono1)