--- a/src/HOL/Real/Hyperreal/HRealAbs.ML Tue Dec 19 15:06:14 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HRealAbs.ML Tue Dec 19 15:06:59 2000 +0100
@@ -69,21 +69,17 @@
qed "hrabs_idempotent";
Addsimps [hrabs_idempotent];
-Goalw [hrabs_def] "(x=(0::hypreal)) = (abs x = (0::hypreal))";
+Goalw [hrabs_def] "(abs x = (0::hypreal)) = (x=0)";
by (Simp_tac 1);
qed "hrabs_zero_iff";
-Addsimps [hrabs_zero_iff RS sym];
+AddIffs [hrabs_zero_iff];
-Goal "(x ~= (0::hypreal)) = (abs x ~= 0)";
-by (Simp_tac 1);
-qed "hrabs_not_zero_iff";
-
-Goalw [hrabs_def] "(x::hypreal)<=abs x";
+Goalw [hrabs_def] "(x::hypreal) <= abs x";
by (auto_tac (claset() addDs [not_hypreal_leE RS hypreal_less_imp_le],
- simpset() addsimps [hypreal_le_zero_iff]));
+ simpset() addsimps [hypreal_le_zero_iff]));
qed "hrabs_ge_self";
-Goalw [hrabs_def] "-(x::hypreal)<=abs x";
+Goalw [hrabs_def] "-(x::hypreal) <= abs x";
by (full_simp_tac (simpset() addsimps [hypreal_ge_zero_iff]) 1);
qed "hrabs_ge_minus_self";
--- a/src/HOL/Real/Hyperreal/Lim.ML Tue Dec 19 15:06:14 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Lim.ML Tue Dec 19 15:06:59 2000 +0100
@@ -1769,14 +1769,23 @@
(* Intermediate Value Theorem (prove contrapositive by bisection) *)
(*----------------------------------------------------------------------------*)
+
+ (*ALREADY IN REALABS.ML????????????????*)
+ Goalw [abs_real_def] "(abs x = #0) = (x=(#0::real))";
+ by (Full_simp_tac 1);
+ qed "abs_zero_iff";
+ AddIffs [abs_zero_iff];
+
+
Goal "[| f(a) <= y & y <= f(b); \
\ a <= b; \
-\ (ALL x. a <= x & x <= b --> isCont f x) \
-\ |] ==> EX x. a <= x & x <= b & f(x) = y";
+\ (ALL x. a <= x & x <= b --> isCont f x) |] \
+\ ==> EX x. a <= x & x <= b & f(x) = y";
by (rtac contrapos_pp 1);
by (assume_tac 1);
-by (cut_inst_tac [("P","%(u,v). a <= u & u <= v & v <= b --> \
-\ ~(f(u) <= y & y <= f(v))")] lemma_BOLZANO2 1);
+by (cut_inst_tac
+ [("P","%(u,v). a <= u & u <= v & v <= b --> ~(f(u) <= y & y <= f(v))")]
+ lemma_BOLZANO2 1);
by (Step_tac 1);
by (ALLGOALS(Asm_full_simp_tac));
by (Blast_tac 2);
@@ -1784,45 +1793,31 @@
by (rtac ccontr 1);
by (subgoal_tac "a <= x & x <= b" 1);
by (Asm_full_simp_tac 2);
-by (rotate_tac 3 2);
-by (dres_inst_tac [("x","1r")] spec 2);
+by (dres_inst_tac [("P", "%d. #0<d --> ?P d"),("x","#1")] spec 2);
by (Step_tac 2);
by (Asm_full_simp_tac 2);
by (Asm_full_simp_tac 2);
by (REPEAT(blast_tac (claset() addIs [real_le_trans]) 2));
by (REPEAT(dres_inst_tac [("x","x")] spec 1));
by (Asm_full_simp_tac 1);
-(**)
-by (rotate_tac 4 1);
-by (dres_inst_tac [("x","abs(y - f x)")] spec 1);
+by (dres_inst_tac [("P", "%r. ?P r --> (EX s. #0<s & ?Q r s)"),
+ ("x","abs(y - f x)")] spec 1);
by (Step_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [real_less_le,
- abs_ge_zero,real_diff_def]) 1);
-by (dtac (sym RS (abs_zero_iff RS iffD2)) 1);
-by (arith_tac 1);
+by (asm_full_simp_tac (simpset() addsimps []) 1);
by (dres_inst_tac [("x","s")] spec 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
by (cut_inst_tac [("R1.0","f x"),("R2.0","y")] real_linear 1);
-by (Auto_tac);
+by Safe_tac;
by (dres_inst_tac [("x","ba - x")] spec 1);
-by (auto_tac (claset(),
- simpset()
- addsimps [abs_iff, real_diff_le_eq,
- (real_diff_def RS meta_eq_to_obj_eq) RS sym,
- real_less_le_iff, real_le_diff_eq,
- CLAIM "(~(x::real) <= y) = (y < x)",
- CLAIM "(-x < -y) = ((y::real) < x)",
- CLAIM "(-(y - x)) = (x - (y::real))",
- CLAIM "(x-y=#0) = (x = (y::real))"]));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [abs_iff])));
by (dres_inst_tac [("x","aa - x")] spec 1);
by (case_tac "x <= aa" 1);
-by (auto_tac (claset(),simpset() addsimps [real_minus_zero_le_iff2,
- real_le_diff_eq,real_diff_le_eq,(real_le_def RS meta_eq_to_obj_eq)
- RS sym]));
+by (ALLGOALS Asm_full_simp_tac);
by (dres_inst_tac [("z","x"),("w","aa")] real_le_anti_sym 1);
by (assume_tac 1 THEN Asm_full_simp_tac 1);
qed "IVT";
+
Goal "[| f(b) <= y & y <= f(a); \
\ a <= b; \
\ (ALL x. a <= x & x <= b --> isCont f x) \
@@ -1833,6 +1828,8 @@
by (auto_tac (claset() addIs [isCont_minus],simpset()));
qed "IVT2";
+
+(*HOL style here: object-level formulations*)
Goal "(f(a) <= y & y <= f(b) & a <= b & \
\ (ALL x. a <= x & x <= b --> isCont f x)) \
\ --> (EX x. a <= x & x <= b & f(x) = y)";
--- a/src/HOL/Real/Hyperreal/SEQ.ML Tue Dec 19 15:06:14 2000 +0100
+++ b/src/HOL/Real/Hyperreal/SEQ.ML Tue Dec 19 15:06:59 2000 +0100
@@ -203,8 +203,7 @@
qed "LIMSEQ_const";
Goalw [NSLIMSEQ_def]
- "[| X ----NS> a; Y ----NS> b |] \
-\ ==> (%n. X n + Y n) ----NS> a + b";
+ "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b";
by (auto_tac (claset() addIs [inf_close_add],
simpset() addsimps [starfunNat_add RS sym,hypreal_of_real_add]));
qed "NSLIMSEQ_add";
@@ -216,28 +215,25 @@
qed "LIMSEQ_add";
Goalw [NSLIMSEQ_def]
- "[| X ----NS> a; Y ----NS> b |] \
-\ ==> (%n. X n * Y n) ----NS> a * b";
+ "[| 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]));
qed "NSLIMSEQ_mult";
-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_mult]) 1);
+ NSLIMSEQ_mult]) 1);
qed "LIMSEQ_mult";
Goalw [NSLIMSEQ_def]
- "X ----NS> a ==> (%n. -(X n)) ----NS> -a";
+ "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]));
+ simpset() addsimps [starfunNat_minus RS sym, hypreal_of_real_minus]));
qed "NSLIMSEQ_minus";
Goal "X ----> a ==> (%n. -(X n)) ----> -a";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
- NSLIMSEQ_minus]) 1);
+ NSLIMSEQ_minus]) 1);
qed "LIMSEQ_minus";
Goal "(%n. -(X n)) ----> -a ==> X ----> a";
--- a/src/HOL/Real/Hyperreal/Series.ML Tue Dec 19 15:06:14 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Series.ML Tue Dec 19 15:06:59 2000 +0100
@@ -260,12 +260,6 @@
qed "sumr_group";
Addsimps [sumr_group];
-Goal "0 < (k::nat) --> ~(n*k < n)";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed_spec_mp "lemma_summable_group";
-Addsimps [lemma_summable_group];
-
(*-------------------------------------------------------------------
Infinite sums
Theorems follow from properties of limits and sums
--- a/src/HOL/Real/RealAbs.ML Tue Dec 19 15:06:14 2000 +0100
+++ b/src/HOL/Real/RealAbs.ML Tue Dec 19 15:06:59 2000 +0100
@@ -70,13 +70,10 @@
qed "abs_idempotent";
Addsimps [abs_idempotent];
-Goalw [abs_real_def] "(x=(#0::real)) = (abs x = #0)";
+Goalw [abs_real_def] "(abs x = #0) = (x=(#0::real))";
by (Full_simp_tac 1);
qed "abs_zero_iff";
-
-Goal "(x ~= (#0::real)) = (abs x ~= #0)";
-by (full_simp_tac (simpset() addsimps [abs_zero_iff RS sym]) 1);
-qed "abs_not_zero_iff";
+AddIffs [abs_zero_iff];
Goalw [abs_real_def] "x<=abs (x::real)";
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
--- a/src/HOL/Real/RealArith.ML Tue Dec 19 15:06:14 2000 +0100
+++ b/src/HOL/Real/RealArith.ML Tue Dec 19 15:06:59 2000 +0100
@@ -8,38 +8,6 @@
Also, common factor cancellation
*)
-(*****????????????????***VERY EARLY! (HOL itself)*********)
-Goal "(number_of w = x+y) = (x+y = number_of w)";
-by Auto_tac;
-qed "number_of_add_reorient";
-AddIffs [number_of_add_reorient];
-
-Goal "(number_of w = x-y) = (x-y = number_of w)";
-by Auto_tac;
-qed "number_of_diff_reorient";
-AddIffs [number_of_diff_reorient];
-
-Goal "(number_of w = x*y) = (x*y = number_of w)";
-by Auto_tac;
-qed "number_of_mult_reorient";
-AddIffs [number_of_mult_reorient];
-
-Goal "(number_of w = x div y) = (x div y = number_of w)";
-by Auto_tac;
-qed "number_of_div_reorient";
-AddIffs [number_of_div_reorient];
-
-Goal "(number_of w = x mod y) = (x mod y = number_of w)";
-by Auto_tac;
-qed "number_of_mod_reorient";
-AddIffs [number_of_mod_reorient];
-
-Goal "(number_of w = x/y) = (x/y = number_of w)";
-by Auto_tac;
-qed "number_of_divide_reorient";
-AddIffs [number_of_divide_reorient];
-
-
(** Division and inverse **)
Goal "#0/x = (#0::real)";
@@ -95,10 +63,27 @@
by (simp_tac (simpset() addsimps [real_divide_def]) 1);
qed "real_inverse_eq_divide";
-Goal "(x::real)/#1 = x";
-by (simp_tac (simpset() addsimps [real_divide_def]) 1);
-qed "real_divide_1";
-Addsimps [real_divide_1];
+Goal "((#0::real) < x/y) = (#0 < x & #0 < y | x < #0 & y < #0)";
+by (simp_tac (simpset() addsimps [real_divide_def, real_0_less_mult_iff]) 1);
+qed "real_0_less_divide_iff";
+Addsimps [inst "x" "number_of ?w" real_0_less_divide_iff];
+
+Goal "(x/y < (#0::real)) = (#0 < x & y < #0 | x < #0 & #0 < y)";
+by (simp_tac (simpset() addsimps [real_divide_def, real_mult_less_0_iff]) 1);
+qed "real_divide_less_0_iff";
+Addsimps [inst "x" "number_of ?w" real_divide_less_0_iff];
+
+Goal "((#0::real) <= x/y) = ((x <= #0 | #0 <= y) & (#0 <= x | y <= #0))";
+by (simp_tac (simpset() addsimps [real_divide_def, real_0_le_mult_iff]) 1);
+by Auto_tac;
+qed "real_0_le_divide_iff";
+Addsimps [inst "x" "number_of ?w" real_0_le_divide_iff];
+
+Goal "(x/y <= (#0::real)) = ((x <= #0 | y <= #0) & (#0 <= x | #0 <= y))";
+by (simp_tac (simpset() addsimps [real_divide_def, real_mult_le_0_iff]) 1);
+by Auto_tac;
+qed "real_divide_le_0_iff";
+Addsimps [inst "x" "number_of ?w" real_divide_le_0_iff];
Goal "(inverse(x::real) = #0) = (x = #0)";
by (auto_tac (claset(), simpset() addsimps [rename_numerals INVERSE_ZERO]));
@@ -521,6 +506,18 @@
real_inverse_less_iff]) 1);
qed "real_inverse_le_iff";
+(** Division by 1, -1 **)
+
+Goal "(x::real)/#1 = x";
+by (simp_tac (simpset() addsimps [real_divide_def]) 1);
+qed "real_divide_1";
+Addsimps [real_divide_1];
+
+Goal "x/#-1 = -(x::real)";
+by (Simp_tac 1);
+qed "real_divide_minus1";
+Addsimps [real_divide_minus1];
+
Goal "[| (#0::real) < d1; #0 < d2 |] ==> EX e. #0 < e & e < d1 & e < d2";
by (res_inst_tac [("x","(min d1 d2)/#2")] exI 1);
by (asm_simp_tac (simpset() addsimps [min_def]) 1);
@@ -556,6 +553,17 @@
qed "real_minus_equation";
+Goal "(x + - a = (#0::real)) = (x=a)";
+by (arith_tac 1);
+qed "real_add_minus_iff";
+Addsimps [real_add_minus_iff];
+
+Goal "(-b = -a) = (b = (a::real))";
+by (arith_tac 1);
+qed "real_minus_eq_cancel";
+Addsimps [real_minus_eq_cancel];
+
+
(*Distributive laws for literals*)
Addsimps (map (inst "w" "number_of ?v")
[real_add_mult_distrib, real_add_mult_distrib2,
@@ -574,13 +582,6 @@
qed "real_add_eq_0_iff";
AddIffs [real_add_eq_0_iff];
-(**?????????not needed with re-orientation
-Goal "((#0::real) = x+y) = (y = -x)";
-by Auto_tac;
-qed "real_0_eq_add_iff";
-AddIffs [real_0_eq_add_iff];
-????????*)
-
Goal "(x+y < (#0::real)) = (y < -x)";
by Auto_tac;
qed "real_add_less_0_iff";
@@ -602,33 +603,15 @@
AddIffs [real_0_le_add_iff];
-(*** Simprules combining x-y and #0 ***)
-
-Goal "(x-y = (#0::real)) = (x = y)";
-by Auto_tac;
-qed "real_diff_eq_0_iff";
-AddIffs [real_diff_eq_0_iff];
-
-Goal "((#0::real) = x-y) = (x = y)";
-by Auto_tac;
-qed "real_0_eq_diff_iff";
-AddIffs [real_0_eq_diff_iff];
-
-Goal "(x-y < (#0::real)) = (x < y)";
-by Auto_tac;
-qed "real_diff_less_0_iff";
-AddIffs [real_diff_less_0_iff];
+(** Simprules combining x-y and #0; see also real_less_iff_diff_less_0, etc.,
+ in RealBin
+**)
Goal "((#0::real) < x-y) = (y < x)";
by Auto_tac;
qed "real_0_less_diff_iff";
AddIffs [real_0_less_diff_iff];
-Goal "(x-y <= (#0::real)) = (x <= y)";
-by Auto_tac;
-qed "real_diff_le_0_iff";
-AddIffs [real_diff_le_0_iff];
-
Goal "((#0::real) <= x-y) = (y <= x)";
by Auto_tac;
qed "real_0_le_diff_iff";
--- a/src/HOL/Real/RealBin.ML Tue Dec 19 15:06:14 2000 +0100
+++ b/src/HOL/Real/RealBin.ML Tue Dec 19 15:06:59 2000 +0100
@@ -364,6 +364,18 @@
(*To let us treat subtraction as addition*)
val diff_simps = [real_diff_def, real_minus_add_distrib, real_minus_minus];
+(*push the unary minus down: - x * y = x * - y *)
+val real_minus_mult_eq_1_to_2 =
+ [real_minus_mult_eq1 RS sym, real_minus_mult_eq2] MRS trans |> standard;
+
+(*to extract again any uncancelled minuses*)
+val real_minus_from_mult_simps =
+ [real_minus_minus, real_minus_mult_eq1 RS sym, real_minus_mult_eq2 RS sym];
+
+(*combine unary minus with numeric literals, however nested within a product*)
+val real_mult_minus_simps =
+ [real_mult_assoc, real_minus_mult_eq1, real_minus_mult_eq_1_to_2];
+
(*Apply the given rewrite (if present) just once*)
fun trans_tac None = all_tac
| trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
@@ -400,11 +412,13 @@
val dest_coeff = dest_coeff 1
val find_first_coeff = find_first_coeff []
val trans_tac = trans_tac
- val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
- real_minus_simps@real_add_ac))
- THEN ALLGOALS
- (simp_tac (HOL_ss addsimps [real_minus_mult_eq2]@
- bin_simps@real_add_ac@real_mult_ac))
+ val norm_tac =
+ ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
+ real_minus_simps@real_add_ac))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
+ THEN ALLGOALS
+ (simp_tac (HOL_ss addsimps real_minus_from_mult_simps@
+ real_add_ac@real_mult_ac))
val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
val simplify_meta_eq = simplify_meta_eq
end;
@@ -466,12 +480,12 @@
val left_distrib = left_real_add_mult_distrib RS trans
val prove_conv = prove_conv_nohyps "real_combine_numerals"
val trans_tac = trans_tac
- val norm_tac = ALLGOALS
- (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
- real_minus_simps@real_add_ac))
- THEN ALLGOALS
- (simp_tac (HOL_ss addsimps [real_minus_mult_eq2]@
- bin_simps@real_add_ac@real_mult_ac))
+ val norm_tac =
+ ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
+ real_minus_simps@real_add_ac))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps real_minus_from_mult_simps@
+ real_add_ac@real_mult_ac))
val numeral_simp_tac = ALLGOALS
(simp_tac (HOL_ss addsimps add_0s@bin_simps))
val simplify_meta_eq = simplify_meta_eq
@@ -571,4 +585,7 @@
Addsimprocs [Real_Times_Assoc.conv];
-
+(*Simplification of x-y < 0, etc.*)
+AddIffs [real_less_iff_diff_less_0 RS sym];
+AddIffs [real_eq_iff_diff_eq_0 RS sym];
+AddIffs [real_le_iff_diff_le_0 RS sym];
--- a/src/HOL/Real/RealOrd.ML Tue Dec 19 15:06:14 2000 +0100
+++ b/src/HOL/Real/RealOrd.ML Tue Dec 19 15:06:59 2000 +0100
@@ -270,7 +270,8 @@
by (simp_tac (simpset() addsimps [real_add_assoc]) 1);
qed "real_add_minus_positive_less_self";
-Goal "((r::real) <= s) = (-s <= -r)";
+Goal "(-s <= -r) = ((r::real) <= s)";
+by (rtac sym 1);
by (Step_tac 1);
by (dres_inst_tac [("x","-s")] real_add_left_le_mono1 1);
by (dres_inst_tac [("x","r")] real_add_left_le_mono1 2);
@@ -279,7 +280,7 @@
by (dres_inst_tac [("z","s")] real_add_le_mono1 2);
by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
qed "real_le_minus_iff";
-Addsimps [real_le_minus_iff RS sym];
+Addsimps [real_le_minus_iff];
Goal "0 <= 1r";
by (rtac (real_zero_less_one RS real_less_imp_le) 1);
--- a/src/HOL/Real/RealPow.ML Tue Dec 19 15:06:14 2000 +0100
+++ b/src/HOL/Real/RealPow.ML Tue Dec 19 15:06:59 2000 +0100
@@ -143,7 +143,6 @@
by (auto_tac (claset() addSDs [real_le_imp_less_or_eq],
simpset()));
by (dtac (rename_numerals (real_zero_less_one RS real_mult_less_mono)) 1);
-by (dtac sym 4);
by (auto_tac (claset() addSIs [real_less_imp_le],
simpset() addsimps [real_zero_less_one]));
qed_spec_mp "realpow_ge_one";