src/HOL/Nonstandard_Analysis/HLog.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (21 months ago)
changeset 67003 49850a679c2c
parent 64604 2bf8cfc98c4d
child 67399 eab6ce8368fa
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      HOL/Nonstandard_Analysis/HLog.thy
     2     Author:     Jacques D. Fleuriot
     3     Copyright:  2000, 2001 University of Edinburgh
     4 *)
     5 
     6 section \<open>Logarithms: Non-Standard Version\<close>
     7 
     8 theory HLog
     9   imports HTranscendental
    10 begin
    11 
    12 
    13 (* should be in NSA.ML *)
    14 lemma epsilon_ge_zero [simp]: "0 \<le> \<epsilon>"
    15   by (simp add: epsilon_def star_n_zero_num star_n_le)
    16 
    17 lemma hpfinite_witness: "\<epsilon> \<in> {x. 0 \<le> x \<and> x \<in> HFinite}"
    18   by auto
    19 
    20 
    21 definition powhr :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal"  (infixr "powhr" 80)
    22   where [transfer_unfold]: "x powhr a = starfun2 (op powr) x a"
    23 
    24 definition hlog :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal"
    25   where [transfer_unfold]: "hlog a x = starfun2 log a x"
    26 
    27 lemma powhr: "(star_n X) powhr (star_n Y) = star_n (\<lambda>n. (X n) powr (Y n))"
    28   by (simp add: powhr_def starfun2_star_n)
    29 
    30 lemma powhr_one_eq_one [simp]: "\<And>a. 1 powhr a = 1"
    31   by transfer simp
    32 
    33 lemma powhr_mult: "\<And>a x y. 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x * y) powhr a = (x powhr a) * (y powhr a)"
    34   by transfer (simp add: powr_mult)
    35 
    36 lemma powhr_gt_zero [simp]: "\<And>a x. 0 < x powhr a \<longleftrightarrow> x \<noteq> 0"
    37   by transfer simp
    38 
    39 lemma powhr_not_zero [simp]: "\<And>a x. x powhr a \<noteq> 0 \<longleftrightarrow> x \<noteq> 0"
    40   by transfer simp
    41 
    42 lemma powhr_divide: "\<And>a x y. 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powhr a = (x powhr a) / (y powhr a)"
    43   by transfer (rule powr_divide)
    44 
    45 lemma powhr_add: "\<And>a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
    46   by transfer (rule powr_add)
    47 
    48 lemma powhr_powhr: "\<And>a b x. (x powhr a) powhr b = x powhr (a * b)"
    49   by transfer (rule powr_powr)
    50 
    51 lemma powhr_powhr_swap: "\<And>a b x. (x powhr a) powhr b = (x powhr b) powhr a"
    52   by transfer (rule powr_powr_swap)
    53 
    54 lemma powhr_minus: "\<And>a x. x powhr (- a) = inverse (x powhr a)"
    55   by transfer (rule powr_minus)
    56 
    57 lemma powhr_minus_divide: "x powhr (- a) = 1 / (x powhr a)"
    58   by (simp add: divide_inverse powhr_minus)
    59 
    60 lemma powhr_less_mono: "\<And>a b x. a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powhr a < x powhr b"
    61   by transfer simp
    62 
    63 lemma powhr_less_cancel: "\<And>a b x. x powhr a < x powhr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
    64   by transfer simp
    65 
    66 lemma powhr_less_cancel_iff [simp]: "1 < x \<Longrightarrow> x powhr a < x powhr b \<longleftrightarrow> a < b"
    67   by (blast intro: powhr_less_cancel powhr_less_mono)
    68 
    69 lemma powhr_le_cancel_iff [simp]: "1 < x \<Longrightarrow> x powhr a \<le> x powhr b \<longleftrightarrow> a \<le> b"
    70   by (simp add: linorder_not_less [symmetric])
    71 
    72 lemma hlog: "hlog (star_n X) (star_n Y) = star_n (\<lambda>n. log (X n) (Y n))"
    73   by (simp add: hlog_def starfun2_star_n)
    74 
    75 lemma hlog_starfun_ln: "\<And>x. ( *f* ln) x = hlog (( *f* exp) 1) x"
    76   by transfer (rule log_ln)
    77 
    78 lemma powhr_hlog_cancel [simp]: "\<And>a x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powhr (hlog a x) = x"
    79   by transfer simp
    80 
    81 lemma hlog_powhr_cancel [simp]: "\<And>a y. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a (a powhr y) = y"
    82   by transfer simp
    83 
    84 lemma hlog_mult:
    85   "\<And>a x y. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a (x * y) = hlog a x + hlog a y"
    86   by transfer (rule log_mult)
    87 
    88 lemma hlog_as_starfun: "\<And>a x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a x = ( *f* ln) x / ( *f* ln) a"
    89   by transfer (simp add: log_def)
    90 
    91 lemma hlog_eq_div_starfun_ln_mult_hlog:
    92   "\<And>a b x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow>
    93     hlog a x = (( *f* ln) b / ( *f* ln) a) * hlog b x"
    94   by transfer (rule log_eq_div_ln_mult_log)
    95 
    96 lemma powhr_as_starfun: "\<And>a x. x powhr a = (if x = 0 then 0 else ( *f* exp) (a * ( *f* real_ln) x))"
    97   by transfer (simp add: powr_def)
    98 
    99 lemma HInfinite_powhr:
   100   "x \<in> HInfinite \<Longrightarrow> 0 < x \<Longrightarrow> a \<in> HFinite - Infinitesimal \<Longrightarrow> 0 < a \<Longrightarrow> x powhr a \<in> HInfinite"
   101   by (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite
   102         HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite
   103       simp add: order_less_imp_le HInfinite_gt_zero_gt_one powhr_as_starfun zero_le_mult_iff)
   104 
   105 lemma hlog_hrabs_HInfinite_Infinitesimal:
   106   "x \<in> HFinite - Infinitesimal \<Longrightarrow> a \<in> HInfinite \<Longrightarrow> 0 < a \<Longrightarrow> hlog a \<bar>x\<bar> \<in> Infinitesimal"
   107   apply (frule HInfinite_gt_zero_gt_one)
   108    apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
   109       HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2
   110       simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero
   111       hlog_as_starfun divide_inverse)
   112   done
   113 
   114 lemma hlog_HInfinite_as_starfun: "a \<in> HInfinite \<Longrightarrow> 0 < a \<Longrightarrow> hlog a x = ( *f* ln) x / ( *f* ln) a"
   115   by (rule hlog_as_starfun) auto
   116 
   117 lemma hlog_one [simp]: "\<And>a. hlog a 1 = 0"
   118   by transfer simp
   119 
   120 lemma hlog_eq_one [simp]: "\<And>a. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a a = 1"
   121   by transfer (rule log_eq_one)
   122 
   123 lemma hlog_inverse: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> hlog a (inverse x) = - hlog a x"
   124   by (rule add_left_cancel [of "hlog a x", THEN iffD1]) (simp add: hlog_mult [symmetric])
   125 
   126 lemma hlog_divide: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a (x / y) = hlog a x - hlog a y"
   127   by (simp add: hlog_mult hlog_inverse divide_inverse)
   128 
   129 lemma hlog_less_cancel_iff [simp]:
   130   "\<And>a x y. 1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a x < hlog a y \<longleftrightarrow> x < y"
   131   by transfer simp
   132 
   133 lemma hlog_le_cancel_iff [simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a x \<le> hlog a y \<longleftrightarrow> x \<le> y"
   134   by (simp add: linorder_not_less [symmetric])
   135 
   136 end