# HG changeset patch
# User paulson
# Date 938104745 -7200
# Node ID 26384af933590d6202ac3b029faa97995cefde68
# Parent  ee0b835ca8fa68787df9803c3cb00bc5cb945009
Tidying to exploit the new arith_tac.  RealBin no longer imports RealPow or
RealAbs.  RealAbs proofs have been highly streamlined.  A couple of RealPow
proofs use #1, #2, etc.

diff -r ee0b835ca8fa -r 26384af93359 src/HOL/Real/Real.thy
--- a/src/HOL/Real/Real.thy	Thu Sep 23 14:39:39 1999 +0200
+++ b/src/HOL/Real/Real.thy	Thu Sep 23 18:39:05 1999 +0200
@@ -1,2 +1,2 @@
 
-Real = Main + RComplete
+Real = Main + RComplete + RealPow
diff -r ee0b835ca8fa -r 26384af93359 src/HOL/Real/RealAbs.ML
--- a/src/HOL/Real/RealAbs.ML	Thu Sep 23 14:39:39 1999 +0200
+++ b/src/HOL/Real/RealAbs.ML	Thu Sep 23 18:39:05 1999 +0200
@@ -20,36 +20,31 @@
 Addsimps [rabs_zero];
 
 Goalw [rabs_def] "rabs 0r = -0r";
-by (stac real_minus_zero 1);
-by (rtac if_cancel 1);
+by (Simp_tac 1);
 qed "rabs_minus_zero";
 
-val [prem] = goalw thy [rabs_def] "0r<=x ==> rabs x = x";
-by (rtac (prem RS if_P) 1);
+Goalw [rabs_def] "0r<=x ==> rabs x = x";
+by (Asm_simp_tac 1);
 qed "rabs_eqI1";
 
-val [prem] = goalw thy [rabs_def] "0r<x ==> rabs x = x";
-by (simp_tac (simpset() addsimps [(prem RS real_less_imp_le),rabs_eqI1]) 1);
+Goalw [rabs_def] "0r<x ==> rabs x = x";
+by (Asm_simp_tac 1);
 qed "rabs_eqI2";
 
 Goalw [rabs_def,real_le_def] "x<0r ==> rabs x = -x";
 by (Asm_simp_tac 1);
 qed "rabs_minus_eqI2";
 
-Goal "x<=0r ==> rabs x = -x";
-by (dtac real_le_imp_less_or_eq 1);
-by (blast_tac (HOL_cs addIs [rabs_minus_zero,rabs_minus_eqI2]) 1);
+Goalw [rabs_def] "x<=0r ==> rabs x = -x";
+by (asm_full_simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
 qed "rabs_minus_eqI1";
 
-Goalw [rabs_def,real_le_def] "0r<= rabs x";
-by (Full_simp_tac 1);
-by (blast_tac (claset() addDs [real_minus_zero_less_iff RS iffD2,
-			       real_less_asym]) 1);
+Goalw [rabs_def] "0r<= rabs x";
+by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
 qed "rabs_ge_zero";
 
-Goal "rabs(rabs x)=rabs x";
-by (res_inst_tac [("r1","rabs x")] (rabs_iff RS ssubst) 1);
-by (blast_tac (claset() addIs [if_P,rabs_ge_zero]) 1);
+Goalw [rabs_def] "rabs(rabs x)=rabs x";
+by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
 qed "rabs_idempotent";
 
 Goalw [rabs_def] "(x=0r) = (rabs x = 0r)";
@@ -61,13 +56,11 @@
 qed "rabs_not_zero_iff";
 
 Goalw [rabs_def] "x<=rabs x";
-by (Full_simp_tac 1);
-by (auto_tac (claset() addDs [not_real_leE RS real_less_imp_le],
-	      simpset() addsimps [real_le_zero_iff]));
+by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
 qed "rabs_ge_self";
 
 Goalw [rabs_def] "-x<=rabs x";
-by (full_simp_tac (simpset() addsimps [real_ge_zero_iff]) 1);
+by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
 qed "rabs_ge_minus_self";
 
 (* case splits nightmare *)
@@ -76,7 +69,7 @@
 	      simpset() addsimps [real_minus_mult_eq1, real_minus_mult_commute,
 				  real_minus_mult_eq2]));
 by (blast_tac (claset() addDs [real_le_mult_order]) 1);
-by (auto_tac (claset() addSDs [not_real_leE],simpset()));
+by (auto_tac (claset() addSDs [not_real_leE], simpset()));
 by (EVERY1[dtac real_mult_le_zero, assume_tac, dtac real_le_anti_sym]);
 by (EVERY[dtac real_mult_le_zero 3, assume_tac 3, dtac real_le_anti_sym 3]);
 by (dtac real_mult_less_zero1 5 THEN assume_tac 5);
@@ -96,67 +89,36 @@
 qed "rabs_rinv";
 
 Goal "y ~= 0r ==> rabs(x*rinv(y)) = rabs(x)*rinv(rabs(y))";
-by (res_inst_tac [("c1","rabs y")] (real_mult_left_cancel RS subst) 1);
-by (asm_simp_tac (simpset() addsimps [rabs_not_zero_iff RS sym]) 1);
-by (asm_simp_tac (simpset() addsimps [rabs_mult RS sym, real_mult_inv_right, 
-				 rabs_not_zero_iff RS sym] @ real_mult_ac) 1);
+by (asm_simp_tac (simpset() addsimps [rabs_mult, rabs_rinv]) 1);
 qed "rabs_mult_rinv";
 
