# HG changeset patch
# User paulson
# Date 1091300063 -7200
# Node ID a7d1a3fdc30d62781a84af2c6109a565ed3ea723
# Parent  49ede01e9ee65bb688277efcd13ffe2b4b871878
conversion of Hyperreal/{Fact,Filter} to Isar scripts

diff -r 49ede01e9ee6 -r a7d1a3fdc30d src/HOL/Hyperreal/Fact.thy
--- a/src/HOL/Hyperreal/Fact.thy	Fri Jul 30 18:37:58 2004 +0200
+++ b/src/HOL/Hyperreal/Fact.thy	Sat Jul 31 20:54:23 2004 +0200
@@ -1,14 +1,74 @@
-(*  Title       : Fact.thy 
+(*  Title       : Fact.thy
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
-    Description : Factorial function
+    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
 *)
 
-Fact = NatStar + 
+header{*Factorial Function*}
+
+theory Fact = Real:
+
+consts fact :: "nat => nat"
+primrec
+   fact_0:     "fact 0 = 1"
+   fact_Suc:   "fact (Suc n) = (Suc n) * fact n"
+
+
+lemma fact_gt_zero [simp]: "0 < fact n"
+by (induct "n", auto)
+
+lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
+by simp
+
+lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
+by auto
+
+lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
+by auto
+
+lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
+by simp
+
+lemma fact_ge_one [simp]: "1 \<le> fact n"
+by (induct "n", auto)
 
-consts fact :: nat => nat 
-primrec 
-   fact_0     "fact 0 = 1"
-   fact_Suc   "fact (Suc n) = (Suc n) * fact n" 
+lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
+apply (drule le_imp_less_or_eq)
+apply (auto dest!: less_imp_Suc_add)
+apply (induct_tac "k", auto)
+done
+
+text{*Note that @{term "fact 0 = fact 1"}*}
+lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
+apply (drule_tac m = m in less_imp_Suc_add, auto)
+apply (induct_tac "k", auto)
+done
+
+lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
+by (auto simp add: positive_imp_inverse_positive)
+
+lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
+by (auto intro: order_less_imp_le)
+
+lemma fact_diff_Suc [rule_format]:
+     "\<forall>m. n < Suc m --> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
+apply (induct n, auto)
+apply (drule_tac x = "m - 1" in spec, auto)
+done
+
+lemma fact_num0 [simp]: "fact 0 = 1"
+by auto
+
+lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
+by (case_tac "m", auto)
+
+lemma fact_add_num_eq_if:
+     "fact (m+n) = (if (m+n = 0) then 1 else (m+n) * (fact (m + n - 1)))"
+by (case_tac "m+n", auto)
+
+lemma fact_add_num_eq_if2:
+     "fact (m+n) = (if m=0 then fact n else (m+n) * (fact ((m - 1) + n)))"
+by (case_tac "m", auto)
+
 
 end
\ No newline at end of file
diff -r 49ede01e9ee6 -r a7d1a3fdc30d src/HOL/Hyperreal/Filter.thy
--- a/src/HOL/Hyperreal/Filter.thy	Fri Jul 30 18:37:58 2004 +0200
+++ b/src/HOL/Hyperreal/Filter.thy	Sat Jul 31 20:54:23 2004 +0200
@@ -2,44 +2,517 @@
     ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
-    Description : Filters and Ultrafilters
+    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
 *) 
 
-Filter = Zorn + 
+header{*Filters and Ultrafilters*}
+
+theory 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))" 
+  is_Filter       :: "['a set set,'a set] => bool"
+  "is_Filter F S == (F <= Pow(S) & S \<in> F & {} ~: F &
+                   (\<forall>u \<in> F. \<forall>v \<in> F. u Int v \<in> F) &
+                   (\<forall>u v. u \<in> F & u <= v & v <= S --> v \<in> F))" 
 
-  Filter          :: 'a set => 'a set set set
+  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)}"
+  Freefilter      :: "'a set => 'a set set set"
+  "Freefilter S == {X. X \<in> Filter S & (\<forall>x \<in> 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)}"
+  Ultrafilter     :: "'a set => 'a set set set"
+  "Ultrafilter S == {X. X \<in> Filter S & (\<forall>A \<in> Pow(S). A \<in> X | S - A \<in> X)}"
 
