Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: HLog.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Nonstandard_Analysis/HLog.thy
    Author:     Jacques D. Fleuriot
    Copyright:  2000, 2001 University of Edinburgh
*)

section \<open>Logarithms: Non-Standard Version\<close>

theory HLog
  imports HTranscendental
begin

definition powhr :: "hypreal \ hypreal \ hypreal" (infixr "powhr" 80)
  where [transfer_unfold]: "x powhr a = starfun2 (powr) x a"

definition hlog :: "hypreal \ hypreal \ hypreal"
  where [transfer_unfold]: "hlog a x = starfun2 log a x"

lemma powhr: "(star_n X) powhr (star_n Y) = star_n (\n. (X n) powr (Y n))"
  by (simp add: powhr_def starfun2_star_n)

lemma powhr_one_eq_one [simp]: "\a. 1 powhr a = 1"
  by transfer simp

lemma powhr_mult: "\a x y. 0 < x \ 0 < y \ (x * y) powhr a = (x powhr a) * (y powhr a)"
  by transfer (simp add: powr_mult)

lemma powhr_gt_zero [simp]: "\a x. 0 < x powhr a \ x \ 0"
  by transfer simp

lemma powhr_not_zero [simp]: "\a x. x powhr a \ 0 \ x \ 0"
  by transfer simp

lemma powhr_divide: "\a x y. 0 \ x \ 0 \ y \ (x / y) powhr a = (x powhr a) / (y powhr a)"
  by transfer (rule powr_divide)

lemma powhr_add: "\a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
  by transfer (rule powr_add)

lemma powhr_powhr: "\a b x. (x powhr a) powhr b = x powhr (a * b)"
  by transfer (rule powr_powr)

lemma powhr_powhr_swap: "\a b x. (x powhr a) powhr b = (x powhr b) powhr a"
  by transfer (rule powr_powr_swap)

lemma powhr_minus: "\a x. x powhr (- a) = inverse (x powhr a)"
  by transfer (rule powr_minus)

lemma powhr_minus_divide: "x powhr (- a) = 1 / (x powhr a)"
  by (simp add: divide_inverse powhr_minus)

lemma powhr_less_mono: "\a b x. a < b \ 1 < x \ x powhr a < x powhr b"
  by transfer simp

lemma powhr_less_cancel: "\a b x. x powhr a < x powhr b \ 1 < x \ a < b"
  by transfer simp

lemma powhr_less_cancel_iff [simp]: "1 < x \ x powhr a < x powhr b \ a < b"
  by (blast intro: powhr_less_cancel powhr_less_mono)

lemma powhr_le_cancel_iff [simp]: "1 < x \ x powhr a \ x powhr b \ a \ b"
  by (simp add: linorder_not_less [symmetric])

lemma hlog: "hlog (star_n X) (star_n Y) = star_n (\n. log (X n) (Y n))"
  by (simp add: hlog_def starfun2_star_n)

lemma hlog_starfun_ln: "\x. ( *f* ln) x = hlog (( *f* exp) 1) x"
  by transfer (rule log_ln)

lemma powhr_hlog_cancel [simp]: "\a x. 0 < a \ a \ 1 \ 0 < x \ a powhr (hlog a x) = x"
  by transfer simp

lemma hlog_powhr_cancel [simp]: "\a y. 0 < a \ a \ 1 \ hlog a (a powhr y) = y"
  by transfer simp

lemma hlog_mult:
  "\a x y. 0 < a \ a \ 1 \ 0 < x \ 0 < y \ hlog a (x * y) = hlog a x + hlog a y"
  by transfer (rule log_mult)

lemma hlog_as_starfun: "\a x. 0 < a \ a \ 1 \ hlog a x = ( *f* ln) x / ( *f* ln) a"
  by transfer (simp add: log_def)

lemma hlog_eq_div_starfun_ln_mult_hlog:
  "\a b x. 0 < a \ a \ 1 \ 0 < b \ b \ 1 \ 0 < x \
    hlog a x = (( *f* ln) b / ( *f* ln) a) * hlog b x"
  by transfer (rule log_eq_div_ln_mult_log)

lemma powhr_as_starfun: "\a x. x powhr a = (if x = 0 then 0 else ( *f* exp) (a * ( *f* real_ln) x))"
  by transfer (simp add: powr_def)

lemma HInfinite_powhr:
  "x \ HInfinite \ 0 < x \ a \ HFinite - Infinitesimal \ 0 < a \ x powhr a \ HInfinite"
  by (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite
        HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite
      simp add: order_less_imp_le HInfinite_gt_zero_gt_one powhr_as_starfun zero_le_mult_iff)

lemma hlog_hrabs_HInfinite_Infinitesimal:
  "x \ HFinite - Infinitesimal \ a \ HInfinite \ 0 < a \ hlog a \x\ \ Infinitesimal"
  apply (frule HInfinite_gt_zero_gt_one)
   apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
      HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2
      simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero
      hlog_as_starfun divide_inverse)
  done

lemma hlog_HInfinite_as_starfun: "a \ HInfinite \ 0 < a \ hlog a x = ( *f* ln) x / ( *f* ln) a"
  by (rule hlog_as_starfun) auto

lemma hlog_one [simp]: "\a. hlog a 1 = 0"
  by transfer simp

lemma hlog_eq_one [simp]: "\a. 0 < a \ a \ 1 \ hlog a a = 1"
  by transfer (rule log_eq_one)

lemma hlog_inverse: "0 < a \ a \ 1 \ 0 < x \ hlog a (inverse x) = - hlog a x"
  by (rule add_left_cancel [of "hlog a x", THEN iffD1]) (simp add: hlog_mult [symmetric])

lemma hlog_divide: "0 < a \ a \ 1 \ 0 < x \ 0 < y \ hlog a (x / y) = hlog a x - hlog a y"
  by (simp add: hlog_mult hlog_inverse divide_inverse)

lemma hlog_less_cancel_iff [simp]:
  "\a x y. 1 < a \ 0 < x \ 0 < y \ hlog a x < hlog a y \ x < y"
  by transfer simp

lemma hlog_le_cancel_iff [simp]: "1 < a \ 0 < x \ 0 < y \ hlog a x \ hlog a y \ x \ y"
  by (simp add: linorder_not_less [symmetric])

end

¤ Dauer der Verarbeitung: 0.11 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.