equal
deleted
inserted
replaced
18 qed "zadd_left_cancel0"; |
18 qed "zadd_left_cancel0"; |
19 Addsimps [zadd_left_cancel0]; |
19 Addsimps [zadd_left_cancel0]; |
20 |
20 |
21 |
21 |
22 (* nat *) |
22 (* nat *) |
23 |
|
24 Goal "0 <= z ==> int (nat z) = z"; |
|
25 by (asm_full_simp_tac |
|
26 (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); |
|
27 qed "nat_0_le"; |
|
28 |
|
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); |
|
32 by (asm_full_simp_tac |
|
33 (simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1); |
|
34 qed "nat_le_0"; |
|
35 |
|
36 Addsimps [nat_0_le, nat_le_0]; |
|
37 |
23 |
38 val [major,minor] = Goal "[| 0 <= z; !!m. z = int m ==> P |] ==> P"; |
24 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); |
25 by (rtac (major RS nat_0_le RS sym RS minor) 1); |
40 qed "nonneg_eq_int"; |
26 qed "nonneg_eq_int"; |
41 |
27 |