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