src/HOL/NSA/NatStar.thy
author nipkow
Tue Sep 07 10:05:19 2010 +0200 (2010-09-07)
changeset 39198 f967a16dfcdd
parent 27468 0783dd1dc13d
child 39302 d7728f65b353
permissions -rw-r--r--
expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets
huffman@27468
     1
(*  Title       : NatStar.thy
huffman@27468
     2
    Author      : Jacques D. Fleuriot
huffman@27468
     3
    Copyright   : 1998  University of Cambridge
huffman@27468
     4
huffman@27468
     5
Converted to Isar and polished by lcp
huffman@27468
     6
*)
huffman@27468
     7
huffman@27468
     8
header{*Star-transforms for the Hypernaturals*}
huffman@27468
     9
huffman@27468
    10
theory NatStar
huffman@27468
    11
imports Star
huffman@27468
    12
begin
huffman@27468
    13
huffman@27468
    14
lemma star_n_eq_starfun_whn: "star_n X = ( *f* X) whn"
huffman@27468
    15
by (simp add: hypnat_omega_def starfun_def star_of_def Ifun_star_n)
huffman@27468
    16
huffman@27468
    17
lemma starset_n_Un: "*sn* (%n. (A n) Un (B n)) = *sn* A Un *sn* B"
huffman@27468
    18
apply (simp add: starset_n_def star_n_eq_starfun_whn Un_def)
huffman@27468
    19
apply (rule_tac x=whn in spec, transfer, simp)
huffman@27468
    20
done
huffman@27468
    21
huffman@27468
    22
lemma InternalSets_Un:
huffman@27468
    23
     "[| X \<in> InternalSets; Y \<in> InternalSets |]
huffman@27468
    24
      ==> (X Un Y) \<in> InternalSets"
huffman@27468
    25
by (auto simp add: InternalSets_def starset_n_Un [symmetric])
huffman@27468
    26
huffman@27468
    27
lemma starset_n_Int:
huffman@27468
    28
      "*sn* (%n. (A n) Int (B n)) = *sn* A Int *sn* B"
huffman@27468
    29
apply (simp add: starset_n_def star_n_eq_starfun_whn Int_def)
huffman@27468
    30
apply (rule_tac x=whn in spec, transfer, simp)
huffman@27468
    31
done
huffman@27468
    32
huffman@27468
    33
lemma InternalSets_Int:
huffman@27468
    34
     "[| X \<in> InternalSets; Y \<in> InternalSets |]
huffman@27468
    35
      ==> (X Int Y) \<in> InternalSets"
huffman@27468
    36
by (auto simp add: InternalSets_def starset_n_Int [symmetric])
huffman@27468
    37
huffman@27468
    38
lemma starset_n_Compl: "*sn* ((%n. - A n)) = -( *sn* A)"
huffman@27468
    39
apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
huffman@27468
    40
apply (rule_tac x=whn in spec, transfer, simp)
huffman@27468
    41
done
huffman@27468
    42
huffman@27468
    43
lemma InternalSets_Compl: "X \<in> InternalSets ==> -X \<in> InternalSets"
huffman@27468
    44
by (auto simp add: InternalSets_def starset_n_Compl [symmetric])
huffman@27468
    45
huffman@27468
    46
lemma starset_n_diff: "*sn* (%n. (A n) - (B n)) = *sn* A - *sn* B"
huffman@27468
    47
apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
huffman@27468
    48
apply (rule_tac x=whn in spec, transfer, simp)
huffman@27468
    49
done
huffman@27468
    50
huffman@27468
    51
lemma InternalSets_diff:
huffman@27468
    52
     "[| X \<in> InternalSets; Y \<in> InternalSets |]
huffman@27468
    53
      ==> (X - Y) \<in> InternalSets"
huffman@27468
    54
by (auto simp add: InternalSets_def starset_n_diff [symmetric])
huffman@27468
    55
huffman@27468
    56
