new lemma less_Suc_eq_0_disj
authorpaulson
Thu Jun 10 10:34:55 1999 +0200 (1999-06-10)
changeset 680552b13dfbe954
parent 6804 66dc8e62a987
child 6806 43c081a0858d
new lemma less_Suc_eq_0_disj
src/HOL/Nat.ML
     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 _ => [