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