-  FreeUltrafilter :: 'a set => 'a set set set
-  "FreeUltrafilter S == {X. X: Ultrafilter S & (ALL x: X. ~ finite x)}" 
+  FreeUltrafilter :: "'a set => 'a set set set"
+  "FreeUltrafilter S == {X. X \<in> Ultrafilter S & (\<forall>x \<in> 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"
+locale (open) UFT = 
+  fixes frechet      :: "'a set => 'a set set"
+    and superfrechet :: "'a set => 'a set set set"
+  assumes not_finite_UNIV:  "~finite (UNIV :: 'a set)"
+  defines frechet_def:  
+		"frechet S == {A. finite (S - A)}"
+      and superfrechet_def:
+		"superfrechet S == {G.  G \<in> Filter S & frechet S <= G}"
+
+
+(*------------------------------------------------------------------
+      Properties of Filters and Freefilters - 
+      rules for intro, destruction etc.
+ ------------------------------------------------------------------*)
+
+lemma is_FilterD1: "is_Filter X S ==> X <= Pow(S)"
+apply (simp add: is_Filter_def)
+done
+
+lemma is_FilterD2: "is_Filter X S ==> X ~= {}"
+apply (auto simp add: is_Filter_def)
+done
+
+lemma is_FilterD3: "is_Filter X S ==> {} ~: X"
+apply (simp add: is_Filter_def)
+done
+
+lemma mem_FiltersetI: "is_Filter X S ==> X \<in> Filter S"
+apply (simp add: Filter_def)
+done
+
+lemma mem_FiltersetD: "X \<in> Filter S ==> is_Filter X S"
+apply (simp add: Filter_def)
+done
+
+lemma Filter_empty_not_mem: "X \<in> Filter S ==> {} ~: X"
+apply (erule mem_FiltersetD [THEN is_FilterD3])
+done
+
+lemmas Filter_empty_not_memE = Filter_empty_not_mem [THEN notE, standard]
+
+lemma mem_FiltersetD1: "[| X \<in> Filter S; A \<in> X; B \<in> X |] ==> A Int B \<in> X"
+apply (unfold Filter_def is_Filter_def)
+apply blast
+done
+
+lemma mem_FiltersetD2: "[| X \<in> Filter S; A \<in> X; A <= B; B <= S|] ==> B \<in> X"
+apply (unfold Filter_def is_Filter_def)
+apply blast
+done
+
+lemma mem_FiltersetD3: "[| X \<in> Filter S; A \<in> X |] ==> A \<in> Pow S"
+apply (unfold Filter_def is_Filter_def)
+apply blast
+done
+
+lemma mem_FiltersetD4: "X \<in> Filter S  ==> S \<in> X"
+apply (unfold Filter_def is_Filter_def)
+apply blast
+done
+
+lemma is_FilterI: 
+      "[| X <= Pow(S); 
+               S \<in> X;  
+               X ~= {};  
+               {} ~: X;  
+               \<forall>u \<in> X. \<forall>v \<in> X. u Int v \<in> X;  
+               \<forall>u v. u \<in> X & u<=v & v<=S --> v \<in> X  
+            |] ==> is_Filter X S"
+apply (unfold is_Filter_def)
+apply blast
+done
+
+lemma mem_FiltersetI2: "[| X <= Pow(S); 
+               S \<in> X;  
+               X ~= {};  
+               {} ~: X;  
+               \<forall>u \<in> X. \<forall>v \<in> X. u Int v \<in> X;  
+               \<forall>u v. u \<in> X & u<=v & v<=S --> v \<in> X  
+            |] ==> X \<in> Filter S"
+by (blast intro: mem_FiltersetI is_FilterI)
+
+lemma is_FilterE_lemma: 
+      "is_Filter X S ==> X <= Pow(S) &  
+                           S \<in> X &  
+                           X ~= {} &  
+                           {} ~: X  &  
+                           (\<forall>u \<in> X. \<forall>v \<in> X. u Int v \<in> X) &  
+                           (\<forall>u v. u \<in> X & u <= v & v<=S --> v \<in> X)"
+apply (unfold is_Filter_def)
+apply fast
+done
+
+lemma memFiltersetE_lemma: 
+      "X \<in> Filter S ==> X <= Pow(S) & 
+                           S \<in> X &  
+                           X ~= {} &  
+                           {} ~: X  &  
+                           (\<forall>u \<in> X. \<forall>v \<in> X. u Int v \<in> X) &  
+                           (\<forall>u v. u \<in> X & u <= v & v<=S --> v \<in> X)"
+by (erule mem_FiltersetD [THEN is_FilterE_lemma])
+
+lemma Freefilter_Filter: "X \<in> Freefilter S ==> X \<in> Filter S"
+apply (simp add: Filter_def Freefilter_def)
+done
+
+lemma mem_Freefilter_not_finite: "X \<in> Freefilter S ==> \<forall>y \<in> X. ~finite(y)"
+apply (simp add: Freefilter_def)
+done
+
+lemma mem_FreefiltersetD1: "[| X \<in> Freefilter S; x \<in> X |] ==> ~ finite x"
+apply (blast dest!: mem_Freefilter_not_finite)
+done
 
