converted Hyperreal/Log and Hyperreal/HLog to Isar scripts

--- a/src/HOL/Hyperreal/HLog.ML	Tue Feb 24 11:15:59 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,262 +0,0 @@
-(*  Title       : HLog.ML
-    Author      : Jacques D. Fleuriot
-    Copyright   : 2000,2001 University of Edinburgh
-    Description : hyperreal base logarithms
-*)
-
-Goalw [powhr_def]
-    "(Abs_hypreal(hyprel `` {X})) powhr (Abs_hypreal(hyprel `` {Y})) = \
-\    Abs_hypreal(hyprel `` {%n.  (X n) powr (Y n)})";
-by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_mult,
-    powr_def]));
-qed "powhr";
-
-Goal "1 powhr a = 1";
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_one_num]));
-qed "powhr_one_eq_one";
-Addsimps [powhr_one_eq_one];
-
-Goal "[| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_zero_num,
-    hypreal_mult,hypreal_less]));
-by (ultra_tac (claset(),simpset() addsimps [powr_mult]) 1);
-qed "powhr_mult";
-
-Goalw [hypreal_zero_def] "0 < x powhr a";
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_less,hypreal_zero_num]));
-qed "powhr_gt_zero";
-Addsimps [powhr_gt_zero];
-
-Goal "x powhr a ~= 0";
-by (rtac ((powhr_gt_zero RS hypreal_not_refl2) RS not_sym) 1);
-qed "powhr_not_zero";
-Addsimps [powhr_not_zero];
-
-Goalw [hypreal_divide_def]
-     "(Abs_hypreal(hyprel `` {X}))/(Abs_hypreal(hyprel `` {Y})) = \
-\     (Abs_hypreal(hyprel `` {%n. (X n)/(Y n)}))";
-by (case_tac "Abs_hypreal (hyprel `` {Y}) = 0" 1);
-by (auto_tac (claset(),
-  simpset() addsimps [hypreal_zero_num,hypreal_inverse,hypreal_mult]));
-by (ALLGOALS(ultra_tac (claset(),simpset() addsimps [real_divide_def])));
-qed "hypreal_divide";
-
-Goal "[| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_divide,
-    hypreal_zero_num,hypreal_less]));
-by (ultra_tac (claset(),simpset() addsimps [powr_divide]) 1);
-qed "powhr_divide";
-
-Goal "x powhr (a + b) = (x powhr a) * (x powhr b)";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","b")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_add,hypreal_mult,
-    powr_add]));
-qed "powhr_add";
-
-Goal "(x powhr a) powhr b = x powhr (a * b)";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","b")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_mult,
-    powr_powr]));
-qed "powhr_powhr";
-
-Goal "(x powhr a) powhr b = (x powhr b) powhr a";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","b")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [powhr,powr_powr_swap]));
-qed "powhr_powhr_swap";
-
-Goal "x powhr (-a) = inverse (x powhr a)";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_minus,
-    hypreal_inverse,hypreal_less,powr_minus]));
-qed "powhr_minus";
-
-Goalw [hypreal_divide_def] "x powhr (-a) = 1/(x powhr a)";
-by (simp_tac (simpset() addsimps [powhr_minus]) 1);
-qed "powhr_minus_divide";
-
-Goal "[| a < b; 1 < x |] ==> x powhr a < x powhr b";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","b")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_one_num,
-    hypreal_less]));
-by (ultra_tac (claset(),simpset() addsimps [powr_less_mono]) 1);
-qed "powhr_less_mono";
-
-Goal "[| x powhr a < x powhr b; 1 < x |] ==> a < b";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","b")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_one_num,
-    hypreal_less]));
-by (ultra_tac (claset() addDs [powr_less_cancel],simpset()) 1);
-qed "powhr_less_cancel";
-
-Goal "1 < x ==> (x powhr a < x powhr b) = (a < b)";
-by (blast_tac (claset() addIs [powhr_less_cancel,powhr_less_mono]) 1);
-qed "powhr_less_cancel_iff";
-Addsimps [powhr_less_cancel_iff];
-
-Goal "1 < x ==> (x powhr a <= x powhr b) = (a <= b)";
-by (auto_tac (claset(),simpset() addsimps [linorder_not_less RS sym]));
-qed "powhr_le_cancel_iff";
-Addsimps [powhr_le_cancel_iff];
-
-Goalw [hlog_def]
-     "hlog (Abs_hypreal(hyprel `` {X})) (Abs_hypreal(hyprel `` {Y})) = \
-\     Abs_hypreal(hyprel `` {%n. log (X n) (Y n)})";
-by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
-by Auto_tac;
-by (Ultra_tac 1);
-qed "hlog";
-
-Goal "( *f* ln) x = hlog (( *f* exp) 1) x";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [starfun,hlog,log_ln,
-    hypreal_one_num]));
-qed "hlog_starfun_ln";
-
-Goal "[| 0 < a; a ~= 1; 0 < x |] ==> a powhr (hlog a x) = x";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hlog,powhr,hypreal_zero_num,
-    hypreal_less,hypreal_one_num]));
-by (Ultra_tac 1);
-qed "powhr_hlog_cancel";
-Addsimps [powhr_hlog_cancel];
-
-Goal "[| 0 < a; a ~= 1 |] ==> hlog a (a powhr y) = y";
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hlog,powhr,hypreal_zero_num,
-    hypreal_less,hypreal_one_num]));
-by (ultra_tac (claset() addIs [log_powr_cancel],simpset()) 1);
-qed "hlog_powhr_cancel";
-Addsimps [hlog_powhr_cancel];
-
-Goal "[| 0 < a; a ~= 1; 0 < x; 0 < y  |] \
-\     ==> hlog a (x * y) = hlog a x + hlog a y";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hlog,powhr,hypreal_zero_num,
-    hypreal_one_num,hypreal_less,hypreal_add,hypreal_mult]));
-by (ultra_tac (claset(),simpset() addsimps [log_mult]) 1);
-qed "hlog_mult";
-
-Goal "[| 0 < a; a ~= 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hlog,starfun,
-    hypreal_zero_num,hypreal_one_num,hypreal_divide,log_def]));
-qed "hlog_as_starfun";
-
-Goal "[| 0 < a; a ~= 1; 0 < b; b ~= 1; 0 < x |] \
-\     ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","b")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hlog,starfun,
-    hypreal_zero_num,hypreal_one_num,hypreal_less,
-    hypreal_divide,hypreal_mult]));
-by (ultra_tac (claset() addDs [log_eq_div_ln_mult_log],simpset()) 1);
-qed "hlog_eq_div_starfun_ln_mult_hlog";
-
-Goal "x powhr a = ( *f* exp) (a * ( *f* ln) x)";
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [powhr,starfun,
-    hypreal_mult,powr_def]));
-qed "powhr_as_starfun";
-
-Goal "[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal; \
-\        0 < a |] ==> x powhr a : HInfinite";
-by (auto_tac (claset() addSIs [starfun_ln_ge_zero,
-    starfun_ln_HInfinite,HInfinite_HFinite_not_Infinitesimal_mult2,
-    starfun_exp_HInfinite],simpset() addsimps [order_less_imp_le,
-    HInfinite_gt_zero_gt_one,powhr_as_starfun,
-    zero_le_mult_iff]));
-qed "HInfinite_powhr";
-
-Goal "[| x : HFinite - Infinitesimal; a : HInfinite; 0 < a |] \
-\     ==> hlog a (abs x) : Infinitesimal";
-by (ftac HInfinite_gt_zero_gt_one 1);
-by (auto_tac (claset() addSIs [starfun_ln_HFinite_not_Infinitesimal,
-    HInfinite_inverse_Infinitesimal,Infinitesimal_HFinite_mult2],
-    simpset() addsimps [starfun_ln_HInfinite,not_Infinitesimal_not_zero,
-    hlog_as_starfun,hypreal_not_refl2 RS not_sym,hypreal_divide_def]));
-qed "hlog_hrabs_HInfinite_Infinitesimal";
-
-Goal "[| a : HInfinite; 0 < a |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a";
-by (rtac hlog_as_starfun 1);
-by Auto_tac;
-qed "hlog_HInfinite_as_starfun";
-
-Goal "hlog a 1 = 0";
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_one_num,
-    hypreal_zero_num,hlog]));
-qed "hlog_one";
-Addsimps [hlog_one];
-
-Goal "[| 0 < a; a ~= 1 |] ==> hlog a a = 1";
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_one_num,
-    hypreal_zero_num,hlog,hypreal_less]));
-by (ultra_tac (claset() addIs [log_eq_one],simpset()) 1);
-qed "hlog_eq_one";
-Addsimps [hlog_eq_one];
-
-Goal "[| 0 < a; a ~= 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x";
-by (res_inst_tac [("a1","hlog a x")] (add_left_cancel RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_not_refl2 RS not_sym,
-    hlog_mult RS sym,positive_imp_inverse_positive]));
-qed "hlog_inverse";
-
-Goal "[| 0 < a; a ~= 1; 0 < x; 0 < y|] \
-\     ==> hlog a (x/y) = hlog a x - hlog a y";
-by (auto_tac (claset(),
-    simpset() addsimps [positive_imp_inverse_positive,hlog_mult, hlog_inverse,hypreal_diff_def,hypreal_divide_def]));
-qed "hlog_divide";
-
-Goal "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)";
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hlog,hypreal_less,
-    hypreal_zero_num,hypreal_one_num]));
-by (ALLGOALS(Ultra_tac));
-qed "hlog_less_cancel_iff";
-Addsimps [hlog_less_cancel_iff];
-
-Goal "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x <= hlog a y) = (x <= y)";
-by (auto_tac (claset(),simpset() addsimps [linorder_not_less RS sym]));
-qed "hlog_le_cancel_iff";
-Addsimps [hlog_le_cancel_iff];
-
-(* should be in NSA.ML *)
-goalw HLog.thy [epsilon_def] "0 <= epsilon";
-by (auto_tac (claset(),simpset() addsimps [hypreal_zero_num,hypreal_le]));
-qed "epsilon_ge_zero";
-Addsimps [epsilon_ge_zero];
-
-goal HLog.thy "epsilon : {x. 0 <= x & x : HFinite}";
-by Auto_tac;
-qed "hpfinite_witness";
-

