# HG changeset patch # User paulson # Date 1082623556 -7200 # Node ID 79b7bd93626465b671ef1ed8d17ee669dcc5a54c # Parent b31870c50c6865357f459b867dc81b55db8f06d0 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate places diff -r b31870c50c68 -r 79b7bd936264 src/HOL/Complex/NSComplex.thy --- a/src/HOL/Complex/NSComplex.thy Thu Apr 22 10:43:06 2004 +0200 +++ b/src/HOL/Complex/NSComplex.thy Thu Apr 22 10:45:56 2004 +0200 @@ -7,7 +7,7 @@ header{*Nonstandard Complex Numbers*} -theory NSComplex = NSInduct: +theory NSComplex = Complex: constdefs hcomplexrel :: "((nat=>complex)*(nat=>complex)) set" diff -r b31870c50c68 -r 79b7bd936264 src/HOL/Complex/NSInduct.thy --- a/src/HOL/Complex/NSInduct.thy Thu Apr 22 10:43:06 2004 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,127 +0,0 @@ -(* Title: NSInduct.thy - Author: Jacques D. Fleuriot - Copyright: 2001 University of Edinburgh -*) - -header{*Nonstandard Characterization of Induction*} - -theory NSInduct = Complex: - -constdefs - - starPNat :: "(nat => bool) => hypnat => bool" ("*pNat* _" [80] 80) - "*pNat* P == (%x. \X. (X \ Rep_hypnat(x) & - {n. P(X n)} \ FreeUltrafilterNat))" - - - starPNat2 :: "(nat => nat => bool) => hypnat =>hypnat => bool" - ("*pNat2* _" [80] 80) - "*pNat2* P == (%x y. \X. \Y. (X \ Rep_hypnat(x) & Y \ Rep_hypnat(y) & - {n. P(X n) (Y n)} \ FreeUltrafilterNat))" - - hSuc :: "hypnat => hypnat" - "hSuc n == n + 1" - - -lemma starPNat: - "(( *pNat* P) (Abs_hypnat(hypnatrel``{%n. X n}))) = - ({n. P (X n)} \ FreeUltrafilterNat)" -by (auto simp add: starPNat_def, ultra) - -lemma starPNat_hypnat_of_nat [simp]: "( *pNat* P) (hypnat_of_nat n) = P n" -by (auto simp add: starPNat hypnat_of_nat_eq) - -lemma hypnat_induct_obj: - "(( *pNat* P) 0 & - (\n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1))) - --> ( *pNat* P)(n)" -apply (cases n) -apply (auto simp add: hypnat_zero_def hypnat_one_def starPNat, ultra) -apply (erule nat_induct) -apply (drule_tac x = "hypnat_of_nat n" in spec) -apply (rule ccontr) -apply (auto simp add: starPNat hypnat_of_nat_eq hypnat_add) -done - -lemma hypnat_induct: - "[| ( *pNat* P) 0; - !!n. ( *pNat* P)(n) ==> ( *pNat* P)(n + 1)|] - ==> ( *pNat* P)(n)" -by (insert hypnat_induct_obj [of P n], auto) - -lemma starPNat2: -"(( *pNat2* P) (Abs_hypnat(hypnatrel``{%n. X n})) - (Abs_hypnat(hypnatrel``{%n. Y n}))) = - ({n. P (X n) (Y n)} \ FreeUltrafilterNat)" -by (auto simp add: starPNat2_def, ultra) - -lemma starPNat2_eq_iff: "( *pNat2* (op =)) = (op =)" -apply (simp add: starPNat2_def) -apply (rule ext) -apply (rule ext) -apply (rule_tac z = x in eq_Abs_hypnat) -apply (rule_tac z = y in eq_Abs_hypnat) -apply (auto, ultra) -done - -lemma starPNat2_eq_iff2: "( *pNat2* (%x y. x = y)) X Y = (X = Y)" -by (simp add: starPNat2_eq_iff) - -lemma lemma_hyp: "(\h. P(h::hypnat)) = (\x. P(Abs_hypnat(hypnatrel `` {x})))" -apply auto -apply (rule_tac z = h in eq_Abs_hypnat, auto) -done - -lemma hSuc_not_zero [iff]: "hSuc m \ 0" -by (simp add: hSuc_def) - -lemmas zero_not_hSuc = hSuc_not_zero [THEN not_sym, standard, iff] - -lemma hSuc_hSuc_eq [iff]: "(hSuc m = hSuc n) = (m = n)" -by (simp add: hSuc_def hypnat_one_def) - -lemma nonempty_nat_set_Least_mem: "c \ (S :: nat set) ==> (LEAST n. n \ S) \ S" -by (erule LeastI) - -lemma nonempty_InternalNatSet_has_least: - "[| S \ InternalNatSets; S \ {} |] ==> \n \ S. \m \ S. n \ m" -apply (auto simp add: InternalNatSets_def starsetNat_n_def lemma_hyp) -apply (rule_tac z = x in eq_Abs_hypnat) -apply (auto dest!: bspec simp add: hypnat_le) -apply (drule_tac x = "%m. LEAST n. n \ As m" in spec, auto) -apply (ultra, force dest: nonempty_nat_set_Least_mem) -apply (drule_tac x = x in bspec, auto) -apply (ultra, auto intro: Least_le) -done - -text{* Goldblatt page 129 Thm 11.3.2*} -lemma internal_induct: - "[| X \ InternalNatSets; 0 \ X; \n. n \ X --> n + 1 \ X |] - ==> X = (UNIV:: hypnat set)" -apply (rule ccontr) -apply (frule InternalNatSets_Compl) -apply (drule_tac S = "- X" in nonempty_InternalNatSet_has_least, auto) -apply (subgoal_tac "1 \ n") -apply (drule_tac x = "n - 1" in bspec, safe) -apply (drule_tac x = "n - 1" in spec) -apply (drule_tac [2] c = 1 and a = n in add_right_mono) -apply (auto simp add: linorder_not_less [symmetric] iff del: hypnat_neq0_conv) -done - -ML -{* -val starPNat = thm "starPNat"; -val starPNat_hypnat_of_nat = thm "starPNat_hypnat_of_nat"; -val hypnat_induct = thm "hypnat_induct"; -val starPNat2 = thm "starPNat2"; -val starPNat2_eq_iff = thm "starPNat2_eq_iff"; -val starPNat2_eq_iff2 = thm "starPNat2_eq_iff2"; -val hSuc_not_zero = thm "hSuc_not_zero"; -val zero_not_hSuc = thms "zero_not_hSuc"; -val hSuc_hSuc_eq = thm "hSuc_hSuc_eq"; -val nonempty_nat_set_Least_mem = thm "nonempty_nat_set_Least_mem"; -val nonempty_InternalNatSet_has_least = thm "nonempty_InternalNatSet_has_least"; -val internal_induct = thm "internal_induct"; -*} - -end diff -r b31870c50c68 -r 79b7bd936264 src/HOL/Complex/README.html --- a/src/HOL/Complex/README.html Thu Apr 22 10:43:06 2004 +0200 +++ b/src/HOL/Complex/README.html Thu Apr 22 10:45:56 2004 +0200 @@ -7,52 +7,52 @@ with numeric constants and some complex analysis. The development includes nonstandard analysis for the complex numbers. Note that the image HOL-Complex includes theories from the directories -HOL/Real and HOL/Hyperreal. They define other types including real (the real numbers) and hypreal (the hyperreal or non-standard reals).

