src/HOL/NSA/NSCA.thy

 (*  Title       : NSA/NSCA.thy
     Author      : Jacques D. Fleuriot
     Copyright   : 2001,2002 University of Edinburgh
 *)
 
-section{*Non-Standard Complex Analysis*}
+section\<open>Non-Standard Complex Analysis\<close>
 
 theory NSCA
 imports NSComplex HTranscendental
 begin
 
 abbreviation
    (* standard complex numbers reagarded as an embedded subset of NS complex *)
    SComplex  :: "hcomplex set" where
    "SComplex \<equiv> Standard"
 
-definition --{* standard part map*}
+definition \<comment>\<open>standard part map\<close>
   stc :: "hcomplex => hcomplex" where 
   "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
 
 
-subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
+subsection\<open>Closure Laws for SComplex, the Standard Complex Numbers\<close>
 
 lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)"
 by (auto, drule Standard_minus, auto)
 
 lemma SComplex_add_cancel:

       |] ==> \<exists>r \<in> Reals. hcmod x< r & r < hcmod y"
 apply (auto intro: SReal_dense simp add: SReal_hcmod_SComplex)
 done
 
 
-subsection{*The Finite Elements form a Subring*}
+subsection\<open>The Finite Elements form a Subring\<close>
 
 lemma HFinite_hcmod_hcomplex_of_complex [simp]:
      "hcmod (hcomplex_of_complex r) \<in> HFinite"
 by (auto intro!: SReal_subset_HFinite [THEN subsetD])
 

 lemma HFinite_bounded_hcmod:
   "[|x \<in> HFinite; y \<le> hcmod x; 0 \<le> y |] ==> y: HFinite"
 by (auto intro: HFinite_bounded simp add: HFinite_hcmod_iff)
 
 
-subsection{*The Complex Infinitesimals form a Subring*}
+subsection\<open>The Complex Infinitesimals form a Subring\<close>
 
 lemma hcomplex_sum_of_halves: "x/(2::hcomplex) + x/(2::hcomplex) = x"
 by auto
 
 lemma Infinitesimal_hcmod_iff: 

          hcmod e' \<le> hcmod x ; hcmod x \<le> hcmod e  
       |] ==> x \<in> Infinitesimal"
 by (auto intro: Infinitesimal_interval2 simp add: Infinitesimal_hcmod_iff)
 
 
-subsection{*The ``Infinitely Close'' Relation*}
+subsection\<open>The ``Infinitely Close'' Relation\<close>
 
 (*
 Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)"
 by (auto_tac (claset(),simpset() addsimps [Infinitesimal_hcmod_iff]));
 *)

 apply (rule approx_minus_iff [THEN iffD2])
 apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric])
 done
 
 
-subsection{*Zero is the Only Infinitesimal Complex Number*}
+subsection\<open>Zero is the Only Infinitesimal Complex Number\<close>
 
 lemma Infinitesimal_less_SComplex:
    "[| x \<in> SComplex; y \<in> Infinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x"
 by (auto intro: Infinitesimal_less_SReal SReal_hcmod_SComplex simp add: Infinitesimal_hcmod_iff)
 

 
 lemma approx_unique_complex:
      "[| r \<in> SComplex; s \<in> SComplex; r @= x; s @= x|] ==> r = s"
 by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2)
 
-subsection {* Properties of @{term hRe}, @{term hIm} and @{term HComplex} *}
+subsection \<open>Properties of @{term hRe}, @{term hIm} and @{term HComplex}\<close>
 
 
 lemma abs_hRe_le_hcmod: "\<And>x. \<bar>hRe x\<bar> \<le> hcmod x"
 by transfer (rule abs_Re_le_cmod)
 

 
 lemmas hcomplex_of_complex_approx_inverse =
   hcomplex_of_complex_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
 
 
-subsection{*Theorems About Monads*}
+subsection\<open>Theorems About Monads\<close>
 
 lemma monad_zero_hcmod_iff: "(x \<in> monad 0) = (hcmod x:monad 0)"
 by (simp add: Infinitesimal_monad_zero_iff [symmetric] Infinitesimal_hcmod_iff)
 
 
-subsection{*Theorems About Standard Part*}
+subsection\<open>Theorems About Standard Part\<close>
 
 lemma stc_approx_self: "x \<in> HFinite ==> stc x @= x"
 apply (simp add: stc_def)
 apply (frule stc_part_Ex, safe)
 apply (rule someI2)