equal
deleted
inserted
replaced
599 |
599 |
600 (*??delete? similar reasoning in hypnat_omega_gt_SHNat above*) |
600 (*??delete? similar reasoning in hypnat_omega_gt_SHNat above*) |
601 lemma HNatInfinite_FreeUltrafilterNat_lemma: |
601 lemma HNatInfinite_FreeUltrafilterNat_lemma: |
602 "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat |
602 "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat |
603 ==> {n. N < f n} \<in> FreeUltrafilterNat" |
603 ==> {n. N < f n} \<in> FreeUltrafilterNat" |
604 apply (induct_tac "N") |
604 apply (induct_tac N) |
605 apply (drule_tac x = 0 in spec) |
605 apply (drule_tac x = 0 in spec) |
606 apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem, drule FreeUltrafilterNat_Int, assumption, simp) |
606 apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem, drule FreeUltrafilterNat_Int, assumption, simp) |
607 apply (drule_tac x = "Suc n" in spec, ultra) |
607 apply (drule_tac x = "Suc n" in spec, ultra) |
608 done |
608 done |
609 |
609 |