CLim Limits, continuous functions, and derivatives for the complex numbers -
CSeries Finite summation and infinite series for the complex numbers -
CStar Star-transforms for the complex numbers, to form non-standard extensions of sets and functions -
Complex The complex numbers -
NSCA Nonstandard complex analysis -
NSComplex Ultrapower construction of the nonstandard complex numbers - -
NSInduct Nonstandard induction for the hypernatural numbers - - -

Real: Dedekind Cut Construction of the Real Line

Lubs Definition of upper bounds, lubs and so on, to support completeness proofs. -
PReal The positive reals constructed using Dedekind cuts -
Rational The rational numbers constructed as equivalence classes of integers -
RComplete The reals are complete: they satisfy the supremum property. They also have the Archimedean property. -
RealDef The real numbers, their ordering properties, and embedding of the integers and the natural numbers -
RealPow Real numbers raised to natural number powers -

Hyperreal: Ultrafilter Construction of the Non-Standard Reals

- See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190. -

Filter Theory of Filters and Ultrafilters. Main result is a version of the Ultrafilter Theorem proved using Zorn's Lemma. -
HLog Non-standard logarithms -
HSeries Non-standard theory of finite summation and infinite series -
HTranscendental Non-standard extensions of transcendental functions -
HyperDef Ultrapower construction of the hyperreals -
HyperNat Ultrapower construction of the hypernaturals -
HyperPow Powers theory for the hyperreals -
IntFloor Floor and Ceiling functions relating the reals and integers -
Integration Gage integrals -
Lim Theory of limits, continuous functions, and derivatives -
Log Logarithms for the reals -
MacLaurin MacLaurin series -
NatStar Star-transforms for the hypernaturals, to form non-standard extensions of sets and functions involving the naturals or reals -
NthRoot Existence of n-th roots of real numbers -
NSA Theory defining sets of infinite numbers, infinitesimals, the infinitely close relation, and their various algebraic properties. -
Poly Univariate real polynomials -
SEQ Convergence of sequences and series using standard and nonstandard analysis -
Series Finite summation and infinite series for the reals -
Star Nonstandard extensions of real sets and real functions -
Transcendental Power series and transcendental functions -

Last modified $Date$ +HOL/Real and HOL/Hyperreal. They define other types including real (the real numbers) and hypreal (the hyperreal or non-standard reals). + +

CLim Limits, continuous functions, and derivatives for the complex numbers +
CSeries Finite summation and infinite series for the complex numbers +
CStar Star-transforms for the complex numbers, to form non-standard extensions of sets and functions +
Complex The complex numbers +
NSCA Nonstandard complex analysis +
NSComplex Ultrapower construction of the nonstandard complex numbers +

+ +

Real: Dedekind Cut Construction of the Real Line

+ +

Lubs Definition of upper bounds, lubs and so on, to support completeness proofs. +
PReal The positive reals constructed using Dedekind cuts +
Rational The rational numbers constructed as equivalence classes of integers +
RComplete The reals are complete: they satisfy the supremum property. They also have the Archimedean property. +
RealDef The real numbers, their ordering properties, and embedding of the integers and the natural numbers +
RealPow Real numbers raised to natural number powers +

Hyperreal: Ultrafilter Construction of the Non-Standard Reals

+See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190. +

