Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: HyperDef.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Nonstandard_Analysis/HyperDef.thy
    Author:     Jacques D. Fleuriot
    Copyright:  1998  University of Cambridge
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
*)

section \<open>Construction of Hyperreals Using Ultrafilters\<close>

theory HyperDef
  imports Complex_Main HyperNat
begin

type_synonym hypreal = "real star"

abbreviation hypreal_of_real :: "real \ real star"
  where "hypreal_of_real \ star_of"

abbreviation hypreal_of_hypnat :: "hypnat \ hypreal"
  where "hypreal_of_hypnat \ of_hypnat"

definition omega :: hypreal  ("\")
  where "\ = star_n (\n. real (Suc n))"
    \<comment> \<open>an infinite number \<open>= [<1, 2, 3, \<dots>>]\<close>\<close>

definition epsilon :: hypreal  ("\")
  where "\ = star_n (\n. inverse (real (Suc n)))"
    \<comment> \<open>an infinitesimal number \<open>= [<1, 1/2, 1/3, \<dots>>]\<close>\<close>

subsection \<open>Real vector class instances\<close>

instantiation star :: (scaleR) scaleR
begin
  definition star_scaleR_def [transfer_unfold]: "scaleR r \ *f* (scaleR r)"
  instance ..
end

lemma Standard_scaleR [simp]: "x \ Standard \ scaleR r x \ Standard"
  by (simp add: star_scaleR_def)

lemma star_of_scaleR [simp]: "star_of (scaleR r x) = scaleR r (star_of x)"
  by transfer (rule refl)

instance star :: (real_vector) real_vector
proof
  fix a b :: real
  show "\x y::'a star. scaleR a (x + y) = scaleR a x + scaleR a y"
    by transfer (rule scaleR_right_distrib)
  show "\x::'a star. scaleR (a + b) x = scaleR a x + scaleR b x"
    by transfer (rule scaleR_left_distrib)
  show "\x::'a star. scaleR a (scaleR b x) = scaleR (a * b) x"
    by transfer (rule scaleR_scaleR)
  show "\x::'a star. scaleR 1 x = x"
    by transfer (rule scaleR_one)
qed

instance star :: (real_algebra) real_algebra
proof
  fix a :: real
  show "\x y::'a star. scaleR a x * y = scaleR a (x * y)"
    by transfer (rule mult_scaleR_left)
  show "\x y::'a star. x * scaleR a y = scaleR a (x * y)"
    by transfer (rule mult_scaleR_right)
qed

instance star :: (real_algebra_1) real_algebra_1 ..

instance star :: (real_div_algebra) real_div_algebra ..

instance star :: (field_char_0) field_char_0 ..

instance star :: (real_field) real_field ..

lemma star_of_real_def [transfer_unfold]: "of_real r = star_of (of_real r)"
  by (unfold of_real_def, transfer, rule refl)

lemma Standard_of_real [simp]: "of_real r \ Standard"
  by (simp add: star_of_real_def)

lemma star_of_of_real [simp]: "star_of (of_real r) = of_real r"
  by transfer (rule refl)

lemma of_real_eq_star_of [simp]: "of_real = star_of"
proof
  show "of_real r = star_of r" for r :: real
    by transfer simp
qed

lemma Reals_eq_Standard: "(\ :: hypreal set) = Standard"
  by (simp add: Reals_def Standard_def)

subsection \<open>Injection from \<^typ>\<open>hypreal\<close>\<close>

definition of_hypreal :: "hypreal \ 'a::real_algebra_1 star"
  where [transfer_unfold]: "of_hypreal = *f* of_real"

lemma Standard_of_hypreal [simp]: "r \ Standard \ of_hypreal r \ Standard"
  by (simp add: of_hypreal_def)

lemma of_hypreal_0 [simp]: "of_hypreal 0 = 0"
  by transfer (rule of_real_0)

lemma of_hypreal_1 [simp]: "of_hypreal 1 = 1"
  by transfer (rule of_real_1)

lemma of_hypreal_add [simp]: "\x y. of_hypreal (x + y) = of_hypreal x + of_hypreal y"
  by transfer (rule of_real_add)

lemma of_hypreal_minus [simp]: "\x. of_hypreal (- x) = - of_hypreal x"
  by transfer (rule of_real_minus)

lemma of_hypreal_diff [simp]: "\x y. of_hypreal (x - y) = of_hypreal x - of_hypreal y"
  by transfer (rule of_real_diff)

lemma of_hypreal_mult [simp]: "\x y. of_hypreal (x * y) = of_hypreal x * of_hypreal y"
  by transfer (rule of_real_mult)

lemma of_hypreal_inverse [simp]:
  "\x. of_hypreal (inverse x) =
    inverse (of_hypreal x :: 'a::{real_div_algebra, division_ring} star)"
  by transfer (rule of_real_inverse)

lemma of_hypreal_divide [simp]:
  "\x y. of_hypreal (x / y) =
    (of_hypreal x / of_hypreal y :: 'a::{real_field, field} star)"
  by transfer (rule of_real_divide)

lemma of_hypreal_eq_iff [simp]: "\x y. (of_hypreal x = of_hypreal y) = (x = y)"
  by transfer (rule of_real_eq_iff)

lemma of_hypreal_eq_0_iff [simp]: "\x. (of_hypreal x = 0) = (x = 0)"
  by transfer (rule of_real_eq_0_iff)

subsection \<open>Properties of \<^term>\<open>starrel\<close>\<close>

lemma lemma_starrel_refl [simp]: "x \ starrel `` {x}"
  by (simp add: starrel_def)

lemma starrel_in_hypreal [simp]: "starrel``{x}\star"
  by (simp add: star_def starrel_def quotient_def, blast)

declare Abs_star_inject [simp] Abs_star_inverse [simp]
declare equiv_starrel [THEN eq_equiv_class_iff, simp]

subsection \<open>\<^term>\<open>hypreal_of_real\<close>: the Injection from \<^typ>\<open>real\<close> to \<^typ>\<open>hypreal\<close>\<close>

lemma inj_star_of: "inj star_of"
  by (rule inj_onI) simp

lemma mem_Rep_star_iff: "X \ Rep_star x \ x = star_n X"
  by (cases x) (simp add: star_n_def)

lemma Rep_star_star_n_iff [simp]: "X \ Rep_star (star_n Y) \ eventually (\n. Y n = X n) \"
  by (simp add: star_n_def)

lemma Rep_star_star_n: "X \ Rep_star (star_n X)"
  by simp

subsection \<open>Properties of \<^term>\<open>star_n\<close>\<close>

lemma star_n_add: "star_n X + star_n Y = star_n (\n. X n + Y n)"
  by (simp only: star_add_def starfun2_star_n)

lemma star_n_minus: "- star_n X = star_n (\n. -(X n))"
  by (simp only: star_minus_def starfun_star_n)

lemma star_n_diff: "star_n X - star_n Y = star_n (\n. X n - Y n)"
  by (simp only: star_diff_def starfun2_star_n)

lemma star_n_mult: "star_n X * star_n Y = star_n (\n. X n * Y n)"
  by (simp only: star_mult_def starfun2_star_n)

lemma star_n_inverse: "inverse (star_n X) = star_n (\n. inverse (X n))"
  by (simp only: star_inverse_def starfun_star_n)

lemma star_n_le: "star_n X \ star_n Y = eventually (\n. X n \ Y n) \"
  by (simp only: star_le_def starP2_star_n)

lemma star_n_less: "star_n X < star_n Y = eventually (\n. X n < Y n) \"
  by (simp only: star_less_def starP2_star_n)

lemma star_n_zero_num: "0 = star_n (\n. 0)"
  by (simp only: star_zero_def star_of_def)

lemma star_n_one_num: "1 = star_n (\n. 1)"
  by (simp only: star_one_def star_of_def)

lemma star_n_abs: "\star_n X\ = star_n (\n. \X n\)"
  by (simp only: star_abs_def starfun_star_n)

lemma hypreal_omega_gt_zero [simp]: "0 < \"
  by (simp add: omega_def star_n_zero_num star_n_less)

subsection \<open>Existence of Infinite Hyperreal Number\<close>

text \<open>Existence of infinite number not corresponding to any real number.
  Use assumption that member \<^term>\<open>\<U>\<close> is not finite.\<close>

lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \ \"
proof -
  have False if "\\<^sub>F n in \. x = 1 + real n" for x
  proof -
    have "finite {n::nat. x = 1 + real n}"
      by (simp add: finite_nat_set_iff_bounded_le) (metis add.commute nat_le_linear nat_le_real_less)
    then show False
      using FreeUltrafilterNat.finite that by blast
  qed
  then show ?thesis
    by (auto simp add: omega_def star_of_def star_n_eq_iff)
qed

text \<open>Existence of infinitesimal number also not corresponding to any real number.\<close>

lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \ \"
proof -
  have False if "\\<^sub>F n in \. x = inverse (1 + real n)" for x
  proof -
    have "finite {n::nat. x = inverse (1 + real n)}"
      by (simp add: finite_nat_set_iff_bounded_le) (metis add.commute inverse_inverse_eq linear nat_le_real_less of_nat_Suc)
    then show False
      using FreeUltrafilterNat.finite that by blast
  qed
  then show ?thesis
    by (auto simp: epsilon_def star_of_def star_n_eq_iff)
qed

lemma epsilon_ge_zero [simp]: "0 \ \"
  by (simp add: epsilon_def star_n_zero_num star_n_le)

lemma epsilon_not_zero: "\ \ 0"
  using hypreal_of_real_not_eq_epsilon by force

lemma epsilon_inverse_omega: "\ = inverse \"
  by (simp add: epsilon_def omega_def star_n_inverse)

lemma epsilon_gt_zero: "0 < \"
  by (simp add: epsilon_inverse_omega)

subsection \<open>Embedding the Naturals into the Hyperreals\<close>

abbreviation hypreal_of_nat :: "nat \ hypreal"
  where "hypreal_of_nat \ of_nat"

lemma SNat_eq: "Nats = {n. \N. n = hypreal_of_nat N}"
  by (simp add: Nats_def image_def)

text \<open>Naturals embedded in hyperreals: is a hyperreal c.f. NS extension.\<close>

lemma hypreal_of_nat: "hypreal_of_nat m = star_n (\n. real m)"
  by (simp add: star_of_def [symmetric])

declaration \<open>
  K (Lin_Arith.add_simps @{thms star_of_zero star_of_one
      star_of_numeral star_of_add
      star_of_minus star_of_diff star_of_mult}
  #> Lin_Arith.add_inj_thms @{thms star_of_le [THEN iffD2]
      star_of_less [THEN iffD2] star_of_eq [THEN iffD2]}
  #> Lin_Arith.add_inj_const (\<^const_name>\<open>StarDef.star_of\<close>, \<^typ>\<open>real \<Rightarrow> hypreal\<close>))
\<close>

simproc_setup fast_arith_hypreal ("(m::hypreal) < n" | "(m::hypreal) \ n" | "(m::hypreal) = n") =
  \<open>K Lin_Arith.simproc\<close>

subsection \<open>Exponentials on the Hyperreals\<close>

lemma hpowr_0 [simp]: "r ^ 0 = (1::hypreal)"
  for r :: hypreal
  by (rule power_0)

lemma hpowr_Suc [simp]: "r ^ (Suc n) = r * (r ^ n)"
  for r :: hypreal
  by (rule power_Suc)

lemma hrealpow_two: "r ^ Suc (Suc 0) = r * r"
  for r :: hypreal
  by simp

lemma hrealpow_two_le [simp]: "0 \ r ^ Suc (Suc 0)"
  for r :: hypreal
  by (auto simp add: zero_le_mult_iff)

lemma hrealpow_two_le_add_order [simp]: "0 \ u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
  for u v :: hypreal
  by (simp only: hrealpow_two_le add_nonneg_nonneg)

lemma hrealpow_two_le_add_order2 [simp]: "0 \ u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)"
  for u v w :: hypreal
  by (simp only: hrealpow_two_le add_nonneg_nonneg)

lemma hypreal_add_nonneg_eq_0_iff: "0 \ x \ 0 \ y \ x + y = 0 \ x = 0 \ y = 0"
  for x y :: hypreal
  by arith

(* FIXME: DELETE THESE *)
lemma hypreal_three_squares_add_zero_iff: "x * x + y * y + z * z = 0 \ x = 0 \ y = 0 \ z = 0"
  for x y z :: hypreal
  by (simp only: zero_le_square add_nonneg_nonneg hypreal_add_nonneg_eq_0_iff) auto

lemma hrealpow_three_squares_add_zero_iff [simp]:
  "x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = 0 \ x = 0 \ y = 0 \ z = 0"
  for x y z :: hypreal
  by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two)

(*FIXME: This and RealPow.abs_realpow_two should be replaced by an abstract
  result proved in Rings or Fields*)
lemma hrabs_hrealpow_two [simp]: "\x ^ Suc (Suc 0)\ = x ^ Suc (Suc 0)"
  for x :: hypreal
  by (simp add: abs_mult)

lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \ 2 ^ n"
  using power_increasing [of 0 n "2::hypreal"] by simp

lemma hrealpow: "star_n X ^ m = star_n (\n. (X n::real) ^ m)"
  by (induct m) (auto simp: star_n_one_num star_n_mult)

lemma hrealpow_sum_square_expand:
  "(x + y) ^ Suc (Suc 0) =
    x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0))) * x * y"
  for x y :: hypreal
  by (simp add: distrib_left distrib_right)

