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