354 by (auto_tac (claset(), simpset() addsimps [neg_nat])); |
354 by (auto_tac (claset(), simpset() addsimps [neg_nat])); |
355 by (auto_tac (claset() addDs [order_less_trans], |
355 by (auto_tac (claset() addDs [order_less_trans], |
356 simpset() addsimps [neg_eq_less_0])); |
356 simpset() addsimps [neg_eq_less_0])); |
357 qed "zless_nat_eq_int_zless"; |
357 qed "zless_nat_eq_int_zless"; |
358 |
358 |
|
359 Goal "0 <= z ==> int (nat z) = z"; |
|
360 by (asm_full_simp_tac |
|
361 (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); |
|
362 qed "nat_0_le"; |
|
363 |
359 Goal "z <= 0 ==> nat z = 0"; |
364 Goal "z <= 0 ==> nat z = 0"; |
360 by (auto_tac (claset(), |
365 by (auto_tac (claset(), |
361 simpset() addsimps [order_le_less, neg_eq_less_0, |
366 simpset() addsimps [order_le_less, neg_eq_less_0, |
362 zle_def, neg_nat])); |
367 zle_def, neg_nat])); |
363 qed "nat_le_int0"; |
368 qed "nat_le_0"; |
|
369 Addsimps [nat_0_le, nat_le_0]; |
364 |
370 |
365 (*An alternative condition is 0 <= w *) |
371 (*An alternative condition is 0 <= w *) |
366 Goal "0 < z ==> (nat w < nat z) = (w < z)"; |
372 Goal "0 < z ==> (nat w < nat z) = (w < z)"; |
367 by (stac (zless_int RS sym) 1); |
373 by (stac (zless_int RS sym) 1); |
368 by (asm_simp_tac (simpset() addsimps [not_neg_nat, not_neg_eq_ge_0, |
374 by (asm_simp_tac (simpset() addsimps [not_neg_nat, not_neg_eq_ge_0, |
373 by (blast_tac (claset() addIs [order_less_trans]) 1); |
379 by (blast_tac (claset() addIs [order_less_trans]) 1); |
374 val lemma = result(); |
380 val lemma = result(); |
375 |
381 |
376 Goal "(nat w < nat z) = (0 < z & w < z)"; |
382 Goal "(nat w < nat z) = (0 < z & w < z)"; |
377 by (case_tac "0 < z" 1); |
383 by (case_tac "0 < z" 1); |
378 by (auto_tac (claset(), |
384 by (auto_tac (claset(), simpset() addsimps [lemma, linorder_not_less])); |
379 simpset() addsimps [lemma, nat_le_int0, linorder_not_less])); |
|
380 qed "zless_nat_conj"; |
385 qed "zless_nat_conj"; |
381 |
386 |
382 |
387 |
383 (* a case theorem distinguishing non-negative and negative int *) |
388 (* a case theorem distinguishing non-negative and negative int *) |
384 |
389 |