equal
deleted
inserted
replaced
51 by (rtac iffI 1); |
51 by (rtac iffI 1); |
52 by (etac swap 1); |
52 by (etac swap 1); |
53 by (ALLGOALS Asm_full_simp_tac); |
53 by (ALLGOALS Asm_full_simp_tac); |
54 qed "not_gr0"; |
54 qed "not_gr0"; |
55 AddIffs [not_gr0]; |
55 AddIffs [not_gr0]; |
|
56 |
|
57 (*Useful in certain inductive arguments*) |
|
58 Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))"; |
|
59 by (exhaust_tac "m" 1); |
|
60 by Auto_tac; |
|
61 qed "less_Suc_eq_0_disj"; |
56 |
62 |
57 qed_goalw "Least_Suc" thy [Least_nat_def] |
63 qed_goalw "Least_Suc" thy [Least_nat_def] |
58 "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" |
64 "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" |
59 (fn _ => [ |
65 (fn _ => [ |
60 rtac select_equality 1, |
66 rtac select_equality 1, |