more finiteness
authornipkow
Sun Feb 15 11:26:38 2009 +0100 (2009-02-15)
changeset 29920b95f5b8b93dd
parent 29919 1e07290c46c3
child 29921 3d50e96bcd6b
more finiteness
src/HOL/Finite_Set.thy
src/HOL/NSA/HyperNat.thy
src/HOL/SetInterval.thy
src/HOL/ex/Sublist.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Sun Feb 15 07:54:46 2009 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Sun Feb 15 11:26:38 2009 +0100
     1.3 @@ -140,6 +140,9 @@
     1.4    "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
     1.5  by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
     1.6  
     1.7 +lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}"
     1.8 +by(fastsimp simp: finite_conv_nat_seg_image)
     1.9 +
    1.10  
    1.11  subsubsection{* Finiteness and set theoretic constructions *}
    1.12  
    1.13 @@ -189,6 +192,9 @@
    1.14    -- {* The converse obviously fails. *}
    1.15  by(simp add:Collect_conj_eq)
    1.16  
    1.17 +lemma finite_Collect_le_nat[iff]: "finite{n::nat. n<=k}"
    1.18 +by(simp add: le_eq_less_or_eq)
    1.19 +
    1.20  lemma finite_insert [simp]: "finite (insert a A) = finite A"
    1.21    apply (subst insert_is_Un)
    1.22    apply (simp only: finite_Un, blast)
    1.23 @@ -329,6 +335,19 @@
    1.24    "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
    1.25  by (blast intro: finite_UN_I finite_subset)
    1.26  
    1.27 +lemma finite_Collect_bex[simp]: "finite A \<Longrightarrow>
    1.28 +  finite{x. EX y:A. Q x y} = (ALL y:A. finite{x. Q x y})"
    1.29 +apply(subgoal_tac "{x. EX y:A. Q x y} = UNION A (%y. {x. Q x y})")
    1.30 + apply auto
    1.31 +done
    1.32 +
    1.33 +lemma finite_Collect_bounded_ex[simp]: "finite{y. P y} \<Longrightarrow>
    1.34 +  finite{x. EX y. P y & Q x y} = (ALL y. P y \<longrightarrow> finite{x. Q x y})"
    1.35 +apply(subgoal_tac "{x. EX y. P y & Q x y} = UNION {y. P y} (%y. {x. Q x y})")
    1.36 + apply auto
    1.37 +done
    1.38 +
    1.39 +
    1.40  lemma finite_Plus: "[| finite A; finite B |] ==> finite (A <+> B)"
    1.41  by (simp add: Plus_def)
    1.42  
    1.43 @@ -396,11 +415,6 @@
    1.44  lemma finite_Collect_subsets[simp,intro]: "finite A \<Longrightarrow> finite{B. B \<subseteq> A}"
    1.45  by(simp add: Pow_def[symmetric])
    1.46  
    1.47 -lemma finite_bex_subset[simp]:
    1.48 -  "finite B \<Longrightarrow> finite{x. EX A<=B. P x A} = (ALL A<=B. finite{x. P x A})"
    1.49 -apply(subgoal_tac "{x. EX A<=B. P x A} = (UN A:Pow B. {x. P x A})")
    1.50 - apply auto
    1.51 -done
    1.52  
    1.53  lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
    1.54  by(blast intro: finite_subset[OF subset_Pow_Union])
     2.1 --- a/src/HOL/NSA/HyperNat.thy	Sun Feb 15 07:54:46 2009 +0100
     2.2 +++ b/src/HOL/NSA/HyperNat.thy	Sun Feb 15 11:26:38 2009 +0100
     2.3 @@ -286,11 +286,10 @@
     2.4  by (simp add: HNatInfinite_def)
     2.5  
     2.6  lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
     2.7 -apply (insert finite_atMost [of m]) 
     2.8 -apply (simp add: atMost_def)
     2.9 +apply (insert finite_atMost [of m])
    2.10  apply (drule FreeUltrafilterNat.finite)
    2.11  apply (drule FreeUltrafilterNat.not_memD)
    2.12 -apply (simp add: Collect_neg_eq [symmetric] linorder_not_le)
    2.13 +apply (simp add: Collect_neg_eq [symmetric] linorder_not_le atMost_def)
    2.14  done
    2.15  
    2.16  lemma Compl_Collect_le: "- {n::nat. N \<le> n} = {n. n < N}"
     3.1 --- a/src/HOL/SetInterval.thy	Sun Feb 15 07:54:46 2009 +0100
     3.2 +++ b/src/HOL/SetInterval.thy	Sun Feb 15 11:26:38 2009 +0100
     3.3 @@ -568,7 +568,6 @@
     3.4  apply auto
     3.5  apply (case_tac xa)
     3.6  apply auto
     3.7 -apply (auto simp add: finite_M_bounded_by_nat)
     3.8  done
     3.9  
    3.10  lemma card_less_Suc:
     4.1 --- a/src/HOL/ex/Sublist.thy	Sun Feb 15 07:54:46 2009 +0100
     4.2 +++ b/src/HOL/ex/Sublist.thy	Sun Feb 15 11:26:38 2009 +0100
     4.3 @@ -64,8 +64,6 @@
     4.4        apply (simp add: sublist_Cons)
     4.5        apply auto
     4.6        apply (auto simp add: nat.split)
     4.7 -      apply (simp add: card_less)
     4.8 -      apply (simp add: card_less)
     4.9        apply (simp add: card_less_Suc[symmetric])
    4.10        apply (simp add: card_less_Suc2)
    4.11        done