equal
deleted
inserted
replaced
43 qed "zero_neq_conv"; |
43 qed "zero_neq_conv"; |
44 AddIffs [zero_neq_conv]; |
44 AddIffs [zero_neq_conv]; |
45 |
45 |
46 (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *) |
46 (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *) |
47 bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1); |
47 bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1); |
|
48 |
|
49 Goal "(0<n) = (EX m. n = Suc m)"; |
|
50 by(fast_tac (claset() addIs [not0_implies_Suc]) 1); |
|
51 qed "gr0_conv_Suc"; |
48 |
52 |
49 Goal "(~(0 < n)) = (n=0)"; |
53 Goal "(~(0 < n)) = (n=0)"; |
50 by (rtac iffI 1); |
54 by (rtac iffI 1); |
51 by (etac swap 1); |
55 by (etac swap 1); |
52 by (ALLGOALS Asm_full_simp_tac); |
56 by (ALLGOALS Asm_full_simp_tac); |