# HG changeset patch # User paulson # Date 912162267 -3600 # Node ID 11cbf236ca162df3242c49453a8599e114d2436b # Parent fa2c2dd74f8cd0e974fdbc57e49a24eee7df61e5 Addition of Hyperreal theories Zorn and Filter diff -r fa2c2dd74f8c -r 11cbf236ca16 src/HOL/Real/Hyperreal/Filter.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/Hyperreal/Filter.ML Fri Nov 27 11:24:27 1998 +0100 @@ -0,0 +1,557 @@ +(* Title : Filter.ML + Author : Jacques D. Fleuriot + Copyright : 1998 University of Cambridge + Description : Filters and Ultrafilter +*) + +open Filter; + + +(*------------------------------------------------------------------ + Properties of Filters and Freefilters - + rules for intro, destruction etc. + ------------------------------------------------------------------*) + +Goalw [is_Filter_def] "is_Filter X S ==> X <= Pow(S)"; +by (Blast_tac 1); +qed "is_FilterD1"; + +Goalw [is_Filter_def] "is_Filter X S ==> X ~= {}"; +by (Blast_tac 1); +qed "is_FilterD2"; + +Goalw [is_Filter_def] "is_Filter X S ==> {} ~: X"; +by (Blast_tac 1); +qed "is_FilterD3"; + +Goalw [Filter_def] "is_Filter X S ==> X : Filter S"; +by (Blast_tac 1); +qed "mem_FiltersetI"; + +Goalw [Filter_def] "X : Filter S ==> is_Filter X S"; +by (Blast_tac 1); +qed "mem_FiltersetD"; + +Goal "X : Filter S ==> {} ~: X"; +by (etac (mem_FiltersetD RS is_FilterD3) 1); +qed "Filter_empty_not_mem"; + +bind_thm ("Filter_empty_not_memE",(Filter_empty_not_mem RS notE)); + +Goalw [Filter_def,is_Filter_def] + "[| X: Filter S; A: X; B: X |] ==> A Int B : X"; +by (Blast_tac 1); +qed "mem_FiltersetD1"; + +Goalw [Filter_def,is_Filter_def] + "[| X: Filter S; A: X; A <= B; B <= S|] ==> B : X"; +by (Blast_tac 1); +qed "mem_FiltersetD2"; + +Goalw [Filter_def,is_Filter_def] + "[| X: Filter S; A: X |] ==> A : Pow S"; +by (Blast_tac 1); +qed "mem_FiltersetD3"; + +Goalw [Filter_def,is_Filter_def] + "X: Filter S ==> S : X"; +by (Blast_tac 1); +qed "mem_FiltersetD4"; + +Goalw [is_Filter_def] + "[| X <= Pow(S);\ +\ S : X; \ +\ X ~= {}; \ +\ {} ~: X; \ +\ ALL u: X. ALL v: X. u Int v : X; \ +\ ALL u v. u: X & u<=v & v<=S --> v: X \ +\ |] ==> is_Filter X S"; +by (Blast_tac 1); +qed "is_FilterI"; + +Goal "[| X <= Pow(S);\ +\ S : X; \ +\ X ~= {}; \ +\ {} ~: X; \ +\ ALL u: X. ALL v: X. u Int v : X; \ +\ ALL u v. u: X & u<=v & v<=S --> v: X \ +\ |] ==> X: Filter S"; +by (blast_tac (claset() addIs [mem_FiltersetI,is_FilterI]) 1); +qed "mem_FiltersetI2"; + +Goalw [is_Filter_def] + "is_Filter X S ==> X <= Pow(S) & \ +\ S : X & \ +\ X ~= {} & \ +\ {} ~: X & \ +\ (ALL u: X. ALL v: X. u Int v : X) & \ +\ (ALL u v. u: X & u <= v & v<=S --> v: X)"; +by (Fast_tac 1); +qed "is_FilterE_lemma"; + +Goalw [is_Filter_def] + "X : Filter S ==> X <= Pow(S) &\ +\ S : X & \ +\ X ~= {} & \ +\ {} ~: X & \ +\ (ALL u: X. ALL v: X. u Int v : X) & \ +\ (ALL u v. u: X & u <= v & v<=S --> v: X)"; +by (etac (mem_FiltersetD RS is_FilterE_lemma) 1); +qed "memFiltersetE_lemma"; + +Goalw [Filter_def,Freefilter_def] + "X: Freefilter S ==> X: Filter S"; +by (Fast_tac 1); +qed "Freefilter_Filter"; + +Goalw [Freefilter_def] + "X: Freefilter S ==> ALL y: X. ~finite(y)"; +by (Blast_tac 1); +qed "mem_Freefilter_not_finite"; + +Goal "[| X: Freefilter S; x: X |] ==> ~ finite x"; +by (blast_tac (claset() addSDs [mem_Freefilter_not_finite]) 1); +qed "mem_FreefiltersetD1"; + +bind_thm ("mem_FreefiltersetE1", (mem_FreefiltersetD1 RS notE)); + +Goal "[| X: Freefilter S; finite x|] ==> x ~: X"; +by (blast_tac (claset() addSDs [mem_Freefilter_not_finite]) 1); +qed "mem_FreefiltersetD2"; + +Goalw [Freefilter_def] + "[| X: Filter S; ALL x. ~(x: X & finite x) |] ==> X: Freefilter S"; +by (Blast_tac 1); +qed "mem_FreefiltersetI1"; + +Goalw [Freefilter_def] + "[| X: Filter S; ALL x. (x ~: X | ~ finite x) |] ==> X: Freefilter S"; +by (Blast_tac 1); +qed "mem_FreefiltersetI2"; + +Goal "[| X: Filter S; A: X; B: X |] ==> A Int B ~= {}"; +by (forw_inst_tac [("A","A"),("B","B")] mem_FiltersetD1 1); +by (auto_tac (claset() addSDs [Filter_empty_not_mem],simpset())); +qed "Filter_Int_not_empty"; + +bind_thm ("Filter_Int_not_emptyE",(Filter_Int_not_empty RS notE)); + +(*---------------------------------------------------------------------------------- + Ultrafilters and Free ultrafilters + ----------------------------------------------------------------------------------*) + +Goalw [Ultrafilter_def] "X : Ultrafilter S ==> X: Filter S"; +by (Blast_tac 1); +qed "Ultrafilter_Filter"; + +Goalw [Ultrafilter_def] + "X : Ultrafilter S ==> !A: Pow(S). A : X | S - A: X"; +by (Blast_tac 1); +qed "mem_UltrafiltersetD2"; + +Goalw [Ultrafilter_def] + "[|X : Ultrafilter S; A <= S; A ~: X |] ==> S - A: X"; +by (Blast_tac 1); +qed "mem_UltrafiltersetD3"; + +Goalw [Ultrafilter_def] + "[|X : Ultrafilter S; A <= S; S - A ~: X |] ==> A: X"; +by (Blast_tac 1); +qed "mem_UltrafiltersetD4"; + +Goalw [Ultrafilter_def] + "[| X: Filter S; \ +\ ALL A: Pow(S). A: X | S - A : X |] ==> X: Ultrafilter S"; +by (Blast_tac 1); +qed "mem_UltrafiltersetI"; + +Goalw [Ultrafilter_def,FreeUltrafilter_def] + "X: FreeUltrafilter S ==> X: Ultrafilter S"; +by (Blast_tac 1); +qed "FreeUltrafilter_Ultrafilter"; + +Goalw [FreeUltrafilter_def] + "X: FreeUltrafilter S ==> ALL y: X. ~finite(y)"; +by (Blast_tac 1); +qed "mem_FreeUltrafilter_not_finite"; + +Goal "[| X: FreeUltrafilter S; x: X |] ==> ~ finite x"; +by (blast_tac (claset() addSDs [mem_FreeUltrafilter_not_finite]) 1); +qed "mem_FreeUltrafiltersetD1"; + +bind_thm ("mem_FreeUltrafiltersetE1", (mem_FreeUltrafiltersetD1 RS notE)); + +Goal "[| X: FreeUltrafilter S; finite x|] ==> x ~: X"; +by (blast_tac (claset() addSDs [mem_FreeUltrafilter_not_finite]) 1); +qed "mem_FreeUltrafiltersetD2"; + +Goalw [FreeUltrafilter_def] + "[| X: Ultrafilter S; \ +\ ALL x. ~(x: X & finite x) |] ==> X: FreeUltrafilter S"; +by (Blast_tac 1); +qed "mem_FreeUltrafiltersetI1"; + +Goalw [FreeUltrafilter_def] + "[| X: Ultrafilter S; \ +\ ALL x. (x ~: X | ~ finite x) |] ==> X: FreeUltrafilter S"; +by (Blast_tac 1); +qed "mem_FreeUltrafiltersetI2"; + +Goalw [FreeUltrafilter_def,Freefilter_def,Ultrafilter_def] + "(X: FreeUltrafilter S) = (X: Freefilter S & (ALL x:Pow(S). x: X | S - x: X))"; +by (Blast_tac 1); +qed "FreeUltrafilter_iff"; + +(*------------------------------------------------------------------- + A Filter F on S is an ultrafilter iff it is a maximal filter + i.e. whenever G is a filter on I and F <= F then F = G + --------------------------------------------------------------------*) +(*--------------------------------------------------------------------- + lemmas that shows existence of an extension to what was assumed to + be a maximal filter. Will be used to derive contradiction in proof of + property of ultrafilter + ---------------------------------------------------------------------*) +Goal "[| F ~= {}; A <= S |] ==> \ +\ EX x. x: {X. X <= S & (EX f:F. A Int f <= X)}"; +by (Blast_tac 1); +qed "lemma_set_extend"; + +Goal "a: X ==> X ~= {}"; +by (Step_tac 1); +qed "lemma_set_not_empty"; + +Goal "x Int F <= {} ==> F <= - x"; +by (Blast_tac 1); +qed "lemma_empty_Int_subset_Compl"; + +Goalw [Filter_def,is_Filter_def] + "[| F: Filter S; A ~: F; A <= S|] \ +\ ==> ALL B. B ~: F | ~ B <= A"; +by (Blast_tac 1); +qed "mem_Filterset_disjI"; + +Goal "F : Ultrafilter S ==> \ +\ (F: Filter S & (ALL G: Filter S. F <= G --> F = G))"; +by (auto_tac (claset(),simpset() addsimps [Ultrafilter_def])); +by (dres_inst_tac [("x","x")] bspec 1); +by (etac mem_FiltersetD3 1 THEN assume_tac 1); +by (Step_tac 1); +by (dtac subsetD 1 THEN assume_tac 1); +by (blast_tac (claset() addSDs [Filter_Int_not_empty]) 1); +qed "Ultrafilter_max_Filter"; + + +(*-------------------------------------------------------------------------------- + This is a very long and tedious proof; need to break it into parts. + Have proof that {X. X <= S & (EX f: F. A Int f <= X)} is a filter as + a lemma +--------------------------------------------------------------------------------*) +Goalw [Ultrafilter_def] + "[| F: Filter S; \ +\ ALL G: Filter S. F <= G --> F = G |] ==> F : Ultrafilter S"; +by (Step_tac 1); +by (rtac ccontr 1); +by (forward_tac [mem_FiltersetD RS is_FilterD2] 1); +by (forw_inst_tac [("x","{X. X <= S & (EX f: F. A Int f <= X)}")] bspec 1); +by (EVERY1[rtac mem_FiltersetI2, Blast_tac, Asm_full_simp_tac]); +by (blast_tac (claset() addDs [mem_FiltersetD3]) 1); +by (etac (lemma_set_extend RS exE) 1); +by (assume_tac 1 THEN etac lemma_set_not_empty 1); +by (REPEAT(rtac ballI 2) THEN Asm_full_simp_tac 2); +by (rtac conjI 2 THEN Blast_tac 2); +by (REPEAT(etac conjE 2) THEN REPEAT(etac bexE 2)); +by (res_inst_tac [("x","f Int fa")] bexI 2); +by (etac mem_FiltersetD1 3); +by (assume_tac 3 THEN assume_tac 3); +by (Fast_tac 2); +by (EVERY[REPEAT(rtac allI 2), rtac impI 2,Asm_full_simp_tac 2]); +by (EVERY[REPEAT(etac conjE 2), etac bexE 2]); +by (res_inst_tac [("x","f")] bexI 2); +by (rtac subsetI 2); +by (Fast_tac 2 THEN assume_tac 2); +by (Step_tac 2); +by (Blast_tac 3); +by (eres_inst_tac [("c","A")] equalityCE 3); +by (REPEAT(Blast_tac 3)); +by (dres_inst_tac [("A","xa")] mem_FiltersetD3 2 THEN assume_tac 2); +by (Blast_tac 2); +by (dtac lemma_empty_Int_subset_Compl 1); +by (EVERY1[forward_tac [mem_Filterset_disjI], assume_tac, Fast_tac]); +by (dtac mem_FiltersetD3 1 THEN assume_tac 1); +by (dres_inst_tac [("x","f")] spec 1); +by (Blast_tac 1); +qed "max_Filter_Ultrafilter"; + +Goal "(F : Ultrafilter S) = (F: Filter S & (ALL G: Filter S. F <= G --> F = G))"; +by (blast_tac (claset() addSIs [Ultrafilter_max_Filter,max_Filter_Ultrafilter]) 1); +qed "Ultrafilter_iff"; + +(*-------------------------------------------------------------------- + A few properties of freefilters + -------------------------------------------------------------------*) + +Goal "F1 Int F2 = ((F1 Int Y) Int F2) Un ((F2 Int - Y) Int F1)"; +by (Auto_tac); +qed "lemma_Compl_cancel_eq"; + +Goal "finite X ==> finite (X Int Y)"; +by (etac (Int_lower1 RS finite_subset) 1); +qed "finite_IntI1"; + +Goal "finite Y ==> finite (X Int Y)"; +by (etac (Int_lower2 RS finite_subset) 1); +qed "finite_IntI2"; + +Goal "[| finite (F1 Int Y); \ +\ finite (F2 Int - Y) \ +\ |] ==> finite (F1 Int F2)"; +by (res_inst_tac [("Y1","Y")] (lemma_Compl_cancel_eq RS ssubst) 1); +by (rtac finite_UnI 1); +by (auto_tac (claset() addSIs [finite_IntI1,finite_IntI2],simpset())); +qed "finite_Int_Compl_cancel"; + +Goal "U: Freefilter S ==> \ +\ ~ (EX f1: U. EX f2: U. finite (f1 Int x) \ +\ & finite (f2 Int (- x)))"; +by (Step_tac 1); +by (forw_inst_tac [("A","f1"),("B","f2")] + (Freefilter_Filter RS mem_FiltersetD1) 1); +by (dres_inst_tac [("x","f1 Int f2")] mem_FreefiltersetD1 3); +by (dtac finite_Int_Compl_cancel 4); +by (Auto_tac); +qed "Freefilter_lemma_not_finite"; + +(* the lemmas below follow *) +Goal "U: Freefilter S ==> \ +\ ALL f: U. ~ finite (f Int x) | ~finite (f Int (- x))"; +by (blast_tac (claset() addSDs [Freefilter_lemma_not_finite,bspec]) 1); +qed "Freefilter_Compl_not_finite_disjI"; + +Goal "U: Freefilter S ==> \ +\ (ALL f: U. ~ finite (f Int x)) | (ALL f:U. ~finite (f Int (- x)))"; +by (blast_tac (claset() addSDs [Freefilter_lemma_not_finite,bspec]) 1); +qed "Freefilter_Compl_not_finite_disjI2"; + +Goal "- UNIV = {}"; +by (Auto_tac ); +qed "Compl_UNIV_eq"; + +Addsimps [Compl_UNIV_eq]; + +Goal "- {} = UNIV"; +by (Auto_tac ); +qed "Compl_empty_eq"; + +Addsimps [Compl_empty_eq]; + +val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \ +\ {A:: 'a set. finite (- A)} : Filter UNIV"; +by (cut_facts_tac [prem] 1); +by (rtac mem_FiltersetI2 1); +by (auto_tac (claset(),simpset() addsimps [Compl_Int])); +by (eres_inst_tac [("c","UNIV")] equalityCE 1); +by (Auto_tac); +by (etac (Compl_anti_mono RS finite_subset) 1); +by (assume_tac 1); +qed "cofinite_Filter"; + +Goal "~finite(UNIV :: 'a set) ==> ~finite (X :: 'a set) | ~finite (- X)"; +by (dres_inst_tac [("A1","X")] (Compl_partition RS ssubst) 1); +by (Asm_full_simp_tac 1); +qed "not_finite_UNIV_disjI"; + +Goal "[| ~finite(UNIV :: 'a set); \ +\ finite (X :: 'a set) \ +\ |] ==> ~finite (- X)"; +by (dres_inst_tac [("X","X")] not_finite_UNIV_disjI 1); +by (Blast_tac 1); +qed "not_finite_UNIV_Compl"; + +val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \ +\ !X: {A:: 'a set. finite (- A)}. ~ finite X"; +by (cut_facts_tac [prem] 1); +by (auto_tac (claset() addDs [not_finite_UNIV_disjI],simpset())); +qed "mem_cofinite_Filter_not_finite"; + +val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \ +\ {A:: 'a set. finite (- A)} : Freefilter UNIV"; +by (cut_facts_tac [prem] 1); +by (rtac mem_FreefiltersetI2 1); +by (rtac cofinite_Filter 1 THEN assume_tac 1); +by (blast_tac (claset() addSDs [mem_cofinite_Filter_not_finite]) 1); +qed "cofinite_Freefilter"; + +Goal "UNIV - x = - x"; +by (Auto_tac); +qed "UNIV_diff_Compl"; +Addsimps [UNIV_diff_Compl]; + +Goalw [Ultrafilter_def,FreeUltrafilter_def] + "[| ~finite(UNIV :: 'a set); (U :: 'a set set): FreeUltrafilter UNIV\ +\ |] ==> {X. finite(- X)} <= U"; +by (forward_tac [cofinite_Filter] 1); +by (Step_tac 1); +by (forw_inst_tac [("X","- x :: 'a set")] not_finite_UNIV_Compl 1); +by (assume_tac 1); +by (Step_tac 1 THEN Fast_tac 1); +by (dres_inst_tac [("x","x")] bspec 1); +by (Blast_tac 1); +by (asm_full_simp_tac (simpset() addsimps [UNIV_diff_Compl]) 1); +qed "FreeUltrafilter_contains_cofinite_set"; + +(*-------------------------------------------------------------------- + We prove: 1. Existence of maximal filter i.e. ultrafilter + 2. Freeness property i.e ultrafilter is free + Use a locale to prove various lemmas and then + export main result- The Ultrafilter Theorem + -------------------------------------------------------------------*) +Open_locale "UFT"; + +Goalw [chain_def, thm "superfrechet_def", thm "frechet_def"] + "!!(c :: 'a set set set). c : chain (superfrechet S) ==> Union c <= Pow S"; +by (Step_tac 1); +by (dtac subsetD 1 THEN assume_tac 1); +by (Step_tac 1); +by (dres_inst_tac [("X","X")] mem_FiltersetD3 1); +by (Auto_tac); +qed "chain_Un_subset_Pow"; + +Goalw [chain_def,Filter_def,is_Filter_def, + thm "superfrechet_def", thm "frechet_def"] + "!!(c :: 'a set set set). c: chain (superfrechet S) \ +\ ==> !x: c. {} < x"; +by (blast_tac (claset() addSIs [psubsetI]) 1); +qed "mem_chain_psubset_empty"; + +Goal "!!(c :: 'a set set set). \ +\ [| c: chain (superfrechet S);\ +\ c ~= {} \ +\ |]\ +\ ==> Union(c) ~= {}"; +by (dtac mem_chain_psubset_empty 1); +by (Step_tac 1); +by (dtac bspec 1 THEN assume_tac 1); +by (auto_tac (claset() addDs [Union_upper,bspec], + simpset() addsimps [psubset_def])); +qed "chain_Un_not_empty"; + +Goalw [is_Filter_def,Filter_def,chain_def,thm "superfrechet_def"] + "!!(c :: 'a set set set). \ +\ c : chain (superfrechet S) \ +\ ==> {} ~: Union(c)"; +by (Blast_tac 1); +qed "Filter_empty_not_mem_Un"; + +Goal "c: chain (superfrechet S) \ +\ ==> ALL u : Union(c). ALL v: Union(c). u Int v : Union(c)"; +by (Step_tac 1); +by (forw_inst_tac [("x","X"),("y","Xa")] chainD 1); +by (REPEAT(assume_tac 1)); +by (dtac chainD2 1); +by (etac disjE 1); +by (res_inst_tac [("X","Xa")] UnionI 1 THEN assume_tac 1); +by (dres_inst_tac [("A","X")] subsetD 1 THEN assume_tac 1); +by (dres_inst_tac [("c","Xa")] subsetD 1 THEN assume_tac 1); +by (res_inst_tac [("X","X")] UnionI 2 THEN assume_tac 2); +by (dres_inst_tac [("A","Xa")] subsetD 2 THEN assume_tac 2); +by (dres_inst_tac [("c","X")] subsetD 2 THEN assume_tac 2); +by (auto_tac (claset() addIs [mem_FiltersetD1], + simpset() addsimps [thm "superfrechet_def"])); +qed "Filter_Un_Int"; + +Goal "c: chain (superfrechet S) \ +\ ==> ALL u v. u: Union(c) & \ +\ (u :: 'a set) <= v & v <= S --> v: Union(c)"; +by (Step_tac 1); +by (dtac chainD2 1); +by (dtac subsetD 1 THEN assume_tac 1); +by (rtac UnionI 1 THEN assume_tac 1); +by (auto_tac (claset() addIs [mem_FiltersetD2], + simpset() addsimps [thm "superfrechet_def"])); +qed "Filter_Un_subset"; + +Goalw [chain_def,thm "superfrechet_def"] + "!!(c :: 'a set set set). \ +\ [| c: chain (superfrechet S);\ +\ x: c \ +\ |] ==> x : Filter S"; +by (Blast_tac 1); +qed "lemma_mem_chain_Filter"; + +Goalw [chain_def,thm "superfrechet_def"] + "!!(c :: 'a set set set). \ +\ [| c: chain (superfrechet S);\ +\ x: c \ +\ |] ==> frechet S <= x"; +by (Blast_tac 1); +qed "lemma_mem_chain_frechet_subset"; + +Goal "!!(c :: 'a set set set). \ +\ [| c ~= {}; \ +\ c : chain (superfrechet (UNIV :: 'a set))\ +\ |] ==> Union c : superfrechet (UNIV)"; +by (simp_tac (simpset() addsimps + [thm "superfrechet_def",thm "frechet_def"]) 1); +by (Step_tac 1); +by (rtac mem_FiltersetI2 1); +by (etac chain_Un_subset_Pow 1); +by (rtac UnionI 1 THEN assume_tac 1); +by (etac (lemma_mem_chain_Filter RS mem_FiltersetD4) 1 THEN assume_tac 1); +by (etac chain_Un_not_empty 1); +by (etac Filter_empty_not_mem_Un 2); +by (etac Filter_Un_Int 2); +by (etac Filter_Un_subset 2); +by (subgoal_tac "xa : frechet (UNIV)" 2); +by (rtac UnionI 2 THEN assume_tac 2); +by (rtac (lemma_mem_chain_frechet_subset RS subsetD) 2); +by (auto_tac (claset(),simpset() addsimps [thm "frechet_def"])); +qed "Un_chain_mem_cofinite_Filter_set"; + +Goal "EX U: superfrechet (UNIV). \ +\ ALL G: superfrechet (UNIV). U <= G --> U = G"; +by (rtac Zorn_Lemma2 1); +by (cut_facts_tac [thm "not_finite_UNIV" RS cofinite_Filter] 1); +by (Step_tac 1); +by (res_inst_tac [("Q","c={}")] (excluded_middle RS disjE) 1); +by (res_inst_tac [("x","Union c")] bexI 1 THEN Blast_tac 1); +by (rtac Un_chain_mem_cofinite_Filter_set 1 THEN REPEAT(assume_tac 1)); +by (res_inst_tac [("x","frechet (UNIV)")] bexI 1 THEN Blast_tac 1); +by (auto_tac (claset(),simpset() addsimps + [thm "superfrechet_def", thm "frechet_def"])); +qed "max_cofinite_Filter_Ex"; + +Goal "EX U: superfrechet UNIV. (\ +\ ALL G: superfrechet UNIV. U <= G --> U = G) \ +\ & (ALL x: U. ~finite x)"; +by (cut_facts_tac [thm "not_finite_UNIV" RS + (export max_cofinite_Filter_Ex)] 1); +by (Step_tac 1); +by (res_inst_tac [("x","U")] bexI 1); +by (auto_tac (claset(),simpset() addsimps + [thm "superfrechet_def", thm "frechet_def"])); +by (dres_inst_tac [("c","- x")] subsetD 1); +by (Asm_simp_tac 1); +by (forw_inst_tac [("A","x"),("B","- x")] mem_FiltersetD1 1); +by (dtac Filter_empty_not_mem 3); +by (ALLGOALS(Asm_full_simp_tac )); +qed "max_cofinite_Freefilter_Ex"; + +(*-------------------------------------------------------------------------------- + There exists a free ultrafilter on any infinite set + --------------------------------------------------------------------------------*) + +Goalw [FreeUltrafilter_def] "EX U. U: FreeUltrafilter (UNIV :: 'a set)"; +by (cut_facts_tac [thm "not_finite_UNIV" RS (export max_cofinite_Freefilter_Ex)] 1); +by (asm_full_simp_tac (simpset() addsimps + [thm "superfrechet_def", Ultrafilter_iff, thm "frechet_def"]) 1); +by (Step_tac 1); +by (res_inst_tac [("x","U")] exI 1); +by (Step_tac 1); +by (Blast_tac 1); +qed "FreeUltrafilter_ex"; + +val FreeUltrafilter_Ex = export FreeUltrafilter_ex; + +Close_locale(); + + diff -r fa2c2dd74f8c -r 11cbf236ca16 src/HOL/Real/Hyperreal/Filter.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/Hyperreal/Filter.thy Fri Nov 27 11:24:27 1998 +0100 @@ -0,0 +1,44 @@ +(* Title : Filter.thy + Author : Jacques D. Fleuriot + Copyright : 1998 University of Cambridge + Description : Filters and Ultrafilters +*) + +Filter = Zorn + + +constdefs + + is_Filter :: ['a set set,'a set] => bool + "is_Filter F S == (F <= Pow(S) & S : F & {} ~: F & + (ALL u: F. ALL v: F. u Int v : F) & + (ALL u v. u: F & u <= v & v <= S --> v: F))" + + Filter :: 'a set => 'a set set set + "Filter S == {X. is_Filter X S}" + + (* free filter does not contain any finite set *) + + Freefilter :: 'a set => 'a set set set + "Freefilter S == {X. X: Filter S & (ALL x: X. ~ finite x)}" + + Ultrafilter :: 'a set => 'a set set set + "Ultrafilter S == {X. X: Filter S & (ALL A: Pow(S). A: X | S - A : X)}" + + FreeUltrafilter :: 'a set => 'a set set set + "FreeUltrafilter S == {X. X: Ultrafilter S & (ALL x: X. ~ finite x)}" + + (* A locale makes proof of Ultrafilter Theorem more modular *) +locale UFT = + fixes frechet :: "'a set => 'a set set" + superfrechet :: "'a set => 'a set set set" + + assumes not_finite_UNIV "~finite (UNIV :: 'a set)" + + defines frechet_def "frechet S == {A. finite (S - A)}" + superfrechet_def "superfrechet S == + {G. G: Filter S & frechet S <= G}" +end + + + + diff -r fa2c2dd74f8c -r 11cbf236ca16 src/HOL/Real/Hyperreal/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/Hyperreal/README.html Fri Nov 27 11:24:27 1998 +0100 @@ -0,0 +1,23 @@ + +
Last modified on $Date$ + +