lemma power_hypreal_of_real_numeral:
  "(numeral v :: hypreal) ^ n = hypreal_of_real ((numeral v) ^ n)"
  by simp
declare power_hypreal_of_real_numeral [of _ "numeral w", simp] for w

lemma power_hypreal_of_real_neg_numeral:
  "(- numeral v :: hypreal) ^ n = hypreal_of_real ((- numeral v) ^ n)"
  by simp
declare power_hypreal_of_real_neg_numeral [of _ "numeral w", simp] for w
(*
lemma hrealpow_HFinite:
  fixes x :: "'a::{real_normed_algebra,power} star"
  shows "x \<in> HFinite ==> x ^ n \<in> HFinite"
apply (induct_tac "n")
apply (auto simp add: power_Suc intro: HFinite_mult)
done
*)

subsection \<open>Powers with Hypernatural Exponents\<close>

text \<open>Hypernatural powers of hyperreals.\<close>
definition pow :: "'a::power star \ nat star \ 'a star" (infixr "pow" 80)
  where hyperpow_def [transfer_unfold]: "R pow N = ( *f2* (^)) R N"

lemma Standard_hyperpow [simp]: "r \ Standard \ n \ Standard \ r pow n \ Standard"
  by (simp add: hyperpow_def)

lemma hyperpow: "star_n X pow star_n Y = star_n (\n. X n ^ Y n)"
  by (simp add: hyperpow_def starfun2_star_n)

