src/HOL/NSA/HLog.thy
author paulson <lp15@cam.ac.uk>
Sat Apr 11 11:56:40 2015 +0100 (2015-04-11)
changeset 60017 b785d6d06430
parent 58878 f962e42e324d
child 61945 1135b8de26c3
permissions -rw-r--r--
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
huffman@27468
     1
(*  Title       : HLog.thy
huffman@27468
     2
    Author      : Jacques D. Fleuriot
huffman@27468
     3
    Copyright   : 2000,2001 University of Edinburgh
huffman@27468
     4
*)
huffman@27468
     5
wenzelm@58878
     6
section{*Logarithms: Non-Standard Version*}
huffman@27468
     7
huffman@27468
     8
theory HLog
hoelzl@51525
     9
imports HTranscendental
huffman@27468
    10
begin
huffman@27468
    11
huffman@27468
    12
huffman@27468
    13
(* should be in NSA.ML *)
huffman@27468
    14
lemma epsilon_ge_zero [simp]: "0 \<le> epsilon"
huffman@27468
    15
by (simp add: epsilon_def star_n_zero_num star_n_le)
huffman@27468
    16
huffman@27468
    17
lemma hpfinite_witness: "epsilon : {x. 0 \<le> x & x : HFinite}"
huffman@27468
    18
by auto
huffman@27468
    19
huffman@27468
    20
huffman@27468
    21
definition
huffman@27468
    22
  powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80) where
haftmann@37765
    23
  [transfer_unfold]: "x powhr a = starfun2 (op powr) x a"
huffman@27468
    24
  
huffman@27468
    25
definition
huffman@27468
    26
  hlog :: "[hypreal,hypreal] => hypreal" where
haftmann@37765
    27
  [transfer_unfold]: "hlog a x = starfun2 log a x"
huffman@27468
    28
huffman@27468
    29
lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
huffman@27468
    30
by (simp add: powhr_def starfun2_star_n)
huffman@27468
    31
huffman@27468
    32
lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1"
huffman@27468
    33
by (transfer, simp)
huffman@27468
    34
huffman@27468
    35
lemma powhr_mult:
huffman@27468
    36
  "!!a x y. [| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
lp15@60017
    37
by (transfer, simp add: powr_mult)
huffman@27468
    38
lp15@60017
    39
lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a \<longleftrightarrow> x \<noteq> 0"
huffman@27468
    40
by (transfer, simp)
huffman@27468
    41
lp15@60017
    42
lemma powhr_not_zero [simp]: "\<And>a x. x powhr a \<noteq> 0 \<longleftrightarrow> x \<noteq> 0"
lp15@60017
    43
by transfer simp
huffman@27468
    44
huffman@27468
    45
lemma powhr_divide:
huffman@27468
    46
  "!!a x y. [| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
huffman@27468
    47
by (transfer, rule powr_divide)
huffman@27468
    48
huffman@27468
    49
lemma powhr_add: "!!a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
huffman@27468
    50
by (transfer, rule powr_add)
huffman@27468
    51
huffman@27468
    52
lemma powhr_powhr: "!!a b x. (x powhr a) powhr b = x powhr (a * b)"
huffman@27468
    53
by (transfer, rule powr_powr)
huffman@27468
    54
huffman@27468
    55
lemma powhr_powhr_swap: "!!a b x. (x powhr a) powhr b = (x powhr b) powhr a"
huffman@27468
    56
by (transfer, rule powr_powr_swap)
huffman@27468
    57
huffman@27468
    58
lemma powhr_minus: "!!a x. x powhr (-a) = inverse (x powhr a)"
huffman@27468
    59
by (transfer, rule powr_minus)
huffman@27468
    60
huffman@27468
    61
lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)"
huffman@27468
    62
by (simp add: divide_inverse powhr_minus)
huffman@27468
    63
huffman@27468
    64
lemma powhr_less_mono: "!!a b x. [| a < b; 1 < x |] ==> x powhr a < x powhr b"
huffman@27468
    65
by (transfer, simp)
huffman@27468
    66
huffman@27468
    67
lemma powhr_less_cancel: "!!a b x. [| x powhr a < x powhr b; 1 < x |] ==> a < b"
huffman@27468
    68
by (transfer, simp)
huffman@27468
    69
huffman@27468
    70
lemma powhr_less_cancel_iff [simp]:
huffman@27468
    71
     "1 < x ==> (x powhr a < x powhr b) = (a < b)"
huffman@27468
    72
by (blast intro: powhr_less_cancel powhr_less_mono)
huffman@27468
    73
huffman@27468
    74
lemma powhr_le_cancel_iff [simp]:
huffman@27468
    75
     "1 < x ==> (x powhr a \<le> x powhr b) = (a \<le> b)"
huffman@27468
    76
by (simp add: linorder_not_less [symmetric])
huffman@27468
    77
huffman@27468
    78