lemma NatStar_SHNat_subset: "Nats \<le> *s* (UNIV:: nat set)"
huffman@27468
    57
by simp
huffman@27468
    58
huffman@27468
    59
lemma NatStar_hypreal_of_real_Int:
huffman@27468
    60
     "*s* X Int Nats = hypnat_of_nat ` X"
huffman@27468
    61
by (auto simp add: SHNat_eq)
huffman@27468
    62
huffman@27468
    63
lemma starset_starset_n_eq: "*s* X = *sn* (%n. X)"
huffman@27468
    64
by (simp add: starset_n_starset)
huffman@27468
    65
huffman@27468
    66
lemma InternalSets_starset_n [simp]: "( *s* X) \<in> InternalSets"
huffman@27468
    67
by (auto simp add: InternalSets_def starset_starset_n_eq)
huffman@27468
    68
huffman@27468
    69
lemma InternalSets_UNIV_diff:
huffman@27468
    70
     "X \<in> InternalSets ==> UNIV - X \<in> InternalSets"
huffman@27468
    71
apply (subgoal_tac "UNIV - X = - X")
huffman@27468
    72
by (auto intro: InternalSets_Compl)
huffman@27468
    73
huffman@27468
    74
huffman@27468
    75
subsection{*Nonstandard Extensions of Functions*}
huffman@27468
    76
huffman@27468
    77
text{* Example of transfer of a property from reals to hyperreals
huffman@27468
    78
    --- used for limit comparison of sequences*}
huffman@27468
    79
huffman@27468
    80
lemma starfun_le_mono:
huffman@27468
    81
     "\<forall>n. N \<le> n --> f n \<le> g n
huffman@27468
    82
      ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *f* f) n \<le> ( *f* g) n"
huffman@27468
    83
by transfer
huffman@27468
    84
huffman@27468
    85
(*****----- and another -----*****)
huffman@27468
    86
lemma starfun_less_mono:
huffman@27468
    87
     "\<forall>n. N \<le> n --> f n < g n
huffman@27468
    88
      ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *f* f) n < ( *f* g) n"
huffman@27468
    89
by transfer
huffman@27468
    90
huffman@27468
    91
text{*Nonstandard extension when we increment the argument by one*}
huffman@27468
    92
huffman@27468
    93
lemma starfun_shift_one:
huffman@27468
    94
     "!!N. ( *f* (%n. f (Suc n))) N = ( *f* f) (N + (1::hypnat))"
huffman@27468
    95
by (transfer, simp)
huffman@27468
    96
huffman@27468
    97
text{*Nonstandard extension with absolute value*}
huffman@27468
    98
huffman@27468
    99
lemma starfun_abs: "!!N. ( *f* (%n. abs (f n))) N = abs(( *f* f) N)"
huffman@27468
   100
by (transfer, rule refl)
huffman@27468
   101
huffman@27468
   102
text{*The hyperpow function as a nonstandard extension of realpow*}
huffman@27468
   103
huffman@27468
   104
lemma starfun_pow: "!!N. ( *f* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
huffman@27468
   105
by (transfer, rule refl)
huffman@27468
   106
huffman@27468
   107
lemma starfun_pow2:
huffman@27468
   108
     "!!N. ( *f* (%n. (X n) ^ m)) N = ( *f* X) N pow hypnat_of_nat m"
huffman@27468
   109
by (transfer, rule refl)
huffman@27468
   110
huffman@27468
   111
lemma starfun_pow3: "!!R. ( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"
huffman@27468
   112
by (transfer, rule refl)
huffman@27468
   113
huffman@27468
   114
text{*The @{term hypreal_of_hypnat} function as a nonstandard extension of
huffman@27468
   115
  @{term real_of_nat} *}
huffman@27468
   116
huffman@27468
   117
lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
nipkow@39198
   118
by transfer (simp add: ext_iff real_of_nat_def)
huffman@27468
   119
huffman@27468
   120
