src/HOL/Integ/int_arith2.ML

sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
"num" syntax (still with "#"), Numeral0, Numeral1;

(*  Title:      HOL/Integ/int_arith2.ML
    ID:         $Id$
    Authors:    Larry Paulson and Tobias Nipkow
*)

(** Simplification of inequalities involving numerical constants **)

Goal "(w <= z - (Numeral1::int)) = (w<(z::int))";
by (arith_tac 1);
qed "zle_diff1_eq";
Addsimps [zle_diff1_eq];

Goal "(w < z + Numeral1) = (w<=(z::int))";
by (arith_tac 1);
qed "zle_add1_eq_le";
Addsimps [zle_add1_eq_le];

Goal "(z = z + w) = (w = (Numeral0::int))";
by (arith_tac 1);
qed "zadd_left_cancel0";
Addsimps [zadd_left_cancel0];


(* nat *)

Goal "Numeral0 <= z ==> int (nat z) = z"; 
by (asm_full_simp_tac
    (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); 
qed "nat_0_le"; 

Goal "z <= Numeral0 ==> nat z = 0"; 
by (case_tac "z = Numeral0" 1);
by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1); 
by (asm_full_simp_tac 
    (simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1);
qed "nat_le_0"; 

Addsimps [nat_0_le, nat_le_0];

val [major,minor] = Goal "[| Numeral0 <= z;  !!m. z = int m ==> P |] ==> P"; 
by (rtac (major RS nat_0_le RS sym RS minor) 1);
qed "nonneg_eq_int"; 

Goal "(nat w = m) = (if Numeral0 <= w then w = int m else m=0)";
by Auto_tac;
qed "nat_eq_iff";

Goal "(m = nat w) = (if Numeral0 <= w then w = int m else m=0)";
by Auto_tac;
qed "nat_eq_iff2";

Goal "Numeral0 <= w ==> (nat w < m) = (w < int m)";
by (rtac iffI 1);
by (asm_full_simp_tac 
    (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2);
by (etac (nat_0_le RS subst) 1);
by (Simp_tac 1);
qed "nat_less_iff";

Goal "(int m = z) = (m = nat z & Numeral0 <= z)";
by (auto_tac (claset(), simpset() addsimps [nat_eq_iff2]));  
qed "int_eq_iff";

Addsimps [inst "z" "number_of ?v" int_eq_iff];


(*Users don't want to see (int 0), int(Suc 0) or w + - z*)
Addsimps [int_0, int_Suc, symmetric zdiff_def];

Goal "nat Numeral0 = 0";
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
qed "nat_0";

Goal "nat Numeral1 = Suc 0";
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
qed "nat_1";

Goal "nat # 2 = Suc (Suc 0)";
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
qed "nat_2";

Goal "Numeral0 <= w ==> (nat w < nat z) = (w<z)";
by (case_tac "neg z" 1);
by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
by (auto_tac (claset() addIs [zless_trans], 
	      simpset() addsimps [neg_eq_less_0, zle_def]));
qed "nat_less_eq_zless";

Goal "Numeral0 < w | Numeral0 <= z ==> (nat w <= nat z) = (w<=z)";
by (auto_tac (claset(), 
	      simpset() addsimps [linorder_not_less RS sym, 
				  zless_nat_conj]));
qed "nat_le_eq_zle";

(*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*)
Goal "n<=m --> int m - int n = int (m-n)";
by (induct_thm_tac diff_induct "m n" 1);
by Auto_tac;
qed_spec_mp "zdiff_int";


(*** abs: absolute value, as an integer ****)

(* Simpler: use zabs_def as rewrite rule;
   but arith_tac is not parameterized by such simp rules
*)

Goalw [zabs_def]
 "P(abs(i::int)) = ((Numeral0 <= i --> P i) & (i < Numeral0 --> P(-i)))";
by(Simp_tac 1);
qed "zabs_split";

Goal "Numeral0 <= abs (z::int)";
by (simp_tac (simpset() addsimps [zabs_def]) 1); 
qed "zero_le_zabs";
AddIffs [zero_le_zabs];

(*continued in IntArith.ML ...*)