src/HOL/Nonstandard_Analysis/NatStar.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (21 months ago)
changeset 67003 49850a679c2c
parent 64435 c93b0e6131c3
child 67091 1393c2340eec
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@62479
     1
(*  Title:      HOL/Nonstandard_Analysis/NatStar.thy
wenzelm@62479
     2
    Author:     Jacques D. Fleuriot
wenzelm@62479
     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
wenzelm@64435
     8
section \<open>Star-transforms for the Hypernaturals\<close>
huffman@27468
     9
huffman@27468
    10
theory NatStar
wenzelm@64435
    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"
wenzelm@64435
    15
  by (simp add: hypnat_omega_def starfun_def star_of_def Ifun_star_n)
huffman@27468
    16
wenzelm@64435
    17
lemma starset_n_Un: "*sn* (\<lambda>n. (A n) \<union> (B n)) = *sn* A \<union> *sn* B"
wenzelm@64435
    18
  apply (simp add: starset_n_def star_n_eq_starfun_whn Un_def)
wenzelm@64435
    19
  apply (rule_tac x=whn in spec, transfer, simp)
wenzelm@64435
    20
  done
huffman@27468
    21
wenzelm@64435
    22
lemma InternalSets_Un: "X \<in> InternalSets \<Longrightarrow> Y \<in> InternalSets \<Longrightarrow> X \<union> Y \<in> InternalSets"
wenzelm@64435
    23
  by (auto simp add: InternalSets_def starset_n_Un [symmetric])
huffman@27468
    24
wenzelm@64435
    25
lemma starset_n_Int: "*sn* (\<lambda>n. A n \<inter> B n) = *sn* A \<inter> *sn* B"
wenzelm@64435
    26
  apply (simp add: starset_n_def star_n_eq_starfun_whn Int_def)
wenzelm@64435
    27
  apply (rule_tac x=whn in spec, transfer, simp)
wenzelm@64435
    28
  done
huffman@27468
    29
wenzelm@64435
    30
lemma InternalSets_Int: "X \<in> InternalSets \<Longrightarrow> Y \<in> InternalSets \<Longrightarrow> X \<inter> Y \<in> InternalSets"
wenzelm@64435
    31
  by (auto simp add: InternalSets_def starset_n_Int [symmetric])
huffman@27468
    32
wenzelm@64435
    33
lemma starset_n_Compl: "*sn* ((\<lambda>n. - A n)) = - ( *sn* A)"
wenzelm@64435
    34
  apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
wenzelm@64435
    35
  apply (rule_tac x=whn in spec, transfer, simp)
wenzelm@64435
    36
  done
huffman@27468
    37
wenzelm@64435
    38
lemma InternalSets_Compl: "X \<in> InternalSets \<Longrightarrow> - X \<in> InternalSets"
wenzelm@64435
    39
  by (auto simp add: InternalSets_def starset_n_Compl [symmetric])
huffman@27468
    40
wenzelm@64435
    41
lemma starset_n_diff: "*sn* (\<lambda>n. (A n) - (B n)) = *sn* A - *sn* B"
wenzelm@64435
    42
  apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
wenzelm@64435
    43
  apply (rule_tac x=whn in spec, transfer, simp)
wenzelm@64435
    44
  done
huffman@27468
    45
wenzelm@64435
    46
lemma InternalSets_diff: "X \<in> InternalSets \<Longrightarrow> Y \<in> InternalSets \<Longrightarrow> X - Y \<in> InternalSets"
wenzelm@64435
    47
  by (auto simp add: InternalSets_def starset_n_diff [symmetric])
huffman@27468
    48
huffman@27468
    49
lemma NatStar_SHNat_subset: "Nats \<le> *s* (UNIV:: nat set)"
wenzelm@64435
    50
  by simp
huffman@27468
    51
wenzelm@64435
    52
lemma NatStar_hypreal_of_real_Int: "*s* X Int Nats = hypnat_of_nat ` X"
wenzelm@64435
    53
  by (auto simp add: SHNat_eq)
huffman@27468
    54
wenzelm@64435
    55
lemma starset_starset_n_eq: "*s* X = *sn* (\<lambda>n. X)"
wenzelm@64435
    56
  by (simp add: starset_n_starset)
huffman@27468
    57
huffman@27468
    58
lemma InternalSets_starset_n [simp]: "( *s* X) \<in> InternalSets"
wenzelm@64435
    59
  by (auto simp add: InternalSets_def starset_starset_n_eq)
huffman@27468
    60
wenzelm@64435
    61
lemma InternalSets_UNIV_diff: "X \<in> InternalSets \<Longrightarrow> UNIV - X \<in> InternalSets"
wenzelm@64435
    62
  apply (subgoal_tac "UNIV - X = - X")
wenzelm@64435
    63
   apply (auto intro: InternalSets_Compl)
wenzelm@64435
    64
  done
huffman@27468
    65
huffman@27468
    66
wenzelm@64435
    67
subsection \<open>Nonstandard Extensions of Functions\<close>
huffman@27468
    68
wenzelm@64435
    69
text \<open>Example of transfer of a property from reals to hyperreals
wenzelm@64435
    70
  --- used for limit comparison of sequences.\<close>
wenzelm@64435
    71
wenzelm@64435
    72
lemma starfun_le_mono: "\<forall>n. N \<le> n \<longrightarrow> f n \<le> g n \<Longrightarrow>
wenzelm@64435
    73
  \<forall>n. hypnat_of_nat N \<le> n \<longrightarrow> ( *f* f) n \<le> ( *f* g) n"
wenzelm@64435
    74
  by transfer
huffman@27468
    75
wenzelm@64435
    76
text \<open>And another:\<close>
huffman@27468
    77
lemma starfun_less_mono:
wenzelm@64435
    78
  "\<forall>n. N \<le> n \<longrightarrow> f n < g n \<Longrightarrow> \<forall>n. hypnat_of_nat N \<le> n \<longrightarrow> ( *f* f) n < ( *f* g) n"
wenzelm@64435
    79
  by transfer
huffman@27468
    80
wenzelm@64435
    81
text \<open>Nonstandard extension when we increment the argument by one.\<close>
huffman@27468
    82
wenzelm@64435
    83
lemma starfun_shift_one: "\<And>N. ( *f* (\<lambda>n. f (Suc n))) N = ( *f* f) (N + (1::hypnat))"
wenzelm@64435
    84
  by transfer simp
huffman@27468
    85
wenzelm@64435
    86
text \<open>Nonstandard extension with absolute value.\<close>
wenzelm@64435
    87
lemma starfun_abs: "\<And>N. ( *f* (\<lambda>n. \<bar>f n\<bar>)) N = \<bar>( *f* f) N\<bar>"
wenzelm@64435
    88
  by transfer (rule refl)
huffman@27468
    89
wenzelm@64435
    90
text \<open>The \<open>hyperpow\<close> function as a nonstandard extension of \<open>realpow\<close>.\<close>
wenzelm@64435
    91
lemma starfun_pow: "\<And>N. ( *f* (\<lambda>n. r ^ n)) N = hypreal_of_real r pow N"
wenzelm@64435
    92
  by transfer (rule refl)
huffman@27468
    93
wenzelm@64435
    94
lemma starfun_pow2: "\<And>N. ( *f* (\<lambda>n. X n ^ m)) N = ( *f* X) N pow hypnat_of_nat m"
wenzelm@64435
    95
  by transfer (rule refl)
huffman@27468
    96
wenzelm@64435
    97
lemma starfun_pow3: "\<And>R. ( *f* (\<lambda>r. r ^ n)) R = R pow hypnat_of_nat n"
wenzelm@64435
    98
  by transfer (rule refl)
huffman@27468
    99
wenzelm@64435
   100
text \<open>The @{term hypreal_of_hypnat} function as a nonstandard extension of
wenzelm@64435
   101
  @{term real_of_nat}.\<close>
huffman@27468
   102
lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
wenzelm@64435
   103
  by transfer (simp add: fun_eq_iff)
huffman@27468
   104
huffman@27468
   105
lemma starfun_inverse_real_of_nat_eq:
wenzelm@64435
   106
  "N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x::nat. inverse (real x))) N = inverse (hypreal_of_hypnat N)"
wenzelm@64435
   107
  apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
wenzelm@64435
   108
  apply (subgoal_tac "hypreal_of_hypnat N \<noteq> 0")
wenzelm@64435
   109
   apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
wenzelm@64435
   110
  done
huffman@27468
   111
wenzelm@64435
   112
text \<open>Internal functions -- some redundancy with \<open>*f*\<close> now.\<close>
huffman@27468
   113
wenzelm@64435
   114
lemma starfun_n: "( *fn* f) (star_n X) = star_n (\<lambda>n. f n (X n))"
wenzelm@64435
   115
  by (simp add: starfun_n_def Ifun_star_n)
huffman@27468
   116
wenzelm@64435
   117
text \<open>Multiplication: \<open>( *fn) x ( *gn) = *(fn x gn)\<close>\<close>
huffman@27468
   118
wenzelm@64435
   119
lemma starfun_n_mult: "( *fn* f) z * ( *fn* g) z = ( *fn* (\<lambda>i x. f i x * g i x)) z"
wenzelm@64435
   120
  by (cases z) (simp add: starfun_n star_n_mult)
huffman@27468
   121
wenzelm@64435
   122
text \<open>Addition: \<open>( *fn) + ( *gn) = *(fn + gn)\<close>\<close>
wenzelm@64435
   123
lemma starfun_n_add: "( *fn* f) z + ( *fn* g) z = ( *fn* (\<lambda>i x. f i x + g i x)) z"
wenzelm@64435
   124
  by (cases z) (simp add: starfun_n star_n_add)
huffman@27468
   125
wenzelm@64435
   126
text \<open>Subtraction: \<open>( *fn) - ( *gn) = *(fn + - gn)\<close>\<close>
wenzelm@64435
   127
lemma starfun_n_add_minus: "( *fn* f) z + -( *fn* g) z = ( *fn* (\<lambda>i x. f i x + -g i x)) z"
wenzelm@64435
   128
  by (cases z) (simp add: starfun_n star_n_minus star_n_add)
huffman@27468
   129
huffman@27468
   130
wenzelm@64435
   131
text \<open>Composition: \<open>( *fn) \<circ> ( *gn) = *(fn \<circ> gn)\<close>\<close>
huffman@27468
   132
wenzelm@64435
   133
lemma starfun_n_const_fun [simp]: "( *fn* (\<lambda>i x. k)) z = star_of k"
wenzelm@64435
   134
  by (cases z) (simp add: starfun_n star_of_def)
huffman@27468
   135
wenzelm@64435
   136
lemma starfun_n_minus: "- ( *fn* f) x = ( *fn* (\<lambda>i x. - (f i) x)) x"
wenzelm@64435
   137
  by (cases x) (simp add: starfun_n star_n_minus)
huffman@27468
   138
wenzelm@64435
   139
lemma starfun_n_eq [simp]: "( *fn* f) (star_of n) = star_n (\<lambda>i. f i n)"
wenzelm@64435
   140
  by (simp add: starfun_n star_of_def)
huffman@27468
   141
wenzelm@64435
   142
lemma starfun_eq_iff: "(( *f* f) = ( *f* g)) \<longleftrightarrow> f = g"
wenzelm@64435
   143
  by transfer (rule refl)
huffman@27468
   144
huffman@27468
   145
lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]:
wenzelm@64435
   146
  "N \<in> HNatInfinite \<Longrightarrow> ( *f* (%x. inverse (real x))) N \<in> Infinitesimal"