-Goal "rabs(x+y) <= rabs x + rabs y";
-by (case_tac "0r<=x+y" 1);
-by (asm_simp_tac
-    (simpset() addsimps [rabs_eqI1,real_add_le_mono,rabs_ge_self]) 1);
-by (asm_simp_tac 
-    (simpset() addsimps [not_real_leE,rabs_minus_eqI2,real_add_le_mono,
-			 rabs_ge_minus_self]) 1);
+Goalw [rabs_def] "rabs(x+y) <= rabs x + rabs y";
+by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
 qed "rabs_triangle_ineq";
 
+(*Unused, but perhaps interesting as an example*)
 Goal "rabs(w + x + y + z) <= rabs(w) + rabs(x) + rabs(y) + rabs(z)";
-by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
-by (blast_tac (claset() addSIs [rabs_triangle_ineq RS real_le_trans,
-				real_add_left_le_mono1]) 1);
+by (simp_tac (simpset() addsimps [rabs_triangle_ineq RS order_trans]) 1);
 qed "rabs_triangle_ineq_four";
 
 Goalw [rabs_def] "rabs(-x)=rabs(x)";
-by (auto_tac (claset() addSDs [not_real_leE,real_less_asym] 
-	               addIs [real_le_anti_sym],
-		       simpset() addsimps [real_ge_zero_iff]));
+by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
 qed "rabs_minus_cancel";
 
-Goal "rabs(x + (-y)) = rabs (y + (-x))";
-by (rtac (rabs_minus_cancel RS subst) 1);
-by (simp_tac (simpset() addsimps [real_add_commute]) 1);
+Goalw [rabs_def] "rabs(x + (-y)) = rabs (y + (-x))";
+by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
 qed "rabs_minus_add_cancel";
 
-Goal "rabs(x + (-y)) <= rabs x + rabs y";
-by (res_inst_tac [("x1","y")] (rabs_minus_cancel RS subst) 1);
-by (rtac rabs_triangle_ineq 1);
+Goalw [rabs_def] "rabs(x + (-y)) <= rabs x + rabs y";
+by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
 qed "rabs_triangle_minus_ineq";
 
-Goal "rabs (x + y + ((-l) + (-m))) <= rabs(x + (-l)) + rabs(y + (-m))";
-by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
-by (res_inst_tac [("x1","y")] (real_add_left_commute RS ssubst) 1);
-by (rtac (real_add_assoc RS subst) 1);
-by (rtac rabs_triangle_ineq 1);
-qed "rabs_sum_triangle_ineq";
+Goalw [rabs_def] "rabs x < r --> rabs y < s --> rabs(x+y) < r+s";
+by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
+qed_spec_mp "rabs_add_less";
 
-Goal "rabs(x) <= rabs(x + (-y)) + rabs(y)";
-by (res_inst_tac [("j","rabs(x + (-y) + y)")] real_le_trans 1);
-by (simp_tac (simpset() addsimps [real_add_assoc]) 1);
-by (simp_tac (simpset() addsimps [real_add_assoc RS sym,
-				  rabs_triangle_ineq]) 1);
-qed "rabs_triangle_ineq_minus_cancel";
-
-Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+y) < r+s";
-by (rtac real_le_less_trans 1);
-by (rtac rabs_triangle_ineq 1);
-by (REPEAT (ares_tac [real_add_less_mono] 1));
-qed "rabs_add_less";
-
-Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+ (-y)) < r+s";
-by (rotate_tac 1 1);
-by (dtac (rabs_minus_cancel RS ssubst) 1);
-by (asm_simp_tac (simpset() addsimps [rabs_add_less]) 1);
+Goalw [rabs_def] "rabs x < r --> rabs y < s --> rabs(x+ (-y)) < r+s";
+by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
 qed "rabs_add_minus_less";
 
 (* lemmas manipulating terms *)
@@ -175,7 +137,8 @@
 			    real_mult_less_trans]) 1);
 qed "real_mult_le_less_trans";
 
-(* proofs lifted from previous older version *)
+(* proofs lifted from previous older version
+   FIXME: use a stronger version of real_mult_less_mono *)
 Goal "[| rabs x<r; rabs y<s |] ==> rabs(x*y)<r*s";
 by (simp_tac (simpset() addsimps [rabs_mult]) 1);
 by (rtac real_mult_le_less_trans 1);
@@ -214,100 +177,31 @@
 qed "rabs_less_gt_zero";
 
 Goalw [rabs_def] "rabs 1r = 1r";
-by (auto_tac (claset() addSDs [not_real_leE RS real_less_asym],
-	      simpset() addsimps [real_zero_less_one]));
+by (simp_tac (simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1]) 1);
 qed "rabs_one";
 
-Goal "[| 0r < x ; x < r |] ==> rabs x < r";
-by (asm_simp_tac (simpset() addsimps [rabs_eqI2]) 1);
-qed "rabs_lessI";
-
-Goal "rabs x =x | rabs x = -x";
-by (cut_inst_tac [("R1.0","0r"),("R2.0","x")] real_linear 1);
-by (blast_tac (claset() addIs [rabs_eqI2,rabs_minus_eqI2,
-			       rabs_zero,rabs_minus_zero]) 1);
+Goalw [rabs_def] "rabs x =x | rabs x = -x";
+by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
 qed "rabs_disj";
 