--- a/src/HOL/Hyperreal/HLog.thy	Tue Feb 24 11:15:59 2004 +0100
+++ b/src/HOL/Hyperreal/HLog.thy	Tue Feb 24 16:38:51 2004 +0100
@@ -1,19 +1,275 @@
 (*  Title       : HLog.thy
     Author      : Jacques D. Fleuriot
     Copyright   : 2000,2001 University of Edinburgh
-    Description : hyperreal base logarithms
 *)
 
-HLog = Log + HTranscendental + 
+header{*Logarithms: Non-Standard Version*}
+
+theory HLog = Log + HTranscendental: 
+
+
+(* should be in NSA.ML *)
+lemma epsilon_ge_zero [simp]: "0 \<le> epsilon"
+by (simp add: epsilon_def hypreal_zero_num hypreal_le)
+
+lemma hpfinite_witness: "epsilon : {x. 0 \<le> x & x : HFinite}"
+by auto
 
 
 constdefs
 
-    powhr  :: [hypreal,hypreal] => hypreal     (infixr 80)
+    powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80)
     "x powhr a == ( *f* exp) (a * ( *f* ln) x)"
   
-    hlog :: [hypreal,hypreal] => hypreal
-    "hlog a x == Abs_hypreal(UN A: Rep_hypreal(a).UN X: Rep_hypreal(x).
+    hlog :: "[hypreal,hypreal] => hypreal"
+    "hlog a x == Abs_hypreal(\<Union>A \<in> Rep_hypreal(a).\<Union>X \<in> Rep_hypreal(x).
 			     hyprel `` {%n. log (A n) (X n)})"
 