lemma hyperpow_zero [simp]: "\n. (0::'a::{power,semiring_0} star) pow (n + (1::hypnat)) = 0"
  by transfer simp

lemma hyperpow_not_zero: "\r n. r \ (0::'a::{field} star) \ r pow n \ 0"
  by transfer (rule power_not_zero)

lemma hyperpow_inverse: "\r n. r \ (0::'a::field star) \ inverse (r pow n) = (inverse r) pow n"
  by transfer (rule power_inverse [symmetric])

lemma hyperpow_hrabs: "\r n. \r::'a::{linordered_idom} star\ pow n = \r pow n\"
  by transfer (rule power_abs [symmetric])

lemma hyperpow_add: "\r n m. (r::'a::monoid_mult star) pow (n + m) = (r pow n) * (r pow m)"
  by transfer (rule power_add)

lemma hyperpow_one [simp]: "\r. (r::'a::monoid_mult star) pow (1::hypnat) = r"
  by transfer (rule power_one_right)

lemma hyperpow_two: "\r. (r::'a::monoid_mult star) pow (2::hypnat) = r * r"
  by transfer (rule power2_eq_square)

lemma hyperpow_gt_zero: "\r n. (0::'a::{linordered_semidom} star) < r \ 0 < r pow n"
  by transfer (rule zero_less_power)

