src/HOL/Integ/Bin.ML
 changeset 6989 dd3e8bd86cc6 parent 6973 52f70b76a8b5 child 6997 1833bdd83ebf
equal 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);`