-end
\ No newline at end of file
+
+lemma powhr: 
+    "(Abs_hypreal(hyprel `` {X})) powhr (Abs_hypreal(hyprel `` {Y})) =  
+     Abs_hypreal(hyprel `` {%n.  (X n) powr (Y n)})"
+by (simp add: powhr_def starfun hypreal_mult powr_def)
+
+lemma powhr_one_eq_one [simp]: "1 powhr a = 1"
+apply (rule eq_Abs_hypreal [of a])
+apply (simp add: powhr hypreal_one_num)
+done
+
+lemma powhr_mult:
+     "[| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of y])
+apply (rule eq_Abs_hypreal [of a])
+apply (simp add: powhr hypreal_zero_num hypreal_mult hypreal_less, ultra)
+apply (simp add: powr_mult) 
+done
+
+lemma powhr_gt_zero [simp]: "0 < x powhr a"
+apply (rule eq_Abs_hypreal [of a])
+apply (rule eq_Abs_hypreal [of x])
+apply (simp add: hypreal_zero_def powhr hypreal_less hypreal_zero_num)
+done
+
+lemma powhr_not_zero [simp]: "x powhr a \<noteq> 0"
+by (rule powhr_gt_zero [THEN hypreal_not_refl2, THEN not_sym])
+
+lemma hypreal_divide: 
+     "(Abs_hypreal(hyprel `` {X}))/(Abs_hypreal(hyprel `` {Y})) =  
+      (Abs_hypreal(hyprel `` {%n. (X n)/(Y n)}))"
+by (simp add: divide_inverse_zero hypreal_zero_num hypreal_inverse hypreal_mult) 
+
+lemma powhr_divide:
+     "[| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of y])
+apply (rule eq_Abs_hypreal [of a])
+apply (simp add: powhr hypreal_divide hypreal_zero_num hypreal_less, ultra)
+apply (simp add: powr_divide)
+done
+
+lemma powhr_add: "x powhr (a + b) = (x powhr a) * (x powhr b)"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of b])
+apply (rule eq_Abs_hypreal [of a])
+apply (simp add: powhr hypreal_add hypreal_mult powr_add)
+done
+
+lemma powhr_powhr: "(x powhr a) powhr b = x powhr (a * b)"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of b])
+apply (rule eq_Abs_hypreal [of a])
+apply (simp add: powhr hypreal_mult powr_powr)
+done
+
+lemma powhr_powhr_swap: "(x powhr a) powhr b = (x powhr b) powhr a"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of b])
+apply (rule eq_Abs_hypreal [of a])
+apply (simp add: powhr powr_powr_swap)
+done
+
+lemma powhr_minus: "x powhr (-a) = inverse (x powhr a)"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of a])
+apply (simp add: powhr hypreal_minus hypreal_inverse hypreal_less powr_minus)
+done
+
+lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)"
+by (simp add: divide_inverse_zero powhr_minus)
+
+lemma powhr_less_mono: "[| a < b; 1 < x |] ==> x powhr a < x powhr b"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of a])
+apply (rule eq_Abs_hypreal [of b])
+apply (simp add: powhr hypreal_one_num hypreal_less, ultra)
+done
+
+lemma powhr_less_cancel: "[| x powhr a < x powhr b; 1 < x |] ==> a < b"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of a])
+apply (rule eq_Abs_hypreal [of b])
+apply (simp add: powhr hypreal_one_num hypreal_less, ultra)
+done
+
+lemma powhr_less_cancel_iff [simp]:
+     "1 < x ==> (x powhr a < x powhr b) = (a < b)"
+by (blast intro: powhr_less_cancel powhr_less_mono)
+
+lemma powhr_le_cancel_iff [simp]:
+     "1 < x ==> (x powhr a \<le> x powhr b) = (a \<le> b)"
+by (simp add: linorder_not_less [symmetric])
+
+lemma hlog: 
+     "hlog (Abs_hypreal(hyprel `` {X})) (Abs_hypreal(hyprel `` {Y})) =  
+      Abs_hypreal(hyprel `` {%n. log (X n) (Y n)})"
+apply (simp add: hlog_def)
+apply (rule arg_cong [where f=Abs_hypreal], auto, ultra)
+done
+
+lemma hlog_starfun_ln: "( *f* ln) x = hlog (( *f* exp) 1) x"
+apply (rule eq_Abs_hypreal [of x])
+apply (simp add: starfun hlog log_ln hypreal_one_num)
+done
+
+lemma powhr_hlog_cancel [simp]:
+     "[| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of a])
+apply (simp add: hlog powhr hypreal_zero_num hypreal_less hypreal_one_num, ultra)
+done
+
+lemma hlog_powhr_cancel [simp]:
+     "[| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y"
+apply (rule eq_Abs_hypreal [of y])
+apply (rule eq_Abs_hypreal [of a])
+apply (simp add: hlog powhr hypreal_zero_num hypreal_less hypreal_one_num, ultra)
+apply (auto intro: log_powr_cancel) 
+done
+
+lemma hlog_mult:
+     "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y  |]  
+      ==> hlog a (x * y) = hlog a x + hlog a y"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of y])
+apply (rule eq_Abs_hypreal [of a])
+apply (simp add: hlog powhr hypreal_zero_num hypreal_one_num hypreal_less hypreal_add hypreal_mult, ultra)
+apply (simp add: log_mult)
+done
+
+lemma hlog_as_starfun:
+     "[| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of a])
+apply (simp add: hlog starfun hypreal_zero_num hypreal_one_num hypreal_divide log_def)
+done
+
+lemma hlog_eq_div_starfun_ln_mult_hlog:
+     "[| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]  
+      ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of a])
+apply (rule eq_Abs_hypreal [of b])
+apply (simp add: hlog starfun hypreal_zero_num hypreal_one_num hypreal_less hypreal_divide hypreal_mult, ultra)
+apply (auto dest: log_eq_div_ln_mult_log) 
+done
+
+lemma powhr_as_starfun: "x powhr a = ( *f* exp) (a * ( *f* ln) x)"
+apply (rule eq_Abs_hypreal [of a])
+apply (rule eq_Abs_hypreal [of x])
+apply (simp add: powhr starfun hypreal_mult powr_def)
+done
+
+lemma HInfinite_powhr:
+     "[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal;  
+         0 < a |] ==> x powhr a : HInfinite"
+apply (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite 
+       simp add: order_less_imp_le HInfinite_gt_zero_gt_one powhr_as_starfun zero_le_mult_iff)
+done
+
+lemma hlog_hrabs_HInfinite_Infinitesimal:
+     "[| x : HFinite - Infinitesimal; a : HInfinite; 0 < a |]  
+      ==> hlog a (abs x) : Infinitesimal"
+apply (frule HInfinite_gt_zero_gt_one)
+apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
+            HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2 
+        simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero 
+          hlog_as_starfun hypreal_not_refl2 [THEN not_sym] divide_inverse_zero)
+done
+
+lemma hlog_HInfinite_as_starfun:
+     "[| a : HInfinite; 0 < a |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
+by (rule hlog_as_starfun, auto)
+
+lemma hlog_one [simp]: "hlog a 1 = 0"
+apply (rule eq_Abs_hypreal [of a])
+apply (simp add: hypreal_one_num hypreal_zero_num hlog)
+done
+
+lemma hlog_eq_one [simp]: "[| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1"
+apply (rule eq_Abs_hypreal [of a])
+apply (simp add: hypreal_one_num hypreal_zero_num hlog hypreal_less, ultra)
+apply (auto intro: log_eq_one) 
+done
+
+lemma hlog_inverse:
+     "[| 0 < a; a \<noteq> 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x"
+apply (rule add_left_cancel [of "hlog a x", THEN iffD1])
+apply (simp add: hlog_mult [symmetric])
+done
+
+lemma hlog_divide:
+     "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> hlog a (x/y) = hlog a x - hlog a y"
+by (simp add: hlog_mult hlog_inverse divide_inverse_zero)
+
+lemma hlog_less_cancel_iff [simp]:
+     "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
+apply (rule eq_Abs_hypreal [of a])
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of y])
+apply (auto simp add: hlog hypreal_less hypreal_zero_num hypreal_one_num, ultra+)
+done
+
+lemma hlog_le_cancel_iff [simp]:
+     "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x \<le> hlog a y) = (x \<le> y)"
+by (simp add: linorder_not_less [symmetric])
+
+
+ML
+{*
+val powhr = thm "powhr";
+val powhr_one_eq_one = thm "powhr_one_eq_one";
+val powhr_mult = thm "powhr_mult";
+val powhr_gt_zero = thm "powhr_gt_zero";
+val powhr_not_zero = thm "powhr_not_zero";
+val hypreal_divide = thm "hypreal_divide";
+val powhr_divide = thm "powhr_divide";
+val powhr_add = thm "powhr_add";
+val powhr_powhr = thm "powhr_powhr";
+val powhr_powhr_swap = thm "powhr_powhr_swap";
+val powhr_minus = thm "powhr_minus";
+val powhr_minus_divide = thm "powhr_minus_divide";
+val powhr_less_mono = thm "powhr_less_mono";
+val powhr_less_cancel = thm "powhr_less_cancel";
+val powhr_less_cancel_iff = thm "powhr_less_cancel_iff";
+val powhr_le_cancel_iff = thm "powhr_le_cancel_iff";
+val hlog = thm "hlog";
+val hlog_starfun_ln = thm "hlog_starfun_ln";
+val powhr_hlog_cancel = thm "powhr_hlog_cancel";
+val hlog_powhr_cancel = thm "hlog_powhr_cancel";
+val hlog_mult = thm "hlog_mult";
+val hlog_as_starfun = thm "hlog_as_starfun";
+val hlog_eq_div_starfun_ln_mult_hlog = thm "hlog_eq_div_starfun_ln_mult_hlog";
+val powhr_as_starfun = thm "powhr_as_starfun";
+val HInfinite_powhr = thm "HInfinite_powhr";
+val hlog_hrabs_HInfinite_Infinitesimal = thm "hlog_hrabs_HInfinite_Infinitesimal";
+val hlog_HInfinite_as_starfun = thm "hlog_HInfinite_as_starfun";
+val hlog_one = thm "hlog_one";
+val hlog_eq_one = thm "hlog_eq_one";
+val hlog_inverse = thm "hlog_inverse";
+val hlog_divide = thm "hlog_divide";
+val hlog_less_cancel_iff = thm "hlog_less_cancel_iff";
+val hlog_le_cancel_iff = thm "hlog_le_cancel_iff";
+*}
+
+end

