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