-       assumes   not_finite_UNIV "~finite (UNIV :: 'a set)"
+lemmas mem_FreefiltersetE1 = mem_FreefiltersetD1 [THEN notE, standard]
+
+lemma mem_FreefiltersetD2: "[| X \<in> Freefilter S; finite x|] ==> x ~: X"
+apply (blast dest!: mem_Freefilter_not_finite)
+done
+
+lemma mem_FreefiltersetI1: 
+      "[| X \<in> Filter S; \<forall>x. ~(x \<in> X & finite x) |] ==> X \<in> Freefilter S"
+by (simp add: Freefilter_def)
+
+lemma mem_FreefiltersetI2: 
+      "[| X \<in> Filter S; \<forall>x. (x ~: X | ~ finite x) |] ==> X \<in> Freefilter S"
+by (simp add: Freefilter_def)
+
+lemma Filter_Int_not_empty: "[| X \<in> Filter S; A \<in> X; B \<in> X |] ==> A Int B ~= {}"
+apply (frule_tac A = "A" and B = "B" in mem_FiltersetD1)
+apply (auto dest!: Filter_empty_not_mem)
+done
+
+lemmas Filter_Int_not_emptyE = Filter_Int_not_empty [THEN notE, standard]
+
+subsection{*Ultrafilters and Free Ultrafilters*}
+
+lemma Ultrafilter_Filter: "X \<in> Ultrafilter S ==> X \<in> Filter S"
+apply (simp add: Ultrafilter_def)
+done
+
+lemma mem_UltrafiltersetD2: 
+      "X \<in> Ultrafilter S ==> \<forall>A \<in> Pow(S). A \<in> X | S - A \<in> X"
+by (auto simp add: Ultrafilter_def)
+
+lemma mem_UltrafiltersetD3: 
+      "[|X \<in> Ultrafilter S; A <= S; A ~: X |] ==> S - A \<in> X"
+by (auto simp add: Ultrafilter_def)
+
+lemma mem_UltrafiltersetD4: 
+      "[|X \<in> Ultrafilter S; A <= S; S - A ~: X |] ==> A \<in> X"
+by (auto simp add: Ultrafilter_def)
+
+lemma mem_UltrafiltersetI: 
+     "[| X \<in> Filter S;  
+         \<forall>A \<in> Pow(S). A \<in> X | S - A \<in> X |] ==> X \<in> Ultrafilter S"
+by (simp add: Ultrafilter_def)
+
+lemma FreeUltrafilter_Ultrafilter: 
+     "X \<in> FreeUltrafilter S ==> X \<in> Ultrafilter S"
+by (auto simp add: Ultrafilter_def FreeUltrafilter_def)
+
+lemma mem_FreeUltrafilter_not_finite: 
+     "X \<in> FreeUltrafilter S ==> \<forall>y \<in> X. ~finite(y)"
+by (simp add: FreeUltrafilter_def)
+
+lemma mem_FreeUltrafiltersetD1: "[| X \<in> FreeUltrafilter S; x \<in> X |] ==> ~ finite x"
+apply (blast dest!: mem_FreeUltrafilter_not_finite)
+done
 