--- a/src/HOL/Hyperreal/Log.ML	Tue Feb 24 11:15:59 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,162 +0,0 @@
-(*  Title       : Log.ML
-    Author      : Jacques D. Fleuriot
-    Copyright   : 2000,2001 University of Edinburgh
-    Description : standard logarithms only 
-*)
-
-
-Goalw [powr_def] "1 powr a = 1";
-by (Simp_tac 1);
-qed "powr_one_eq_one";
-Addsimps [powr_one_eq_one];
-
-Goalw [powr_def] "x powr 0 = 1";
-by (Simp_tac 1);
-qed "powr_zero_eq_one";
-Addsimps [powr_zero_eq_one];
-
-Goalw [powr_def] 
-      "(x powr 1 = x) = (0 < x)";
-by (Simp_tac 1);
-qed "powr_one_gt_zero_iff";
-Addsimps [powr_one_gt_zero_iff];
-Addsimps [powr_one_gt_zero_iff RS iffD2];
-
-Goalw [powr_def] 
-      "[| 0 < x; 0 < y |] ==> (x * y) powr a = (x powr a) * (y powr a)";
-by (asm_simp_tac (simpset() addsimps [exp_add RS sym,ln_mult,
-    right_distrib]) 1);
-qed "powr_mult";
-
-Goalw [powr_def] "0 < x powr a";
-by (Simp_tac 1);
-qed "powr_gt_zero";
-Addsimps [powr_gt_zero];
-
-Goalw [powr_def] "x powr a ~= 0";
-by (Simp_tac 1);
-qed "powr_not_zero";
-Addsimps [powr_not_zero];
-
-Goal "[| 0 < x; 0 < y |] ==> (x / y) powr a = (x powr a)/(y powr a)";
-by (asm_simp_tac (simpset() addsimps [real_divide_def,positive_imp_inverse_positive, powr_mult]) 1);
-by (asm_simp_tac (simpset() addsimps [powr_def,exp_minus RS sym,
-    exp_add RS sym,ln_inverse]) 1);
-qed "powr_divide";
-
-Goalw [powr_def] "x powr (a + b) = (x powr a) * (x powr b)";
-by (asm_simp_tac (simpset() addsimps [exp_add RS sym,
-    left_distrib]) 1);
-qed "powr_add";
-
-Goalw [powr_def] "(x powr a) powr b = x powr (a * b)";
-by (simp_tac (simpset() addsimps mult_ac) 1);
-qed "powr_powr";
-
-Goal "(x powr a) powr b = (x powr b) powr a";
-by (simp_tac (simpset() addsimps [powr_powr,real_mult_commute]) 1);
-qed "powr_powr_swap";
-
-Goalw [powr_def] "x powr (-a) = inverse (x powr a)";
-by (simp_tac (simpset() addsimps [exp_minus RS sym]) 1);
-qed "powr_minus";
-
-Goalw [real_divide_def] "x powr (-a) = 1/(x powr a)";
-by (simp_tac (simpset() addsimps [powr_minus]) 1);
-qed "powr_minus_divide";
-
-Goalw [powr_def] 
-   "[| a < b; 1 < x |] ==> x powr a < x powr b";
-by Auto_tac;
-qed "powr_less_mono";
-
-Goalw [powr_def] 
-   "[| x powr a < x powr b; 1 < x |] ==> a < b";
-by (auto_tac (claset() addDs [ln_gt_zero],
-              simpset() addsimps [mult_less_cancel_right]));
-qed "powr_less_cancel";
-
-Goal "1 < x ==> (x powr a < x powr b) = (a < b)";
-by (blast_tac (claset() addIs [powr_less_cancel,powr_less_mono]) 1);
-qed "powr_less_cancel_iff";
-Addsimps [powr_less_cancel_iff];
-
-Goal "1 < x ==> (x powr a <= x powr b) = (a <= b)";
-by (auto_tac (claset(), simpset() addsimps [linorder_not_less RS sym]));
-qed "powr_le_cancel_iff";
-Addsimps [powr_le_cancel_iff];
-
-Goalw [log_def] "ln x = log (exp(1)) x";
-by (Simp_tac 1);
-qed "log_ln";
-
-Goalw [powr_def,log_def] 
-    "[| 0 < a; a ~= 1; 0 < x |] ==> a powr (log a x) = x";
-by Auto_tac;
-qed "powr_log_cancel";
-Addsimps [powr_log_cancel];
-
-Goalw [log_def,powr_def] 
-    "[| 0 < a; a ~= 1 |] ==> log a (a powr y) = y";
-by (auto_tac (claset(),simpset() addsimps [real_divide_def,
-    real_mult_assoc]));
-qed "log_powr_cancel";
-Addsimps [log_powr_cancel];
-
-Goalw [log_def] 
-     "[| 0 < a; a ~= 1; 0 < x; 0 < y  |] \
-\     ==> log a (x * y) = log a x + log a y";
-by (auto_tac (claset(),simpset() addsimps [ln_mult,real_divide_def,
-    left_distrib]));
-qed "log_mult";
-
-Goalw [log_def,real_divide_def]
-     "[| 0 < a; a ~= 1; 0 < b; b ~= 1; 0 < x |] \
-\     ==> log a x = (ln b/ln a) * log b x";
-by Auto_tac;
-qed "log_eq_div_ln_mult_log";
-
-(* specific case *)
-Goal "0 < x ==> log 10 x = (ln (exp 1) / ln 10) * ln x";
-by (auto_tac (claset(),simpset() addsimps [log_def]));
-qed "log_base_10_eq1";
-
-Goal "0 < x ==> log 10 x = (log 10 (exp 1)) * ln x";
-by (auto_tac (claset(),simpset() addsimps [log_def]));
-qed "log_base_10_eq2";
-
-Goalw [log_def] "log a 1 = 0";
-by Auto_tac;
-qed "log_one";
-Addsimps [log_one];
-
-Goalw [log_def] 
-    "[| 0 < a; a ~= 1 |] ==> log a a = 1";
-by Auto_tac;
-qed "log_eq_one";
-Addsimps [log_eq_one];
-
-Goal "[| 0 < a; a ~= 1; 0 < x |] ==> log a (inverse x) = - log a x";
-by (res_inst_tac [("a1","log a x")] (add_left_cancel RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [log_mult RS sym]));
-qed "log_inverse";
-
-Goal "[|0 < a; a ~= 1; 0 < x; 0 < y|] \
-\     ==> log a (x/y) = log a x - log a y";
-by (auto_tac (claset(),simpset() addsimps [log_mult,real_divide_def,
-    log_inverse]));
-qed "log_divide";
-
-Goal "[| 1 < a; 0 < x; 0 < y |] ==> (log a x < log a y) = (x < y)";
-by (Step_tac 1);
-by (rtac powr_less_cancel 2);
-by (dres_inst_tac [("a","log a x")] powr_less_mono 1);
-by Auto_tac;
-qed "log_less_cancel_iff";
-Addsimps [log_less_cancel_iff];
-
-Goal "[| 1 < a; 0 < x; 0 < y |] ==> (log a x <= log a y) = (x <= y)";
-by (auto_tac (claset(),simpset() addsimps [linorder_not_less RS sym]));
-qed "log_le_cancel_iff";
-Addsimps [log_le_cancel_iff];
-