lemma hlog:
huffman@27468
    79
     "hlog (star_n X) (star_n Y) =  
huffman@27468
    80
      star_n (%n. log (X n) (Y n))"
huffman@27468
    81
by (simp add: hlog_def starfun2_star_n)
huffman@27468
    82
huffman@27468
    83
lemma hlog_starfun_ln: "!!x. ( *f* ln) x = hlog (( *f* exp) 1) x"
huffman@27468
    84
by (transfer, rule log_ln)
huffman@27468
    85
huffman@27468
    86
lemma powhr_hlog_cancel [simp]:
huffman@27468
    87
     "!!a x. [| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x"
huffman@27468
    88
by (transfer, simp)
huffman@27468
    89
huffman@27468
    90
lemma hlog_powhr_cancel [simp]:
huffman@27468
    91
     "!!a y. [| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y"
huffman@27468
    92
by (transfer, simp)
huffman@27468
    93
huffman@27468
    94
lemma hlog_mult:
huffman@27468
    95
     "!!a x y. [| 0 < a; a \<noteq> 1; 0 < x; 0 < y  |]  
huffman@27468
    96
      ==> hlog a (x * y) = hlog a x + hlog a y"
huffman@27468
    97
by (transfer, rule log_mult)
huffman@27468
    98
huffman@27468
    99
lemma hlog_as_starfun:
huffman@27468
   100
     "!!a x. [| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
huffman@27468
   101
by (transfer, simp add: log_def)
huffman@27468
   102
huffman@27468
   103
lemma hlog_eq_div_starfun_ln_mult_hlog:
huffman@27468
   104
     "!!a b x. [| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]  
huffman@27468
   105
      ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
huffman@27468
   106
by (transfer, rule log_eq_div_ln_mult_log)
huffman@27468
   107
lp15@60017
   108
lemma powhr_as_starfun: "!!a x. x powhr a = (if x=0 then 0 else ( *f* exp) (a * ( *f* real_ln) x))"
lp15@60017
   109
  by (transfer, simp add: powr_def)
huffman@27468
   110
huffman@27468
   111
lemma HInfinite_powhr:
huffman@27468
   112
     "[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal;  
huffman@27468
   113
         0 < a |] ==> x powhr a : HInfinite"
huffman@27468
   114
apply (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite 
huffman@27468
   115
       simp add: order_less_imp_le HInfinite_gt_zero_gt_one powhr_as_starfun zero_le_mult_iff)
huffman@27468
   116
done
huffman@27468
   117
huffman@27468
   118
lemma hlog_hrabs_HInfinite_Infinitesimal:
huffman@27468
   119
     "[| x : HFinite - Infinitesimal; a : HInfinite; 0 < a |]  
huffman@27468
   120
      ==> hlog a (abs x) : Infinitesimal"
huffman@27468
   121
apply (frule HInfinite_gt_zero_gt_one)
huffman@27468
   122
apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
huffman@27468
   123
            HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2 
huffman@27468
   124
        simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero 
lp15@56225
   125
          hlog_as_starfun divide_inverse)
huffman@27468
   126
done
huffman@27468
   127
huffman@27468
   128
lemma hlog_HInfinite_as_starfun:
huffman@27468
   129
     "[| a : HInfinite; 0 < a |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
huffman@27468
   130
by (rule hlog_as_starfun, auto)
huffman@27468
   131
huffman@27468
   132
lemma hlog_one [simp]: "!!a. hlog a 1 = 0"
huffman@27468
   133
by (transfer, simp)
huffman@27468
   134
huffman@27468
   135
lemma hlog_eq_one [simp]: "!!a. [| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1"
huffman@27468
   136
by (transfer, rule log_eq_one)
huffman@27468
   137
huffman@27468
   138
lemma hlog_inverse:
huffman@27468
   139
     "[| 0 < a; a \<noteq> 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x"
huffman@27468
   140
apply (rule add_left_cancel [of "hlog a x", THEN iffD1])
huffman@27468
   141
apply (simp add: hlog_mult [symmetric])
huffman@27468
   142
done
huffman@27468
   143
huffman@27468
   144
lemma hlog_divide:
huffman@27468
   145
     "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> hlog a (x/y) = hlog a x - hlog a y"
huffman@27468
   146
by (simp add: hlog_mult hlog_inverse divide_inverse)
huffman@27468
   147
huffman@27468
   148
lemma hlog_less_cancel_iff [simp]:
huffman@27468
   149
     "!!a x y. [| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
huffman@27468
   150
by (transfer, simp)
huffman@27468
   151
huffman@27468
   152
lemma hlog_le_cancel_iff [simp]:
huffman@27468
   153
     "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x \<le> hlog a y) = (x \<le> y)"
huffman@27468
   154
by (simp add: linorder_not_less [symmetric])
huffman@27468
   155
huffman@27468
   156
end