equal
deleted
inserted
replaced
202 apply (simp add: is_starext_def) |
202 apply (simp add: is_starext_def) |
203 apply (rule ext) |
203 apply (rule ext) |
204 apply (rule_tac x = x in star_cases) |
204 apply (rule_tac x = x in star_cases) |
205 apply (drule_tac x = x in spec) |
205 apply (drule_tac x = x in spec) |
206 apply (drule_tac x = "( *f* f) x" in spec) |
206 apply (drule_tac x = "( *f* f) x" in spec) |
207 apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: starfun, ultra) |
207 apply (auto simp add: starfun_star_n) |
|
208 apply (simp add: star_n_eq_iff [symmetric]) |
|
209 apply (simp add: starfun_star_n [of f, symmetric]) |
208 done |
210 done |
209 |
211 |
210 lemma is_starext_starfun_iff: "(is_starext F f) = (F = *f* f)" |
212 lemma is_starext_starfun_iff: "(is_starext F f) = (F = *f* f)" |
211 by (blast intro: is_starfun_starext is_starext_starfun) |
213 by (blast intro: is_starfun_starext is_starext_starfun) |
212 |
214 |