--- a/src/HOL/Hyperreal/Log.thy	Tue Feb 24 11:15:59 2004 +0100
+++ b/src/HOL/Hyperreal/Log.thy	Tue Feb 24 16:38:51 2004 +0100
@@ -1,19 +1,164 @@
 (*  Title       : Log.thy
     Author      : Jacques D. Fleuriot
     Copyright   : 2000,2001 University of Edinburgh
-    Description : standard logarithms only 
 *)
 
-Log = Transcendental +
+header{*Logarithms: Standard Version*}
+
+theory Log = Transcendental:
 
 constdefs
 
-    (* power function with exponent a *)
-    powr  :: [real,real] => real     (infixr 80)
+  powr  :: "[real,real] => real"     (infixr "powr" 80)
+    --{*exponentation with real exponent*}
     "x powr a == exp(a * ln x)"
 
-    (* logarithm of x to base a *)
-    log :: [real,real] => real
+  log :: "[real,real] => real"
+    --{*logarithm of @[term x} to base @[term a}*}
     "log a x == ln x / ln a"
 
+
+
+lemma powr_one_eq_one [simp]: "1 powr a = 1"
+by (simp add: powr_def)
+
+lemma powr_zero_eq_one [simp]: "x powr 0 = 1"
+by (simp add: powr_def)
+
+lemma powr_one_gt_zero_iff [simp]: "(x powr 1 = x) = (0 < x)"
+by (simp add: powr_def)
+declare powr_one_gt_zero_iff [THEN iffD2, simp]
+
+lemma powr_mult: 
+      "[| 0 < x; 0 < y |] ==> (x * y) powr a = (x powr a) * (y powr a)"
+by (simp add: powr_def exp_add [symmetric] ln_mult right_distrib)
+
+lemma powr_gt_zero [simp]: "0 < x powr a"
+by (simp add: powr_def)
+
+lemma powr_not_zero [simp]: "x powr a \<noteq> 0"
+by (simp add: powr_def)
+
+lemma powr_divide:
+     "[| 0 < x; 0 < y |] ==> (x / y) powr a = (x powr a)/(y powr a)"
+apply (simp add: divide_inverse_zero positive_imp_inverse_positive powr_mult)
+apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
+done
+
+lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
+by (simp add: powr_def exp_add [symmetric] left_distrib)
+
+lemma powr_powr: "(x powr a) powr b = x powr (a * b)"
+by (simp add: powr_def)
+
+lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
+by (simp add: powr_powr real_mult_commute)
+
+lemma powr_minus: "x powr (-a) = inverse (x powr a)"
+by (simp add: powr_def exp_minus [symmetric])
+
+lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)"
+by (simp add: divide_inverse_zero powr_minus)
+
+lemma powr_less_mono: "[| a < b; 1 < x |] ==> x powr a < x powr b"
+by (simp add: powr_def)
+
+lemma powr_less_cancel: "[| x powr a < x powr b; 1 < x |] ==> a < b"
+by (simp add: powr_def)
+
+lemma powr_less_cancel_iff [simp]: "1 < x ==> (x powr a < x powr b) = (a < b)"
+by (blast intro: powr_less_cancel powr_less_mono)
+
+lemma powr_le_cancel_iff [simp]: "1 < x ==> (x powr a \<le> x powr b) = (a \<le> b)"
+by (simp add: linorder_not_less [symmetric])
+
+lemma log_ln: "ln x = log (exp(1)) x"
+by (simp add: log_def)
+
+lemma powr_log_cancel [simp]:
+     "[| 0 < a; a \<noteq> 1; 0 < x |] ==> a powr (log a x) = x"
+by (simp add: powr_def log_def)
+
+lemma log_powr_cancel [simp]: "[| 0 < a; a \<noteq> 1 |] ==> log a (a powr y) = y"
+by (simp add: log_def powr_def)
+
+lemma log_mult: 
+     "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y |]  
+      ==> log a (x * y) = log a x + log a y"
+by (simp add: log_def ln_mult divide_inverse_zero left_distrib)
+
+lemma log_eq_div_ln_mult_log: 
+     "[| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]  
+      ==> log a x = (ln b/ln a) * log b x"
+by (simp add: log_def divide_inverse_zero)
+
+text{*Base 10 logarithms*}
+lemma log_base_10_eq1: "0 < x ==> log 10 x = (ln (exp 1) / ln 10) * ln x"
+by (simp add: log_def)
+
+lemma log_base_10_eq2: "0 < x ==> log 10 x = (log 10 (exp 1)) * ln x"
+by (simp add: log_def)
+
+lemma log_one [simp]: "log a 1 = 0"
+by (simp add: log_def)
+
+lemma log_eq_one [simp]: "[| 0 < a; a \<noteq> 1 |] ==> log a a = 1"
+by (simp add: log_def)
+
+lemma log_inverse:
+     "[| 0 < a; a \<noteq> 1; 0 < x |] ==> log a (inverse x) = - log a x"
+apply (rule_tac a1 = "log a x" in add_left_cancel [THEN iffD1])
+apply (simp add: log_mult [symmetric])
+done
+
+lemma log_divide:
+     "[|0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> log a (x/y) = log a x - log a y"
+by (simp add: log_mult divide_inverse_zero log_inverse)
+
+lemma log_less_cancel_iff [simp]:
+     "[| 1 < a; 0 < x; 0 < y |] ==> (log a x < log a y) = (x < y)"
+apply safe
+apply (rule_tac [2] powr_less_cancel)
+apply (drule_tac a = "log a x" in powr_less_mono, auto)
+done
+
+lemma log_le_cancel_iff [simp]:
+     "[| 1 < a; 0 < x; 0 < y |] ==> (log a x \<le> log a y) = (x \<le> y)"
+by (simp add: linorder_not_less [symmetric])
+
+
+
+ML
+{*
+val powr_one_eq_one = thm "powr_one_eq_one";
+val powr_zero_eq_one = thm "powr_zero_eq_one";
+val powr_one_gt_zero_iff = thm "powr_one_gt_zero_iff";
+val powr_mult = thm "powr_mult";
+val powr_gt_zero = thm "powr_gt_zero";
+val powr_not_zero = thm "powr_not_zero";
+val powr_divide = thm "powr_divide";
+val powr_add = thm "powr_add";
+val powr_powr = thm "powr_powr";
+val powr_powr_swap = thm "powr_powr_swap";
+val powr_minus = thm "powr_minus";
+val powr_minus_divide = thm "powr_minus_divide";
+val powr_less_mono = thm "powr_less_mono";
+val powr_less_cancel = thm "powr_less_cancel";
+val powr_less_cancel_iff = thm "powr_less_cancel_iff";
+val powr_le_cancel_iff = thm "powr_le_cancel_iff";
+val log_ln = thm "log_ln";
+val powr_log_cancel = thm "powr_log_cancel";
+val log_powr_cancel = thm "log_powr_cancel";
+val log_mult = thm "log_mult";
+val log_eq_div_ln_mult_log = thm "log_eq_div_ln_mult_log";
+val log_base_10_eq1 = thm "log_base_10_eq1";
+val log_base_10_eq2 = thm "log_base_10_eq2";
+val log_one = thm "log_one";
+val log_eq_one = thm "log_eq_one";
+val log_inverse = thm "log_inverse";
+val log_divide = thm "log_divide";
+val log_less_cancel_iff = thm "log_less_cancel_iff";
+val log_le_cancel_iff = thm "log_le_cancel_iff";
+*}
+
 end

--- a/src/HOL/IsaMakefile	Tue Feb 24 11:15:59 2004 +0100
+++ b/src/HOL/IsaMakefile	Tue Feb 24 16:38:51 2004 +0100
@@ -144,13 +144,13 @@
   Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy \
   Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
   Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \
-  Hyperreal/Fact.ML Hyperreal/Fact.thy\
+  Hyperreal/Fact.ML Hyperreal/Fact.thy Hyperreal/HLog.thy\
   Hyperreal/Filter.ML Hyperreal/Filter.thy\
   Hyperreal/HSeries.ML Hyperreal/HSeries.thy\
   Hyperreal/HyperArith.thy Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\
   Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
   Hyperreal/IntFloor.thy Hyperreal/IntFloor.ML\
-  Hyperreal/Lim.ML Hyperreal/Lim.thy  Hyperreal/Log.ML Hyperreal/Log.thy\
+  Hyperreal/Lim.ML Hyperreal/Lim.thy Hyperreal/Log.thy\
   Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy\
   Hyperreal/NatStar.ML Hyperreal/NatStar.thy\
   Hyperreal/NSA.thy Hyperreal/NthRoot.thy\