-Goal "rabs x = y ==> x = y | -x = y";
-by (dtac sym 1);
-by (hyp_subst_tac 1);
-by (res_inst_tac [("x1","x")] (rabs_disj RS disjE) 1);
-by (REPEAT(Asm_simp_tac 1));
-qed "rabs_eq_disj";
-
-Goal "(rabs x < r) = (-r<x & x<r)";
-by Safe_tac;
-by (rtac (real_less_swap_iff RS iffD2) 1);
-by (asm_simp_tac (simpset() addsimps [(rabs_ge_minus_self 
-				       RS real_le_less_trans)]) 1);
-by (asm_simp_tac (simpset() addsimps [rabs_ge_self RS real_le_less_trans]) 1);
-by (EVERY1 [dtac (real_less_swap_iff RS iffD1), rotate_tac 1, 
-            dtac (real_minus_minus RS subst), 
-            cut_inst_tac [("x","x")] rabs_disj, dtac disjE ]);
-by (assume_tac 3 THEN Auto_tac);
+Goalw [rabs_def] "(rabs x < r) = (-r<x & x<r)";
+by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
 qed "rabs_interval_iff";
 
-Goal "(rabs x < r) = (-x < r & x < r)";
-by (auto_tac (claset(),simpset() addsimps [rabs_interval_iff]));
-by (dtac (real_less_swap_iff RS iffD1) 1);
-by (dtac (real_less_swap_iff RS iffD1) 2);
-by Auto_tac;
-qed "rabs_interval_iff2";
-
-Goal "rabs x <= r ==> -r<=x & x<=r";
-by (dtac real_le_imp_less_or_eq 1);
-by (auto_tac (claset() addSDs [real_less_imp_le],
-	      simpset() addsimps [rabs_interval_iff,rabs_ge_self]));
-by (auto_tac (claset(),simpset() addsimps [real_le_def]));
-by (dtac (real_less_swap_iff RS iffD1) 1);
-by (auto_tac (claset() addSDs [rabs_ge_minus_self RS real_le_less_trans],
-	      simpset() addsimps [real_less_not_refl]));
-qed "rabs_leD";
-
-Goal "[| -r<x; x<=r |] ==> rabs x <= r";
-by (dtac real_le_imp_less_or_eq 1);
-by (Step_tac 1);
-by (blast_tac (claset() addIs 
-	       [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1);
-by (auto_tac (claset() addSDs [rabs_eqI2],
-	      simpset() addsimps 
-	        [real_le_def,real_gt_zero_iff RS sym,real_less_not_refl]));
-qed "rabs_leI1";
-
-Goal "[| -r<=x; x<=r |] ==> rabs x <= r";
-by (REPEAT(dtac real_le_imp_less_or_eq 1));
-by (Step_tac 1);
-by (blast_tac (claset() 
-	       addIs [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1);
-by (auto_tac (claset() addSDs [rabs_eqI2],
-	      simpset() addsimps 
-	      [real_le_def,real_gt_zero_iff RS sym,real_less_not_refl,
-	       rabs_minus_cancel]));
-by (cut_inst_tac [("x","r")] rabs_disj 1);
-by (rotate_tac 1 1);
-by (auto_tac (claset(), simpset() addsimps [real_less_not_refl]));
-qed "rabs_leI";
-
-Goal "(rabs x <= r) = (-r<=x & x<=r)";
-by (blast_tac (claset() addSIs [rabs_leD,rabs_leI]) 1);
+Goalw [rabs_def] "(rabs x <= r) = (-r<=x & x<=r)";
+by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
 qed "rabs_le_interval_iff";
 
-Goal "(rabs (x + (-y)) < r) = (y + (-r) < x & x < y + r)";
-by (auto_tac (claset(), simpset() addsimps [rabs_interval_iff]));
-by (ALLGOALS(dtac real_less_sum_gt_zero));
-by (ALLGOALS(dtac real_less_sum_gt_zero));
-by (ALLGOALS(rtac real_sum_gt_zero_less));
-by (auto_tac (claset(),
-	      simpset() addsimps [real_minus_add_distrib] @ real_add_ac));
+Goalw [rabs_def] "(rabs (x + (-y)) < r) = (y + (-r) < x & x < y + r)";
+by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
 qed "rabs_add_minus_interval_iff";
 
-Goal "0r < k ==> 0r < k + rabs(x)";
-by (res_inst_tac [("t","0r")] (real_add_zero_right RS subst) 1);
-by (etac (rabs_ge_zero RSN (2,real_add_less_le_mono)) 1);
+Goalw [rabs_def] "0r < k ==> 0r < k + rabs(x)";
+by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
 qed "rabs_add_pos_gt_zero";
 
-Goal "0r < 1r + rabs(x)";
-by (rtac (real_zero_less_one RS rabs_add_pos_gt_zero) 1);
+Goalw [rabs_def] "0r < 1r + rabs(x)";
+by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1]));
 qed "rabs_add_one_gt_zero";
 Addsimps [rabs_add_one_gt_zero];
 
diff -r ee0b835ca8fa -r 26384af93359 src/HOL/Real/RealAbs.thy
--- a/src/HOL/Real/RealAbs.thy	Thu Sep 23 14:39:39 1999 +0200
+++ b/src/HOL/Real/RealAbs.thy	Thu Sep 23 18:39:05 1999 +0200
@@ -5,10 +5,6 @@
     Description : Absolute value function for the reals
 *) 
 
