# HG changeset patch
# User nipkow
# Date 962890706 -7200
# Node ID b62d5265b9597b90b1206bb63766d117ca3bcf51
# Parent  4313b08b6e1b53c95bf6a888864423f4ee7a7f9a
added zabs to arith_tac

diff -r 4313b08b6e1b -r b62d5265b959 src/HOL/Integ/IntArith.ML
--- a/src/HOL/Integ/IntArith.ML	Thu Jul 06 15:38:00 2000 +0200
+++ b/src/HOL/Integ/IntArith.ML	Thu Jul 06 15:38:26 2000 +0200
@@ -560,16 +560,30 @@
 
 (*** abs: absolute value, as an integer ****)
 
-Goalw [zabs_def] "abs(abs(x::int)) = abs(x)";
+(* Simpler: use zabs_def as rewrite rule;
+   but arith_tac is not parameterized by such simp rules
+*)
+Goalw [zabs_def]
+ "P(abs(i::int)) = ((#0 <= i --> P i) & (i < #0 --> P(-i)))";
 by(Simp_tac 1);
+qed "zabs_split";
+
+arith_tac_split_thms := !arith_tac_split_thms @ [zabs_split];
+
+Goal "abs(abs(x::int)) = abs(x)";
+by(arith_tac 1);
 qed "abs_abs";
 Addsimps [abs_abs];
 
-Goalw [zabs_def] "abs(-(x::int)) = abs(x)";
-by(Simp_tac 1);
+Goal "abs(-(x::int)) = abs(x)";
+by(arith_tac 1);
 qed "abs_minus";
 Addsimps [abs_minus];
 
+Goal "abs(x+y) <= abs(x) + abs(y::int)";
+by(arith_tac 1);
+qed "triangle_ineq";
+
 
 (*** Some convenient biconditionals for products of signs ***)