-       defines   frechet_def "frechet S == {A. finite (S - A)}"
-                 superfrechet_def "superfrechet S == 
-                                   {G.  G: Filter S & frechet S <= G}"
-end
+lemmas mem_FreeUltrafiltersetE1 = mem_FreeUltrafiltersetD1 [THEN notE, standard]
+
+lemma mem_FreeUltrafiltersetD2: "[| X \<in> FreeUltrafilter S; finite x|] ==> x ~: X"
+apply (blast dest!: mem_FreeUltrafilter_not_finite)
+done
+
+lemma mem_FreeUltrafiltersetI1: 
+      "[| X \<in> Ultrafilter S;  
+          \<forall>x. ~(x \<in> X & finite x) |] ==> X \<in> FreeUltrafilter S"
+by (simp add: FreeUltrafilter_def)
+
+lemma mem_FreeUltrafiltersetI2: 
+      "[| X \<in> Ultrafilter S;  
+          \<forall>x. (x ~: X | ~ finite x) |] ==> X \<in> FreeUltrafilter S"
+by (simp add: FreeUltrafilter_def)
+
+lemma FreeUltrafilter_iff: 
+     "(X \<in> FreeUltrafilter S) = (X \<in> Freefilter S & (\<forall>x \<in> Pow(S). x \<in> X | S - x \<in> X))"
+by (auto simp add: FreeUltrafilter_def Freefilter_def Ultrafilter_def)
+
+
+(*-------------------------------------------------------------------
+   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 
+ ---------------------------------------------------------------------*)
+lemma lemma_set_extend: "[| F ~= {}; A <= S |] ==> \<exists>x. x \<in> {X. X <= S & (\<exists>f \<in> F. A Int f <= X)}"
+apply blast
+done
+
+lemma lemma_set_not_empty: "a \<in> X ==> X ~= {}"
+apply (safe)
+done
+
+lemma lemma_empty_Int_subset_Compl: "x Int F <= {} ==> F <= - x"
+apply blast
+done
+
+lemma mem_Filterset_disjI: 
+      "[| F \<in> Filter S; A ~: F; A <= S|]  
+           ==> \<forall>B. B ~: F | ~ B <= A"
+apply (unfold Filter_def is_Filter_def)
+apply blast
+done
+
+lemma Ultrafilter_max_Filter: "F \<in> Ultrafilter S ==>  
+          (F \<in> Filter S & (\<forall>G \<in> Filter S. F <= G --> F = G))"
+apply (auto simp add: Ultrafilter_def)
+apply (drule_tac x = "x" in bspec)
+apply (erule mem_FiltersetD3 , assumption)
+apply (safe)
+apply (drule subsetD , assumption)
+apply (blast dest!: Filter_Int_not_empty)
+done
 
 
+(*--------------------------------------------------------------------------------
+     This is a very long and tedious proof; need to break it into parts.
+     Have proof that {X. X <= S & (\<exists>f \<in> F. A Int f <= X)} is a filter as 
+     a lemma
+--------------------------------------------------------------------------------*)
+lemma max_Filter_Ultrafilter: 
+      "[| F \<in> Filter S;  
+          \<forall>G \<in> Filter S. F <= G --> F = G |] ==> F \<in> Ultrafilter S"
+apply (simp add: Ultrafilter_def)
+apply (safe)
+apply (rule ccontr)
+apply (frule mem_FiltersetD [THEN is_FilterD2])
+apply (frule_tac x = "{X. X <= S & (\<exists>f \<in> F. A Int f <= X) }" in bspec)
+apply (rule mem_FiltersetI2) 
+apply (blast intro: elim:); 
+apply (simp add: ); 
+apply (blast dest: mem_FiltersetD3)
+apply (erule lemma_set_extend [THEN exE])
+apply (assumption , erule lemma_set_not_empty)
+txt{*First we prove @{term "{} \<notin> {X. X \<subseteq> S \<and> (\<exists>f\<in>F. A \<inter> f \<subseteq> X)}"}*}
+   apply (clarify ); 
+   apply (drule lemma_empty_Int_subset_Compl)
+   apply (frule mem_Filterset_disjI) 
+   apply assumption; 
+   apply (blast intro: elim:); 
+   apply (fast dest: mem_FiltersetD3 elim:) 
+txt{*Next case: @{term "u \<inter> v"} is an element*}
+  apply (intro ballI) 
+apply (simp add: ); 
+  apply (rule conjI, blast) 
+apply (clarify ); 
+  apply (rule_tac x = "f Int fa" in bexI)
+   apply (fast intro: elim:); 
+  apply (blast dest: mem_FiltersetD1 elim:)
+ apply force;
+apply (blast dest: mem_FiltersetD3 elim:) 
+done
+
+lemma Ultrafilter_iff: "(F \<in> Ultrafilter S) = (F \<in> Filter S & (\<forall>G \<in> Filter S. F <= G --> F = G))"
+apply (blast intro!: Ultrafilter_max_Filter max_Filter_Ultrafilter)
+done
 
 
+subsection{* A Few Properties of Freefilters*}
+
+lemma lemma_Compl_cancel_eq: "F1 Int F2 = ((F1 Int Y) Int F2) Un ((F2 Int (- Y)) Int F1)"
+apply auto
+done
+
+lemma finite_IntI1: "finite X ==> finite (X Int Y)"
+apply (erule Int_lower1 [THEN finite_subset])
+done
+
+lemma finite_IntI2: "finite Y ==> finite (X Int Y)"
+apply (erule Int_lower2 [THEN finite_subset])
+done
+
+lemma finite_Int_Compl_cancel: "[| finite (F1 Int Y);  
+                  finite (F2 Int (- Y))  
+               |] ==> finite (F1 Int F2)"
+apply (rule_tac Y1 = "Y" in lemma_Compl_cancel_eq [THEN ssubst])
+apply (rule finite_UnI)
+apply (auto intro!: finite_IntI1 finite_IntI2)
+done
+
+lemma Freefilter_lemma_not_finite: "U \<in> Freefilter S  ==>  
+          ~ (\<exists>f1 \<in> U. \<exists>f2 \<in> U. finite (f1 Int x)  
+                             & finite (f2 Int (- x)))"
+apply (safe)
+apply (frule_tac A = "f1" and B = "f2" in Freefilter_Filter [THEN mem_FiltersetD1])
+apply (drule_tac [3] x = "f1 Int f2" in mem_FreefiltersetD1)
+apply (drule_tac [4] finite_Int_Compl_cancel)
+apply auto
+done
+
+(* the lemmas below follow *)
+lemma Freefilter_Compl_not_finite_disjI: "U \<in> Freefilter S ==>  
+           \<forall>f \<in> U. ~ finite (f Int x) | ~finite (f Int (- x))"
+by (blast dest!: Freefilter_lemma_not_finite bspec)
+
+lemma Freefilter_Compl_not_finite_disjI2: "U \<in> Freefilter S ==> (\<forall>f \<in> U. ~ finite (f Int x)) | (\<forall>f \<in> U. ~finite (f Int (- x)))"
+apply (blast dest!: Freefilter_lemma_not_finite bspec)
+done
+
+lemma cofinite_Filter: "~ finite (UNIV:: 'a set) ==> {A:: 'a set. finite (- A)} \<in> Filter UNIV"
+apply (rule mem_FiltersetI2)
+apply (auto simp del: Collect_empty_eq)
+apply (erule_tac c = "UNIV" in equalityCE)
+apply auto
+apply (erule Compl_anti_mono [THEN finite_subset])
+apply assumption
+done
+
+lemma not_finite_UNIV_disjI: "~finite(UNIV :: 'a set) ==> ~finite (X :: 'a set) | ~finite (- X)" 
+apply (drule_tac A1 = "X" in Compl_partition [THEN ssubst])
+apply simp
+done
+
+lemma not_finite_UNIV_Compl: "[| ~finite(UNIV :: 'a set); finite (X :: 'a set) |] ==>  ~finite (- X)"
+apply (drule_tac X = "X" in not_finite_UNIV_disjI)
+apply blast
+done
+
+lemma mem_cofinite_Filter_not_finite:
+     "~ finite (UNIV:: 'a set) 
+      ==> \<forall>X \<in> {A:: 'a set. finite (- A)}. ~ finite X"
+by (auto dest: not_finite_UNIV_disjI)
+
+lemma cofinite_Freefilter:
+    "~ finite (UNIV:: 'a set) ==> {A:: 'a set. finite (- A)} \<in> Freefilter UNIV"
+apply (rule mem_FreefiltersetI2)
+apply (rule cofinite_Filter , assumption)
+apply (blast dest!: mem_cofinite_Filter_not_finite)
+done
+
+(*????Set.thy*)
+lemma UNIV_diff_Compl [simp]: "UNIV - x = - x"
+apply auto
+done
+
+lemma FreeUltrafilter_contains_cofinite_set: 
+     "[| ~finite(UNIV :: 'a set); (U :: 'a set set): FreeUltrafilter UNIV 
+          |] ==> {X. finite(- X)} <= U"
+by (auto simp add: Ultrafilter_def FreeUltrafilter_def)
+
+(*--------------------------------------------------------------------
+   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
+ -------------------------------------------------------------------*)
+
+lemma (in UFT) chain_Un_subset_Pow: 
+   "!!(c :: 'a set set set). c \<in> chain (superfrechet S) ==>  Union c <= Pow S"
+apply (simp add: chain_def superfrechet_def frechet_def)
+apply (blast dest: mem_FiltersetD3 elim:) 
+done
+
+lemma (in UFT) mem_chain_psubset_empty: 
+          "!!(c :: 'a set set set). c: chain (superfrechet S)  
+          ==> !x: c. {} < x"
+by (auto simp add: chain_def Filter_def is_Filter_def superfrechet_def frechet_def)
+
+lemma (in UFT) chain_Un_not_empty: "!!(c :: 'a set set set).  
+             [| c: chain (superfrechet S); 
+                c ~= {} |] 
+             ==> Union(c) ~= {}"
+apply (drule mem_chain_psubset_empty)
+apply (safe)
+apply (drule bspec , assumption)
+apply (auto dest: Union_upper bspec simp add: psubset_def)
+done
+
+lemma (in UFT) Filter_empty_not_mem_Un: 
+       "!!(c :: 'a set set set). c \<in> chain (superfrechet S) ==> {} ~: Union(c)"
+by (auto simp add: is_Filter_def Filter_def chain_def superfrechet_def)
+
+lemma (in UFT) Filter_Un_Int: "c \<in> chain (superfrechet S)  
+          ==> \<forall>u \<in> Union(c). \<forall>v \<in> Union(c). u Int v \<in> Union(c)"
+apply (safe)
+apply (frule_tac x = "X" and y = "Xa" in chainD)
+apply (assumption)+
+apply (drule chainD2)
+apply (erule disjE)
+ apply (rule_tac [2] X = "X" in UnionI)
+  apply (rule_tac X = "Xa" in UnionI)
+apply (auto intro: mem_FiltersetD1 simp add: superfrechet_def)
+done
+
+lemma (in UFT) Filter_Un_subset: "c \<in> chain (superfrechet S)  
+          ==> \<forall>u v. u \<in> Union(c) &  
+                  (u :: 'a set) <= v & v <= S --> v \<in> Union(c)"
+apply (safe)
+apply (drule chainD2)
+apply (drule subsetD , assumption)
+apply (rule UnionI , assumption)
+apply (auto intro: mem_FiltersetD2 simp add: superfrechet_def)
+done
+
+lemma (in UFT) lemma_mem_chain_Filter:
+      "!!(c :: 'a set set set).  
+             [| c \<in> chain (superfrechet S); 
+                x \<in> c  
+             |] ==> x \<in> Filter S"
+by (auto simp add: chain_def superfrechet_def)
+
+lemma (in UFT) lemma_mem_chain_frechet_subset: 
+     "!!(c :: 'a set set set).  
+             [| c \<in> chain (superfrechet S); 
+                x \<in> c  
+             |] ==> frechet S <= x"
+by (auto simp add: chain_def superfrechet_def)
+
+lemma (in UFT) Un_chain_mem_cofinite_Filter_set: "!!(c :: 'a set set set).  
+          [| c ~= {};  
+             c \<in> chain (superfrechet (UNIV :: 'a set)) 
+          |] ==> Union c \<in> superfrechet (UNIV)"
+apply (simp (no_asm) add: superfrechet_def frechet_def)
+apply (safe)
+apply (rule mem_FiltersetI2)
+apply (erule chain_Un_subset_Pow)
+apply (rule UnionI , assumption)
+apply (erule lemma_mem_chain_Filter [THEN mem_FiltersetD4] , assumption)
+apply (erule chain_Un_not_empty)
+apply (erule_tac [2] Filter_empty_not_mem_Un)
+apply (erule_tac [2] Filter_Un_Int)
+apply (erule_tac [2] Filter_Un_subset)
+apply (subgoal_tac [2] "xa \<in> frechet (UNIV) ")
+apply (blast intro: elim:); 
+apply (rule UnionI)
+apply assumption; 
+apply (rule lemma_mem_chain_frechet_subset [THEN subsetD])
+apply (auto simp add: frechet_def)
+done
+
+lemma (in UFT) max_cofinite_Filter_Ex: "\<exists>U \<in> superfrechet (UNIV).  
+                \<forall>G \<in> superfrechet (UNIV). U <= G --> U = G"
+apply (rule Zorn_Lemma2)
+apply (insert not_finite_UNIV [THEN cofinite_Filter])
+apply (safe)
+apply (rule_tac Q = "c={}" in excluded_middle [THEN disjE])
+apply (rule_tac x = "Union c" in bexI , blast)
+apply (rule Un_chain_mem_cofinite_Filter_set);
+apply (auto simp add: superfrechet_def frechet_def)
+done
+
+lemma (in UFT) max_cofinite_Freefilter_Ex: "\<exists>U \<in> superfrechet UNIV. ( 
+                \<forall>G \<in> superfrechet UNIV. U <= G --> U = G)   
+                              & (\<forall>x \<in> U. ~finite x)"
+apply (insert not_finite_UNIV [THEN UFT.max_cofinite_Filter_Ex]);
+apply (safe)
+apply (rule_tac x = "U" in bexI)
+apply (auto simp add: superfrechet_def frechet_def)
+apply (drule_tac c = "- x" in subsetD)
+apply (simp (no_asm_simp))
+apply (frule_tac A = "x" and B = "- x" in mem_FiltersetD1)
+apply (drule_tac [3] Filter_empty_not_mem)
+apply (auto ); 
+done
+
+text{*There exists a free ultrafilter on any infinite set*}
+
+theorem (in UFT) FreeUltrafilter_ex: "\<exists>U. U \<in> FreeUltrafilter (UNIV :: 'a set)"
+apply (simp add: FreeUltrafilter_def)
+apply (insert not_finite_UNIV [THEN UFT.max_cofinite_Freefilter_Ex])
+apply (simp add: superfrechet_def Ultrafilter_iff frechet_def)
+apply (safe)
+apply (rule_tac x = "U" in exI)
+apply (safe)
+apply blast
+done
+
+theorems FreeUltrafilter_Ex = UFT.FreeUltrafilter_ex
+
+end
diff -r 49ede01e9ee6 -r a7d1a3fdc30d src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Fri Jul 30 18:37:58 2004 +0200
+++ b/src/HOL/Hyperreal/Integration.thy	Sat Jul 31 20:54:23 2004 +0200
@@ -83,7 +83,7 @@
 apply (rotate_tac 2)
 apply (drule_tac x = N in spec, simp)
 apply (drule_tac x = Na in spec)
-apply (drule_tac x = "Suc Na" and P = "%n. Na \<le> n \<longrightarrow> D n = D Na" in spec, auto)
+apply (drule_tac x = "Suc Na" and P = "%n. Na\<le>n \<longrightarrow> D n = D Na" in spec, auto)
 done
 
 lemma partition_rhs: "partition(a,b) D ==> (D(psize D) = b)"
@@ -203,7 +203,7 @@
 lemma lemma_psize1:
      "[| partition (a, b) D1; partition (b, c) D2; N < psize D1 |]
       ==> D1(N) < D2 (psize D2)"
-apply (rule_tac y = "D1 (psize D1) " in order_less_le_trans)
+apply (rule_tac y = "D1 (psize D1)" in order_less_le_trans)
 apply (erule partition_gt, assumption)
 apply (auto simp add: partition_rhs partition_le)
 done
@@ -319,7 +319,7 @@
 apply (drule fine_min)
 apply (drule spec)+
 apply auto
-apply (subgoal_tac "abs ((rsum (D,p) f - k2) - (rsum (D,p) f - k1)) < \<bar>k1 - k2\<bar> ")
+apply (subgoal_tac "\<bar>(rsum (D,p) f - k2) - (rsum (D,p) f - k1)\<bar> < \<bar>k1 - k2\<bar>")
 apply arith
 apply (drule add_strict_mono, assumption)
 apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] 
@@ -363,7 +363,7 @@
 apply (rule exI, auto)
 apply (drule spec)+
 apply auto
-apply (rule_tac z1 = "inverse (abs c) " in real_mult_less_iff1 [THEN iffD1])
+apply (rule_tac z1 = "inverse (abs c)" in real_mult_less_iff1 [THEN iffD1])
 apply (auto simp add: divide_inverse [symmetric] right_diff_distrib [symmetric])
 done
 
@@ -385,14 +385,14 @@
 
 
 (* new simplifications e.g. (y < x/n) = (y * n < x) are a real nuisance
-   they break the original proofs and make new proofs longer!                 *)
+   they break the original proofs and make new proofs longer!*)
 lemma strad1:
        "\<lbrakk>\<forall>xa::real. xa \<noteq> x \<and> \<bar>xa + - x\<bar> < s \<longrightarrow>
              \<bar>(f xa - f x) / (xa - x) + - f' x\<bar> * 2 < e;
         0 < e; a \<le> x; x \<le> b; 0 < s\<rbrakk>
        \<Longrightarrow> \<forall>z. \<bar>z - x\<bar> < s -->\<bar>f z - f x - f' x * (z - x)\<bar> * 2 \<le> e * \<bar>z - x\<bar>"
 apply auto