wenzelm@64435
   147
  apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
wenzelm@64435
   148
  apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
wenzelm@64435
   149
   apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
wenzelm@64435
   150
  done
huffman@27468
   151
huffman@27468
   152
wenzelm@64435
   153
subsection \<open>Nonstandard Characterization of Induction\<close>
huffman@27468
   154
huffman@27468
   155
lemma hypnat_induct_obj:
wenzelm@64435
   156
  "\<And>n. (( *p* P) (0::hypnat) \<and> (\<forall>n. ( *p* P) n \<longrightarrow> ( *p* P) (n + 1))) \<longrightarrow> ( *p* P) n"
wenzelm@64435
   157
  by transfer (induct_tac n, auto)
huffman@27468
   158
huffman@27468
   159
lemma hypnat_induct:
wenzelm@64435
   160
  "\<And>n. ( *p* P) (0::hypnat) \<Longrightarrow> (\<And>n. ( *p* P) n \<Longrightarrow> ( *p* P) (n + 1)) \<Longrightarrow> ( *p* P) n"
wenzelm@64435
   161
  by transfer (induct_tac n, auto)
huffman@27468
   162
huffman@27468
   163
lemma starP2_eq_iff: "( *p2* (op =)) = (op =)"
wenzelm@64435
   164
  by transfer (rule refl)
