1 (* Title: HOL/Integ/int_arith2.ML
3 Authors: Larry Paulson and Tobias Nipkow
6 Goal "(w <= z - (1::int)) = (w<(z::int))";
9 Addsimps [zle_diff1_eq];
11 Goal "(w < z + 1) = (w<=(z::int))";
14 Addsimps [zle_add1_eq_le];
16 Goal "(z = z + w) = (w = (0::int))";
18 qed "zadd_left_cancel0";
19 Addsimps [zadd_left_cancel0];
24 Goal "0 <= z ==> int (nat z) = z";
26 (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1);
29 Goal "z <= 0 ==> nat z = 0";
30 by (case_tac "z = 0" 1);
31 by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1);
33 (simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1);
36 Addsimps [nat_0_le, nat_le_0];
38 val [major,minor] = Goal "[| 0 <= z; !!m. z = int m ==> P |] ==> P";
39 by (rtac (major RS nat_0_le RS sym RS minor) 1);
42 Goal "(nat w = m) = (if 0 <= w then w = int m else m=0)";
46 Goal "(m = nat w) = (if 0 <= w then w = int m else m=0)";
50 Goal "0 <= w ==> (nat w < m) = (w < int m)";
53 (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2);
54 by (etac (nat_0_le RS subst) 1);
58 Goal "(int m = z) = (m = nat z & 0 <= z)";
59 by (auto_tac (claset(), simpset() addsimps [nat_eq_iff2]));
63 (*Users don't want to see (int 0), int(Suc 0) or w + - z*)
64 Addsimps (map symmetric [Zero_int_def, One_int_def, zdiff_def]);
67 by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
71 by (stac nat_eq_iff 1);
75 Goal "nat 2 = Suc (Suc 0)";
76 by (stac nat_eq_iff 1);
80 Goal "0 <= w ==> (nat w < nat z) = (w<z)";
81 by (case_tac "neg z" 1);
82 by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
83 by (auto_tac (claset() addIs [zless_trans],
84 simpset() addsimps [neg_eq_less_0, zle_def]));
85 qed "nat_less_eq_zless";
87 Goal "0 < w | 0 <= z ==> (nat w <= nat z) = (w<=z)";
88 by (auto_tac (claset(),
89 simpset() addsimps [linorder_not_less RS sym,
93 (*** abs: absolute value, as an integer ****)
95 (* Simpler: use zabs_def as rewrite rule;
96 but arith_tac is not parameterized by such simp rules
100 "P(abs(i::int)) = ((0 <= i --> P i) & (i < 0 --> P(-i)))";
104 Goal "0 <= abs (z::int)";
105 by (simp_tac (simpset() addsimps [zabs_def]) 1);
107 AddIffs [zero_le_zabs];
110 (*Not sure why this simprule is required!*)
111 Addsimps [inst "z" "number_of ?v" int_eq_iff];
113 (*continued in IntArith.ML ...*)