-apply (case_tac "0 < \<bar>z - x\<bar> ")
+apply (case_tac "0 < \<bar>z - x\<bar>")
  prefer 2 apply (simp add: zero_less_abs_iff)
 apply (drule_tac x = z in spec)
 apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>" 
@@ -413,10 +413,12 @@
      "[| \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x); 0 < e |]
       ==> \<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
                 (\<forall>x u v. a \<le> u & u \<le> x & x \<le> v & v \<le> b & (v - u) < g(x)
-                  --> abs((f(v) - f(u)) - (f'(x) * (v - u))) \<le> e * (v - u))"
+                  --> \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
 apply (simp add: gauge_def)
 apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> 
-        (\<exists>d. 0 < d & (\<forall>u v. u \<le> x & x \<le> v & (v - u) < d --> abs ((f (v) - f (u)) - (f' (x) * (v - u))) \<le> e * (v - u)))")
+        (\<exists>d. 0 < d & 
+             (\<forall>u v. u \<le> x & x \<le> v & (v - u) < d --> 
+                \<bar>(f (v) - f (u)) - (f' (x) * (v - u))\<bar> \<le> e * (v - u)))")
 apply (drule choiceP, auto)
 apply (drule spec, auto)
 apply (auto simp add: DERIV_iff2 LIM_def)
@@ -424,13 +426,14 @@
 apply (frule strad1, assumption+)
 apply (rule_tac x = s in exI, auto)
 apply (rule_tac x = u and y = v in linorder_cases, auto)
-apply (rule_tac j = "abs ((f (v) - f (x)) - (f' (x) * (v - x))) + abs ((f (x) - f (u)) - (f' (x) * (x - u)))"
+apply (rule_tac j = "\<bar>(f (v) - f (x)) - (f' (x) * (v - x))\<bar> + 
+                     \<bar>(f (x) - f (u)) - (f' (x) * (x - u))\<bar>"
        in real_le_trans)
 apply (rule abs_triangle_ineq [THEN [2] real_le_trans])
 apply (simp add: right_diff_distrib, arith)
-apply (rule_tac t = "e* (v - u) " in real_sum_of_halves [THEN subst])
+apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst])
 apply (rule add_mono)
-apply (rule_tac j = " (e / 2) * \<bar>v - x\<bar> " in real_le_trans)
+apply (rule_tac j = " (e / 2) * \<bar>v - x\<bar>" in real_le_trans)
  prefer 2 apply simp apply arith
 apply (erule_tac [!]
        V= "\<forall>xa. xa ~= x & \<bar>xa + - x\<bar> < s --> \<bar>(f xa - f x) / (xa - x) + - f' x\<bar> * 2 < e"
@@ -453,19 +456,19 @@
 apply (drule_tac x = "e/2" in spec, auto)
 apply (drule spec, auto)
 apply ((drule spec)+, auto)
-apply (drule_tac e = "ea/ (b - a) " in lemma_straddle)
+apply (drule_tac e = "ea/ (b - a)" in lemma_straddle)
 apply (auto simp add: zero_less_divide_iff)
 apply (rule exI)
 apply (auto simp add: tpart_def rsum_def)
-apply (subgoal_tac "sumr 0 (psize D) (%n. f (D (Suc n)) - f (D n)) = f b - f a")
+apply (subgoal_tac "sumr 0 (psize D) (%n. f(D(Suc n)) - f(D n)) = f b - f a")
  prefer 2
- apply (cut_tac D = "%n. f (D n) " and m = "psize D"
+ apply (cut_tac D = "%n. f (D n)" and m = "psize D"
         in sumr_partition_eq_diff_bounds)
  apply (simp add: partition_lhs partition_rhs)
 apply (drule sym, simp)
 apply (simp (no_asm) add: sumr_diff)
 apply (rule sumr_rabs [THEN real_le_trans])
-apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D (Suc n) - (D n))) ")
+apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D (Suc n) - (D n)))")
 apply (simp add: abs_minus_commute)
 apply (rule_tac t = ea in ssubst, assumption)
 apply (rule sumr_le2)
@@ -775,8 +778,8 @@
 apply (drule_tac x = "na + n" in spec)
 apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto, arith)
 apply (simp add: tpart_def, safe)
-apply (subgoal_tac "D n \<le> p (na + n) ")
-apply (drule_tac y = "p (na + n) " in real_le_imp_less_or_eq)
+apply (subgoal_tac "D n \<le> p (na + n)")
+apply (drule_tac y = "p (na + n)" in real_le_imp_less_or_eq)
 apply safe
 apply (simp split: split_if_asm, simp)
 apply (drule less_le_trans, assumption)
@@ -790,7 +793,7 @@
 lemma rsum_add: "rsum (D, p) (%x. f x + g x) =  rsum (D, p) f + rsum(D, p) g"
 by (simp add: rsum_def sumr_add left_distrib)
 
-(* Bartle/Sherbert: Theorem 10.1.5 p. 278 *)
+text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *}
 lemma Integral_add_fun:
     "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) g k2 |]
      ==> Integral(a,b) (%x. f x + g x) (k1 + k2)"
@@ -798,7 +801,7 @@
 apply ((drule_tac x = "e/2" in spec)+)
 apply auto
 apply (drule gauge_min, assumption)
-apply (rule_tac x = " (%x. if ga x < gaa x then ga x else gaa x) " in exI)
+apply (rule_tac x = " (%x. if ga x < gaa x then ga x else gaa x)" in exI)
 apply auto
 apply (drule fine_min)
 apply ((drule spec)+, auto)
@@ -852,7 +855,7 @@
 apply (drule_tac x = D in spec, drule_tac x = D in spec)
 apply (drule_tac x = p in spec, drule_tac x = p in spec, auto)
 apply (frule lemma_Integral_rsum_le, assumption)
-apply (subgoal_tac "\<bar>(rsum (D,p) f - k1) - (rsum (D,p) g - k2)\<bar> < \<bar>k1 - k2\<bar> ")
+apply (subgoal_tac "\<bar>(rsum (D,p) f - k1) - (rsum (D,p) g - k2)\<bar> < \<bar>k1 - k2\<bar>")
 apply arith
 apply (drule add_strict_mono, assumption)
 apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
diff -r 49ede01e9ee6 -r a7d1a3fdc30d src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jul 30 18:37:58 2004 +0200
+++ b/src/HOL/IsaMakefile	Sat Jul 31 20:54:23 2004 +0200
@@ -144,10 +144,9 @@
   Real/Lubs.thy Real/rat_arith.ML\
   Real/Rational.thy Real/PReal.thy Real/RComplete.thy \
   Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy \
-  Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
-  Hyperreal/EvenOdd.thy\
-  Hyperreal/Fact.ML Hyperreal/Fact.thy Hyperreal/HLog.thy\
-  Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HSeries.thy\
+  Real/RealPow.thy Real/document/root.tex\
+  Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy\
+  Hyperreal/Filter.thy Hyperreal/HSeries.thy\
   Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy\
   Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\
   Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\