lemma hyperpow_ge_zero: "\r n. (0::'a::{linordered_semidom} star) \ r \ 0 \ r pow n"
  by transfer (rule zero_le_power)

lemma hyperpow_le: "\x y n. (0::'a::{linordered_semidom} star) < x \ x \ y \ x pow n \ y pow n"
  by transfer (rule power_mono [OF _ order_less_imp_le])

lemma hyperpow_eq_one [simp]: "\n. 1 pow n = (1::'a::monoid_mult star)"
  by transfer (rule power_one)

lemma hrabs_hyperpow_minus [simp]: "\(a::'a::linordered_idom star) n. \(-a) pow n\ = \a pow n\"
  by transfer (rule abs_power_minus)

lemma hyperpow_mult: "\r s n. (r * s::'a::comm_monoid_mult star) pow n = (r pow n) * (s pow n)"
  by transfer (rule power_mult_distrib)

lemma hyperpow_two_le [simp]: "\r. (0::'a::{monoid_mult,linordered_ring_strict} star) \ r pow 2"
  by (auto simp add: hyperpow_two zero_le_mult_iff)

lemma hyperpow_two_hrabs [simp]: "\x::'a::linordered_idom star\ pow 2 = x pow 2"
  by (simp add: hyperpow_hrabs)

lemma hyperpow_two_gt_one: "\r::'a::linordered_semidom star. 1 < r \ 1 < r pow 2"
  by transfer simp

