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.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.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.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
```