# HG changeset patch
# User nipkow
# Date 958840641 -7200
# Node ID 2ec6371fde543e579bc1b65a0713a743ce27afd5
# Parent  343c304e714acd2d62415b5130a7044129dbf012
added lemma.

diff -r 343c304e714a -r 2ec6371fde54 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Sat May 20 15:15:02 2000 +0200
+++ b/src/HOL/Finite.ML	Sat May 20 18:37:21 2000 +0200
@@ -213,6 +213,23 @@
 qed "finite_converse";
 AddIffs [finite_converse];
 
+(* A bounded set of natural numbers is finite *)
+Goal "!N. (!i:N. i<(n::nat)) --> finite N";
+by(induct_tac "n" 1);
+ by(Simp_tac 1);
+by(asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
+br allI 1;
+by(case_tac "n : N" 1);
+ by(ftac insert_Diff 1);
+ by(etac subst 1);
+ br impI 1;
+ br (finite_insert RS iffD2) 1;
+ by(EVERY1[etac allE, etac mp]);
+ by(Blast_tac 1);
+by(Blast_tac 1);
+qed_spec_mp "bounded_nat_set_is_finite";
+
+
 section "Finite cardinality -- 'card'";
 
 (* Ugly proofs for the traditional definition