# HG changeset patch
# User paulson
# Date 977234819 -3600
# Node ID f0c3da8477e963c0dfbc7205a700de200cd1a79f
# Parent  dc5e984dfe1337eed59f1169ae0af825a74a07e5
more tidying

diff -r dc5e984dfe13 -r f0c3da8477e9 src/HOL/Real/Hyperreal/HRealAbs.ML
--- 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";
 
diff -r dc5e984dfe13 -r f0c3da8477e9 src/HOL/Real/Hyperreal/Lim.ML
--- 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)";
diff -r dc5e984dfe13 -r f0c3da8477e9 src/HOL/Real/Hyperreal/SEQ.ML
--- 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";
diff -r dc5e984dfe13 -r f0c3da8477e9 src/HOL/Real/Hyperreal/Series.ML
--- 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
diff -r dc5e984dfe13 -r f0c3da8477e9 src/HOL/Real/RealAbs.ML
--- 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);
diff -r dc5e984dfe13 -r f0c3da8477e9 src/HOL/Real/RealArith.ML
--- 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";
diff -r dc5e984dfe13 -r f0c3da8477e9 src/HOL/Real/RealBin.ML
--- 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];
diff -r dc5e984dfe13 -r f0c3da8477e9 src/HOL/Real/RealOrd.ML
--- 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);
diff -r dc5e984dfe13 -r f0c3da8477e9 src/HOL/Real/RealPow.ML
--- 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";