src/HOL/Hyperreal/NatStar.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       : NatStar.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{*Star-transforms for the Hypernaturals*}
     9 
    10 theory NatStar
    11 imports "../Real/RealPow" HyperPow
    12 begin
    13 
    14 text{*Extends sets of nats, and functions from the nats to nats or reals*}
    15 
    16 
    17 constdefs
    18 
    19   (* internal sets and nonstandard extensions -- see Star.thy as well *)
    20 
    21     starsetNat :: "nat set => hypnat set"          ("*sNat* _" [80] 80)
    22     "*sNat* A ==
    23        {x. \<forall>X\<in>Rep_hypnat(x). {n::nat. X n \<in> A}: FreeUltrafilterNat}"
    24 
    25    starsetNat_n :: "(nat => nat set) => hypnat set"      ("*sNatn* _" [80] 80)
    26     "*sNatn* As ==
    27        {x. \<forall>X\<in>Rep_hypnat(x). {n::nat. X n \<in> (As n)}: FreeUltrafilterNat}"
    28 
    29    InternalNatSets :: "hypnat set set"
    30     "InternalNatSets == {X. \<exists>As. X = *sNatn* As}"
    31 
    32     (* star transform of functions f:Nat --> Real *)
    33 
    34     starfunNat :: "(nat => real) => hypnat => hypreal"
    35                   ("*fNat* _" [80] 80)
    36     "*fNat* f  == (%x. Abs_hypreal(\<Union>X\<in>Rep_hypnat(x). hyprel``{%n. f (X n)}))"
    37 
    38    starfunNat_n :: "(nat => (nat => real)) => hypnat => hypreal"
    39                    ("*fNatn* _" [80] 80)
    40     "*fNatn* F ==
    41       (%x. Abs_hypreal(\<Union>X\<in>Rep_hypnat(x). hyprel``{%n. (F n)(X n)}))"
    42 
    43    InternalNatFuns :: "(hypnat => hypreal) set"
    44     "InternalNatFuns == {X. \<exists>F. X = *fNatn* F}"
    45 
    46     (* star transform of functions f:Nat --> Nat *)
    47 
    48    starfunNat2 :: "(nat => nat) => hypnat => hypnat"
    49                    ("*fNat2* _" [80] 80)
    50     "*fNat2* f == %x. Abs_hypnat(\<Union>X\<in>Rep_hypnat(x). hypnatrel``{%n. f (X n)})"
    51 
    52    starfunNat2_n :: "(nat => (nat => nat)) => hypnat => hypnat"
    53                      ("*fNat2n* _" [80] 80)
    54     "*fNat2n* F == 
    55         %x. Abs_hypnat(\<Union>X\<in>Rep_hypnat(x). hypnatrel``{%n. (F n)(X n)})"
    56 
    57    InternalNatFuns2 :: "(hypnat => hypnat) set"
    58     "InternalNatFuns2 == {X. \<exists>F. X = *fNat2n* F}"
    59 
    60 
    61 lemma NatStar_real_set: "*sNat*(UNIV::nat set) = (UNIV::hypnat set)"
    62 by (simp add: starsetNat_def)
    63 
    64 lemma NatStar_empty_set [simp]: "*sNat* {} = {}"
    65 by (simp add: starsetNat_def)
    66 
    67 lemma NatStar_Un: "*sNat* (A Un B) = *sNat* A Un *sNat* B"
    68 apply (auto simp add: starsetNat_def)
    69  prefer 2 apply (blast intro: FreeUltrafilterNat_subset)
    70  prefer 2 apply (blast intro: FreeUltrafilterNat_subset)
    71 apply (drule FreeUltrafilterNat_Compl_mem)
    72 apply (drule bspec, assumption)
    73 apply (rule_tac z = x in eq_Abs_hypnat, auto, ultra)
    74 done
    75 
    76 lemma starsetNat_n_Un: "*sNatn* (%n. (A n) Un (B n)) = *sNatn* A Un *sNatn* B"
    77 apply (auto simp add: starsetNat_n_def)
    78 apply (drule_tac x = Xa in bspec)
    79 apply (rule_tac [2] z = x in eq_Abs_hypnat)
    80 apply (auto dest!: bspec, ultra+)
    81 done
    82 
    83 lemma InternalNatSets_Un:
    84      "[| X \<in> InternalNatSets; Y \<in> InternalNatSets |]
    85       ==> (X Un Y) \<in> InternalNatSets"
    86 by (auto simp add: InternalNatSets_def starsetNat_n_Un [symmetric])
    87 
    88 lemma NatStar_Int: "*sNat* (A Int B) = *sNat* A Int *sNat* B"
    89 apply (auto simp add: starsetNat_def)
    90 prefer 3 apply (blast intro: FreeUltrafilterNat_Int FreeUltrafilterNat_subset)
    91 apply (blast intro: FreeUltrafilterNat_subset)+
    92 done
    93 
    94 lemma starsetNat_n_Int:
    95       "*sNatn* (%n. (A n) Int (B n)) = *sNatn* A Int *sNatn* B"
    96 apply (auto simp add: starsetNat_n_def)
    97 apply (auto dest!: bspec, ultra+)
    98 done
    99 
   100 lemma InternalNatSets_Int:
   101      "[| X \<in> InternalNatSets; Y \<in> InternalNatSets |]
   102       ==> (X Int Y) \<in> InternalNatSets"
   103 by (auto simp add: InternalNatSets_def starsetNat_n_Int [symmetric])
   104 
   105 lemma NatStar_Compl: "*sNat* (-A) = -( *sNat* A)"
   106 apply (auto simp add: starsetNat_def)
   107 apply (rule_tac z = x in eq_Abs_hypnat)
   108 apply (rule_tac [2] z = x in eq_Abs_hypnat)
   109 apply (auto dest!: bspec, ultra+)
   110 done
   111 
   112 lemma starsetNat_n_Compl: "*sNatn* ((%n. - A n)) = -( *sNatn* A)"
   113 apply (auto simp add: starsetNat_n_def)
   114 apply (rule_tac z = x in eq_Abs_hypnat)
   115 apply (rule_tac [2] z = x in eq_Abs_hypnat)
   116 apply (auto dest!: bspec, ultra+)
   117 done
   118 
   119 lemma InternalNatSets_Compl: "X \<in> InternalNatSets ==> -X \<in> InternalNatSets"
   120 by (auto simp add: InternalNatSets_def starsetNat_n_Compl [symmetric])
   121 
   122 lemma starsetNat_n_diff: "*sNatn* (%n. (A n) - (B n)) = *sNatn* A - *sNatn* B"
   123 apply (auto simp add: starsetNat_n_def)
   124 apply (rule_tac [2] z = x in eq_Abs_hypnat)
   125 apply (rule_tac [3] z = x in eq_Abs_hypnat)
   126 apply (auto dest!: bspec, ultra+)
   127 done
   128 
   129 lemma InternalNatSets_diff:
   130      "[| X \<in> InternalNatSets; Y \<in> InternalNatSets |]
   131       ==> (X - Y) \<in> InternalNatSets"
   132 by (auto simp add: InternalNatSets_def starsetNat_n_diff [symmetric])
   133 
   134 lemma NatStar_subset: "A \<le> B ==> *sNat* A \<le> *sNat* B"
   135 apply (simp add: starsetNat_def)
   136 apply (blast intro: FreeUltrafilterNat_subset)
   137 done
   138 
   139 lemma NatStar_mem: "a \<in> A ==> hypnat_of_nat a \<in> *sNat* A"
   140 by (auto intro: FreeUltrafilterNat_subset 
   141          simp add: starsetNat_def hypnat_of_nat_eq)
   142 
   143 lemma NatStar_hypreal_of_real_image_subset: "hypnat_of_nat ` A \<le> *sNat* A"
   144 apply (auto simp add: starsetNat_def hypnat_of_nat_eq)
   145 apply (blast intro: FreeUltrafilterNat_subset)
   146 done
   147 
   148 lemma NatStar_SHNat_subset: "Nats \<le> *sNat* (UNIV:: nat set)"
   149 by (simp add: starsetNat_def SHNat_eq hypnat_of_nat_eq)
   150 
   151 lemma NatStar_hypreal_of_real_Int:
   152      "*sNat* X Int Nats = hypnat_of_nat ` X"
   153 apply (auto simp add: starsetNat_def hypnat_of_nat_eq SHNat_eq)
   154 apply (simp add: hypnat_of_nat_eq [symmetric])
   155 apply (rule imageI, rule ccontr)
   156 apply (drule bspec)
   157 apply (rule lemma_hypnatrel_refl)
   158 prefer 2 apply (blast intro: FreeUltrafilterNat_subset, auto)
   159 done
   160 
   161 lemma starsetNat_starsetNat_n_eq: "*sNat* X = *sNatn* (%n. X)"
   162 by (simp add: starsetNat_n_def starsetNat_def)
   163 
   164 lemma InternalNatSets_starsetNat_n [simp]: "( *sNat* X) \<in> InternalNatSets"
   165 by (auto simp add: InternalNatSets_def starsetNat_starsetNat_n_eq)
   166 
   167 lemma InternalNatSets_UNIV_diff:
   168      "X \<in> InternalNatSets ==> UNIV - X \<in> InternalNatSets"
   169 by (auto intro: InternalNatSets_Compl)
   170 
   171 text{*Nonstandard extension of a set (defined using a constant
   172    sequence) as a special case of an internal set*}
   173 lemma starsetNat_n_starsetNat: "\<forall>n. (As n = A) ==> *sNatn* As = *sNat* A"
   174 by (simp add: starsetNat_n_def starsetNat_def)
   175 
   176 
   177 subsection{*Nonstandard Extensions of Functions*}
   178 
   179 text{* Nonstandard extension of a function (defined using a constant
   180    sequence) as a special case of an internal function*}
   181 
   182 lemma starfunNat_n_starfunNat: "\<forall>n. (F n = f) ==> *fNatn* F = *fNat* f"
   183 by (simp add: starfunNat_n_def starfunNat_def)
   184 
   185 lemma starfunNat2_n_starfunNat2: "\<forall>n. (F n = f) ==> *fNat2n* F = *fNat2* f"
   186 by (simp add: starfunNat2_n_def starfunNat2_def)
   187 
   188 lemma starfunNat_congruent:
   189       "congruent hypnatrel (%X. hypnatrel``{%n. f (X n)})"
   190 apply (simp add: congruent_def, safe)
   191 apply (ultra+)
   192 done
   193 
   194 (* f::nat=>real *)
   195 lemma starfunNat:
   196       "( *fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
   197        Abs_hypreal(hyprel `` {%n. f (X n)})"
   198 apply (simp add: starfunNat_def)
   199 apply (rule arg_cong [where f = Abs_hypreal])
   200 apply (auto, ultra)
   201 done
   202 
   203 (* f::nat=>nat *)
   204 lemma starfunNat2:
   205       "( *fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
   206        Abs_hypnat(hypnatrel `` {%n. f (X n)})"
   207 apply (simp add: starfunNat2_def)
   208 apply (rule arg_cong [where f = Abs_hypnat])
   209 apply (simp add: hypnatrel_in_hypnat [THEN Abs_hypnat_inverse]
   210          UN_equiv_class [OF equiv_hypnatrel starfunNat_congruent])
   211 done
   212 
   213 subsubsection{*Multiplication: @{text "( *f) x ( *g) = *(f x g)"}*}
   214 
   215 lemma starfunNat_mult:
   216      "( *fNat* f) z * ( *fNat* g) z = ( *fNat* (%x. f x * g x)) z"
   217 apply (cases z)
   218 apply (simp add: starfunNat hypreal_mult)
   219 done
   220 
   221 lemma starfunNat2_mult:
   222      "( *fNat2* f) z * ( *fNat2* g) z = ( *fNat2* (%x. f x * g x)) z"
   223 apply (cases z)
   224 apply (simp add: starfunNat2 hypnat_mult)
   225 done
   226 
   227 subsubsection{*Addition: @{text "( *f) + ( *g) = *(f + g)"}*}
   228 
   229 lemma starfunNat_add:
   230      "( *fNat* f) z + ( *fNat* g) z = ( *fNat* (%x. f x + g x)) z"
   231 apply (cases z)
   232 apply (simp add: starfunNat hypreal_add)
   233 done
   234 
   235 lemma starfunNat2_add:
   236      "( *fNat2* f) z + ( *fNat2* g) z = ( *fNat2* (%x. f x + g x)) z"
   237 apply (cases z)
   238 apply (simp add: starfunNat2 hypnat_add)
   239 done
   240 
   241 lemma starfunNat2_minus:
   242      "( *fNat2* f) z - ( *fNat2* g) z = ( *fNat2* (%x. f x - g x)) z"
   243 apply (cases z)
   244 apply (simp add: starfunNat2 hypnat_minus)
   245 done
   246 
   247 subsubsection{*Composition: @{text "( *f) o ( *g) = *(f o g)"}*}
   248 
   249 (***** ( *f::nat=>real) o ( *g::nat=>nat) = *(f o g) *****)
   250 
   251 lemma starfunNatNat2_o:
   252      "( *fNat* f) o ( *fNat2* g) = ( *fNat* (f o g))"
   253 apply (rule ext)
   254 apply (rule_tac z = x in eq_Abs_hypnat)
   255 apply (simp add: starfunNat2 starfunNat)
   256 done
   257 
   258 lemma starfunNatNat2_o2:
   259      "(%x. ( *fNat* f) (( *fNat2* g) x)) = ( *fNat* (%x. f(g x)))"
   260 apply (insert starfunNatNat2_o [of f g]) 
   261 apply (simp add: o_def) 
   262 done
   263 
   264 (***** ( *f::nat=>nat) o ( *g::nat=>nat) = *(f o g) *****)
   265 lemma starfunNat2_o: "( *fNat2* f) o ( *fNat2* g) = ( *fNat2* (f o g))"
   266 apply (rule ext)
   267 apply (rule_tac z = x in eq_Abs_hypnat)
   268 apply (simp add: starfunNat2)
   269 done
   270 
   271 (***** ( *f::real=>real) o ( *g::nat=>real) = *(f o g) *****)
   272 
   273 lemma starfun_stafunNat_o: "( *f* f) o ( *fNat* g) = ( *fNat* (f o g))"
   274 apply (rule ext)
   275 apply (rule_tac z = x in eq_Abs_hypnat)
   276 apply (simp add: starfunNat starfun)
   277 done
   278 
   279 lemma starfun_stafunNat_o2:
   280      "(%x. ( *f* f) (( *fNat* g) x)) = ( *fNat* (%x. f (g x)))"
   281 apply (insert starfun_stafunNat_o [of f g]) 
   282 apply (simp add: o_def) 
   283 done
   284 
   285 
   286 text{*NS extension of constant function*}
   287 
   288 lemma starfunNat_const_fun [simp]: "( *fNat* (%x. k)) z = hypreal_of_real k"
   289 apply (cases z)
   290 apply (simp add: starfunNat hypreal_of_real_def)
   291 done
   292 
   293 lemma starfunNat2_const_fun [simp]: "( *fNat2* (%x. k)) z = hypnat_of_nat  k"
   294 apply (cases z)
   295 apply (simp add: starfunNat2 hypnat_of_nat_eq)
   296 done
   297 
   298 lemma starfunNat_minus: "- ( *fNat* f) x = ( *fNat* (%x. - f x)) x"
   299 apply (cases x)
   300 apply (simp add: starfunNat hypreal_minus)
   301 done
   302 
   303 lemma starfunNat_inverse:
   304      "inverse (( *fNat* f) x) = ( *fNat* (%x. inverse (f x))) x"
   305 apply (cases x)
   306 apply (simp add: starfunNat hypreal_inverse)
   307 done
   308 
   309 text{* Extended function has same solution as its standard
   310    version for natural arguments. i.e they are the same
   311    for all natural arguments (c.f. Hoskins pg. 107- SEQ)*}
   312 
   313 lemma starfunNat_eq [simp]:
   314      "( *fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)"
   315 by (simp add: starfunNat hypnat_of_nat_eq hypreal_of_real_def)
   316 
   317 lemma starfunNat2_eq [simp]:
   318      "( *fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)"
   319 by (simp add: starfunNat2 hypnat_of_nat_eq)
   320 
   321 lemma starfunNat_approx:
   322      "( *fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)"
   323 by auto
   324 
   325 
   326 text{* Example of transfer of a property from reals to hyperreals
   327     --- used for limit comparison of sequences*}
   328 
   329 lemma starfun_le_mono:
   330      "\<forall>n. N \<le> n --> f n \<le> g n
   331       ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *fNat* f) n \<le> ( *fNat* g) n"
   332 apply safe
   333 apply (rule_tac z = n in eq_Abs_hypnat)
   334 apply (auto simp add: starfunNat hypnat_of_nat_eq hypreal_le hypreal_less hypnat_le hypnat_less, ultra, auto)
   335 done
   336 
   337 (*****----- and another -----*****)
   338 lemma starfun_less_mono:
   339      "\<forall>n. N \<le> n --> f n < g n
   340       ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *fNat* f) n < ( *fNat* g) n"
   341 apply safe
   342 apply (rule_tac z = n in eq_Abs_hypnat)
   343 apply (auto simp add: starfunNat hypnat_of_nat_eq hypreal_le hypreal_less hypnat_le hypnat_less, ultra, auto)
   344 done
   345 
   346 text{*Nonstandard extension when we increment the argument by one*}
   347 
   348 lemma starfunNat_shift_one:
   349      "( *fNat* (%n. f (Suc n))) N = ( *fNat* f) (N + (1::hypnat))"
   350 apply (cases N)
   351 apply (simp add: starfunNat hypnat_one_def hypnat_add)
   352 done
   353 
   354 text{*Nonstandard extension with absolute value*}
   355 
   356 lemma starfunNat_rabs: "( *fNat* (%n. abs (f n))) N = abs(( *fNat* f) N)"
   357 apply (cases N)
   358 apply (simp add: starfunNat hypreal_hrabs)
   359 done
   360 
   361 text{*The hyperpow function as a nonstandard extension of realpow*}
   362 
   363 lemma starfunNat_pow: "( *fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
   364 apply (cases N)
   365 apply (simp add: hyperpow hypreal_of_real_def starfunNat)
   366 done
   367 
   368 lemma starfunNat_pow2:
   369      "( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m"
   370 apply (cases N)
   371 apply (simp add: hyperpow hypnat_of_nat_eq starfunNat)
   372 done
   373 
   374 lemma starfun_pow: "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"
   375 apply (rule_tac z = R in eq_Abs_hypreal)
   376 apply (simp add: hyperpow starfun hypnat_of_nat_eq)
   377 done
   378 
   379 text{*The @{term hypreal_of_hypnat} function as a nonstandard extension of
   380   @{term real_of_nat} *}
   381 
   382 lemma starfunNat_real_of_nat: "( *fNat* real) = hypreal_of_hypnat"
   383 apply (rule ext)
   384 apply (rule_tac z = x in eq_Abs_hypnat)
   385 apply (simp add: hypreal_of_hypnat starfunNat)
   386 done
   387 
   388 lemma starfunNat_inverse_real_of_nat_eq:
   389      "N \<in> HNatInfinite
   390    ==> ( *fNat* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)"
   391 apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst])
   392 apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
   393 apply (simp_all add: HNatInfinite_not_eq_zero starfunNat_real_of_nat starfun_inverse_inverse)
   394 done
   395 
   396 text{*Internal functions - some redundancy with *fNat* now*}
   397 
   398 lemma starfunNat_n_congruent:
   399       "congruent hypnatrel (%X. hypnatrel``{%n. f n (X n)})"
   400 apply (simp add: congruent_def, safe)
   401 apply (ultra+)
   402 done
   403 
   404 lemma starfunNat_n:
   405      "( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
   406       Abs_hypreal(hyprel `` {%n. f n (X n)})"
   407 apply (simp add: starfunNat_n_def)
   408 apply (rule_tac f = Abs_hypreal in arg_cong, auto, ultra)
   409 done
   410 
   411 text{*Multiplication: @{text "( *fn) x ( *gn) = *(fn x gn)"}*}
   412 
   413 lemma starfunNat_n_mult:
   414      "( *fNatn* f) z * ( *fNatn* g) z = ( *fNatn* (% i x. f i x * g i x)) z"
   415 apply (cases z)
   416 apply (simp add: starfunNat_n hypreal_mult)
   417 done
   418 
   419 text{*Addition: @{text "( *fn) + ( *gn) = *(fn + gn)"}*}
   420 
   421 lemma starfunNat_n_add:
   422      "( *fNatn* f) z + ( *fNatn* g) z = ( *fNatn* (%i x. f i x + g i x)) z"
   423 apply (cases z)
   424 apply (simp add: starfunNat_n hypreal_add)
   425 done
   426 
   427 text{*Subtraction: @{text "( *fn) - ( *gn) = *(fn + - gn)"}*}
   428 
   429 lemma starfunNat_n_add_minus:
   430      "( *fNatn* f) z + -( *fNatn* g) z = ( *fNatn* (%i x. f i x + -g i x)) z"
   431 apply (cases z)
   432 apply (simp add: starfunNat_n hypreal_minus hypreal_add)
   433 done
   434 
   435 
   436 text{*Composition: @{text "( *fn) o ( *gn) = *(fn o gn)"}*}
   437 
   438 lemma starfunNat_n_const_fun [simp]:
   439      "( *fNatn* (%i x. k)) z = hypreal_of_real  k"
   440 apply (cases z)
   441 apply (simp add: starfunNat_n hypreal_of_real_def)
   442 done
   443 
   444 lemma starfunNat_n_minus: "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x"
   445 apply (cases x)
   446 apply (simp add: starfunNat_n hypreal_minus)
   447 done
   448 
   449 lemma starfunNat_n_eq [simp]:
   450      "( *fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})"
   451 by (simp add: starfunNat_n hypnat_of_nat_eq)
   452 
   453 lemma starfun_eq_iff: "(( *fNat* f) = ( *fNat* g)) = (f = g)"
   454 apply auto
   455 apply (rule ext, rule ccontr)
   456 apply (drule_tac x = "hypnat_of_nat (x) " in fun_cong)
   457 apply (simp add: starfunNat hypnat_of_nat_eq)
   458 done
   459 
   460 
   461 lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]:
   462      "N \<in> HNatInfinite ==> ( *fNat* (%x. inverse (real x))) N \<in> Infinitesimal"
   463 apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst])
   464 apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
   465 apply (simp_all add: HNatInfinite_not_eq_zero starfunNat_real_of_nat)
   466 done
   467 
   468 ML
   469 {*
   470 val starsetNat_def = thm "starsetNat_def";
   471 
   472 val NatStar_real_set = thm "NatStar_real_set";
   473 val NatStar_empty_set = thm "NatStar_empty_set";
   474 val NatStar_Un = thm "NatStar_Un";
   475 val starsetNat_n_Un = thm "starsetNat_n_Un";
   476 val InternalNatSets_Un = thm "InternalNatSets_Un";
   477 val NatStar_Int = thm "NatStar_Int";
   478 val starsetNat_n_Int = thm "starsetNat_n_Int";
   479 val InternalNatSets_Int = thm "InternalNatSets_Int";
   480 val NatStar_Compl = thm "NatStar_Compl";
   481 val starsetNat_n_Compl = thm "starsetNat_n_Compl";
   482 val InternalNatSets_Compl = thm "InternalNatSets_Compl";
   483 val starsetNat_n_diff = thm "starsetNat_n_diff";
   484 val InternalNatSets_diff = thm "InternalNatSets_diff";
   485 val NatStar_subset = thm "NatStar_subset";
   486 val NatStar_mem = thm "NatStar_mem";
   487 val NatStar_hypreal_of_real_image_subset = thm "NatStar_hypreal_of_real_image_subset";
   488 val NatStar_SHNat_subset = thm "NatStar_SHNat_subset";
   489 val NatStar_hypreal_of_real_Int = thm "NatStar_hypreal_of_real_Int";
   490 val starsetNat_starsetNat_n_eq = thm "starsetNat_starsetNat_n_eq";
   491 val InternalNatSets_starsetNat_n = thm "InternalNatSets_starsetNat_n";
   492 val InternalNatSets_UNIV_diff = thm "InternalNatSets_UNIV_diff";
   493 val starsetNat_n_starsetNat = thm "starsetNat_n_starsetNat";
   494 val starfunNat_n_starfunNat = thm "starfunNat_n_starfunNat";
   495 val starfunNat2_n_starfunNat2 = thm "starfunNat2_n_starfunNat2";
   496 val starfunNat_congruent = thm "starfunNat_congruent";
   497 val starfunNat = thm "starfunNat";
   498 val starfunNat2 = thm "starfunNat2";
   499 val starfunNat_mult = thm "starfunNat_mult";
   500 val starfunNat2_mult = thm "starfunNat2_mult";
   501 val starfunNat_add = thm "starfunNat_add";
   502 val starfunNat2_add = thm "starfunNat2_add";
   503 val starfunNat2_minus = thm "starfunNat2_minus";
   504 val starfunNatNat2_o = thm "starfunNatNat2_o";
   505 val starfunNatNat2_o2 = thm "starfunNatNat2_o2";
   506 val starfunNat2_o = thm "starfunNat2_o";
   507 val starfun_stafunNat_o = thm "starfun_stafunNat_o";
   508 val starfun_stafunNat_o2 = thm "starfun_stafunNat_o2";
   509 val starfunNat_const_fun = thm "starfunNat_const_fun";
   510 val starfunNat2_const_fun = thm "starfunNat2_const_fun";
   511 val starfunNat_minus = thm "starfunNat_minus";
   512 val starfunNat_inverse = thm "starfunNat_inverse";
   513 val starfunNat_eq = thm "starfunNat_eq";
   514 val starfunNat2_eq = thm "starfunNat2_eq";
   515 val starfunNat_approx = thm "starfunNat_approx";
   516 val starfun_le_mono = thm "starfun_le_mono";
   517 val starfun_less_mono = thm "starfun_less_mono";
   518 val starfunNat_shift_one = thm "starfunNat_shift_one";
   519 val starfunNat_rabs = thm "starfunNat_rabs";
   520 val starfunNat_pow = thm "starfunNat_pow";
   521 val starfunNat_pow2 = thm "starfunNat_pow2";
   522 val starfun_pow = thm "starfun_pow";
   523 val starfunNat_real_of_nat = thm "starfunNat_real_of_nat";
   524 val starfunNat_inverse_real_of_nat_eq = thm "starfunNat_inverse_real_of_nat_eq";
   525 val starfunNat_n_congruent = thm "starfunNat_n_congruent";
   526 val starfunNat_n = thm "starfunNat_n";
   527 val starfunNat_n_mult = thm "starfunNat_n_mult";
   528 val starfunNat_n_add = thm "starfunNat_n_add";
   529 val starfunNat_n_add_minus = thm "starfunNat_n_add_minus";
   530 val starfunNat_n_const_fun = thm "starfunNat_n_const_fun";
   531 val starfunNat_n_minus = thm "starfunNat_n_minus";
   532 val starfunNat_n_eq = thm "starfunNat_n_eq";
   533 val starfun_eq_iff = thm "starfun_eq_iff";
   534 val starfunNat_inverse_real_of_nat_Infinitesimal = thm "starfunNat_inverse_real_of_nat_Infinitesimal";
   535 *}
   536 
   537 
   538 
   539 subsection{*Nonstandard Characterization of Induction*}
   540 
   541 constdefs
   542 
   543   starPNat :: "(nat => bool) => hypnat => bool"  ("*pNat* _" [80] 80)
   544   "*pNat* P == (%x. \<exists>X. (X \<in> Rep_hypnat(x) &
   545                       {n. P(X n)} \<in> FreeUltrafilterNat))"
   546 
   547 
   548   starPNat2 :: "(nat => nat => bool) => hypnat =>hypnat => bool"
   549                ("*pNat2* _" [80] 80)
   550   "*pNat2* P == (%x y. \<exists>X. \<exists>Y. (X \<in> Rep_hypnat(x) & Y \<in> Rep_hypnat(y) &
   551                       {n. P(X n) (Y n)} \<in> FreeUltrafilterNat))"
   552 
   553   hSuc :: "hypnat => hypnat"
   554   "hSuc n == n + 1"
   555 
   556 
   557 lemma starPNat:
   558      "(( *pNat* P) (Abs_hypnat(hypnatrel``{%n. X n}))) =
   559       ({n. P (X n)} \<in> FreeUltrafilterNat)"
   560 by (auto simp add: starPNat_def, ultra)
   561 
   562 lemma starPNat_hypnat_of_nat [simp]: "( *pNat* P) (hypnat_of_nat n) = P n"
   563 by (auto simp add: starPNat hypnat_of_nat_eq)
   564 
   565 lemma hypnat_induct_obj:
   566     "(( *pNat* P) 0 &
   567             (\<forall>n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1)))
   568        --> ( *pNat* P)(n)"
   569 apply (cases n)
   570 apply (auto simp add: hypnat_zero_def hypnat_one_def starPNat, ultra)
   571 apply (erule nat_induct)
   572 apply (drule_tac x = "hypnat_of_nat n" in spec)
   573 apply (rule ccontr)
   574 apply (auto simp add: starPNat hypnat_of_nat_eq hypnat_add)
   575 done
   576 
   577 lemma hypnat_induct:
   578   "[| ( *pNat* P) 0;
   579       !!n. ( *pNat* P)(n) ==> ( *pNat* P)(n + 1)|]
   580      ==> ( *pNat* P)(n)"
   581 by (insert hypnat_induct_obj [of P n], auto)
   582 
   583 lemma starPNat2:
   584 "(( *pNat2* P) (Abs_hypnat(hypnatrel``{%n. X n}))
   585              (Abs_hypnat(hypnatrel``{%n. Y n}))) =
   586       ({n. P (X n) (Y n)} \<in> FreeUltrafilterNat)"
   587 by (auto simp add: starPNat2_def, ultra)
   588 
   589 lemma starPNat2_eq_iff: "( *pNat2* (op =)) = (op =)"
   590 apply (simp add: starPNat2_def)
   591 apply (rule ext)
   592 apply (rule ext)
   593 apply (rule_tac z = x in eq_Abs_hypnat)
   594 apply (rule_tac z = y in eq_Abs_hypnat)
   595 apply (auto, ultra)
   596 done
   597 
   598 lemma starPNat2_eq_iff2: "( *pNat2* (%x y. x = y)) X Y = (X = Y)"
   599 by (simp add: starPNat2_eq_iff)
   600 
   601 lemma lemma_hyp: "(\<exists>h. P(h::hypnat)) = (\<exists>x. P(Abs_hypnat(hypnatrel `` {x})))"
   602 apply auto
   603 apply (rule_tac z = h in eq_Abs_hypnat, auto)
   604 done
   605 
   606 lemma hSuc_not_zero [iff]: "hSuc m \<noteq> 0"
   607 by (simp add: hSuc_def)
   608 
   609 lemmas zero_not_hSuc = hSuc_not_zero [THEN not_sym, standard, iff]
   610 
   611 lemma hSuc_hSuc_eq [iff]: "(hSuc m = hSuc n) = (m = n)"
   612 by (simp add: hSuc_def hypnat_one_def)
   613 
   614 lemma nonempty_nat_set_Least_mem: "c \<in> (S :: nat set) ==> (LEAST n. n  \<in> S)  \<in> S"
   615 by (erule LeastI)
   616 
   617 lemma nonempty_InternalNatSet_has_least:
   618     "[| S \<in> InternalNatSets; S \<noteq> {} |] ==> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m"
   619 apply (auto simp add: InternalNatSets_def starsetNat_n_def lemma_hyp)
   620 apply (rule_tac z = x in eq_Abs_hypnat)
   621 apply (auto dest!: bspec simp add: hypnat_le)
   622 apply (drule_tac x = "%m. LEAST n. n \<in> As m" in spec, auto)
   623 apply (ultra, force dest: nonempty_nat_set_Least_mem)
   624 apply (drule_tac x = x in bspec, auto)
   625 apply (ultra, auto intro: Least_le)
   626 done
   627 
   628 text{* Goldblatt page 129 Thm 11.3.2*}
   629 lemma internal_induct:
   630      "[| X \<in> InternalNatSets; 0 \<in> X; \<forall>n. n \<in> X --> n + 1 \<in> X |]
   631       ==> X = (UNIV:: hypnat set)"
   632 apply (rule ccontr)
   633 apply (frule InternalNatSets_Compl)
   634 apply (drule_tac S = "- X" in nonempty_InternalNatSet_has_least, auto)
   635 apply (subgoal_tac "1 \<le> n")
   636 apply (drule_tac x = "n - 1" in bspec, safe)
   637 apply (drule_tac x = "n - 1" in spec)
   638 apply (drule_tac [2] c = 1 and a = n in add_right_mono)
   639 apply (auto simp add: linorder_not_less [symmetric] iff del: hypnat_neq0_conv)
   640 done
   641 
   642 
   643 end
   644 
   645