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.
     1 (*  Title       : HLog.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 2000,2001 University of Edinburgh
     4 *)
     5 
     6 section{*Logarithms: Non-Standard Version*}
     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 : {x. 0 \<le> x & x : HFinite}"
    18 by auto
    19 
    20 
    21 definition
    22   powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80) where
    23   [transfer_unfold]: "x powhr a = starfun2 (op powr) x a"
    24   
    25 definition
    26   hlog :: "[hypreal,hypreal] => hypreal" where
    27   [transfer_unfold]: "hlog a x = starfun2 log a x"
    28 
    29 lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
    30 by (simp add: powhr_def starfun2_star_n)
    31 
    32 lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1"
    33 by (transfer, simp)
    34 
    35 lemma powhr_mult:
    36   "!!a x y. [| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
    37 by (transfer, simp add: powr_mult)
    38 
    39 lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a \<longleftrightarrow> x \<noteq> 0"
    40 by (transfer, simp)
    41 
    42 lemma powhr_not_zero [simp]: "\<And>a x. x powhr a \<noteq> 0 \<longleftrightarrow> x \<noteq> 0"
    43 by transfer simp
    44 
    45 lemma powhr_divide:
    46   "!!a x y. [| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
    47 by (transfer, rule powr_divide)
    48 
    49 lemma powhr_add: "!!a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
    50 by (transfer, rule powr_add)
    51 
    52 lemma powhr_powhr: "!!a b x. (x powhr a) powhr b = x powhr (a * b)"
    53 by (transfer, rule powr_powr)
    54 
    55 lemma powhr_powhr_swap: "!!a b x. (x powhr a) powhr b = (x powhr b) powhr a"
    56 by (transfer, rule powr_powr_swap)
    57 
    58 lemma powhr_minus: "!!a x. x powhr (-a) = inverse (x powhr a)"
    59 by (transfer, rule powr_minus)
    60 
    61 lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)"
    62 by (simp add: divide_inverse powhr_minus)
    63 
    64 lemma powhr_less_mono: "!!a b x. [| a < b; 1 < x |] ==> x powhr a < x powhr b"
    65 by (transfer, simp)
    66 
    67 lemma powhr_less_cancel: "!!a b x. [| x powhr a < x powhr b; 1 < x |] ==> a < b"
    68 by (transfer, simp)
    69 
    70 lemma powhr_less_cancel_iff [simp]:
    71      "1 < x ==> (x powhr a < x powhr b) = (a < b)"
    72 by (blast intro: powhr_less_cancel powhr_less_mono)
    73 
    74 lemma powhr_le_cancel_iff [simp]:
    75      "1 < x ==> (x powhr a \<le> x powhr b) = (a \<le> b)"
    76 by (simp add: linorder_not_less [symmetric])
    77 
    78 lemma hlog:
    79      "hlog (star_n X) (star_n Y) =  
    80       star_n (%n. log (X n) (Y n))"
    81 by (simp add: hlog_def starfun2_star_n)
    82 
    83 lemma hlog_starfun_ln: "!!x. ( *f* ln) x = hlog (( *f* exp) 1) x"
    84 by (transfer, rule log_ln)
    85 
    86 lemma powhr_hlog_cancel [simp]:
    87      "!!a x. [| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x"
    88 by (transfer, simp)
    89 
    90 lemma hlog_powhr_cancel [simp]:
    91      "!!a y. [| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y"
    92 by (transfer, simp)
    93 
    94 lemma hlog_mult:
    95      "!!a x y. [| 0 < a; a \<noteq> 1; 0 < x; 0 < y  |]  
    96       ==> hlog a (x * y) = hlog a x + hlog a y"
    97 by (transfer, rule log_mult)
    98 
    99 lemma hlog_as_starfun:
   100      "!!a x. [| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
   101 by (transfer, simp add: log_def)
   102 
   103 lemma hlog_eq_div_starfun_ln_mult_hlog:
   104      "!!a b x. [| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]  
   105       ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
   106 by (transfer, rule log_eq_div_ln_mult_log)
   107 
   108 lemma powhr_as_starfun: "!!a x. x powhr a = (if x=0 then 0 else ( *f* exp) (a * ( *f* real_ln) x))"
   109   by (transfer, simp add: powr_def)
   110 
   111 lemma HInfinite_powhr:
   112      "[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal;  
   113          0 < a |] ==> x powhr a : HInfinite"
   114 apply (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite 
   115        simp add: order_less_imp_le HInfinite_gt_zero_gt_one powhr_as_starfun zero_le_mult_iff)
   116 done
   117 
   118 lemma hlog_hrabs_HInfinite_Infinitesimal:
   119      "[| x : HFinite - Infinitesimal; a : HInfinite; 0 < a |]  
   120       ==> hlog a (abs x) : Infinitesimal"
   121 apply (frule HInfinite_gt_zero_gt_one)
   122 apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
   123             HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2 
   124         simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero 
   125           hlog_as_starfun divide_inverse)
   126 done
   127 
   128 lemma hlog_HInfinite_as_starfun:
   129      "[| a : HInfinite; 0 < a |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
   130 by (rule hlog_as_starfun, auto)
   131 
   132 lemma hlog_one [simp]: "!!a. hlog a 1 = 0"
   133 by (transfer, simp)
   134 
   135 lemma hlog_eq_one [simp]: "!!a. [| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1"
   136 by (transfer, rule log_eq_one)
   137 
   138 lemma hlog_inverse:
   139      "[| 0 < a; a \<noteq> 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x"
   140 apply (rule add_left_cancel [of "hlog a x", THEN iffD1])
   141 apply (simp add: hlog_mult [symmetric])
   142 done
   143 
   144 lemma hlog_divide:
   145      "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> hlog a (x/y) = hlog a x - hlog a y"
   146 by (simp add: hlog_mult hlog_inverse divide_inverse)
   147 
   148 lemma hlog_less_cancel_iff [simp]:
   149      "!!a x y. [| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
   150 by (transfer, simp)
   151 
   152 lemma hlog_le_cancel_iff [simp]:
   153      "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x \<le> hlog a y) = (x \<le> y)"
   154 by (simp add: linorder_not_less [symmetric])
   155 
   156 end