# HG changeset patch # User paulson # Date 978210226 -3600 # Node ID a681d3df1a39608418f5281ad51151cdae35bfd5 # Parent afdb47b973171141c15dc70a5b0588c8a5d14450 separation of HOL-Hyperreal from HOL-Real diff -r afdb47b97317 -r a681d3df1a39 src/HOL/Hyperreal/Filter.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hyperreal/Filter.ML Sat Dec 30 22:03:46 2000 +0100 @@ -0,0 +1,554 @@ +(* Title : Filter.ML + ID : $Id$ + Author : Jacques D. Fleuriot + Copyright : 1998 University of Cambridge + Description : Filters and Ultrafilter +*) + +(*------------------------------------------------------------------ + 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"; diff -r afdb47b97317 -r a681d3df1a39 src/HOL/Hyperreal/Filter.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hyperreal/Filter.thy Sat Dec 30 22:03:46 2000 +0100 @@ -0,0 +1,45 @@ +(* Title : Filter.thy + ID : $Id$ + 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 afdb47b97317 -r a681d3df1a39 src/HOL/Hyperreal/HRealAbs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hyperreal/HRealAbs.ML Sat Dec 30 22:03:46 2000 +0100 @@ -0,0 +1,206 @@ +(* Title : HRealAbs.ML + Author : Jacques D. Fleuriot + Copyright : 1998 University of Cambridge + Description : Absolute value function for the hyperreals + Similar to RealAbs.thy +*) + +(*------------------------------------------------------------ + absolute value on hyperreals as pointwise operation on + equivalence class representative + ------------------------------------------------------------*) + +Goalw [hrabs_def] + "abs (number_of v :: hypreal) = \ +\ (if neg (number_of v) then number_of (bin_minus v) \ +\ else number_of v)"; +by (Simp_tac 1); +qed "hrabs_number_of"; +Addsimps [hrabs_number_of]; + +Goalw [hrabs_def] + "abs (Abs_hypreal (hyprel ^^ {X})) = \ +\ Abs_hypreal(hyprel ^^ {%n. abs (X n)})"; +by (auto_tac (claset(), + simpset_of HyperDef.thy + addsimps [hypreal_zero_def, hypreal_le,hypreal_minus])); +by (ALLGOALS(Ultra_tac THEN' arith_tac )); +qed "hypreal_hrabs"; + +(*------------------------------------------------------------ + Properties of the absolute value function over the reals + (adapted version of previously proved theorems about abs) + ------------------------------------------------------------*) + +Goal "abs (#0::hypreal) = #0"; +by (simp_tac (simpset() addsimps [hrabs_def]) 1); +qed "hrabs_zero"; +Addsimps [hrabs_zero]; + +Goal "(#0::hypreal)<=x ==> abs x = x"; +by (asm_simp_tac (simpset() addsimps [hrabs_def]) 1); +qed "hrabs_eqI1"; + +Goal "(#0::hypreal) abs x = x"; +by (asm_simp_tac (simpset() addsimps [order_less_imp_le, hrabs_eqI1]) 1); +qed "hrabs_eqI2"; + +Goal "x<(#0::hypreal) ==> abs x = -x"; +by (asm_simp_tac (simpset() addsimps [hypreal_le_def, hrabs_def]) 1); +qed "hrabs_minus_eqI2"; + +Goal "x<=(#0::hypreal) ==> abs x = -x"; +by (auto_tac (claset() addDs [order_antisym], simpset() addsimps [hrabs_def])); +qed "hrabs_minus_eqI1"; + +Goal "(#0::hypreal)<= abs x"; +by (auto_tac (claset() addDs [hypreal_minus_zero_less_iff RS iffD2, + hypreal_less_asym], + simpset() addsimps [hypreal_le_def, hrabs_def])); +qed "hrabs_ge_zero"; + +Goal "abs(abs x) = abs (x::hypreal)"; +by (auto_tac (claset() addDs [hypreal_minus_zero_less_iff RS iffD2, + hypreal_less_asym], + simpset() addsimps [hypreal_le_def, hrabs_def])); +qed "hrabs_idempotent"; +Addsimps [hrabs_idempotent]; + +Goalw [hrabs_def] "(abs x = (#0::hypreal)) = (x=#0)"; +by (Simp_tac 1); +qed "hrabs_zero_iff"; +AddIffs [hrabs_zero_iff]; + +Goalw [hrabs_def] "(x::hypreal) <= abs x"; +by (auto_tac (claset() addDs [not_hypreal_leE, order_less_imp_le], + simpset() addsimps [hypreal_le_zero_iff RS sym])); +qed "hrabs_ge_self"; + +Goalw [hrabs_def] "-(x::hypreal) <= abs x"; +by (simp_tac (simpset() addsimps [hypreal_ge_zero_iff]) 1); +qed "hrabs_ge_minus_self"; + +(* very short proof by "transfer" *) +Goal "abs(x*(y::hypreal)) = (abs x)*(abs y)"; +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); +by (auto_tac (claset(), + simpset() addsimps [hypreal_hrabs, hypreal_mult,abs_mult])); +qed "hrabs_mult"; +Addsimps [hrabs_mult]; + +Goal "abs(inverse(x)) = inverse(abs(x::hypreal))"; +by (hypreal_div_undefined_case_tac "x=#0" 1); +by (simp_tac (simpset() addsimps [HYPREAL_DIVIDE_ZERO]) 1); +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); +by (auto_tac (claset(), + simpset() addsimps [hypreal_hrabs, + hypreal_inverse,hypreal_zero_def])); +by (ultra_tac (claset(), simpset() addsimps [abs_inverse]) 1); +qed "hrabs_inverse"; + +Goal "abs(x+(y::hypreal)) <= abs x + abs y"; +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); +by (auto_tac (claset(), + simpset() addsimps [hypreal_hrabs, hypreal_add,hypreal_le, + abs_triangle_ineq])); +qed "hrabs_triangle_ineq"; + +Goal "abs((w::hypreal) + x + y) <= abs(w) + abs(x) + abs(y)"; +by (auto_tac (claset() addSIs [hrabs_triangle_ineq RS order_trans, + hypreal_add_left_le_mono1], + simpset() addsimps [hypreal_add_assoc])); +qed "hrabs_triangle_ineq_three"; + +Goalw [hrabs_def] "abs(-x)=abs((x::hypreal))"; +by (auto_tac (claset() addSDs [not_hypreal_leE, hypreal_less_asym] + addIs [hypreal_le_anti_sym], + simpset() addsimps [hypreal_ge_zero_iff])); +qed "hrabs_minus_cancel"; +Addsimps [hrabs_minus_cancel]; + +val prem1::prem2::rest = goal thy + "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"; +by (rtac order_le_less_trans 1); +by (rtac hrabs_triangle_ineq 1); +by (rtac ([prem1,prem2] MRS hypreal_add_less_mono) 1); +qed "hrabs_add_less"; + +Goal "[| abs x abs x * abs y < r * (s::hypreal)"; +by (subgoal_tac "#0 < r" 1); +by (asm_full_simp_tac (simpset() addsimps [hrabs_def] + addsplits [split_if_asm]) 2); +by (case_tac "y = #0" 1); +by (asm_full_simp_tac (simpset() addsimps [hypreal_0_less_mult_iff]) 1); +by (rtac hypreal_mult_less_mono 1); +by (auto_tac (claset(), + simpset() addsimps [hrabs_def, linorder_neq_iff] + addsplits [split_if_asm])); +qed "hrabs_mult_less"; + +Goal "((#0::hypreal) < abs x) = (x ~= 0)"; +by (simp_tac (simpset() addsimps [hrabs_def]) 1); +by (arith_tac 1); +qed "hypreal_0_less_abs_iff"; +Addsimps [hypreal_0_less_abs_iff]; + +Goal "abs x < r ==> (#0::hypreal) < r"; +by (blast_tac (claset() addSIs [order_le_less_trans, hrabs_ge_zero]) 1); +qed "hrabs_less_gt_zero"; + +Goal "abs x = (x::hypreal) | abs x = -x"; +by (cut_inst_tac [("x","#0"),("y","x")] hypreal_linear 1); +by (fast_tac (claset() addIs [hrabs_eqI2,hrabs_minus_eqI2, + hrabs_zero]) 1); +qed "hrabs_disj"; + +Goal "abs x = (y::hypreal) ==> x = y | -x = y"; +by (dtac sym 1); +by (hyp_subst_tac 1); +by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1); +by (REPEAT(Asm_simp_tac 1)); +qed "hrabs_eq_disj"; + +Goal "(abs x < (r::hypreal)) = (-r < x & x < r)"; +by (Step_tac 1); +by (rtac (hypreal_less_swap_iff RS iffD2) 1); +by (asm_simp_tac (simpset() addsimps [(hrabs_ge_minus_self + RS order_le_less_trans)]) 1); +by (asm_simp_tac (simpset() addsimps [(hrabs_ge_self + RS order_le_less_trans)]) 1); +by (EVERY1 [dtac (hypreal_less_swap_iff RS iffD1), rotate_tac 1, + dtac (hypreal_minus_minus RS subst), + cut_inst_tac [("x","x")] hrabs_disj, dtac disjE ]); +by (assume_tac 3 THEN Auto_tac); +qed "hrabs_interval_iff"; + +Goal "(abs x < (r::hypreal)) = (- x < r & x < r)"; +by (auto_tac (claset(), simpset() addsimps [hrabs_interval_iff])); +qed "hrabs_interval_iff2"; + + +(* Needed in Geom.ML *) +Goal "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"; +by (asm_full_simp_tac (simpset() addsimps [hrabs_def] + addsplits [split_if_asm]) 1); +qed "hrabs_add_lemma_disj"; + +Goal "abs((x::hypreal) + -y) = abs (y + -x)"; +by (simp_tac (simpset() addsimps [hrabs_def]) 1); +qed "hrabs_minus_add_cancel"; + +(* Needed in Geom.ML?? *) +Goal "(x::hypreal) + - y + (z + - y) = abs (x + - z) ==> y = z | x = y"; +by (asm_full_simp_tac (simpset() addsimps [hrabs_def] + addsplits [split_if_asm]) 1); +qed "hrabs_add_lemma_disj2"; + + +(*---------------------------------------------------------- + Relating hrabs to abs through embedding of IR into IR* + ----------------------------------------------------------*) +Goalw [hypreal_of_real_def] + "abs (hypreal_of_real r) = hypreal_of_real (abs r)"; +by (auto_tac (claset(), simpset() addsimps [hypreal_hrabs])); +qed "hypreal_of_real_hrabs"; diff -r afdb47b97317 -r a681d3df1a39 src/HOL/Hyperreal/HRealAbs.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hyperreal/HRealAbs.thy Sat Dec 30 22:03:46 2000 +0100 @@ -0,0 +1,12 @@ +(* Title : HRealAbs.thy + Author : Jacques D. Fleuriot + Copyright : 1998 University of Cambridge + Description : Absolute value function for the hyperreals +*) + +HRealAbs = HyperArith + RealAbs + + +defs + hrabs_def "abs r == if (0::hypreal) <=r then r else -r" + +end \ No newline at end of file