src/HOL/Hyperreal/HyperNat.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15169 2b5da07a0b89
permissions -rw-r--r--
import -> imports
     1 (*  Title       : HyperNat.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998  University of Cambridge
     4 
     5 Converted to Isar and polished by lcp    
     6 *)
     7 
     8 header{*Construction of Hypernaturals using Ultrafilters*}
     9 
    10 theory HyperNat
    11 imports Star
    12 begin
    13 
    14 constdefs
    15     hypnatrel :: "((nat=>nat)*(nat=>nat)) set"
    16     "hypnatrel == {p. \<exists>X Y. p = ((X::nat=>nat),Y) &
    17                        {n::nat. X(n) = Y(n)} \<in> FreeUltrafilterNat}"
    18 
    19 typedef hypnat = "UNIV//hypnatrel"
    20     by (auto simp add: quotient_def)
    21 
    22 instance hypnat :: "{ord, zero, one, plus, times, minus}" ..
    23 
    24 consts whn :: hypnat
    25 
    26 
    27 defs (overloaded)
    28 
    29   (** hypernatural arithmetic **)
    30 
    31   hypnat_zero_def:  "0 == Abs_hypnat(hypnatrel``{%n::nat. 0})"
    32   hypnat_one_def:   "1 == Abs_hypnat(hypnatrel``{%n::nat. 1})"
    33 
    34   (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
    35   hypnat_omega_def:  "whn == Abs_hypnat(hypnatrel``{%n::nat. n})"
    36 
    37   hypnat_add_def:
    38   "P + Q == Abs_hypnat(\<Union>X \<in> Rep_hypnat(P). \<Union>Y \<in> Rep_hypnat(Q).
    39                 hypnatrel``{%n::nat. X n + Y n})"
    40 
    41   hypnat_mult_def:
    42   "P * Q == Abs_hypnat(\<Union>X \<in> Rep_hypnat(P). \<Union>Y \<in> Rep_hypnat(Q).
    43                 hypnatrel``{%n::nat. X n * Y n})"
    44 
    45   hypnat_minus_def:
    46   "P - Q == Abs_hypnat(\<Union>X \<in> Rep_hypnat(P). \<Union>Y \<in> Rep_hypnat(Q).
    47                 hypnatrel``{%n::nat. X n - Y n})"
    48 
    49   hypnat_le_def:
    50   "P \<le> (Q::hypnat) == \<exists>X Y. X \<in> Rep_hypnat(P) & Y \<in> Rep_hypnat(Q) &
    51                             {n::nat. X n \<le> Y n} \<in> FreeUltrafilterNat"
    52 
    53   hypnat_less_def: "(x < (y::hypnat)) == (x \<le> y & x \<noteq> y)"
    54 
    55 
    56 
    57 subsection{*Properties of @{term hypnatrel}*}
    58 
    59 text{*Proving that @{term hypnatrel} is an equivalence relation*}
    60 
    61 lemma hypnatrel_iff:
    62      "((X,Y) \<in> hypnatrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
    63 apply (simp add: hypnatrel_def)
    64 done
    65 
    66 lemma hypnatrel_refl: "(x,x) \<in> hypnatrel"
    67 by (simp add: hypnatrel_def)
    68 
    69 lemma hypnatrel_sym: "(x,y) \<in> hypnatrel ==> (y,x) \<in> hypnatrel"
    70 by (auto simp add: hypnatrel_def eq_commute)
    71 
    72 lemma hypnatrel_trans [rule_format (no_asm)]:
    73      "(x,y) \<in> hypnatrel --> (y,z) \<in> hypnatrel --> (x,z) \<in> hypnatrel"
    74 by (auto simp add: hypnatrel_def, ultra)
    75 
    76 lemma equiv_hypnatrel:
    77      "equiv UNIV hypnatrel"
    78 apply (simp add: equiv_def refl_def sym_def trans_def hypnatrel_refl)
    79 apply (blast intro: hypnatrel_sym hypnatrel_trans)
    80 done
    81 
    82 (* (hypnatrel `` {x} = hypnatrel `` {y}) = ((x,y) \<in> hypnatrel) *)
    83 lemmas equiv_hypnatrel_iff =
    84     eq_equiv_class_iff [OF equiv_hypnatrel UNIV_I UNIV_I, simp]
    85 
    86 lemma hypnatrel_in_hypnat [simp]: "hypnatrel``{x}:hypnat"
    87 by (simp add: hypnat_def hypnatrel_def quotient_def, blast)
    88 
    89 lemma inj_on_Abs_hypnat: "inj_on Abs_hypnat hypnat"
    90 apply (rule inj_on_inverseI)
    91 apply (erule Abs_hypnat_inverse)
    92 done
    93 
    94 declare inj_on_Abs_hypnat [THEN inj_on_iff, simp]
    95         Abs_hypnat_inverse [simp]
    96 
    97 declare equiv_hypnatrel [THEN eq_equiv_class_iff, simp]
    98 
    99 declare hypnatrel_iff [iff]
   100 
   101 
   102 lemma inj_Rep_hypnat: "inj(Rep_hypnat)"
   103 apply (rule inj_on_inverseI)
   104 apply (rule Rep_hypnat_inverse)
   105 done
   106 
   107 lemma lemma_hypnatrel_refl: "x \<in> hypnatrel `` {x}"
   108 by (simp add: hypnatrel_def)
   109 
   110 declare lemma_hypnatrel_refl [simp]
   111 
   112 lemma hypnat_empty_not_mem: "{} \<notin> hypnat"
   113 apply (simp add: hypnat_def)
   114 apply (auto elim!: quotientE equalityCE)
   115 done
   116 
   117 declare hypnat_empty_not_mem [simp]
   118 
   119 lemma Rep_hypnat_nonempty: "Rep_hypnat x \<noteq> {}"
   120 by (cut_tac x = x in Rep_hypnat, auto)
   121 
   122 declare Rep_hypnat_nonempty [simp]
   123 
   124 
   125 lemma eq_Abs_hypnat:
   126     "(!!x. z = Abs_hypnat(hypnatrel``{x}) ==> P) ==> P"
   127 apply (rule_tac x1=z in Rep_hypnat [unfolded hypnat_def, THEN quotientE])
   128 apply (drule_tac f = Abs_hypnat in arg_cong)
   129 apply (force simp add: Rep_hypnat_inverse)
   130 done
   131 
   132 theorem hypnat_cases [case_names Abs_hypnat, cases type: hypnat]:
   133     "(!!x. z = Abs_hypnat(hypnatrel``{x}) ==> P) ==> P"
   134 by (rule eq_Abs_hypnat [of z], blast)
   135 
   136 subsection{*Hypernat Addition*}
   137 
   138 lemma hypnat_add_congruent2:
   139      "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})"
   140 by (simp add: congruent2_def, auto, ultra)
   141 
   142 lemma hypnat_add:
   143   "Abs_hypnat(hypnatrel``{%n. X n}) + Abs_hypnat(hypnatrel``{%n. Y n}) =
   144    Abs_hypnat(hypnatrel``{%n. X n + Y n})"
   145 by (simp add: hypnat_add_def 
   146     UN_equiv_class2 [OF equiv_hypnatrel equiv_hypnatrel hypnat_add_congruent2])
   147 
   148 lemma hypnat_add_commute: "(z::hypnat) + w = w + z"
   149 apply (cases z, cases w)
   150 apply (simp add: add_ac hypnat_add)
   151 done
   152 
   153 lemma hypnat_add_assoc: "((z1::hypnat) + z2) + z3 = z1 + (z2 + z3)"
   154 apply (cases z1, cases z2, cases z3)
   155 apply (simp add: hypnat_add nat_add_assoc)
   156 done
   157 
   158 lemma hypnat_add_zero_left: "(0::hypnat) + z = z"
   159 apply (cases z)
   160 apply (simp add: hypnat_zero_def hypnat_add)
   161 done
   162 
   163 instance hypnat :: comm_monoid_add
   164   by intro_classes
   165     (assumption |
   166       rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+
   167 
   168 
   169 subsection{*Subtraction inverse on @{typ hypreal}*}
   170 
   171 
   172 lemma hypnat_minus_congruent2:
   173     "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})"
   174 by (simp add: congruent2_def, auto, ultra)
   175 
   176 lemma hypnat_minus:
   177   "Abs_hypnat(hypnatrel``{%n. X n}) - Abs_hypnat(hypnatrel``{%n. Y n}) =
   178    Abs_hypnat(hypnatrel``{%n. X n - Y n})"
   179 by (simp add: hypnat_minus_def 
   180   UN_equiv_class2 [OF equiv_hypnatrel equiv_hypnatrel hypnat_minus_congruent2])
   181 
   182 lemma hypnat_minus_zero: "z - z = (0::hypnat)"
   183 apply (cases z)
   184 apply (simp add: hypnat_zero_def hypnat_minus)
   185 done
   186 
   187 lemma hypnat_diff_0_eq_0: "(0::hypnat) - n = 0"
   188 apply (cases n)
   189 apply (simp add: hypnat_minus hypnat_zero_def)
   190 done
   191 
   192 declare hypnat_minus_zero [simp] hypnat_diff_0_eq_0 [simp]
   193 
   194 lemma hypnat_add_is_0: "(m+n = (0::hypnat)) = (m=0 & n=0)"
   195 apply (cases m, cases n)
   196 apply (auto intro: FreeUltrafilterNat_subset dest: FreeUltrafilterNat_Int simp add: hypnat_zero_def hypnat_add)
   197 done
   198 
   199 declare hypnat_add_is_0 [iff]
   200 
   201 lemma hypnat_diff_diff_left: "(i::hypnat) - j - k = i - (j+k)"
   202 apply (cases i, cases j, cases k)
   203 apply (simp add: hypnat_minus hypnat_add diff_diff_left)
   204 done
   205 
   206 lemma hypnat_diff_commute: "(i::hypnat) - j - k = i-k-j"
   207 by (simp add: hypnat_diff_diff_left hypnat_add_commute)
   208 
   209 lemma hypnat_diff_add_inverse: "((n::hypnat) + m) - n = m"
   210 apply (cases m, cases n)
   211 apply (simp add: hypnat_minus hypnat_add)
   212 done
   213 declare hypnat_diff_add_inverse [simp]
   214 
   215 lemma hypnat_diff_add_inverse2:  "((m::hypnat) + n) - n = m"
   216 apply (cases m, cases n)
   217 apply (simp add: hypnat_minus hypnat_add)
   218 done
   219 declare hypnat_diff_add_inverse2 [simp]
   220 
   221 lemma hypnat_diff_cancel: "((k::hypnat) + m) - (k+n) = m - n"
   222 apply (cases k, cases m, cases n)
   223 apply (simp add: hypnat_minus hypnat_add)
   224 done
   225 declare hypnat_diff_cancel [simp]
   226 
   227 lemma hypnat_diff_cancel2: "((m::hypnat) + k) - (n+k) = m - n"
   228 by (simp add: hypnat_add_commute [of _ k])
   229 declare hypnat_diff_cancel2 [simp]
   230 
   231 lemma hypnat_diff_add_0: "(n::hypnat) - (n+m) = (0::hypnat)"
   232 apply (cases m, cases n)
   233 apply (simp add: hypnat_zero_def hypnat_minus hypnat_add)
   234 done
   235 declare hypnat_diff_add_0 [simp]
   236 
   237 
   238 subsection{*Hyperreal Multiplication*}
   239 
   240 lemma hypnat_mult_congruent2:
   241     "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})"
   242 by (simp add: congruent2_def, auto, ultra)
   243 
   244 lemma hypnat_mult:
   245   "Abs_hypnat(hypnatrel``{%n. X n}) * Abs_hypnat(hypnatrel``{%n. Y n}) =
   246    Abs_hypnat(hypnatrel``{%n. X n * Y n})"
   247 by (simp add: hypnat_mult_def
   248    UN_equiv_class2 [OF equiv_hypnatrel equiv_hypnatrel hypnat_mult_congruent2])
   249 
   250 lemma hypnat_mult_commute: "(z::hypnat) * w = w * z"
   251 by (cases z, cases w, simp add: hypnat_mult mult_ac)
   252 
   253 lemma hypnat_mult_assoc: "((z1::hypnat) * z2) * z3 = z1 * (z2 * z3)"
   254 apply (cases z1, cases z2, cases z3)
   255 apply (simp add: hypnat_mult mult_assoc)
   256 done
   257 
   258 lemma hypnat_mult_1: "(1::hypnat) * z = z"
   259 apply (cases z)
   260 apply (simp add: hypnat_mult hypnat_one_def)
   261 done
   262 
   263 lemma hypnat_diff_mult_distrib: "((m::hypnat) - n) * k = (m * k) - (n * k)"
   264 apply (cases k, cases m, cases n)
   265 apply (simp add: hypnat_mult hypnat_minus diff_mult_distrib)
   266 done
   267 
   268 lemma hypnat_diff_mult_distrib2: "(k::hypnat) * (m - n) = (k * m) - (k * n)"
   269 by (simp add: hypnat_diff_mult_distrib hypnat_mult_commute [of k])
   270 
   271 lemma hypnat_add_mult_distrib: "((z1::hypnat) + z2) * w = (z1 * w) + (z2 * w)"
   272 apply (cases z1, cases z2, cases w)
   273 apply (simp add: hypnat_mult hypnat_add add_mult_distrib)
   274 done
   275 
   276 lemma hypnat_add_mult_distrib2: "(w::hypnat) * (z1 + z2) = (w * z1) + (w * z2)"
   277 by (simp add: hypnat_mult_commute [of w] hypnat_add_mult_distrib)
   278 
   279 text{*one and zero are distinct*}
   280 lemma hypnat_zero_not_eq_one: "(0::hypnat) \<noteq> (1::hypnat)"
   281 by (auto simp add: hypnat_zero_def hypnat_one_def)
   282 declare hypnat_zero_not_eq_one [THEN not_sym, simp]
   283 
   284 
   285 text{*The hypernaturals form a @{text comm_semiring_1_cancel}: *}
   286 instance hypnat :: comm_semiring_1_cancel
   287 proof
   288   fix i j k :: hypnat
   289   show "(i * j) * k = i * (j * k)" by (rule hypnat_mult_assoc)
   290   show "i * j = j * i" by (rule hypnat_mult_commute)
   291   show "1 * i = i" by (rule hypnat_mult_1)
   292   show "(i + j) * k = i * k + j * k" by (simp add: hypnat_add_mult_distrib)
   293   show "0 \<noteq> (1::hypnat)" by (rule hypnat_zero_not_eq_one)
   294   assume "k+i = k+j"
   295   hence "(k+i) - k = (k+j) - k" by simp
   296   thus "i=j" by simp
   297 qed
   298 
   299 
   300 subsection{*Properties of The @{text "\<le>"} Relation*}
   301 
   302 lemma hypnat_le:
   303       "(Abs_hypnat(hypnatrel``{%n. X n}) \<le> Abs_hypnat(hypnatrel``{%n. Y n})) =
   304        ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
   305 apply (simp add: hypnat_le_def)
   306 apply (auto intro!: lemma_hypnatrel_refl, ultra)
   307 done
   308 
   309 lemma hypnat_le_refl: "w \<le> (w::hypnat)"
   310 apply (cases w)
   311 apply (simp add: hypnat_le)
   312 done
   313 
   314 lemma hypnat_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::hypnat)"
   315 apply (cases i, cases j, cases k)
   316 apply (simp add: hypnat_le, ultra)
   317 done
   318 
   319 lemma hypnat_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypnat)"
   320 apply (cases z, cases w)
   321 apply (simp add: hypnat_le, ultra)
   322 done
   323 
   324 (* Axiom 'order_less_le' of class 'order': *)
   325 lemma hypnat_less_le: "((w::hypnat) < z) = (w \<le> z & w \<noteq> z)"
   326 by (simp add: hypnat_less_def)
   327 
   328 instance hypnat :: order
   329   by intro_classes
   330     (assumption |
   331       rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+
   332 
   333 (* Axiom 'linorder_linear' of class 'linorder': *)
   334 lemma hypnat_le_linear: "(z::hypnat) \<le> w | w \<le> z"
   335 apply (cases z, cases w)
   336 apply (auto simp add: hypnat_le, ultra)
   337 done
   338 
   339 instance hypnat :: linorder
   340   by intro_classes (rule hypnat_le_linear)
   341 
   342 lemma hypnat_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypnat)"
   343 apply (cases x, cases y, cases z)
   344 apply (auto simp add: hypnat_le hypnat_add)
   345 done
   346 
   347 lemma hypnat_mult_less_mono2: "[| (0::hypnat)<z; x<y |] ==> z*x<z*y"
   348 apply (cases x, cases y, cases z)
   349 apply (simp add: hypnat_zero_def  hypnat_mult linorder_not_le [symmetric])
   350 apply (auto simp add: hypnat_le, ultra)
   351 done
   352 
   353 
   354 subsection{*The Hypernaturals Form an Ordered @{text comm_semiring_1_cancel} *}
   355 
   356 instance hypnat :: ordered_semidom
   357 proof
   358   fix x y z :: hypnat
   359   show "0 < (1::hypnat)"
   360     by (simp add: hypnat_zero_def hypnat_one_def linorder_not_le [symmetric],
   361         simp add: hypnat_le)
   362   show "x \<le> y ==> z + x \<le> z + y"
   363     by (rule hypnat_add_left_mono)
   364   show "x < y ==> 0 < z ==> z * x < z * y"
   365     by (simp add: hypnat_mult_less_mono2)
   366 qed
   367 
   368 lemma hypnat_le_zero_cancel [iff]: "(n \<le> (0::hypnat)) = (n = 0)"
   369 apply (cases n)
   370 apply (simp add: hypnat_zero_def hypnat_le)
   371 done
   372 
   373 lemma hypnat_mult_is_0 [simp]: "(m*n = (0::hypnat)) = (m=0 | n=0)"
   374 apply (cases m, cases n)
   375 apply (auto simp add: hypnat_zero_def hypnat_mult, ultra+)
   376 done
   377 
   378 lemma hypnat_diff_is_0_eq [simp]: "((m::hypnat) - n = 0) = (m \<le> n)"
   379 apply (cases m, cases n)
   380 apply (simp add: hypnat_le hypnat_minus hypnat_zero_def)
   381 done
   382 
   383 
   384 
   385 subsection{*Theorems for Ordering*}
   386 
   387 lemma hypnat_less:
   388       "(Abs_hypnat(hypnatrel``{%n. X n}) < Abs_hypnat(hypnatrel``{%n. Y n})) =
   389        ({n. X n < Y n} \<in> FreeUltrafilterNat)"
   390 apply (auto simp add: hypnat_le  linorder_not_le [symmetric])
   391 apply (ultra+)
   392 done
   393 
   394 lemma hypnat_not_less0 [iff]: "~ n < (0::hypnat)"
   395 apply (cases n)
   396 apply (auto simp add: hypnat_zero_def hypnat_less)
   397 done
   398 
   399 lemma hypnat_less_one [iff]:
   400       "(n < (1::hypnat)) = (n=0)"
   401 apply (cases n)
   402 apply (auto simp add: hypnat_zero_def hypnat_one_def hypnat_less)
   403 done
   404 
   405 lemma hypnat_add_diff_inverse: "~ m<n ==> n+(m-n) = (m::hypnat)"
   406 apply (cases m, cases n)
   407 apply (simp add: hypnat_minus hypnat_add hypnat_less split: nat_diff_split, ultra)
   408 done
   409 
   410 lemma hypnat_le_add_diff_inverse [simp]: "n \<le> m ==> n+(m-n) = (m::hypnat)"
   411 by (simp add: hypnat_add_diff_inverse linorder_not_less [symmetric])
   412 
   413 lemma hypnat_le_add_diff_inverse2 [simp]: "n\<le>m ==> (m-n)+n = (m::hypnat)"
   414 by (simp add: hypnat_le_add_diff_inverse hypnat_add_commute)
   415 
   416 declare hypnat_le_add_diff_inverse2 [OF order_less_imp_le]
   417 
   418 lemma hypnat_le0 [iff]: "(0::hypnat) \<le> n"
   419 by (simp add: linorder_not_less [symmetric])
   420 
   421 lemma hypnat_add_self_le [simp]: "(x::hypnat) \<le> n + x"
   422 by (insert add_right_mono [of 0 n x], simp)
   423 
   424 lemma hypnat_add_one_self_less [simp]: "(x::hypnat) < x + (1::hypnat)"
   425 by (insert add_strict_left_mono [OF zero_less_one], auto)
   426 
   427 lemma hypnat_neq0_conv [iff]: "(n \<noteq> 0) = (0 < (n::hypnat))"
   428 by (simp add: order_less_le)
   429 
   430 lemma hypnat_gt_zero_iff: "((0::hypnat) < n) = ((1::hypnat) \<le> n)"
   431 by (auto simp add: linorder_not_less [symmetric])
   432 
   433 lemma hypnat_gt_zero_iff2: "(0 < n) = (\<exists>m. n = m + (1::hypnat))"
   434 apply safe
   435  apply (rule_tac x = "n - (1::hypnat) " in exI)
   436  apply (simp add: hypnat_gt_zero_iff) 
   437 apply (insert add_le_less_mono [OF _ zero_less_one, of 0], auto) 
   438 done
   439 
   440 lemma hypnat_add_self_not_less: "~ (x + y < (x::hypnat))"
   441 by (simp add: linorder_not_le [symmetric] add_commute [of x]) 
   442 
   443 lemma hypnat_diff_split:
   444     "P(a - b::hypnat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
   445     -- {* elimination of @{text -} on @{text hypnat} *}
   446 proof (cases "a<b" rule: case_split)
   447   case True
   448     thus ?thesis
   449       by (auto simp add: hypnat_add_self_not_less order_less_imp_le 
   450                          hypnat_diff_is_0_eq [THEN iffD2])
   451 next
   452   case False
   453     thus ?thesis
   454       by (auto simp add: linorder_not_less dest: order_le_less_trans) 
   455 qed
   456 
   457 
   458 subsection{*The Embedding @{term hypnat_of_nat} Preserves @{text
   459 comm_ring_1} and Order Properties*}
   460 
   461 constdefs
   462 
   463   hypnat_of_nat   :: "nat => hypnat"
   464   "hypnat_of_nat m  == of_nat m"
   465 
   466   (* the set of infinite hypernatural numbers *)
   467   HNatInfinite :: "hypnat set"
   468   "HNatInfinite == {n. n \<notin> Nats}"
   469 
   470 
   471 lemma hypnat_of_nat_add:
   472       "hypnat_of_nat ((z::nat) + w) = hypnat_of_nat z + hypnat_of_nat w"
   473 by (simp add: hypnat_of_nat_def)
   474 
   475 lemma hypnat_of_nat_mult:
   476       "hypnat_of_nat (z * w) = hypnat_of_nat z * hypnat_of_nat w"
   477 by (simp add: hypnat_of_nat_def)
   478 
   479 lemma hypnat_of_nat_less_iff [simp]:
   480       "(hypnat_of_nat z < hypnat_of_nat w) = (z < w)"
   481 by (simp add: hypnat_of_nat_def)
   482 
   483 lemma hypnat_of_nat_le_iff [simp]:
   484       "(hypnat_of_nat z \<le> hypnat_of_nat w) = (z \<le> w)"
   485 by (simp add: hypnat_of_nat_def)
   486 
   487 lemma hypnat_of_nat_eq_iff [simp]:
   488       "(hypnat_of_nat z = hypnat_of_nat w) = (z = w)"
   489 by (simp add: hypnat_of_nat_def)
   490 
   491 lemma hypnat_of_nat_one [simp]: "hypnat_of_nat (Suc 0) = (1::hypnat)"
   492 by (simp add: hypnat_of_nat_def)
   493 
   494 lemma hypnat_of_nat_zero [simp]: "hypnat_of_nat 0 = 0"
   495 by (simp add: hypnat_of_nat_def)
   496 
   497 lemma hypnat_of_nat_zero_iff [simp]: "(hypnat_of_nat n = 0) = (n = 0)"
   498 by (simp add: hypnat_of_nat_def)
   499 
   500 lemma hypnat_of_nat_Suc [simp]:
   501      "hypnat_of_nat (Suc n) = hypnat_of_nat n + (1::hypnat)"
   502 by (simp add: hypnat_of_nat_def)
   503 
   504 lemma hypnat_of_nat_minus:
   505       "hypnat_of_nat ((j::nat) - k) = hypnat_of_nat j - hypnat_of_nat k"
   506 by (simp add: hypnat_of_nat_def split: nat_diff_split hypnat_diff_split)
   507 
   508 
   509 subsection{*Existence of an infinite hypernatural number*}
   510 
   511 lemma hypnat_omega: "hypnatrel``{%n::nat. n} \<in> hypnat"
   512 by auto
   513 
   514 lemma Rep_hypnat_omega: "Rep_hypnat(whn) \<in> hypnat"
   515 by (simp add: hypnat_omega_def)
   516 
   517 text{*Existence of infinite number not corresponding to any natural number
   518 follows because member @{term FreeUltrafilterNat} is not finite.
   519 See @{text HyperDef.thy} for similar argument.*}
   520 
   521 
   522 subsection{*Properties of the set of embedded natural numbers*}
   523 
   524 lemma of_nat_eq_add [rule_format]:
   525      "\<forall>d::hypnat. of_nat m = of_nat n + d --> d \<in> range of_nat"
   526 apply (induct n) 
   527 apply (auto simp add: add_assoc) 
   528 apply (case_tac x) 
   529 apply (auto simp add: add_commute [of 1]) 
   530 done
   531 
   532 lemma Nats_diff [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> (a-b :: hypnat) \<in> Nats"
   533 by (auto simp add: of_nat_eq_add Nats_def split: hypnat_diff_split)
   534 
   535 lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
   536 apply (insert finite_atMost [of m]) 
   537 apply (simp add: atMost_def) 
   538 apply (drule FreeUltrafilterNat_finite) 
   539 apply (drule FreeUltrafilterNat_Compl_mem, ultra)
   540 done
   541 
   542 lemma Compl_Collect_le: "- {n::nat. N \<le> n} = {n. n < N}"
   543 by (simp add: Collect_neg_eq [symmetric] linorder_not_le) 
   544 
   545 
   546 lemma hypnat_of_nat_eq:
   547      "hypnat_of_nat m  = Abs_hypnat(hypnatrel``{%n::nat. m})"
   548 apply (induct m) 
   549 apply (simp_all add: hypnat_zero_def hypnat_one_def hypnat_add) 
   550 done
   551 
   552 lemma SHNat_eq: "Nats = {n. \<exists>N. n = hypnat_of_nat N}"
   553 by (force simp add: hypnat_of_nat_def Nats_def) 
   554 
   555 lemma hypnat_omega_gt_SHNat:
   556      "n \<in> Nats ==> n < whn"
   557 apply (auto simp add: hypnat_of_nat_eq hypnat_less_def hypnat_le_def
   558                       hypnat_omega_def SHNat_eq)
   559  prefer 2 apply (force dest: FreeUltrafilterNat_not_finite)
   560 apply (auto intro!: exI)
   561 apply (rule cofinite_mem_FreeUltrafilterNat)
   562 apply (simp add: Compl_Collect_le finite_nat_segment) 
   563 done
   564 
   565 (* Infinite hypernatural not in embedded Nats *)
   566 lemma SHNAT_omega_not_mem [simp]: "whn \<notin> Nats"
   567 by (blast dest: hypnat_omega_gt_SHNat)
   568 
   569 lemma hypnat_of_nat_less_whn [simp]: "hypnat_of_nat n < whn"
   570 apply (insert hypnat_omega_gt_SHNat [of "hypnat_of_nat n"])
   571 apply (simp add: hypnat_of_nat_def) 
   572 done
   573 
   574 lemma hypnat_of_nat_le_whn [simp]: "hypnat_of_nat n \<le> whn"
   575 by (rule hypnat_of_nat_less_whn [THEN order_less_imp_le])
   576 
   577 lemma hypnat_zero_less_hypnat_omega [simp]: "0 < whn"
   578 by (simp add: hypnat_omega_gt_SHNat)
   579 
   580 lemma hypnat_one_less_hypnat_omega [simp]: "(1::hypnat) < whn"
   581 by (simp add: hypnat_omega_gt_SHNat)
   582 
   583 
   584 subsection{*Infinite Hypernatural Numbers -- @{term HNatInfinite}*}
   585 
   586 lemma HNatInfinite_whn [simp]: "whn \<in> HNatInfinite"
   587 by (simp add: HNatInfinite_def)
   588 
   589 lemma Nats_not_HNatInfinite_iff: "(x \<in> Nats) = (x \<notin> HNatInfinite)"
   590 by (simp add: HNatInfinite_def)
   591 
   592 lemma HNatInfinite_not_Nats_iff: "(x \<in> HNatInfinite) = (x \<notin> Nats)"
   593 by (simp add: HNatInfinite_def)
   594 
   595 
   596 subsection{*Alternative characterization of the set of infinite hypernaturals*}
   597 
   598 text{* @{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}*}
   599 
   600 (*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
   601 lemma HNatInfinite_FreeUltrafilterNat_lemma:
   602      "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat
   603       ==> {n. N < f n} \<in> FreeUltrafilterNat"
   604 apply (induct_tac "N")
   605 apply (drule_tac x = 0 in spec)
   606 apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem, drule FreeUltrafilterNat_Int, assumption, simp)
   607 apply (drule_tac x = "Suc n" in spec, ultra)
   608 done
   609 
   610 lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"
   611 apply (auto simp add: HNatInfinite_def SHNat_eq hypnat_of_nat_eq)
   612 apply (rule_tac z = x in eq_Abs_hypnat)
   613 apply (auto elim: HNatInfinite_FreeUltrafilterNat_lemma 
   614             simp add: hypnat_less FreeUltrafilterNat_Compl_iff1 
   615                       Collect_neg_eq [symmetric])
   616 done
   617 
   618 
   619 subsection{*Alternative Characterization of @{term HNatInfinite} using 
   620 Free Ultrafilter*}
   621 
   622 lemma HNatInfinite_FreeUltrafilterNat:
   623      "x \<in> HNatInfinite 
   624       ==> \<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat"
   625 apply (cases x)
   626 apply (auto simp add: HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
   627 apply (rule bexI [OF _ lemma_hypnatrel_refl], clarify) 
   628 apply (auto simp add: hypnat_of_nat_def hypnat_less)
   629 done
   630 
   631 lemma FreeUltrafilterNat_HNatInfinite:
   632      "\<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat
   633       ==> x \<in> HNatInfinite"
   634 apply (cases x)
   635 apply (auto simp add: hypnat_less HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
   636 apply (drule spec, ultra, auto) 
   637 done
   638 
   639 lemma HNatInfinite_FreeUltrafilterNat_iff:
   640      "(x \<in> HNatInfinite) = 
   641       (\<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat)"
   642 by (blast intro: HNatInfinite_FreeUltrafilterNat 
   643                  FreeUltrafilterNat_HNatInfinite)
   644 
   645 lemma HNatInfinite_gt_one [simp]: "x \<in> HNatInfinite ==> (1::hypnat) < x"
   646 by (auto simp add: HNatInfinite_iff)
   647 
   648 lemma zero_not_mem_HNatInfinite [simp]: "0 \<notin> HNatInfinite"
   649 apply (auto simp add: HNatInfinite_iff)
   650 apply (drule_tac a = " (1::hypnat) " in equals0D)
   651 apply simp
   652 done
   653 
   654 lemma HNatInfinite_not_eq_zero: "x \<in> HNatInfinite ==> 0 < x"
   655 apply (drule HNatInfinite_gt_one) 
   656 apply (auto simp add: order_less_trans [OF zero_less_one])
   657 done
   658 
   659 lemma HNatInfinite_ge_one [simp]: "x \<in> HNatInfinite ==> (1::hypnat) \<le> x"
   660 by (blast intro: order_less_imp_le HNatInfinite_gt_one)
   661 
   662 
   663 subsection{*Closure Rules*}
   664 
   665 lemma HNatInfinite_add:
   666      "[| x \<in> HNatInfinite; y \<in> HNatInfinite |] ==> x + y \<in> HNatInfinite"
   667 apply (auto simp add: HNatInfinite_iff)
   668 apply (drule bspec, assumption)
   669 apply (drule bspec [OF _ Nats_0])
   670 apply (drule add_strict_mono, assumption, simp)
   671 done
   672 
   673 lemma HNatInfinite_SHNat_add:
   674      "[| x \<in> HNatInfinite; y \<in> Nats |] ==> x + y \<in> HNatInfinite"
   675 apply (auto simp add: HNatInfinite_not_Nats_iff) 
   676 apply (drule_tac a = "x + y" in Nats_diff, auto) 
   677 done
   678 
   679 lemma HNatInfinite_Nats_imp_less: "[| x \<in> HNatInfinite; y \<in> Nats |] ==> y < x"
   680 by (simp add: HNatInfinite_iff) 
   681 
   682 lemma HNatInfinite_SHNat_diff:
   683   assumes x: "x \<in> HNatInfinite" and y: "y \<in> Nats" 
   684   shows "x - y \<in> HNatInfinite"
   685 proof -
   686   have "y < x" by (simp add: HNatInfinite_Nats_imp_less prems)
   687   hence "x - y + y = x" by (simp add: order_less_imp_le)
   688   with x show ?thesis
   689     by (force simp add: HNatInfinite_not_Nats_iff 
   690               dest: Nats_add [of "x-y", OF _ y]) 
   691 qed
   692 
   693 lemma HNatInfinite_add_one:
   694      "x \<in> HNatInfinite ==> x + (1::hypnat) \<in> HNatInfinite"
   695 by (auto intro: HNatInfinite_SHNat_add)
   696 
   697 lemma HNatInfinite_is_Suc: "x \<in> HNatInfinite ==> \<exists>y. x = y + (1::hypnat)"
   698 apply (rule_tac x = "x - (1::hypnat) " in exI)
   699 apply auto
   700 done
   701 
   702 
   703 subsection{*Embedding of the Hypernaturals into the Hyperreals*}
   704 text{*Obtained using the nonstandard extension of the naturals*}
   705 
   706 constdefs
   707   hypreal_of_hypnat :: "hypnat => hypreal"
   708    "hypreal_of_hypnat N  == 
   709       Abs_hypreal(\<Union>X \<in> Rep_hypnat(N). hyprel``{%n::nat. real (X n)})"
   710 
   711 
   712 lemma HNat_hypreal_of_nat [simp]: "hypreal_of_nat N \<in> Nats"
   713 by (simp add: hypreal_of_nat_def) 
   714 
   715 (*WARNING: FRAGILE!*)
   716 lemma lemma_hyprel_FUFN:
   717      "(Ya \<in> hyprel ``{%n. f(n)}) = ({n. f n = Ya n} \<in> FreeUltrafilterNat)"
   718 by force
   719 
   720 lemma hypreal_of_hypnat:
   721       "hypreal_of_hypnat (Abs_hypnat(hypnatrel``{%n. X n})) =
   722        Abs_hypreal(hyprel `` {%n. real (X n)})"
   723 apply (simp add: hypreal_of_hypnat_def)
   724 apply (rule_tac f = Abs_hypreal in arg_cong)
   725 apply (auto elim: FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset] 
   726        simp add: lemma_hyprel_FUFN)
   727 done
   728 
   729 lemma hypreal_of_hypnat_inject [simp]:
   730      "(hypreal_of_hypnat m = hypreal_of_hypnat n) = (m=n)"
   731 apply (cases m, cases n)
   732 apply (auto simp add: hypreal_of_hypnat)
   733 done
   734 
   735 lemma hypreal_of_hypnat_zero: "hypreal_of_hypnat 0 = 0"
   736 by (simp add: hypnat_zero_def hypreal_zero_def hypreal_of_hypnat)
   737 
   738 lemma hypreal_of_hypnat_one: "hypreal_of_hypnat (1::hypnat) = 1"
   739 by (simp add: hypnat_one_def hypreal_one_def hypreal_of_hypnat)
   740 
   741 lemma hypreal_of_hypnat_add [simp]:
   742      "hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n"
   743 apply (cases m, cases n)
   744 apply (simp add: hypreal_of_hypnat hypreal_add hypnat_add real_of_nat_add)
   745 done
   746 
   747 lemma hypreal_of_hypnat_mult [simp]:
   748      "hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n"
   749 apply (cases m, cases n)
   750 apply (simp add: hypreal_of_hypnat hypreal_mult hypnat_mult real_of_nat_mult)
   751 done
   752 
   753 lemma hypreal_of_hypnat_less_iff [simp]:
   754      "(hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)"
   755 apply (cases m, cases n)
   756 apply (simp add: hypreal_of_hypnat hypreal_less hypnat_less)
   757 done
   758 
   759 lemma hypreal_of_hypnat_eq_zero_iff: "(hypreal_of_hypnat N = 0) = (N = 0)"
   760 by (simp add: hypreal_of_hypnat_zero [symmetric])
   761 declare hypreal_of_hypnat_eq_zero_iff [simp]
   762 
   763 lemma hypreal_of_hypnat_ge_zero [simp]: "0 \<le> hypreal_of_hypnat n"
   764 apply (cases n)
   765 apply (simp add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
   766 done
   767 
   768 lemma HNatInfinite_inverse_Infinitesimal [simp]:
   769      "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
   770 apply (cases n)
   771 apply (auto simp add: hypreal_of_hypnat hypreal_inverse 
   772       HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
   773 apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
   774 apply (drule_tac x = "m + 1" in spec, ultra)
   775 done
   776 
   777 lemma HNatInfinite_hypreal_of_hypnat_gt_zero:
   778      "N \<in> HNatInfinite ==> 0 < hypreal_of_hypnat N"
   779 apply (rule ccontr)
   780 apply (simp add: hypreal_of_hypnat_zero [symmetric] linorder_not_less)
   781 done
   782 
   783 
   784 ML
   785 {*
   786 val hypnat_of_nat_def = thm"hypnat_of_nat_def";
   787 val HNatInfinite_def = thm"HNatInfinite_def";
   788 val hypreal_of_hypnat_def = thm"hypreal_of_hypnat_def";
   789 val hypnat_zero_def = thm"hypnat_zero_def";
   790 val hypnat_one_def = thm"hypnat_one_def";
   791 val hypnat_omega_def = thm"hypnat_omega_def";
   792 
   793 val hypnatrel_iff = thm "hypnatrel_iff";
   794 val hypnatrel_in_hypnat = thm "hypnatrel_in_hypnat";
   795 val inj_on_Abs_hypnat = thm "inj_on_Abs_hypnat";
   796 val inj_Rep_hypnat = thm "inj_Rep_hypnat";
   797 val lemma_hypnatrel_refl = thm "lemma_hypnatrel_refl";
   798 val hypnat_empty_not_mem = thm "hypnat_empty_not_mem";
   799 val Rep_hypnat_nonempty = thm "Rep_hypnat_nonempty";
   800 val eq_Abs_hypnat = thm "eq_Abs_hypnat";
   801 val hypnat_add = thm "hypnat_add";
   802 val hypnat_add_commute = thm "hypnat_add_commute";
   803 val hypnat_add_assoc = thm "hypnat_add_assoc";
   804 val hypnat_add_zero_left = thm "hypnat_add_zero_left";
   805 val hypnat_minus_congruent2 = thm "hypnat_minus_congruent2";
   806 val hypnat_minus = thm "hypnat_minus";
   807 val hypnat_minus_zero = thm "hypnat_minus_zero";
   808 val hypnat_diff_0_eq_0 = thm "hypnat_diff_0_eq_0";
   809 val hypnat_add_is_0 = thm "hypnat_add_is_0";
   810 val hypnat_diff_diff_left = thm "hypnat_diff_diff_left";
   811 val hypnat_diff_commute = thm "hypnat_diff_commute";
   812 val hypnat_diff_add_inverse = thm "hypnat_diff_add_inverse";
   813 val hypnat_diff_add_inverse2 = thm "hypnat_diff_add_inverse2";
   814 val hypnat_diff_cancel = thm "hypnat_diff_cancel";
   815 val hypnat_diff_cancel2 = thm "hypnat_diff_cancel2";
   816 val hypnat_diff_add_0 = thm "hypnat_diff_add_0";
   817 val hypnat_mult_congruent2 = thm "hypnat_mult_congruent2";
   818 val hypnat_mult = thm "hypnat_mult";
   819 val hypnat_mult_commute = thm "hypnat_mult_commute";
   820 val hypnat_mult_assoc = thm "hypnat_mult_assoc";
   821 val hypnat_mult_1 = thm "hypnat_mult_1";
   822 val hypnat_diff_mult_distrib = thm "hypnat_diff_mult_distrib";
   823 val hypnat_diff_mult_distrib2 = thm "hypnat_diff_mult_distrib2";
   824 val hypnat_add_mult_distrib = thm "hypnat_add_mult_distrib";
   825 val hypnat_add_mult_distrib2 = thm "hypnat_add_mult_distrib2";
   826 val hypnat_zero_not_eq_one = thm "hypnat_zero_not_eq_one";
   827 val hypnat_le = thm "hypnat_le";
   828 val hypnat_le_refl = thm "hypnat_le_refl";
   829 val hypnat_le_trans = thm "hypnat_le_trans";
   830 val hypnat_le_anti_sym = thm "hypnat_le_anti_sym";
   831 val hypnat_less_le = thm "hypnat_less_le";
   832 val hypnat_le_linear = thm "hypnat_le_linear";
   833 val hypnat_add_left_mono = thm "hypnat_add_left_mono";
   834 val hypnat_mult_less_mono2 = thm "hypnat_mult_less_mono2";
   835 val hypnat_mult_is_0 = thm "hypnat_mult_is_0";
   836 val hypnat_less = thm "hypnat_less";
   837 val hypnat_not_less0 = thm "hypnat_not_less0";
   838 val hypnat_less_one = thm "hypnat_less_one";
   839 val hypnat_add_diff_inverse = thm "hypnat_add_diff_inverse";
   840 val hypnat_le_add_diff_inverse = thm "hypnat_le_add_diff_inverse";
   841 val hypnat_le_add_diff_inverse2 = thm "hypnat_le_add_diff_inverse2";
   842 val hypnat_le0 = thm "hypnat_le0";
   843 val hypnat_add_self_le = thm "hypnat_add_self_le";
   844 val hypnat_add_one_self_less = thm "hypnat_add_one_self_less";
   845 val hypnat_neq0_conv = thm "hypnat_neq0_conv";
   846 val hypnat_gt_zero_iff = thm "hypnat_gt_zero_iff";
   847 val hypnat_gt_zero_iff2 = thm "hypnat_gt_zero_iff2";
   848 val hypnat_of_nat_add = thm "hypnat_of_nat_add";
   849 val hypnat_of_nat_minus = thm "hypnat_of_nat_minus";
   850 val hypnat_of_nat_mult = thm "hypnat_of_nat_mult";
   851 val hypnat_of_nat_less_iff = thm "hypnat_of_nat_less_iff";
   852 val hypnat_of_nat_le_iff = thm "hypnat_of_nat_le_iff";
   853 val hypnat_of_nat_eq = thm"hypnat_of_nat_eq"
   854 val SHNat_eq = thm"SHNat_eq"
   855 val hypnat_of_nat_one = thm "hypnat_of_nat_one";
   856 val hypnat_of_nat_zero = thm "hypnat_of_nat_zero";
   857 val hypnat_of_nat_zero_iff = thm "hypnat_of_nat_zero_iff";
   858 val hypnat_of_nat_Suc = thm "hypnat_of_nat_Suc";
   859 val hypnat_omega = thm "hypnat_omega";
   860 val Rep_hypnat_omega = thm "Rep_hypnat_omega";
   861 val SHNAT_omega_not_mem = thm "SHNAT_omega_not_mem";
   862 val cofinite_mem_FreeUltrafilterNat = thm "cofinite_mem_FreeUltrafilterNat";
   863 val hypnat_omega_gt_SHNat = thm "hypnat_omega_gt_SHNat";
   864 val hypnat_of_nat_less_whn = thm "hypnat_of_nat_less_whn";
   865 val hypnat_of_nat_le_whn = thm "hypnat_of_nat_le_whn";
   866 val hypnat_zero_less_hypnat_omega = thm "hypnat_zero_less_hypnat_omega";
   867 val hypnat_one_less_hypnat_omega = thm "hypnat_one_less_hypnat_omega";
   868 val HNatInfinite_whn = thm "HNatInfinite_whn";
   869 val HNatInfinite_iff = thm "HNatInfinite_iff";
   870 val HNatInfinite_FreeUltrafilterNat = thm "HNatInfinite_FreeUltrafilterNat";
   871 val FreeUltrafilterNat_HNatInfinite = thm "FreeUltrafilterNat_HNatInfinite";
   872 val HNatInfinite_FreeUltrafilterNat_iff = thm "HNatInfinite_FreeUltrafilterNat_iff";
   873 val HNatInfinite_gt_one = thm "HNatInfinite_gt_one";
   874 val zero_not_mem_HNatInfinite = thm "zero_not_mem_HNatInfinite";
   875 val HNatInfinite_not_eq_zero = thm "HNatInfinite_not_eq_zero";
   876 val HNatInfinite_ge_one = thm "HNatInfinite_ge_one";
   877 val HNatInfinite_add = thm "HNatInfinite_add";
   878 val HNatInfinite_SHNat_add = thm "HNatInfinite_SHNat_add";
   879 val HNatInfinite_SHNat_diff = thm "HNatInfinite_SHNat_diff";
   880 val HNatInfinite_add_one = thm "HNatInfinite_add_one";
   881 val HNatInfinite_is_Suc = thm "HNatInfinite_is_Suc";
   882 val HNat_hypreal_of_nat = thm "HNat_hypreal_of_nat";
   883 val hypreal_of_hypnat = thm "hypreal_of_hypnat";
   884 val hypreal_of_hypnat_zero = thm "hypreal_of_hypnat_zero";
   885 val hypreal_of_hypnat_one = thm "hypreal_of_hypnat_one";
   886 val hypreal_of_hypnat_add = thm "hypreal_of_hypnat_add";
   887 val hypreal_of_hypnat_mult = thm "hypreal_of_hypnat_mult";
   888 val hypreal_of_hypnat_less_iff = thm "hypreal_of_hypnat_less_iff";
   889 val hypreal_of_hypnat_ge_zero = thm "hypreal_of_hypnat_ge_zero";
   890 val HNatInfinite_inverse_Infinitesimal = thm "HNatInfinite_inverse_Infinitesimal";
   891 *}
   892 
   893 end