added Least_Suc2
authoroheimb
Thu May 31 16:50:13 2001 +0200 (2001-05-31)
changeset 113379d6d6a8966b9
parent 11336 fedccaeb5267
child 11338 779d289255f7
added Least_Suc2
src/HOL/Nat.ML
     1.1 --- a/src/HOL/Nat.ML	Thu May 31 16:50:04 2001 +0200
     1.2 +++ b/src/HOL/Nat.ML	Thu May 31 16:50:13 2001 +0200
     1.3 @@ -94,6 +94,11 @@
     1.4  by (blast_tac (claset() addIs [order_antisym]) 1); 
     1.5  qed "Least_Suc";
     1.6  
     1.7 +Goal "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)";
     1.8 +by (eatac (Least_Suc RS ssubst) 1 1);
     1.9 +by (Asm_simp_tac 1);
    1.10 +qed "Least_Suc2";
    1.11 +
    1.12  
    1.13  (** min and max **)
    1.14