src/HOL/Integ/IntArith.thy
changeset 14378 69c4d5997669
parent 14365 3d4df8c166ae
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Integ/IntArith.thy	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Integ/IntArith.thy	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -12,15 +12,11 @@
     1.4  subsection{*Inequality Reasoning for the Arithmetic Simproc*}
     1.5  
     1.6  lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"
     1.7 -  proof (auto simp add: zle_def zless_iff_Suc_zadd) 
     1.8 -  fix m n
     1.9 -  assume "w + 1 = w + (1 + int m) + (1 + int n)"
    1.10 -  hence "(w + 1) + (1 + int (m + n)) = (w + 1) + 0" 
    1.11 -    by (simp add: add_ac zadd_int [symmetric])
    1.12 -  hence "int (Suc(m+n)) = 0" 
    1.13 -    by (simp only: Ring_and_Field.add_left_cancel int_Suc)
    1.14 -  thus False by (simp only: int_eq_0_conv)
    1.15 -  qed
    1.16 +apply (rule eq_Abs_Integ [of z])
    1.17 +apply (rule eq_Abs_Integ [of w])
    1.18 +apply (simp add: linorder_not_le [symmetric] zle int_def zadd One_int_def)
    1.19 +done
    1.20 +
    1.21  
    1.22  use "int_arith1.ML"
    1.23  setup int_arith_setup
    1.24 @@ -86,11 +82,11 @@
    1.25  by (subst nat_eq_iff, simp)
    1.26  
    1.27  lemma nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
    1.28 -apply (case_tac "neg z")
    1.29 +apply (case_tac "z < 0")
    1.30  apply (auto simp add: nat_less_iff)
    1.31 -apply (auto intro: zless_trans simp add: neg_eq_less_0 zle_def)
    1.32  done
    1.33  
    1.34 +
    1.35  lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
    1.36  by (auto simp add: linorder_not_less [symmetric] zless_nat_conj)
    1.37  
    1.38 @@ -229,12 +225,12 @@
    1.39  lemma zmult_eq_self_iff: "(m = m*(n::int)) = (n = 1 | m = 0)"
    1.40  apply auto
    1.41  apply (subgoal_tac "m*1 = m*n")
    1.42 -apply (drule zmult_cancel1 [THEN iffD1], auto)
    1.43 +apply (drule mult_cancel_left [THEN iffD1], auto)
    1.44  done
    1.45  
    1.46  lemma zless_1_zmult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::int)"
    1.47  apply (rule_tac y = "1*n" in order_less_trans)
    1.48 -apply (rule_tac [2] zmult_zless_mono1)
    1.49 +apply (rule_tac [2] mult_strict_right_mono)
    1.50  apply (simp_all (no_asm_simp))
    1.51  done
    1.52