-RealAbs = RealOrd +
+RealAbs = RealOrd + RealBin +
 
-constdefs
-   rabs   :: real => real
-   "rabs r      == if 0r<=r then r else -r" 
-
-end
\ No newline at end of file
+end
diff -r ee0b835ca8fa -r 26384af93359 src/HOL/Real/RealBin.ML
--- a/src/HOL/Real/RealBin.ML	Thu Sep 23 14:39:39 1999 +0200
+++ b/src/HOL/Real/RealBin.ML	Thu Sep 23 18:39:05 1999 +0200
@@ -58,6 +58,21 @@
 
 Addsimps [mult_real_number_of];
 
+Goal "(#2::real) = #1 + #1";
+by (Simp_tac 1);
+val lemma = result();
+
+(*For specialist use: NOT as default simprules*)
+Goal "#2 * z = (z+z::real)";
+by (simp_tac (simpset_of RealDef.thy
+	      addsimps [lemma, real_add_mult_distrib,
+			one_eq_numeral_1 RS sym]) 1);
+qed "real_mult_2";
+
+Goal "z * #2 = (z+z::real)";
+by (stac real_mult_commute 1 THEN rtac real_mult_2 1);
+qed "real_mult_2_right";
+
 
 (*** Comparisons ***)
 
@@ -141,12 +156,6 @@
 	   real_mult_minus_1_right, real_mult_minus_1, real_rinv_1,
 	   real_minus_zero_less_iff]);
 
-(** RealPow **)
-
-Addsimps (map (rename_numerals thy) 
-	  [realpow_zero, realpow_two_le, realpow_zero_le,
-	   realpow_eq_one, rabs_minus_realpow_one, rabs_realpow_minus_one,
-	   realpow_minus_one, realpow_minus_one2, realpow_minus_one_odd]);
 
 (*Perhaps add some theorems that aren't in the default simpset, as
   done in Integ/NatBin.ML*)
@@ -211,290 +220,3 @@
 
 arith_tac_split_thms := !arith_tac_split_thms @ [rabs_split];
 
