src/HOL/Hyperreal/HyperDef.thy
changeset 14378 69c4d5997669
parent 14371 c78c7da09519
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -176,6 +176,11 @@
     1.4       "(X: FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)"
     1.5  by (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric])
     1.6  
     1.7 +lemma cofinite_mem_FreeUltrafilterNat: "finite (-X) ==> X \<in> FreeUltrafilterNat"
     1.8 +apply (drule FreeUltrafilterNat_finite)  
     1.9 +apply (simp add: FreeUltrafilterNat_Compl_iff2 [symmetric])
    1.10 +done
    1.11 +
    1.12  lemma FreeUltrafilterNat_UNIV [simp]: "(UNIV::nat set) \<in> FreeUltrafilterNat"
    1.13  by (rule FreeUltrafilterNat_mem [THEN FreeUltrafilter_Ultrafilter, THEN Ultrafilter_Filter, THEN mem_FiltersetD4])
    1.14  
    1.15 @@ -768,7 +773,7 @@
    1.16  
    1.17  lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} |  
    1.18        (\<exists>y. {n::nat. x = real n} = {y})"
    1.19 -by (force dest: inj_real_of_nat [THEN injD])
    1.20 +by (force)
    1.21  
    1.22  lemma lemma_finite_omega_set: "finite {n::nat. x = real n}"
    1.23  by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto)
    1.24 @@ -789,7 +794,7 @@
    1.25  lemma lemma_epsilon_empty_singleton_disj:
    1.26       "{n::nat. x = inverse(real(Suc n))} = {} |  
    1.27        (\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})"
    1.28 -by (auto simp add: inj_real_of_nat [THEN inj_eq])
    1.29 +by (auto)
    1.30  
    1.31  lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}"
    1.32  by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto)