# HG changeset patch # User paulson # Date 1091438437 -7200 # Node ID dfb4e23923e044d02ea57f8250a7a6b38d7a3b95 # Parent 6d8619440ea03116df162bdf838c587719cda034 conversion of Hyperreal/Filter to Isar scripts diff -r 6d8619440ea0 -r dfb4e23923e0 src/HOL/Hyperreal/Filter.ML --- a/src/HOL/Hyperreal/Filter.ML Mon Aug 02 10:16:58 2004 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,560 +0,0 @@ -(* Title : Filter.ML - ID : $Id$ - Author : Jacques D. Fleuriot - Copyright : 1998 University of Cambridge - Description : Filters and Ultrafilter -*) - -(*ML bindings for Library/Zorn theorems*) -val chain_def = thm "chain_def"; -val chainD = thm "chainD"; -val chainD2 = thm "chainD2"; -val Zorn_Lemma2 = thm "Zorn_Lemma2"; - -(*------------------------------------------------------------------ - 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[ftac 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 (the_context ()) "~ 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() delsimps [Collect_empty_eq])); -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 (the_context ()) "~ 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 (the_context ()) "~ 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 (ftac 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"; - -bind_thm ("FreeUltrafilter_Ex", export FreeUltrafilter_ex); - -Close_locale "UFT";