16 FreeUltrafilterNat :: "nat set set" ("\<U>") where |
16 FreeUltrafilterNat :: "nat set set" ("\<U>") where |
17 "\<U> = (SOME U. freeultrafilter U)" |
17 "\<U> = (SOME U. freeultrafilter U)" |
18 |
18 |
19 lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>" |
19 lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>" |
20 apply (unfold FreeUltrafilterNat_def) |
20 apply (unfold FreeUltrafilterNat_def) |
21 apply (rule someI_ex) |
21 apply (rule someI_ex [where P=freeultrafilter]) |
22 apply (rule freeultrafilter_Ex) |
22 apply (rule freeultrafilter_Ex) |
23 apply (rule nat_infinite) |
23 apply (rule nat_infinite) |
24 done |
24 done |
25 |
25 |
26 interpretation FreeUltrafilterNat: freeultrafilter [FreeUltrafilterNat] |
26 interpretation FreeUltrafilterNat: freeultrafilter [FreeUltrafilterNat] |
399 |
399 |
400 lemma starset_Int: "*s* (A \<inter> B) = *s* A \<inter> *s* B" |
400 lemma starset_Int: "*s* (A \<inter> B) = *s* A \<inter> *s* B" |
401 by (transfer Int_def, rule refl) |
401 by (transfer Int_def, rule refl) |
402 |
402 |
403 lemma starset_Compl: "*s* -A = -( *s* A)" |
403 lemma starset_Compl: "*s* -A = -( *s* A)" |
404 by (transfer Compl_def, rule refl) |
404 by (transfer Compl_eq, rule refl) |
405 |
405 |
406 lemma starset_diff: "*s* (A - B) = *s* A - *s* B" |
406 lemma starset_diff: "*s* (A - B) = *s* A - *s* B" |
407 by (transfer set_diff_def, rule refl) |
407 by (transfer set_diff_eq, rule refl) |
408 |
408 |
409 lemma starset_image: "*s* (f ` A) = ( *f* f) ` ( *s* A)" |
409 lemma starset_image: "*s* (f ` A) = ( *f* f) ` ( *s* A)" |
410 by (transfer image_def, rule refl) |
410 by (transfer image_def, rule refl) |
411 |
411 |
412 lemma starset_vimage: "*s* (f -` A) = ( *f* f) -` ( *s* A)" |
412 lemma starset_vimage: "*s* (f -` A) = ( *f* f) -` ( *s* A)" |
413 by (transfer vimage_def, rule refl) |
413 by (transfer vimage_def, rule refl) |
414 |
414 |
415 lemma starset_subset: "( *s* A \<subseteq> *s* B) = (A \<subseteq> B)" |
415 lemma starset_subset: "( *s* A \<subseteq> *s* B) = (A \<subseteq> B)" |
416 by (transfer subset_def, rule refl) |
416 by (transfer subset_eq, rule refl) |
417 |
417 |
418 lemma starset_eq: "( *s* A = *s* B) = (A = B)" |
418 lemma starset_eq: "( *s* A = *s* B) = (A = B)" |
419 by (transfer, rule refl) |
419 by (transfer, rule refl) |
420 |
420 |
421 lemmas starset_simps [simp] = |
421 lemmas starset_simps [simp] = |