added abs_mult, abs_eq_0, square_nonzero;
authorwenzelm
Thu Nov 16 19:01:39 2000 +0100 (2000-11-16)
changeset 10476dbc181a32702
parent 10475 77fafa07fc8f
child 10477 c21bee84cefe
added abs_mult, abs_eq_0, square_nonzero;
src/HOL/Integ/IntArith.ML
     1.1 --- a/src/HOL/Integ/IntArith.ML	Thu Nov 16 10:47:11 2000 +0100
     1.2 +++ b/src/HOL/Integ/IntArith.ML	Thu Nov 16 19:01:39 2000 +0100
     1.3 @@ -104,6 +104,25 @@
     1.4  qed "zmult_le_0_iff";
     1.5  
     1.6  
     1.7 +Goal "abs (x * y) = abs x * abs (y::int)";
     1.8 +by (simp_tac (simpset () addsplits [zabs_split] addsimps [zmult_less_0_iff, zle_def]) 1);
     1.9 +qed "abs_mult";
    1.10 +
    1.11 +Goal "(abs x = 0) = (x = (0::int))";
    1.12 +by (simp_tac (simpset () addsplits [zabs_split]) 1);
    1.13 +qed "abs_eq_0";
    1.14 +AddIffs [abs_eq_0];
    1.15 +
    1.16 +Goal "#0 <= x * (x::int)";
    1.17 +by (subgoal_tac "(- x) * x <= #0" 1);
    1.18 + by (Asm_full_simp_tac 1);
    1.19 +by (simp_tac (HOL_basic_ss addsimps [zmult_le_0_iff]) 1);
    1.20 +by Auto_tac;
    1.21 +qed "square_nonzero";
    1.22 +Addsimps [square_nonzero];
    1.23 +AddIs [square_nonzero];
    1.24 +
    1.25 +
    1.26  (*** Products and 1, by T. M. Rasmussen ***)
    1.27  
    1.28  Goal "(m = m*(n::int)) = (n = #1 | m = #0)";