-(** Tests **)
-Goal "(x + y = x) = (y = (#0::real))";
-by(arith_tac 1);
-
-Goal "(x + y = y) = (x = (#0::real))";
-by(arith_tac 1);
-
-Goal "(x + y = (#0::real)) = (x = -y)";
-by(arith_tac 1);
-
-Goal "(x + y = (#0::real)) = (y = -x)";
-by(arith_tac 1);
-
-Goal "((x + y) < (x + z)) = (y < (z::real))";
-by(arith_tac 1);
-
-Goal "((x + z) < (y + z)) = (x < (y::real))";
-by(arith_tac 1);
-
-Goal "(~ x < y) = (y <= (x::real))";
-by(arith_tac 1);
-
-Goal "~(x < y & y < (x::real))";
-by(arith_tac 1);
-
-Goal "(x::real) < y ==> ~ y < x";
-by(arith_tac 1);
-
-Goal "((x::real) ~= y) = (x < y | y < x)";
-by(arith_tac 1);
-
-Goal "(~ x <= y) = (y < (x::real))";
-by(arith_tac 1);
-
-Goal "x <= y | y <= (x::real)";
-by(arith_tac 1);
-
-Goal "x <= y | y < (x::real)";
-by(arith_tac 1);
-
-Goal "x < y | y <= (x::real)";
-by(arith_tac 1);
-
-Goal "x <= (x::real)";
-by(arith_tac 1);
-
-Goal "((x::real) <= y) = (x < y | x = y)";
-by(arith_tac 1);
-
-Goal "((x::real) <= y & y <= x) = (x = y)";
-by(arith_tac 1);
-
-Goal "~(x < y & y <= (x::real))";
-by(arith_tac 1);
-
-Goal "~(x <= y & y < (x::real))";
-by(arith_tac 1);
-
-Goal "(-x < (#0::real)) = (#0 < x)";
-by(arith_tac 1);
-
-Goal "((#0::real) < -x) = (x < #0)";
-by(arith_tac 1);
-
-Goal "(-x <= (#0::real)) = (#0 <= x)";
-by(arith_tac 1);
-
-Goal "((#0::real) <= -x) = (x <= #0)";
-by(arith_tac 1);
-
-Goal "(x::real) = y | x < y | y < x";
-by(arith_tac 1);
-
-Goal "(x::real) = #0 | #0 < x | #0 < -x";
-by(arith_tac 1);
-
-Goal "(#0::real) <= x | #0 <= -x";
-by(arith_tac 1);
-
-Goal "((x::real) + y <= x + z) = (y <= z)";
-by(arith_tac 1);
-
-Goal "((x::real) + z <= y + z) = (x <= y)";
-by(arith_tac 1);
-
-Goal "(w::real) < x & y < z ==> w + y < x + z";
-by(arith_tac 1);
-
-Goal "(w::real) <= x & y <= z ==> w + y <= x + z";
-by(arith_tac 1);
-
-Goal "(#0::real) <= x & #0 <= y ==> #0 <= x + y";
-by(arith_tac 1);
-
-Goal "(#0::real) < x & #0 < y ==> #0 < x + y";
-by(arith_tac 1);
-
-Goal "(-x < y) = (#0 < x + (y::real))";
-by(arith_tac 1);
-
-Goal "(x < -y) = (x + y < (#0::real))";
-by(arith_tac 1);
-
-Goal "(y < x + -z) = (y + z < (x::real))";
-by(arith_tac 1);
-
-Goal "(x + -y < z) = (x < z + (y::real))";
-by(arith_tac 1);
-
-Goal "x <= y ==> x < y + (#1::real)";
-by(arith_tac 1);
-
-Goal "(x - y) + y = (x::real)";
-by(arith_tac 1);
-
-Goal "y + (x - y) = (x::real)";
-by(arith_tac 1);
-
-Goal "x - x = (#0::real)";
-by(arith_tac 1);
-
-Goal "(x - y = #0) = (x = (y::real))";
-by(arith_tac 1);
-
-Goal "((#0::real) <= x + x) = (#0 <= x)";
-by(arith_tac 1);
-
-Goal "(-x <= x) = ((#0::real) <= x)";
-by(arith_tac 1);
-
-Goal "(x <= -x) = (x <= (#0::real))";
-by(arith_tac 1);
-
-Goal "(-x = (#0::real)) = (x = #0)";
-by(arith_tac 1);
-
-Goal "-(x - y) = y - (x::real)";
-by(arith_tac 1);
-
-Goal "((#0::real) < x - y) = (y < x)";
-by(arith_tac 1);
-
-Goal "((#0::real) <= x - y) = (y <= x)";
-by(arith_tac 1);
-
-Goal "(x + y) - x = (y::real)";
-by(arith_tac 1);
-
-Goal "(-x = y) = (x = (-y::real))";
-by(arith_tac 1);
-
-Goal "x < (y::real) ==> ~(x = y)";
-by(arith_tac 1);
-
-Goal "(x <= x + y) = ((#0::real) <= y)";
-by(arith_tac 1);
-
-Goal "(y <= x + y) = ((#0::real) <= x)";
-by(arith_tac 1);
-
-Goal "(x < x + y) = ((#0::real) < y)";
-by(arith_tac 1);
-
-Goal "(y < x + y) = ((#0::real) < x)";
-by(arith_tac 1);
-
-Goal "(x - y) - x = (-y::real)";
-by(arith_tac 1);
-
-Goal "(x + y < z) = (x < z - (y::real))";
-by(arith_tac 1);
-
-Goal "(x - y < z) = (x < z + (y::real))";
-by(arith_tac 1);
-
-Goal "(x < y - z) = (x + z < (y::real))";
-by(arith_tac 1);
-
-Goal "(x <= y - z) = (x + z <= (y::real))";
-by(arith_tac 1);
-
-Goal "(x - y <= z) = (x <= z + (y::real))";
-by(arith_tac 1);
-
-Goal "(-x < -y) = (y < (x::real))";
-by(arith_tac 1);
-
-Goal "(-x <= -y) = (y <= (x::real))";
-by(arith_tac 1);
-
-Goal "(a + b) - (c + d) = (a - c) + (b - (d::real))";
-by(arith_tac 1);
-
-Goal "(#0::real) - x = -x";
-by(arith_tac 1);
-
-Goal "x - (#0::real) = x";
-by(arith_tac 1);
-
-Goal "w <= x & y < z ==> w + y < x + (z::real)";
-by(arith_tac 1);
-
-Goal "w < x & y <= z ==> w + y < x + (z::real)";
-by(arith_tac 1);
-
-Goal "(#0::real) <= x & #0 < y ==> #0 < x + (y::real)";
-by(arith_tac 1);
-
-Goal "(#0::real) < x & #0 <= y ==> #0 < x + y";
-by(arith_tac 1);
-
-Goal "-x - y = -(x + (y::real))";
-by(arith_tac 1);
-
-Goal "x - (-y) = x + (y::real)";
-by(arith_tac 1);
-
-Goal "-x - -y = y - (x::real)";
-by(arith_tac 1);
-
-Goal "(a - b) + (b - c) = a - (c::real)";
-by(arith_tac 1);
-
-Goal "(x = y - z) = (x + z = (y::real))";
-by(arith_tac 1);
-
-Goal "(x - y = z) = (x = z + (y::real))";
-by(arith_tac 1);
-
-Goal "x - (x - y) = (y::real)";
-by(arith_tac 1);
-
-Goal "x - (x + y) = -(y::real)";
-by(arith_tac 1);
-
-Goal "x = y ==> x <= (y::real)";
-by(arith_tac 1);
-
-Goal "(#0::real) < x ==> ~(x = #0)";
-by(arith_tac 1);
-
-Goal "(x + y) * (x - y) = (x * x) - (y * y)";
-
-Goal "(-x = -y) = (x = (y::real))";
-by(arith_tac 1);
-
-Goal "(-x < -y) = (y < (x::real))";
-by(arith_tac 1);
-
-Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
-by (fast_arith_tac 1);
-
-Goal "!!a::real. [| a < b; c < d |] ==> a-d <= b+(-c)";
-by (fast_arith_tac 1);
-
-Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
-by (fast_arith_tac 1);
-
-Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] \
-\     ==> a+a <= j+j";
-by (fast_arith_tac 1);
-
-Goal "!!a::real. [| a+b < i+j; a<b; i<j |] \
-\     ==> a+a < j+j";
-by (fast_arith_tac 1);
-
-Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
-by (arith_tac 1);
-
-Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\     ==> a <= l";
-by (fast_arith_tac 1);
-
-Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\     ==> a+a+a+a <= l+l+l+l";
-by (fast_arith_tac 1);
-
-(* Too slow. Needs "combine_coefficients" simproc
-Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\     ==> a+a+a+a+a <= l+l+l+l+i";
-by (fast_arith_tac 1);
-
-Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
-by (fast_arith_tac 1);
-*)
-
diff -r ee0b835ca8fa -r 26384af93359 src/HOL/Real/RealBin.thy
--- a/src/HOL/Real/RealBin.thy	Thu Sep 23 14:39:39 1999 +0200
+++ b/src/HOL/Real/RealBin.thy	Thu Sep 23 18:39:05 1999 +0200
@@ -8,7 +8,7 @@
 This case is reduced to that for the integers
 *)
 