lemma starfun_inverse_real_of_nat_eq:
huffman@27468
   121
     "N \<in> HNatInfinite
huffman@27468
   122
   ==> ( *f* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)"
huffman@27468
   123
apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
huffman@27468
   124
apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
huffman@27468
   125
apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat starfun_inverse_inverse)
huffman@27468
   126
done
huffman@27468
   127
huffman@27468
   128
text{*Internal functions - some redundancy with *f* now*}
huffman@27468
   129
huffman@27468
   130
lemma starfun_n: "( *fn* f) (star_n X) = star_n (%n. f n (X n))"
huffman@27468
   131
by (simp add: starfun_n_def Ifun_star_n)
huffman@27468
   132
huffman@27468
   133
text{*Multiplication: @{text "( *fn) x ( *gn) = *(fn x gn)"}*}
huffman@27468
   134
huffman@27468
   135
lemma starfun_n_mult:
huffman@27468
   136
     "( *fn* f) z * ( *fn* g) z = ( *fn* (% i x. f i x * g i x)) z"
huffman@27468
   137
apply (cases z)
huffman@27468
   138
apply (simp add: starfun_n star_n_mult)
huffman@27468
   139
done
huffman@27468
   140
huffman@27468
   141
text{*Addition: @{text "( *fn) + ( *gn) = *(fn + gn)"}*}
huffman@27468
   142
huffman@27468
   143
lemma starfun_n_add:
huffman@27468
   144
     "( *fn* f) z + ( *fn* g) z = ( *fn* (%i x. f i x + g i x)) z"
huffman@27468
   145
apply (cases z)
huffman@27468
   146
apply (simp add: starfun_n star_n_add)
huffman@27468
   147
done
huffman@27468
   148
huffman@27468
   149
text{*Subtraction: @{text "( *fn) - ( *gn) = *(fn + - gn)"}*}
huffman@27468
   150
huffman@27468
   151
lemma starfun_n_add_minus:
huffman@27468
   152
     "( *fn* f) z + -( *fn* g) z = ( *fn* (%i x. f i x + -g i x)) z"
huffman@27468
   153
apply (cases z)
huffman@27468
   154
apply (simp add: starfun_n star_n_minus star_n_add)
huffman@27468
   155
done
huffman@27468
   156
huffman@27468
   157
huffman@27468
   158
text{*Composition: @{text "( *fn) o ( *gn) = *(fn o gn)"}*}
huffman@27468
   159
huffman@27468
   160
lemma starfun_n_const_fun [simp]:
huffman@27468
   161
     "( *fn* (%i x. k)) z = star_of k"
huffman@27468
   162
apply (cases z)
huffman@27468
   163
apply (simp add: starfun_n star_of_def)
huffman@27468
   164
done
huffman@27468
   165
huffman@27468
   166
lemma starfun_n_minus: "- ( *fn* f) x = ( *fn* (%i x. - (f i) x)) x"
huffman@27468
   167
apply (cases x)
huffman@27468
   168
apply (simp add: starfun_n star_n_minus)
huffman@27468
   169
done
huffman@27468
   170
huffman@27468
   171
lemma starfun_n_eq [simp]:
huffman@27468
   172
     "( *fn* f) (star_of n) = star_n (%i. f i n)"
huffman@27468
   173
by (simp add: starfun_n star_of_def)
huffman@27468
   174
huffman@27468
   175
lemma starfun_eq_iff: "(( *f* f) = ( *f* g)) = (f = g)"
huffman@27468
   176
by (transfer, rule refl)
huffman@27468
   177
huffman@27468
   178
lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]:
huffman@27468
   179
     "N \<in> HNatInfinite ==> ( *f* (%x. inverse (real x))) N \<in> Infinitesimal"
huffman@27468
   180
apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
huffman@27468
   181
apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
huffman@27468
   182
apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
huffman@27468
   183
done
huffman@27468
   184