Filter Theory of Filters and Ultrafilters. Main result is a version of the Ultrafilter Theorem proved using Zorn's Lemma. +
HLog Non-standard logarithms +
HSeries Non-standard theory of finite summation and infinite series +
HTranscendental Non-standard extensions of transcendental functions +
HyperDef Ultrapower construction of the hyperreals +
HyperNat Ultrapower construction of the hypernaturals +
HyperPow Powers theory for the hyperreals +
IntFloor Floor and Ceiling functions relating the reals and integers +
Integration Gage integrals +
Lim Theory of limits, continuous functions, and derivatives +
Log Logarithms for the reals +
MacLaurin MacLaurin series +
NatStar Star-transforms for the hypernaturals, to form non-standard extensions of sets and functions involving the naturals or reals +
NthRoot Existence of n-th roots of real numbers +
NSA Theory defining sets of infinite numbers, infinitesimals, the infinitely close relation, and their various algebraic properties. +
Poly Univariate real polynomials +
SEQ Convergence of sequences and series using standard and nonstandard analysis +
Series Finite summation and infinite series for the reals +
Star Nonstandard extensions of real sets and real functions +
Transcendental Power series and transcendental functions +

Last modified $Date$ diff -r b31870c50c68 -r 79b7bd936264 src/HOL/Hyperreal/HTranscendental.thy --- a/src/HOL/Hyperreal/HTranscendental.thy Thu Apr 22 10:43:06 2004 +0200 +++ b/src/HOL/Hyperreal/HTranscendental.thy Thu Apr 22 10:45:56 2004 +0200 @@ -7,7 +7,7 @@ header{*Nonstandard Extensions of Transcendental Functions*} -theory HTranscendental = Transcendental + IntFloor: +theory HTranscendental = Transcendental + Integration: constdefs diff -r b31870c50c68 -r 79b7bd936264 src/HOL/Hyperreal/IntFloor.thy --- a/src/HOL/Hyperreal/IntFloor.thy Thu Apr 22 10:43:06 2004 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,322 +0,0 @@ -(* Title: IntFloor.thy - Author: Jacques D. Fleuriot - Copyright: 2001,2002 University of Edinburgh -Converted to Isar and polished by lcp -*) - -header{*Floor and Ceiling Functions from the Reals to the Integers*} - -theory IntFloor = Integration: - -constdefs - - floor :: "real => int" - "floor r == (LEAST n. r < real (n + (1::int)))" - - ceiling :: "real => int" - "ceiling r == - floor (- r)" - -syntax (xsymbols) - floor :: "real => int" ("\_\") - ceiling :: "real => int" ("\_\") - -syntax (HTML output) - floor :: "real => int" ("\_\") - ceiling :: "real => int" ("\_\") - - -lemma number_of_less_real_of_int_iff [simp]: - "((number_of n) < real (m::int)) = (number_of n < m)" -apply auto -apply (rule real_of_int_less_iff [THEN iffD1]) -apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto) -done - -lemma number_of_less_real_of_int_iff2 [simp]: - "(real (m::int) < (number_of n)) = (m < number_of n)" -apply auto -apply (rule real_of_int_less_iff [THEN iffD1]) -apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto) -done - -lemma number_of_le_real_of_int_iff [simp]: - "((number_of n) \ real (m::int)) = (number_of n \ m)" -by (simp add: linorder_not_less [symmetric]) - -lemma number_of_le_real_of_int_iff2 [simp]: - "(real (m::int) \ (number_of n)) = (m \ number_of n)" -by (simp add: linorder_not_less [symmetric]) - -lemma floor_zero [simp]: "floor 0 = 0" -apply (simp add: floor_def) -apply (rule Least_equality, auto) -done - -lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0" -by auto - -lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n" -apply (simp only: floor_def) -apply (rule Least_equality) -apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) -apply (drule_tac [2] real_of_int_less_iff [THEN iffD1]) -apply (simp_all add: real_of_int_real_of_nat) -done - -lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n" -apply (simp only: floor_def) -apply (rule Least_equality) -apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) -apply (drule_tac [2] real_of_int_minus [THEN subst]) -apply (drule_tac [2] real_of_int_less_iff [THEN iffD1]) -apply (simp_all add: real_of_int_real_of_nat) -done - -lemma floor_real_of_int [simp]: "floor (real (n::int)) = n" -apply (simp only: floor_def) -apply (rule Least_equality) -apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) -apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto) -done - -lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n" -apply (simp only: floor_def) -apply (rule Least_equality) -apply (drule_tac [2] real_of_int_minus [THEN subst]) -apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) -apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto) -done - -lemma reals_Archimedean6: - "0 \ r ==> \(n::nat). real (n - 1) \ r & r < real (n)" -apply (insert reals_Archimedean2 [of r], safe) -apply (frule_tac P = "%k. r < real k" and k = n and m = "%x. x" - in ex_has_least_nat, auto) -apply (rule_tac x = x in exI) -apply (case_tac x, simp) -apply (rename_tac x') -apply (drule_tac x = x' in spec, simp) -done - -lemma reals_Archimedean6a: "0 \ r ==> \n. real (n) \ r & r < real (Suc n)" -by (drule reals_Archimedean6, auto) - -lemma reals_Archimedean_6b_int: - "0 \ r ==> \n. real n \ r & r < real ((n::int) + 1)" -apply (drule reals_Archimedean6a, auto) -apply (rule_tac x = "int n" in exI) -apply (simp add: real_of_int_real_of_nat real_of_nat_Suc) -done - -lemma reals_Archimedean_6c_int: - "r < 0 ==> \n. real n \ r & r < real ((n::int) + 1)" -apply (rule reals_Archimedean_6b_int [of "-r", THEN exE], simp, auto) -apply (rename_tac n) -apply (drule real_le_imp_less_or_eq, auto) -apply (rule_tac x = "- n - 1" in exI) -apply (rule_tac [2] x = "- n" in exI, auto) -done - -lemma real_lb_ub_int: " \(n::int). real n \ r & r < real ((n::int) + 1)" -apply (case_tac "r < 0") -apply (blast intro: reals_Archimedean_6c_int) -apply (simp only: linorder_not_less) -apply (blast intro: reals_Archimedean_6b_int reals_Archimedean_6c_int) -done - -lemma lemma_floor: - assumes a1: "real m \ r" and a2: "r < real n + 1" - shows "m \ (n::int)" -proof - - have "real m < real n + 1" by (rule order_le_less_trans) - also have "... = real(n+1)" by simp - finally have "m < n+1" by (simp only: real_of_int_less_iff) - thus ?thesis by arith -qed - -lemma real_of_int_floor_le [simp]: "real (floor r) \ r" -apply (simp add: floor_def Least_def) -apply (insert real_lb_ub_int [of r], safe) -apply (rule theI2, auto) -done - -lemma floor_le: "x < y ==> floor x \ floor y" -apply (simp add: floor_def Least_def) -apply (insert real_lb_ub_int [of x]) -apply (insert real_lb_ub_int [of y], safe) -apply (rule theI2) -apply (rule_tac [3] theI2, auto) -done - -lemma floor_le2: "x \ y ==> floor x \ floor y" -by (auto dest: real_le_imp_less_or_eq simp add: floor_le) - -lemma lemma_floor2: "real na < real (x::int) + 1 ==> na \ x" -by (auto intro: lemma_floor) - -lemma real_of_int_floor_cancel [simp]: - "(real (floor x) = x) = (\n::int. x = real n)" -apply (simp add: floor_def Least_def) -apply (insert real_lb_ub_int [of x], erule exE) -apply (rule theI2) -apply (auto intro: lemma_floor) -done - -lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n" -apply (simp add: floor_def) -apply (rule Least_equality) -apply (auto intro: lemma_floor) -done - -lemma floor_eq2: "[| real n \ x; x < real n + 1 |] ==> floor x = n" -apply (simp add: floor_def) -apply (rule Least_equality) -apply (auto intro: lemma_floor) -done - -lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n" -apply (rule inj_int [THEN injD]) -apply (simp add: real_of_nat_Suc) -apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "of_nat n"]) -done - -lemma floor_eq4: "[| real n \ x; x < real (Suc n) |] ==> nat(floor x) = n" -apply (drule order_le_imp_less_or_eq) -apply (auto intro: floor_eq3) -done - -lemma floor_number_of_eq [simp]: - "floor(number_of n :: real) = (number_of n :: int)" -apply (subst real_number_of [symmetric]) -apply (rule floor_real_of_int) -done - -lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \ real(floor r)" -apply (simp add: floor_def Least_def) -apply (insert real_lb_ub_int [of r], safe) -apply (rule theI2) -apply (auto intro: lemma_floor) -done - -lemma real_of_int_floor_add_one_ge [simp]: "r \ real(floor r) + 1" -apply (insert real_of_int_floor_ge_diff_one [of r]) -apply (auto simp del: real_of_int_floor_ge_diff_one) -done - - -subsection{*Ceiling Function for Positive Reals*} - -lemma ceiling_zero [simp]: "ceiling 0 = 0" -by (simp add: ceiling_def) - -lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n" -by (simp add: ceiling_def) - -lemma ceiling_real_of_nat_zero [simp]: "ceiling (real (0::nat)) = 0" -by auto - -lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r" -by (simp add: ceiling_def) - -lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r" -by (simp add: ceiling_def) - -lemma real_of_int_ceiling_ge [simp]: "r \ real (ceiling r)" -apply (simp add: ceiling_def) -apply (subst le_minus_iff, simp) -done - -lemma ceiling_le: "x < y ==> ceiling x \ ceiling y" -by (simp add: floor_le ceiling_def) - -lemma ceiling_le2: "x \ y ==> ceiling x \ ceiling y" -by (simp add: floor_le2 ceiling_def) - -lemma real_of_int_ceiling_cancel [simp]: - "(real (ceiling x) = x) = (\n::int. x = real n)" -apply (auto simp add: ceiling_def) -apply (drule arg_cong [where f = uminus], auto) -apply (rule_tac x = "-n" in exI, auto) -done - -lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1" -apply (simp add: ceiling_def) -apply (rule minus_equation_iff [THEN iffD1]) -apply (simp add: floor_eq [where n = "-(n+1)"]) -done - -lemma ceiling_eq2: "[| real n < x; x \ real n + 1 |] ==> ceiling x = n + 1" -by (simp add: ceiling_def floor_eq2 [where n = "-(n+1)"]) - -lemma ceiling_eq3: "[| real n - 1 < x; x \ real n |] ==> ceiling x = n" -by (simp add: ceiling_def floor_eq2 [where n = "-n"]) - -lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n" -by (simp add: ceiling_def) - -lemma ceiling_number_of_eq [simp]: - "ceiling (number_of n :: real) = (number_of n)" -apply (subst real_number_of [symmetric]) -apply (rule ceiling_real_of_int) -done - -lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \ r" -apply (rule neg_le_iff_le [THEN iffD1]) -apply (simp add: ceiling_def diff_minus) -done - -lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \ r + 1" -apply (insert real_of_int_ceiling_diff_one_le [of r]) -apply (simp del: real_of_int_ceiling_diff_one_le) -done - -ML -{* -val number_of_less_real_of_int_iff = thm "number_of_less_real_of_int_iff"; -val number_of_less_real_of_int_iff2 = thm "number_of_less_real_of_int_iff2"; -val number_of_le_real_of_int_iff = thm "number_of_le_real_of_int_iff"; -val number_of_le_real_of_int_iff2 = thm "number_of_le_real_of_int_iff2"; -val floor_zero = thm "floor_zero"; -val floor_real_of_nat_zero = thm "floor_real_of_nat_zero"; -val floor_real_of_nat = thm "floor_real_of_nat"; -val floor_minus_real_of_nat = thm "floor_minus_real_of_nat"; -val floor_real_of_int = thm "floor_real_of_int"; -val floor_minus_real_of_int = thm "floor_minus_real_of_int"; -val reals_Archimedean6 = thm "reals_Archimedean6"; -val reals_Archimedean6a = thm "reals_Archimedean6a"; -val reals_Archimedean_6b_int = thm "reals_Archimedean_6b_int"; -val reals_Archimedean_6c_int = thm "reals_Archimedean_6c_int"; -val real_lb_ub_int = thm "real_lb_ub_int"; -val lemma_floor = thm "lemma_floor"; -val real_of_int_floor_le = thm "real_of_int_floor_le"; -val floor_le = thm "floor_le"; -val floor_le2 = thm "floor_le2"; -val lemma_floor2 = thm "lemma_floor2"; -val real_of_int_floor_cancel = thm "real_of_int_floor_cancel"; -val floor_eq = thm "floor_eq"; -val floor_eq2 = thm "floor_eq2"; -val floor_eq3 = thm "floor_eq3"; -val floor_eq4 = thm "floor_eq4"; -val floor_number_of_eq = thm "floor_number_of_eq"; -val real_of_int_floor_ge_diff_one = thm "real_of_int_floor_ge_diff_one"; -val real_of_int_floor_add_one_ge = thm "real_of_int_floor_add_one_ge"; -val ceiling_zero = thm "ceiling_zero"; -val ceiling_real_of_nat = thm "ceiling_real_of_nat"; -val ceiling_real_of_nat_zero = thm "ceiling_real_of_nat_zero"; -val ceiling_floor = thm "ceiling_floor"; -val floor_ceiling = thm "floor_ceiling"; -val real_of_int_ceiling_ge = thm "real_of_int_ceiling_ge"; -val ceiling_le = thm "ceiling_le"; -val ceiling_le2 = thm "ceiling_le2"; -val real_of_int_ceiling_cancel = thm "real_of_int_ceiling_cancel"; -val ceiling_eq = thm "ceiling_eq"; -val ceiling_eq2 = thm "ceiling_eq2"; -val ceiling_eq3 = thm "ceiling_eq3"; -val ceiling_real_of_int = thm "ceiling_real_of_int"; -val ceiling_number_of_eq = thm "ceiling_number_of_eq"; -val real_of_int_ceiling_diff_one_le = thm "real_of_int_ceiling_diff_one_le"; -val real_of_int_ceiling_le_add_one = thm "real_of_int_ceiling_le_add_one"; -*} - - -end diff -r b31870c50c68 -r 79b7bd936264 src/HOL/Hyperreal/NatStar.thy --- a/src/HOL/Hyperreal/NatStar.thy Thu Apr 22 10:43:06 2004 +0200 +++ b/src/HOL/Hyperreal/NatStar.thy Thu Apr 22 10:45:56 2004 +0200 @@ -533,6 +533,112 @@ val starfunNat_inverse_real_of_nat_Infinitesimal = thm "starfunNat_inverse_real_of_nat_Infinitesimal"; *} + + +subsection{*Nonstandard Characterization of Induction*} + +constdefs + + starPNat :: "(nat => bool) => hypnat => bool" ("*pNat* _" [80] 80) + "*pNat* P == (%x. \X. (X \ Rep_hypnat(x) & + {n. P(X n)} \ FreeUltrafilterNat))" + + + starPNat2 :: "(nat => nat => bool) => hypnat =>hypnat => bool" + ("*pNat2* _" [80] 80) + "*pNat2* P == (%x y. \X. \Y. (X \ Rep_hypnat(x) & Y \ Rep_hypnat(y) & + {n. P(X n) (Y n)} \ FreeUltrafilterNat))" + + hSuc :: "hypnat => hypnat" + "hSuc n == n + 1" + + +lemma starPNat: + "(( *pNat* P) (Abs_hypnat(hypnatrel``{%n. X n}))) = + ({n. P (X n)} \ FreeUltrafilterNat)" +by (auto simp add: starPNat_def, ultra) + +lemma starPNat_hypnat_of_nat [simp]: "( *pNat* P) (hypnat_of_nat n) = P n" +by (auto simp add: starPNat hypnat_of_nat_eq) + +lemma hypnat_induct_obj: + "(( *pNat* P) 0 & + (\n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1))) + --> ( *pNat* P)(n)" +apply (cases n) +apply (auto simp add: hypnat_zero_def hypnat_one_def starPNat, ultra) +apply (erule nat_induct) +apply (drule_tac x = "hypnat_of_nat n" in spec) +apply (rule ccontr) +apply (auto simp add: starPNat hypnat_of_nat_eq hypnat_add) +done + +lemma hypnat_induct: + "[| ( *pNat* P) 0; + !!n. ( *pNat* P)(n) ==> ( *pNat* P)(n + 1)|] + ==> ( *pNat* P)(n)" +by (insert hypnat_induct_obj [of P n], auto) + +lemma starPNat2: +"(( *pNat2* P) (Abs_hypnat(hypnatrel``{%n. X n})) + (Abs_hypnat(hypnatrel``{%n. Y n}))) = + ({n. P (X n) (Y n)} \ FreeUltrafilterNat)" +by (auto simp add: starPNat2_def, ultra) + +lemma starPNat2_eq_iff: "( *pNat2* (op =)) = (op =)" +apply (simp add: starPNat2_def) +apply (rule ext) +apply (rule ext) +apply (rule_tac z = x in eq_Abs_hypnat) +apply (rule_tac z = y in eq_Abs_hypnat) +apply (auto, ultra) +done + +lemma starPNat2_eq_iff2: "( *pNat2* (%x y. x = y)) X Y = (X = Y)" +by (simp add: starPNat2_eq_iff) + +lemma lemma_hyp: "(\h. P(h::hypnat)) = (\x. P(Abs_hypnat(hypnatrel `` {x})))" +apply auto +apply (rule_tac z = h in eq_Abs_hypnat, auto) +done + +lemma hSuc_not_zero [iff]: "hSuc m \ 0" +by (simp add: hSuc_def) + +lemmas zero_not_hSuc = hSuc_not_zero [THEN not_sym, standard, iff] + +lemma hSuc_hSuc_eq [iff]: "(hSuc m = hSuc n) = (m = n)" +by (simp add: hSuc_def hypnat_one_def) + +lemma nonempty_nat_set_Least_mem: "c \ (S :: nat set) ==> (LEAST n. n \ S) \ S" +by (erule LeastI) + +lemma nonempty_InternalNatSet_has_least: + "[| S \ InternalNatSets; S \ {} |] ==> \n \ S. \m \ S. n \ m" +apply (auto simp add: InternalNatSets_def starsetNat_n_def lemma_hyp) +apply (rule_tac z = x in eq_Abs_hypnat) +apply (auto dest!: bspec simp add: hypnat_le) +apply (drule_tac x = "%m. LEAST n. n \ As m" in spec, auto) +apply (ultra, force dest: nonempty_nat_set_Least_mem) +apply (drule_tac x = x in bspec, auto) +apply (ultra, auto intro: Least_le) +done + +text{* Goldblatt page 129 Thm 11.3.2*} +lemma internal_induct: + "[| X \ InternalNatSets; 0 \ X; \n. n \ X --> n + 1 \ X |] + ==> X = (UNIV:: hypnat set)" +apply (rule ccontr) +apply (frule InternalNatSets_Compl) +apply (drule_tac S = "- X" in nonempty_InternalNatSet_has_least, auto) +apply (subgoal_tac "1 \ n") +apply (drule_tac x = "n - 1" in bspec, safe) +apply (drule_tac x = "n - 1" in spec) +apply (drule_tac [2] c = 1 and a = n in add_right_mono) +apply (auto simp add: linorder_not_less [symmetric] iff del: hypnat_neq0_conv) +done + + end diff -r b31870c50c68 -r 79b7bd936264 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Apr 22 10:43:06 2004 +0200 +++ b/src/HOL/IsaMakefile Thu Apr 22 10:45:56 2004 +0200 @@ -150,7 +150,7 @@ Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HSeries.thy\ Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy\ Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\ - Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy Hyperreal/IntFloor.thy\ + Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\ Hyperreal/Lim.thy Hyperreal/Log.thy\ Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy\ Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy\ @@ -159,7 +159,7 @@ Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \ Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy\ Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy\ - Complex/NSCA.thy Complex/NSComplex.thy Complex/NSInduct.thy + Complex/NSCA.thy Complex/NSComplex.thy @cd Complex; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Complex diff -r b31870c50c68 -r 79b7bd936264 src/HOL/Real/RComplete.thy --- a/src/HOL/Real/RComplete.thy Thu Apr 22 10:43:06 2004 +0200 +++ b/src/HOL/Real/RComplete.thy Thu Apr 22 10:45:56 2004 +0200 @@ -2,11 +2,11 @@ ID : $Id$ Author : Jacques D. Fleuriot Copyright : 1998 University of Cambridge - Description : Completeness theorems for positive - reals and reals + Copyright : 2001,2002 University of Edinburgh +Converted to Isar and polished by lcp *) -header{*Completeness Theorems for Positive Reals and Reals.*} +header{*Completeness of the Reals; Floor and Ceiling Functions*} theory RComplete = Lubs + RealDef: @@ -215,7 +215,322 @@ val reals_Archimedean3 = thm "reals_Archimedean3"; *} + +subsection{*Floor and Ceiling Functions from the Reals to the Integers*} + +constdefs + + floor :: "real => int" + "floor r == (LEAST n::int. r < real (n+1))" + + ceiling :: "real => int" + "ceiling r == - floor (- r)" + +syntax (xsymbols) + floor :: "real => int" ("\_\") + ceiling :: "real => int" ("\_\") + +syntax (HTML output) + floor :: "real => int" ("\_\") + ceiling :: "real => int" ("\_\") + + +lemma number_of_less_real_of_int_iff [simp]: + "((number_of n) < real (m::int)) = (number_of n < m)" +apply auto +apply (rule real_of_int_less_iff [THEN iffD1]) +apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto) +done + +lemma number_of_less_real_of_int_iff2 [simp]: + "(real (m::int) < (number_of n)) = (m < number_of n)" +apply auto +apply (rule real_of_int_less_iff [THEN iffD1]) +apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto) +done + +lemma number_of_le_real_of_int_iff [simp]: + "((number_of n) \ real (m::int)) = (number_of n \ m)" +by (simp add: linorder_not_less [symmetric]) + +lemma number_of_le_real_of_int_iff2 [simp]: + "(real (m::int) \ (number_of n)) = (m \ number_of n)" +by (simp add: linorder_not_less [symmetric]) + +lemma floor_zero [simp]: "floor 0 = 0" +apply (simp add: floor_def) +apply (rule Least_equality, auto) +done + +lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0" +by auto + +lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n" +apply (simp only: floor_def) +apply (rule Least_equality) +apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) +apply (drule_tac [2] real_of_int_less_iff [THEN iffD1]) +apply (simp_all add: real_of_int_real_of_nat) +done + +lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n" +apply (simp only: floor_def) +apply (rule Least_equality) +apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) +apply (drule_tac [2] real_of_int_minus [THEN subst]) +apply (drule_tac [2] real_of_int_less_iff [THEN iffD1]) +apply (simp_all add: real_of_int_real_of_nat) +done + +lemma floor_real_of_int [simp]: "floor (real (n::int)) = n" +apply (simp only: floor_def) +apply (rule Least_equality) +apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) +apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto) +done + +lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n" +apply (simp only: floor_def) +apply (rule Least_equality) +apply (drule_tac [2] real_of_int_minus [THEN subst]) +apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) +apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto) +done + +lemma reals_Archimedean6: + "0 \ r ==> \(n::nat). real (n - 1) \ r & r < real (n)" +apply (insert reals_Archimedean2 [of r], safe) +apply (frule_tac P = "%k. r < real k" and k = n and m = "%x. x" + in ex_has_least_nat, auto) +apply (rule_tac x = x in exI) +apply (case_tac x, simp) +apply (rename_tac x') +apply (drule_tac x = x' in spec, simp) +done + +lemma reals_Archimedean6a: "0 \ r ==> \n. real (n) \ r & r < real (Suc n)" +by (drule reals_Archimedean6, auto) + +lemma reals_Archimedean_6b_int: + "0 \ r ==> \n::int. real n \ r & r < real (n+1)" +apply (drule reals_Archimedean6a, auto) +apply (rule_tac x = "int n" in exI) +apply (simp add: real_of_int_real_of_nat real_of_nat_Suc) +done + +lemma reals_Archimedean_6c_int: + "r < 0 ==> \n::int. real n \ r & r < real (n+1)" +apply (rule reals_Archimedean_6b_int [of "-r", THEN exE], simp, auto) +apply (rename_tac n) +apply (drule real_le_imp_less_or_eq, auto) +apply (rule_tac x = "- n - 1" in exI) +apply (rule_tac [2] x = "- n" in exI, auto) +done + +lemma real_lb_ub_int: " \n::int. real n \ r & r < real (n+1)" +apply (case_tac "r < 0") +apply (blast intro: reals_Archimedean_6c_int) +apply (simp only: linorder_not_less) +apply (blast intro: reals_Archimedean_6b_int reals_Archimedean_6c_int) +done + +lemma lemma_floor: + assumes a1: "real m \ r" and a2: "r < real n + 1" + shows "m \ (n::int)" +proof - + have "real m < real n + 1" by (rule order_le_less_trans) + also have "... = real(n+1)" by simp + finally have "m < n+1" by (simp only: real_of_int_less_iff) + thus ?thesis by arith +qed + +lemma real_of_int_floor_le [simp]: "real (floor r) \ r" +apply (simp add: floor_def Least_def) +apply (insert real_lb_ub_int [of r], safe) +apply (rule theI2, auto) +done + +lemma floor_le: "x < y ==> floor x \ floor y" +apply (simp add: floor_def Least_def) +apply (insert real_lb_ub_int [of x]) +apply (insert real_lb_ub_int [of y], safe) +apply (rule theI2) +apply (rule_tac [3] theI2, auto) +done + +lemma floor_le2: "x \ y ==> floor x \ floor y" +by (auto dest: real_le_imp_less_or_eq simp add: floor_le) + +lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \ x" +by (auto intro: lemma_floor) + +lemma real_of_int_floor_cancel [simp]: + "(real (floor x) = x) = (\n::int. x = real n)" +apply (simp add: floor_def Least_def) +apply (insert real_lb_ub_int [of x], erule exE) +apply (rule theI2) +apply (auto intro: lemma_floor) +done + +lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n" +apply (simp add: floor_def) +apply (rule Least_equality) +apply (auto intro: lemma_floor) +done + +lemma floor_eq2: "[| real n \ x; x < real n + 1 |] ==> floor x = n" +apply (simp add: floor_def) +apply (rule Least_equality) +apply (auto intro: lemma_floor) +done + +lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n" +apply (rule inj_int [THEN injD]) +apply (simp add: real_of_nat_Suc) +apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "of_nat n"]) +done + +lemma floor_eq4: "[| real n \ x; x < real (Suc n) |] ==> nat(floor x) = n" +apply (drule order_le_imp_less_or_eq) +apply (auto intro: floor_eq3) +done + +lemma floor_number_of_eq [simp]: + "floor(number_of n :: real) = (number_of n :: int)" +apply (subst real_number_of [symmetric]) +apply (rule floor_real_of_int) +done + +lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \ real(floor r)" +apply (simp add: floor_def Least_def) +apply (insert real_lb_ub_int [of r], safe) +apply (rule theI2) +apply (auto intro: lemma_floor) +done + +lemma real_of_int_floor_add_one_ge [simp]: "r \ real(floor r) + 1" +apply (insert real_of_int_floor_ge_diff_one [of r]) +apply (auto simp del: real_of_int_floor_ge_diff_one) +done + + +subsection{*Ceiling Function for Positive Reals*} + +lemma ceiling_zero [simp]: "ceiling 0 = 0" +by (simp add: ceiling_def) + +lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n" +by (simp add: ceiling_def) + +lemma ceiling_real_of_nat_zero [simp]: "ceiling (real (0::nat)) = 0" +by auto + +lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r" +by (simp add: ceiling_def) + +lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r" +by (simp add: ceiling_def) + +lemma real_of_int_ceiling_ge [simp]: "r \ real (ceiling r)" +apply (simp add: ceiling_def) +apply (subst le_minus_iff, simp) +done + +lemma ceiling_le: "x < y ==> ceiling x \ ceiling y" +by (simp add: floor_le ceiling_def) + +lemma ceiling_le2: "x \ y ==> ceiling x \ ceiling y" +by (simp add: floor_le2 ceiling_def) + +lemma real_of_int_ceiling_cancel [simp]: + "(real (ceiling x) = x) = (\n::int. x = real n)" +apply (auto simp add: ceiling_def) +apply (drule arg_cong [where f = uminus], auto) +apply (rule_tac x = "-n" in exI, auto) +done + +lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1" +apply (simp add: ceiling_def) +apply (rule minus_equation_iff [THEN iffD1]) +apply (simp add: floor_eq [where n = "-(n+1)"]) +done + +lemma ceiling_eq2: "[| real n < x; x \ real n + 1 |] ==> ceiling x = n + 1" +by (simp add: ceiling_def floor_eq2 [where n = "-(n+1)"]) + +lemma ceiling_eq3: "[| real n - 1 < x; x \ real n |] ==> ceiling x = n" +by (simp add: ceiling_def floor_eq2 [where n = "-n"]) + +lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n" +by (simp add: ceiling_def) + +lemma ceiling_number_of_eq [simp]: + "ceiling (number_of n :: real) = (number_of n)" +apply (subst real_number_of [symmetric]) +apply (rule ceiling_real_of_int) +done + +lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \ r" +apply (rule neg_le_iff_le [THEN iffD1]) +apply (simp add: ceiling_def diff_minus) +done + +lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \ r + 1" +apply (insert real_of_int_ceiling_diff_one_le [of r]) +apply (simp del: real_of_int_ceiling_diff_one_le) +done + +ML +{* +val number_of_less_real_of_int_iff = thm "number_of_less_real_of_int_iff"; +val number_of_less_real_of_int_iff2 = thm "number_of_less_real_of_int_iff2"; +val number_of_le_real_of_int_iff = thm "number_of_le_real_of_int_iff"; +val number_of_le_real_of_int_iff2 = thm "number_of_le_real_of_int_iff2"; +val floor_zero = thm "floor_zero"; +val floor_real_of_nat_zero = thm "floor_real_of_nat_zero"; +val floor_real_of_nat = thm "floor_real_of_nat"; +val floor_minus_real_of_nat = thm "floor_minus_real_of_nat"; +val floor_real_of_int = thm "floor_real_of_int"; +val floor_minus_real_of_int = thm "floor_minus_real_of_int"; +val reals_Archimedean6 = thm "reals_Archimedean6"; +val reals_Archimedean6a = thm "reals_Archimedean6a"; +val reals_Archimedean_6b_int = thm "reals_Archimedean_6b_int"; +val reals_Archimedean_6c_int = thm "reals_Archimedean_6c_int"; +val real_lb_ub_int = thm "real_lb_ub_int"; +val lemma_floor = thm "lemma_floor"; +val real_of_int_floor_le = thm "real_of_int_floor_le"; +val floor_le = thm "floor_le"; +val floor_le2 = thm "floor_le2"; +val lemma_floor2 = thm "lemma_floor2"; +val real_of_int_floor_cancel = thm "real_of_int_floor_cancel"; +val floor_eq = thm "floor_eq"; +val floor_eq2 = thm "floor_eq2"; +val floor_eq3 = thm "floor_eq3"; +val floor_eq4 = thm "floor_eq4"; +val floor_number_of_eq = thm "floor_number_of_eq"; +val real_of_int_floor_ge_diff_one = thm "real_of_int_floor_ge_diff_one"; +val real_of_int_floor_add_one_ge = thm "real_of_int_floor_add_one_ge"; +val ceiling_zero = thm "ceiling_zero"; +val ceiling_real_of_nat = thm "ceiling_real_of_nat"; +val ceiling_real_of_nat_zero = thm "ceiling_real_of_nat_zero"; +val ceiling_floor = thm "ceiling_floor"; +val floor_ceiling = thm "floor_ceiling"; +val real_of_int_ceiling_ge = thm "real_of_int_ceiling_ge"; +val ceiling_le = thm "ceiling_le"; +val ceiling_le2 = thm "ceiling_le2"; +val real_of_int_ceiling_cancel = thm "real_of_int_ceiling_cancel"; +val ceiling_eq = thm "ceiling_eq"; +val ceiling_eq2 = thm "ceiling_eq2"; +val ceiling_eq3 = thm "ceiling_eq3"; +val ceiling_real_of_int = thm "ceiling_real_of_int"; +val ceiling_number_of_eq = thm "ceiling_number_of_eq"; +val real_of_int_ceiling_diff_one_le = thm "real_of_int_ceiling_diff_one_le"; +val real_of_int_ceiling_le_add_one = thm "real_of_int_ceiling_le_add_one"; +*} + + end +