src/HOL/Nat.ML
changeset 6805 52b13dfbe954
parent 6433 228237ec56e5
child 7058 8dfea70eb6b7
     1.1 --- a/src/HOL/Nat.ML	Thu Jun 10 10:24:32 1999 +0200
     1.2 +++ b/src/HOL/Nat.ML	Thu Jun 10 10:34:55 1999 +0200
     1.3 @@ -54,6 +54,12 @@
     1.4  qed "not_gr0";
     1.5  AddIffs [not_gr0];
     1.6  
     1.7 +(*Useful in certain inductive arguments*)
     1.8 +Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
     1.9 +by (exhaust_tac "m" 1);
    1.10 +by Auto_tac;
    1.11 +qed "less_Suc_eq_0_disj";
    1.12 +
    1.13  qed_goalw "Least_Suc" thy [Least_nat_def]
    1.14   "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
    1.15   (fn _ => [