src/HOL/Integ/Bin.ML
changeset 6989 dd3e8bd86cc6
parent 6973 52f70b76a8b5
child 6997 1833bdd83ebf
equal deleted inserted replaced
6988:eed63543a3af 6989:dd3e8bd86cc6
   265 qed "zmult_2_right";
   265 qed "zmult_2_right";
   266 
   266 
   267 
   267 
   268 (** Inequality reasoning **)
   268 (** Inequality reasoning **)
   269 
   269 
       
   270 Goal "(m*n = (#0::int)) = (m = #0 | n = #0)";
       
   271 by (stac (int_0 RS sym) 1 THEN rtac zmult_eq_int0_iff 1);
       
   272 qed "zmult_eq_0_iff";
       
   273 
   270 Goal "(w < z + (#1::int)) = (w<z | w=z)";
   274 Goal "(w < z + (#1::int)) = (w<z | w=z)";
   271 by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1);
   275 by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1);
   272 qed "zless_add1_eq";
   276 qed "zless_add1_eq";
   273 
   277 
   274 Goal "(w + (#1::int) <= z) = (w<z)";
   278 Goal "(w + (#1::int) <= z) = (w<z)";
   278 
   282 
   279 Goal "neg x = (x < #0)";
   283 Goal "neg x = (x < #0)";
   280 by (simp_tac (simpset() addsimps [neg_eq_less_int0]) 1); 
   284 by (simp_tac (simpset() addsimps [neg_eq_less_int0]) 1); 
   281 qed "neg_eq_less_0"; 
   285 qed "neg_eq_less_0"; 
   282 
   286 
   283 Goal "(~neg x) = (int 0 <= x)";
   287 Goal "(~neg x) = (#0 <= x)";
   284 by (simp_tac (simpset() addsimps [not_neg_eq_ge_int0]) 1); 
   288 by (simp_tac (simpset() addsimps [not_neg_eq_ge_int0]) 1); 
   285 qed "not_neg_eq_ge_0"; 
   289 qed "not_neg_eq_ge_0"; 
   286 
   290 
   287 Goal "#0 <= int m";
   291 Goal "#0 <= int m";
   288 by (Simp_tac 1);
   292 by (Simp_tac 1);