--- a/src/HOL/Real/Hyperreal/HRealAbs.ML Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HRealAbs.ML Thu Dec 21 10:16:33 2000 +0100
@@ -5,17 +5,16 @@
Similar to RealAbs.thy
*)
-
(*------------------------------------------------------------
absolute value on hyperreals as pointwise operation on
equivalence class representative
------------------------------------------------------------*)
Goalw [hrabs_def]
-"abs (Abs_hypreal (hyprel ^^ {X})) = \
-\ Abs_hypreal(hyprel ^^ {%n. abs (X n)})";
-by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def,
- hypreal_le,hypreal_minus]));
+ "abs (Abs_hypreal (hyprel ^^ {X})) = \
+\ Abs_hypreal(hyprel ^^ {%n. abs (X n)})";
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_zero_def, hypreal_le,hypreal_minus]));
by (ALLGOALS(Ultra_tac THEN' arith_tac ));
qed "hypreal_hrabs";
@@ -23,49 +22,38 @@
Properties of the absolute value function over the reals
(adapted version of previously proved theorems about abs)
------------------------------------------------------------*)
-Goalw [hrabs_def] "abs r = (if (0::hypreal)<=r then r else -r)";
-by (Step_tac 1);
-qed "hrabs_iff";
-Goalw [hrabs_def] "abs (0::hypreal) = (0::hypreal)";
-by (rtac (hypreal_le_refl RS if_P) 1);
+Goal "abs (0::hypreal) = 0";
+by (simp_tac (simpset() addsimps [hrabs_def]) 1);
qed "hrabs_zero";
-
Addsimps [hrabs_zero];
-Goalw [hrabs_def] "abs (0::hypreal) = -(0::hypreal)";
-by (rtac (hypreal_minus_zero RS ssubst) 1);
-by (rtac if_cancel 1);
-qed "hrabs_minus_zero";
-
-val [prem] = goalw thy [hrabs_def] "(0::hypreal)<=x ==> abs x = x";
-by (rtac (prem RS if_P) 1);
+Goal "(0::hypreal)<=x ==> abs x = x";
+by (asm_simp_tac (simpset() addsimps [hrabs_def]) 1);
qed "hrabs_eqI1";
-val [prem] = goalw thy [hrabs_def] "(0::hypreal)<x ==> abs x = x";
-by (simp_tac (simpset() addsimps [(prem
- RS hypreal_less_imp_le),hrabs_eqI1]) 1);
+Goal "(0::hypreal)<x ==> abs x = x";
+by (asm_simp_tac (simpset() addsimps [hypreal_less_imp_le, hrabs_eqI1]) 1);
qed "hrabs_eqI2";
-val [prem] = goalw thy [hrabs_def,hypreal_le_def]
- "x<(0::hypreal) ==> abs x = -x";
-by (simp_tac (simpset() addsimps [prem,if_not_P]) 1);
+Goal "x<(0::hypreal) ==> abs x = -x";
+by (asm_simp_tac (simpset() addsimps [hypreal_le_def, hrabs_def]) 1);
qed "hrabs_minus_eqI2";
-Goal "!!x. x<=(0::hypreal) ==> abs x = -x";
-by (dtac hypreal_le_imp_less_or_eq 1);
-by (fast_tac (HOL_cs addIs [hrabs_minus_zero,
- hrabs_minus_eqI2]) 1);
+Goal "x<=(0::hypreal) ==> abs x = -x";
+by (auto_tac (claset() addDs [order_antisym], simpset() addsimps [hrabs_def]));
qed "hrabs_minus_eqI1";
-Goalw [hrabs_def,hypreal_le_def] "(0::hypreal)<= abs x";
-by (auto_tac (claset() addDs [hypreal_minus_zero_less_iff RS iffD2,
- hypreal_less_asym],simpset()));
+Goal "(0::hypreal)<= abs x";
+by (auto_tac (claset() addDs [hypreal_minus_zero_less_iff RS iffD2,
+ hypreal_less_asym],
+ simpset() addsimps [hypreal_le_def, hrabs_def]));
qed "hrabs_ge_zero";
Goal "abs(abs x) = abs (x::hypreal)";
-by (res_inst_tac [("r1","abs x")] (hrabs_iff RS ssubst) 1);
-by (blast_tac (claset() addIs [if_P,hrabs_ge_zero]) 1);
+by (auto_tac (claset() addDs [hypreal_minus_zero_less_iff RS iffD2,
+ hypreal_less_asym],
+ simpset() addsimps [hypreal_le_def, hrabs_def]));
qed "hrabs_idempotent";
Addsimps [hrabs_idempotent];
@@ -87,8 +75,8 @@
Goal "abs(x*(y::hypreal)) = (abs x)*(abs y)";
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 [hypreal_hrabs,
- hypreal_mult,abs_mult]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_hrabs, hypreal_mult,abs_mult]));
qed "hrabs_mult";
Goal "abs(inverse(x)) = inverse(abs(x::hypreal))";
@@ -103,31 +91,23 @@
Goal "abs(x+(y::hypreal)) <= abs x + abs y";
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 [hypreal_hrabs,
- hypreal_add,hypreal_le,abs_triangle_ineq]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_hrabs, hypreal_add,hypreal_le,
+ abs_triangle_ineq]));
qed "hrabs_triangle_ineq";
Goal "abs((w::hypreal) + x + y) <= abs(w) + abs(x) + abs(y)";
-by (auto_tac (claset() addSIs [(hrabs_triangle_ineq
- RS hypreal_le_trans),hypreal_add_left_le_mono1],
+by (auto_tac (claset() addSIs [hrabs_triangle_ineq RS hypreal_le_trans,
+ hypreal_add_left_le_mono1],
simpset() addsimps [hypreal_add_assoc]));
qed "hrabs_triangle_ineq_three";
Goalw [hrabs_def] "abs(-x)=abs((x::hypreal))";
-by (auto_tac (claset() addSDs [not_hypreal_leE,
- hypreal_less_asym] addIs [hypreal_le_anti_sym],
- simpset() addsimps [hypreal_ge_zero_iff]));
+by (auto_tac (claset() addSDs [not_hypreal_leE, hypreal_less_asym]
+ addIs [hypreal_le_anti_sym],
+ simpset() addsimps [hypreal_ge_zero_iff]));
qed "hrabs_minus_cancel";
-
-Goal "abs((x::hypreal) + -y) = abs (y + -x)";
-by (rtac (hrabs_minus_cancel RS subst) 1);
-by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
-qed "hrabs_minus_add_cancel";
-
-Goal "abs((x::hypreal) + -y) <= abs x + abs y";
-by (res_inst_tac [("x1","y")] (hrabs_minus_cancel RS subst) 1);
-by (rtac hrabs_triangle_ineq 1);
-qed "rhabs_triangle_minus_ineq";
+Addsimps [hrabs_minus_cancel];
val prem1::prem2::rest = goal thy
"[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)";
@@ -136,13 +116,6 @@
by (rtac ([prem1,prem2] MRS hypreal_add_less_mono) 1);
qed "hrabs_add_less";
-Goal "[| abs x < r; abs y < s |] \
-\ ==> abs(x+ -y) < r + (s::hypreal)";
-by (rotate_tac 1 1);
-by (dtac (hrabs_minus_cancel RS ssubst) 1);
-by (asm_simp_tac (simpset() addsimps [hrabs_add_less]) 1);
-qed "hrabs_add_minus_less";
-
val prem1::prem2::rest =
goal thy "[| abs x<r; abs y<s |] ==> abs(x*y)<r*(s::hypreal)";
by (simp_tac (simpset() addsimps [hrabs_mult]) 1);
@@ -153,11 +126,11 @@
by (rtac (prem2 RS (hrabs_ge_zero RS hypreal_le_less_trans)) 1);
by (rtac prem1 1);
by (rtac ([prem1 RS (hrabs_ge_zero RS hypreal_le_less_trans),
- prem2 RS (hrabs_ge_zero RS hypreal_le_less_trans)]
- MRS hypreal_mult_order) 1);
+ prem2 RS (hrabs_ge_zero RS hypreal_le_less_trans)]
+ MRS hypreal_mult_order) 1);
qed "hrabs_mult_less";
-Goal "!! x y r. 1hr < abs x ==> abs y <= abs(x*y)";
+Goal "1hr < abs x ==> abs y <= abs(x*y)";
by (cut_inst_tac [("x1","y")] (hrabs_ge_zero RS hypreal_le_imp_less_or_eq) 1);
by (EVERY1[etac disjE,rtac hypreal_less_imp_le]);
by (dres_inst_tac [("x1","1hr")] (hypreal_less_minus_iff RS iffD1) 1);
@@ -170,30 +143,24 @@
by (asm_full_simp_tac (simpset() addsimps [hypreal_le_refl,hrabs_mult]) 1);
qed "hrabs_mult_le";
-Goal "!!x. [| 1hr < abs x; r < abs y|] ==> r < abs(x*y)";
+Goal "[| 1hr < abs x; r < abs y|] ==> r < abs(x*y)";
by (fast_tac (HOL_cs addIs [hrabs_mult_le, hypreal_less_le_trans]) 1);
qed "hrabs_mult_gt";
-Goal "!!r. abs x < r ==> (0::hypreal) < r";
+Goal "abs x < r ==> (0::hypreal) < r";
by (blast_tac (claset() addSIs [hypreal_le_less_trans,
hrabs_ge_zero]) 1);
qed "hrabs_less_gt_zero";
Goalw [hrabs_def] "abs 1hr = 1hr";
-by (auto_tac (claset() addSDs [not_hypreal_leE
- RS hypreal_less_asym],simpset() addsimps
- [hypreal_zero_less_one]));
+by (auto_tac (claset() addSDs [not_hypreal_leE RS hypreal_less_asym],
+ simpset() addsimps [hypreal_zero_less_one]));
qed "hrabs_one";
-val prem1::prem2::rest =
- goal thy "[| (0::hypreal) < x ; x < r |] ==> abs x < r";
-by (simp_tac (simpset() addsimps [(prem1 RS hrabs_eqI2),prem2]) 1);
-qed "hrabs_lessI";
-
Goal "abs x = (x::hypreal) | abs x = -x";
by (cut_inst_tac [("x","0"),("y","x")] hypreal_linear 1);
by (fast_tac (claset() addIs [hrabs_eqI2,hrabs_minus_eqI2,
- hrabs_zero,hrabs_minus_zero]) 1);
+ hrabs_zero]) 1);
qed "hrabs_disj";
Goal "abs x = (y::hypreal) ==> x = y | -x = y";
@@ -217,54 +184,28 @@
qed "hrabs_interval_iff";
Goal "(abs x < (r::hypreal)) = (- x < r & x < r)";
-by (auto_tac (claset(),simpset() addsimps [hrabs_interval_iff]));
+by (auto_tac (claset(), simpset() addsimps [hrabs_interval_iff]));
by (dtac (hypreal_less_swap_iff RS iffD1) 1);
by (dtac (hypreal_less_swap_iff RS iffD1) 2);
by (Auto_tac);
qed "hrabs_interval_iff2";
-Goal
- "(abs (x + -y) < (r::hypreal)) = (y + -r < x & x < y + r)";
-by (auto_tac (claset(),simpset() addsimps
- [hrabs_interval_iff]));
-by (ALLGOALS(dtac (hypreal_less_minus_iff RS iffD1)));
-by (ALLGOALS(dtac (hypreal_less_minus_iff RS iffD1)));
-by (ALLGOALS(rtac (hypreal_less_minus_iff RS iffD2)));
-by (auto_tac (claset(),simpset() addsimps
- [hypreal_minus_add_distrib] addsimps hypreal_add_ac));
-qed "hrabs_add_minus_interval_iff";
-
-Goal "x < (y::hypreal) ==> abs(y + -x) = y + -x";
-by (dtac (hypreal_less_minus_iff RS iffD1) 1);
-by (etac hrabs_eqI2 1);
-qed "hrabs_less_eqI2";
-
-Goal "x < (y::hypreal) ==> abs(x + -y) = y + -x";
-by (auto_tac (claset() addDs [hrabs_less_eqI2],
- simpset() addsimps [hrabs_minus_add_cancel]));
-qed "hrabs_less_eqI2a";
-
-Goal "x <= (y::hypreal) ==> abs(y + -x) = y + -x";
-by (auto_tac (claset() addDs [hypreal_le_imp_less_or_eq,
- hrabs_less_eqI2],simpset()));
-qed "hrabs_le_eqI2";
-
-Goal "x <= (y::hypreal) ==> abs(x + -y) = y + -x";
-by (auto_tac (claset() addDs [hrabs_le_eqI2],
- simpset() addsimps [hrabs_minus_add_cancel]));
-qed "hrabs_le_eqI2a";
-
(* Needed in Geom.ML *)
-Goal "(y::hypreal) + - x + (y + - z) = abs (x + - z) \
-\ ==> y = z | x = y";
+Goal "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = 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","z")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_hrabs,
- hypreal_minus,hypreal_add]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_hrabs, hypreal_minus,hypreal_add]));
by (Ultra_tac 1 THEN arith_tac 1);
qed "hrabs_add_lemma_disj";
+(***SHOULD BE TRIVIAL GIVEN SIMPROCS
+Goal "abs((x::hypreal) + -y) = abs (y + -x)";
+by (rtac (hrabs_minus_cancel RS subst) 1);
+by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
+qed "hrabs_minus_add_cancel";
+
(* Needed in Geom.ML *)
Goal "(x::hypreal) + - y + (z + - y) = abs (x + - z) \
\ ==> y = z | x = y";
@@ -274,11 +215,12 @@
by (asm_full_simp_tac (simpset() addsimps [hrabs_minus_add_cancel]
@ hypreal_add_ac) 1);
qed "hrabs_add_lemma_disj2";
+***)
(*----------------------------------------------------------
Relating hrabs to abs through embedding of IR into IR*
----------------------------------------------------------*)
Goalw [hypreal_of_real_def]
"abs (hypreal_of_real r) = hypreal_of_real (abs r)";
-by (auto_tac (claset(),simpset() addsimps [hypreal_hrabs]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_hrabs]));
qed "hypreal_of_real_hrabs";
--- a/src/HOL/Real/Hyperreal/HyperDef.ML Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML Thu Dec 21 10:16:33 2000 +0100
@@ -707,11 +707,9 @@
simpset()));
qed "hypreal_mult_zero_disj";
-Goal "x ~= 0 ==> x * x ~= (0::hypreal)";
-by (blast_tac (claset() addDs [hypreal_mult_not_0]) 1);
-qed "hypreal_mult_self_not_zero";
-
-Goal "[| x ~= 0; y ~= 0 |] ==> inverse(x*y) = inverse(x)*inverse(y::hypreal)";
+Goal "inverse(x*y) = inverse(x)*inverse(y::hypreal)";
+by (case_tac "x=0 | y=0" 1);
+by (force_tac (claset(), simpset() addsimps [HYPREAL_INVERSE_ZERO]) 1);
by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
by (auto_tac (claset(),
simpset() addsimps [hypreal_mult_assoc RS sym, hypreal_mult_not_0]));
@@ -1109,6 +1107,7 @@
Goalw [hypreal_of_real_def] "hypreal_of_real (-r) = - hypreal_of_real r";
by (auto_tac (claset(),simpset() addsimps [hypreal_minus]));
qed "hypreal_of_real_minus";
+Addsimps [hypreal_of_real_minus];
(*DON'T insert this or the next one as default simprules.
They are used in both orientations and anyway aren't the ones we finally
--- a/src/HOL/Real/Hyperreal/HyperPow.ML Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperPow.ML Thu Dec 21 10:16:33 2000 +0100
@@ -20,18 +20,17 @@
by (induct_tac "n" 1);
by (Auto_tac);
by (forw_inst_tac [("n","n")] hrealpow_not_zero 1);
-by (auto_tac (claset() addDs [inverse_mult_eq],
- simpset()));
+by (auto_tac (claset(), simpset() addsimps [inverse_mult_eq]));
qed_spec_mp "hrealpow_inverse";
Goal "abs (r::hypreal) ^ n = abs (r ^ n)";
by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [hrabs_mult,hrabs_one]));
+by (auto_tac (claset(), simpset() addsimps [hrabs_mult,hrabs_one]));
qed "hrealpow_hrabs";
Goal "(r::hypreal) ^ (n + m) = (r ^ n) * (r ^ m)";
by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps hypreal_mult_ac));
+by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac));
qed "hrealpow_add";
Goal "(r::hypreal) ^ 1 = r";
@@ -46,33 +45,34 @@
Goal "(0::hypreal) < r --> 0 <= r ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addDs [hypreal_less_imp_le]
- addIs [hypreal_le_mult_order],simpset() addsimps
- [hypreal_zero_less_one RS hypreal_less_imp_le]));
+ addIs [hypreal_le_mult_order],
+ simpset() addsimps [hypreal_zero_less_one RS hypreal_less_imp_le]));
qed_spec_mp "hrealpow_ge_zero";
Goal "(0::hypreal) < r --> 0 < r ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addIs [hypreal_mult_order],
- simpset() addsimps [hypreal_zero_less_one]));
+ simpset() addsimps [hypreal_zero_less_one]));
qed_spec_mp "hrealpow_gt_zero";
Goal "(0::hypreal) <= r --> 0 <= r ^ n";
by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [hypreal_le_mult_order],simpset()
- addsimps [hypreal_zero_less_one RS hypreal_less_imp_le]));
+by (auto_tac (claset() addIs [hypreal_le_mult_order],
+ simpset() addsimps [hypreal_zero_less_one RS hypreal_less_imp_le]));
qed_spec_mp "hrealpow_ge_zero2";
Goal "(0::hypreal) < x & x <= y --> x ^ n <= y ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addSIs [hypreal_mult_le_mono],
- simpset() addsimps [hypreal_le_refl]));
+ simpset() addsimps [hypreal_le_refl]));
by (asm_simp_tac (simpset() addsimps [hrealpow_ge_zero]) 1);
qed_spec_mp "hrealpow_le";
Goal "(0::hypreal) < x & x < y & 0 < n --> x ^ n < y ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addIs [hypreal_mult_less_mono,gr0I]
- addDs [hrealpow_gt_zero],simpset()));
+ addDs [hrealpow_gt_zero],
+ simpset()));
qed "hrealpow_less";
Goal "1hr ^ n = 1hr";
@@ -82,21 +82,20 @@
Addsimps [hrealpow_eq_one];
Goal "abs(-(1hr ^ n)) = 1hr";
-by (simp_tac (simpset() addsimps
- [hrabs_minus_cancel,hrabs_one]) 1);
+by (simp_tac (simpset() addsimps [hrabs_one]) 1);
qed "hrabs_minus_hrealpow_one";
Addsimps [hrabs_minus_hrealpow_one];
Goal "abs((-1hr) ^ n) = 1hr";
by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [hrabs_mult,
- hrabs_minus_cancel,hrabs_one]));
+by (auto_tac (claset(),
+ simpset() addsimps [hrabs_mult, hrabs_one]));
qed "hrabs_hrealpow_minus_one";
Addsimps [hrabs_hrealpow_minus_one];
Goal "((r::hypreal) * s) ^ n = (r ^ n) * (s ^ n)";
by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps hypreal_mult_ac));
+by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac));
qed "hrealpow_mult";
Goal "(0::hypreal) <= r ^ 2";
@@ -105,12 +104,12 @@
Addsimps [hrealpow_two_le];
Goal "(0::hypreal) <= u ^ 2 + v ^ 2";
-by (auto_tac (claset() addIs [hypreal_le_add_order],simpset()));
+by (auto_tac (claset() addIs [hypreal_le_add_order], simpset()));
qed "hrealpow_two_le_add_order";
Addsimps [hrealpow_two_le_add_order];
Goal "(0::hypreal) <= u ^ 2 + v ^ 2 + w ^ 2";
-by (auto_tac (claset() addSIs [hypreal_le_add_order],simpset()));
+by (auto_tac (claset() addSIs [hypreal_le_add_order], simpset()));
qed "hrealpow_two_le_add_order2";
Addsimps [hrealpow_two_le_add_order2];
@@ -132,12 +131,12 @@
Addsimps [hrealpow_two_hrabs];
Goal "!!r. 1hr < r ==> 1hr < r ^ 2";
-by (auto_tac (claset(),simpset() addsimps [hrealpow_two]));
+by (auto_tac (claset(), simpset() addsimps [hrealpow_two]));
by (cut_facts_tac [hypreal_zero_less_one] 1);
by (forw_inst_tac [("R1.0","0")] hypreal_less_trans 1);
by (assume_tac 1);
by (dres_inst_tac [("z","r"),("x","1hr")] hypreal_mult_less_mono1 1);
-by (auto_tac (claset() addIs [hypreal_less_trans],simpset()));
+by (auto_tac (claset() addIs [hypreal_less_trans], simpset()));
qed "hrealpow_two_gt_one";
Goal "!!r. 1hr <= r ==> 1hr <= r ^ 2";
@@ -151,7 +150,8 @@
by (forw_inst_tac [("n1","n")]
((hypreal_not_refl2 RS not_sym) RS hrealpow_not_zero RS not_sym) 1);
by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq]
- addIs [hypreal_mult_order],simpset()));
+ addIs [hypreal_mult_order],
+ simpset()));
qed "hrealpow_Suc_gt_zero";
Goal "!!r. (0::hypreal) <= r ==> 0 <= r ^ Suc n";
@@ -170,8 +170,9 @@
Goal "hypreal_of_nat n < (1hr + 1hr) ^ n";
by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_nat_Suc,hypreal_of_nat_zero,
- hypreal_zero_less_one,hypreal_add_mult_distrib,hypreal_of_nat_one]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_of_nat_Suc,hypreal_of_nat_zero,
+ hypreal_zero_less_one,hypreal_add_mult_distrib,hypreal_of_nat_one]));
by (blast_tac (claset() addSIs [hypreal_add_less_le_mono,
two_hrealpow_ge_one]) 1);
qed "two_hrealpow_gt";
@@ -195,21 +196,21 @@
Goal "(0::hypreal) < r & r < 1hr --> r ^ Suc n < r ^ n";
by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps
- [hypreal_mult_less_mono2]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_mult_less_mono2]));
qed_spec_mp "hrealpow_Suc_less";
Goal "(0::hypreal) <= r & r < 1hr --> r ^ Suc n <= r ^ n";
by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [hypreal_less_imp_le] addSDs
- [hypreal_le_imp_less_or_eq,hrealpow_Suc_less],simpset()
- addsimps [hypreal_le_refl,hypreal_mult_less_mono2]));
+by (auto_tac (claset() addIs [hypreal_less_imp_le]
+ addSDs [hypreal_le_imp_less_or_eq,hrealpow_Suc_less],
+ simpset() addsimps [hypreal_le_refl,hypreal_mult_less_mono2]));
qed_spec_mp "hrealpow_Suc_le";
(* a few more theorems needed here *)
Goal "1hr <= r --> r ^ n <= r ^ Suc n";
by (induct_tac "n" 1);
-by (auto_tac (claset() addSIs [hypreal_mult_le_le_mono1],simpset()));
+by (auto_tac (claset() addSIs [hypreal_mult_le_le_mono1], simpset()));
by (rtac ccontr 1 THEN dtac not_hypreal_leE 1);
by (dtac hypreal_le_less_trans 1 THEN assume_tac 1);
by (etac (hypreal_zero_less_one RS hypreal_less_asym) 1);
@@ -217,8 +218,8 @@
Goal "Abs_hypreal(hyprel^^{%n. X n}) ^ m = Abs_hypreal(hyprel^^{%n. (X n) ^ m})";
by (nat_ind_tac "m" 1);
-by (auto_tac (claset(),simpset() addsimps
- [hypreal_one_def,hypreal_mult]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_one_def,hypreal_mult]));
qed "hrealpow";
Goal "(x + (y::hypreal)) ^ 2 = \
@@ -238,24 +239,23 @@
"[|(0::hypreal) <= x;0 <= y;x ^ Suc n <= y ^ Suc n |] ==> x <= y";
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
- [hrealpow,hypreal_le,hypreal_mult]));
-by (ultra_tac (claset() addIs [realpow_increasing],simpset()) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [hrealpow,hypreal_le,hypreal_mult]));
+by (ultra_tac (claset() addIs [realpow_increasing], simpset()) 1);
qed "hrealpow_increasing";
goalw HyperPow.thy [hypreal_zero_def]
"!!x. [|(0::hypreal) <= x;0 <= y;x ^ Suc n = y ^ Suc n |] ==> x = y";
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
- [hrealpow,hypreal_mult,hypreal_le]));
+by (auto_tac (claset(), simpset() addsimps [hrealpow,hypreal_mult,hypreal_le]));
by (ultra_tac (claset() addIs [realpow_Suc_cancel_eq],
simpset()) 1);
qed "hrealpow_Suc_cancel_eq";
Goal "x : HFinite --> x ^ n : HFinite";
by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [HFinite_mult],simpset()));
+by (auto_tac (claset() addIs [HFinite_mult], simpset()));
qed_spec_mp "hrealpow_HFinite";
(*---------------------------------------------------------------
@@ -281,8 +281,7 @@
Goalw [hypreal_zero_def,hypnat_one_def]
"(0::hypreal) pow (n + 1hn) = 0";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps
- [hyperpow,hypnat_add]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow,hypnat_add]));
qed "hyperpow_zero";
Addsimps [hyperpow_zero];
@@ -290,7 +289,7 @@
"r ~= (0::hypreal) --> r pow n ~= 0";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow]));
by (dtac FreeUltrafilterNat_Compl_mem 1);
by (fuf_empty_tac (claset() addIs [realpow_not_zero RS notE],
simpset()) 1);
@@ -304,57 +303,56 @@
simpset() addsimps [hypreal_inverse,hyperpow]));
by (rtac FreeUltrafilterNat_subset 1);
by (auto_tac (claset() addDs [realpow_not_zero]
- addIs [realpow_inverse],simpset()));
+ addIs [realpow_inverse],
+ simpset()));
qed "hyperpow_inverse";
Goal "abs r pow n = abs (r pow n)";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_hrabs,
- hyperpow,realpow_abs]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_hrabs, hyperpow,realpow_abs]));
qed "hyperpow_hrabs";
Goal "r pow (n + m) = (r pow n) * (r pow m)";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow,hypnat_add,
- hypreal_mult,realpow_add]));
+by (auto_tac (claset(),
+ simpset() addsimps [hyperpow,hypnat_add, hypreal_mult,realpow_add]));
qed "hyperpow_add";
Goalw [hypnat_one_def] "r pow 1hn = r";
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow]));
qed "hyperpow_one";
Addsimps [hyperpow_one];
Goalw [hypnat_one_def]
"r pow (1hn + 1hn) = r * r";
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow,hypnat_add,
- hypreal_mult,realpow_two]));
+by (auto_tac (claset(),
+ simpset() addsimps [hyperpow,hypnat_add, hypreal_mult,realpow_two]));
qed "hyperpow_two";
Goalw [hypreal_zero_def]
"(0::hypreal) < r --> 0 < r pow n";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset,
- realpow_gt_zero],simpset() addsimps [hyperpow,hypreal_less,
- hypreal_le]));
+by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_gt_zero],
+ simpset() addsimps [hyperpow,hypreal_less, hypreal_le]));
qed_spec_mp "hyperpow_gt_zero";
Goal "(0::hypreal) < r --> 0 <= r pow n";
-by (blast_tac (claset() addSIs [hyperpow_gt_zero,
- hypreal_less_imp_le]) 1);
+by (blast_tac (claset() addSIs [hyperpow_gt_zero, hypreal_less_imp_le]) 1);
qed_spec_mp "hyperpow_ge_zero";
Goalw [hypreal_zero_def]
"(0::hypreal) <= r --> 0 <= r pow n";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset,
- realpow_ge_zero2],simpset() addsimps [hyperpow,hypreal_le]));
+by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_ge_zero2],
+ simpset() addsimps [hyperpow,hypreal_le]));
qed "hyperpow_ge_zero2";
Goalw [hypreal_zero_def]
@@ -369,23 +367,23 @@
Goalw [hypreal_one_def] "1hr pow n = 1hr";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow]));
qed "hyperpow_eq_one";
Addsimps [hyperpow_eq_one];
Goalw [hypreal_one_def]
"abs(-(1hr pow n)) = 1hr";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [abs_one,
- hrabs_minus_cancel,hyperpow,hypreal_hrabs]));
+by (auto_tac (claset(),
+ simpset() addsimps [abs_one, hyperpow,hypreal_hrabs]));
qed "hrabs_minus_hyperpow_one";
Addsimps [hrabs_minus_hyperpow_one];
Goalw [hypreal_one_def]
"abs((-1hr) pow n) = 1hr";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps
- [hyperpow,hypreal_minus,hypreal_hrabs]));
+by (auto_tac (claset(),
+ simpset() addsimps [hyperpow,hypreal_minus,hypreal_hrabs]));
qed "hrabs_hyperpow_minus_one";
Addsimps [hrabs_hyperpow_minus_one];
@@ -393,8 +391,8 @@
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","s")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow,
- hypreal_mult,realpow_mult]));
+by (auto_tac (claset(),
+ simpset() addsimps [hyperpow, hypreal_mult,realpow_mult]));
qed "hyperpow_mult";
Goal "(0::hypreal) <= r pow (1hn + 1hn)";
@@ -413,13 +411,13 @@
Addsimps [hyperpow_two_hrabs];
Goal "!!r. 1hr < r ==> 1hr < r pow (1hn + 1hn)";
-by (auto_tac (claset(),simpset() addsimps [hyperpow_two]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow_two]));
by (cut_facts_tac [hypreal_zero_less_one] 1);
by (forw_inst_tac [("R1.0","0")] hypreal_less_trans 1);
by (assume_tac 1);
by (dres_inst_tac [("z","r"),("x","1hr")]
hypreal_mult_less_mono1 1);
-by (auto_tac (claset() addIs [hypreal_less_trans],simpset()));
+by (auto_tac (claset() addIs [hypreal_less_trans], simpset()));
qed "hyperpow_two_gt_one";
Goal "!!r. 1hr <= r ==> 1hr <= r pow (1hn + 1hn)";
@@ -433,8 +431,8 @@
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset]
- addDs [realpow_Suc_gt_zero],simpset() addsimps [hyperpow,
- hypreal_less,hypnat_add]));
+ addDs [realpow_Suc_gt_zero],
+ simpset() addsimps [hyperpow, hypreal_less,hypnat_add]));
qed "hyperpow_Suc_gt_zero";
Goal "!!r. (0::hypreal) <= r ==> 0 <= r pow (n + 1hn)";
@@ -456,8 +454,8 @@
Goalw [hypreal_one_def]
"(-1hr) pow ((1hn + 1hn)*n) = 1hr";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow,
- hypnat_add,hypreal_minus]));
+by (auto_tac (claset(),
+ simpset() addsimps [hyperpow, hypnat_add,hypreal_minus]));
qed "hyperpow_minus_one2";
Addsimps [hyperpow_minus_one2];
@@ -488,8 +486,8 @@
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow,
- hypreal_le,hypreal_less,hypnat_less]));
+by (auto_tac (claset(),
+ simpset() addsimps [hyperpow, hypreal_le,hypreal_less,hypnat_less]));
by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1);
by (etac FreeUltrafilterNat_Int 1);
by (auto_tac (claset() addSDs [conjI RS realpow_less_le],
@@ -510,12 +508,12 @@
Goalw [hypreal_of_real_def,hypnat_of_nat_def]
"(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)";
-by (auto_tac (claset(),simpset() addsimps [hyperpow]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow]));
qed "hyperpow_realpow";
Goalw [SReal_def]
"(hypreal_of_real r) pow (hypnat_of_nat n) : SReal";
-by (auto_tac (claset(),simpset() addsimps [hyperpow_realpow]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow_realpow]));
qed "hyperpow_SReal";
Addsimps [hyperpow_SReal];
@@ -563,8 +561,7 @@
"(x ^ n : Infinitesimal) = \
\ (x pow (hypnat_of_nat n) : Infinitesimal)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hrealpow,
- hyperpow]));
+by (auto_tac (claset(), simpset() addsimps [hrealpow, hyperpow]));
qed "hrealpow_hyperpow_Infinitesimal_iff";
goal HyperPow.thy
@@ -572,8 +569,8 @@
\ ==> x ^ n : Infinitesimal";
by (auto_tac (claset() addSIs [Infinitesimal_hyperpow],
simpset() addsimps [hrealpow_hyperpow_Infinitesimal_iff,
- hypnat_of_nat_less_iff,hypnat_of_nat_zero]
- delsimps [hypnat_of_nat_less_iff RS sym]));
+ hypnat_of_nat_less_iff,hypnat_of_nat_zero]
+ delsimps [hypnat_of_nat_less_iff RS sym]));
qed "Infinitesimal_hrealpow";
--- a/src/HOL/Real/Hyperreal/Lim.ML Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Lim.ML Thu Dec 21 10:16:33 2000 +0100
@@ -55,9 +55,8 @@
qed "LIM_add";
Goalw [LIM_def] "f -- a --> L ==> (%x. -f(x)) -- a --> -L";
-by (full_simp_tac (simpset() addsimps [real_minus_add_distrib RS sym,
- abs_minus_cancel]
- delsimps [real_minus_add_distrib,real_minus_minus]) 1);
+by (full_simp_tac (simpset() addsimps [real_minus_add_distrib RS sym]
+ delsimps [real_minus_add_distrib, real_minus_minus]) 1);
qed "LIM_minus";
(*----------------------------------------------
@@ -108,8 +107,7 @@
Goal "[| f -- x --> L; f -- x --> M |] ==> L = M";
by (dtac LIM_minus 1);
by (dtac LIM_add 1 THEN assume_tac 1);
-by (auto_tac (claset() addSDs [LIM_const_eq RS sym],
- simpset()));
+by (auto_tac (claset() addSDs [LIM_const_eq RS sym], simpset()));
qed "LIM_unique";
(*-------------
@@ -142,7 +140,7 @@
qed "LIM_mult_zero";
Goalw [LIM_def] "(%x. x) -- a --> a";
-by (Auto_tac);
+by Auto_tac;
qed "LIM_self";
(*--------------------------------------------------------------
@@ -174,8 +172,7 @@
by (Step_tac 1);
by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
by (auto_tac (claset(),
- simpset() addsimps [real_add_minus_iff,
- starfun, hypreal_minus,hypreal_of_real_minus RS sym,
+ simpset() addsimps [real_add_minus_iff, starfun, hypreal_minus,
hypreal_of_real_def, hypreal_add]));
by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2 THEN Step_tac 1);
by (dres_inst_tac [("x","u")] spec 1 THEN Clarify_tac 1);
@@ -230,15 +227,14 @@
by (Step_tac 1);
by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{X})")] spec 1);
by (asm_full_simp_tac
- (simpset() addsimps [starfun,
- hypreal_minus,hypreal_of_real_minus RS sym,
+ (simpset() addsimps [starfun, hypreal_minus,
hypreal_of_real_def,hypreal_add]) 1);
by (Step_tac 1);
by (dtac (lemma_simp RS real_seq_to_hypreal_Infinitesimal) 1);
by (asm_full_simp_tac
(simpset() addsimps
[Infinitesimal_FreeUltrafilterNat_iff,hypreal_of_real_def,
- hypreal_minus,hypreal_of_real_minus,hypreal_add]) 1);
+ hypreal_minus, hypreal_add]) 1);
by (Blast_tac 1);
by (rotate_tac 2 1);
by (dres_inst_tac [("x","r")] spec 1);
@@ -264,14 +260,13 @@
Goalw [NSLIM_def]
"[| f -- x --NS> l; g -- x --NS> m |] \
\ ==> (%x. f(x) * g(x)) -- x --NS> (l * m)";
-by (auto_tac (claset() addSIs [starfun_mult_HFinite_inf_close],
+by (auto_tac (claset() addSIs [inf_close_mult_HFinite],
simpset() addsimps [hypreal_of_real_mult]));
qed "NSLIM_mult";
Goal "[| f -- x --> l; g -- x --> m |] \
\ ==> (%x. f(x) * g(x)) -- x --> (l * m)";
-by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
- NSLIM_mult]) 1);
+by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_mult]) 1);
qed "LIM_mult2";
(*----------------------------------------------
@@ -281,21 +276,20 @@
Goalw [NSLIM_def]
"[| f -- x --NS> l; g -- x --NS> m |] \
\ ==> (%x. f(x) + g(x)) -- x --NS> (l + m)";
-by (auto_tac (claset() addSIs [starfun_add_inf_close],
+by (auto_tac (claset() addSIs [inf_close_add],
simpset() addsimps [hypreal_of_real_add]));
qed "NSLIM_add";
Goal "[| f -- x --> l; g -- x --> m |] \
\ ==> (%x. f(x) + g(x)) -- x --> (l + m)";
-by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
- NSLIM_add]) 1);
+by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_add]) 1);
qed "LIM_add2";
(*----------------------------------------------
NSLIM_const
----------------------------------------------*)
Goalw [NSLIM_def] "(%x. k) -- x --NS> k";
-by (Auto_tac);
+by Auto_tac;
qed "NSLIM_const";
Addsimps [NSLIM_const];
@@ -309,14 +303,11 @@
----------------------------------------------*)
Goalw [NSLIM_def]
"f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L";
-by (auto_tac (claset() addIs [inf_close_minus],
- simpset() addsimps [starfun_minus RS sym,
- hypreal_of_real_minus]));
+by Auto_tac;
qed "NSLIM_minus";
Goal "f -- a --> L ==> (%x. -f(x)) -- a --> -L";
-by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
- NSLIM_minus]) 1);
+by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_minus]) 1);
qed "LIM_minus2";
(*----------------------------------------------
@@ -346,7 +337,6 @@
hypreal_of_real_inverse RS sym]));
by (forward_tac [inf_close_hypreal_of_real_not_zero] 1 THEN assume_tac 1);
by (dtac hypreal_of_real_HFinite_diff_Infinitesimal 1);
-by (stac (starfun_inverse RS sym) 1);
by (auto_tac (claset() addSEs [inf_close_inverse],
simpset() addsimps [hypreal_of_real_zero_iff]));
qed "NSLIM_inverse";
@@ -387,7 +377,7 @@
NSLIM_not_zero
--------------------------*)
Goalw [NSLIM_def] "k ~= #0 ==> ~ ((%x. k) -- x --NS> #0)";
-by (Auto_tac);
+by Auto_tac;
by (res_inst_tac [("x","hypreal_of_real x + ehr")] exI 1);
by (auto_tac (claset() addIs [Infinitesimal_add_inf_close_self
RS inf_close_sym],simpset()));
@@ -482,10 +472,10 @@
Goalw [isNSCont_def,NSLIM_def]
"f -- a --NS> (f a) ==> isNSCont f a";
-by (Auto_tac);
+by Auto_tac;
by (res_inst_tac [("Q","y = hypreal_of_real a")]
(excluded_middle RS disjE) 1);
-by (Auto_tac);
+by Auto_tac;
qed "NSLIM_isNSCont";
(*-----------------------------------------------------
@@ -569,16 +559,18 @@
sum continuous
------------------------*)
Goal "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) + g(x)) a";
-by (auto_tac (claset() addIs [starfun_add_inf_close],simpset() addsimps
- [isNSCont_isCont_iff RS sym,isNSCont_def,hypreal_of_real_add]));
+by (auto_tac (claset() addIs [inf_close_add],
+ simpset() addsimps [isNSCont_isCont_iff RS sym, isNSCont_def,
+ hypreal_of_real_add]));
qed "isCont_add";
(*------------------------
mult continuous
------------------------*)
Goal "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a";
-by (auto_tac (claset() addSIs [starfun_mult_HFinite_inf_close],simpset() addsimps
- [isNSCont_isCont_iff RS sym,isNSCont_def,hypreal_of_real_mult]));
+by (auto_tac (claset() addSIs [starfun_mult_HFinite_inf_close],
+ simpset() delsimps [starfun_mult RS sym]
+ addsimps [isNSCont_isCont_iff RS sym, isNSCont_def, hypreal_of_real_mult]));
qed "isCont_mult";
(*-------------------------------------------
@@ -597,8 +589,7 @@
qed "isCont_o2";
Goalw [isNSCont_def] "isNSCont f a ==> isNSCont (%x. - f x) a";
-by (auto_tac (claset(),simpset() addsimps [starfun_minus RS sym,
- hypreal_of_real_minus]));
+by Auto_tac;
qed "isNSCont_minus";
Goal "isCont f a ==> isCont (%x. - f x) a";
@@ -632,13 +623,14 @@
Addsimps [isNSCont_const];
Goalw [isNSCont_def] "isNSCont abs a";
-by (auto_tac (claset() addIs [inf_close_hrabs],simpset() addsimps
- [hypreal_of_real_hrabs RS sym,starfun_rabs_hrabs]));
+by (auto_tac (claset() addIs [inf_close_hrabs],
+ simpset() addsimps [hypreal_of_real_hrabs RS sym,
+ starfun_rabs_hrabs]));
qed "isNSCont_rabs";
Addsimps [isNSCont_rabs];
Goal "isCont abs a";
-by (auto_tac (claset(),simpset() addsimps [isNSCont_isCont_iff RS sym]));
+by (auto_tac (claset(), simpset() addsimps [isNSCont_isCont_iff RS sym]));
qed "isCont_rabs";
Addsimps [isCont_rabs];
@@ -756,7 +748,7 @@
\ {n. abs (X n + - Y n) < inverse (real_of_posnat n) & \
\ r <= abs (f (X n) + - f(Y n))} <= \
\ {n. r <= abs (Ya n)}";
-by (Auto_tac);
+by Auto_tac;
val lemma_Intu = result ();
Goalw [isNSUCont_def,isUCont_def,inf_close_def]
@@ -771,7 +763,7 @@
by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{Y})")] spec 1);
by (asm_full_simp_tac (simpset() addsimps [starfun,
hypreal_minus,hypreal_add]) 1);
-by (Auto_tac);
+by Auto_tac;
by (dtac (lemma_simpu RS real_seq_to_hypreal_Infinitesimal2) 1);
by (asm_full_simp_tac (simpset() addsimps
[Infinitesimal_FreeUltrafilterNat_iff,
@@ -884,9 +876,7 @@
by (rtac ccontr 3);
by (dres_inst_tac [("x","h")] spec 3);
by (auto_tac (claset(),
- simpset() addsimps [mem_infmal_iff,
- starfun_divide RS sym, starfun_add RS sym,
- hypreal_of_real_minus, starfun_lambda_cancel]));
+ simpset() addsimps [mem_infmal_iff, starfun_lambda_cancel]));
qed "NSDERIV_NSLIM_iff";
(*--- second equivalence ---*)
@@ -947,9 +937,7 @@
by (subgoal_tac "(*f* (%z. z - x)) xa ~= (0::hypreal)" 2);
by (rotate_tac ~1 2);
by (auto_tac (claset(),
- simpset() addsimps [starfun_divide RS sym,
- starfun_add RS sym, real_diff_def,
- hypreal_of_real_minus, hypreal_diff_def,
+ simpset() addsimps [real_diff_def, hypreal_diff_def,
(inf_close_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),
Infinitesimal_subset_HFinite RS subsetD]));
qed "NSDERIVD5";
@@ -1048,9 +1036,9 @@
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff,
NSLIM_def]) 1 THEN REPEAT(Step_tac 1));
by (auto_tac (claset(),
- simpset() addsimps [starfun_divide RS sym, starfun_add RS sym,
- hypreal_of_real_minus, hypreal_of_real_add, hypreal_of_real_divide,
- hypreal_add_divide_distrib]));
+ simpset() addsimps [hypreal_of_real_add,
+ hypreal_of_real_divide,
+ hypreal_add_divide_distrib]));
by (thin_tac "xa @= hypreal_of_real #0" 1 THEN dtac inf_close_add 1);
by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
qed "NSDERIV_add";
@@ -1068,10 +1056,10 @@
----------------------------------------------------*)
(* lemma - terms manipulation tedious as usual*)
-Goal "((a::real)*b) + -(c*d) = (b*(a + -c)) + \
+Goal "((a::hypreal)*b) + -(c*d) = (b*(a + -c)) + \
\ (c*(b + -d))";
-by (full_simp_tac (simpset() addsimps [real_add_mult_distrib2,
- real_minus_mult_eq2 RS sym,real_mult_commute]) 1);
+by (full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
+ hypreal_minus_mult_eq2 RS sym,hypreal_mult_commute]) 1);
val lemma_nsderiv1 = result();
Goal "[| (x + y) / z = hypreal_of_real D + yb; z ~= 0; \
@@ -1085,20 +1073,19 @@
by (etac (Infinitesimal_subset_HFinite RS subsetD) 1);
val lemma_nsderiv2 = result();
+
Goal "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \
\ ==> NSDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))";
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def]) 1
THEN REPEAT(Step_tac 1));
by (auto_tac (claset(),
- simpset() addsimps [starfun_divide RS sym, starfun_mult RS sym,
- starfun_add RS sym,starfun_lambda_cancel,hypreal_of_real_zero,
+ simpset() addsimps [starfun_lambda_cancel, hypreal_of_real_zero,
lemma_nsderiv1]));
-by (simp_tac (simpset() addsimps [hypreal_add_divide_distrib]) 1);
+by (simp_tac (simpset() addsimps [hypreal_add_divide_distrib]) 1);
by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
by (auto_tac (claset(),
simpset() delsimps [hypreal_times_divide1_eq]
- addsimps [hypreal_times_divide1_eq RS sym,
- hypreal_of_real_minus]));
+ addsimps [hypreal_times_divide1_eq RS sym]));
by (dres_inst_tac [("D","Db")] lemma_nsderiv2 1);
by (dtac (inf_close_minus_iff RS iffD2 RS (bex_Infinitesimal_iff2 RS iffD2)) 4);
by (auto_tac (claset() addSIs [inf_close_add_mono1],
@@ -1148,13 +1135,12 @@
(*--------------------------------
Negation of function
-------------------------------*)
-Goal "NSDERIV f x :> D \
-\ ==> NSDERIV (%x. -(f x)) x :> -D";
+Goal "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D";
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff]) 1);
by (res_inst_tac [("t","f x")] (real_minus_minus RS subst) 1);
by (asm_simp_tac (simpset() addsimps [real_minus_add_distrib RS sym,
- real_minus_mult_eq1 RS sym] delsimps [real_minus_add_distrib,
- real_minus_minus]) 1);
+ real_minus_mult_eq1 RS sym]
+ delsimps [real_minus_add_distrib, real_minus_minus]) 1);
by (etac NSLIM_minus 1);
qed "NSDERIV_minus";
@@ -1254,7 +1240,7 @@
\ xa ~= 0 \
\ |] ==> D = #0";
by (dtac bspec 1);
-by (Auto_tac);
+by Auto_tac;
by (asm_full_simp_tac (simpset() addsimps [hypreal_of_real_zero RS sym]) 1);
qed "NSDERIV_zero";
@@ -1267,7 +1253,7 @@
[mem_infmal_iff RS sym]) 1);
by (rtac Infinitesimal_ratio 1);
by (rtac inf_close_hypreal_of_real_HFinite 3);
-by (Auto_tac);
+by Auto_tac;
qed "NSDERIV_inf_close";
(*---------------------------------------------------------------
@@ -1285,9 +1271,7 @@
\ / ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real (g x)) \
\ @= hypreal_of_real(Da)";
by (auto_tac (claset(),
- simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def, starfun_divide RS sym,
- hypreal_of_real_minus,
- starfun_add RS sym]));
+ simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def]));
qed "NSDERIVD1";
(*--------------------------------------------------------------
@@ -1301,9 +1285,8 @@
\ ==> ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa \
\ @= hypreal_of_real(Db)";
by (auto_tac (claset(),
- simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def, starfun_divide RS sym,
- starfun_add RS sym, hypreal_of_real_zero, mem_infmal_iff,
- starfun_lambda_cancel,hypreal_of_real_minus]));
+ simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def,
+ hypreal_of_real_zero, mem_infmal_iff, starfun_lambda_cancel]));
qed "NSDERIVD2";
(*---------------------------------------------
@@ -1315,9 +1298,9 @@
by (asm_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff,
NSLIM_def,hypreal_of_real_zero,mem_infmal_iff RS sym]) 1 THEN Step_tac 1);
by (forw_inst_tac [("f","g")] NSDERIV_inf_close 1);
-by (auto_tac (claset(),simpset() addsimps [starfun_add RS sym,
- hypreal_of_real_minus, hypreal_of_real_mult,
- starfun_lambda_cancel2,starfun_o RS sym, starfun_divide RS sym]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_of_real_mult,
+ starfun_lambda_cancel2, starfun_o RS sym]));
by (case_tac "(*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real (g x)" 1);
by (dres_inst_tac [("g","g")] NSDERIV_zero 1);
by (auto_tac (claset(),
@@ -1351,7 +1334,7 @@
Goal "NSDERIV (%x. x) x :> #1";
by (auto_tac (claset(),
simpset() addsimps [NSDERIV_NSLIM_iff,
- NSLIM_def, starfun_divide RS sym,starfun_Id, hypreal_of_real_zero,
+ NSLIM_def ,starfun_Id, hypreal_of_real_zero,
hypreal_of_real_one]));
qed "NSDERIV_Id";
Addsimps [NSDERIV_Id];
@@ -1396,31 +1379,15 @@
Power of -1
---------------------------------------------------------------*)
-
-
-(*??REPLACE THE ONE IN HYPERDEF*??*)
-Goal "inverse(x*y) = inverse(x)*inverse(y::hypreal)";
-by (case_tac "x=0 | y=0" 1);
-by (force_tac (claset(), simpset() addsimps [HYPREAL_INVERSE_ZERO]) 1);
-by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_mult_assoc RS sym, hypreal_mult_not_0]));
-by (res_inst_tac [("c1","y")] (hypreal_mult_right_cancel RS iffD1) 1);
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac));
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_mult_assoc RS sym, hypreal_mult_not_0]));
-qed "inverse_mult_eq";
-
-(**?? FIXME messy proof, needs simprocs! ??*)
(*Can't get rid of x ~= #0 because it isn't continuous at zero*)
Goalw [nsderiv_def]
"x ~= #0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))";
by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1);
by (forward_tac [Infinitesimal_add_not_zero] 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 2);
by (auto_tac (claset(),
simpset() addsimps [starfun_inverse_inverse,
- hypreal_of_real_inverse RS sym,hypreal_of_real_minus,realpow_two,
+ hypreal_of_real_inverse RS sym, realpow_two,
hypreal_of_real_mult,
hypreal_of_real_divide]
delsimps [hypreal_minus_mult_eq1 RS sym,
@@ -1432,16 +1399,6 @@
@ hypreal_add_ac @ hypreal_mult_ac
delsimps [hypreal_minus_mult_eq1 RS sym,
hypreal_minus_mult_eq2 RS sym] ) 1);
-by (stac hypreal_inverse_add 1);
-by (asm_full_simp_tac (simpset() addsimps []) 1);
-by (stac hypreal_add_commute 1);
-by (asm_simp_tac (simpset() addsimps []) 1);
-by (asm_full_simp_tac
- (simpset() addsimps [hypreal_inverse_add,
- inverse_mult_eq RS sym, hypreal_minus_inverse RS sym]
- @ hypreal_add_ac @ hypreal_mult_ac
- delsimps [hypreal_minus_mult_eq1 RS sym,
- hypreal_minus_mult_eq2 RS sym] ) 1);
by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym,
hypreal_add_mult_distrib2]
delsimps [hypreal_minus_mult_eq1 RS sym,
@@ -1449,8 +1406,10 @@
by (dres_inst_tac [("x3","x") ] ((HFinite_hypreal_of_real RSN
(2,Infinitesimal_HFinite_mult2)) RS
(Infinitesimal_minus_iff RS iffD1)) 1);
-by (forw_inst_tac [("x","hypreal_of_real x"),("y","hypreal_of_real x")] hypreal_mult_not_0 1);
-by (res_inst_tac [("y"," inverse(- hypreal_of_real x * hypreal_of_real x)")] inf_close_trans 2);
+by (forw_inst_tac [("x","hypreal_of_real x"),("y","hypreal_of_real x")]
+ hypreal_mult_not_0 1);
+by (res_inst_tac [("y"," inverse(- hypreal_of_real x * hypreal_of_real x)")]
+ inf_close_trans 2);
by (rtac inverse_add_Infinitesimal_inf_close2 2);
by (auto_tac (claset() addIs [HFinite_minus_iff RS iffD1]
addSDs [Infinitesimal_minus_iff RS iffD2,
@@ -1533,11 +1492,9 @@
\ ==> NSDERIV f x :> l";
by (auto_tac (claset(),
simpset() delsimprocs real_cancel_factor
- addsimps [NSDERIV_iff2, starfun_mult RS sym,
- starfun_divide RS sym]));
+ addsimps [NSDERIV_iff2]));
by (auto_tac (claset(),
- simpset() addsimps [hypreal_mult_assoc,
- starfun_diff RS sym]));
+ simpset() addsimps [hypreal_mult_assoc]));
by (asm_full_simp_tac (simpset() addsimps [hypreal_eq_minus_iff3 RS sym,
hypreal_diff_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [isNSCont_def]) 1);
@@ -1545,16 +1502,16 @@
-(*----------------------------------------------------------------------------*)
-(* Useful lemmas about nested intervals and proof by bisection (cf.Harrison) *)
-(*----------------------------------------------------------------------------*)
+(*--------------------------------------------------------------------------*)
+(* Lemmas about nested intervals and proof by bisection (cf.Harrison) *)
+(* All considerably tidied by lcp *)
+(*--------------------------------------------------------------------------*)
Goal "(ALL n. (f::nat=>real) n <= f (Suc n)) --> f m <= f(m + no)";
by (induct_tac "no" 1);
by (auto_tac (claset() addIs [real_le_trans],simpset()));
qed_spec_mp "lemma_f_mono_add";
-
Goal "[| ALL n. f(n) <= f(Suc n); \
\ ALL n. g(Suc n) <= g(n); \
\ ALL n. f(n) <= g(n) |] \
@@ -1588,7 +1545,7 @@
by (subgoal_tac "lim f <= f(no + n)" 1);
by (induct_tac "no" 2);
by (auto_tac (claset() addIs [real_le_trans],
- simpset() addsimps [real_diff_def, abs_real_def]));
+ simpset() addsimps [real_diff_def, real_abs_def]));
by (dres_inst_tac [("i","f(no + n)"),("no1","no")]
(lemma_f_mono_add RSN (2,real_less_le_trans)) 1);
by (auto_tac (claset(), simpset() addsimps [add_commute]));
@@ -1625,7 +1582,6 @@
convergent_LIMSEQ_iff]));
qed "lemma_nest";
-
Goal "[| ALL n. f(n) <= f(Suc n); \
\ ALL n. g(Suc n) <= g(n); \
\ ALL n. f(n) <= g(n); \
@@ -1638,15 +1594,29 @@
by (auto_tac (claset() addIs [LIMSEQ_unique], simpset()));
qed "lemma_nest_unique";
-Goal "EX! fn. (fn 0 = e) & (ALL n. fn (Suc n) = f n (fn n))";
-by (rtac ex1I 1);
-by (rtac conjI 1 THEN rtac allI 2);
-by (rtac def_nat_rec_0 1 THEN rtac def_nat_rec_Suc 2);
-by (Auto_tac);
-by (rtac ext 1 THEN induct_tac "n" 1);
-by (Auto_tac);
-qed "nat_Axiom";
+
+Goal "a <= b ==> \
+\ ALL n. fst (Bolzano_bisect P a b n) <= snd (Bolzano_bisect P a b n)";
+by (rtac allI 1);
+by (induct_tac "n" 1);
+by (auto_tac (claset(), simpset() addsimps [Let_def, split_def]));
+qed "Bolzano_bisect_le";
+Goal "a <= b ==> \
+\ ALL n. fst(Bolzano_bisect P a b n) <= fst (Bolzano_bisect P a b (Suc n))";
+by (rtac allI 1);
+by (induct_tac "n" 1);
+by (auto_tac (claset(),
+ simpset() addsimps [Bolzano_bisect_le, Let_def, split_def]));
+qed "Bolzano_bisect_fst_le_Suc";
+
+Goal "a <= b ==> \
+\ ALL n. snd(Bolzano_bisect P a b (Suc n)) <= snd (Bolzano_bisect P a b n)";
+by (rtac allI 1);
+by (induct_tac "n" 1);
+by (auto_tac (claset(),
+ simpset() addsimps [Bolzano_bisect_le, Let_def, split_def]));
+qed "Bolzano_bisect_Suc_le_snd";
Goal "((x::real) = y / (#2 * z)) = (#2 * x = y/z)";
by Auto_tac;
@@ -1654,131 +1624,90 @@
by Auto_tac;
qed "eq_divide_2_times_iff";
+Goal "a <= b ==> \
+\ snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) = \
+\ (b-a) / (#2 ^ n)";
+by (induct_tac "n" 1);
+by (auto_tac (claset(),
+ simpset() addsimps [eq_divide_2_times_iff, real_add_divide_distrib,
+ Let_def, split_def]));
+by (auto_tac (claset(),
+ simpset() addsimps [Bolzano_bisect_le, real_diff_def]));
+qed "Bolzano_bisect_diff";
-val [prem1,prem2] =
-Goal "[| !!a b c. [| a <= b; b <= c; P(a,b); P(b,c)|] ==> P(a,c); \
+val Bolzano_nest_unique =
+ [Bolzano_bisect_fst_le_Suc, Bolzano_bisect_Suc_le_snd, Bolzano_bisect_le]
+ MRS lemma_nest_unique;
+
+(*P_prem is a looping simprule, so it works better if it isn't an assumption*)
+val P_prem::notP_prem::rest =
+Goal "[| !!a b c. [| P(a,b); P(b,c); a <= b; b <= c|] ==> P(a,c); \
+\ ~ P(a,b); a <= b |] ==> \
+\ ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))";
+by (cut_facts_tac rest 1);
+by (induct_tac "n" 1);
+by (auto_tac (claset(),
+ simpset() delsimps [surjective_pairing RS sym]
+ addsimps [notP_prem, Let_def, split_def]));
+by (swap_res_tac [P_prem] 1);
+by (assume_tac 1);
+by (auto_tac (claset(), simpset() addsimps [Bolzano_bisect_le]));
+qed "not_P_Bolzano_bisect";
+
+(*Now we re-package P_prem as a formula*)
+Goal "[| ALL a b c. P(a,b) & P(b,c) & a <= b & b <= c --> P(a,c); \
+\ ~ P(a,b); a <= b |] ==> \
+\ ALL n. ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))";
+by (blast_tac (claset() addSEs [not_P_Bolzano_bisect RSN (2,rev_notE)]) 1);
+qed "not_P_Bolzano_bisect'";
+
+
+Goal "[| ALL a b c. P(a,b) & P(b,c) & a <= b & b <= c --> P(a,c); \
\ ALL x. EX d::real. 0 < d & \
-\ (ALL a b. a <= x & x <= b & (b - a) < d --> P(a,b)) \
-\ |] ==> ALL a b. a <= b --> P(a,b)";
-by (Step_tac 1);
-by (cut_inst_tac [("e","(a,b)"),
- ("f","%n fn. if P(fst fn, (fst fn + snd fn)/#2) \
-\ then ((fst fn + snd fn) /#2,snd fn) \
-\ else (fst fn,(fst fn + snd fn)/#2)")]
- nat_Axiom 1);
-by (etac ex1E 1 THEN etac conjE 1 THEN rtac ccontr 1);
-(* set up 1st premise of lemma_nest_unique *)
-by (subgoal_tac "ALL n. fst((fn::nat =>(real*real)) n) <= snd (fn n)" 1);
-by (rtac allI 2);
-by (induct_tac "n" 2);
-by (Asm_simp_tac 2);
-by (dres_inst_tac [("x","na")] spec 2);
-by (case_tac "P (fst (fn na), (fst (fn na) + snd (fn na)) / #2)" 2);
-by (Asm_simp_tac 3);
-by (Asm_simp_tac 2);
-(* 2nd premise *)
-by (subgoal_tac "ALL n. fst(fn n) <= fst (fn (Suc n))" 1);
-by (rtac allI 2);
-by (induct_tac "n" 2);
-by (dres_inst_tac [("x","0")] spec 2);
-by (Asm_simp_tac 3); (*super slow, but proved!*)
-by (Asm_simp_tac 2);
-(* 3rd premise? [lcp] *)
-by (subgoal_tac "ALL n. ~P(fst(fn n),snd(fn n))" 1);
-by (rtac allI 2);
-by (induct_tac "n" 2);
-by (Asm_simp_tac 2);
-by (Asm_simp_tac 2 THEN rtac impI 2);
-by (rtac ccontr 2);
-by (res_inst_tac [("Pa","P (fst (fn na), snd (fn na))")] swap 2);
-by (assume_tac 2);
-by (res_inst_tac [("b","(fst(fn na) + snd(fn na))/#2")] prem1 2);
-by (Asm_full_simp_tac 4);
-by (Asm_full_simp_tac 4);
-by (Asm_full_simp_tac 2);
-by (Asm_simp_tac 2);
-(* 3rd premise [looks like the 4th to lcp!] *)
-by (subgoal_tac "ALL n. snd(fn (Suc n)) <= snd (fn n)" 1);
-by (rtac allI 2);
-by (induct_tac "n" 2);
-by (Asm_simp_tac 2);
-by (Asm_simp_tac 2);
-(* FIXME: simplification takes a very long time! *)
-by (ALLGOALS(thin_tac "ALL y. \
-\ y 0 = (a, b) & \
-\ (ALL n. \
-\ y (Suc n) = \
-\ (if P (fst (y n), (fst (y n) + snd (y n)) /#2) \
-\ then ((fst (y n) + snd (y n)) /#2, snd (y n)) \
-\ else (fst (y n),\
-\ (fst (y n) + snd (y n)) /#2))) --> \
-\ y = fn"));
-(*another premise? the 5th? lcp*)
-by (subgoal_tac "ALL n. snd(fn n) - fst(fn n) = \
-\ (b - a) * inverse(#2 ^ n)" 1);
-by (rtac allI 2);
-by (induct_tac "n" 2);
-by (Asm_simp_tac 2);
-by (asm_full_simp_tac
- (simpset() addsimps [eq_divide_2_times_iff, real_inverse_eq_divide,
- real_diff_mult_distrib2]) 2);
-(*end of the premises [lcp]*)
-by (dtac lemma_nest_unique 1);
-by (REPEAT(assume_tac 1));
-by (Step_tac 2);
+\ (ALL a b. a <= x & x <= b & (b - a) < d --> P(a,b)); \
+\ a <= b |] \
+\ ==> P(a,b)";
+by (rtac (inst "P1" "P" Bolzano_nest_unique RS exE) 1);
+by (REPEAT (assume_tac 1));
by (rtac LIMSEQ_minus_cancel 1);
-by (asm_simp_tac (simpset() addsimps [CLAIM "-((a::real) - b) = (b - a)",
- realpow_inverse]) 1);
-by (subgoal_tac "#0 = (b-a) * #0" 1);
-by (eres_inst_tac [("t","#0")] ssubst 1);
-by (rtac (LIMSEQ_const RS LIMSEQ_mult) 1);
-by (rtac LIMSEQ_realpow_zero 1);
-by (Asm_full_simp_tac 3);
-by (EVERY1[Simp_tac, Simp_tac]);
-by (cut_facts_tac [prem2] 1);
-by (dres_inst_tac [("x","l")] spec 1 THEN Step_tac 1);
+by (asm_simp_tac (simpset() addsimps [Bolzano_bisect_diff,
+ LIMSEQ_divide_realpow_zero]) 1);
+by (rtac ccontr 1);
+by (dtac not_P_Bolzano_bisect' 1);
+by (REPEAT (assume_tac 1));
+by (rename_tac "l" 1);
+by (dres_inst_tac [("x","l")] spec 1 THEN Clarify_tac 1);
by (rewtac LIMSEQ_def);
-by (dres_inst_tac [("x","d/#2")] spec 1);
-by (dres_inst_tac [("x","d/#2")] spec 1);
+by (dres_inst_tac [("P", "%r. #0<r --> ?Q r"), ("x","d/#2")] spec 1);
+by (dres_inst_tac [("P", "%r. #0<r --> ?Q r"), ("x","d/#2")] spec 1);
by (dtac real_less_half_sum 1);
-by (thin_tac "ALL n. \
-\ fn (Suc n) = \
-\ (if P (fst (fn n), (fst (fn n) + snd (fn n))/#2) \
-\ then ((fst (fn n) + snd (fn n))/#2, snd (fn n)) \
-\ else (fst (fn n), \
-\ (fst (fn n) + snd (fn n))/#2))" 1);
-by (Step_tac 1);
-by (ALLGOALS(Asm_full_simp_tac));
-by (dres_inst_tac [("x","fst(fn (no + noa))")] spec 1);
-by (dres_inst_tac [("x","snd(fn (no + noa))")] spec 1);
-by (Step_tac 1);
-by (ALLGOALS(Asm_full_simp_tac));
-by (res_inst_tac [("j","abs(fst(fn(no + noa)) - l) + \
-\ abs(snd(fn(no + noa)) - l)")] real_le_less_trans 1);
-by (rtac (real_sum_of_halves RS subst) 2);
-by (rewtac real_diff_def);
-by (rtac real_add_less_mono 2);
-
-by (Asm_full_simp_tac 2);
-by (Asm_full_simp_tac 2);
-by (res_inst_tac [("y1","fst(fn (no + noa)) ")]
- (abs_minus_add_cancel RS subst) 1);
-by (subgoal_tac "#0 <= (l + - fst (fn (no + noa)))" 1);
-by (subgoal_tac "#0 <= (snd (fn (no + noa)) + - l)" 1);
-by (asm_simp_tac (simpset() addsimps [abs_eqI1] @ real_add_ac) 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps real_add_divide_distrib::real_add_ac)));
+by Safe_tac;
+(*linear arithmetic bug if we just use Asm_simp_tac*)
+by (ALLGOALS Asm_full_simp_tac);
+by (dres_inst_tac [("x","fst(Bolzano_bisect P a b (no + noa))")] spec 1);
+by (dres_inst_tac [("x","snd(Bolzano_bisect P a b (no + noa))")] spec 1);
+by Safe_tac;
+by (ALLGOALS Asm_simp_tac);
+by (res_inst_tac [("j","abs(fst(Bolzano_bisect P a b(no + noa)) - l) + \
+\ abs(snd(Bolzano_bisect P a b(no + noa)) - l)")]
+ real_le_less_trans 1);
+by (asm_simp_tac (simpset() addsimps [real_abs_def]) 1);
+by (rtac (real_sum_of_halves RS subst) 1);
+by (rtac real_add_less_mono 1);
+by (ALLGOALS
+ (asm_full_simp_tac (simpset() addsimps [symmetric real_diff_def])));
qed "lemma_BOLZANO";
+
Goal "((ALL a b c. (a <= b & b <= c & P(a,b) & P(b,c)) --> P(a,c)) & \
-\ (ALL x. EX d::real. 0 < d & \
+\ (ALL x. EX d::real. 0 < d & \
\ (ALL a b. a <= x & x <= b & (b - a) < d --> P(a,b)))) \
-\ --> (ALL a b. a <= b --> P(a,b))";
-by (Step_tac 1);
-by (rtac (lemma_BOLZANO RS allE) 1);
-by (assume_tac 2);
-by (ALLGOALS(Blast_tac));
+\ --> (ALL a b. a <= b --> P(a,b))";
+by (Clarify_tac 1);
+by (blast_tac (claset() addIs [lemma_BOLZANO]) 1);
qed "lemma_BOLZANO2";
+
(*----------------------------------------------------------------------------*)
(* Intermediate Value Theorem (prove contrapositive by bisection) *)
(*----------------------------------------------------------------------------*)
@@ -1906,7 +1835,7 @@
by (auto_tac (claset() addIs [abs_triangle_ineq RSN (2, real_le_trans)],
simpset() addsimps [real_diff_def,abs_ge_self]));
by (auto_tac (claset(),
- simpset() addsimps [abs_real_def] addsplits [split_if_asm]));
+ simpset() addsimps [real_abs_def] addsplits [split_if_asm]));
qed "isCont_bounded";
(*----------------------------------------------------------------------------*)
@@ -1923,7 +1852,7 @@
\ (ALL N. N < M --> (EX x. a <= x & x <= b & N < f(x)))";
by (cut_inst_tac [("S","Collect (%y. EX x. a <= x & x <= b & y = f x)")]
lemma_reals_complete 1);
-by (Auto_tac);
+by Auto_tac;
by (dtac isCont_bounded 1 THEN assume_tac 1);
by (auto_tac (claset(),simpset() addsimps [isUb_def,leastP_def,
isLub_def,setge_def,setle_def]));
@@ -2000,7 +1929,7 @@
by (blast_tac (claset() addIs [isCont_minus]) 2);
by (dres_inst_tac [("f","(%x. -(f x))")] isCont_eq_Ub 1);
by (Step_tac 1);
-by (Auto_tac);
+by Auto_tac;
qed "isCont_eq_Lb";
@@ -2042,7 +1971,7 @@
by (asm_full_simp_tac (simpset() addsimps [real_0_less_mult_iff]) 2);
by (dres_inst_tac [("x","h")] spec 1);
by (asm_full_simp_tac
- (simpset() addsimps [abs_real_def, real_inverse_eq_divide,
+ (simpset() addsimps [real_abs_def, real_inverse_eq_divide,
pos_real_le_divide_eq, pos_real_less_divide_eq]
addsplits [split_if_asm]) 1);
qed "DERIV_left_inc";
@@ -2056,7 +1985,7 @@
by (asm_full_simp_tac (simpset() addsimps [real_mult_less_0_iff]) 2);
by (dres_inst_tac [("x","-h")] spec 1);
by (asm_full_simp_tac
- (simpset() addsimps [abs_real_def, real_inverse_eq_divide,
+ (simpset() addsimps [real_abs_def, real_inverse_eq_divide,
pos_real_less_divide_eq,
symmetric real_diff_def]
addsplits [split_if_asm]) 1);
@@ -2080,7 +2009,7 @@
by (Step_tac 1);
by (dres_inst_tac [("x","x - e")] spec 1);
by (dres_inst_tac [("x","x + e")] spec 2);
-by (auto_tac (claset(),simpset() addsimps [abs_eqI2,abs_minus_cancel]));
+by (auto_tac (claset(), simpset() addsimps [abs_eqI2]));
qed "DERIV_local_max";
(*----------------------------------------------------------------------------*)
@@ -2116,14 +2045,14 @@
by (Step_tac 1);
by (res_inst_tac [("x","x - a")] exI 1);
by (res_inst_tac [("x","b - x")] exI 2);
-by (Auto_tac);
+by Auto_tac;
by (auto_tac (claset(),simpset() addsimps [real_less_diff_eq]));
qed "lemma_interval_lt";
Goal "[| a < x; x < b |] ==> \
\ EX d::real. #0 < d & (ALL y. abs(x - y) < d --> a <= y & y <= b)";
by (dtac lemma_interval_lt 1);
-by (Auto_tac);
+by Auto_tac;
by (auto_tac (claset() addSIs [exI] ,simpset()));
qed "lemma_interval";
@@ -2270,7 +2199,7 @@
by (dres_inst_tac [("x","a")] real_le_imp_less_or_eq 1);
by (Step_tac 1);
by (dres_inst_tac [("b","x")] DERIV_isconst_end 1);
-by (Auto_tac);
+by Auto_tac;
qed "DERIV_isconst1";
Goal "[| a < b; \
@@ -2289,7 +2218,7 @@
Goal "[|a ~= b; ALL x. DERIV f x :> k |] ==> (f(b) - f(a)) = (b - a) * k";
by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1);
-by (Auto_tac);
+by Auto_tac;
by (ALLGOALS(dres_inst_tac [("f","f")] MVT));
by (auto_tac (claset() addDs [DERIV_isCont,DERIV_unique],simpset() addsimps
[differentiable_def]));
@@ -2319,7 +2248,7 @@
Goal "[|a ~= (b::real); ALL x. DERIV v x :> k|] \
\ ==> v((a + b)/#2) = (v a + v b)/#2";
by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1);
-by (Auto_tac);
+by Auto_tac;
by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1);
by (ftac DERIV_const_ratio_const2 2 THEN assume_tac 2);
by (dtac real_less_half_sum 1);
--- a/src/HOL/Real/Hyperreal/Lim.thy Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Lim.thy Thu Dec 21 10:16:33 2000 +0100
@@ -62,5 +62,18 @@
isNSUCont :: (real=>real) => bool
"isNSUCont f == (ALL x y. x @= y --> (*f* f) x @= (*f* f) y)"
+
+(*Used in the proof of the Bolzano theorem*)
+consts
+ Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)"
+
+primrec
+ "Bolzano_bisect P a b 0 = (a,b)"
+ "Bolzano_bisect P a b (Suc n) =
+ (let (x,y) = Bolzano_bisect P a b n
+ in if P(x, (x+y)/#2) then ((x+y)/#2, y)
+ else (x, (x+y)/#2) )"
+
+
end
--- a/src/HOL/Real/Hyperreal/NSA.ML Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/NSA.ML Thu Dec 21 10:16:33 2000 +0100
@@ -32,7 +32,7 @@
qed "SReal_inverse";
Goalw [SReal_def] "x: SReal ==> -x : SReal";
-by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_minus RS sym]));
+by (blast_tac (claset() addIs [hypreal_of_real_minus RS sym]) 1);
qed "SReal_minus";
Goal "[| x + y : SReal; y: SReal |] ==> x: SReal";
@@ -220,7 +220,7 @@
qed "HFinite_mult";
Goalw [HFinite_def] "(x:HFinite)=(-x:HFinite)";
-by (simp_tac (simpset() addsimps [hrabs_minus_cancel]) 1);
+by (Simp_tac 1);
qed "HFinite_minus_iff";
Goal "[| x: HFinite; y: HFinite|] ==> (x + -y): HFinite";
@@ -298,7 +298,7 @@
Goalw [Infinitesimal_def]
"(x:Infinitesimal) = (-x:Infinitesimal)";
-by (full_simp_tac (simpset() addsimps [hrabs_minus_cancel]) 1);
+by (Full_simp_tac 1);
qed "Infinitesimal_minus_iff";
Goal "x ~:Infinitesimal = (-x ~:Infinitesimal)";
@@ -389,8 +389,7 @@
qed "HInfinite_add_gt_zero";
Goalw [HInfinite_def] "(-x: HInfinite) = (x: HInfinite)";
-by (auto_tac (claset(),simpset() addsimps
- [hrabs_minus_cancel]));
+by Auto_tac;
qed "HInfinite_minus_iff";
Goal "[|x: HInfinite; y <= 0; x <= 0|] ==> (x + y): HInfinite";
@@ -592,7 +591,7 @@
qed "inf_close_minus";
Goal "-a @= -b ==> a @= b";
-by (auto_tac (claset() addDs [inf_close_minus],simpset()));
+by (auto_tac (claset() addDs [inf_close_minus], simpset()));
qed "inf_close_minus2";
Goal "(-a @= -b) = (a @= b)";
@@ -615,12 +614,6 @@
by (asm_simp_tac (simpset() addsimps [inf_close_mult1,hypreal_mult_commute]) 1);
qed "inf_close_mult2";
-val [prem1,prem2,prem3,prem4] =
-goal thy "[|a @= b; c @= d; b: HFinite; c: HFinite|] ==> a*c @= b*d";
-by (fast_tac (claset() addIs [([prem1,prem4] MRS inf_close_mult1),
- ([prem2,prem3] MRS inf_close_mult2),inf_close_trans]) 1);
-qed "inf_close_mult_HFinite";
-
Goal "[|u @= v*x; x @= y; v: HFinite|] ==> u @= v*y";
by (fast_tac (claset() addIs [inf_close_mult2,inf_close_trans]) 1);
qed "inf_close_mult_subst";
@@ -730,7 +723,7 @@
by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1);
by (Step_tac 1);
by (dtac (Infinitesimal_subset_HFinite RS subsetD
- RS (HFinite_minus_iff RS iffD1)) 1);
+ RS (HFinite_minus_iff RS iffD1)) 1);
by (dtac HFinite_add 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
qed "inf_close_HFinite";
@@ -740,10 +733,18 @@
by Auto_tac;
qed "inf_close_hypreal_of_real_HFinite";
+Goal "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d";
+by (rtac inf_close_trans 1);
+by (rtac inf_close_mult2 2);
+by (rtac inf_close_mult1 1);
+by (blast_tac (claset() addIs [inf_close_HFinite, inf_close_sym]) 2);
+by Auto_tac;
+qed "inf_close_mult_HFinite";
+
Goal "[|a @= hypreal_of_real b; c @= hypreal_of_real d |] \
\ ==> a*c @= hypreal_of_real b*hypreal_of_real d";
by (blast_tac (claset() addSIs [inf_close_mult_HFinite,
- inf_close_hypreal_of_real_HFinite,HFinite_hypreal_of_real]) 1);
+ inf_close_hypreal_of_real_HFinite,HFinite_hypreal_of_real]) 1);
qed "inf_close_mult_hypreal_of_real";
Goal "[| a: SReal; a ~= 0; a*x @= 0 |] ==> x @= 0";
@@ -886,7 +887,7 @@
Goal "[| x @= y; y : HFinite - Infinitesimal |] \
\ ==> x : HFinite - Infinitesimal";
by (auto_tac (claset() addIs [inf_close_sym RSN (2,inf_close_HFinite)],
- simpset() addsimps [mem_infmal_iff]));
+ simpset() addsimps [mem_infmal_iff]));
by (dtac inf_close_trans3 1 THEN assume_tac 1);
by (blast_tac (claset() addDs [inf_close_sym]) 1);
qed "HFinite_diff_Infinitesimal_inf_close";
@@ -1457,12 +1458,14 @@
by (dtac (hypreal_less_minus_iff RS iffD1) 1 THEN Step_tac 1);
by (rtac (hypreal_less_minus_iff RS iffD2) 1);
by (dres_inst_tac [("x","hypreal_of_real y + -hypreal_of_real x")] bspec 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_add_commute,
- hypreal_of_real_minus RS sym, hypreal_of_real_add RS sym,
- hrabs_interval_iff]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_add_commute,
+ hypreal_of_real_add, hrabs_interval_iff,
+ SReal_add, SReal_minus]));
by (dres_inst_tac [("x1","xa")] (hypreal_less_minus_iff RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_minus,
- hypreal_minus_add_distrib,hypreal_of_real_add] @ hypreal_add_ac));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_minus_add_distrib,hypreal_of_real_add] @
+ hypreal_add_ac));
qed "Infinitesimal_add_hypreal_of_real_less";
Goal "[| x: Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |] \
@@ -2241,12 +2244,14 @@
-----------------------------------------------------*)
Goal "ALL n. abs(X n + -x) < inverse(real_of_posnat n) \
\ ==> Abs_hypreal(hyprel^^{X}) + -hypreal_of_real x : Infinitesimal";
-by (auto_tac (claset() addSIs [bexI] addDs [rename_numerals
- FreeUltrafilterNat_inverse_real_of_posnat,
- FreeUltrafilterNat_all,FreeUltrafilterNat_Int] addIs [order_less_trans,
- FreeUltrafilterNat_subset],simpset() addsimps [hypreal_minus,
- hypreal_of_real_minus RS sym,hypreal_of_real_def,hypreal_add,
- Infinitesimal_FreeUltrafilterNat_iff,hypreal_inverse,hypreal_of_real_of_posnat]));
+by (auto_tac (claset() addSIs [bexI]
+ addDs [rename_numerals FreeUltrafilterNat_inverse_real_of_posnat,
+ FreeUltrafilterNat_all,FreeUltrafilterNat_Int]
+ addIs [order_less_trans, FreeUltrafilterNat_subset],
+ simpset() addsimps [hypreal_minus,
+ hypreal_of_real_def,hypreal_add,
+ Infinitesimal_FreeUltrafilterNat_iff,hypreal_inverse,
+ hypreal_of_real_of_posnat]));
qed "real_seq_to_hypreal_Infinitesimal";
Goal "ALL n. abs(X n + -x) < inverse(real_of_posnat n) \
@@ -2274,4 +2279,3 @@
[Infinitesimal_FreeUltrafilterNat_iff,hypreal_minus,hypreal_add,
hypreal_inverse,hypreal_of_real_of_posnat]));
qed "real_seq_to_hypreal_Infinitesimal2";
-
\ No newline at end of file
--- a/src/HOL/Real/Hyperreal/NatStar.ML Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/NatStar.ML Thu Dec 21 10:16:33 2000 +0100
@@ -8,16 +8,14 @@
Goalw [starsetNat_def]
"*sNat*(UNIV::nat set) = (UNIV::hypnat set)";
-by (auto_tac (claset(),simpset() addsimps
- [FreeUltrafilterNat_Nat_set]));
+by (auto_tac (claset(), simpset() addsimps [FreeUltrafilterNat_Nat_set]));
qed "NatStar_real_set";
Goalw [starsetNat_def] "*sNat* {} = {}";
by (Step_tac 1);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (dres_inst_tac [("x","%n. xa n")] bspec 1);
-by (auto_tac (claset(),simpset() addsimps
- [FreeUltrafilterNat_empty]));
+by (auto_tac (claset(), simpset() addsimps [FreeUltrafilterNat_empty]));
qed "NatStar_empty_set";
Addsimps [NatStar_empty_set];
@@ -25,8 +23,7 @@
Goalw [starsetNat_def]
"*sNat* (A Un B) = *sNat* A Un *sNat* B";
by (Auto_tac);
-by (REPEAT(blast_tac (claset() addIs
- [FreeUltrafilterNat_subset]) 2));
+by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2));
by (dtac FreeUltrafilterNat_Compl_mem 1);
by (dtac bspec 1 THEN assume_tac 1);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
@@ -39,14 +36,15 @@
by Auto_tac;
by (dres_inst_tac [("x","Xa")] bspec 1);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
-by (auto_tac (claset() addSDs [bspec],simpset()));
+by (auto_tac (claset() addSDs [bspec], simpset()));
by (TRYALL(Ultra_tac));
qed "starsetNat_n_Un";
Goalw [InternalNatSets_def]
"[| X : InternalNatSets; Y : InternalNatSets |] \
\ ==> (X Un Y) : InternalNatSets";
-by (auto_tac (claset(),simpset() addsimps [starsetNat_n_Un RS sym]));
+by (auto_tac (claset(),
+ simpset() addsimps [starsetNat_n_Un RS sym]));
qed "InternalNatSets_Un";
Goalw [starsetNat_def] "*sNat* (A Int B) = *sNat* A Int *sNat* B";
@@ -60,14 +58,16 @@
Goalw [starsetNat_n_def]
"*sNatn* (%n. (A n) Int (B n)) = *sNatn* A Int *sNatn* B";
by (Auto_tac);
-by (auto_tac (claset() addSDs [bspec],simpset()));
+by (auto_tac (claset() addSDs [bspec],
+ simpset()));
by (TRYALL(Ultra_tac));
qed "starsetNat_n_Int";
Goalw [InternalNatSets_def]
"[| X : InternalNatSets; Y : InternalNatSets |] \
\ ==> (X Int Y) : InternalNatSets";
-by (auto_tac (claset(),simpset() addsimps [starsetNat_n_Int RS sym]));
+by (auto_tac (claset(),
+ simpset() addsimps [starsetNat_n_Int RS sym]));
qed "InternalNatSets_Int";
Goalw [starsetNat_def] "*sNat* (-A) = -(*sNat* A)";
@@ -88,7 +88,8 @@
Goalw [InternalNatSets_def]
"X :InternalNatSets ==> -X : InternalNatSets";
-by (auto_tac (claset(),simpset() addsimps [starsetNat_n_Compl RS sym]));
+by (auto_tac (claset(),
+ simpset() addsimps [starsetNat_n_Compl RS sym]));
qed "InternalNatSets_Compl";
Goalw [starsetNat_n_def]
@@ -96,27 +97,28 @@
by (Auto_tac);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 3);
-by (auto_tac (claset() addSDs [bspec],simpset()));
+by (auto_tac (claset() addSDs [bspec], simpset()));
by (TRYALL(Ultra_tac));
qed "starsetNat_n_diff";
Goalw [InternalNatSets_def]
"[| X : InternalNatSets; Y : InternalNatSets |] \
\ ==> (X - Y) : InternalNatSets";
-by (auto_tac (claset(),simpset() addsimps [starsetNat_n_diff RS sym]));
+by (auto_tac (claset(), simpset() addsimps [starsetNat_n_diff RS sym]));
qed "InternalNatSets_diff";
-Goalw [starsetNat_def] "!!A. A <= B ==> *sNat* A <= *sNat* B";
+Goalw [starsetNat_def] "A <= B ==> *sNat* A <= *sNat* B";
by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1));
qed "NatStar_subset";
Goalw [starsetNat_def,hypnat_of_nat_def]
- "!!A. a : A ==> hypnat_of_nat a : *sNat* A";
-by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],simpset()));
+ "a : A ==> hypnat_of_nat a : *sNat* A";
+by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],
+ simpset()));
qed "NatStar_mem";
Goalw [starsetNat_def] "hypnat_of_nat `` A <= *sNat* A";
-by (auto_tac (claset(),simpset() addsimps [hypnat_of_nat_def]));
+by (auto_tac (claset(), simpset() addsimps [hypnat_of_nat_def]));
by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
qed "NatStar_hypreal_of_real_image_subset";
@@ -127,7 +129,8 @@
Goalw [starsetNat_def]
"*sNat* X Int SHNat = hypnat_of_nat `` X";
-by (auto_tac (claset(),simpset() addsimps
+by (auto_tac (claset(),
+ simpset() addsimps
[hypnat_of_nat_def,SHNat_def]));
by (fold_tac [hypnat_of_nat_def]);
by (rtac imageI 1 THEN rtac ccontr 1);
@@ -137,7 +140,7 @@
by (Auto_tac);
qed "NatStar_hypreal_of_real_Int";
-Goal "!!x. x ~: hypnat_of_nat `` A ==> ALL y: A. x ~= hypnat_of_nat y";
+Goal "x ~: hypnat_of_nat `` A ==> ALL y: A. x ~= hypnat_of_nat y";
by (Auto_tac);
qed "lemma_not_hypnatA";
@@ -146,12 +149,13 @@
qed "starsetNat_starsetNat_n_eq";
Goalw [InternalNatSets_def] "(*sNat* X) : InternalNatSets";
-by (auto_tac (claset(),simpset() addsimps [starsetNat_starsetNat_n_eq]));
+by (auto_tac (claset(),
+ simpset() addsimps [starsetNat_starsetNat_n_eq]));
qed "InternalNatSets_starsetNat_n";
Addsimps [InternalNatSets_starsetNat_n];
Goal "X : InternalNatSets ==> UNIV - X : InternalNatSets";
-by (auto_tac (claset() addIs [InternalNatSets_Compl],simpset()));
+by (auto_tac (claset() addIs [InternalNatSets_Compl], simpset()));
qed "InternalNatSets_UNIV_diff";
(*------------------------------------------------------------------
@@ -160,7 +164,7 @@
-----------------------------------------------------------------*)
Goalw [starsetNat_n_def,starsetNat_def]
- "!!A. ALL n. (As n = A) ==> *sNatn* As = *sNat* A";
+ "ALL n. (As n = A) ==> *sNatn* As = *sNat* A";
by (Auto_tac);
qed "starsetNat_n_starsetNat";
@@ -174,12 +178,12 @@
-----------------------------------------------------------------*)
Goalw [starfunNat_n_def,starfunNat_def]
- "!!A. ALL n. (F n = f) ==> *fNatn* F = *fNat* f";
+ "ALL n. (F n = f) ==> *fNatn* F = *fNat* f";
by (Auto_tac);
qed "starfunNat_n_starfunNat";
Goalw [starfunNat2_n_def,starfunNat2_def]
- "!!A. ALL n. (F n = f) ==> *fNat2n* F = *fNat2* f";
+ "ALL n. (F n = f) ==> *fNat2n* F = *fNat2* f";
by (Auto_tac);
qed "starfunNat2_n_starfunNat2";
@@ -214,14 +218,12 @@
---------------------------------------------*)
Goal "(*fNat* f) xa * (*fNat* g) xa = (*fNat* (%x. f x * g x)) xa";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps
- [starfunNat,hypreal_mult]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_mult]));
qed "starfunNat_mult";
Goal "(*fNat2* f) xa * (*fNat2* g) xa = (*fNat2* (%x. f x * g x)) xa";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps
- [starfunNat2,hypnat_mult]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_mult]));
qed "starfunNat2_mult";
(*---------------------------------------
@@ -229,29 +231,17 @@
---------------------------------------*)
Goal "(*fNat* f) xa + (*fNat* g) xa = (*fNat* (%x. f x + g x)) xa";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps
- [starfunNat,hypreal_add]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_add]));
qed "starfunNat_add";
Goal "(*fNat2* f) xa + (*fNat2* g) xa = (*fNat2* (%x. f x + g x)) xa";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps
- [starfunNat2,hypnat_add]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_add]));
qed "starfunNat2_add";
-(*--------------------------------------------
- subtraction: ( *f ) + -( *g ) = *(f + -g)
- --------------------------------------------*)
-Goal "(*fNat* f) xa + -(*fNat* g) xa = (*fNat* (%x. f x + -g x)) xa";
-by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
- hypreal_minus,hypreal_add]));
-qed "starfunNat_add_minus";
-
Goal "(*fNat2* f) xa - (*fNat2* g) xa = (*fNat2* (%x. f x - g x)) xa";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat2,
- hypnat_minus]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_minus]));
qed "starfunNat2_minus";
(*--------------------------------------
@@ -262,8 +252,7 @@
Goal "(*fNat* f) o (*fNat2* g) = (*fNat* (f o g))";
by (rtac ext 1);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat2,
- starfunNat]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat2, starfunNat]));
qed "starfunNatNat2_o";
Goal "(%x. (*fNat* f) ((*fNat2* g) x)) = (*fNat* (%x. f(g x)))";
@@ -274,7 +263,7 @@
Goal "(*fNat2* f) o (*fNat2* g) = (*fNat2* (f o g))";
by (rtac ext 1);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat2]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat2]));
qed "starfunNat2_o";
(***** ( *f::real=>real ) o ( *g::nat=>real ) = *(f o g) *****)
@@ -282,7 +271,7 @@
Goal "(*f* f) o (*fNat* g) = (*fNat* (f o g))";
by (rtac ext 1);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,starfun]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat,starfun]));
qed "starfun_stafunNat_o";
Goal "(%x. (*f* f) ((*fNat* g) x)) = (*fNat* (%x. f (g x)))";
@@ -294,23 +283,20 @@
--------------------------------------*)
Goal "(*fNat* (%x. k)) xa = hypreal_of_real k";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
- hypreal_of_real_def]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_of_real_def]));
qed "starfunNat_const_fun";
Addsimps [starfunNat_const_fun];
Goal "(*fNat2* (%x. k)) xa = hypnat_of_nat k";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat2,
- hypnat_of_nat_def]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_of_nat_def]));
qed "starfunNat2_const_fun";
Addsimps [starfunNat2_const_fun];
Goal "- (*fNat* f) x = (*fNat* (%x. - f x)) x";
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
- hypreal_minus]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_minus]));
qed "starfunNat_minus";
Goal "inverse ((*fNat* f) x) = (*fNat* (%x. inverse (f x))) x";
@@ -325,15 +311,14 @@
-------------------------------------------------------*)
Goal "(*fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)";
-by (auto_tac (claset(),simpset() addsimps
- [starfunNat,hypnat_of_nat_def,hypreal_of_real_def]));
+by (auto_tac (claset(),
+ simpset() addsimps [starfunNat,hypnat_of_nat_def,hypreal_of_real_def]));
qed "starfunNat_eq";
Addsimps [starfunNat_eq];
Goal "(*fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)";
-by (auto_tac (claset(),simpset() addsimps
- [starfunNat2,hypnat_of_nat_def]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_of_nat_def]));
qed "starfunNat2_eq";
Addsimps [starfunNat2_eq];
@@ -342,46 +327,30 @@
by (Auto_tac);
qed "starfunNat_inf_close";
-Goal "!!f. [| (*fNat* f) xa @= l; (*fNat* g) xa @= m; \
-\ l: HFinite; m: HFinite \
-\ |] ==> (*fNat* (%x. f x * g x)) xa @= l * m";
-by (dtac inf_close_mult_HFinite 1);
-by (REPEAT(assume_tac 1));
-by (auto_tac (claset() addIs [inf_close_sym RSN (2,inf_close_HFinite)],
- simpset() addsimps [starfunNat_mult]));
-qed "starfunNat_mult_HFinite_inf_close";
-
-Goal "!!f. [| (*fNat* f) xa @= l; (*fNat* g) xa @= m \
-\ |] ==> (*fNat* (%x. f x + g x)) xa @= l + m";
-by (auto_tac (claset() addIs [inf_close_add],
- simpset() addsimps [starfunNat_add RS sym]));
-qed "starfunNat_add_inf_close";
-
(*-----------------------------------------------------------------
Example of transfer of a property from reals to hyperreals
--- used for limit comparison of sequences
----------------------------------------------------------------*)
-Goal "!!f. ALL n. N <= n --> f n <= g n \
+Goal "ALL n. N <= n --> f n <= g n \
\ ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n <= (*fNat* g) n";
by (Step_tac 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
- hypnat_of_nat_def,hypreal_le,hypreal_less,
- hypnat_le,hypnat_less]));
+by (auto_tac (claset(),
+ simpset() addsimps [starfunNat, hypnat_of_nat_def,hypreal_le,
+ hypreal_less, hypnat_le,hypnat_less]));
by (Ultra_tac 1);
by Auto_tac;
qed "starfun_le_mono";
(*****----- and another -----*****)
-goal NatStar.thy
- "!!f. ALL n. N <= n --> f n < g n \
+Goal "ALL n. N <= n --> f n < g n \
\ ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n < (*fNat* g) n";
by (Step_tac 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
- hypnat_of_nat_def,hypreal_le,hypreal_less,
- hypnat_le,hypnat_less]));
+by (auto_tac (claset(),
+ simpset() addsimps [starfunNat, hypnat_of_nat_def,hypreal_le,
+ hypreal_less, hypnat_le,hypnat_less]));
by (Ultra_tac 1);
by Auto_tac;
qed "starfun_less_mono";
@@ -391,8 +360,8 @@
---------------------------------------------------------------*)
Goal "(*fNat* (%n. f (Suc n))) N = (*fNat* f) (N + 1hn)";
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
- hypnat_one_def,hypnat_add]));
+by (auto_tac (claset(),
+ simpset() addsimps [starfunNat, hypnat_one_def,hypnat_add]));
qed "starfunNat_shift_one";
(*----------------------------------------------------------------
@@ -400,8 +369,7 @@
---------------------------------------------------------------*)
Goal "(*fNat* (%n. abs (f n))) N = abs((*fNat* f) N)";
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
- hypreal_hrabs]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_hrabs]));
qed "starfunNat_rabs";
(*----------------------------------------------------------------
@@ -409,19 +377,19 @@
----------------------------------------------------------------*)
Goal "(*fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N";
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow,
- hypreal_of_real_def,starfunNat]));
+by (auto_tac (claset(),
+ simpset() addsimps [hyperpow, hypreal_of_real_def,starfunNat]));
qed "starfunNat_pow";
Goal "(*fNat* (%n. (X n) ^ m)) N = (*fNat* X) N pow hypnat_of_nat m";
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow,
- hypnat_of_nat_def,starfunNat]));
+by (auto_tac (claset(),
+ simpset() addsimps [hyperpow, hypnat_of_nat_def,starfunNat]));
qed "starfunNat_pow2";
Goalw [hypnat_of_nat_def] "(*f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n";
by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hyperpow,starfun]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow,starfun]));
qed "starfun_pow";
(*-----------------------------------------------------
@@ -430,15 +398,15 @@
Goal "(*fNat* real_of_nat) = hypreal_of_hypnat";
by (rtac ext 1);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_hypnat,starfunNat]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_of_hypnat,starfunNat]));
qed "starfunNat_real_of_nat";
Goal "N : HNatInfinite \
\ ==> (*fNat* (%x. inverse (real_of_nat x))) N = inverse(hypreal_of_hypnat N)";
by (res_inst_tac [("f1","inverse")] (starfun_stafunNat_o2 RS subst) 1);
by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat_real_of_nat,
- starfun_inverse_inverse]));
+by (auto_tac (claset(),
+ simpset() addsimps [starfunNat_real_of_nat, starfun_inverse_inverse]));
qed "starfunNat_inverse_real_of_nat_eq";
(*----------------------------------------------------------
@@ -464,8 +432,7 @@
Goal "(*fNatn* f) xa * (*fNatn* g) xa = \
\ (*fNatn* (% i x. f i x * g i x)) xa";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps
- [starfunNat_n,hypreal_mult]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_mult]));
qed "starfunNat_n_mult";
(*-----------------------------------------------
@@ -474,8 +441,7 @@
Goal "(*fNatn* f) xa + (*fNatn* g) xa = \
\ (*fNatn* (%i x. f i x + g i x)) xa";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps
- [starfunNat_n,hypreal_add]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_add]));
qed "starfunNat_n_add";
(*-------------------------------------------------
@@ -484,8 +450,8 @@
Goal "(*fNatn* f) xa + -(*fNatn* g) xa = \
\ (*fNatn* (%i x. f i x + -g i x)) xa";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat_n,
- hypreal_minus,hypreal_add]));
+by (auto_tac (claset(),
+ simpset() addsimps [starfunNat_n, hypreal_minus,hypreal_add]));
qed "starfunNat_n_add_minus";
(*--------------------------------------------------
@@ -494,22 +460,20 @@
Goal "(*fNatn* (%i x. k)) xa = hypreal_of_real k";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat_n,
- hypreal_of_real_def]));
+by (auto_tac (claset(),
+ simpset() addsimps [starfunNat_n, hypreal_of_real_def]));
qed "starfunNat_n_const_fun";
Addsimps [starfunNat_n_const_fun];
Goal "- (*fNatn* f) x = (*fNatn* (%i x. - (f i) x)) x";
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat_n,
- hypreal_minus]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat_n, hypreal_minus]));
qed "starfunNat_n_minus";
Goal "(*fNatn* f) (hypnat_of_nat n) = \
\ Abs_hypreal(hyprel ^^ {%i. f i n})";
-by (auto_tac (claset(),simpset() addsimps
- [starfunNat_n,hypnat_of_nat_def]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def]));
qed "starfunNat_n_eq";
Addsimps [starfunNat_n_eq];
@@ -517,7 +481,7 @@
by Auto_tac;
by (rtac ext 1 THEN rtac ccontr 1);
by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,hypnat_of_nat_def]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat,hypnat_of_nat_def]));
qed "starfun_eq_iff";
--- a/src/HOL/Real/Hyperreal/SEQ.ML Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/SEQ.ML Thu Dec 21 10:16:33 2000 +0100
@@ -208,16 +208,15 @@
simpset() addsimps [starfunNat_add RS sym,hypreal_of_real_add]));
qed "NSLIMSEQ_add";
-Goal "[| X ----> a; Y ----> b |] \
-\ ==> (%n. X n + Y n) ----> a + b";
+Goal "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
NSLIMSEQ_add]) 1);
qed "LIMSEQ_add";
Goalw [NSLIMSEQ_def]
"[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b";
-by (auto_tac (claset() addSIs [starfunNat_mult_HFinite_inf_close],
- simpset() addsimps [hypreal_of_real_mult]));
+by (auto_tac (claset() addSIs [inf_close_mult_HFinite],
+ simpset() addsimps [hypreal_of_real_mult, starfunNat_mult RS sym]));
qed "NSLIMSEQ_mult";
Goal "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b";
@@ -227,8 +226,7 @@
Goalw [NSLIMSEQ_def]
"X ----NS> a ==> (%n. -(X n)) ----NS> -a";
-by (auto_tac (claset() addIs [inf_close_minus],
- simpset() addsimps [starfunNat_minus RS sym, hypreal_of_real_minus]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat_minus RS sym]));
qed "NSLIMSEQ_minus";
Goal "X ----> a ==> (%n. -(X n)) ----> -a";
@@ -756,14 +754,13 @@
qed "convergent_minus_iff";
Goalw [Bseq_def] "Bseq (%n. -(X n)) = Bseq X";
-by (asm_full_simp_tac (simpset() addsimps [abs_minus_cancel]) 1);
+by (Asm_full_simp_tac 1);
qed "Bseq_minus_iff";
(*--------------------------------
**** main mono theorem ****
-------------------------------*)
-Goalw [monoseq_def]
- "[| Bseq X; monoseq X |] ==> convergent X";
+Goalw [monoseq_def] "[| Bseq X; monoseq X |] ==> convergent X";
by (Step_tac 1);
by (rtac (convergent_minus_iff RS ssubst) 2);
by (dtac (Bseq_minus_iff RS ssubst) 2);
--- a/src/HOL/Real/Hyperreal/Star.ML Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Star.ML Thu Dec 21 10:16:33 2000 +0100
@@ -212,6 +212,7 @@
by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_mult]));
qed "starfun_mult";
+Addsimps [starfun_mult RS sym];
(*---------------------------------------
addition: ( *f ) + ( *g ) = *(f + g)
@@ -220,6 +221,7 @@
by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add]));
qed "starfun_add";
+Addsimps [starfun_add RS sym];
(*--------------------------------------------
subtraction: ( *f ) + -( *g ) = *(f + -g)
@@ -229,21 +231,25 @@
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun, hypreal_minus]));
qed "starfun_minus";
+Addsimps [starfun_minus RS sym];
+(*FIXME: delete*)
Goal "(*f* f) xa + -(*f* g) xa = (*f* (%x. f x + -g x)) xa";
-by (simp_tac (simpset() addsimps [starfun_minus, starfun_add]) 1);
+by (Simp_tac 1);
qed "starfun_add_minus";
+Addsimps [starfun_add_minus RS sym];
Goalw [hypreal_diff_def,real_diff_def]
"(*f* f) xa - (*f* g) xa = (*f* (%x. f x - g x)) xa";
by (rtac starfun_add_minus 1);
qed "starfun_diff";
+Addsimps [starfun_diff RS sym];
(*--------------------------------------
composition: ( *f ) o ( *g ) = *(f o g)
---------------------------------------*)
-Goal "(%x. (*f* f) ((*f* g) x)) = *f* (%x. f (g x))";
+Goal "(%x. (*f* f) ((*f* g) x)) = *f* (%x. f (g x))";
by (rtac ext 1);
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun]));
@@ -343,13 +349,12 @@
by (dtac inf_close_mult_HFinite 1);
by (REPEAT(assume_tac 1));
by (auto_tac (claset() addIs [inf_close_sym RSN (2,inf_close_HFinite)],
- simpset() addsimps [starfun_mult]));
+ simpset()));
qed "starfun_mult_HFinite_inf_close";
Goal "[| (*f* f) xa @= l; (*f* g) xa @= m \
\ |] ==> (*f* (%x. f x + g x)) xa @= l + m";
-by (auto_tac (claset() addIs [inf_close_add],
- simpset() addsimps [starfun_add RS sym]));
+by (auto_tac (claset() addIs [inf_close_add], simpset()));
qed "starfun_add_inf_close";
(*----------------------------------------------------
@@ -363,7 +368,7 @@
Goal "*f* abs = abs";
by (rtac (hrabs_is_starext_rabs RS
- (is_starext_starfun_iff RS iffD1) RS sym) 1);
+ (is_starext_starfun_iff RS iffD1) RS sym) 1);
qed "starfun_rabs_hrabs";
Goal "(*f* inverse) x = inverse(x)";
@@ -382,11 +387,13 @@
by (auto_tac (claset(),
simpset() addsimps [starfun, hypreal_inverse]));
qed "starfun_inverse";
+Addsimps [starfun_inverse RS sym];
Goalw [hypreal_divide_def,real_divide_def]
"(*f* f) xa / (*f* g) xa = (*f* (%x. f x / g x)) xa";
-by (simp_tac (simpset() addsimps [starfun_inverse, starfun_mult]) 1);
+by Auto_tac;
qed "starfun_divide";
+Addsimps [starfun_divide RS sym];
Goal "inverse ((*f* f) x) = (*f* (%x. inverse (f x))) x";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
@@ -424,12 +431,13 @@
by its NS extenson ( *f* f). See second NS set extension below.
----------------------------------------------------------------*)
Goalw [starset_def]
- "*s* {x. abs (x + - y) < r} = {x. abs(x + -hypreal_of_real y) < hypreal_of_real r}";
+ "*s* {x. abs (x + - y) < r} = \
+\ {x. abs(x + -hypreal_of_real y) < hypreal_of_real r}";
by (Step_tac 1);
by (ALLGOALS(res_inst_tac [("z","x")] eq_Abs_hypreal));
by (auto_tac (claset() addSIs [exI] addSDs [bspec],
- simpset() addsimps [hypreal_minus, hypreal_of_real_def,hypreal_add,
- hypreal_hrabs,hypreal_less_def]));
+ simpset() addsimps [hypreal_minus, hypreal_of_real_def,hypreal_add,
+ hypreal_hrabs,hypreal_less_def]));
by (Fuf_tac 1);
qed "STAR_rabs_add_minus";
--- a/src/HOL/Real/RealAbs.ML Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/RealAbs.ML Thu Dec 21 10:16:33 2000 +0100
@@ -8,7 +8,7 @@
(** abs (absolute value) **)
-Goalw [abs_real_def]
+Goalw [real_abs_def]
"abs (number_of v :: real) = \
\ (if neg (number_of v) then number_of (bin_minus v) \
\ else number_of v)";
@@ -21,7 +21,7 @@
Addsimps [abs_nat_number_of];
-Goalw [abs_real_def]
+Goalw [real_abs_def]
"P(abs (x::real)) = ((#0 <= x --> P x) & (x < #0 --> P(-x)))";
by(auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
qed "abs_split";
@@ -32,63 +32,63 @@
(adapted version of previously proved theorems about abs)
----------------------------------------------------------------------------*)
-Goalw [abs_real_def] "abs (r::real) = (if #0<=r then r else -r)";
+Goalw [real_abs_def] "abs (r::real) = (if #0<=r then r else -r)";
by Auto_tac;
qed "abs_iff";
-Goalw [abs_real_def] "abs #0 = (#0::real)";
+Goalw [real_abs_def] "abs #0 = (#0::real)";
by Auto_tac;
qed "abs_zero";
Addsimps [abs_zero];
-Goalw [abs_real_def] "abs (#0::real) = -#0";
+Goalw [real_abs_def] "abs (#0::real) = -#0";
by (Simp_tac 1);
qed "abs_minus_zero";
-Goalw [abs_real_def] "(#0::real)<=x ==> abs x = x";
+Goalw [real_abs_def] "(#0::real)<=x ==> abs x = x";
by (Asm_simp_tac 1);
qed "abs_eqI1";
-Goalw [abs_real_def] "(#0::real)<x ==> abs x = x";
+Goalw [real_abs_def] "(#0::real)<x ==> abs x = x";
by (Asm_simp_tac 1);
qed "abs_eqI2";
-Goalw [abs_real_def,real_le_def] "x<(#0::real) ==> abs x = -x";
+Goalw [real_abs_def,real_le_def] "x<(#0::real) ==> abs x = -x";
by (Asm_simp_tac 1);
qed "abs_minus_eqI2";
-Goalw [abs_real_def] "x<=(#0::real) ==> abs x = -x";
+Goalw [real_abs_def] "x<=(#0::real) ==> abs x = -x";
by (Asm_simp_tac 1);
qed "abs_minus_eqI1";
-Goalw [abs_real_def] "(#0::real)<= abs x";
+Goalw [real_abs_def] "(#0::real)<= abs x";
by (Simp_tac 1);
qed "abs_ge_zero";
-Goalw [abs_real_def] "abs(abs x)=abs (x::real)";
+Goalw [real_abs_def] "abs(abs x)=abs (x::real)";
by (Simp_tac 1);
qed "abs_idempotent";
Addsimps [abs_idempotent];
-Goalw [abs_real_def] "(abs x = #0) = (x=(#0::real))";
+Goalw [real_abs_def] "(abs x = #0) = (x=(#0::real))";
by (Full_simp_tac 1);
qed "abs_zero_iff";
AddIffs [abs_zero_iff];
-Goalw [abs_real_def] "x<=abs (x::real)";
+Goalw [real_abs_def] "x<=abs (x::real)";
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
qed "abs_ge_self";
-Goalw [abs_real_def] "-x<=abs (x::real)";
+Goalw [real_abs_def] "-x<=abs (x::real)";
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
qed "abs_ge_minus_self";
-Goalw [abs_real_def] "abs (x * y) = abs x * abs (y::real)";
+Goalw [real_abs_def] "abs (x * y) = abs x * abs (y::real)";
by (auto_tac (claset() addSDs [order_antisym],
simpset() addsimps [real_0_le_mult_iff]));
qed "abs_mult";
-Goalw [abs_real_def] "abs(inverse(x::real)) = inverse(abs(x))";
+Goalw [real_abs_def] "abs(inverse(x::real)) = inverse(abs(x))";
by (real_div_undefined_case_tac "x=0" 1);
by (auto_tac (claset(),
simpset() addsimps [real_minus_inverse, real_le_less] @
@@ -99,7 +99,7 @@
by (asm_simp_tac (simpset() addsimps [abs_mult, abs_inverse]) 1);
qed "abs_mult_inverse";
-Goalw [abs_real_def] "abs(x+y) <= abs x + abs (y::real)";
+Goalw [real_abs_def] "abs(x+y) <= abs x + abs (y::real)";
by (Simp_tac 1);
qed "abs_triangle_ineq";
@@ -108,23 +108,24 @@
by (simp_tac (simpset() addsimps [abs_triangle_ineq RS order_trans]) 1);
qed "abs_triangle_ineq_four";
-Goalw [abs_real_def] "abs(-x)=abs(x::real)";
+Goalw [real_abs_def] "abs(-x)=abs(x::real)";
by (Simp_tac 1);
qed "abs_minus_cancel";
+Addsimps [abs_minus_cancel];
-Goalw [abs_real_def] "abs(x + (-y)) = abs (y + (-(x::real)))";
+Goalw [real_abs_def] "abs(x + (-y)) = abs (y + (-(x::real)))";
by (Simp_tac 1);
qed "abs_minus_add_cancel";
-Goalw [abs_real_def] "abs(x + (-y)) <= abs x + abs (y::real)";
+Goalw [real_abs_def] "abs(x + (-y)) <= abs x + abs (y::real)";
by (Simp_tac 1);
qed "abs_triangle_minus_ineq";
-Goalw [abs_real_def] "abs x < r --> abs y < s --> abs(x+y) < r+(s::real)";
+Goalw [real_abs_def] "abs x < r --> abs y < s --> abs(x+y) < r+(s::real)";
by (Simp_tac 1);
qed_spec_mp "abs_add_less";
-Goalw [abs_real_def] "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)";
+Goalw [real_abs_def] "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)";
by (Simp_tac 1);
qed "abs_add_minus_less";
@@ -181,42 +182,38 @@
by (blast_tac (claset() addSIs [real_le_less_trans,abs_ge_zero]) 1);
qed "abs_less_gt_zero";
-Goalw [abs_real_def] "abs #1 = (#1::real)";
+Goalw [real_abs_def] "abs #1 = (#1::real)";
by (Simp_tac 1);
qed "abs_one";
-Goalw [abs_real_def] "abs (-#1) = (#1::real)";
+Goalw [real_abs_def] "abs (-#1) = (#1::real)";
by (Simp_tac 1);
qed "abs_minus_one";
Addsimps [abs_minus_one];
-Goalw [abs_real_def] "abs x =x | abs x = -(x::real)";
+Goalw [real_abs_def] "abs x =x | abs x = -(x::real)";
by Auto_tac;
qed "abs_disj";
-Goalw [abs_real_def] "(abs x < r) = (-r<x & x<(r::real))";
+Goalw [real_abs_def] "(abs x < r) = (-r<x & x<(r::real))";
by Auto_tac;
qed "abs_interval_iff";
-Goalw [abs_real_def] "(abs x <= r) = (-r<=x & x<=(r::real))";
+Goalw [real_abs_def] "(abs x <= r) = (-r<=x & x<=(r::real))";
by Auto_tac;
qed "abs_le_interval_iff";
-Goalw [abs_real_def] "(abs (x + (-y)) < r) = (y + (-r) < x & x < y + (r::real))";
-by Auto_tac;
-qed "abs_add_minus_interval_iff";
-
-Goalw [abs_real_def] "(#0::real) < k ==> #0 < k + abs(x)";
+Goalw [real_abs_def] "(#0::real) < k ==> #0 < k + abs(x)";
by Auto_tac;
qed "abs_add_pos_gt_zero";
-Goalw [abs_real_def] "(#0::real) < #1 + abs(x)";
+Goalw [real_abs_def] "(#0::real) < #1 + abs(x)";
by Auto_tac;
qed "abs_add_one_gt_zero";
Addsimps [abs_add_one_gt_zero];
(* 05/2000 *)
-Goalw [abs_real_def] "~ abs x < (#0::real)";
+Goalw [real_abs_def] "~ abs x < (#0::real)";
by Auto_tac;
qed "abs_not_less_zero";
Addsimps [abs_not_less_zero];
@@ -226,44 +223,44 @@
simpset()));
qed "abs_circle";
-Goalw [abs_real_def] "(abs x <= (#0::real)) = (x = #0)";
+Goalw [real_abs_def] "(abs x <= (#0::real)) = (x = #0)";
by Auto_tac;
qed "abs_le_zero_iff";
Addsimps [abs_le_zero_iff];
Goal "((#0::real) < abs x) = (x ~= 0)";
-by (simp_tac (simpset() addsimps [abs_real_def]) 1);
+by (simp_tac (simpset() addsimps [real_abs_def]) 1);
by (arith_tac 1);
qed "real_0_less_abs_iff";
Addsimps [real_0_less_abs_iff];
Goal "abs (real_of_nat x) = real_of_nat x";
-by (auto_tac (claset() addIs [abs_eqI1],simpset()
- addsimps [rename_numerals real_of_nat_ge_zero]));
+by (auto_tac (claset() addIs [abs_eqI1],
+ simpset() addsimps [rename_numerals real_of_nat_ge_zero]));
qed "abs_real_of_nat_cancel";
Addsimps [abs_real_of_nat_cancel];
Goal "~ abs(x) + (#1::real) < x";
by (rtac real_leD 1);
-by (auto_tac (claset() addIs [abs_ge_self RS real_le_trans],simpset()));
+by (auto_tac (claset() addIs [abs_ge_self RS real_le_trans], simpset()));
qed "abs_add_one_not_less_self";
Addsimps [abs_add_one_not_less_self];
-
+
(* used in vector theory *)
Goal "abs(w + x + (y::real)) <= abs(w) + abs(x) + abs(y)";
-by (auto_tac (claset() addSIs [(abs_triangle_ineq
- RS real_le_trans),real_add_left_le_mono1],
- simpset() addsimps [real_add_assoc]));
+by (auto_tac (claset() addSIs [abs_triangle_ineq RS real_le_trans,
+ real_add_left_le_mono1],
+ simpset() addsimps [real_add_assoc]));
qed "abs_triangle_ineq_three";
-Goalw [abs_real_def] "abs(x - y) < y ==> (#0::real) < y";
+Goalw [real_abs_def] "abs(x - y) < y ==> (#0::real) < y";
by (case_tac "#0 <= x - y" 1);
-by (Auto_tac);
+by Auto_tac;
qed "abs_diff_less_imp_gt_zero";
-Goalw [abs_real_def] "abs(x - y) < x ==> (#0::real) < x";
+Goalw [real_abs_def] "abs(x - y) < x ==> (#0::real) < x";
by (case_tac "#0 <= x - y" 1);
-by (Auto_tac);
+by Auto_tac;
qed "abs_diff_less_imp_gt_zero2";
Goal "abs(x - y) < y ==> (#0::real) < x";
@@ -274,8 +271,8 @@
by (auto_tac (claset(),simpset() addsimps [abs_interval_iff]));
qed "abs_diff_less_imp_gt_zero4";
-Goalw [abs_real_def]
- " abs(x) <= abs(x + (-y)) + abs((y::real))";
+Goalw [real_abs_def]
+ "abs(x) <= abs(x + (-y)) + abs((y::real))";
by Auto_tac;
qed "abs_triangle_ineq_minus_cancel";
--- a/src/HOL/Real/RealAbs.thy Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/RealAbs.thy Thu Dec 21 10:16:33 2000 +0100
@@ -9,6 +9,6 @@
defs
- abs_real_def "abs r == (if (#0::real) <= r then r else -r)"
+ real_abs_def "abs r == (if (#0::real) <= r then r else -r)"
end
--- a/src/HOL/Real/RealPow.ML Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/RealPow.ML Thu Dec 21 10:16:33 2000 +0100
@@ -94,15 +94,13 @@
Addsimps [realpow_eq_one];
Goal "abs(-(#1 ^ n)) = (#1::real)";
-by (simp_tac (simpset() addsimps
- [abs_minus_cancel,abs_one]) 1);
+by (simp_tac (simpset() addsimps [abs_one]) 1);
qed "abs_minus_realpow_one";
Addsimps [abs_minus_realpow_one];
Goal "abs((#-1) ^ n) = (#1::real)";
by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [abs_mult,
- abs_minus_cancel,abs_one]));
+by (auto_tac (claset(),simpset() addsimps [abs_mult,abs_one]));
qed "abs_realpow_minus_one";
Addsimps [abs_realpow_minus_one];