src/HOL/Hyperreal/HLog.thy
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 14468 6be497cacab5
child 15140 322485b816ac
permissions -rw-r--r--
New theory header syntax.
     1 (*  Title       : HLog.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 2000,2001 University of Edinburgh
     4 *)
     5 
     6 header{*Logarithms: Non-Standard Version*}
     7 
     8 theory HLog
     9 import Log 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 hypreal_zero_num hypreal_le)
    16 
    17 lemma hpfinite_witness: "epsilon : {x. 0 \<le> x & x : HFinite}"
    18 by auto
    19 
    20 
    21 constdefs
    22 
    23     powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80)
    24     "x powhr a == ( *f* exp) (a * ( *f* ln) x)"
    25   
    26     hlog :: "[hypreal,hypreal] => hypreal"
    27     "hlog a x == Abs_hypreal(\<Union>A \<in> Rep_hypreal(a).\<Union>X \<in> Rep_hypreal(x).
    28 			     hyprel `` {%n. log (A n) (X n)})"
    29 
    30 
    31 lemma powhr: 
    32     "(Abs_hypreal(hyprel `` {X})) powhr (Abs_hypreal(hyprel `` {Y})) =  
    33      Abs_hypreal(hyprel `` {%n.  (X n) powr (Y n)})"
    34 by (simp add: powhr_def starfun hypreal_mult powr_def)
    35 
    36 lemma powhr_one_eq_one [simp]: "1 powhr a = 1"
    37 apply (cases a)
    38 apply (simp add: powhr hypreal_one_num)
    39 done
    40 
    41 lemma powhr_mult:
    42      "[| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
    43 apply (cases x, cases y, cases a)
    44 apply (simp add: powhr hypreal_zero_num hypreal_mult hypreal_less, ultra)
    45 apply (simp add: powr_mult) 
    46 done
    47 
    48 lemma powhr_gt_zero [simp]: "0 < x powhr a"
    49 apply (cases a, cases x)
    50 apply (simp add: hypreal_zero_def powhr hypreal_less hypreal_zero_num)
    51 done
    52 
    53 lemma powhr_not_zero [simp]: "x powhr a \<noteq> 0"
    54 by (rule powhr_gt_zero [THEN hypreal_not_refl2, THEN not_sym])
    55 
    56 lemma hypreal_divide: 
    57      "(Abs_hypreal(hyprel `` {X}))/(Abs_hypreal(hyprel `` {Y})) =  
    58       (Abs_hypreal(hyprel `` {%n. (X n)/(Y n)}))"
    59 by (simp add: divide_inverse hypreal_zero_num hypreal_inverse hypreal_mult) 
    60 
    61 lemma powhr_divide:
    62      "[| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
    63 apply (cases x, cases y, cases a)
    64 apply (simp add: powhr hypreal_divide hypreal_zero_num hypreal_less, ultra)
    65 apply (simp add: powr_divide)
    66 done
    67 
    68 lemma powhr_add: "x powhr (a + b) = (x powhr a) * (x powhr b)"
    69 apply (cases x, cases b, cases a)
    70 apply (simp add: powhr hypreal_add hypreal_mult powr_add)
    71 done
    72 
    73 lemma powhr_powhr: "(x powhr a) powhr b = x powhr (a * b)"
    74 apply (cases x, cases b, cases a)
    75 apply (simp add: powhr hypreal_mult powr_powr)
    76 done
    77 
    78 lemma powhr_powhr_swap: "(x powhr a) powhr b = (x powhr b) powhr a"
    79 apply (cases x, cases b, cases a)
    80 apply (simp add: powhr powr_powr_swap)
    81 done
    82 
    83 lemma powhr_minus: "x powhr (-a) = inverse (x powhr a)"
    84 apply (cases x, cases a)
    85 apply (simp add: powhr hypreal_minus hypreal_inverse hypreal_less powr_minus)
    86 done
    87 
    88 lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)"
    89 by (simp add: divide_inverse powhr_minus)
    90 
    91 lemma powhr_less_mono: "[| a < b; 1 < x |] ==> x powhr a < x powhr b"
    92 apply (cases x, cases a, cases b)
    93 apply (simp add: powhr hypreal_one_num hypreal_less, ultra)
    94 done
    95 
    96 lemma powhr_less_cancel: "[| x powhr a < x powhr b; 1 < x |] ==> a < b"
    97 apply (cases x, cases a, cases b)
    98 apply (simp add: powhr hypreal_one_num hypreal_less, ultra)
    99 done
   100 
   101 lemma powhr_less_cancel_iff [simp]:
   102      "1 < x ==> (x powhr a < x powhr b) = (a < b)"
   103 by (blast intro: powhr_less_cancel powhr_less_mono)
   104 
   105 lemma powhr_le_cancel_iff [simp]:
   106      "1 < x ==> (x powhr a \<le> x powhr b) = (a \<le> b)"
   107 by (simp add: linorder_not_less [symmetric])
   108 
   109 lemma hlog: 
   110      "hlog (Abs_hypreal(hyprel `` {X})) (Abs_hypreal(hyprel `` {Y})) =  
   111       Abs_hypreal(hyprel `` {%n. log (X n) (Y n)})"
   112 apply (simp add: hlog_def)
   113 apply (rule arg_cong [where f=Abs_hypreal], auto, ultra)
   114 done
   115 
   116 lemma hlog_starfun_ln: "( *f* ln) x = hlog (( *f* exp) 1) x"
   117 apply (cases x)
   118 apply (simp add: starfun hlog log_ln hypreal_one_num)
   119 done
   120 
   121 lemma powhr_hlog_cancel [simp]:
   122      "[| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x"
   123 apply (cases x, cases a)
   124 apply (simp add: hlog powhr hypreal_zero_num hypreal_less hypreal_one_num, ultra)
   125 done
   126 
   127 lemma hlog_powhr_cancel [simp]:
   128      "[| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y"
   129 apply (cases y, cases a)
   130 apply (simp add: hlog powhr hypreal_zero_num hypreal_less hypreal_one_num, ultra)
   131 apply (auto intro: log_powr_cancel) 
   132 done
   133 
   134 lemma hlog_mult:
   135      "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y  |]  
   136       ==> hlog a (x * y) = hlog a x + hlog a y"
   137 apply (cases x, cases y, cases a)
   138 apply (simp add: hlog powhr hypreal_zero_num hypreal_one_num hypreal_less hypreal_add hypreal_mult, ultra)
   139 apply (simp add: log_mult)
   140 done
   141 
   142 lemma hlog_as_starfun:
   143      "[| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
   144 apply (cases x, cases a)
   145 apply (simp add: hlog starfun hypreal_zero_num hypreal_one_num hypreal_divide log_def)
   146 done
   147 
   148 lemma hlog_eq_div_starfun_ln_mult_hlog:
   149      "[| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]  
   150       ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
   151 apply (cases x, cases a, cases b)
   152 apply (simp add: hlog starfun hypreal_zero_num hypreal_one_num hypreal_less hypreal_divide hypreal_mult, ultra)
   153 apply (auto dest: log_eq_div_ln_mult_log) 
   154 done
   155 
   156 lemma powhr_as_starfun: "x powhr a = ( *f* exp) (a * ( *f* ln) x)"
   157 apply (cases a, cases x)
   158 apply (simp add: powhr starfun hypreal_mult powr_def)
   159 done
   160 
   161 lemma HInfinite_powhr:
   162      "[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal;  
   163          0 < a |] ==> x powhr a : HInfinite"
   164 apply (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite 
   165        simp add: order_less_imp_le HInfinite_gt_zero_gt_one powhr_as_starfun zero_le_mult_iff)
   166 done
   167 
   168 lemma hlog_hrabs_HInfinite_Infinitesimal:
   169      "[| x : HFinite - Infinitesimal; a : HInfinite; 0 < a |]  
   170       ==> hlog a (abs x) : Infinitesimal"
   171 apply (frule HInfinite_gt_zero_gt_one)
   172 apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
   173             HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2 
   174         simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero 
   175           hlog_as_starfun hypreal_not_refl2 [THEN not_sym] divide_inverse)
   176 done
   177 
   178 lemma hlog_HInfinite_as_starfun:
   179      "[| a : HInfinite; 0 < a |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
   180 by (rule hlog_as_starfun, auto)
   181 
   182 lemma hlog_one [simp]: "hlog a 1 = 0"
   183 apply (cases a)
   184 apply (simp add: hypreal_one_num hypreal_zero_num hlog)
   185 done
   186 
   187 lemma hlog_eq_one [simp]: "[| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1"
   188 apply (cases a)
   189 apply (simp add: hypreal_one_num hypreal_zero_num hlog hypreal_less, ultra)
   190 apply (auto intro: log_eq_one) 
   191 done
   192 
   193 lemma hlog_inverse:
   194      "[| 0 < a; a \<noteq> 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x"
   195 apply (rule add_left_cancel [of "hlog a x", THEN iffD1])
   196 apply (simp add: hlog_mult [symmetric])
   197 done
   198 
   199 lemma hlog_divide:
   200      "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> hlog a (x/y) = hlog a x - hlog a y"
   201 by (simp add: hlog_mult hlog_inverse divide_inverse)
   202 
   203 lemma hlog_less_cancel_iff [simp]:
   204      "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
   205 apply (cases a, cases x, cases y)
   206 apply (auto simp add: hlog hypreal_less hypreal_zero_num hypreal_one_num, ultra+)
   207 done
   208 
   209 lemma hlog_le_cancel_iff [simp]:
   210      "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x \<le> hlog a y) = (x \<le> y)"
   211 by (simp add: linorder_not_less [symmetric])
   212 
   213 
   214 ML
   215 {*
   216 val powhr = thm "powhr";
   217 val powhr_one_eq_one = thm "powhr_one_eq_one";
   218 val powhr_mult = thm "powhr_mult";
   219 val powhr_gt_zero = thm "powhr_gt_zero";
   220 val powhr_not_zero = thm "powhr_not_zero";
   221 val hypreal_divide = thm "hypreal_divide";
   222 val powhr_divide = thm "powhr_divide";
   223 val powhr_add = thm "powhr_add";
   224 val powhr_powhr = thm "powhr_powhr";
   225 val powhr_powhr_swap = thm "powhr_powhr_swap";
   226 val powhr_minus = thm "powhr_minus";
   227 val powhr_minus_divide = thm "powhr_minus_divide";
   228 val powhr_less_mono = thm "powhr_less_mono";
   229 val powhr_less_cancel = thm "powhr_less_cancel";
   230 val powhr_less_cancel_iff = thm "powhr_less_cancel_iff";
   231 val powhr_le_cancel_iff = thm "powhr_le_cancel_iff";
   232 val hlog = thm "hlog";
   233 val hlog_starfun_ln = thm "hlog_starfun_ln";
   234 val powhr_hlog_cancel = thm "powhr_hlog_cancel";
   235 val hlog_powhr_cancel = thm "hlog_powhr_cancel";
   236 val hlog_mult = thm "hlog_mult";
   237 val hlog_as_starfun = thm "hlog_as_starfun";
   238 val hlog_eq_div_starfun_ln_mult_hlog = thm "hlog_eq_div_starfun_ln_mult_hlog";
   239 val powhr_as_starfun = thm "powhr_as_starfun";
   240 val HInfinite_powhr = thm "HInfinite_powhr";
   241 val hlog_hrabs_HInfinite_Infinitesimal = thm "hlog_hrabs_HInfinite_Infinitesimal";
   242 val hlog_HInfinite_as_starfun = thm "hlog_HInfinite_as_starfun";
   243 val hlog_one = thm "hlog_one";
   244 val hlog_eq_one = thm "hlog_eq_one";
   245 val hlog_inverse = thm "hlog_inverse";
   246 val hlog_divide = thm "hlog_divide";
   247 val hlog_less_cancel_iff = thm "hlog_less_cancel_iff";
   248 val hlog_le_cancel_iff = thm "hlog_le_cancel_iff";
   249 *}
   250 
   251 end