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