-RealBin = RealInt + Bin + RealPow +
+RealBin = RealInt + Bin + 
 
 instance
   real :: number 
diff -r ee0b835ca8fa -r 26384af93359 src/HOL/Real/RealOrd.thy
--- a/src/HOL/Real/RealOrd.thy	Thu Sep 23 14:39:39 1999 +0200
+++ b/src/HOL/Real/RealOrd.thy	Thu Sep 23 18:39:05 1999 +0200
@@ -11,4 +11,8 @@
 instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
 instance real :: linorder (real_le_linear)
 
+constdefs
+   rabs   :: real => real
+   "rabs r      == if 0r<=r then r else -r" 
+
 end
diff -r ee0b835ca8fa -r 26384af93359 src/HOL/Real/RealPow.ML
--- a/src/HOL/Real/RealPow.ML	Thu Sep 23 14:39:39 1999 +0200
+++ b/src/HOL/Real/RealPow.ML	Thu Sep 23 18:39:05 1999 +0200
@@ -94,6 +94,12 @@
 qed "realpow_eq_one";
 Addsimps [realpow_eq_one];
 
+(** New versions using #0 and #1 instead of 0r and 1r
+    REMOVE AFTER CONVERTING THIS FILE TO USE #0 AND #1 **)
+
+Addsimps (map (rename_numerals thy) [realpow_zero, realpow_eq_one]);
+
+
 Goal "rabs(-(1r ^ n)) = 1r";
 by (simp_tac (simpset() addsimps 
     [rabs_minus_cancel,rabs_one]) 1);
@@ -137,21 +143,13 @@
 by (auto_tac (claset() addIs [real_less_trans],simpset()));
 qed "realpow_two_gt_one";
 
-Goal "1r <= r ==> 1r <= r ^ 2";
-by (etac (real_le_imp_less_or_eq RS disjE) 1);
-by (etac (realpow_two_gt_one RS real_less_imp_le) 1);
-by (asm_simp_tac (simpset()) 1);
-qed "realpow_two_ge_one";
-
-(* more general result *)
 Goal "1r < r --> 1r <= r ^ n";
 by (induct_tac "n" 1);
 by (auto_tac (claset() addSDs [real_le_imp_less_or_eq],
-    simpset()));
+	      simpset()));
 by (dtac (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]));
+	      simpset() addsimps [real_zero_less_one]));
 qed_spec_mp "realpow_ge_one";
 
 Goal "1r < r ==> 1r < r ^ (Suc n)";
@@ -166,8 +164,7 @@
 
 Goal "1r <= r ==> 1r <= r ^ n";
 by (dtac real_le_imp_less_or_eq 1); 
-by (auto_tac (claset() addDs [realpow_ge_one],
-    simpset()));
+by (auto_tac (claset() addDs [realpow_ge_one], simpset()));
 qed "realpow_ge_one2";
 
 Goal "0r < r ==> 0r < r ^ Suc n";
@@ -181,24 +178,23 @@
 Goal "0r <= r ==> 0r <= r ^ Suc n";
 by (etac (real_le_imp_less_or_eq RS disjE) 1);
 by (etac (realpow_ge_zero) 1);
-by (asm_simp_tac (simpset()) 1);
+by (Asm_simp_tac 1);
 qed "realpow_Suc_ge_zero";
 
-Goal "1r <= (1r +1r) ^ n";
-by (res_inst_tac [("j","1r ^ n")] real_le_trans 1);
+Goal "(#1::real) <= #2 ^ n";
+by (res_inst_tac [("j","#1 ^ n")] real_le_trans 1);
 by (rtac realpow_le 2);
 by (auto_tac (claset() addIs [real_less_imp_le],
-    simpset() addsimps [real_zero_less_one,
-    real_one_less_two]));
+	      simpset() addsimps [zero_eq_numeral_0]));
 qed "two_realpow_ge_one";
 
