# HG changeset patch
# User nipkow
# Date 1234693598 -3600
# Node ID b95f5b8b93dd4378107a0f26318e22f99c3c0ac8
# Parent  1e07290c46c3786497c6ec501e092bd0e5faac1d
more finiteness

diff -r 1e07290c46c3 -r b95f5b8b93dd src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Feb 15 07:54:46 2009 +0100
+++ b/src/HOL/Finite_Set.thy	Sun Feb 15 11:26:38 2009 +0100
@@ -140,6 +140,9 @@
   "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
 by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
 
+lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}"
+by(fastsimp simp: finite_conv_nat_seg_image)
+
 
 subsubsection{* Finiteness and set theoretic constructions *}
 
@@ -189,6 +192,9 @@
   -- {* The converse obviously fails. *}
 by(simp add:Collect_conj_eq)
 
+lemma finite_Collect_le_nat[iff]: "finite{n::nat. n<=k}"
+by(simp add: le_eq_less_or_eq)
+
 lemma finite_insert [simp]: "finite (insert a A) = finite A"
   apply (subst insert_is_Un)
   apply (simp only: finite_Un, blast)
@@ -329,6 +335,19 @@
   "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
 by (blast intro: finite_UN_I finite_subset)
 
+lemma finite_Collect_bex[simp]: "finite A \<Longrightarrow>
+  finite{x. EX y:A. Q x y} = (ALL y:A. finite{x. Q x y})"
+apply(subgoal_tac "{x. EX y:A. Q x y} = UNION A (%y. {x. Q x y})")
+ apply auto
+done
+
+lemma finite_Collect_bounded_ex[simp]: "finite{y. P y} \<Longrightarrow>
+  finite{x. EX y. P y & Q x y} = (ALL y. P y \<longrightarrow> finite{x. Q x y})"
+apply(subgoal_tac "{x. EX y. P y & Q x y} = UNION {y. P y} (%y. {x. Q x y})")
+ apply auto
+done
+
+
 lemma finite_Plus: "[| finite A; finite B |] ==> finite (A <+> B)"
 by (simp add: Plus_def)
 
@@ -396,11 +415,6 @@
 lemma finite_Collect_subsets[simp,intro]: "finite A \<Longrightarrow> finite{B. B \<subseteq> A}"
 by(simp add: Pow_def[symmetric])
 
-lemma finite_bex_subset[simp]:
-  "finite B \<Longrightarrow> finite{x. EX A<=B. P x A} = (ALL A<=B. finite{x. P x A})"
-apply(subgoal_tac "{x. EX A<=B. P x A} = (UN A:Pow B. {x. P x A})")
- apply auto
-done
 
 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
 by(blast intro: finite_subset[OF subset_Pow_Union])
diff -r 1e07290c46c3 -r b95f5b8b93dd src/HOL/NSA/HyperNat.thy
--- a/src/HOL/NSA/HyperNat.thy	Sun Feb 15 07:54:46 2009 +0100
+++ b/src/HOL/NSA/HyperNat.thy	Sun Feb 15 11:26:38 2009 +0100
@@ -286,11 +286,10 @@
 by (simp add: HNatInfinite_def)
 
 lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
-apply (insert finite_atMost [of m]) 
-apply (simp add: atMost_def)
+apply (insert finite_atMost [of m])
 apply (drule FreeUltrafilterNat.finite)
 apply (drule FreeUltrafilterNat.not_memD)
-apply (simp add: Collect_neg_eq [symmetric] linorder_not_le)
+apply (simp add: Collect_neg_eq [symmetric] linorder_not_le atMost_def)
 done
 
 lemma Compl_Collect_le: "- {n::nat. N \<le> n} = {n. n < N}"
diff -r 1e07290c46c3 -r b95f5b8b93dd src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Sun Feb 15 07:54:46 2009 +0100
+++ b/src/HOL/SetInterval.thy	Sun Feb 15 11:26:38 2009 +0100
@@ -568,7 +568,6 @@
 apply auto
 apply (case_tac xa)
 apply auto
-apply (auto simp add: finite_M_bounded_by_nat)
 done
 
 lemma card_less_Suc:
diff -r 1e07290c46c3 -r b95f5b8b93dd src/HOL/ex/Sublist.thy
--- a/src/HOL/ex/Sublist.thy	Sun Feb 15 07:54:46 2009 +0100
+++ b/src/HOL/ex/Sublist.thy	Sun Feb 15 11:26:38 2009 +0100
@@ -64,8 +64,6 @@
       apply (simp add: sublist_Cons)
       apply auto
       apply (auto simp add: nat.split)
-      apply (simp add: card_less)
-      apply (simp add: card_less)
       apply (simp add: card_less_Suc[symmetric])
       apply (simp add: card_less_Suc2)
       done