src/HOL/NSA/NatStar.thy

     Copyright   : 1998  University of Cambridge
 
 Converted to Isar and polished by lcp
 *)
 
-section{*Star-transforms for the Hypernaturals*}
+section\<open>Star-transforms for the Hypernaturals\<close>
 
 theory NatStar
 imports Star
 begin
 

      "X \<in> InternalSets ==> UNIV - X \<in> InternalSets"
 apply (subgoal_tac "UNIV - X = - X")
 by (auto intro: InternalSets_Compl)
 
 
-subsection{*Nonstandard Extensions of Functions*}
-
-text{* Example of transfer of a property from reals to hyperreals
-    --- used for limit comparison of sequences*}
+subsection\<open>Nonstandard Extensions of Functions\<close>
+
+text\<open>Example of transfer of a property from reals to hyperreals
+    --- used for limit comparison of sequences\<close>
 
 lemma starfun_le_mono:
      "\<forall>n. N \<le> n --> f n \<le> g n
       ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *f* f) n \<le> ( *f* g) n"
 by transfer

 lemma starfun_less_mono:
      "\<forall>n. N \<le> n --> f n < g n
       ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *f* f) n < ( *f* g) n"
 by transfer
 
-text{*Nonstandard extension when we increment the argument by one*}
+text\<open>Nonstandard extension when we increment the argument by one\<close>
 
 lemma starfun_shift_one:
      "!!N. ( *f* (%n. f (Suc n))) N = ( *f* f) (N + (1::hypnat))"
 by (transfer, simp)
 
-text{*Nonstandard extension with absolute value*}
+text\<open>Nonstandard extension with absolute value\<close>
 
 lemma starfun_abs: "!!N. ( *f* (%n. \<bar>f n\<bar>)) N = \<bar>( *f* f) N\<bar>"
 by (transfer, rule refl)
 
-text{*The hyperpow function as a nonstandard extension of realpow*}
+text\<open>The hyperpow function as a nonstandard extension of realpow\<close>
 
 lemma starfun_pow: "!!N. ( *f* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
 by (transfer, rule refl)
 
 lemma starfun_pow2:

 by (transfer, rule refl)
 
 lemma starfun_pow3: "!!R. ( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"
 by (transfer, rule refl)
 
-text{*The @{term hypreal_of_hypnat} function as a nonstandard extension of
-  @{term real_of_nat} *}
+text\<open>The @{term hypreal_of_hypnat} function as a nonstandard extension of
+  @{term real_of_nat}\<close>
 
 lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
 by transfer (simp add: fun_eq_iff)
 
 lemma starfun_inverse_real_of_nat_eq:

 apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
 apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
 apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat starfun_inverse_inverse)
 done
 
-text{*Internal functions - some redundancy with *f* now*}
+text\<open>Internal functions - some redundancy with *f* now\<close>
 
 lemma starfun_n: "( *fn* f) (star_n X) = star_n (%n. f n (X n))"
 by (simp add: starfun_n_def Ifun_star_n)
 
-text{*Multiplication: @{text "( *fn) x ( *gn) = *(fn x gn)"}*}
+text\<open>Multiplication: \<open>( *fn) x ( *gn) = *(fn x gn)\<close>\<close>
 
 lemma starfun_n_mult:
      "( *fn* f) z * ( *fn* g) z = ( *fn* (% i x. f i x * g i x)) z"
 apply (cases z)
 apply (simp add: starfun_n star_n_mult)
 done
 
-text{*Addition: @{text "( *fn) + ( *gn) = *(fn + gn)"}*}
+text\<open>Addition: \<open>( *fn) + ( *gn) = *(fn + gn)\<close>\<close>
 
 lemma starfun_n_add:
      "( *fn* f) z + ( *fn* g) z = ( *fn* (%i x. f i x + g i x)) z"
 apply (cases z)
 apply (simp add: starfun_n star_n_add)
 done
 
-text{*Subtraction: @{text "( *fn) - ( *gn) = *(fn + - gn)"}*}
+text\<open>Subtraction: \<open>( *fn) - ( *gn) = *(fn + - gn)\<close>\<close>
 
 lemma starfun_n_add_minus:
      "( *fn* f) z + -( *fn* g) z = ( *fn* (%i x. f i x + -g i x)) z"
 apply (cases z)
 apply (simp add: starfun_n star_n_minus star_n_add)
 done
 
 
-text{*Composition: @{text "( *fn) o ( *gn) = *(fn o gn)"}*}
+text\<open>Composition: \<open>( *fn) o ( *gn) = *(fn o gn)\<close>\<close>
 
 lemma starfun_n_const_fun [simp]:
      "( *fn* (%i x. k)) z = star_of k"
 apply (cases z)
 apply (simp add: starfun_n star_of_def)

 apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
 apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
 done
 
 
-subsection{*Nonstandard Characterization of Induction*}
+subsection\<open>Nonstandard Characterization of Induction\<close>
 
 lemma hypnat_induct_obj:
     "!!n. (( *p* P) (0::hypnat) &
             (\<forall>n. ( *p* P)(n) --> ( *p* P)(n + 1)))
        --> ( *p* P)(n)"

     "[| (S::hypnat set) \<in> InternalSets; S \<noteq> {} |] ==> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m"
 apply (clarsimp simp add: InternalSets_def starset_n_def)
 apply (erule nonempty_set_star_has_least)
 done
 
-text{* Goldblatt page 129 Thm 11.3.2*}
+text\<open>Goldblatt page 129 Thm 11.3.2\<close>
 lemma internal_induct_lemma:
      "!!X::nat set star. [| (0::hypnat) \<in> Iset X; \<forall>n. n \<in> Iset X --> n + 1 \<in> Iset X |]
       ==> Iset X = (UNIV:: hypnat set)"
 apply (transfer UNIV_def)
 apply (rule equalityI [OF subset_UNIV subsetI])