equal
deleted
inserted
replaced
329 (*??delete? similar reasoning in hypnat_omega_gt_SHNat above*) |
329 (*??delete? similar reasoning in hypnat_omega_gt_SHNat above*) |
330 lemma HNatInfinite_FreeUltrafilterNat_lemma: |
330 lemma HNatInfinite_FreeUltrafilterNat_lemma: |
331 "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat |
331 "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat |
332 ==> {n. N < f n} \<in> FreeUltrafilterNat" |
332 ==> {n. N < f n} \<in> FreeUltrafilterNat" |
333 apply (induct_tac N) |
333 apply (induct_tac N) |
334 apply (drule_tac x = 0 in spec) |
334 apply (drule_tac x = 0 in spec, simp add: neq0_conv) |
335 apply (rule ccontr, drule FreeUltrafilterNat.not_memD, drule FreeUltrafilterNat.Int, assumption, simp) |
|
336 apply (drule_tac x = "Suc n" in spec) |
335 apply (drule_tac x = "Suc n" in spec) |
337 apply (elim ultra, auto) |
336 apply (elim ultra, auto) |
338 done |
337 done |
339 |
338 |
340 lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}" |
339 lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}" |