Up to index of Isabelle/HOL/HOL-Complex
theory StarDef(* Title : HOL/Hyperreal/StarDef.thy ID : $Id: StarDef.thy,v 1.2 2005/09/16 23:50:01 huffman Exp $ Author : Jacques D. Fleuriot and Brian Huffman *) header {* Construction of Star Types Using Ultrafilters *} theory StarDef imports Filter uses ("transfer.ML") begin subsection {* A Free Ultrafilter over the Naturals *} constdefs FreeUltrafilterNat :: "nat set set" ("\<U>") "\<U> ≡ SOME U. freeultrafilter U" lemma freeultrafilter_FUFNat: "freeultrafilter \<U>" apply (unfold FreeUltrafilterNat_def) apply (rule someI_ex) apply (rule freeultrafilter_Ex) apply (rule nat_infinite) done interpretation FUFNat: freeultrafilter [FreeUltrafilterNat] by (cut_tac [!] freeultrafilter_FUFNat, simp_all add: freeultrafilter_def) text {* This rule takes the place of the old ultra tactic *} lemma ultra: "[|{n. P n} ∈ \<U>; {n. P n --> Q n} ∈ \<U>|] ==> {n. Q n} ∈ \<U>" by (simp add: Collect_imp_eq FUFNat.F.Un_iff FUFNat.F.Compl_iff) subsection {* Definition of @{text star} type constructor *} constdefs starrel :: "((nat => 'a) × (nat => 'a)) set" "starrel ≡ {(X,Y). {n. X n = Y n} ∈ \<U>}" typedef 'a star = "(UNIV :: (nat => 'a) set) // starrel" by (auto intro: quotientI) constdefs star_n :: "(nat => 'a) => 'a star" "star_n X ≡ Abs_star (starrel `` {X})" theorem star_cases [case_names star_n, cases type: star]: "(!!X. x = star_n X ==> P) ==> P" by (cases x, unfold star_n_def star_def, erule quotientE, fast) lemma all_star_eq: "(∀x. P x) = (∀X. P (star_n X))" by (auto, rule_tac x=x in star_cases, simp) lemma ex_star_eq: "(∃x. P x) = (∃X. P (star_n X))" by (auto, rule_tac x=x in star_cases, auto) text {* Proving that @{term starrel} is an equivalence relation *} lemma starrel_iff [iff]: "((X,Y) ∈ starrel) = ({n. X n = Y n} ∈ \<U>)" by (simp add: starrel_def) lemma equiv_starrel: "equiv UNIV starrel" proof (rule equiv.intro) show "reflexive starrel" by (simp add: refl_def) show "sym starrel" by (simp add: sym_def eq_commute) show "trans starrel" by (auto intro: transI elim!: ultra) qed lemmas equiv_starrel_iff = eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I] lemma starrel_in_star: "starrel``{x} ∈ star" by (simp add: star_def quotientI) lemma star_n_eq_iff: "(star_n X = star_n Y) = ({n. X n = Y n} ∈ \<U>)" by (simp add: star_n_def Abs_star_inject starrel_in_star equiv_starrel_iff) subsection {* Transfer principle *} text {* This introduction rule starts each transfer proof. *} lemma transfer_start: "P ≡ {n. Q} ∈ \<U> ==> Trueprop P ≡ Trueprop Q" by (subgoal_tac "P ≡ Q", simp, simp add: atomize_eq) text {*Initialize transfer tactic.*} use "transfer.ML" setup Transfer.setup text {* Transfer introduction rules. *} lemma transfer_ex [transfer_intro]: "[|!!X. p (star_n X) ≡ {n. P n (X n)} ∈ \<U>|] ==> ∃x::'a star. p x ≡ {n. ∃x. P n x} ∈ \<U>" by (simp only: ex_star_eq FUFNat.F.Collect_ex) lemma transfer_all [transfer_intro]: "[|!!X. p (star_n X) ≡ {n. P n (X n)} ∈ \<U>|] ==> ∀x::'a star. p x ≡ {n. ∀x. P n x} ∈ \<U>" by (simp only: all_star_eq FUFNat.F.Collect_all) lemma transfer_not [transfer_intro]: "[|p ≡ {n. P n} ∈ \<U>|] ==> ¬ p ≡ {n. ¬ P n} ∈ \<U>" by (simp only: FUFNat.F.Collect_not) lemma transfer_conj [transfer_intro]: "[|p ≡ {n. P n} ∈ \<U>; q ≡ {n. Q n} ∈ \<U>|] ==> p ∧ q ≡ {n. P n ∧ Q n} ∈ \<U>" by (simp only: FUFNat.F.Collect_conj) lemma transfer_disj [transfer_intro]: "[|p ≡ {n. P n} ∈ \<U>; q ≡ {n. Q n} ∈ \<U>|] ==> p ∨ q ≡ {n. P n ∨ Q n} ∈ \<U>" by (simp only: FUFNat.F.Collect_disj) lemma transfer_imp [transfer_intro]: "[|p ≡ {n. P n} ∈ \<U>; q ≡ {n. Q n} ∈ \<U>|] ==> p --> q ≡ {n. P n --> Q n} ∈ \<U>" by (simp only: imp_conv_disj transfer_disj transfer_not) lemma transfer_iff [transfer_intro]: "[|p ≡ {n. P n} ∈ \<U>; q ≡ {n. Q n} ∈ \<U>|] ==> p = q ≡ {n. P n = Q n} ∈ \<U>" by (simp only: iff_conv_conj_imp transfer_conj transfer_imp) lemma transfer_if_bool [transfer_intro]: "[|p ≡ {n. P n} ∈ \<U>; x ≡ {n. X n} ∈ \<U>; y ≡ {n. Y n} ∈ \<U>|] ==> (if p then x else y) ≡ {n. if P n then X n else Y n} ∈ \<U>" by (simp only: if_bool_eq_conj transfer_conj transfer_imp transfer_not) lemma transfer_eq [transfer_intro]: "[|x ≡ star_n X; y ≡ star_n Y|] ==> x = y ≡ {n. X n = Y n} ∈ \<U>" by (simp only: star_n_eq_iff) lemma transfer_if [transfer_intro]: "[|p ≡ {n. P n} ∈ \<U>; x ≡ star_n X; y ≡ star_n Y|] ==> (if p then x else y) ≡ star_n (λn. if P n then X n else Y n)" apply (rule eq_reflection) apply (auto simp add: star_n_eq_iff transfer_not elim!: ultra) done lemma transfer_fun_eq [transfer_intro]: "[|!!X. f (star_n X) = g (star_n X) ≡ {n. F n (X n) = G n (X n)} ∈ \<U>|] ==> f = g ≡ {n. F n = G n} ∈ \<U>" by (simp only: expand_fun_eq transfer_all) lemma transfer_star_n [transfer_intro]: "star_n X ≡ star_n (λn. X n)" by (rule reflexive) lemma transfer_bool [transfer_intro]: "p ≡ {n. p} ∈ \<U>" by (simp add: atomize_eq) subsection {* Standard elements *} constdefs star_of :: "'a => 'a star" "star_of x ≡ star_n (λn. x)" text {* Transfer tactic should remove occurrences of @{term star_of} *} setup {* [Transfer.add_const "StarDef.star_of"] *} declare star_of_def [transfer_intro] lemma star_of_inject: "(star_of x = star_of y) = (x = y)" by (transfer, rule refl) subsection {* Internal functions *} constdefs Ifun :: "('a => 'b) star => 'a star => 'b star" ("_ ∗ _" [300,301] 300) "Ifun f ≡ λx. Abs_star (\<Union>F∈Rep_star f. \<Union>X∈Rep_star x. starrel``{λn. F n (X n)})" lemma Ifun_congruent2: "(λF X. starrel``{λn. F n (X n)}) respects2 starrel" by (auto simp add: congruent2_def equiv_starrel_iff elim!: ultra) lemma Ifun_star_n: "star_n F ∗ star_n X = star_n (λn. F n (X n))" by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2]) text {* Transfer tactic should remove occurrences of @{term Ifun} *} setup {* [Transfer.add_const "StarDef.Ifun"] *} lemma transfer_Ifun [transfer_intro]: "[|f ≡ star_n F; x ≡ star_n X|] ==> f ∗ x ≡ star_n (λn. F n (X n))" by (simp only: Ifun_star_n) lemma Ifun_star_of [simp]: "star_of f ∗ star_of x = star_of (f x)" by (transfer, rule refl) text {* Nonstandard extensions of functions *} constdefs starfun :: "('a => 'b) => ('a star => 'b star)" ("*f* _" [80] 80) "starfun f ≡ λx. star_of f ∗ x" starfun2 :: "('a => 'b => 'c) => ('a star => 'b star => 'c star)" ("*f2* _" [80] 80) "starfun2 f ≡ λx y. star_of f ∗ x ∗ y" declare starfun_def [transfer_unfold] declare starfun2_def [transfer_unfold] lemma starfun_star_n: "( *f* f) (star_n X) = star_n (λn. f (X n))" by (simp only: starfun_def star_of_def Ifun_star_n) lemma starfun2_star_n: "( *f2* f) (star_n X) (star_n Y) = star_n (λn. f (X n) (Y n))" by (simp only: starfun2_def star_of_def Ifun_star_n) lemma starfun_star_of [simp]: "( *f* f) (star_of x) = star_of (f x)" by (transfer, rule refl) lemma starfun2_star_of [simp]: "( *f2* f) (star_of x) = *f* f x" by (transfer, rule refl) subsection {* Internal predicates *} constdefs unstar :: "bool star => bool" "unstar b ≡ b = star_of True" lemma unstar_star_n: "unstar (star_n P) = ({n. P n} ∈ \<U>)" by (simp add: unstar_def star_of_def star_n_eq_iff) lemma unstar_star_of [simp]: "unstar (star_of p) = p" by (simp add: unstar_def star_of_inject) text {* Transfer tactic should remove occurrences of @{term unstar} *} setup {* [Transfer.add_const "StarDef.unstar"] *} lemma transfer_unstar [transfer_intro]: "p ≡ star_n P ==> unstar p ≡ {n. P n} ∈ \<U>" by (simp only: unstar_star_n) constdefs starP :: "('a => bool) => 'a star => bool" ("*p* _" [80] 80) "*p* P ≡ λx. unstar (star_of P ∗ x)" starP2 :: "('a => 'b => bool) => 'a star => 'b star => bool" ("*p2* _" [80] 80) "*p2* P ≡ λx y. unstar (star_of P ∗ x ∗ y)" declare starP_def [transfer_unfold] declare starP2_def [transfer_unfold] lemma starP_star_n: "( *p* P) (star_n X) = ({n. P (X n)} ∈ \<U>)" by (simp only: starP_def star_of_def Ifun_star_n unstar_star_n) lemma starP2_star_n: "( *p2* P) (star_n X) (star_n Y) = ({n. P (X n) (Y n)} ∈ \<U>)" by (simp only: starP2_def star_of_def Ifun_star_n unstar_star_n) lemma starP_star_of [simp]: "( *p* P) (star_of x) = P x" by (transfer, rule refl) lemma starP2_star_of [simp]: "( *p2* P) (star_of x) = *p* P x" by (transfer, rule refl) subsection {* Internal sets *} constdefs Iset :: "'a set star => 'a star set" "Iset A ≡ {x. ( *p2* op ∈) x A}" lemma Iset_star_n: "(star_n X ∈ Iset (star_n A)) = ({n. X n ∈ A n} ∈ \<U>)" by (simp add: Iset_def starP2_star_n) text {* Transfer tactic should remove occurrences of @{term Iset} *} setup {* [Transfer.add_const "StarDef.Iset"] *} lemma transfer_mem [transfer_intro]: "[|x ≡ star_n X; a ≡ Iset (star_n A)|] ==> x ∈ a ≡ {n. X n ∈ A n} ∈ \<U>" by (simp only: Iset_star_n) lemma transfer_Collect [transfer_intro]: "[|!!X. p (star_n X) ≡ {n. P n (X n)} ∈ \<U>|] ==> Collect p ≡ Iset (star_n (λn. Collect (P n)))" by (simp add: atomize_eq expand_set_eq all_star_eq Iset_star_n) lemma transfer_set_eq [transfer_intro]: "[|a ≡ Iset (star_n A); b ≡ Iset (star_n B)|] ==> a = b ≡ {n. A n = B n} ∈ \<U>" by (simp only: expand_set_eq transfer_all transfer_iff transfer_mem) lemma transfer_ball [transfer_intro]: "[|a ≡ Iset (star_n A); !!X. p (star_n X) ≡ {n. P n (X n)} ∈ \<U>|] ==> ∀x∈a. p x ≡ {n. ∀x∈A n. P n x} ∈ \<U>" by (simp only: Ball_def transfer_all transfer_imp transfer_mem) lemma transfer_bex [transfer_intro]: "[|a ≡ Iset (star_n A); !!X. p (star_n X) ≡ {n. P n (X n)} ∈ \<U>|] ==> ∃x∈a. p x ≡ {n. ∃x∈A n. P n x} ∈ \<U>" by (simp only: Bex_def transfer_ex transfer_conj transfer_mem) lemma transfer_Iset [transfer_intro]: "[|a ≡ star_n A|] ==> Iset a ≡ Iset (star_n (λn. A n))" by simp text {* Nonstandard extensions of sets. *} constdefs starset :: "'a set => 'a star set" ("*s* _" [80] 80) "starset A ≡ Iset (star_of A)" declare starset_def [transfer_unfold] lemma starset_mem: "(star_of x ∈ *s* A) = (x ∈ A)" by (transfer, rule refl) lemma starset_UNIV: "*s* (UNIV::'a set) = (UNIV::'a star set)" by (transfer UNIV_def, rule refl) lemma starset_empty: "*s* {} = {}" by (transfer empty_def, rule refl) lemma starset_insert: "*s* (insert x A) = insert (star_of x) ( *s* A)" by (transfer insert_def Un_def, rule refl) lemma starset_Un: "*s* (A ∪ B) = *s* A ∪ *s* B" by (transfer Un_def, rule refl) lemma starset_Int: "*s* (A ∩ B) = *s* A ∩ *s* B" by (transfer Int_def, rule refl) lemma starset_Compl: "*s* -A = -( *s* A)" by (transfer Compl_def, rule refl) lemma starset_diff: "*s* (A - B) = *s* A - *s* B" by (transfer set_diff_def, rule refl) lemma starset_image: "*s* (f ` A) = ( *f* f) ` ( *s* A)" by (transfer image_def, rule refl) lemma starset_vimage: "*s* (f -` A) = ( *f* f) -` ( *s* A)" by (transfer vimage_def, rule refl) lemma starset_subset: "( *s* A ⊆ *s* B) = (A ⊆ B)" by (transfer subset_def, rule refl) lemma starset_eq: "( *s* A = *s* B) = (A = B)" by (transfer, rule refl) lemmas starset_simps [simp] = starset_mem starset_UNIV starset_empty starset_insert starset_Un starset_Int starset_Compl starset_diff starset_image starset_vimage starset_subset starset_eq end
lemma freeultrafilter_FUFNat:
freeultrafilter \<U>
lemma ultra:
[| {n. P n} ∈ \<U>; {n. P n --> Q n} ∈ \<U> |] ==> {n. Q n} ∈ \<U>
theorem star_cases:
(!!X. x = star_n X ==> P) ==> P
lemma all_star_eq:
(∀x. P x) = (∀X. P (star_n X))
lemma ex_star_eq:
(∃x. P x) = (∃X. P (star_n X))
lemma starrel_iff:
((X, Y) ∈ starrel) = ({n. X n = Y n} ∈ \<U>)
lemma equiv_starrel:
equiv UNIV starrel
lemmas equiv_starrel_iff:
(starrel `` {x} = starrel `` {y}) = ((x, y) ∈ starrel)
lemmas equiv_starrel_iff:
(starrel `` {x} = starrel `` {y}) = ((x, y) ∈ starrel)
lemma starrel_in_star:
starrel `` {x} ∈ star
lemma star_n_eq_iff:
(star_n X = star_n Y) = ({n. X n = Y n} ∈ \<U>)
lemma transfer_start:
P == {n. Q} ∈ \<U> ==> P == Q
lemma transfer_ex:
(!!X. p (star_n X) == {n. P n (X n)} ∈ \<U>) ==> ∃x. p x == {n. ∃x. P n x} ∈ \<U>
lemma transfer_all:
(!!X. p (star_n X) == {n. P n (X n)} ∈ \<U>) ==> ∀x. p x == {n. ∀x. P n x} ∈ \<U>
lemma transfer_not:
p == {n. P n} ∈ \<U> ==> ¬ p == {n. ¬ P n} ∈ \<U>
lemma transfer_conj:
[| p == {n. P n} ∈ \<U>; q == {n. Q n} ∈ \<U> |] ==> p ∧ q == {n. P n ∧ Q n} ∈ \<U>
lemma transfer_disj:
[| p == {n. P n} ∈ \<U>; q == {n. Q n} ∈ \<U> |] ==> p ∨ q == {n. P n ∨ Q n} ∈ \<U>
lemma transfer_imp:
[| p == {n. P n} ∈ \<U>; q == {n. Q n} ∈ \<U> |] ==> p --> q == {n. P n --> Q n} ∈ \<U>
lemma transfer_iff:
[| p == {n. P n} ∈ \<U>; q == {n. Q n} ∈ \<U> |] ==> p = q == {n. P n = Q n} ∈ \<U>
lemma transfer_if_bool:
[| p == {n. P n} ∈ \<U>; x == {n. X n} ∈ \<U>; y == {n. Y n} ∈ \<U> |] ==> if p then x else y == {n. if P n then X n else Y n} ∈ \<U>
lemma transfer_eq:
[| x == star_n X; y == star_n Y |] ==> x = y == {n. X n = Y n} ∈ \<U>
lemma transfer_if:
[| p == {n. P n} ∈ \<U>; x == star_n X; y == star_n Y |] ==> if p then x else y == star_n (%n. if P n then X n else Y n)
lemma transfer_fun_eq:
(!!X. f (star_n X) = g (star_n X) == {n. F n (X n) = G n (X n)} ∈ \<U>) ==> f = g == {n. F n = G n} ∈ \<U>
lemma transfer_star_n:
star_n X == star_n X
lemma transfer_bool:
p == {n. p} ∈ \<U>
lemma star_of_inject:
(star_of x = star_of y) = (x = y)
lemma Ifun_congruent2:
congruent2 starrel starrel (%F X. starrel `` {%n. F n (X n)})
lemma Ifun_star_n:
star_n F ∗ star_n X = star_n (%n. F n (X n))
lemma transfer_Ifun:
[| f == star_n F; x == star_n X |] ==> f ∗ x == star_n (%n. F n (X n))
lemma Ifun_star_of:
star_of f ∗ star_of x = star_of (f x)
lemma starfun_star_n:
(*f* f) (star_n X) = star_n (%n. f (X n))
lemma starfun2_star_n:
(*f2* f) (star_n X) (star_n Y) = star_n (%n. f (X n) (Y n))
lemma starfun_star_of:
(*f* f) (star_of x) = star_of (f x)
lemma starfun2_star_of:
(*f2* f) (star_of x) = *f* f x
lemma unstar_star_n:
unstar (star_n P) = ({n. P n} ∈ \<U>)
lemma unstar_star_of:
unstar (star_of p) = p
lemma transfer_unstar:
p == star_n P ==> unstar p == {n. P n} ∈ \<U>
lemma starP_star_n:
(*p* P) (star_n X) = ({n. P (X n)} ∈ \<U>)
lemma starP2_star_n:
(*p2* P) (star_n X) (star_n Y) = ({n. P (X n) (Y n)} ∈ \<U>)
lemma starP_star_of:
(*p* P) (star_of x) = P x
lemma starP2_star_of:
(*p2* P) (star_of x) = *p* P x
lemma Iset_star_n:
(star_n X ∈ Iset (star_n A)) = ({n. X n ∈ A n} ∈ \<U>)
lemma transfer_mem:
[| x == star_n X; a == Iset (star_n A) |] ==> x ∈ a == {n. X n ∈ A n} ∈ \<U>
lemma transfer_Collect:
(!!X. p (star_n X) == {n. P n (X n)} ∈ \<U>) ==> Collect p == Iset (star_n (%n. Collect (P n)))
lemma transfer_set_eq:
[| a == Iset (star_n A); b == Iset (star_n B) |] ==> a = b == {n. A n = B n} ∈ \<U>
lemma transfer_ball:
[| a == Iset (star_n A); !!X. p (star_n X) == {n. P n (X n)} ∈ \<U> |] ==> ∀x∈a. p x == {n. ∀x∈A n. P n x} ∈ \<U>
lemma transfer_bex:
[| a == Iset (star_n A); !!X. p (star_n X) == {n. P n (X n)} ∈ \<U> |] ==> ∃x∈a. p x == {n. ∃x∈A n. P n x} ∈ \<U>
lemma transfer_Iset:
a == star_n A ==> Iset a == Iset (star_n A)
lemma starset_mem:
(star_of x ∈ *s* A) = (x ∈ A)
lemma starset_UNIV:
*s* UNIV = UNIV
lemma starset_empty:
*s* {} = {}
lemma starset_insert:
*s* insert x A = insert (star_of x) (*s* A)
lemma starset_Un:
*s* (A ∪ B) = *s* A ∪ *s* B
lemma starset_Int:
*s* (A ∩ B) = *s* A ∩ *s* B
lemma starset_Compl:
*s* - A = - (*s* A)
lemma starset_diff:
*s* (A - B) = *s* A - *s* B
lemma starset_image:
*s* f ` A = (*f* f) ` (*s* A)
lemma starset_vimage:
*s* f -` A = (*f* f) -` (*s* A)
lemma starset_subset:
(*s* A ⊆ *s* B) = (A ⊆ B)
lemma starset_eq:
(*s* A = *s* B) = (A = B)
lemmas starset_simps:
(star_of x ∈ *s* A) = (x ∈ A)
*s* UNIV = UNIV
*s* {} = {}
*s* insert x A = insert (star_of x) (*s* A)
*s* (A ∪ B) = *s* A ∪ *s* B
*s* (A ∩ B) = *s* A ∩ *s* B
*s* - A = - (*s* A)
*s* (A - B) = *s* A - *s* B
*s* f ` A = (*f* f) ` (*s* A)
*s* f -` A = (*f* f) -` (*s* A)
(*s* A ⊆ *s* B) = (A ⊆ B)
(*s* A = *s* B) = (A = B)
lemmas starset_simps:
(star_of x ∈ *s* A) = (x ∈ A)
*s* UNIV = UNIV
*s* {} = {}
*s* insert x A = insert (star_of x) (*s* A)
*s* (A ∪ B) = *s* A ∪ *s* B
*s* (A ∩ B) = *s* A ∩ *s* B
*s* - A = - (*s* A)
*s* (A - B) = *s* A - *s* B
*s* f ` A = (*f* f) ` (*s* A)
*s* f -` A = (*f* f) -` (*s* A)
(*s* A ⊆ *s* B) = (A ⊆ B)
(*s* A = *s* B) = (A = B)