src/HOL/Hyperreal/HyperDef.thy
author wenzelm
Sun Apr 09 18:51:13 2006 +0200 (2006-04-09)
changeset 19380 b808efaa5828
parent 17429 e8d6ed3aacfe
child 19765 dfe940911617
permissions -rw-r--r--
tuned syntax/abbreviations;
     1 (*  Title       : HOL/Real/Hyperreal/HyperDef.thy
     2     ID          : $Id$
     3     Author      : Jacques D. Fleuriot
     4     Copyright   : 1998  University of Cambridge
     5     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     6 *)
     7 
     8 header{*Construction of Hyperreals Using Ultrafilters*}
     9 
    10 theory HyperDef
    11 imports StarClasses "../Real/Real"
    12 uses ("fuf.ML")  (*Warning: file fuf.ML refers to the name Hyperdef!*)
    13 begin
    14 
    15 types hypreal = "real star"
    16 
    17 abbreviation
    18   hypreal_of_real :: "real => real star"
    19   "hypreal_of_real == star_of"
    20 
    21 constdefs
    22 
    23   omega   :: hypreal   -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
    24   "omega == star_n (%n. real (Suc n))"
    25 
    26   epsilon :: hypreal   -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
    27   "epsilon == star_n (%n. inverse (real (Suc n)))"
    28 
    29 syntax (xsymbols)
    30   omega   :: hypreal   ("\<omega>")
    31   epsilon :: hypreal   ("\<epsilon>")
    32 
    33 syntax (HTML output)
    34   omega   :: hypreal   ("\<omega>")
    35   epsilon :: hypreal   ("\<epsilon>")
    36 
    37 
    38 subsection{*Existence of Free Ultrafilter over the Naturals*}
    39 
    40 text{*Also, proof of various properties of @{term FreeUltrafilterNat}: 
    41 an arbitrary free ultrafilter*}
    42 
    43 lemma FreeUltrafilterNat_Ex: "\<exists>U::nat set set. freeultrafilter U"
    44 by (rule nat_infinite [THEN freeultrafilter_Ex])
    45 
    46 lemma FreeUltrafilterNat_mem: "freeultrafilter FreeUltrafilterNat"
    47 apply (unfold FreeUltrafilterNat_def)
    48 apply (rule someI_ex)
    49 apply (rule FreeUltrafilterNat_Ex)
    50 done
    51 
    52 lemma UltrafilterNat_mem: "ultrafilter FreeUltrafilterNat"
    53 by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.ultrafilter])
    54 
    55 lemma FilterNat_mem: "filter FreeUltrafilterNat"
    56 by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.filter])
    57 
    58 lemma FreeUltrafilterNat_finite: "finite x ==> x \<notin> FreeUltrafilterNat"
    59 by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.finite])
    60 
    61 lemma FreeUltrafilterNat_not_finite: "x \<in> FreeUltrafilterNat ==> ~ finite x"
    62 by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.infinite])
    63 
    64 lemma FreeUltrafilterNat_empty [simp]: "{} \<notin> FreeUltrafilterNat"
    65 by (rule FilterNat_mem [THEN filter.empty])
    66 
    67 lemma FreeUltrafilterNat_Int:
    68      "[| X \<in> FreeUltrafilterNat;  Y \<in> FreeUltrafilterNat |]   
    69       ==> X Int Y \<in> FreeUltrafilterNat"
    70 by (rule FilterNat_mem [THEN filter.Int])
    71 
    72 lemma FreeUltrafilterNat_subset:
    73      "[| X \<in> FreeUltrafilterNat;  X \<subseteq> Y |]  
    74       ==> Y \<in> FreeUltrafilterNat"
    75 by (rule FilterNat_mem [THEN filter.subset])
    76 
    77 lemma FreeUltrafilterNat_Compl:
    78      "X \<in> FreeUltrafilterNat ==> -X \<notin> FreeUltrafilterNat"
    79 apply (erule contrapos_pn)
    80 apply (erule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff, THEN iffD2])
    81 done
    82 
    83 lemma FreeUltrafilterNat_Compl_mem:
    84      "X\<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat"
    85 by (rule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff, THEN iffD1])
    86 
    87 lemma FreeUltrafilterNat_Compl_iff1:
    88      "(X \<notin> FreeUltrafilterNat) = (-X \<in> FreeUltrafilterNat)"
    89 by (rule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff])
    90 
    91 lemma FreeUltrafilterNat_Compl_iff2:
    92      "(X \<in> FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)"
    93 by (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric])
    94 
    95 lemma cofinite_mem_FreeUltrafilterNat: "finite (-X) ==> X \<in> FreeUltrafilterNat"
    96 apply (drule FreeUltrafilterNat_finite)  
    97 apply (simp add: FreeUltrafilterNat_Compl_iff2 [symmetric])
    98 done
    99 
   100 lemma FreeUltrafilterNat_UNIV [iff]: "UNIV \<in> FreeUltrafilterNat"
   101 by (rule FilterNat_mem [THEN filter.UNIV])
   102 
   103 lemma FreeUltrafilterNat_Nat_set_refl [intro]:
   104      "{n. P(n) = P(n)} \<in> FreeUltrafilterNat"
   105 by simp
   106 
   107 lemma FreeUltrafilterNat_P: "{n::nat. P} \<in> FreeUltrafilterNat ==> P"
   108 by (rule ccontr, simp)
   109 
   110 lemma FreeUltrafilterNat_Ex_P: "{n. P(n)} \<in> FreeUltrafilterNat ==> \<exists>n. P(n)"
   111 by (rule ccontr, simp)
   112 
   113 lemma FreeUltrafilterNat_all: "\<forall>n. P(n) ==> {n. P(n)} \<in> FreeUltrafilterNat"
   114 by (auto)
   115 
   116 
   117 text{*Define and use Ultrafilter tactics*}
   118 use "fuf.ML"
   119 
   120 method_setup fuf = {*
   121     Method.ctxt_args (fn ctxt =>
   122         Method.METHOD (fn facts =>
   123             fuf_tac (local_clasimpset_of ctxt) 1)) *}
   124     "free ultrafilter tactic"
   125 
   126 method_setup ultra = {*
   127     Method.ctxt_args (fn ctxt =>
   128         Method.METHOD (fn facts =>
   129             ultra_tac (local_clasimpset_of ctxt) 1)) *}
   130     "ultrafilter tactic"
   131 
   132 
   133 text{*One further property of our free ultrafilter*}
   134 lemma FreeUltrafilterNat_Un:
   135      "X Un Y \<in> FreeUltrafilterNat  
   136       ==> X \<in> FreeUltrafilterNat | Y \<in> FreeUltrafilterNat"
   137 by (auto, ultra)
   138 
   139 
   140 subsection{*Properties of @{term starrel}*}
   141 
   142 text{*Proving that @{term starrel} is an equivalence relation*}
   143 
   144 lemma starrel_iff: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> FreeUltrafilterNat)"
   145 by (rule StarDef.starrel_iff)
   146 
   147 lemma starrel_refl: "(x,x) \<in> starrel"
   148 by (simp add: starrel_def)
   149 
   150 lemma starrel_sym [rule_format (no_asm)]: "(x,y) \<in> starrel --> (y,x) \<in> starrel"
   151 by (simp add: starrel_def eq_commute)
   152 
   153 lemma starrel_trans: 
   154       "[|(x,y) \<in> starrel; (y,z) \<in> starrel|] ==> (x,z) \<in> starrel"
   155 by (simp add: starrel_def, ultra)
   156 
   157 lemma equiv_starrel: "equiv UNIV starrel"
   158 by (rule StarDef.equiv_starrel)
   159 
   160 (* (starrel `` {x} = starrel `` {y}) = ((x,y) \<in> starrel) *)
   161 lemmas equiv_starrel_iff =
   162     eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I, simp] 
   163 
   164 lemma starrel_in_hypreal [simp]: "starrel``{x}:star"
   165 by (simp add: star_def starrel_def quotient_def, blast)
   166 
   167 declare Abs_star_inject [simp] Abs_star_inverse [simp]
   168 declare equiv_starrel [THEN eq_equiv_class_iff, simp]
   169 
   170 lemmas eq_starrelD = eq_equiv_class [OF _ equiv_starrel]
   171 
   172 lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}"
   173 by (simp add: starrel_def)
   174 
   175 lemma hypreal_empty_not_mem [simp]: "{} \<notin> star"
   176 apply (simp add: star_def)
   177 apply (auto elim!: quotientE equalityCE)
   178 done
   179 
   180 lemma Rep_hypreal_nonempty [simp]: "Rep_star x \<noteq> {}"
   181 by (insert Rep_star [of x], auto)
   182 
   183 subsection{*@{term hypreal_of_real}: 
   184             the Injection from @{typ real} to @{typ hypreal}*}
   185 
   186 lemma inj_hypreal_of_real: "inj(hypreal_of_real)"
   187 by (rule inj_onI, simp)
   188 
   189 lemma Rep_star_star_n_iff [simp]:
   190   "(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)"
   191 by (simp add: star_n_def)
   192 
   193 lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)"
   194 by simp
   195 
   196 subsection{* Properties of @{term star_n} *}
   197 
   198 lemma star_n_add:
   199   "star_n X + star_n Y = star_n (%n. X n + Y n)"
   200 by (simp only: star_add_def starfun2_star_n)
   201 
   202 lemma star_n_minus:
   203    "- star_n X = star_n (%n. -(X n))"
   204 by (simp only: star_minus_def starfun_star_n)
   205 
   206 lemma star_n_diff:
   207      "star_n X - star_n Y = star_n (%n. X n - Y n)"
   208 by (simp only: star_diff_def starfun2_star_n)
   209 
   210 lemma star_n_mult:
   211   "star_n X * star_n Y = star_n (%n. X n * Y n)"
   212 by (simp only: star_mult_def starfun2_star_n)
   213 
   214 lemma star_n_inverse:
   215       "inverse (star_n X) = star_n (%n. inverse(X n))"
   216 by (simp only: star_inverse_def starfun_star_n)
   217 
   218 lemma star_n_le:
   219       "star_n X \<le> star_n Y =  
   220        ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
   221 by (simp only: star_le_def starP2_star_n)
   222 
   223 lemma star_n_less:
   224       "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)"
   225 by (simp only: star_less_def starP2_star_n)
   226 
   227 lemma star_n_zero_num: "0 = star_n (%n. 0)"
   228 by (simp only: star_zero_def star_of_def)
   229 
   230 lemma star_n_one_num: "1 = star_n (%n. 1)"
   231 by (simp only: star_one_def star_of_def)
   232 
   233 lemma star_n_abs:
   234      "abs (star_n X) = star_n (%n. abs (X n))"
   235 by (simp only: star_abs_def starfun_star_n)
   236 
   237 subsection{*Misc Others*}
   238 
   239 lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y"
   240 by (auto)
   241 
   242 lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
   243 by auto
   244 
   245 lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
   246 by auto
   247     
   248 lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
   249 by auto
   250 
   251 lemma hypreal_omega_gt_zero [simp]: "0 < omega"
   252 by (simp add: omega_def star_n_zero_num star_n_less)
   253 
   254 subsection{*Existence of Infinite Hyperreal Number*}
   255 
   256 text{*Existence of infinite number not corresponding to any real number.
   257 Use assumption that member @{term FreeUltrafilterNat} is not finite.*}
   258 
   259 
   260 text{*A few lemmas first*}
   261 
   262 lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} |  
   263       (\<exists>y. {n::nat. x = real n} = {y})"
   264 by force
   265 
   266 lemma lemma_finite_omega_set: "finite {n::nat. x = real n}"
   267 by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto)
   268 
   269 lemma not_ex_hypreal_of_real_eq_omega: 
   270       "~ (\<exists>x. hypreal_of_real x = omega)"
   271 apply (simp add: omega_def)
   272 apply (simp add: star_of_def star_n_eq_iff)
   273 apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] 
   274             lemma_finite_omega_set [THEN FreeUltrafilterNat_finite])
   275 done
   276 
   277 lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> omega"
   278 by (insert not_ex_hypreal_of_real_eq_omega, auto)
   279 
   280 text{*Existence of infinitesimal number also not corresponding to any
   281  real number*}
   282 
   283 lemma lemma_epsilon_empty_singleton_disj:
   284      "{n::nat. x = inverse(real(Suc n))} = {} |  
   285       (\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})"
   286 by auto
   287 
   288 lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}"
   289 by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto)
   290 
   291 lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\<exists>x. hypreal_of_real x = epsilon)"
   292 by (auto simp add: epsilon_def star_of_def star_n_eq_iff
   293                    lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite])
   294 
   295 lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> epsilon"
   296 by (insert not_ex_hypreal_of_real_eq_epsilon, auto)
   297 
   298 lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0"
   299 by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff
   300          del: star_of_zero)
   301 
   302 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
   303 by (simp add: epsilon_def omega_def star_n_inverse)
   304 
   305 
   306 ML
   307 {*
   308 val omega_def = thm "omega_def";
   309 val epsilon_def = thm "epsilon_def";
   310 
   311 val FreeUltrafilterNat_Ex = thm "FreeUltrafilterNat_Ex";
   312 val FreeUltrafilterNat_mem = thm "FreeUltrafilterNat_mem";
   313 val FreeUltrafilterNat_finite = thm "FreeUltrafilterNat_finite";
   314 val FreeUltrafilterNat_not_finite = thm "FreeUltrafilterNat_not_finite";
   315 val FreeUltrafilterNat_empty = thm "FreeUltrafilterNat_empty";
   316 val FreeUltrafilterNat_Int = thm "FreeUltrafilterNat_Int";
   317 val FreeUltrafilterNat_subset = thm "FreeUltrafilterNat_subset";
   318 val FreeUltrafilterNat_Compl = thm "FreeUltrafilterNat_Compl";
   319 val FreeUltrafilterNat_Compl_mem = thm "FreeUltrafilterNat_Compl_mem";
   320 val FreeUltrafilterNat_Compl_iff1 = thm "FreeUltrafilterNat_Compl_iff1";
   321 val FreeUltrafilterNat_Compl_iff2 = thm "FreeUltrafilterNat_Compl_iff2";
   322 val FreeUltrafilterNat_UNIV = thm "FreeUltrafilterNat_UNIV";
   323 val FreeUltrafilterNat_Nat_set_refl = thm "FreeUltrafilterNat_Nat_set_refl";
   324 val FreeUltrafilterNat_P = thm "FreeUltrafilterNat_P";
   325 val FreeUltrafilterNat_Ex_P = thm "FreeUltrafilterNat_Ex_P";
   326 val FreeUltrafilterNat_all = thm "FreeUltrafilterNat_all";
   327 val FreeUltrafilterNat_Un = thm "FreeUltrafilterNat_Un";
   328 val starrel_iff = thm "starrel_iff";
   329 val starrel_in_hypreal = thm "starrel_in_hypreal";
   330 val Abs_star_inverse = thm "Abs_star_inverse";
   331 val lemma_starrel_refl = thm "lemma_starrel_refl";
   332 val hypreal_empty_not_mem = thm "hypreal_empty_not_mem";
   333 val Rep_hypreal_nonempty = thm "Rep_hypreal_nonempty";
   334 val inj_hypreal_of_real = thm "inj_hypreal_of_real";
   335 (* val eq_Abs_star = thm "eq_Abs_star"; *)
   336 val star_n_minus = thm "star_n_minus";
   337 val star_n_add = thm "star_n_add";
   338 val star_n_diff = thm "star_n_diff";
   339 val star_n_mult = thm "star_n_mult";
   340 val star_n_inverse = thm "star_n_inverse";
   341 val hypreal_mult_left_cancel = thm "hypreal_mult_left_cancel";
   342 val hypreal_mult_right_cancel = thm "hypreal_mult_right_cancel";
   343 val hypreal_not_refl2 = thm "hypreal_not_refl2";
   344 val star_n_less = thm "star_n_less";
   345 val hypreal_eq_minus_iff = thm "hypreal_eq_minus_iff";
   346 val star_n_le = thm "star_n_le";
   347 val star_n_zero_num = thm "star_n_zero_num";
   348 val star_n_one_num = thm "star_n_one_num";
   349 val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero";
   350 
   351 val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj";
   352 val lemma_finite_omega_set = thm"lemma_finite_omega_set";
   353 val not_ex_hypreal_of_real_eq_omega = thm"not_ex_hypreal_of_real_eq_omega";
   354 val hypreal_of_real_not_eq_omega = thm"hypreal_of_real_not_eq_omega";
   355 val not_ex_hypreal_of_real_eq_epsilon = thm"not_ex_hypreal_of_real_eq_epsilon";
   356 val hypreal_of_real_not_eq_epsilon = thm"hypreal_of_real_not_eq_epsilon";
   357 val hypreal_epsilon_not_zero = thm"hypreal_epsilon_not_zero";
   358 val hypreal_epsilon_inverse_omega = thm"hypreal_epsilon_inverse_omega";
   359 *}
   360 
   361 end