huffman@27468
   165
wenzelm@64435
   166
lemma starP2_eq_iff2: "( *p2* (\<lambda>x y. x = y)) X Y \<longleftrightarrow> X = Y"
wenzelm@64435
   167
  by (simp add: starP2_eq_iff)
huffman@27468
   168
wenzelm@64435
   169
lemma nonempty_nat_set_Least_mem: "c \<in> S \<Longrightarrow> (LEAST n. n \<in> S) \<in> S"
wenzelm@64435
   170
  for S :: "nat set"
wenzelm@64435
   171
  by (erule LeastI)
huffman@27468
   172
huffman@27468
   173
lemma nonempty_set_star_has_least:
wenzelm@64435
   174
  "\<And>S::nat set star. Iset S \<noteq> {} \<Longrightarrow> \<exists>n \<in> Iset S. \<forall>m \<in> Iset S. n \<le> m"
wenzelm@64435
   175
  apply (transfer empty_def)
wenzelm@64435
   176
  apply (rule_tac x="LEAST n. n \<in> S" in bexI)
wenzelm@64435
   177
   apply (simp add: Least_le)
wenzelm@64435
   178
  apply (rule LeastI_ex, auto)
wenzelm@64435
   179
  done
huffman@27468
   180
wenzelm@64435
   181