-Goal "real_of_nat n < (1r + 1r) ^ n";
+Goal "real_of_nat n < #2 ^ n";
 by (induct_tac "n" 1);
 by (auto_tac (claset(),
-	      simpset() addsimps [real_of_nat_Suc, real_of_nat_zero,
-				  real_zero_less_one,real_add_mult_distrib,
-				  real_of_nat_one]));
-by (blast_tac (claset() addSIs [real_add_less_le_mono, two_realpow_ge_one]) 1);
+	      simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1,
+				  real_mult_2,
+				  real_of_nat_Suc, real_of_nat_zero,
+				  real_add_less_le_mono, two_realpow_ge_one]));
 qed "two_realpow_gt";
 Addsimps [two_realpow_gt,two_realpow_ge_one];
 
@@ -371,3 +367,11 @@
 qed "realpow_two_mult_rinv";
 Addsimps [realpow_two_mult_rinv];
 
+
+(** New versions using #0 and #1 instead of 0r and 1r
+    REMOVE AFTER CONVERTING THIS FILE TO USE #0 AND #1 **)
+
+Addsimps (map (rename_numerals thy) 
+	  [realpow_two_le, realpow_zero_le,
+	   rabs_minus_realpow_one, rabs_realpow_minus_one,
+	   realpow_minus_one, realpow_minus_one2, realpow_minus_one_odd]);
diff -r ee0b835ca8fa -r 26384af93359 src/HOL/Real/ex/BinEx.ML
--- a/src/HOL/Real/ex/BinEx.ML	Thu Sep 23 14:39:39 1999 +0200
+++ b/src/HOL/Real/ex/BinEx.ML	Thu Sep 23 18:39:05 1999 +0200
@@ -67,3 +67,291 @@
 Goal "(#1234567::real) <= #1234567";  
 by (Simp_tac 1); 
 qed "";
+
+(** Tests **)
+Goal "(x + y = x) = (y = (#0::real))";
+by(arith_tac 1);
+
+Goal "(x + y = y) = (x = (#0::real))";
+by(arith_tac 1);
+
+Goal "(x + y = (#0::real)) = (x = -y)";
+by(arith_tac 1);
+
+Goal "(x + y = (#0::real)) = (y = -x)";
+by(arith_tac 1);
+
+Goal "((x + y) < (x + z)) = (y < (z::real))";
+by(arith_tac 1);
+
+Goal "((x + z) < (y + z)) = (x < (y::real))";
+by(arith_tac 1);
+
+Goal "(~ x < y) = (y <= (x::real))";
+by(arith_tac 1);
+
+Goal "~(x < y & y < (x::real))";
+by(arith_tac 1);
+
+Goal "(x::real) < y ==> ~ y < x";
+by(arith_tac 1);
+
+Goal "((x::real) ~= y) = (x < y | y < x)";
+by(arith_tac 1);
+
+Goal "(~ x <= y) = (y < (x::real))";
+by(arith_tac 1);
+
+Goal "x <= y | y <= (x::real)";
+by(arith_tac 1);
+
+Goal "x <= y | y < (x::real)";
+by(arith_tac 1);
+
+Goal "x < y | y <= (x::real)";
+by(arith_tac 1);
+
+Goal "x <= (x::real)";
+by(arith_tac 1);
+
+Goal "((x::real) <= y) = (x < y | x = y)";
+by(arith_tac 1);
+
+Goal "((x::real) <= y & y <= x) = (x = y)";
+by(arith_tac 1);
+
+Goal "~(x < y & y <= (x::real))";
+by(arith_tac 1);
+
+Goal "~(x <= y & y < (x::real))";
+by(arith_tac 1);
+
+Goal "(-x < (#0::real)) = (#0 < x)";
+by(arith_tac 1);
+
+Goal "((#0::real) < -x) = (x < #0)";
+by(arith_tac 1);
+
+Goal "(-x <= (#0::real)) = (#0 <= x)";
+by(arith_tac 1);
+
+Goal "((#0::real) <= -x) = (x <= #0)";
+by(arith_tac 1);
+
+Goal "(x::real) = y | x < y | y < x";
+by(arith_tac 1);
+
+Goal "(x::real) = #0 | #0 < x | #0 < -x";
+by(arith_tac 1);
+
+Goal "(#0::real) <= x | #0 <= -x";
+by(arith_tac 1);
+
+Goal "((x::real) + y <= x + z) = (y <= z)";
+by(arith_tac 1);
+
+Goal "((x::real) + z <= y + z) = (x <= y)";
+by(arith_tac 1);
+
+Goal "(w::real) < x & y < z ==> w + y < x + z";
+by(arith_tac 1);
+
+Goal "(w::real) <= x & y <= z ==> w + y <= x + z";
+by(arith_tac 1);
+
+Goal "(#0::real) <= x & #0 <= y ==> #0 <= x + y";
+by(arith_tac 1);
+
+Goal "(#0::real) < x & #0 < y ==> #0 < x + y";
+by(arith_tac 1);
+
+Goal "(-x < y) = (#0 < x + (y::real))";
+by(arith_tac 1);
+
+Goal "(x < -y) = (x + y < (#0::real))";
+by(arith_tac 1);
+
+Goal "(y < x + -z) = (y + z < (x::real))";
+by(arith_tac 1);
+
+Goal "(x + -y < z) = (x < z + (y::real))";
+by(arith_tac 1);
+
+Goal "x <= y ==> x < y + (#1::real)";
+by(arith_tac 1);
+
+Goal "(x - y) + y = (x::real)";
+by(arith_tac 1);
+
+Goal "y + (x - y) = (x::real)";
+by(arith_tac 1);
+
+Goal "x - x = (#0::real)";
+by(arith_tac 1);
+
+Goal "(x - y = #0) = (x = (y::real))";
+by(arith_tac 1);
+
+Goal "((#0::real) <= x + x) = (#0 <= x)";
+by(arith_tac 1);
+
+Goal "(-x <= x) = ((#0::real) <= x)";
+by(arith_tac 1);
+
+Goal "(x <= -x) = (x <= (#0::real))";
+by(arith_tac 1);
+
+Goal "(-x = (#0::real)) = (x = #0)";
+by(arith_tac 1);
+
+Goal "-(x - y) = y - (x::real)";
+by(arith_tac 1);
+
+Goal "((#0::real) < x - y) = (y < x)";
+by(arith_tac 1);
+
+Goal "((#0::real) <= x - y) = (y <= x)";
+by(arith_tac 1);
+
+Goal "(x + y) - x = (y::real)";
+by(arith_tac 1);
+
+Goal "(-x = y) = (x = (-y::real))";
+by(arith_tac 1);
+
+Goal "x < (y::real) ==> ~(x = y)";
+by(arith_tac 1);
+
+Goal "(x <= x + y) = ((#0::real) <= y)";
+by(arith_tac 1);
+
+Goal "(y <= x + y) = ((#0::real) <= x)";
+by(arith_tac 1);
+
+Goal "(x < x + y) = ((#0::real) < y)";
+by(arith_tac 1);
+
+Goal "(y < x + y) = ((#0::real) < x)";
+by(arith_tac 1);
+
+Goal "(x - y) - x = (-y::real)";
+by(arith_tac 1);
+
+Goal "(x + y < z) = (x < z - (y::real))";
+by(arith_tac 1);
+
+Goal "(x - y < z) = (x < z + (y::real))";
+by(arith_tac 1);
+
+Goal "(x < y - z) = (x + z < (y::real))";
+by(arith_tac 1);
+
+Goal "(x <= y - z) = (x + z <= (y::real))";
+by(arith_tac 1);
+
+Goal "(x - y <= z) = (x <= z + (y::real))";
+by(arith_tac 1);
+
+Goal "(-x < -y) = (y < (x::real))";
+by(arith_tac 1);
+
+Goal "(-x <= -y) = (y <= (x::real))";
+by(arith_tac 1);
+
+Goal "(a + b) - (c + d) = (a - c) + (b - (d::real))";
+by(arith_tac 1);
+
+Goal "(#0::real) - x = -x";
+by(arith_tac 1);
+
+Goal "x - (#0::real) = x";
+by(arith_tac 1);
+
+Goal "w <= x & y < z ==> w + y < x + (z::real)";
+by(arith_tac 1);
+
+Goal "w < x & y <= z ==> w + y < x + (z::real)";
+by(arith_tac 1);
+
+Goal "(#0::real) <= x & #0 < y ==> #0 < x + (y::real)";
+by(arith_tac 1);
+
+Goal "(#0::real) < x & #0 <= y ==> #0 < x + y";
+by(arith_tac 1);
+
+Goal "-x - y = -(x + (y::real))";
+by(arith_tac 1);
+
+Goal "x - (-y) = x + (y::real)";
+by(arith_tac 1);
+
+Goal "-x - -y = y - (x::real)";
+by(arith_tac 1);
+
+Goal "(a - b) + (b - c) = a - (c::real)";
+by(arith_tac 1);
+
+Goal "(x = y - z) = (x + z = (y::real))";
+by(arith_tac 1);
+
+Goal "(x - y = z) = (x = z + (y::real))";
+by(arith_tac 1);
+
+Goal "x - (x - y) = (y::real)";
+by(arith_tac 1);
+
+Goal "x - (x + y) = -(y::real)";
+by(arith_tac 1);
+
+Goal "x = y ==> x <= (y::real)";
+by(arith_tac 1);
+
+Goal "(#0::real) < x ==> ~(x = #0)";
+by(arith_tac 1);
+
+Goal "(x + y) * (x - y) = (x * x) - (y * y)";
+
+Goal "(-x = -y) = (x = (y::real))";
+by(arith_tac 1);
+
+Goal "(-x < -y) = (y < (x::real))";
+by(arith_tac 1);
+
+Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
+by (fast_arith_tac 1);
+
+Goal "!!a::real. [| a < b; c < d |] ==> a-d <= b+(-c)";
+by (fast_arith_tac 1);
+
+Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
+by (fast_arith_tac 1);
+
+Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] \
+\     ==> a+a <= j+j";
+by (fast_arith_tac 1);
+
+Goal "!!a::real. [| a+b < i+j; a<b; i<j |] \
+\     ==> a+a < j+j";
+by (fast_arith_tac 1);
+
+Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
+by (arith_tac 1);
+
+Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\     ==> a <= l";
+by (fast_arith_tac 1);
+
+Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\     ==> a+a+a+a <= l+l+l+l";
+by (fast_arith_tac 1);
+
+(* Too slow. Needs "combine_coefficients" simproc
+Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\     ==> a+a+a+a+a <= l+l+l+l+i";
+by (fast_arith_tac 1);
+
+Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
+by (fast_arith_tac 1);
+*)
+