moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
authorpaulson
Thu Apr 22 10:45:56 2004 +0200 (2004-04-22)
changeset 1464179b7bd936264
parent 14640 b31870c50c68
child 14642 2bfe5de2d1fa
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
places
src/HOL/Complex/NSComplex.thy
src/HOL/Complex/NSInduct.thy
src/HOL/Complex/README.html
src/HOL/Hyperreal/HTranscendental.thy
src/HOL/Hyperreal/IntFloor.thy
src/HOL/Hyperreal/NatStar.thy
src/HOL/IsaMakefile
src/HOL/Real/RComplete.thy
     1.1 --- a/src/HOL/Complex/NSComplex.thy	Thu Apr 22 10:43:06 2004 +0200
     1.2 +++ b/src/HOL/Complex/NSComplex.thy	Thu Apr 22 10:45:56 2004 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  header{*Nonstandard Complex Numbers*}
     1.6  
     1.7 -theory NSComplex = NSInduct:
     1.8 +theory NSComplex = Complex:
     1.9  
    1.10  constdefs
    1.11      hcomplexrel :: "((nat=>complex)*(nat=>complex)) set"
     2.1 --- a/src/HOL/Complex/NSInduct.thy	Thu Apr 22 10:43:06 2004 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,127 +0,0 @@
     2.4 -(*  Title:       NSInduct.thy
     2.5 -    Author:      Jacques D. Fleuriot
     2.6 -    Copyright:   2001  University of Edinburgh
     2.7 -*)
     2.8 -
     2.9 -header{*Nonstandard Characterization of Induction*}
    2.10 -
    2.11 -theory NSInduct =  Complex:
    2.12 -
    2.13 -constdefs
    2.14 -
    2.15 -  starPNat :: "(nat => bool) => hypnat => bool"  ("*pNat* _" [80] 80)
    2.16 -  "*pNat* P == (%x. \<exists>X. (X \<in> Rep_hypnat(x) &
    2.17 -                      {n. P(X n)} \<in> FreeUltrafilterNat))"
    2.18 -
    2.19 -
    2.20 -  starPNat2 :: "(nat => nat => bool) => hypnat =>hypnat => bool"
    2.21 -               ("*pNat2* _" [80] 80)
    2.22 -  "*pNat2* P == (%x y. \<exists>X. \<exists>Y. (X \<in> Rep_hypnat(x) & Y \<in> Rep_hypnat(y) &
    2.23 -                      {n. P(X n) (Y n)} \<in> FreeUltrafilterNat))"
    2.24 -
    2.25 -  hSuc :: "hypnat => hypnat"
    2.26 -  "hSuc n == n + 1"
    2.27 -
    2.28 -
    2.29 -lemma starPNat:
    2.30 -     "(( *pNat* P) (Abs_hypnat(hypnatrel``{%n. X n}))) =
    2.31 -      ({n. P (X n)} \<in> FreeUltrafilterNat)"
    2.32 -by (auto simp add: starPNat_def, ultra)
    2.33 -
    2.34 -lemma starPNat_hypnat_of_nat [simp]: "( *pNat* P) (hypnat_of_nat n) = P n"
    2.35 -by (auto simp add: starPNat hypnat_of_nat_eq)
    2.36 -
    2.37 -lemma hypnat_induct_obj:
    2.38 -    "(( *pNat* P) 0 &
    2.39 -            (\<forall>n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1)))
    2.40 -       --> ( *pNat* P)(n)"
    2.41 -apply (cases n)
    2.42 -apply (auto simp add: hypnat_zero_def hypnat_one_def starPNat, ultra)
    2.43 -apply (erule nat_induct)
    2.44 -apply (drule_tac x = "hypnat_of_nat n" in spec)
    2.45 -apply (rule ccontr)
    2.46 -apply (auto simp add: starPNat hypnat_of_nat_eq hypnat_add)
    2.47 -done
    2.48 -
    2.49 -lemma hypnat_induct:
    2.50 -  "[| ( *pNat* P) 0;
    2.51 -      !!n. ( *pNat* P)(n) ==> ( *pNat* P)(n + 1)|]
    2.52 -     ==> ( *pNat* P)(n)"
    2.53 -by (insert hypnat_induct_obj [of P n], auto)
    2.54 -
    2.55 -lemma starPNat2:
    2.56 -"(( *pNat2* P) (Abs_hypnat(hypnatrel``{%n. X n}))
    2.57 -             (Abs_hypnat(hypnatrel``{%n. Y n}))) =
    2.58 -      ({n. P (X n) (Y n)} \<in> FreeUltrafilterNat)"
    2.59 -by (auto simp add: starPNat2_def, ultra)
    2.60 -
    2.61 -lemma starPNat2_eq_iff: "( *pNat2* (op =)) = (op =)"
    2.62 -apply (simp add: starPNat2_def)
    2.63 -apply (rule ext)
    2.64 -apply (rule ext)
    2.65 -apply (rule_tac z = x in eq_Abs_hypnat)
    2.66 -apply (rule_tac z = y in eq_Abs_hypnat)
    2.67 -apply (auto, ultra)
    2.68 -done
    2.69 -
    2.70 -lemma starPNat2_eq_iff2: "( *pNat2* (%x y. x = y)) X Y = (X = Y)"
    2.71 -by (simp add: starPNat2_eq_iff)
    2.72 -
    2.73 -lemma lemma_hyp: "(\<exists>h. P(h::hypnat)) = (\<exists>x. P(Abs_hypnat(hypnatrel `` {x})))"
    2.74 -apply auto
    2.75 -apply (rule_tac z = h in eq_Abs_hypnat, auto)
    2.76 -done
    2.77 -
    2.78 -lemma hSuc_not_zero [iff]: "hSuc m \<noteq> 0"
    2.79 -by (simp add: hSuc_def)
    2.80 -
    2.81 -lemmas zero_not_hSuc = hSuc_not_zero [THEN not_sym, standard, iff]
    2.82 -
    2.83 -lemma hSuc_hSuc_eq [iff]: "(hSuc m = hSuc n) = (m = n)"
    2.84 -by (simp add: hSuc_def hypnat_one_def)
    2.85 -
    2.86 -lemma nonempty_nat_set_Least_mem: "c \<in> (S :: nat set) ==> (LEAST n. n  \<in> S)  \<in> S"
    2.87 -by (erule LeastI)
    2.88 -
    2.89 -lemma nonempty_InternalNatSet_has_least:
    2.90 -    "[| S \<in> InternalNatSets; S \<noteq> {} |] ==> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m"
    2.91 -apply (auto simp add: InternalNatSets_def starsetNat_n_def lemma_hyp)
    2.92 -apply (rule_tac z = x in eq_Abs_hypnat)
    2.93 -apply (auto dest!: bspec simp add: hypnat_le)
    2.94 -apply (drule_tac x = "%m. LEAST n. n \<in> As m" in spec, auto)
    2.95 -apply (ultra, force dest: nonempty_nat_set_Least_mem)
    2.96 -apply (drule_tac x = x in bspec, auto)
    2.97 -apply (ultra, auto intro: Least_le)
    2.98 -done
    2.99 -
   2.100 -text{* Goldblatt page 129 Thm 11.3.2*}
   2.101 -lemma internal_induct:
   2.102 -     "[| X \<in> InternalNatSets; 0 \<in> X; \<forall>n. n \<in> X --> n + 1 \<in> X |]
   2.103 -      ==> X = (UNIV:: hypnat set)"
   2.104 -apply (rule ccontr)
   2.105 -apply (frule InternalNatSets_Compl)
   2.106 -apply (drule_tac S = "- X" in nonempty_InternalNatSet_has_least, auto)
   2.107 -apply (subgoal_tac "1 \<le> n")
   2.108 -apply (drule_tac x = "n - 1" in bspec, safe)
   2.109 -apply (drule_tac x = "n - 1" in spec)
   2.110 -apply (drule_tac [2] c = 1 and a = n in add_right_mono)
   2.111 -apply (auto simp add: linorder_not_less [symmetric] iff del: hypnat_neq0_conv)
   2.112 -done
   2.113 -
   2.114 -ML
   2.115 -{*
   2.116 -val starPNat = thm "starPNat";
   2.117 -val starPNat_hypnat_of_nat = thm "starPNat_hypnat_of_nat";
   2.118 -val hypnat_induct = thm "hypnat_induct";
   2.119 -val starPNat2 = thm "starPNat2";
   2.120 -val starPNat2_eq_iff = thm "starPNat2_eq_iff";
   2.121 -val starPNat2_eq_iff2 = thm "starPNat2_eq_iff2";
   2.122 -val hSuc_not_zero = thm "hSuc_not_zero";
   2.123 -val zero_not_hSuc = thms "zero_not_hSuc";
   2.124 -val hSuc_hSuc_eq = thm "hSuc_hSuc_eq";
   2.125 -val nonempty_nat_set_Least_mem = thm "nonempty_nat_set_Least_mem";
   2.126 -val nonempty_InternalNatSet_has_least = thm "nonempty_InternalNatSet_has_least";
   2.127 -val internal_induct = thm "internal_induct";
   2.128 -*}
   2.129 -
   2.130 -end
     3.1 --- a/src/HOL/Complex/README.html	Thu Apr 22 10:43:06 2004 +0200
     3.2 +++ b/src/HOL/Complex/README.html	Thu Apr 22 10:45:56 2004 +0200
     3.3 @@ -7,52 +7,52 @@
     3.4  with numeric constants and some complex analysis.  The development includes
     3.5  nonstandard analysis for the complex numbers.  Note that the image
     3.6  <KBD>HOL-Complex</KBD> includes theories from the directories 
     3.7 -<KBD><a href="#Anchor-Real">HOL/Real</a></KBD>  and <KBD><a href="#Anchor-Hyperreal">HOL/Hyperreal</a></KBD>. They define other types including <kbd>real</kbd> (the real numbers) and <kbd>hypreal</kbd> (the hyperreal or non-standard reals).<ul>
     3.8 -			<li><a href="CLim.html">CLim</a> Limits, continuous functions, and derivatives for the complex numbers
     3.9 -			<li><a href="CSeries.html">CSeries</a> Finite summation and infinite series for the complex numbers
    3.10 -			<li><a href="CStar.html">CStar</a> Star-transforms for the complex numbers, to form non-standard extensions of sets and functions
    3.11 -			<li><a href="Complex.html">Complex</a> The complex numbers
    3.12 -			<li><a href="NSCA.html">NSCA</a> Nonstandard complex analysis
    3.13 -			<li><a href="NSComplex.html">NSComplex</a> Ultrapower construction of the nonstandard complex numbers
    3.14 -			
    3.15 -			<li><a href="NSInduct.html">NSInduct</a> Nonstandard induction for the hypernatural numbers
    3.16 -		
    3.17 -			
    3.18 -		</ul>
    3.19 -		<h2><a name="Anchor-Real" id="Anchor-Real"></a>Real: Dedekind Cut Construction of the Real Line</h2>
    3.20 -		<ul>
    3.21 -			<li><a href="Lubs.html">Lubs</a> Definition of upper bounds, lubs and so on, to support completeness proofs.
    3.22 -			<li><a href="PReal.html">PReal</a> The positive reals constructed using Dedekind cuts
    3.23 -			<li><a href="Rational.html">Rational</a> The rational numbers constructed as equivalence classes of integers
    3.24 -			<li><a href="RComplete.html">RComplete</a> The reals are complete: they satisfy the supremum property. They also have the Archimedean property.
    3.25 -			<li><a href="RealDef.html">RealDef</a> The real numbers, their ordering properties, and embedding of the integers and the natural numbers
    3.26 -			<li><a href="RealPow.html">RealPow</a> Real numbers raised to natural number powers
    3.27 -		</ul>
    3.28 -		<h2><a name="Anchor-Hyperreal" id="Anchor-Hyperreal"></a>Hyperreal: Ultrafilter Construction of the Non-Standard Reals</h2>
    3.29 -		See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190.
    3.30 -		<ul>
    3.31 -			<li><a href="Filter.html">Filter</a> Theory of Filters and Ultrafilters. Main result is a version of the Ultrafilter Theorem proved using Zorn's Lemma.
    3.32 -			<li><a href="HLog.html">HLog</a> Non-standard logarithms
    3.33 -			<li><a href="HSeries.html">HSeries</a> Non-standard theory of finite summation and infinite series
    3.34 -			<li><a href="HTranscendental.html">HTranscendental</a> Non-standard extensions of transcendental functions
    3.35 -			<li><a href="HyperDef.html">HyperDef</a> Ultrapower construction of the hyperreals
    3.36 -			<li><a href="HyperNat.html">HyperNat</a> Ultrapower construction of the hypernaturals
    3.37 -			<li><a href="HyperPow.html">HyperPow</a> Powers theory for the hyperreals
    3.38 -			<li><a href="IntFloor.html">IntFloor</a> Floor and Ceiling functions relating the reals and integers
    3.39 -			<li><a href="Integration.html">Integration</a> Gage integrals
    3.40 -			<li><a href="Lim.html">Lim</a> Theory of limits, continuous functions, and derivatives
    3.41 -			<li><a href="Log.html">Log</a> Logarithms for the reals
    3.42 -			<li><a href="MacLaurin.html">MacLaurin</a> MacLaurin series
    3.43 -			<li><a href="NatStar.html">NatStar</a> Star-transforms for the hypernaturals, to form non-standard extensions of sets and functions involving the naturals or reals
    3.44 -			<li><a href="NthRoot.html">NthRoot</a> Existence of n-th roots of real numbers
    3.45 -			<li><a href="NSA.html">NSA</a> Theory defining sets of infinite numbers, infinitesimals, the infinitely close relation, and their various algebraic properties.
    3.46 -			<li><a href="Poly.html">Poly</a> Univariate real polynomials
    3.47 -			<li><a href="SEQ.html">SEQ</a> Convergence of sequences and series using standard and nonstandard analysis
    3.48 -			<li><a href="Series.html">Series</a> Finite summation and infinite series for the reals
    3.49 -			<li><a href="Star.html">Star</a> Nonstandard extensions of real sets and real functions
    3.50 -			<li><a href="Transcendental.html">Transcendental</a> Power series and transcendental functions
    3.51 -		</ul>
    3.52 -		<HR>
    3.53 -		<P>Last modified $Date$
    3.54 +<KBD><a href="#Anchor-Real">HOL/Real</a></KBD>  and <KBD><a href="#Anchor-Hyperreal">HOL/Hyperreal</a></KBD>. They define other types including <kbd>real</kbd> (the real numbers) and <kbd>hypreal</kbd> (the hyperreal or non-standard reals).
    3.55 +
    3.56 +<ul>
    3.57 +<li><a href="CLim.html">CLim</a> Limits, continuous functions, and derivatives for the complex numbers
    3.58 +<li><a href="CSeries.html">CSeries</a> Finite summation and infinite series for the complex numbers
    3.59 +<li><a href="CStar.html">CStar</a> Star-transforms for the complex numbers, to form non-standard extensions of sets and functions
    3.60 +<li><a href="Complex.html">Complex</a> The complex numbers
    3.61 +<li><a href="NSCA.html">NSCA</a> Nonstandard complex analysis
    3.62 +<li><a href="NSComplex.html">NSComplex</a> Ultrapower construction of the nonstandard complex numbers
    3.63 +</ul>
    3.64 +
    3.65 +<h2><a name="Anchor-Real" id="Anchor-Real"></a>Real: Dedekind Cut Construction of the Real Line</h2>
    3.66 +
    3.67 +<ul>
    3.68 +<li><a href="Lubs.html">Lubs</a> Definition of upper bounds, lubs and so on, to support completeness proofs.
    3.69 +<li><a href="PReal.html">PReal</a> The positive reals constructed using Dedekind cuts
    3.70 +<li><a href="Rational.html">Rational</a> The rational numbers constructed as equivalence classes of integers
    3.71 +<li><a href="RComplete.html">RComplete</a> The reals are complete: they satisfy the supremum property. They also have the Archimedean property.
    3.72 +<li><a href="RealDef.html">RealDef</a> The real numbers, their ordering properties, and embedding of the integers and the natural numbers
    3.73 +<li><a href="RealPow.html">RealPow</a> Real numbers raised to natural number powers
    3.74 +</ul>
    3.75 +<h2><a name="Anchor-Hyperreal" id="Anchor-Hyperreal"></a>Hyperreal: Ultrafilter Construction of the Non-Standard Reals</h2>
    3.76 +See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190.
    3.77 +<ul>
    3.78 +<li><a href="Filter.html">Filter</a> Theory of Filters and Ultrafilters. Main result is a version of the Ultrafilter Theorem proved using Zorn's Lemma.
    3.79 +<li><a href="HLog.html">HLog</a> Non-standard logarithms
    3.80 +<li><a href="HSeries.html">HSeries</a> Non-standard theory of finite summation and infinite series
    3.81 +<li><a href="HTranscendental.html">HTranscendental</a> Non-standard extensions of transcendental functions
    3.82 +<li><a href="HyperDef.html">HyperDef</a> Ultrapower construction of the hyperreals
    3.83 +<li><a href="HyperNat.html">HyperNat</a> Ultrapower construction of the hypernaturals
    3.84 +<li><a href="HyperPow.html">HyperPow</a> Powers theory for the hyperreals
    3.85 +<li><a href="IntFloor.html">IntFloor</a> Floor and Ceiling functions relating the reals and integers
    3.86 +<li><a href="Integration.html">Integration</a> Gage integrals
    3.87 +<li><a href="Lim.html">Lim</a> Theory of limits, continuous functions, and derivatives
    3.88 +<li><a href="Log.html">Log</a> Logarithms for the reals
    3.89 +<li><a href="MacLaurin.html">MacLaurin</a> MacLaurin series
    3.90 +<li><a href="NatStar.html">NatStar</a> Star-transforms for the hypernaturals, to form non-standard extensions of sets and functions involving the naturals or reals
    3.91 +<li><a href="NthRoot.html">NthRoot</a> Existence of n-th roots of real numbers
    3.92 +<li><a href="NSA.html">NSA</a> Theory defining sets of infinite numbers, infinitesimals, the infinitely close relation, and their various algebraic properties.
    3.93 +<li><a href="Poly.html">Poly</a> Univariate real polynomials
    3.94 +<li><a href="SEQ.html">SEQ</a> Convergence of sequences and series using standard and nonstandard analysis
    3.95 +<li><a href="Series.html">Series</a> Finite summation and infinite series for the reals
    3.96 +<li><a href="Star.html">Star</a> Nonstandard extensions of real sets and real functions
    3.97 +<li><a href="Transcendental.html">Transcendental</a> Power series and transcendental functions
    3.98 +</ul>
    3.99 +<HR>
   3.100 +<P>Last modified $Date$
   3.101  
   3.102  </HTML>
     4.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Thu Apr 22 10:43:06 2004 +0200
     4.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Thu Apr 22 10:45:56 2004 +0200
     4.3 @@ -7,7 +7,7 @@
     4.4  
     4.5  header{*Nonstandard Extensions of Transcendental Functions*}
     4.6  
     4.7 -theory HTranscendental = Transcendental + IntFloor:
     4.8 +theory HTranscendental = Transcendental + Integration:
     4.9  
    4.10  constdefs
    4.11  
     5.1 --- a/src/HOL/Hyperreal/IntFloor.thy	Thu Apr 22 10:43:06 2004 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,322 +0,0 @@
     5.4 -(*  Title:       IntFloor.thy
     5.5 -    Author:      Jacques D. Fleuriot
     5.6 -    Copyright:   2001,2002  University of Edinburgh
     5.7 -Converted to Isar and polished by lcp
     5.8 -*)
     5.9 -
    5.10 -header{*Floor and Ceiling Functions from the Reals to the Integers*}
    5.11 -
    5.12 -theory IntFloor = Integration:
    5.13 -
    5.14 -constdefs
    5.15 -
    5.16 -  floor :: "real => int"
    5.17 -   "floor r == (LEAST n. r < real (n + (1::int)))"
    5.18 -
    5.19 -  ceiling :: "real => int"
    5.20 -    "ceiling r == - floor (- r)"
    5.21 -
    5.22 -syntax (xsymbols)
    5.23 -  floor :: "real => int"     ("\<lfloor>_\<rfloor>")
    5.24 -  ceiling :: "real => int"   ("\<lceil>_\<rceil>")
    5.25 -
    5.26 -syntax (HTML output)
    5.27 -  floor :: "real => int"     ("\<lfloor>_\<rfloor>")
    5.28 -  ceiling :: "real => int"   ("\<lceil>_\<rceil>")
    5.29 -
    5.30 -
    5.31 -lemma number_of_less_real_of_int_iff [simp]:
    5.32 -     "((number_of n) < real (m::int)) = (number_of n < m)"
    5.33 -apply auto
    5.34 -apply (rule real_of_int_less_iff [THEN iffD1])
    5.35 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
    5.36 -done
    5.37 -
    5.38 -lemma number_of_less_real_of_int_iff2 [simp]:
    5.39 -     "(real (m::int) < (number_of n)) = (m < number_of n)"
    5.40 -apply auto
    5.41 -apply (rule real_of_int_less_iff [THEN iffD1])
    5.42 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
    5.43 -done
    5.44 -
    5.45 -lemma number_of_le_real_of_int_iff [simp]:
    5.46 -     "((number_of n) \<le> real (m::int)) = (number_of n \<le> m)"
    5.47 -by (simp add: linorder_not_less [symmetric])
    5.48 -
    5.49 -lemma number_of_le_real_of_int_iff2 [simp]:
    5.50 -     "(real (m::int) \<le> (number_of n)) = (m \<le> number_of n)"
    5.51 -by (simp add: linorder_not_less [symmetric])
    5.52 -
    5.53 -lemma floor_zero [simp]: "floor 0 = 0"
    5.54 -apply (simp add: floor_def)
    5.55 -apply (rule Least_equality, auto)
    5.56 -done
    5.57 -
    5.58 -lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0"
    5.59 -by auto
    5.60 -
    5.61 -lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
    5.62 -apply (simp only: floor_def)
    5.63 -apply (rule Least_equality)
    5.64 -apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    5.65 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
    5.66 -apply (simp_all add: real_of_int_real_of_nat)
    5.67 -done
    5.68 -
    5.69 -lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
    5.70 -apply (simp only: floor_def)
    5.71 -apply (rule Least_equality)
    5.72 -apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    5.73 -apply (drule_tac [2] real_of_int_minus [THEN subst])
    5.74 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
    5.75 -apply (simp_all add: real_of_int_real_of_nat)
    5.76 -done
    5.77 -
    5.78 -lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
    5.79 -apply (simp only: floor_def)
    5.80 -apply (rule Least_equality)
    5.81 -apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    5.82 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto)
    5.83 -done
    5.84 -
    5.85 -lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
    5.86 -apply (simp only: floor_def)
    5.87 -apply (rule Least_equality)
    5.88 -apply (drule_tac [2] real_of_int_minus [THEN subst])
    5.89 -apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    5.90 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto)
    5.91 -done
    5.92 -
    5.93 -lemma reals_Archimedean6:
    5.94 -     "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)"
    5.95 -apply (insert reals_Archimedean2 [of r], safe)
    5.96 -apply (frule_tac P = "%k. r < real k" and k = n and m = "%x. x"
    5.97 -       in ex_has_least_nat, auto)
    5.98 -apply (rule_tac x = x in exI)
    5.99 -apply (case_tac x, simp)
   5.100 -apply (rename_tac x')
   5.101 -apply (drule_tac x = x' in spec, simp)
   5.102 -done
   5.103 -
   5.104 -lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"
   5.105 -by (drule reals_Archimedean6, auto)
   5.106 -
   5.107 -lemma reals_Archimedean_6b_int:
   5.108 -     "0 \<le> r ==> \<exists>n. real n \<le> r & r < real ((n::int) + 1)"
   5.109 -apply (drule reals_Archimedean6a, auto)
   5.110 -apply (rule_tac x = "int n" in exI)
   5.111 -apply (simp add: real_of_int_real_of_nat real_of_nat_Suc)
   5.112 -done
   5.113 -
   5.114 -lemma reals_Archimedean_6c_int:
   5.115 -     "r < 0 ==> \<exists>n. real n \<le> r & r < real ((n::int) + 1)"
   5.116 -apply (rule reals_Archimedean_6b_int [of "-r", THEN exE], simp, auto)
   5.117 -apply (rename_tac n)
   5.118 -apply (drule real_le_imp_less_or_eq, auto)
   5.119 -apply (rule_tac x = "- n - 1" in exI)
   5.120 -apply (rule_tac [2] x = "- n" in exI, auto)
   5.121 -done
   5.122 -
   5.123 -lemma real_lb_ub_int: " \<exists>(n::int). real n \<le> r & r < real ((n::int) + 1)"
   5.124 -apply (case_tac "r < 0")
   5.125 -apply (blast intro: reals_Archimedean_6c_int)
   5.126 -apply (simp only: linorder_not_less)
   5.127 -apply (blast intro: reals_Archimedean_6b_int reals_Archimedean_6c_int)
   5.128 -done
   5.129 -
   5.130 -lemma lemma_floor:
   5.131 -  assumes a1: "real m \<le> r" and a2: "r < real n + 1"
   5.132 -  shows "m \<le> (n::int)"
   5.133 -proof -
   5.134 -  have "real m < real n + 1" by (rule order_le_less_trans)
   5.135 -  also have "... = real(n+1)" by simp
   5.136 -  finally have "m < n+1" by (simp only: real_of_int_less_iff)
   5.137 -  thus ?thesis by arith
   5.138 -qed
   5.139 -
   5.140 -lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
   5.141 -apply (simp add: floor_def Least_def)
   5.142 -apply (insert real_lb_ub_int [of r], safe)
   5.143 -apply (rule theI2, auto)
   5.144 -done
   5.145 -
   5.146 -lemma floor_le: "x < y ==> floor x \<le> floor y"
   5.147 -apply (simp add: floor_def Least_def)
   5.148 -apply (insert real_lb_ub_int [of x])
   5.149 -apply (insert real_lb_ub_int [of y], safe)
   5.150 -apply (rule theI2)
   5.151 -apply (rule_tac [3] theI2, auto)
   5.152 -done
   5.153 -
   5.154 -lemma floor_le2: "x \<le> y ==> floor x \<le> floor y"
   5.155 -by (auto dest: real_le_imp_less_or_eq simp add: floor_le)
   5.156 -
   5.157 -lemma lemma_floor2: "real na < real (x::int) + 1 ==> na \<le> x"
   5.158 -by (auto intro: lemma_floor)
   5.159 -
   5.160 -lemma real_of_int_floor_cancel [simp]:
   5.161 -    "(real (floor x) = x) = (\<exists>n::int. x = real n)"
   5.162 -apply (simp add: floor_def Least_def)
   5.163 -apply (insert real_lb_ub_int [of x], erule exE)
   5.164 -apply (rule theI2)
   5.165 -apply (auto intro: lemma_floor)
   5.166 -done
   5.167 -
   5.168 -lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
   5.169 -apply (simp add: floor_def)
   5.170 -apply (rule Least_equality)
   5.171 -apply (auto intro: lemma_floor)
   5.172 -done
   5.173 -
   5.174 -lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n"
   5.175 -apply (simp add: floor_def)
   5.176 -apply (rule Least_equality)
   5.177 -apply (auto intro: lemma_floor)
   5.178 -done
   5.179 -
   5.180 -lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
   5.181 -apply (rule inj_int [THEN injD])
   5.182 -apply (simp add: real_of_nat_Suc)
   5.183 -apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "of_nat n"])
   5.184 -done
   5.185 -
   5.186 -lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
   5.187 -apply (drule order_le_imp_less_or_eq)
   5.188 -apply (auto intro: floor_eq3)
   5.189 -done
   5.190 -
   5.191 -lemma floor_number_of_eq [simp]:
   5.192 -     "floor(number_of n :: real) = (number_of n :: int)"
   5.193 -apply (subst real_number_of [symmetric])
   5.194 -apply (rule floor_real_of_int)
   5.195 -done
   5.196 -
   5.197 -lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
   5.198 -apply (simp add: floor_def Least_def)
   5.199 -apply (insert real_lb_ub_int [of r], safe)
   5.200 -apply (rule theI2)
   5.201 -apply (auto intro: lemma_floor)
   5.202 -done
   5.203 -
   5.204 -lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
   5.205 -apply (insert real_of_int_floor_ge_diff_one [of r])
   5.206 -apply (auto simp del: real_of_int_floor_ge_diff_one)
   5.207 -done
   5.208 -
   5.209 -
   5.210 -subsection{*Ceiling Function for Positive Reals*}
   5.211 -
   5.212 -lemma ceiling_zero [simp]: "ceiling 0 = 0"
   5.213 -by (simp add: ceiling_def)
   5.214 -
   5.215 -lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
   5.216 -by (simp add: ceiling_def)
   5.217 -
   5.218 -lemma ceiling_real_of_nat_zero [simp]: "ceiling (real (0::nat)) = 0"
   5.219 -by auto
   5.220 -
   5.221 -lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r"
   5.222 -by (simp add: ceiling_def)
   5.223 -
   5.224 -lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r"
   5.225 -by (simp add: ceiling_def)
   5.226 -
   5.227 -lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
   5.228 -apply (simp add: ceiling_def)
   5.229 -apply (subst le_minus_iff, simp)
   5.230 -done
   5.231 -
   5.232 -lemma ceiling_le: "x < y ==> ceiling x \<le> ceiling y"
   5.233 -by (simp add: floor_le ceiling_def)
   5.234 -
   5.235 -lemma ceiling_le2: "x \<le> y ==> ceiling x \<le> ceiling y"
   5.236 -by (simp add: floor_le2 ceiling_def)
   5.237 -
   5.238 -lemma real_of_int_ceiling_cancel [simp]:
   5.239 -     "(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
   5.240 -apply (auto simp add: ceiling_def)
   5.241 -apply (drule arg_cong [where f = uminus], auto)
   5.242 -apply (rule_tac x = "-n" in exI, auto)
   5.243 -done
   5.244 -
   5.245 -lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1"
   5.246 -apply (simp add: ceiling_def)
   5.247 -apply (rule minus_equation_iff [THEN iffD1])
   5.248 -apply (simp add: floor_eq [where n = "-(n+1)"])
   5.249 -done
   5.250 -
   5.251 -lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1"
   5.252 -by (simp add: ceiling_def floor_eq2 [where n = "-(n+1)"])
   5.253 -
   5.254 -lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n  |] ==> ceiling x = n"
   5.255 -by (simp add: ceiling_def floor_eq2 [where n = "-n"])
   5.256 -
   5.257 -lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
   5.258 -by (simp add: ceiling_def)
   5.259 -
   5.260 -lemma ceiling_number_of_eq [simp]:
   5.261 -     "ceiling (number_of n :: real) = (number_of n)"
   5.262 -apply (subst real_number_of [symmetric])
   5.263 -apply (rule ceiling_real_of_int)
   5.264 -done
   5.265 -
   5.266 -lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
   5.267 -apply (rule neg_le_iff_le [THEN iffD1])
   5.268 -apply (simp add: ceiling_def diff_minus)
   5.269 -done
   5.270 -
   5.271 -lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1"
   5.272 -apply (insert real_of_int_ceiling_diff_one_le [of r])
   5.273 -apply (simp del: real_of_int_ceiling_diff_one_le)
   5.274 -done
   5.275 -
   5.276 -ML
   5.277 -{*
   5.278 -val number_of_less_real_of_int_iff = thm "number_of_less_real_of_int_iff";
   5.279 -val number_of_less_real_of_int_iff2 = thm "number_of_less_real_of_int_iff2";
   5.280 -val number_of_le_real_of_int_iff = thm "number_of_le_real_of_int_iff";
   5.281 -val number_of_le_real_of_int_iff2 = thm "number_of_le_real_of_int_iff2";
   5.282 -val floor_zero = thm "floor_zero";
   5.283 -val floor_real_of_nat_zero = thm "floor_real_of_nat_zero";
   5.284 -val floor_real_of_nat = thm "floor_real_of_nat";
   5.285 -val floor_minus_real_of_nat = thm "floor_minus_real_of_nat";
   5.286 -val floor_real_of_int = thm "floor_real_of_int";
   5.287 -val floor_minus_real_of_int = thm "floor_minus_real_of_int";
   5.288 -val reals_Archimedean6 = thm "reals_Archimedean6";
   5.289 -val reals_Archimedean6a = thm "reals_Archimedean6a";
   5.290 -val reals_Archimedean_6b_int = thm "reals_Archimedean_6b_int";
   5.291 -val reals_Archimedean_6c_int = thm "reals_Archimedean_6c_int";
   5.292 -val real_lb_ub_int = thm "real_lb_ub_int";
   5.293 -val lemma_floor = thm "lemma_floor";
   5.294 -val real_of_int_floor_le = thm "real_of_int_floor_le";
   5.295 -val floor_le = thm "floor_le";
   5.296 -val floor_le2 = thm "floor_le2";
   5.297 -val lemma_floor2 = thm "lemma_floor2";
   5.298 -val real_of_int_floor_cancel = thm "real_of_int_floor_cancel";
   5.299 -val floor_eq = thm "floor_eq";
   5.300 -val floor_eq2 = thm "floor_eq2";
   5.301 -val floor_eq3 = thm "floor_eq3";
   5.302 -val floor_eq4 = thm "floor_eq4";
   5.303 -val floor_number_of_eq = thm "floor_number_of_eq";
   5.304 -val real_of_int_floor_ge_diff_one = thm "real_of_int_floor_ge_diff_one";
   5.305 -val real_of_int_floor_add_one_ge = thm "real_of_int_floor_add_one_ge";
   5.306 -val ceiling_zero = thm "ceiling_zero";
   5.307 -val ceiling_real_of_nat = thm "ceiling_real_of_nat";
   5.308 -val ceiling_real_of_nat_zero = thm "ceiling_real_of_nat_zero";
   5.309 -val ceiling_floor = thm "ceiling_floor";
   5.310 -val floor_ceiling = thm "floor_ceiling";
   5.311 -val real_of_int_ceiling_ge = thm "real_of_int_ceiling_ge";
   5.312 -val ceiling_le = thm "ceiling_le";
   5.313 -val ceiling_le2 = thm "ceiling_le2";
   5.314 -val real_of_int_ceiling_cancel = thm "real_of_int_ceiling_cancel";
   5.315 -val ceiling_eq = thm "ceiling_eq";
   5.316 -val ceiling_eq2 = thm "ceiling_eq2";
   5.317 -val ceiling_eq3 = thm "ceiling_eq3";
   5.318 -val ceiling_real_of_int = thm "ceiling_real_of_int";
   5.319 -val ceiling_number_of_eq = thm "ceiling_number_of_eq";
   5.320 -val real_of_int_ceiling_diff_one_le = thm "real_of_int_ceiling_diff_one_le";
   5.321 -val real_of_int_ceiling_le_add_one = thm "real_of_int_ceiling_le_add_one";
   5.322 -*}
   5.323 -
   5.324 -
   5.325 -end
     6.1 --- a/src/HOL/Hyperreal/NatStar.thy	Thu Apr 22 10:43:06 2004 +0200
     6.2 +++ b/src/HOL/Hyperreal/NatStar.thy	Thu Apr 22 10:45:56 2004 +0200
     6.3 @@ -533,6 +533,112 @@
     6.4  val starfunNat_inverse_real_of_nat_Infinitesimal = thm "starfunNat_inverse_real_of_nat_Infinitesimal";
     6.5  *}
     6.6  
     6.7 +
     6.8 +
     6.9 +subsection{*Nonstandard Characterization of Induction*}
    6.10 +
    6.11 +constdefs
    6.12 +
    6.13 +  starPNat :: "(nat => bool) => hypnat => bool"  ("*pNat* _" [80] 80)
    6.14 +  "*pNat* P == (%x. \<exists>X. (X \<in> Rep_hypnat(x) &
    6.15 +                      {n. P(X n)} \<in> FreeUltrafilterNat))"
    6.16 +
    6.17 +
    6.18 +  starPNat2 :: "(nat => nat => bool) => hypnat =>hypnat => bool"
    6.19 +               ("*pNat2* _" [80] 80)
    6.20 +  "*pNat2* P == (%x y. \<exists>X. \<exists>Y. (X \<in> Rep_hypnat(x) & Y \<in> Rep_hypnat(y) &
    6.21 +                      {n. P(X n) (Y n)} \<in> FreeUltrafilterNat))"
    6.22 +
    6.23 +  hSuc :: "hypnat => hypnat"
    6.24 +  "hSuc n == n + 1"
    6.25 +
    6.26 +
    6.27 +lemma starPNat:
    6.28 +     "(( *pNat* P) (Abs_hypnat(hypnatrel``{%n. X n}))) =
    6.29 +      ({n. P (X n)} \<in> FreeUltrafilterNat)"
    6.30 +by (auto simp add: starPNat_def, ultra)
    6.31 +
    6.32 +lemma starPNat_hypnat_of_nat [simp]: "( *pNat* P) (hypnat_of_nat n) = P n"
    6.33 +by (auto simp add: starPNat hypnat_of_nat_eq)
    6.34 +
    6.35 +lemma hypnat_induct_obj:
    6.36 +    "(( *pNat* P) 0 &
    6.37 +            (\<forall>n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1)))
    6.38 +       --> ( *pNat* P)(n)"
    6.39 +apply (cases n)
    6.40 +apply (auto simp add: hypnat_zero_def hypnat_one_def starPNat, ultra)
    6.41 +apply (erule nat_induct)
    6.42 +apply (drule_tac x = "hypnat_of_nat n" in spec)
    6.43 +apply (rule ccontr)
    6.44 +apply (auto simp add: starPNat hypnat_of_nat_eq hypnat_add)
    6.45 +done
    6.46 +
    6.47 +lemma hypnat_induct:
    6.48 +  "[| ( *pNat* P) 0;
    6.49 +      !!n. ( *pNat* P)(n) ==> ( *pNat* P)(n + 1)|]
    6.50 +     ==> ( *pNat* P)(n)"
    6.51 +by (insert hypnat_induct_obj [of P n], auto)
    6.52 +
    6.53 +lemma starPNat2:
    6.54 +"(( *pNat2* P) (Abs_hypnat(hypnatrel``{%n. X n}))
    6.55 +             (Abs_hypnat(hypnatrel``{%n. Y n}))) =
    6.56 +      ({n. P (X n) (Y n)} \<in> FreeUltrafilterNat)"
    6.57 +by (auto simp add: starPNat2_def, ultra)
    6.58 +
    6.59 +lemma starPNat2_eq_iff: "( *pNat2* (op =)) = (op =)"
    6.60 +apply (simp add: starPNat2_def)
    6.61 +apply (rule ext)
    6.62 +apply (rule ext)
    6.63 +apply (rule_tac z = x in eq_Abs_hypnat)
    6.64 +apply (rule_tac z = y in eq_Abs_hypnat)
    6.65 +apply (auto, ultra)
    6.66 +done
    6.67 +
    6.68 +lemma starPNat2_eq_iff2: "( *pNat2* (%x y. x = y)) X Y = (X = Y)"
    6.69 +by (simp add: starPNat2_eq_iff)
    6.70 +
    6.71 +lemma lemma_hyp: "(\<exists>h. P(h::hypnat)) = (\<exists>x. P(Abs_hypnat(hypnatrel `` {x})))"
    6.72 +apply auto
    6.73 +apply (rule_tac z = h in eq_Abs_hypnat, auto)
    6.74 +done
    6.75 +
    6.76 +lemma hSuc_not_zero [iff]: "hSuc m \<noteq> 0"
    6.77 +by (simp add: hSuc_def)
    6.78 +
    6.79 +lemmas zero_not_hSuc = hSuc_not_zero [THEN not_sym, standard, iff]
    6.80 +
    6.81 +lemma hSuc_hSuc_eq [iff]: "(hSuc m = hSuc n) = (m = n)"
    6.82 +by (simp add: hSuc_def hypnat_one_def)
    6.83 +
    6.84 +lemma nonempty_nat_set_Least_mem: "c \<in> (S :: nat set) ==> (LEAST n. n  \<in> S)  \<in> S"
    6.85 +by (erule LeastI)
    6.86 +
    6.87 +lemma nonempty_InternalNatSet_has_least:
    6.88 +    "[| S \<in> InternalNatSets; S \<noteq> {} |] ==> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m"
    6.89 +apply (auto simp add: InternalNatSets_def starsetNat_n_def lemma_hyp)
    6.90 +apply (rule_tac z = x in eq_Abs_hypnat)
    6.91 +apply (auto dest!: bspec simp add: hypnat_le)
    6.92 +apply (drule_tac x = "%m. LEAST n. n \<in> As m" in spec, auto)
    6.93 +apply (ultra, force dest: nonempty_nat_set_Least_mem)
    6.94 +apply (drule_tac x = x in bspec, auto)
    6.95 +apply (ultra, auto intro: Least_le)
    6.96 +done
    6.97 +
    6.98 +text{* Goldblatt page 129 Thm 11.3.2*}
    6.99 +lemma internal_induct:
   6.100 +     "[| X \<in> InternalNatSets; 0 \<in> X; \<forall>n. n \<in> X --> n + 1 \<in> X |]
   6.101 +      ==> X = (UNIV:: hypnat set)"
   6.102 +apply (rule ccontr)
   6.103 +apply (frule InternalNatSets_Compl)
   6.104 +apply (drule_tac S = "- X" in nonempty_InternalNatSet_has_least, auto)
   6.105 +apply (subgoal_tac "1 \<le> n")
   6.106 +apply (drule_tac x = "n - 1" in bspec, safe)
   6.107 +apply (drule_tac x = "n - 1" in spec)
   6.108 +apply (drule_tac [2] c = 1 and a = n in add_right_mono)
   6.109 +apply (auto simp add: linorder_not_less [symmetric] iff del: hypnat_neq0_conv)
   6.110 +done
   6.111 +
   6.112 +
   6.113  end
   6.114  
   6.115  
     7.1 --- a/src/HOL/IsaMakefile	Thu Apr 22 10:43:06 2004 +0200
     7.2 +++ b/src/HOL/IsaMakefile	Thu Apr 22 10:45:56 2004 +0200
     7.3 @@ -150,7 +150,7 @@
     7.4    Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HSeries.thy\
     7.5    Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy\
     7.6    Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\
     7.7 -  Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy Hyperreal/IntFloor.thy\
     7.8 +  Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
     7.9    Hyperreal/Lim.thy Hyperreal/Log.thy\
    7.10    Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy\
    7.11    Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy\
    7.12 @@ -159,7 +159,7 @@
    7.13    Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
    7.14    Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy\
    7.15    Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy\
    7.16 -  Complex/NSCA.thy Complex/NSComplex.thy Complex/NSInduct.thy
    7.17 +  Complex/NSCA.thy Complex/NSComplex.thy
    7.18  	@cd Complex; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Complex
    7.19  
    7.20  
     8.1 --- a/src/HOL/Real/RComplete.thy	Thu Apr 22 10:43:06 2004 +0200
     8.2 +++ b/src/HOL/Real/RComplete.thy	Thu Apr 22 10:45:56 2004 +0200
     8.3 @@ -2,11 +2,11 @@
     8.4      ID          : $Id$
     8.5      Author      : Jacques D. Fleuriot
     8.6      Copyright   : 1998  University of Cambridge
     8.7 -    Description : Completeness theorems for positive
     8.8 -                  reals and reals 
     8.9 +    Copyright   : 2001,2002  University of Edinburgh
    8.10 +Converted to Isar and polished by lcp
    8.11  *) 
    8.12  
    8.13 -header{*Completeness Theorems for Positive Reals and Reals.*}
    8.14 +header{*Completeness of the Reals; Floor and Ceiling Functions*}
    8.15  
    8.16  theory RComplete = Lubs + RealDef:
    8.17  
    8.18 @@ -215,7 +215,322 @@
    8.19  val reals_Archimedean3 = thm "reals_Archimedean3";
    8.20  *}
    8.21  
    8.22 +
    8.23 +subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
    8.24 +
    8.25 +constdefs
    8.26 +
    8.27 +  floor :: "real => int"
    8.28 +   "floor r == (LEAST n::int. r < real (n+1))"
    8.29 +
    8.30 +  ceiling :: "real => int"
    8.31 +    "ceiling r == - floor (- r)"
    8.32 +
    8.33 +syntax (xsymbols)
    8.34 +  floor :: "real => int"     ("\<lfloor>_\<rfloor>")
    8.35 +  ceiling :: "real => int"   ("\<lceil>_\<rceil>")
    8.36 +
    8.37 +syntax (HTML output)
    8.38 +  floor :: "real => int"     ("\<lfloor>_\<rfloor>")
    8.39 +  ceiling :: "real => int"   ("\<lceil>_\<rceil>")
    8.40 +
    8.41 +
    8.42 +lemma number_of_less_real_of_int_iff [simp]:
    8.43 +     "((number_of n) < real (m::int)) = (number_of n < m)"
    8.44 +apply auto
    8.45 +apply (rule real_of_int_less_iff [THEN iffD1])
    8.46 +apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
    8.47 +done
    8.48 +
    8.49 +lemma number_of_less_real_of_int_iff2 [simp]:
    8.50 +     "(real (m::int) < (number_of n)) = (m < number_of n)"
    8.51 +apply auto
    8.52 +apply (rule real_of_int_less_iff [THEN iffD1])
    8.53 +apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
    8.54 +done
    8.55 +
    8.56 +lemma number_of_le_real_of_int_iff [simp]:
    8.57 +     "((number_of n) \<le> real (m::int)) = (number_of n \<le> m)"
    8.58 +by (simp add: linorder_not_less [symmetric])
    8.59 +
    8.60 +lemma number_of_le_real_of_int_iff2 [simp]:
    8.61 +     "(real (m::int) \<le> (number_of n)) = (m \<le> number_of n)"
    8.62 +by (simp add: linorder_not_less [symmetric])
    8.63 +
    8.64 +lemma floor_zero [simp]: "floor 0 = 0"
    8.65 +apply (simp add: floor_def)
    8.66 +apply (rule Least_equality, auto)
    8.67 +done
    8.68 +
    8.69 +lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0"
    8.70 +by auto
    8.71 +
    8.72 +lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
    8.73 +apply (simp only: floor_def)
    8.74 +apply (rule Least_equality)
    8.75 +apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    8.76 +apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
    8.77 +apply (simp_all add: real_of_int_real_of_nat)
    8.78 +done
    8.79 +
    8.80 +lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
    8.81 +apply (simp only: floor_def)
    8.82 +apply (rule Least_equality)
    8.83 +apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    8.84 +apply (drule_tac [2] real_of_int_minus [THEN subst])
    8.85 +apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
    8.86 +apply (simp_all add: real_of_int_real_of_nat)
    8.87 +done
    8.88 +
    8.89 +lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
    8.90 +apply (simp only: floor_def)
    8.91 +apply (rule Least_equality)
    8.92 +apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    8.93 +apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto)
    8.94 +done
    8.95 +
    8.96 +lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
    8.97 +apply (simp only: floor_def)
    8.98 +apply (rule Least_equality)
    8.99 +apply (drule_tac [2] real_of_int_minus [THEN subst])
   8.100 +apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
   8.101 +apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto)
   8.102 +done
   8.103 +
   8.104 +lemma reals_Archimedean6:
   8.105 +     "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)"
   8.106 +apply (insert reals_Archimedean2 [of r], safe)
   8.107 +apply (frule_tac P = "%k. r < real k" and k = n and m = "%x. x"
   8.108 +       in ex_has_least_nat, auto)
   8.109 +apply (rule_tac x = x in exI)
   8.110 +apply (case_tac x, simp)
   8.111 +apply (rename_tac x')
   8.112 +apply (drule_tac x = x' in spec, simp)
   8.113 +done
   8.114 +
   8.115 +lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"
   8.116 +by (drule reals_Archimedean6, auto)
   8.117 +
   8.118 +lemma reals_Archimedean_6b_int:
   8.119 +     "0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
   8.120 +apply (drule reals_Archimedean6a, auto)
   8.121 +apply (rule_tac x = "int n" in exI)
   8.122 +apply (simp add: real_of_int_real_of_nat real_of_nat_Suc)
   8.123 +done
   8.124 +
   8.125 +lemma reals_Archimedean_6c_int:
   8.126 +     "r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
   8.127 +apply (rule reals_Archimedean_6b_int [of "-r", THEN exE], simp, auto)
   8.128 +apply (rename_tac n)
   8.129 +apply (drule real_le_imp_less_or_eq, auto)
   8.130 +apply (rule_tac x = "- n - 1" in exI)
   8.131 +apply (rule_tac [2] x = "- n" in exI, auto)
   8.132 +done
   8.133 +
   8.134 +lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
   8.135 +apply (case_tac "r < 0")
   8.136 +apply (blast intro: reals_Archimedean_6c_int)
   8.137 +apply (simp only: linorder_not_less)
   8.138 +apply (blast intro: reals_Archimedean_6b_int reals_Archimedean_6c_int)
   8.139 +done
   8.140 +
   8.141 +lemma lemma_floor:
   8.142 +  assumes a1: "real m \<le> r" and a2: "r < real n + 1"
   8.143 +  shows "m \<le> (n::int)"
   8.144 +proof -
   8.145 +  have "real m < real n + 1" by (rule order_le_less_trans)
   8.146 +  also have "... = real(n+1)" by simp
   8.147 +  finally have "m < n+1" by (simp only: real_of_int_less_iff)
   8.148 +  thus ?thesis by arith
   8.149 +qed
   8.150 +
   8.151 +lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
   8.152 +apply (simp add: floor_def Least_def)
   8.153 +apply (insert real_lb_ub_int [of r], safe)
   8.154 +apply (rule theI2, auto)
   8.155 +done
   8.156 +
   8.157 +lemma floor_le: "x < y ==> floor x \<le> floor y"
   8.158 +apply (simp add: floor_def Least_def)
   8.159 +apply (insert real_lb_ub_int [of x])
   8.160 +apply (insert real_lb_ub_int [of y], safe)
   8.161 +apply (rule theI2)
   8.162 +apply (rule_tac [3] theI2, auto)
   8.163 +done
   8.164 +
   8.165 +lemma floor_le2: "x \<le> y ==> floor x \<le> floor y"
   8.166 +by (auto dest: real_le_imp_less_or_eq simp add: floor_le)
   8.167 +
   8.168 +lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
   8.169 +by (auto intro: lemma_floor)
   8.170 +
   8.171 +lemma real_of_int_floor_cancel [simp]:
   8.172 +    "(real (floor x) = x) = (\<exists>n::int. x = real n)"
   8.173 +apply (simp add: floor_def Least_def)
   8.174 +apply (insert real_lb_ub_int [of x], erule exE)
   8.175 +apply (rule theI2)
   8.176 +apply (auto intro: lemma_floor)
   8.177 +done
   8.178 +
   8.179 +lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
   8.180 +apply (simp add: floor_def)
   8.181 +apply (rule Least_equality)
   8.182 +apply (auto intro: lemma_floor)
   8.183 +done
   8.184 +
   8.185 +lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n"
   8.186 +apply (simp add: floor_def)
   8.187 +apply (rule Least_equality)
   8.188 +apply (auto intro: lemma_floor)
   8.189 +done
   8.190 +
   8.191 +lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
   8.192 +apply (rule inj_int [THEN injD])
   8.193 +apply (simp add: real_of_nat_Suc)
   8.194 +apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "of_nat n"])
   8.195 +done
   8.196 +
   8.197 +lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
   8.198 +apply (drule order_le_imp_less_or_eq)
   8.199 +apply (auto intro: floor_eq3)
   8.200 +done
   8.201 +
   8.202 +lemma floor_number_of_eq [simp]:
   8.203 +     "floor(number_of n :: real) = (number_of n :: int)"
   8.204 +apply (subst real_number_of [symmetric])
   8.205 +apply (rule floor_real_of_int)
   8.206 +done
   8.207 +
   8.208 +lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
   8.209 +apply (simp add: floor_def Least_def)
   8.210 +apply (insert real_lb_ub_int [of r], safe)
   8.211 +apply (rule theI2)
   8.212 +apply (auto intro: lemma_floor)
   8.213 +done
   8.214 +
   8.215 +lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
   8.216 +apply (insert real_of_int_floor_ge_diff_one [of r])
   8.217 +apply (auto simp del: real_of_int_floor_ge_diff_one)
   8.218 +done
   8.219 +
   8.220 +
   8.221 +subsection{*Ceiling Function for Positive Reals*}
   8.222 +
   8.223 +lemma ceiling_zero [simp]: "ceiling 0 = 0"
   8.224 +by (simp add: ceiling_def)
   8.225 +
   8.226 +lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
   8.227 +by (simp add: ceiling_def)
   8.228 +
   8.229 +lemma ceiling_real_of_nat_zero [simp]: "ceiling (real (0::nat)) = 0"
   8.230 +by auto
   8.231 +
   8.232 +lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r"
   8.233 +by (simp add: ceiling_def)
   8.234 +
   8.235 +lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r"
   8.236 +by (simp add: ceiling_def)
   8.237 +
   8.238 +lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
   8.239 +apply (simp add: ceiling_def)
   8.240 +apply (subst le_minus_iff, simp)
   8.241 +done
   8.242 +
   8.243 +lemma ceiling_le: "x < y ==> ceiling x \<le> ceiling y"
   8.244 +by (simp add: floor_le ceiling_def)
   8.245 +
   8.246 +lemma ceiling_le2: "x \<le> y ==> ceiling x \<le> ceiling y"
   8.247 +by (simp add: floor_le2 ceiling_def)
   8.248 +
   8.249 +lemma real_of_int_ceiling_cancel [simp]:
   8.250 +     "(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
   8.251 +apply (auto simp add: ceiling_def)
   8.252 +apply (drule arg_cong [where f = uminus], auto)
   8.253 +apply (rule_tac x = "-n" in exI, auto)
   8.254 +done
   8.255 +
   8.256 +lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1"
   8.257 +apply (simp add: ceiling_def)
   8.258 +apply (rule minus_equation_iff [THEN iffD1])
   8.259 +apply (simp add: floor_eq [where n = "-(n+1)"])
   8.260 +done
   8.261 +
   8.262 +lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1"
   8.263 +by (simp add: ceiling_def floor_eq2 [where n = "-(n+1)"])
   8.264 +
   8.265 +lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n  |] ==> ceiling x = n"
   8.266 +by (simp add: ceiling_def floor_eq2 [where n = "-n"])
   8.267 +
   8.268 +lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
   8.269 +by (simp add: ceiling_def)
   8.270 +
   8.271 +lemma ceiling_number_of_eq [simp]:
   8.272 +     "ceiling (number_of n :: real) = (number_of n)"
   8.273 +apply (subst real_number_of [symmetric])
   8.274 +apply (rule ceiling_real_of_int)
   8.275 +done
   8.276 +
   8.277 +lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
   8.278 +apply (rule neg_le_iff_le [THEN iffD1])
   8.279 +apply (simp add: ceiling_def diff_minus)
   8.280 +done
   8.281 +
   8.282 +lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1"
   8.283 +apply (insert real_of_int_ceiling_diff_one_le [of r])
   8.284 +apply (simp del: real_of_int_ceiling_diff_one_le)
   8.285 +done
   8.286 +
   8.287 +ML
   8.288 +{*
   8.289 +val number_of_less_real_of_int_iff = thm "number_of_less_real_of_int_iff";
   8.290 +val number_of_less_real_of_int_iff2 = thm "number_of_less_real_of_int_iff2";
   8.291 +val number_of_le_real_of_int_iff = thm "number_of_le_real_of_int_iff";
   8.292 +val number_of_le_real_of_int_iff2 = thm "number_of_le_real_of_int_iff2";
   8.293 +val floor_zero = thm "floor_zero";
   8.294 +val floor_real_of_nat_zero = thm "floor_real_of_nat_zero";
   8.295 +val floor_real_of_nat = thm "floor_real_of_nat";
   8.296 +val floor_minus_real_of_nat = thm "floor_minus_real_of_nat";
   8.297 +val floor_real_of_int = thm "floor_real_of_int";
   8.298 +val floor_minus_real_of_int = thm "floor_minus_real_of_int";
   8.299 +val reals_Archimedean6 = thm "reals_Archimedean6";
   8.300 +val reals_Archimedean6a = thm "reals_Archimedean6a";
   8.301 +val reals_Archimedean_6b_int = thm "reals_Archimedean_6b_int";
   8.302 +val reals_Archimedean_6c_int = thm "reals_Archimedean_6c_int";
   8.303 +val real_lb_ub_int = thm "real_lb_ub_int";
   8.304 +val lemma_floor = thm "lemma_floor";
   8.305 +val real_of_int_floor_le = thm "real_of_int_floor_le";
   8.306 +val floor_le = thm "floor_le";
   8.307 +val floor_le2 = thm "floor_le2";
   8.308 +val lemma_floor2 = thm "lemma_floor2";
   8.309 +val real_of_int_floor_cancel = thm "real_of_int_floor_cancel";
   8.310 +val floor_eq = thm "floor_eq";
   8.311 +val floor_eq2 = thm "floor_eq2";
   8.312 +val floor_eq3 = thm "floor_eq3";
   8.313 +val floor_eq4 = thm "floor_eq4";
   8.314 +val floor_number_of_eq = thm "floor_number_of_eq";
   8.315 +val real_of_int_floor_ge_diff_one = thm "real_of_int_floor_ge_diff_one";
   8.316 +val real_of_int_floor_add_one_ge = thm "real_of_int_floor_add_one_ge";
   8.317 +val ceiling_zero = thm "ceiling_zero";
   8.318 +val ceiling_real_of_nat = thm "ceiling_real_of_nat";
   8.319 +val ceiling_real_of_nat_zero = thm "ceiling_real_of_nat_zero";
   8.320 +val ceiling_floor = thm "ceiling_floor";
   8.321 +val floor_ceiling = thm "floor_ceiling";
   8.322 +val real_of_int_ceiling_ge = thm "real_of_int_ceiling_ge";
   8.323 +val ceiling_le = thm "ceiling_le";
   8.324 +val ceiling_le2 = thm "ceiling_le2";
   8.325 +val real_of_int_ceiling_cancel = thm "real_of_int_ceiling_cancel";
   8.326 +val ceiling_eq = thm "ceiling_eq";
   8.327 +val ceiling_eq2 = thm "ceiling_eq2";
   8.328 +val ceiling_eq3 = thm "ceiling_eq3";
   8.329 +val ceiling_real_of_int = thm "ceiling_real_of_int";
   8.330 +val ceiling_number_of_eq = thm "ceiling_number_of_eq";
   8.331 +val real_of_int_ceiling_diff_one_le = thm "real_of_int_ceiling_diff_one_le";
   8.332 +val real_of_int_ceiling_le_add_one = thm "real_of_int_ceiling_le_add_one";
   8.333 +*}
   8.334 +
   8.335 +
   8.336  end
   8.337  
   8.338  
   8.339  
   8.340 +