lemma nonempty_InternalNatSet_has_least: "S \<in> InternalSets \<Longrightarrow> S \<noteq> {} \<Longrightarrow> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m"
wenzelm@64435
   182
  for S :: "hypnat set"
wenzelm@64435
   183
  apply (clarsimp simp add: InternalSets_def starset_n_def)
wenzelm@64435
   184
  apply (erule nonempty_set_star_has_least)
wenzelm@64435
   185
  done
huffman@27468
   186
wenzelm@64435
   187
text \<open>Goldblatt, page 129 Thm 11.3.2.\<close>
huffman@27468
   188
lemma internal_induct_lemma:
wenzelm@64435
   189
  "\<And>X::nat set star.
wenzelm@64435
   190
    (0::hypnat) \<in> Iset X \<Longrightarrow> \<forall>n. n \<in> Iset X \<longrightarrow> n + 1 \<in> Iset X \<Longrightarrow> Iset X = (UNIV:: hypnat set)"
wenzelm@64435
   191
  apply (transfer UNIV_def)
wenzelm@64435
   192
  apply (rule equalityI [OF subset_UNIV subsetI])
wenzelm@64435
   193
  apply (induct_tac x, auto)
wenzelm@64435
   194
  done
huffman@27468
   195
huffman@27468
   196
lemma internal_induct:
wenzelm@64435
   197
  "X \<in> InternalSets \<Longrightarrow> (0::hypnat) \<in> X \<Longrightarrow> \<forall>n. n \<in> X \<longrightarrow> n + 1 \<in> X \<Longrightarrow> X = (UNIV:: hypnat set)"
wenzelm@64435
   198
  apply (clarsimp simp add: InternalSets_def starset_n_def)
wenzelm@64435
   199
  apply (erule (1) internal_induct_lemma)
wenzelm@64435
   200
  done
huffman@27468
   201
huffman@27468
   202
end