# HG changeset patch
# User paulson
# Date 929274896 -7200
# Node ID 30e09714eef5f81439790d25ad8dec1833953581
# Parent  8f7bfd81a4c615f1baee9fad412d47e77813c20a
new finiteness theorems

diff -r 8f7bfd81a4c6 -r 30e09714eef5 src/HOL/UNITY/LessThan.ML
--- a/src/HOL/UNITY/LessThan.ML	Sun Jun 13 13:54:34 1999 +0200
+++ b/src/HOL/UNITY/LessThan.ML	Sun Jun 13 13:54:56 1999 +0200
@@ -28,6 +28,12 @@
 by (simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
 qed "lessThan_Suc_atMost";
 
+Goal "finite (lessThan k)";
+by (induct_tac "k" 1);
+by (simp_tac (simpset() addsimps [lessThan_Suc]) 2);
+by Auto_tac;
+qed "finite_lessThan";
+
 Goal "(UN m. lessThan m) = UNIV";
 by (Blast_tac 1);
 qed "UN_lessThan_UNIV";
@@ -124,6 +130,12 @@
 by (Blast_tac 1);
 qed "atMost_Suc";
 
+Goal "finite (atMost k)";
+by (induct_tac "k" 1);
+by (simp_tac (simpset() addsimps [atMost_Suc]) 2);
+by Auto_tac;
+qed "finite_atMost";
+
 Goal "(UN m. atMost m) = UNIV";
 by (Blast_tac 1);
 qed "UN_atMost_UNIV";