added nat_induct2
authoroheimb
Wed Dec 18 15:10:33 1996 +0100 (1996-12-18)
changeset 2441decc46a5cdb5
parent 2440 b3ac45aba238
child 2442 6663e0d210b0
added nat_induct2
src/HOL/Nat.ML
     1.1 --- a/src/HOL/Nat.ML	Wed Dec 18 14:31:27 1996 +0100
     1.2 +++ b/src/HOL/Nat.ML	Wed Dec 18 15:10:33 1996 +0100
     1.3 @@ -1,9 +1,9 @@
     1.4 -(*  Title:      HOL/nat
     1.5 +(*  Title:      HOL/Nat.ML
     1.6      ID:         $Id$
     1.7      Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     1.8      Copyright   1991  University of Cambridge
     1.9  
    1.10 -For nat.thy.  Type nat is defined as a set (Nat) over the type ind.
    1.11 +For Nat.thy.  Type nat is defined as a set (Nat) over the type ind.
    1.12  *)
    1.13  
    1.14  open Nat;
    1.15 @@ -380,6 +380,23 @@
    1.16  by (eresolve_tac prems 1);
    1.17  qed "less_induct";
    1.18  
    1.19 +qed_goal "nat_induct2" Nat.thy 
    1.20 +"[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [
    1.21 +	cut_facts_tac prems 1,
    1.22 +	rtac less_induct 1,
    1.23 +	res_inst_tac [("n","n")] natE 1,
    1.24 +	 hyp_subst_tac 1,
    1.25 +	 atac 1,
    1.26 +	hyp_subst_tac 1,
    1.27 +	res_inst_tac [("n","x")] natE 1,
    1.28 +	 hyp_subst_tac 1,
    1.29 +	 atac 1,
    1.30 +	hyp_subst_tac 1,
    1.31 +	resolve_tac prems 1,
    1.32 +	dtac spec 1,
    1.33 +	etac mp 1,
    1.34 +	rtac (lessI RS less_trans) 1,
    1.35 +	rtac (lessI RS Suc_mono) 1]);
    1.36  
    1.37  (*** Properties of <= ***)
    1.38  
    1.39 @@ -473,6 +490,8 @@
    1.40  qed "le_SucI";
    1.41  Addsimps[le_SucI];
    1.42  
    1.43 +bind_thm ("le_Suc", not_Suc_n_less_n RS leI);
    1.44 +
    1.45  goalw Nat.thy [le_def] "!!m. m < n ==> m <= (n::nat)";
    1.46  by (fast_tac (!claset addEs [less_asym]) 1);
    1.47  qed "less_imp_le";