huffman@27468
   185
huffman@27468
   186
subsection{*Nonstandard Characterization of Induction*}
huffman@27468
   187
huffman@27468
   188
lemma hypnat_induct_obj:
huffman@27468
   189
    "!!n. (( *p* P) (0::hypnat) &
huffman@27468
   190
            (\<forall>n. ( *p* P)(n) --> ( *p* P)(n + 1)))
huffman@27468
   191
       --> ( *p* P)(n)"
huffman@27468
   192
by (transfer, induct_tac n, auto)
huffman@27468
   193
huffman@27468
   194
lemma hypnat_induct:
huffman@27468
   195
  "!!n. [| ( *p* P) (0::hypnat);
huffman@27468
   196
      !!n. ( *p* P)(n) ==> ( *p* P)(n + 1)|]
huffman@27468
   197
     ==> ( *p* P)(n)"
huffman@27468
   198
by (transfer, induct_tac n, auto)
huffman@27468
   199
huffman@27468
   200
lemma starP2_eq_iff: "( *p2* (op =)) = (op =)"
huffman@27468
   201
by transfer (rule refl)
huffman@27468
   202
huffman@27468
   203
lemma starP2_eq_iff2: "( *p2* (%x y. x = y)) X Y = (X = Y)"
huffman@27468
   204
by (simp add: starP2_eq_iff)
huffman@27468
   205
huffman@27468
   206
lemma nonempty_nat_set_Least_mem:
huffman@27468
   207
  "c \<in> (S :: nat set) ==> (LEAST n. n \<in> S) \<in> S"
huffman@27468
   208
by (erule LeastI)
huffman@27468
   209
huffman@27468
   210
lemma nonempty_set_star_has_least:
huffman@27468
   211
    "!!S::nat set star. Iset S \<noteq> {} ==> \<exists>n \<in> Iset S. \<forall>m \<in> Iset S. n \<le> m"
huffman@27468
   212
apply (transfer empty_def)
huffman@27468
   213
apply (rule_tac x="LEAST n. n \<in> S" in bexI)
huffman@27468
   214
apply (simp add: Least_le)
huffman@27468
   215
apply (rule LeastI_ex, auto)
huffman@27468
   216
done
huffman@27468
   217
huffman@27468
   218
lemma nonempty_InternalNatSet_has_least:
huffman@27468
   219
    "[| (S::hypnat set) \<in> InternalSets; S \<noteq> {} |] ==> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m"
huffman@27468
   220
apply (clarsimp simp add: InternalSets_def starset_n_def)
huffman@27468
   221
apply (erule nonempty_set_star_has_least)
huffman@27468
   222
done
huffman@27468
   223
huffman@27468
   224
text{* Goldblatt page 129 Thm 11.3.2*}
huffman@27468
   225
lemma internal_induct_lemma:
huffman@27468
   226
     "!!X::nat set star. [| (0::hypnat) \<in> Iset X; \<forall>n. n \<in> Iset X --> n + 1 \<in> Iset X |]
huffman@27468
   227
      ==> Iset X = (UNIV:: hypnat set)"
huffman@27468
   228
apply (transfer UNIV_def)
huffman@27468
   229
apply (rule equalityI [OF subset_UNIV subsetI])
huffman@27468
   230
apply (induct_tac x, auto)
huffman@27468
   231
done
huffman@27468
   232
huffman@27468
   233
lemma internal_induct:
huffman@27468
   234
     "[| X \<in> InternalSets; (0::hypnat) \<in> X; \<forall>n. n \<in> X --> n + 1 \<in> X |]
huffman@27468
   235
      ==> X = (UNIV:: hypnat set)"
huffman@27468
   236
apply (clarsimp simp add: InternalSets_def starset_n_def)
huffman@27468
   237
apply (erule (1) internal_induct_lemma)
huffman@27468
   238
done
huffman@27468
   239
huffman@27468
   240
huffman@27468
   241
end