# HG changeset patch
# User oheimb
# Date 850918233 -3600
# Node ID decc46a5cdb58145176418af4dd8a365f33e96cd
# Parent  b3ac45aba238a10e904e6d65bf0892887b83c823
added nat_induct2

diff -r b3ac45aba238 -r decc46a5cdb5 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Wed Dec 18 14:31:27 1996 +0100
+++ b/src/HOL/Nat.ML	Wed Dec 18 15:10:33 1996 +0100
@@ -1,9 +1,9 @@
-(*  Title:      HOL/nat
+(*  Title:      HOL/Nat.ML
     ID:         $Id$
     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-For nat.thy.  Type nat is defined as a set (Nat) over the type ind.
+For Nat.thy.  Type nat is defined as a set (Nat) over the type ind.
 *)
 
 open Nat;
@@ -380,6 +380,23 @@
 by (eresolve_tac prems 1);
 qed "less_induct";
 
+qed_goal "nat_induct2" Nat.thy 
+"[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [
+	cut_facts_tac prems 1,
+	rtac less_induct 1,
+	res_inst_tac [("n","n")] natE 1,
+	 hyp_subst_tac 1,
+	 atac 1,
+	hyp_subst_tac 1,
+	res_inst_tac [("n","x")] natE 1,
+	 hyp_subst_tac 1,
+	 atac 1,
+	hyp_subst_tac 1,
+	resolve_tac prems 1,
+	dtac spec 1,
+	etac mp 1,
+	rtac (lessI RS less_trans) 1,
+	rtac (lessI RS Suc_mono) 1]);
 
 (*** Properties of <= ***)
 
@@ -473,6 +490,8 @@
 qed "le_SucI";
 Addsimps[le_SucI];
 
+bind_thm ("le_Suc", not_Suc_n_less_n RS leI);
+
 goalw Nat.thy [le_def] "!!m. m < n ==> m <= (n::nat)";
 by (fast_tac (!claset addEs [less_asym]) 1);
 qed "less_imp_le";