lemma hyperpow_two_ge_one: "\r::'a::linordered_semidom star. 1 \ r \ 1 \ r pow 2"
  by transfer (rule one_le_power)

lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \ 2 pow n"
  by (metis hyperpow_eq_one hyperpow_le one_le_numeral zero_less_one)

lemma hyperpow_minus_one2 [simp]: "\n. (- 1) pow (2 * n) = (1::hypreal)"
  by transfer (rule power_minus1_even)

lemma hyperpow_less_le: "\r n N. (0::hypreal) \ r \ r \ 1 \ n < N \ r pow N \ r pow n"
  by transfer (rule power_decreasing [OF order_less_imp_le])

lemma hyperpow_SHNat_le:
  "0 \ r \ r \ (1::hypreal) \ N \ HNatInfinite \ \n\Nats. r pow N \ r pow n"
  by (auto intro!: hyperpow_less_le simp: HNatInfinite_iff)

lemma hyperpow_realpow: "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
  by transfer (rule refl)

lemma hyperpow_SReal [simp]: "(hypreal_of_real r) pow (hypnat_of_nat n) \ \"
  by (simp add: Reals_eq_Standard)

lemma hyperpow_zero_HNatInfinite [simp]: "N \ HNatInfinite \ (0::hypreal) pow N = 0"
  by (drule HNatInfinite_is_Suc, auto)

lemma hyperpow_le_le: "(0::hypreal) \ r \ r \ 1 \ n \ N \ r pow N \ r pow n"
  by (metis hyperpow_less_le le_less)

lemma hyperpow_Suc_le_self2: "(0::hypreal) \ r \ r < 1 \ r pow (n + (1::hypnat)) \ r"
  by (metis hyperpow_less_le hyperpow_one hypnat_add_self_le le_less)

lemma hyperpow_hypnat_of_nat: "\x. x pow hypnat_of_nat n = x ^ n"
  by transfer (rule refl)

lemma of_hypreal_hyperpow:
  "\x n. of_hypreal (x pow n) = (of_hypreal x::'a::{real_algebra_1} star) pow n"
  by transfer (rule of_real_power)

end

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.