--- a/src/HOL/Complex/Complex.ML Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Complex/Complex.ML Fri Nov 28 12:09:37 2003 +0100
@@ -594,7 +594,7 @@
qed "complex_of_real_minus";
Goal "complex_of_real(inverse x) = inverse(complex_of_real x)";
-by (real_div_undefined_case_tac "x=0" 1);
+by (case_tac "x=0" 1);
by (simp_tac (simpset() addsimps [DIVISION_BY_ZERO,COMPLEX_INVERSE_ZERO]) 1);
by (auto_tac (claset(),simpset() addsimps [complex_inverse,
complex_of_real_def,realpow_num_two,real_divide_def,
@@ -616,8 +616,8 @@
Goalw [complex_divide_def]
"complex_of_real x / complex_of_real y = complex_of_real(x/y)";
-by (real_div_undefined_case_tac "y=0" 1);
-by (simp_tac (simpset() addsimps [rename_numerals DIVISION_BY_ZERO,
+by (case_tac "y=0" 1);
+by (asm_simp_tac (simpset() addsimps [rename_numerals DIVISION_BY_ZERO,
COMPLEX_INVERSE_ZERO]) 1);
by (asm_simp_tac (simpset() addsimps [complex_of_real_mult RS sym,
complex_of_real_inverse,real_divide_def]) 1);
@@ -1273,7 +1273,7 @@
Addsimps [complex_of_real_zero_iff];
Goal "y ~= 0 ==> cos (arg(ii * complex_of_real y)) = 0";
-by (cut_inst_tac [("R1.0","y"),("R2.0","0")] real_linear 1);
+by (cut_inst_tac [("x","y"),("y","0")] linorder_less_linear 1);
by Auto_tac;
qed "cos_arg_i_mult_zero3";
Addsimps [cos_arg_i_mult_zero3];
@@ -1475,8 +1475,8 @@
Addsimps [cis_inverse];
Goal "inverse(rcis r a) = rcis (1/r) (-a)";
-by (real_div_undefined_case_tac "r=0" 1);
-by (simp_tac (simpset() addsimps [rename_numerals DIVISION_BY_ZERO,
+by (case_tac "r=0" 1);
+by (asm_simp_tac (simpset() addsimps [rename_numerals DIVISION_BY_ZERO,
COMPLEX_INVERSE_ZERO]) 1);
by (auto_tac (claset(),simpset() addsimps [complex_inverse_complex_split,
complex_add_mult_distrib2,complex_of_real_mult,rcis_def,cis_def,
@@ -1491,8 +1491,8 @@
Goalw [complex_divide_def]
"rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)";
-by (real_div_undefined_case_tac "r2=0" 1);
-by (simp_tac (simpset() addsimps [rename_numerals DIVISION_BY_ZERO,
+by (case_tac "r2=0" 1);
+by (asm_simp_tac (simpset() addsimps [rename_numerals DIVISION_BY_ZERO,
COMPLEX_INVERSE_ZERO]) 1);
by (auto_tac (claset(),simpset() addsimps [rcis_inverse,rcis_mult,
real_diff_def]));
@@ -1578,7 +1578,7 @@
\ ==> arg(complex_of_real r * \
\ (complex_of_real(cos a) + ii * complex_of_real(sin a))) = a";
by Auto_tac;
-by (cut_inst_tac [("R1.0","0"),("R2.0","r")] real_linear 1);
+by (cut_inst_tac [("x","0"),("y","r")] linorder_less_linear 1);
by (auto_tac (claset(),simpset() addsimps (map (full_rename_numerals thy)
[rabs_eqI2,rabs_minus_eqI2,real_minus_rinv]) @ [real_divide_def,
real_minus_mult_eq2 RS sym] @ real_mult_ac));
--- a/src/HOL/Hyperreal/HRealAbs.thy Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Hyperreal/HRealAbs.thy Fri Nov 28 12:09:37 2003 +0100
@@ -4,7 +4,7 @@
Description : Absolute value function for the hyperreals
*)
-HRealAbs = HyperArith + RealAbs +
+HRealAbs = HyperArith + RealArith +
defs
hrabs_def "abs r == if (0::hypreal) <=r then r else -r"
--- a/src/HOL/Hyperreal/Lim.ML Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Hyperreal/Lim.ML Fri Nov 28 12:09:37 2003 +0100
@@ -1661,7 +1661,7 @@
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (dres_inst_tac [("x","s")] spec 1);
by (Clarify_tac 1);
-by (cut_inst_tac [("R1.0","f x"),("R2.0","y")] real_linear 1);
+by (cut_inst_tac [("x","f x"),("y","y")] linorder_less_linear 1);
by Safe_tac;
by (dres_inst_tac [("x","ba - x")] spec 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [abs_iff])));
--- a/src/HOL/Hyperreal/Lim.thy Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Hyperreal/Lim.thy Fri Nov 28 12:09:37 2003 +0100
@@ -5,7 +5,7 @@
differentiation of real=>real functions
*)
-Lim = SEQ + RealAbs +
+Lim = SEQ + RealArith +
(*-----------------------------------------------------------------------
Limits, continuity and differentiation: standard and NS definitions
--- a/src/HOL/Hyperreal/MacLaurin.ML Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Hyperreal/MacLaurin.ML Fri Nov 28 12:09:37 2003 +0100
@@ -317,7 +317,7 @@
by (induct_tac "n" 1);
by (Simp_tac 1);
by Auto_tac;
-by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
+by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);
by Auto_tac;
by (cut_inst_tac [("f","diff 0"),
("diff","diff"),
--- a/src/HOL/Hyperreal/NthRoot.ML Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Hyperreal/NthRoot.ML Fri Nov 28 12:09:37 2003 +0100
@@ -160,7 +160,7 @@
(* uniqueness of nth positive root *)
Goal "[| (0::real) < a; 0 < n |] ==> EX! r. 0 < r & r ^ n = a";
by (auto_tac (claset() addSIs [realpow_pos_nth],simpset()));
-by (cut_inst_tac [("R1.0","r"),("R2.0","y")] real_linear 1);
+by (cut_inst_tac [("x","r"),("y","y")] linorder_less_linear 1);
by (Auto_tac);
by (dres_inst_tac [("x","r")] realpow_less 1);
by (dres_inst_tac [("x","y")] realpow_less 4);
--- a/src/HOL/Hyperreal/SEQ.ML Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML Fri Nov 28 12:09:37 2003 +0100
@@ -859,8 +859,8 @@
by (res_inst_tac [("x","0")] exI 1);
by (Asm_full_simp_tac 1);
by (Step_tac 1);
-by (cut_inst_tac [("R1.0","abs (X (Suc n))"),("R2.0","abs(X m)")]
- real_linear 1);
+by (cut_inst_tac [("x","abs (X (Suc n))"),("y","abs(X m)")]
+ linorder_less_linear 1);
by (Step_tac 1);
by (res_inst_tac [("x","m")] exI 1);
by (res_inst_tac [("x","m")] exI 2);
@@ -919,8 +919,8 @@
by (dtac lemmaCauchy 1);
by (cut_inst_tac [("M","M"),("X","X")] SUP_rabs_subseq 1);
by (Step_tac 1);
-by (cut_inst_tac [("R1.0","abs(X m)"),
- ("R2.0","1 + abs(X M)")] real_linear 1);
+by (cut_inst_tac [("x","abs(X m)"),
+ ("y","1 + abs(X M)")] linorder_less_linear 1);
by (Step_tac 1);
by (dtac lemma_trans1 1 THEN assume_tac 1);
by (dtac lemma_trans2 3 THEN assume_tac 3);
--- a/src/HOL/Hyperreal/Transcendental.ML Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML Fri Nov 28 12:09:37 2003 +0100
@@ -146,7 +146,7 @@
Goal "(~ (0::real) < x*x) = (x = 0)";
by Auto_tac;
by (rtac ccontr 1);
-by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
+by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);
by Auto_tac;
by (ftac (real_mult_order) 2);
by (asm_full_simp_tac (simpset() addsimps [real_0_less_mult_iff]) 1);
@@ -1675,7 +1675,7 @@
by (subgoal_tac "EX x. 0 <= x & x <= 2 & cos x = 0" 1);
by (rtac IVT2 2);
by (auto_tac (claset() addIs [DERIV_isCont,DERIV_cos],simpset ()));
-by (cut_inst_tac [("R1.0","xa"),("R2.0","y")] real_linear 1);
+by (cut_inst_tac [("x","xa"),("y","y")] linorder_less_linear 1);
by (rtac ccontr 1);
by (subgoal_tac "(ALL x. cos differentiable x) & \
\ (ALL x. isCont cos x)" 1);
@@ -1898,7 +1898,7 @@
by (rtac IVT2 2);
by (auto_tac (claset() addIs [order_less_imp_le,DERIV_isCont,DERIV_cos],
simpset ()));
-by (cut_inst_tac [("R1.0","xa"),("R2.0","y")] real_linear 1);
+by (cut_inst_tac [("x","xa"),("y","y")] linorder_less_linear 1);
by (rtac ccontr 1 THEN Auto_tac);
by (dres_inst_tac [("f","cos")] Rolle 1);
by (dres_inst_tac [("f","cos")] Rolle 5);
@@ -2171,7 +2171,7 @@
Goal "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y";
by (cut_inst_tac [("y","y")] lemma_tan_total1 1);
by (Auto_tac);
-by (cut_inst_tac [("R1.0","xa"),("R2.0","y")] real_linear 1);
+by (cut_inst_tac [("x","xa"),("y","y")] linorder_less_linear 1);
by (Auto_tac);
by (subgoal_tac "EX z. xa < z & z < y & DERIV tan z :> 0" 1);
by (subgoal_tac "EX z. y < z & z < xa & DERIV tan z :> 0" 3);
@@ -2628,7 +2628,7 @@
Addsimps [real_sqrt_sos_eq_one_iff];
Goalw [real_divide_def] "(((r::real) * a) / (r * r)) = a / r";
-by (real_div_undefined_case_tac "r=0" 1);
+by (case_tac "r=0" 1);
by (auto_tac (claset(),simpset() addsimps [real_inverse_distrib] @ real_mult_ac));
qed "real_divide_square_eq";
Addsimps [real_divide_square_eq];
@@ -2675,7 +2675,7 @@
qed "real_sqrt_sum_squares_gt_zero2";
Goal "x ~= 0 ==> 0 < sqrt(x ^ 2 + y ^ 2)";
-by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
+by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);
by (auto_tac (claset() addIs [real_sqrt_sum_squares_gt_zero2,
real_sqrt_sum_squares_gt_zero1],simpset() addsimps [realpow_num_two]));
qed "real_sqrt_sum_squares_gt_zero3";
@@ -2741,7 +2741,7 @@
(* was qed "lemma_real_mult_self_rinv_sqrt_squared5" *)
Goal "-(1::real)<= x / sqrt (x * x + y * y)";
-by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
+by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);
by (Step_tac 1);
by (rtac lemma_real_divide_sqrt_ge_minus_one2 1);
by (rtac lemma_real_divide_sqrt_ge_minus_one 3);
@@ -2757,7 +2757,7 @@
simplify (simpset()) cos_x_y_ge_minus_one1a];
Goal "x / sqrt (x * x + y * y) <= 1";
-by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
+by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);
by (Step_tac 1);
by (rtac lemma_real_divide_sqrt_le_one 1);
by (rtac lemma_real_divide_sqrt_le_one2 3);
@@ -2778,7 +2778,7 @@
Addsimps [[cos_x_y_ge_minus_one1a,cos_x_y_le_one2] MRS arcos_bounded];
Goal "-(1::real) <= abs(x) / sqrt (x * x + y * y)";
-by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
+by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);
by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2,abs_eqI2]));
by (dtac lemma_real_divide_sqrt_ge_minus_one 1 THEN Force_tac 1);
qed "cos_rabs_x_y_ge_minus_one";
@@ -2787,7 +2787,7 @@
simplify (simpset()) cos_rabs_x_y_ge_minus_one];
Goal "abs(x) / sqrt (x * x + y * y) <= 1";
-by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
+by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);
by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2,abs_eqI2]));
by (dtac lemma_real_divide_sqrt_ge_minus_one2 1 THEN Force_tac 1);
qed "cos_rabs_x_y_le_one";
@@ -2952,7 +2952,7 @@
qed "real_sum_squares_cancel2a";
Goal "[| x ~= 0; y < 0 |] ==> EX r a. x = r * cos a & y = r * sin a";
-by (cut_inst_tac [("R1.0","0"),("R2.0","x")] real_linear 1);
+by (cut_inst_tac [("x","0"),("y","x")] linorder_less_linear 1);
by Auto_tac;
by (res_inst_tac [("x","sqrt(x ^ 2 + y ^ 2)")] exI 1);
by (res_inst_tac [("x","arcsin(y / sqrt (x * x + y * y))")] exI 1);
@@ -2982,7 +2982,7 @@
by Auto_tac;
by (res_inst_tac [("x","y")] exI 1);
by (res_inst_tac [("x","pi/2")] exI 1 THEN Auto_tac);
-by (cut_inst_tac [("R1.0","0"),("R2.0","y")] real_linear 1);
+by (cut_inst_tac [("x","0"),("y","y")] linorder_less_linear 1);
by Auto_tac;
by (res_inst_tac [("x","x")] exI 2);
by (res_inst_tac [("x","0")] exI 2 THEN Auto_tac);
@@ -3176,7 +3176,7 @@
Goal "[| f -- c --> l; l ~= 0 |] \
\ ==> EX r. 0 < r & (ALL x. x ~= c & abs (c - x) < r --> f x ~= 0)";
-by (cut_inst_tac [("R1.0","l"),("R2.0","0")] real_linear 1);
+by (cut_inst_tac [("x","l"),("y","0")] linorder_less_linear 1);
by Auto_tac;
by (dtac LIM_fun_less_zero 1);
by (dtac LIM_fun_gt_zero 3);
--- a/src/HOL/Integ/IntDef.thy Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Integ/IntDef.thy Fri Nov 28 12:09:37 2003 +0100
@@ -38,7 +38,7 @@
iszero :: "int => bool"
"iszero z == z = (0::int)"
-defs (*of overloaded constants*)
+defs (overloaded)
Zero_int_def: "0 == int 0"
One_int_def: "1 == int 1"
--- a/src/HOL/IsaMakefile Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/IsaMakefile Fri Nov 28 12:09:37 2003 +0100
@@ -141,10 +141,10 @@
Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \
Real/PRat.ML Real/PRat.thy \
Real/PReal.ML Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \
- Real/ROOT.ML Real/Real.thy Real/RealAbs.ML Real/RealAbs.thy \
+ Real/ROOT.ML Real/Real.thy \
Real/RealArith0.ML Real/RealArith0.thy Real/real_arith0.ML \
Real/RealArith.thy Real/real_arith.ML Real/RealBin.ML \
- Real/RealBin.thy Real/RealDef.ML Real/RealDef.thy Real/RealInt.ML \
+ Real/RealBin.thy Real/RealDef.thy \
Real/RealInt.thy Real/RealOrd.thy \
Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \
--- a/src/HOL/Real/RealAbs.ML Thu Nov 27 10:47:55 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,264 +0,0 @@
-(* Title : RealAbs.ML
- ID : $Id$
- Author : Jacques D. Fleuriot
- Copyright : 1998 University of Cambridge
- Description : Absolute value function for the reals
-*)
-
-
-(** abs (absolute value) **)
-
-Goalw [real_abs_def]
- "abs (number_of v :: real) = \
-\ (if neg (number_of v) then number_of (bin_minus v) \
-\ else number_of v)";
-by (simp_tac
- (simpset () addsimps
- bin_arith_simps@
- [minus_real_number_of, le_real_number_of_eq_not_less,
- less_real_number_of, real_of_int_le_iff]) 1);
-qed "abs_nat_number_of";
-
-Addsimps [abs_nat_number_of];
-
-Goalw [real_abs_def]
- "P(abs (x::real)) = ((0 <= x --> P x) & (x < 0 --> P(-x)))";
-by Auto_tac;
-qed "abs_split";
-
-
-(*----------------------------------------------------------------------------
- Properties of the absolute value function over the reals
- (adapted version of previously proved theorems about abs)
- ----------------------------------------------------------------------------*)
-
-Goalw [real_abs_def] "abs (r::real) = (if 0<=r then r else -r)";
-by Auto_tac;
-qed "abs_iff";
-
-Goalw [real_abs_def] "abs 0 = (0::real)";
-by Auto_tac;
-qed "abs_zero";
-Addsimps [abs_zero];
-
-Goalw [real_abs_def] "abs (1::real) = 1";
-by (Simp_tac 1);
-qed "abs_one";
-Addsimps [abs_one];
-
-Goalw [real_abs_def] "(0::real)<=x ==> abs x = x";
-by (Asm_simp_tac 1);
-qed "abs_eqI1";
-
-Goalw [real_abs_def] "(0::real) < x ==> abs x = x";
-by (Asm_simp_tac 1);
-qed "abs_eqI2";
-
-Goalw [real_abs_def,real_le_def] "x < (0::real) ==> abs x = -x";
-by (Asm_simp_tac 1);
-qed "abs_minus_eqI2";
-
-Goalw [real_abs_def] "x<=(0::real) ==> abs x = -x";
-by (Asm_simp_tac 1);
-qed "abs_minus_eqI1";
-
-Goalw [real_abs_def] "(0::real)<= abs x";
-by (Simp_tac 1);
-qed "abs_ge_zero";
-Addsimps [abs_ge_zero];
-
-Goalw [real_abs_def] "abs(abs x)=abs (x::real)";
-by (Simp_tac 1);
-qed "abs_idempotent";
-Addsimps [abs_idempotent];
-
-Goalw [real_abs_def] "(abs x = 0) = (x=(0::real))";
-by (Full_simp_tac 1);
-qed "abs_zero_iff";
-AddIffs [abs_zero_iff];
-
-Goalw [real_abs_def] "x<=abs (x::real)";
-by (Simp_tac 1);
-qed "abs_ge_self";
-
-Goalw [real_abs_def] "-x<=abs (x::real)";
-by (Simp_tac 1);
-qed "abs_ge_minus_self";
-
-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 [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,
- INVERSE_ZERO, real_inverse_gt_0]));
-qed "abs_inverse";
-
-Goal "abs (x * inverse y) = (abs x) * inverse (abs (y::real))";
-by (asm_simp_tac (simpset() addsimps [abs_mult, abs_inverse]) 1);
-qed "abs_mult_inverse";
-
-Goalw [real_abs_def] "abs(x+y) <= abs x + abs (y::real)";
-by (Simp_tac 1);
-qed "abs_triangle_ineq";
-
-(*Unused, but perhaps interesting as an example*)
-Goal "abs(w + x + y + z) <= abs(w) + abs(x) + abs(y) + abs(z::real)";
-by (simp_tac (simpset() addsimps [abs_triangle_ineq RS order_trans]) 1);
-qed "abs_triangle_ineq_four";
-
-Goalw [real_abs_def] "abs(-x)=abs(x::real)";
-by (Simp_tac 1);
-qed "abs_minus_cancel";
-Addsimps [abs_minus_cancel];
-
-Goalw [real_abs_def] "abs(x + (-y)) = abs (y + (-(x::real)))";
-by (Simp_tac 1);
-qed "abs_minus_add_cancel";
-
-Goalw [real_abs_def] "abs(x + (-y)) <= abs x + abs (y::real)";
-by (Simp_tac 1);
-qed "abs_triangle_minus_ineq";
-
-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 [real_abs_def] "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)";
-by (Simp_tac 1);
-qed "abs_add_minus_less";
-
-(* lemmas manipulating terms *)
-Goal "((0::real)*x < r)=(0 < r)";
-by (Simp_tac 1);
-qed "real_mult_0_less";
-
-Goal "[| (0::real) < y; x < r; y*r < t*s |] ==> y*x < t*s";
-by (blast_tac (claset() addSIs [real_mult_less_mono2]
- addIs [order_less_trans]) 1);
-qed "real_mult_less_trans";
-
-Goal "[| (0::real)<=y; x < r; y*r < t*s; 0 < t*s|] ==> y*x < t*s";
-by (dtac order_le_imp_less_or_eq 1);
-by (fast_tac (HOL_cs addEs [real_mult_0_less RS iffD2,
- real_mult_less_trans]) 1);
-qed "real_mult_le_less_trans";
-
-Goal "[| abs x < r; abs y < s |] ==> abs(x*y) < r*(s::real)";
-by (simp_tac (simpset() addsimps [abs_mult]) 1);
-by (rtac real_mult_le_less_trans 1);
-by (rtac abs_ge_zero 1);
-by (assume_tac 1);
-by (rtac real_mult_order 2);
-by (auto_tac (claset() addSIs [real_mult_less_mono1, abs_ge_zero]
- addIs [order_le_less_trans],
- simpset()));
-qed "abs_mult_less";
-
-Goal "[| abs x < r; abs y < s |] ==> abs(x)*abs(y) < r*(s::real)";
-by (auto_tac (claset() addIs [abs_mult_less],
- simpset() addsimps [abs_mult RS sym]));
-qed "abs_mult_less2";
-
-Goal "abs(x) < r ==> (0::real) < r";
-by (blast_tac (claset() addSIs [order_le_less_trans,abs_ge_zero]) 1);
-qed "abs_less_gt_zero";
-
-Goalw [real_abs_def] "abs (-1) = (1::real)";
-by (Simp_tac 1);
-qed "abs_minus_one";
-Addsimps [abs_minus_one];
-
-Goalw [real_abs_def] "abs x =x | abs x = -(x::real)";
-by Auto_tac;
-qed "abs_disj";
-
-Goalw [real_abs_def] "(abs x < r) = (-r < x & x < (r::real))";
-by Auto_tac;
-qed "abs_interval_iff";
-
-Goalw [real_abs_def] "(abs x <= r) = (-r<=x & x<=(r::real))";
-by Auto_tac;
-qed "abs_le_interval_iff";
-
-Goalw [real_abs_def] "(0::real) < k ==> 0 < k + abs(x)";
-by Auto_tac;
-qed "abs_add_pos_gt_zero";
-
-Goalw [real_abs_def] "(0::real) < 1 + abs(x)";
-by Auto_tac;
-qed "abs_add_one_gt_zero";
-Addsimps [abs_add_one_gt_zero];
-
-Goalw [real_abs_def] "~ abs x < (0::real)";
-by Auto_tac;
-qed "abs_not_less_zero";
-Addsimps [abs_not_less_zero];
-
-Goal "abs h < abs y - abs x ==> abs (x + h) < abs (y::real)";
-by (auto_tac (claset() addIs [abs_triangle_ineq RS order_le_less_trans],
- simpset()));
-qed "abs_circle";
-
-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 [real_abs_def]) 1);
-by (arith_tac 1);
-qed "real_0_less_abs_iff";
-Addsimps [real_0_less_abs_iff];
-
-Goal "abs (real x) = real (x::nat)";
-by (auto_tac (claset() addIs [abs_eqI1],
- simpset() addsimps [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 order_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 order_trans,
- real_add_left_le_mono1],
- simpset() addsimps [real_add_assoc]));
-qed "abs_triangle_ineq_three";
-
-Goalw [real_abs_def] "abs(x - y) < y ==> (0::real) < y";
-by (case_tac "0 <= x - y" 1);
-by Auto_tac;
-qed "abs_diff_less_imp_gt_zero";
-
-Goalw [real_abs_def] "abs(x - y) < x ==> (0::real) < x";
-by (case_tac "0 <= x - y" 1);
-by Auto_tac;
-qed "abs_diff_less_imp_gt_zero2";
-
-Goal "abs(x - y) < y ==> (0::real) < x";
-by (auto_tac (claset(),simpset() addsimps [abs_interval_iff]));
-qed "abs_diff_less_imp_gt_zero3";
-
-Goal "abs(x - y) < -y ==> x < (0::real)";
-by (auto_tac (claset(),simpset() addsimps [abs_interval_iff]));
-qed "abs_diff_less_imp_gt_zero4";
-
-Goalw [real_abs_def]
- "abs(x) <= abs(x + (-y)) + abs((y::real))";
-by Auto_tac;
-qed "abs_triangle_ineq_minus_cancel";
-
-Goal "abs ((x::real) + y + (-l + -m)) <= abs(x + -l) + abs(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 abs_triangle_ineq 1);
-qed "abs_sum_triangle_ineq";
--- a/src/HOL/Real/RealAbs.thy Thu Nov 27 10:47:55 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(* Title : RealAbs.thy
- ID : $Id$
- Author : Jacques D. Fleuriot
- Copyright : 1998 University of Cambridge
- Description : Absolute value function for the reals
-*)
-
-RealAbs = RealArith
--- a/src/HOL/Real/RealArith.thy Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Real/RealArith.thy Fri Nov 28 12:09:37 2003 +0100
@@ -3,4 +3,265 @@
setup real_arith_setup
+subsection{*Absolute Value Function for the Reals*}
+
+(** abs (absolute value) **)
+
+lemma abs_nat_number_of:
+ "abs (number_of v :: real) =
+ (if neg (number_of v) then number_of (bin_minus v)
+ else number_of v)"
+apply (simp add: real_abs_def bin_arith_simps minus_real_number_of le_real_number_of_eq_not_less less_real_number_of real_of_int_le_iff)
+done
+
+declare abs_nat_number_of [simp]
+
+lemma abs_split [arith_split]:
+ "P(abs (x::real)) = ((0 <= x --> P x) & (x < 0 --> P(-x)))"
+apply (unfold real_abs_def, auto)
+done
+
+
+(*----------------------------------------------------------------------------
+ Properties of the absolute value function over the reals
+ (adapted version of previously proved theorems about abs)
+ ----------------------------------------------------------------------------*)
+
+lemma abs_iff: "abs (r::real) = (if 0<=r then r else -r)"
+apply (unfold real_abs_def, auto)
+done
+
+lemma abs_zero: "abs 0 = (0::real)"
+by (unfold real_abs_def, auto)
+declare abs_zero [simp]
+
+lemma abs_one: "abs (1::real) = 1"
+by (unfold real_abs_def, simp)
+declare abs_one [simp]
+
+lemma abs_eqI1: "(0::real)<=x ==> abs x = x"
+by (unfold real_abs_def, simp)
+
+lemma abs_eqI2: "(0::real) < x ==> abs x = x"
+by (unfold real_abs_def, simp)
+
+lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x"
+by (unfold real_abs_def real_le_def, simp)
+
+lemma abs_minus_eqI1: "x<=(0::real) ==> abs x = -x"
+by (unfold real_abs_def, simp)
+
+lemma abs_ge_zero: "(0::real)<= abs x"
+by (unfold real_abs_def, simp)
+declare abs_ge_zero [simp]
+
+lemma abs_idempotent: "abs(abs x)=abs (x::real)"
+by (unfold real_abs_def, simp)
+declare abs_idempotent [simp]
+
+lemma abs_zero_iff: "(abs x = 0) = (x=(0::real))"
+by (unfold real_abs_def, simp)
+declare abs_zero_iff [iff]
+
+lemma abs_ge_self: "x<=abs (x::real)"
+by (unfold real_abs_def, simp)
+
+lemma abs_ge_minus_self: "-x<=abs (x::real)"
+by (unfold real_abs_def, simp)
+
+lemma abs_mult: "abs (x * y) = abs x * abs (y::real)"
+apply (unfold real_abs_def)
+apply (auto dest!: order_antisym simp add: real_0_le_mult_iff)
+done
+
+lemma abs_inverse: "abs(inverse(x::real)) = inverse(abs(x))"
+apply (unfold real_abs_def)
+apply (case_tac "x=0")
+apply (auto simp add: real_minus_inverse real_le_less INVERSE_ZERO real_inverse_gt_0)
+done
+
+lemma abs_mult_inverse: "abs (x * inverse y) = (abs x) * inverse (abs (y::real))"
+by (simp add: abs_mult abs_inverse)
+
+lemma abs_triangle_ineq: "abs(x+y) <= abs x + abs (y::real)"
+by (unfold real_abs_def, simp)
+
+(*Unused, but perhaps interesting as an example*)
+lemma abs_triangle_ineq_four: "abs(w + x + y + z) <= abs(w) + abs(x) + abs(y) + abs(z::real)"
+by (simp add: abs_triangle_ineq [THEN order_trans])
+
+lemma abs_minus_cancel: "abs(-x)=abs(x::real)"
+by (unfold real_abs_def, simp)
+declare abs_minus_cancel [simp]
+
+lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
+by (unfold real_abs_def, simp)
+
+lemma abs_triangle_minus_ineq: "abs(x + (-y)) <= abs x + abs (y::real)"
+by (unfold real_abs_def, simp)
+
+lemma abs_add_less [rule_format (no_asm)]: "abs x < r --> abs y < s --> abs(x+y) < r+(s::real)"
+by (unfold real_abs_def, simp)
+
+lemma abs_add_minus_less: "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)"
+by (unfold real_abs_def, simp)
+
+(* lemmas manipulating terms *)
+lemma real_mult_0_less: "((0::real)*x < r)=(0 < r)"
+by simp
+
+lemma real_mult_less_trans: "[| (0::real) < y; x < r; y*r < t*s |] ==> y*x < t*s"
+by (blast intro!: real_mult_less_mono2 intro: order_less_trans)
+
+(*USED ONLY IN NEXT THM*)
+lemma real_mult_le_less_trans:
+ "[| (0::real)<=y; x < r; y*r < t*s; 0 < t*s|] ==> y*x < t*s"
+apply (drule order_le_imp_less_or_eq)
+apply (fast elim: real_mult_0_less [THEN iffD2] real_mult_less_trans)
+done
+
+lemma abs_mult_less: "[| abs x < r; abs y < s |] ==> abs(x*y) < r*(s::real)"
+apply (simp add: abs_mult)
+apply (rule real_mult_le_less_trans)
+apply (rule abs_ge_zero, assumption)
+apply (rule_tac [2] real_mult_order)
+apply (auto intro!: real_mult_less_mono1 abs_ge_zero intro: order_le_less_trans)
+done
+
+lemma abs_mult_less2: "[| abs x < r; abs y < s |] ==> abs(x)*abs(y) < r*(s::real)"
+by (auto intro: abs_mult_less simp add: abs_mult [symmetric])
+
+lemma abs_less_gt_zero: "abs(x) < r ==> (0::real) < r"
+by (blast intro!: order_le_less_trans abs_ge_zero)
+
+lemma abs_minus_one: "abs (-1) = (1::real)"
+by (unfold real_abs_def, simp)
+declare abs_minus_one [simp]
+
+lemma abs_disj: "abs x =x | abs x = -(x::real)"
+by (unfold real_abs_def, auto)
+
+lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))"
+by (unfold real_abs_def, auto)
+
+lemma abs_le_interval_iff: "(abs x <= r) = (-r<=x & x<=(r::real))"
+by (unfold real_abs_def, auto)
+
+lemma abs_add_pos_gt_zero: "(0::real) < k ==> 0 < k + abs(x)"
+by (unfold real_abs_def, auto)
+
+lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)"
+by (unfold real_abs_def, auto)
+declare abs_add_one_gt_zero [simp]
+
+lemma abs_not_less_zero: "~ abs x < (0::real)"
+by (unfold real_abs_def, auto)
+declare abs_not_less_zero [simp]
+
+lemma abs_circle: "abs h < abs y - abs x ==> abs (x + h) < abs (y::real)"
+by (auto intro: abs_triangle_ineq [THEN order_le_less_trans])
+
+lemma abs_le_zero_iff: "(abs x <= (0::real)) = (x = 0)"
+by (unfold real_abs_def, auto)
+declare abs_le_zero_iff [simp]
+
+lemma real_0_less_abs_iff: "((0::real) < abs x) = (x ~= 0)"
+by (simp add: real_abs_def, arith)
+declare real_0_less_abs_iff [simp]
+
+lemma abs_real_of_nat_cancel: "abs (real x) = real (x::nat)"
+by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero)
+declare abs_real_of_nat_cancel [simp]
+
+lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x"
+apply (rule real_leD)
+apply (auto intro: abs_ge_self [THEN order_trans])
+done
+declare abs_add_one_not_less_self [simp]
+
+(* used in vector theory *)
+lemma abs_triangle_ineq_three: "abs(w + x + (y::real)) <= abs(w) + abs(x) + abs(y)"
+by (auto intro!: abs_triangle_ineq [THEN order_trans] real_add_left_le_mono1 simp add: real_add_assoc)
+
+lemma abs_diff_less_imp_gt_zero: "abs(x - y) < y ==> (0::real) < y"
+apply (unfold real_abs_def)
+apply (case_tac "0 <= x - y", auto)
+done
+
+lemma abs_diff_less_imp_gt_zero2: "abs(x - y) < x ==> (0::real) < x"
+apply (unfold real_abs_def)
+apply (case_tac "0 <= x - y", auto)
+done
+
+lemma abs_diff_less_imp_gt_zero3: "abs(x - y) < y ==> (0::real) < x"
+by (auto simp add: abs_interval_iff)
+
+lemma abs_diff_less_imp_gt_zero4: "abs(x - y) < -y ==> x < (0::real)"
+by (auto simp add: abs_interval_iff)
+
+lemma abs_triangle_ineq_minus_cancel:
+ "abs(x) <= abs(x + (-y)) + abs((y::real))"
+apply (unfold real_abs_def, auto)
+done
+
+lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) <= abs(x + -l) + abs(y + -m)"
+apply (simp add: real_add_assoc)
+apply (rule_tac x1 = y in real_add_left_commute [THEN ssubst])
+apply (rule real_add_assoc [THEN subst])
+apply (rule abs_triangle_ineq)
+done
+
+ML
+{*
+val abs_nat_number_of = thm"abs_nat_number_of";
+val abs_split = thm"abs_split";
+val abs_iff = thm"abs_iff";
+val abs_zero = thm"abs_zero";
+val abs_one = thm"abs_one";
+val abs_eqI1 = thm"abs_eqI1";
+val abs_eqI2 = thm"abs_eqI2";
+val abs_minus_eqI2 = thm"abs_minus_eqI2";
+val abs_minus_eqI1 = thm"abs_minus_eqI1";
+val abs_ge_zero = thm"abs_ge_zero";
+val abs_idempotent = thm"abs_idempotent";
+val abs_zero_iff = thm"abs_zero_iff";
+val abs_ge_self = thm"abs_ge_self";
+val abs_ge_minus_self = thm"abs_ge_minus_self";
+val abs_mult = thm"abs_mult";
+val abs_inverse = thm"abs_inverse";
+val abs_mult_inverse = thm"abs_mult_inverse";
+val abs_triangle_ineq = thm"abs_triangle_ineq";
+val abs_triangle_ineq_four = thm"abs_triangle_ineq_four";
+val abs_minus_cancel = thm"abs_minus_cancel";
+val abs_minus_add_cancel = thm"abs_minus_add_cancel";
+val abs_triangle_minus_ineq = thm"abs_triangle_minus_ineq";
+val abs_add_less = thm"abs_add_less";
+val abs_add_minus_less = thm"abs_add_minus_less";
+val real_mult_0_less = thm"real_mult_0_less";
+val real_mult_less_trans = thm"real_mult_less_trans";
+val real_mult_le_less_trans = thm"real_mult_le_less_trans";
+val abs_mult_less = thm"abs_mult_less";
+val abs_mult_less2 = thm"abs_mult_less2";
+val abs_less_gt_zero = thm"abs_less_gt_zero";
+val abs_minus_one = thm"abs_minus_one";
+val abs_disj = thm"abs_disj";
+val abs_interval_iff = thm"abs_interval_iff";
+val abs_le_interval_iff = thm"abs_le_interval_iff";
+val abs_add_pos_gt_zero = thm"abs_add_pos_gt_zero";
+val abs_add_one_gt_zero = thm"abs_add_one_gt_zero";
+val abs_not_less_zero = thm"abs_not_less_zero";
+val abs_circle = thm"abs_circle";
+val abs_le_zero_iff = thm"abs_le_zero_iff";
+val real_0_less_abs_iff = thm"real_0_less_abs_iff";
+val abs_real_of_nat_cancel = thm"abs_real_of_nat_cancel";
+val abs_add_one_not_less_self = thm"abs_add_one_not_less_self";
+val abs_triangle_ineq_three = thm"abs_triangle_ineq_three";
+val abs_diff_less_imp_gt_zero = thm"abs_diff_less_imp_gt_zero";
+val abs_diff_less_imp_gt_zero2 = thm"abs_diff_less_imp_gt_zero2";
+val abs_diff_less_imp_gt_zero3 = thm"abs_diff_less_imp_gt_zero3";
+val abs_diff_less_imp_gt_zero4 = thm"abs_diff_less_imp_gt_zero4";
+val abs_triangle_ineq_minus_cancel = thm"abs_triangle_ineq_minus_cancel";
+val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq";
+*}
+
end
--- a/src/HOL/Real/RealDef.ML Thu Nov 27 10:47:55 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1130 +0,0 @@
-(* Title : Real/RealDef.ML
- ID : $Id$
- Author : Jacques D. Fleuriot
- Copyright : 1998 University of Cambridge
- Description : The reals
-*)
-
-(*** Proving that realrel is an equivalence relation ***)
-
-Goal "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \
-\ ==> x1 + y3 = x3 + y1";
-by (res_inst_tac [("C","y2")] preal_add_right_cancel 1);
-by (rotate_tac 1 1 THEN dtac sym 1);
-by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
-by (rtac (preal_add_left_commute RS subst) 1);
-by (res_inst_tac [("x1","x1")] (preal_add_assoc RS subst) 1);
-by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
-qed "preal_trans_lemma";
-
-(** Natural deduction for realrel **)
-
-Goalw [realrel_def]
- "(((x1,y1),(x2,y2)): realrel) = (x1 + y2 = x2 + y1)";
-by (Blast_tac 1);
-qed "realrel_iff";
-
-Goalw [realrel_def]
- "[| x1 + y2 = x2 + y1 |] ==> ((x1,y1),(x2,y2)): realrel";
-by (Blast_tac 1);
-qed "realrelI";
-
-Goalw [realrel_def]
- "p: realrel --> (EX x1 y1 x2 y2. \
-\ p = ((x1,y1),(x2,y2)) & x1 + y2 = x2 + y1)";
-by (Blast_tac 1);
-qed "realrelE_lemma";
-
-val [major,minor] = Goal
- "[| p: realrel; \
-\ !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2)); x1+y2 = x2+y1 \
-\ |] ==> Q |] ==> Q";
-by (cut_facts_tac [major RS (realrelE_lemma RS mp)] 1);
-by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
-qed "realrelE";
-
-Goal "(x,x): realrel";
-by (case_tac "x" 1);
-by (asm_simp_tac (simpset() addsimps [realrel_def]) 1);
-qed "realrel_refl";
-
-Goalw [equiv_def, refl_def, sym_def, trans_def] "equiv UNIV realrel";
-by (fast_tac (claset() addSIs [realrelI, realrel_refl]
- addSEs [sym, realrelE, preal_trans_lemma]) 1);
-qed "equiv_realrel";
-
-(* (realrel `` {x} = realrel `` {y}) = ((x,y) : realrel) *)
-bind_thm ("equiv_realrel_iff",
- [equiv_realrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
-
-Goalw [REAL_def,realrel_def,quotient_def] "realrel``{(x,y)}: REAL";
-by (Blast_tac 1);
-qed "realrel_in_real";
-
-Goal "inj_on Abs_REAL REAL";
-by (rtac inj_on_inverseI 1);
-by (etac Abs_REAL_inverse 1);
-qed "inj_on_Abs_REAL";
-
-Addsimps [equiv_realrel_iff,inj_on_Abs_REAL RS inj_on_iff,
- realrel_iff, realrel_in_real, Abs_REAL_inverse];
-
-Addsimps [equiv_realrel RS eq_equiv_class_iff];
-bind_thm ("eq_realrelD", equiv_realrel RSN (2,eq_equiv_class));
-
-Goal "inj Rep_REAL";
-by (rtac inj_inverseI 1);
-by (rtac Rep_REAL_inverse 1);
-qed "inj_Rep_REAL";
-
-(** real_of_preal: the injection from preal to real **)
-Goal "inj(real_of_preal)";
-by (rtac injI 1);
-by (rewtac real_of_preal_def);
-by (dtac (inj_on_Abs_REAL RS inj_onD) 1);
-by (REPEAT (rtac realrel_in_real 1));
-by (dtac eq_equiv_class 1);
-by (rtac equiv_realrel 1);
-by (Blast_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [realrel_def]) 1);
-qed "inj_real_of_preal";
-
-val [prem] = Goal
- "(!!x y. z = Abs_REAL(realrel``{(x,y)}) ==> P) ==> P";
-by (res_inst_tac [("x1","z")]
- (rewrite_rule [REAL_def] Rep_REAL RS quotientE) 1);
-by (dres_inst_tac [("f","Abs_REAL")] arg_cong 1);
-by (case_tac "x" 1);
-by (rtac prem 1);
-by (asm_full_simp_tac (simpset() addsimps [Rep_REAL_inverse]) 1);
-qed "eq_Abs_REAL";
-
-(**** real_minus: additive inverse on real ****)
-
-Goalw [congruent_def]
- "congruent realrel (%p. (%(x,y). realrel``{(y,x)}) p)";
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1);
-qed "real_minus_congruent";
-
-Goalw [real_minus_def]
- "- (Abs_REAL(realrel``{(x,y)})) = Abs_REAL(realrel `` {(y,x)})";
-by (res_inst_tac [("f","Abs_REAL")] arg_cong 1);
-by (simp_tac (simpset() addsimps [realrel_in_real RS Abs_REAL_inverse,
- [equiv_realrel, real_minus_congruent] MRS UN_equiv_class]) 1);
-qed "real_minus";
-
-Goal "- (- z) = (z::real)";
-by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
-by (asm_simp_tac (simpset() addsimps [real_minus]) 1);
-qed "real_minus_minus";
-
-Addsimps [real_minus_minus];
-
-Goal "inj(%r::real. -r)";
-by (rtac injI 1);
-by (dres_inst_tac [("f","uminus")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [real_minus_minus]) 1);
-qed "inj_real_minus";
-
-Goalw [real_zero_def] "- 0 = (0::real)";
-by (simp_tac (simpset() addsimps [real_minus]) 1);
-qed "real_minus_zero";
-
-Addsimps [real_minus_zero];
-
-Goal "(-x = 0) = (x = (0::real))";
-by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_zero_def, real_minus] @ preal_add_ac));
-qed "real_minus_zero_iff";
-
-Addsimps [real_minus_zero_iff];
-
-(*** Congruence property for addition ***)
-Goalw [congruent2_def]
- "congruent2 realrel (%p1 p2. \
-\ (%(x1,y1). (%(x2,y2). realrel``{(x1+x2, y1+y2)}) p2) p1)";
-by (clarify_tac (claset() addSEs [realrelE]) 1);
-by (asm_simp_tac (simpset() addsimps [preal_add_assoc]) 1);
-by (res_inst_tac [("z1.1","x1a")] (preal_add_left_commute RS ssubst) 1);
-by (asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
-by (asm_simp_tac (simpset() addsimps preal_add_ac) 1);
-qed "real_add_congruent2";
-
-Goalw [real_add_def]
- "Abs_REAL(realrel``{(x1,y1)}) + Abs_REAL(realrel``{(x2,y2)}) = \
-\ Abs_REAL(realrel``{(x1+x2, y1+y2)})";
-by (simp_tac (simpset() addsimps
- [[equiv_realrel, real_add_congruent2] MRS UN_equiv_class2]) 1);
-qed "real_add";
-
-Goal "(z::real) + w = w + z";
-by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
-by (res_inst_tac [("z","w")] eq_Abs_REAL 1);
-by (asm_simp_tac (simpset() addsimps preal_add_ac @ [real_add]) 1);
-qed "real_add_commute";
-
-Goal "((z1::real) + z2) + z3 = z1 + (z2 + z3)";
-by (res_inst_tac [("z","z1")] eq_Abs_REAL 1);
-by (res_inst_tac [("z","z2")] eq_Abs_REAL 1);
-by (res_inst_tac [("z","z3")] eq_Abs_REAL 1);
-by (asm_simp_tac (simpset() addsimps [real_add, preal_add_assoc]) 1);
-qed "real_add_assoc";
-
-(*For AC rewriting*)
-Goal "(x::real)+(y+z)=y+(x+z)";
-by(rtac ([real_add_assoc,real_add_commute] MRS
- read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
-qed "real_add_left_commute";
-
-(* real addition is an AC operator *)
-bind_thms ("real_add_ac", [real_add_assoc,real_add_commute,real_add_left_commute]);
-
-Goalw [real_of_preal_def,real_zero_def] "(0::real) + z = z";
-by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
-by (asm_full_simp_tac (simpset() addsimps [real_add] @ preal_add_ac) 1);
-qed "real_add_zero_left";
-Addsimps [real_add_zero_left];
-
-Goal "z + (0::real) = z";
-by (simp_tac (simpset() addsimps [real_add_commute]) 1);
-qed "real_add_zero_right";
-Addsimps [real_add_zero_right];
-
-Goalw [real_zero_def] "z + (-z) = (0::real)";
-by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
-by (asm_full_simp_tac (simpset() addsimps [real_minus,
- real_add, preal_add_commute]) 1);
-qed "real_add_minus";
-Addsimps [real_add_minus];
-
-Goal "(-z) + z = (0::real)";
-by (simp_tac (simpset() addsimps [real_add_commute]) 1);
-qed "real_add_minus_left";
-Addsimps [real_add_minus_left];
-
-
-Goal "z + ((- z) + w) = (w::real)";
-by (simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
-qed "real_add_minus_cancel";
-
-Goal "(-z) + (z + w) = (w::real)";
-by (simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
-qed "real_minus_add_cancel";
-
-Addsimps [real_add_minus_cancel, real_minus_add_cancel];
-
-Goal "EX y. (x::real) + y = 0";
-by (blast_tac (claset() addIs [real_add_minus]) 1);
-qed "real_minus_ex";
-
-Goal "EX! y. (x::real) + y = 0";
-by (auto_tac (claset() addIs [real_add_minus],simpset()));
-by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
-by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
-qed "real_minus_ex1";
-
-Goal "EX! y. y + (x::real) = 0";
-by (auto_tac (claset() addIs [real_add_minus_left],simpset()));
-by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
-by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
-qed "real_minus_left_ex1";
-
-Goal "x + y = (0::real) ==> x = -y";
-by (cut_inst_tac [("z","y")] real_add_minus_left 1);
-by (res_inst_tac [("x1","y")] (real_minus_left_ex1 RS ex1E) 1);
-by (Blast_tac 1);
-qed "real_add_minus_eq_minus";
-
-Goal "EX (y::real). x = -y";
-by (cut_inst_tac [("x","x")] real_minus_ex 1);
-by (etac exE 1 THEN dtac real_add_minus_eq_minus 1);
-by (Fast_tac 1);
-qed "real_as_add_inverse_ex";
-
-Goal "-(x + y) = (-x) + (- y :: real)";
-by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
-by (res_inst_tac [("z","y")] eq_Abs_REAL 1);
-by (auto_tac (claset(),simpset() addsimps [real_minus,real_add]));
-qed "real_minus_add_distrib";
-
-Addsimps [real_minus_add_distrib];
-
-Goal "((x::real) + y = x + z) = (y = z)";
-by (Step_tac 1);
-by (dres_inst_tac [("f","%t. (-x) + t")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
-qed "real_add_left_cancel";
-
-Goal "(y + (x::real)= z + x) = (y = z)";
-by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1);
-qed "real_add_right_cancel";
-
-Goal "(0::real) - x = -x";
-by (simp_tac (simpset() addsimps [real_diff_def]) 1);
-qed "real_diff_0";
-
-Goal "x - (0::real) = x";
-by (simp_tac (simpset() addsimps [real_diff_def]) 1);
-qed "real_diff_0_right";
-
-Goal "x - x = (0::real)";
-by (simp_tac (simpset() addsimps [real_diff_def]) 1);
-qed "real_diff_self";
-
-Addsimps [real_diff_0, real_diff_0_right, real_diff_self];
-
-
-(*** Congruence property for multiplication ***)
-
-Goal "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==> \
-\ x * x1 + y * y1 + (x * y2 + x2 * y) = \
-\ x * x2 + y * y2 + (x * y1 + x1 * y)";
-by (asm_full_simp_tac (simpset() addsimps [preal_add_left_commute,
- preal_add_assoc RS sym,preal_add_mult_distrib2 RS sym]) 1);
-by (rtac (preal_mult_commute RS subst) 1);
-by (res_inst_tac [("y1","x2")] (preal_mult_commute RS subst) 1);
-by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc,
- preal_add_mult_distrib2 RS sym]) 1);
-by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1);
-qed "real_mult_congruent2_lemma";
-
-Goal
- "congruent2 realrel (%p1 p2. \
-\ (%(x1,y1). (%(x2,y2). realrel``{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)";
-by (rtac (equiv_realrel RS congruent2_commuteI) 1);
-by (Clarify_tac 1);
-by (rewtac split_def);
-by (asm_simp_tac (simpset() addsimps [preal_mult_commute,preal_add_commute]) 1);
-by (auto_tac (claset(),simpset() addsimps [real_mult_congruent2_lemma]));
-qed "real_mult_congruent2";
-
-Goalw [real_mult_def]
- "Abs_REAL((realrel``{(x1,y1)})) * Abs_REAL((realrel``{(x2,y2)})) = \
-\ Abs_REAL(realrel `` {(x1*x2+y1*y2,x1*y2+x2*y1)})";
-by (simp_tac (simpset() addsimps
- [[equiv_realrel, real_mult_congruent2] MRS UN_equiv_class2]) 1);
-qed "real_mult";
-
-Goal "(z::real) * w = w * z";
-by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
-by (res_inst_tac [("z","w")] eq_Abs_REAL 1);
-by (asm_simp_tac
- (simpset() addsimps [real_mult] @ preal_add_ac @ preal_mult_ac) 1);
-qed "real_mult_commute";
-
-Goal "((z1::real) * z2) * z3 = z1 * (z2 * z3)";
-by (res_inst_tac [("z","z1")] eq_Abs_REAL 1);
-by (res_inst_tac [("z","z2")] eq_Abs_REAL 1);
-by (res_inst_tac [("z","z3")] eq_Abs_REAL 1);
-by (asm_simp_tac (simpset() addsimps [preal_add_mult_distrib2,real_mult] @
- preal_add_ac @ preal_mult_ac) 1);
-qed "real_mult_assoc";
-
-Goal "(z1::real) * (z2 * z3) = z2 * (z1 * z3)";
-by(rtac ([real_mult_assoc,real_mult_commute] MRS
- read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
-qed "real_mult_left_commute";
-
-(* real multiplication is an AC operator *)
-bind_thms ("real_mult_ac",
- [real_mult_assoc, real_mult_commute, real_mult_left_commute]);
-
-Goalw [real_one_def,pnat_one_def] "(1::real) * z = z";
-by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
-by (asm_full_simp_tac
- (simpset() addsimps [real_mult,
- preal_add_mult_distrib2,preal_mult_1_right]
- @ preal_mult_ac @ preal_add_ac) 1);
-qed "real_mult_1";
-
-Addsimps [real_mult_1];
-
-Goal "z * (1::real) = z";
-by (simp_tac (simpset() addsimps [real_mult_commute]) 1);
-qed "real_mult_1_right";
-
-Addsimps [real_mult_1_right];
-
-Goalw [real_zero_def,pnat_one_def] "0 * z = (0::real)";
-by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
-by (asm_full_simp_tac (simpset() addsimps [real_mult,
- preal_add_mult_distrib2,preal_mult_1_right]
- @ preal_mult_ac @ preal_add_ac) 1);
-qed "real_mult_0";
-
-Goal "z * 0 = (0::real)";
-by (simp_tac (simpset() addsimps [real_mult_commute, real_mult_0]) 1);
-qed "real_mult_0_right";
-
-Addsimps [real_mult_0_right, real_mult_0];
-
-Goal "(-x) * (y::real) = -(x * y)";
-by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
-by (res_inst_tac [("z","y")] eq_Abs_REAL 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_minus,real_mult]
- @ preal_mult_ac @ preal_add_ac));
-qed "real_mult_minus_eq1";
-Addsimps [real_mult_minus_eq1];
-
-bind_thm("real_minus_mult_eq1", real_mult_minus_eq1 RS sym);
-
-Goal "x * (- y :: real) = -(x * y)";
-by (simp_tac (simpset() addsimps [inst "z" "x" real_mult_commute]) 1);
-qed "real_mult_minus_eq2";
-Addsimps [real_mult_minus_eq2];
-
-bind_thm("real_minus_mult_eq2", real_mult_minus_eq2 RS sym);
-
-Goal "(- (1::real)) * z = -z";
-by (Simp_tac 1);
-qed "real_mult_minus_1";
-Addsimps [real_mult_minus_1];
-
-Goal "z * (- (1::real)) = -z";
-by (stac real_mult_commute 1);
-by (Simp_tac 1);
-qed "real_mult_minus_1_right";
-Addsimps [real_mult_minus_1_right];
-
-Goal "(-x) * (-y) = x * (y::real)";
-by (Simp_tac 1);
-qed "real_minus_mult_cancel";
-
-Addsimps [real_minus_mult_cancel];
-
-Goal "(-x) * y = x * (- y :: real)";
-by (Simp_tac 1);
-qed "real_minus_mult_commute";
-
-(** Lemmas **)
-
-Goal "(z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
-by (asm_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
-qed "real_add_assoc_cong";
-
-Goal "(z::real) + (v + w) = v + (z + w)";
-by (REPEAT (ares_tac [real_add_commute RS real_add_assoc_cong] 1));
-qed "real_add_assoc_swap";
-
-Goal "((z1::real) + z2) * w = (z1 * w) + (z2 * w)";
-by (res_inst_tac [("z","z1")] eq_Abs_REAL 1);
-by (res_inst_tac [("z","z2")] eq_Abs_REAL 1);
-by (res_inst_tac [("z","w")] eq_Abs_REAL 1);
-by (asm_simp_tac
- (simpset() addsimps [preal_add_mult_distrib2, real_add, real_mult] @
- preal_add_ac @ preal_mult_ac) 1);
-qed "real_add_mult_distrib";
-
-val real_mult_commute'= inst "z" "w" real_mult_commute;
-
-Goal "(w::real) * (z1 + z2) = (w * z1) + (w * z2)";
-by (simp_tac (simpset() addsimps [real_mult_commute',
- real_add_mult_distrib]) 1);
-qed "real_add_mult_distrib2";
-
-Goalw [real_diff_def] "((z1::real) - z2) * w = (z1 * w) - (z2 * w)";
-by (simp_tac (simpset() addsimps [real_add_mult_distrib]) 1);
-qed "real_diff_mult_distrib";
-
-Goal "(w::real) * (z1 - z2) = (w * z1) - (w * z2)";
-by (simp_tac (simpset() addsimps [real_mult_commute',
- real_diff_mult_distrib]) 1);
-qed "real_diff_mult_distrib2";
-
-(*** one and zero are distinct ***)
-Goalw [real_zero_def,real_one_def] "0 ~= (1::real)";
-by (auto_tac (claset(),
- simpset() addsimps [preal_self_less_add_left RS preal_not_refl2]));
-qed "real_zero_not_eq_one";
-
-(*** existence of inverse ***)
-(** lemma -- alternative definition of 0 **)
-Goalw [real_zero_def] "0 = Abs_REAL (realrel `` {(x, x)})";
-by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
-qed "real_zero_iff";
-
-Goalw [real_zero_def,real_one_def]
- "!!(x::real). x ~= 0 ==> EX y. x*y = (1::real)";
-by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
-by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1);
-by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
- simpset() addsimps [real_zero_iff RS sym]));
-by (res_inst_tac [("x",
- "Abs_REAL (realrel `` \
-\ {(preal_of_prat(prat_of_pnat 1), \
-\ pinv(D) + preal_of_prat(prat_of_pnat 1))})")] exI 1);
-by (res_inst_tac [("x",
- "Abs_REAL (realrel `` \
-\ {(pinv(D) + preal_of_prat(prat_of_pnat 1),\
-\ preal_of_prat(prat_of_pnat 1))})")] exI 2);
-by (auto_tac (claset(),
- simpset() addsimps [real_mult,
- pnat_one_def,preal_mult_1_right,preal_add_mult_distrib2,
- preal_add_mult_distrib,preal_mult_1,preal_mult_inv_right]
- @ preal_add_ac @ preal_mult_ac));
-qed "real_mult_inv_right_ex";
-
-Goal "x ~= 0 ==> EX y. y*x = (1::real)";
-by (dtac real_mult_inv_right_ex 1);
-by (auto_tac (claset(), simpset() addsimps [real_mult_commute]));
-qed "real_mult_inv_left_ex";
-
-Goalw [real_inverse_def] "x ~= 0 ==> inverse(x)*x = (1::real)";
-by (ftac real_mult_inv_left_ex 1);
-by (Step_tac 1);
-by (rtac someI2 1);
-by Auto_tac;
-qed "real_mult_inv_left";
-Addsimps [real_mult_inv_left];
-
-Goal "x ~= 0 ==> x*inverse(x) = (1::real)";
-by (stac real_mult_commute 1);
-by (auto_tac (claset(), simpset() addsimps [real_mult_inv_left]));
-qed "real_mult_inv_right";
-Addsimps [real_mult_inv_right];
-
-(** Inverse of zero! Useful to simplify certain equations **)
-
-Goalw [real_inverse_def] "inverse 0 = (0::real)";
-by (rtac someI2 1);
-by (auto_tac (claset(), simpset() addsimps [real_zero_not_eq_one]));
-qed "INVERSE_ZERO";
-
-Goal "a / (0::real) = 0";
-by (simp_tac (simpset() addsimps [real_divide_def, INVERSE_ZERO]) 1);
-qed "DIVISION_BY_ZERO";
-
-fun real_div_undefined_case_tac s i =
- case_tac s i THEN
- asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO, INVERSE_ZERO]) i;
-
-
-Goal "(c::real) ~= 0 ==> (c*a=c*b) = (a=b)";
-by Auto_tac;
-by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps real_mult_ac) 1);
-qed "real_mult_left_cancel";
-
-Goal "(c::real) ~= 0 ==> (a*c=b*c) = (a=b)";
-by (Step_tac 1);
-by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps real_mult_ac) 1);
-qed "real_mult_right_cancel";
-
-Goal "c*a ~= c*b ==> a ~= b";
-by Auto_tac;
-qed "real_mult_left_cancel_ccontr";
-
-Goal "a*c ~= b*c ==> a ~= b";
-by Auto_tac;
-qed "real_mult_right_cancel_ccontr";
-
-Goalw [real_inverse_def] "x ~= 0 ==> inverse(x::real) ~= 0";
-by (ftac real_mult_inv_left_ex 1);
-by (etac exE 1);
-by (rtac someI2 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_mult_0, real_zero_not_eq_one]));
-qed "real_inverse_not_zero";
-
-Goal "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::real)";
-by (Step_tac 1);
-by (dres_inst_tac [("f","%z. inverse x*z")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
-qed "real_mult_not_zero";
-
-Goal "inverse(inverse (x::real)) = x";
-by (real_div_undefined_case_tac "x=0" 1);
-by (res_inst_tac [("c1","inverse x")] (real_mult_right_cancel RS iffD1) 1);
-by (etac real_inverse_not_zero 1);
-by (auto_tac (claset() addDs [real_inverse_not_zero],simpset()));
-qed "real_inverse_inverse";
-Addsimps [real_inverse_inverse];
-
-Goalw [real_inverse_def] "inverse((1::real)) = (1::real)";
-by (cut_facts_tac [real_zero_not_eq_one RS
- not_sym RS real_mult_inv_left_ex] 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_zero_not_eq_one RS not_sym]));
-qed "real_inverse_1";
-Addsimps [real_inverse_1];
-
-Goal "inverse(-x) = -inverse(x::real)";
-by (real_div_undefined_case_tac "x=0" 1);
-by (res_inst_tac [("c1","-x")] (real_mult_right_cancel RS iffD1) 1);
-by (stac real_mult_inv_left 2);
-by Auto_tac;
-qed "real_minus_inverse";
-
-Goal "inverse(x*y) = inverse(x)*inverse(y::real)";
-by (real_div_undefined_case_tac "x=0" 1);
-by (real_div_undefined_case_tac "y=0" 1);
-by (forw_inst_tac [("y","y")] real_mult_not_zero 1 THEN assume_tac 1);
-by (res_inst_tac [("c1","x")] (real_mult_left_cancel RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym]));
-by (res_inst_tac [("c1","y")] (real_mult_left_cancel RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [real_mult_left_commute]));
-by (asm_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
-qed "real_inverse_distrib";
-
-Goal "(x::real) * (y/z) = (x*y)/z";
-by (simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 1);
-qed "real_times_divide1_eq";
-
-Goal "(y/z) * (x::real) = (y*x)/z";
-by (simp_tac (simpset() addsimps [real_divide_def]@real_mult_ac) 1);
-qed "real_times_divide2_eq";
-
-Addsimps [real_times_divide1_eq, real_times_divide2_eq];
-
-Goal "(x::real) / (y/z) = (x*z)/y";
-by (simp_tac (simpset() addsimps [real_divide_def, real_inverse_distrib]@
- real_mult_ac) 1);
-qed "real_divide_divide1_eq";
-
-Goal "((x::real) / y) / z = x/(y*z)";
-by (simp_tac (simpset() addsimps [real_divide_def, real_inverse_distrib,
- real_mult_assoc]) 1);
-qed "real_divide_divide2_eq";
-
-Addsimps [real_divide_divide1_eq, real_divide_divide2_eq];
-
-(** As with multiplication, pull minus signs OUT of the / operator **)
-
-Goal "(-x) / (y::real) = - (x/y)";
-by (simp_tac (simpset() addsimps [real_divide_def]) 1);
-qed "real_minus_divide_eq";
-Addsimps [real_minus_divide_eq];
-
-Goal "(x / -(y::real)) = - (x/y)";
-by (simp_tac (simpset() addsimps [real_divide_def, real_minus_inverse]) 1);
-qed "real_divide_minus_eq";
-Addsimps [real_divide_minus_eq];
-
-Goal "(x+y)/(z::real) = x/z + y/z";
-by (simp_tac (simpset() addsimps [real_divide_def, real_add_mult_distrib]) 1);
-qed "real_add_divide_distrib";
-
-(*The following would e.g. convert (x+y)/2 to x/2 + y/2. Sometimes that
- leads to cancellations in x or y, but is also prevents "multiplying out"
- the 2 in e.g. (x+y)/2 = 5.
-
-Addsimps [inst "z" "number_of ?w" real_add_divide_distrib];
-**)
-
-
-(*---------------------------------------------------------
- Theorems for ordering
- --------------------------------------------------------*)
-(* prove introduction and elimination rules for real_less *)
-
-(* real_less is a strong order i.e. nonreflexive and transitive *)
-
-(*** lemmas ***)
-Goal "!!(x::preal). [| x = y; x1 = y1 |] ==> x + y1 = x1 + y";
-by (asm_simp_tac (simpset() addsimps [preal_add_commute]) 1);
-qed "preal_lemma_eq_rev_sum";
-
-Goal "!!(b::preal). x + (b + y) = x1 + (b + y1) ==> x + y = x1 + y1";
-by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
-qed "preal_add_left_commute_cancel";
-
-Goal "!!(x::preal). [| x + y2a = x2a + y; \
-\ x + y2b = x2b + y |] \
-\ ==> x2a + y2b = x2b + y2a";
-by (dtac preal_lemma_eq_rev_sum 1);
-by (assume_tac 1);
-by (thin_tac "x + y2b = x2b + y" 1);
-by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
-by (dtac preal_add_left_commute_cancel 1);
-by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
-qed "preal_lemma_for_not_refl";
-
-Goal "~ (R::real) < R";
-by (res_inst_tac [("z","R")] eq_Abs_REAL 1);
-by (auto_tac (claset(),simpset() addsimps [real_less_def]));
-by (dtac preal_lemma_for_not_refl 1);
-by (assume_tac 1);
-by Auto_tac;
-qed "real_less_not_refl";
-
-(*** y < y ==> P ***)
-bind_thm("real_less_irrefl", real_less_not_refl RS notE);
-AddSEs [real_less_irrefl];
-
-Goal "!!(x::real). x < y ==> x ~= y";
-by (auto_tac (claset(),simpset() addsimps [real_less_not_refl]));
-qed "real_not_refl2";
-
-(* lemma re-arranging and eliminating terms *)
-Goal "!! (a::preal). [| a + b = c + d; \
-\ x2b + d + (c + y2e) < a + y2b + (x2e + b) |] \
-\ ==> x2b + y2e < x2e + y2b";
-by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
-by (res_inst_tac [("C","c+d")] preal_add_left_less_cancel 1);
-by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
-qed "preal_lemma_trans";
-
-(** heavy re-writing involved*)
-Goal "!!(R1::real). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
-by (res_inst_tac [("z","R1")] eq_Abs_REAL 1);
-by (res_inst_tac [("z","R2")] eq_Abs_REAL 1);
-by (res_inst_tac [("z","R3")] eq_Abs_REAL 1);
-by (auto_tac (claset(),simpset() addsimps [real_less_def]));
-by (REPEAT(rtac exI 1));
-by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Blast_tac 2));
-by (dtac preal_lemma_for_not_refl 1 THEN assume_tac 1);
-by (blast_tac (claset() addDs [preal_add_less_mono]
- addIs [preal_lemma_trans]) 1);
-qed "real_less_trans";
-
-Goal "!! (R1::real). R1 < R2 ==> ~ (R2 < R1)";
-by (rtac notI 1);
-by (dtac real_less_trans 1 THEN assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [real_less_not_refl]) 1);
-qed "real_less_not_sym";
-
-(* [| x < y; ~P ==> y < x |] ==> P *)
-bind_thm ("real_less_asym", real_less_not_sym RS contrapos_np);
-
-Goalw [real_of_preal_def]
- "real_of_preal ((z1::preal) + z2) = \
-\ real_of_preal z1 + real_of_preal z2";
-by (asm_simp_tac (simpset() addsimps [real_add,
- preal_add_mult_distrib,preal_mult_1] addsimps preal_add_ac) 1);
-qed "real_of_preal_add";
-
-Goalw [real_of_preal_def]
- "real_of_preal ((z1::preal) * z2) = \
-\ real_of_preal z1* real_of_preal z2";
-by (full_simp_tac (simpset() addsimps [real_mult,
- preal_add_mult_distrib2,preal_mult_1,
- preal_mult_1_right,pnat_one_def]
- @ preal_add_ac @ preal_mult_ac) 1);
-qed "real_of_preal_mult";
-
-Goalw [real_of_preal_def]
- "!!(x::preal). y < x ==> \
-\ EX m. Abs_REAL (realrel `` {(x,y)}) = real_of_preal m";
-by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
- simpset() addsimps preal_add_ac));
-qed "real_of_preal_ExI";
-
-Goalw [real_of_preal_def]
- "!!(x::preal). EX m. Abs_REAL (realrel `` {(x,y)}) = \
-\ real_of_preal m ==> y < x";
-by (auto_tac (claset(),
- simpset() addsimps
- [preal_add_commute,preal_add_assoc]));
-by (asm_full_simp_tac (simpset() addsimps
- [preal_add_assoc RS sym,preal_self_less_add_left]) 1);
-qed "real_of_preal_ExD";
-
-Goal "(EX m. Abs_REAL (realrel `` {(x,y)}) = real_of_preal m) = (y < x)";
-by (blast_tac (claset() addSIs [real_of_preal_ExI,real_of_preal_ExD]) 1);
-qed "real_of_preal_iff";
-
-(*** Gleason prop 9-4.4 p 127 ***)
-Goalw [real_of_preal_def,real_zero_def]
- "EX m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)";
-by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
-by (auto_tac (claset(),simpset() addsimps [real_minus] @ preal_add_ac));
-by (cut_inst_tac [("r1.0","x"),("r2.0","y")] preal_linear 1);
-by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
- simpset() addsimps [preal_add_assoc RS sym]));
-by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
-qed "real_of_preal_trichotomy";
-
-Goal "!!P. [| !!m. x = real_of_preal m ==> P; \
-\ x = 0 ==> P; \
-\ !!m. x = -(real_of_preal m) ==> P |] ==> P";
-by (cut_inst_tac [("x","x")] real_of_preal_trichotomy 1);
-by Auto_tac;
-qed "real_of_preal_trichotomyE";
-
-Goalw [real_of_preal_def]
- "real_of_preal m1 < real_of_preal m2 ==> m1 < m2";
-by (auto_tac (claset(),simpset() addsimps [real_less_def] @ preal_add_ac));
-by (auto_tac (claset(),simpset() addsimps [preal_add_assoc RS sym]));
-by (auto_tac (claset(),simpset() addsimps preal_add_ac));
-qed "real_of_preal_lessD";
-
-Goal "m1 < m2 ==> real_of_preal m1 < real_of_preal m2";
-by (dtac preal_less_add_left_Ex 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_of_preal_add,
- real_of_preal_def,real_less_def]));
-by (REPEAT(rtac exI 1));
-by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Blast_tac 2));
-by (simp_tac (simpset() addsimps [preal_self_less_add_left]
- delsimps [preal_add_less_iff2]) 1);
-qed "real_of_preal_lessI";
-
-Goal "(real_of_preal m1 < real_of_preal m2) = (m1 < m2)";
-by (blast_tac (claset() addIs [real_of_preal_lessI,real_of_preal_lessD]) 1);
-qed "real_of_preal_less_iff1";
-
-Addsimps [real_of_preal_less_iff1];
-
-Goal "- real_of_preal m < real_of_preal m";
-by (auto_tac (claset(),
- simpset() addsimps
- [real_of_preal_def,real_less_def,real_minus]));
-by (REPEAT(rtac exI 1));
-by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Blast_tac 2));
-by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
-by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
- preal_add_assoc RS sym]) 1);
-qed "real_of_preal_minus_less_self";
-
-Goalw [real_zero_def] "- real_of_preal m < 0";
-by (auto_tac (claset(),
- simpset() addsimps [real_of_preal_def,
- real_less_def,real_minus]));
-by (REPEAT(rtac exI 1));
-by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Blast_tac 2));
-by (full_simp_tac (simpset() addsimps
- [preal_self_less_add_right] @ preal_add_ac) 1);
-qed "real_of_preal_minus_less_zero";
-
-Goal "~ 0 < - real_of_preal m";
-by (cut_facts_tac [real_of_preal_minus_less_zero] 1);
-by (fast_tac (claset() addDs [real_less_trans]
- addEs [real_less_irrefl]) 1);
-qed "real_of_preal_not_minus_gt_zero";
-
-Goalw [real_zero_def] "0 < real_of_preal m";
-by (auto_tac (claset(),simpset() addsimps
- [real_of_preal_def,real_less_def,real_minus]));
-by (REPEAT(rtac exI 1));
-by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Blast_tac 2));
-by (full_simp_tac (simpset() addsimps
- [preal_self_less_add_right] @ preal_add_ac) 1);
-qed "real_of_preal_zero_less";
-
-Goal "~ real_of_preal m < 0";
-by (cut_facts_tac [real_of_preal_zero_less] 1);
-by (blast_tac (claset() addDs [real_less_trans]
- addEs [real_less_irrefl]) 1);
-qed "real_of_preal_not_less_zero";
-
-Goal "0 < - (- real_of_preal m)";
-by (simp_tac (simpset() addsimps
- [real_of_preal_zero_less]) 1);
-qed "real_minus_minus_zero_less";
-
-(* another lemma *)
-Goalw [real_zero_def]
- "0 < real_of_preal m + real_of_preal m1";
-by (auto_tac (claset(),
- simpset() addsimps [real_of_preal_def,
- real_less_def,real_add]));
-by (REPEAT(rtac exI 1));
-by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Blast_tac 2));
-by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
-by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
- preal_add_assoc RS sym]) 1);
-qed "real_of_preal_sum_zero_less";
-
-Goal "- real_of_preal m < real_of_preal m1";
-by (auto_tac (claset(),
- simpset() addsimps [real_of_preal_def,
- real_less_def,real_minus]));
-by (REPEAT(rtac exI 1));
-by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Blast_tac 2));
-by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
-by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
- preal_add_assoc RS sym]) 1);
-qed "real_of_preal_minus_less_all";
-
-Goal "~ real_of_preal m < - real_of_preal m1";
-by (cut_facts_tac [real_of_preal_minus_less_all] 1);
-by (blast_tac (claset() addDs [real_less_trans]
- addEs [real_less_irrefl]) 1);
-qed "real_of_preal_not_minus_gt_all";
-
-Goal "- real_of_preal m1 < - real_of_preal m2 \
-\ ==> real_of_preal m2 < real_of_preal m1";
-by (auto_tac (claset(),
- simpset() addsimps [real_of_preal_def,
- real_less_def,real_minus]));
-by (REPEAT(rtac exI 1));
-by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Blast_tac 2));
-by (auto_tac (claset(),simpset() addsimps preal_add_ac));
-by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
-by (auto_tac (claset(),simpset() addsimps preal_add_ac));
-qed "real_of_preal_minus_less_rev1";
-
-Goal "real_of_preal m1 < real_of_preal m2 \
-\ ==> - real_of_preal m2 < - real_of_preal m1";
-by (auto_tac (claset(),
- simpset() addsimps [real_of_preal_def,
- real_less_def,real_minus]));
-by (REPEAT(rtac exI 1));
-by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Blast_tac 2));
-by (auto_tac (claset(),simpset() addsimps preal_add_ac));
-by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
-by (auto_tac (claset(),simpset() addsimps preal_add_ac));
-qed "real_of_preal_minus_less_rev2";
-
-Goal "(- real_of_preal m1 < - real_of_preal m2) = \
-\ (real_of_preal m2 < real_of_preal m1)";
-by (blast_tac (claset() addSIs [real_of_preal_minus_less_rev1,
- real_of_preal_minus_less_rev2]) 1);
-qed "real_of_preal_minus_less_rev_iff";
-
-Addsimps [real_of_preal_minus_less_rev_iff];
-
-(*** linearity ***)
-Goal "(R1::real) < R2 | R1 = R2 | R2 < R1";
-by (res_inst_tac [("x","R1")] real_of_preal_trichotomyE 1);
-by (ALLGOALS(res_inst_tac [("x","R2")] real_of_preal_trichotomyE));
-by (auto_tac (claset() addSDs [preal_le_anti_sym],
- simpset() addsimps [preal_less_le_iff,real_of_preal_minus_less_zero,
- real_of_preal_zero_less,real_of_preal_minus_less_all]));
-qed "real_linear";
-
-Goal "!!w::real. (w ~= z) = (w<z | z<w)";
-by (cut_facts_tac [real_linear] 1);
-by (Blast_tac 1);
-qed "real_neq_iff";
-
-Goal "!!(R1::real). [| R1 < R2 ==> P; R1 = R2 ==> P; \
-\ R2 < R1 ==> P |] ==> P";
-by (cut_inst_tac [("R1.0","R1"),("R2.0","R2")] real_linear 1);
-by Auto_tac;
-qed "real_linear_less2";
-
-(*** Properties of <= ***)
-
-Goalw [real_le_def] "~(w < z) ==> z <= (w::real)";
-by (assume_tac 1);
-qed "real_leI";
-
-Goalw [real_le_def] "z<=w ==> ~(w<(z::real))";
-by (assume_tac 1);
-qed "real_leD";
-
-bind_thm ("real_leE", make_elim real_leD);
-
-Goal "(~(w < z)) = (z <= (w::real))";
-by (blast_tac (claset() addSIs [real_leI,real_leD]) 1);
-qed "real_less_le_iff";
-
-Goalw [real_le_def] "~ z <= w ==> w<(z::real)";
-by (Blast_tac 1);
-qed "not_real_leE";
-
-Goalw [real_le_def] "!!(x::real). x <= y ==> x < y | x = y";
-by (cut_facts_tac [real_linear] 1);
-by (blast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
-qed "real_le_imp_less_or_eq";
-
-Goalw [real_le_def] "z<w | z=w ==> z <=(w::real)";
-by (cut_facts_tac [real_linear] 1);
-by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
-qed "real_less_or_eq_imp_le";
-
-Goal "(x <= (y::real)) = (x < y | x=y)";
-by (REPEAT(ares_tac [iffI, real_less_or_eq_imp_le, real_le_imp_less_or_eq] 1));
-qed "real_le_less";
-
-Goal "w <= (w::real)";
-by (simp_tac (simpset() addsimps [real_le_less]) 1);
-qed "real_le_refl";
-
-(* Axiom 'linorder_linear' of class 'linorder': *)
-Goal "(z::real) <= w | w <= z";
-by (simp_tac (simpset() addsimps [real_le_less]) 1);
-by (cut_facts_tac [real_linear] 1);
-by (Blast_tac 1);
-qed "real_le_linear";
-
-Goal "[| i <= j; j <= k |] ==> i <= (k::real)";
-by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
- rtac real_less_or_eq_imp_le,
- blast_tac (claset() addIs [real_less_trans])]);
-qed "real_le_trans";
-
-Goal "[| z <= w; w <= z |] ==> z = (w::real)";
-by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
- fast_tac (claset() addEs [real_less_irrefl,real_less_asym])]);
-qed "real_le_anti_sym";
-
-Goal "[| ~ y < x; y ~= x |] ==> x < (y::real)";
-by (rtac not_real_leE 1);
-by (blast_tac (claset() addDs [real_le_imp_less_or_eq]) 1);
-qed "not_less_not_eq_real_less";
-
-(* Axiom 'order_less_le' of class 'order': *)
-Goal "((w::real) < z) = (w <= z & w ~= z)";
-by (simp_tac (simpset() addsimps [real_le_def, real_neq_iff]) 1);
-by (blast_tac (claset() addSEs [real_less_asym]) 1);
-qed "real_less_le";
-
-Goal "(0 < -R) = (R < (0::real))";
-by (res_inst_tac [("x","R")] real_of_preal_trichotomyE 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_of_preal_not_minus_gt_zero,
- real_of_preal_not_less_zero,real_of_preal_zero_less,
- real_of_preal_minus_less_zero]));
-qed "real_minus_zero_less_iff";
-Addsimps [real_minus_zero_less_iff];
-
-Goal "(-R < 0) = ((0::real) < R)";
-by (res_inst_tac [("x","R")] real_of_preal_trichotomyE 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_of_preal_not_minus_gt_zero,
- real_of_preal_not_less_zero,real_of_preal_zero_less,
- real_of_preal_minus_less_zero]));
-qed "real_minus_zero_less_iff2";
-Addsimps [real_minus_zero_less_iff2];
-
-(*Alternative definition for real_less*)
-Goal "R < S ==> EX T::real. 0 < T & R + T = S";
-by (res_inst_tac [("x","R")] real_of_preal_trichotomyE 1);
-by (ALLGOALS(res_inst_tac [("x","S")] real_of_preal_trichotomyE));
-by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
- simpset() addsimps [real_of_preal_not_minus_gt_all,
- real_of_preal_add, real_of_preal_not_less_zero,
- real_less_not_refl,
- real_of_preal_not_minus_gt_zero]));
-by (res_inst_tac [("x","real_of_preal D")] exI 1);
-by (res_inst_tac [("x","real_of_preal m+real_of_preal ma")] exI 2);
-by (res_inst_tac [("x","real_of_preal D")] exI 3);
-by (auto_tac (claset(),
- simpset() addsimps [real_of_preal_zero_less,
- real_of_preal_sum_zero_less,real_add_assoc]));
-qed "real_less_add_positive_left_Ex";
-
-(** change naff name(s)! **)
-Goal "(W < S) ==> (0 < S + (-W::real))";
-by (dtac real_less_add_positive_left_Ex 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_add_minus,
- real_add_zero_right] @ real_add_ac));
-qed "real_less_sum_gt_zero";
-
-Goal "!!S::real. T = S + W ==> S = T + (-W)";
-by (asm_simp_tac (simpset() addsimps real_add_ac) 1);
-qed "real_lemma_change_eq_subj";
-
-(* FIXME: long! *)
-Goal "(0 < S + (-W::real)) ==> (W < S)";
-by (rtac ccontr 1);
-by (dtac (real_leI RS real_le_imp_less_or_eq) 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_less_not_refl]));
-by (EVERY1[dtac real_less_add_positive_left_Ex, etac exE, etac conjE]);
-by (Asm_full_simp_tac 1);
-by (dtac real_lemma_change_eq_subj 1);
-by Auto_tac;
-by (dtac real_less_sum_gt_zero 1);
-by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1);
-by (EVERY1[rotate_tac 1, dtac (real_add_left_commute RS ssubst)]);
-by (auto_tac (claset() addEs [real_less_asym], simpset()));
-qed "real_sum_gt_zero_less";
-
-Goal "(0 < S + (-W::real)) = (W < S)";
-by (blast_tac (claset() addIs [real_less_sum_gt_zero,
- real_sum_gt_zero_less]) 1);
-qed "real_less_sum_gt_0_iff";
-
-
-Goalw [real_diff_def] "(x<y) = (x-y < (0::real))";
-by (stac (real_minus_zero_less_iff RS sym) 1);
-by (simp_tac (simpset() addsimps [real_add_commute,
- real_less_sum_gt_0_iff]) 1);
-qed "real_less_eq_diff";
-
-
-(*** Subtraction laws ***)
-
-Goal "x + (y - z) = (x + y) - (z::real)";
-by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
-qed "real_add_diff_eq";
-
-Goal "(x - y) + z = (x + z) - (y::real)";
-by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
-qed "real_diff_add_eq";
-
-Goal "(x - y) - z = x - (y + (z::real))";
-by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
-qed "real_diff_diff_eq";
-
-Goal "x - (y - z) = (x + z) - (y::real)";
-by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
-qed "real_diff_diff_eq2";
-
-Goal "(x-y < z) = (x < z + (y::real))";
-by (stac real_less_eq_diff 1);
-by (res_inst_tac [("y1", "z")] (real_less_eq_diff RS ssubst) 1);
-by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
-qed "real_diff_less_eq";
-
-Goal "(x < z-y) = (x + (y::real) < z)";
-by (stac real_less_eq_diff 1);
-by (res_inst_tac [("y1", "z-y")] (real_less_eq_diff RS ssubst) 1);
-by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
-qed "real_less_diff_eq";
-
-Goalw [real_le_def] "(x-y <= z) = (x <= z + (y::real))";
-by (simp_tac (simpset() addsimps [real_less_diff_eq]) 1);
-qed "real_diff_le_eq";
-
-Goalw [real_le_def] "(x <= z-y) = (x + (y::real) <= z)";
-by (simp_tac (simpset() addsimps [real_diff_less_eq]) 1);
-qed "real_le_diff_eq";
-
-Goalw [real_diff_def] "(x-y = z) = (x = z + (y::real))";
-by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
-qed "real_diff_eq_eq";
-
-Goalw [real_diff_def] "(x = z-y) = (x + (y::real) = z)";
-by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
-qed "real_eq_diff_eq";
-
-(*This list of rewrites simplifies (in)equalities by bringing subtractions
- to the top and then moving negative terms to the other side.
- Use with real_add_ac*)
-bind_thms ("real_compare_rls",
- [symmetric real_diff_def,
- real_add_diff_eq, real_diff_add_eq, real_diff_diff_eq, real_diff_diff_eq2,
- real_diff_less_eq, real_less_diff_eq, real_diff_le_eq, real_le_diff_eq,
- real_diff_eq_eq, real_eq_diff_eq]);
-
-
-(** For the cancellation simproc.
- The idea is to cancel like terms on opposite sides by subtraction **)
-
-Goal "(x::real) - y = x' - y' ==> (x<y) = (x'<y')";
-by (stac real_less_eq_diff 1);
-by (res_inst_tac [("y1", "y")] (real_less_eq_diff RS ssubst) 1);
-by (Asm_simp_tac 1);
-qed "real_less_eqI";
-
-Goal "(x::real) - y = x' - y' ==> (y<=x) = (y'<=x')";
-by (dtac real_less_eqI 1);
-by (asm_simp_tac (simpset() addsimps [real_le_def]) 1);
-qed "real_le_eqI";
-
-Goal "(x::real) - y = x' - y' ==> (x=y) = (x'=y')";
-by Safe_tac;
-by (ALLGOALS
- (asm_full_simp_tac
- (simpset() addsimps [real_eq_diff_eq, real_diff_eq_eq])));
-qed "real_eq_eqI";
--- a/src/HOL/Real/RealDef.thy Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Real/RealDef.thy Fri Nov 28 12:09:37 2003 +0100
@@ -3,91 +3,1140 @@
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
Description : The reals
-*)
+*)
+
+theory RealDef = PReal:
-RealDef = PReal +
-
-instance preal :: order (preal_le_refl,preal_le_trans,preal_le_anti_sym,
- preal_less_le)
+instance preal :: order
+proof qed
+ (assumption |
+ rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
constdefs
realrel :: "((preal * preal) * (preal * preal)) set"
- "realrel == {p. EX x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
+ "realrel == {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
+
+typedef (REAL) real = "UNIV//realrel"
+ by (auto simp add: quotient_def)
-typedef (REAL)
- real = "UNIV//realrel" (quotient_def)
+instance real :: ord ..
+instance real :: zero ..
+instance real :: one ..
+instance real :: plus ..
+instance real :: times ..
+instance real :: minus ..
+instance real :: inverse ..
+
+consts
+ (*Overloaded constants denoting the Nat and Real subsets of enclosing
+ types such as hypreal and complex*)
+ Nats :: "'a set"
+ Reals :: "'a set"
+
+ (*overloaded constant for injecting other types into "real"*)
+ real :: "'a => real"
-instance
- real :: {ord, zero, one, plus, times, minus, inverse}
+defs (overloaded)
-consts
- (*Overloaded constants denoting the Nat and Real subsets of enclosing
- types such as hypreal and complex*)
- Nats, Reals :: "'a set"
-
- (*overloaded constant for injecting other types into "real"*)
- real :: 'a => real
-
-
-defs
-
- real_zero_def
+ real_zero_def:
"0 == Abs_REAL(realrel``{(preal_of_prat(prat_of_pnat 1),
preal_of_prat(prat_of_pnat 1))})"
- real_one_def
+ real_one_def:
"1 == Abs_REAL(realrel``
{(preal_of_prat(prat_of_pnat 1) + preal_of_prat(prat_of_pnat 1),
preal_of_prat(prat_of_pnat 1))})"
- real_minus_def
+ real_minus_def:
"- R == Abs_REAL(UN (x,y):Rep_REAL(R). realrel``{(y,x)})"
- real_diff_def
+ real_diff_def:
"R - (S::real) == R + - S"
- real_inverse_def
+ real_inverse_def:
"inverse (R::real) == (SOME S. (R = 0 & S = 0) | S * R = 1)"
- real_divide_def
+ real_divide_def:
"R / (S::real) == R * inverse S"
-
+
constdefs
(** these don't use the overloaded "real" function: users don't see them **)
-
- real_of_preal :: preal => real
+
+ real_of_preal :: "preal => real"
"real_of_preal m ==
Abs_REAL(realrel``{(m + preal_of_prat(prat_of_pnat 1),
preal_of_prat(prat_of_pnat 1))})"
- real_of_posnat :: nat => real
+ real_of_posnat :: "nat => real"
"real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"
-defs
+defs (overloaded)
- (*overloaded*)
- real_of_nat_def "real n == real_of_posnat n + (- 1)"
+ real_of_nat_def: "real n == real_of_posnat n + (- 1)"
- real_add_def
+ real_add_def:
"P+Q == Abs_REAL(UN p1:Rep_REAL(P). UN p2:Rep_REAL(Q).
(%(x1,y1). (%(x2,y2). realrel``{(x1+x2, y1+y2)}) p2) p1)"
-
- real_mult_def
+
+ real_mult_def:
"P*Q == Abs_REAL(UN p1:Rep_REAL(P). UN p2:Rep_REAL(Q).
(%(x1,y1). (%(x2,y2). realrel``{(x1*x2+y1*y2,x1*y2+x2*y1)})
p2) p1)"
- real_less_def
- "P<Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 &
- (x1,y1):Rep_REAL(P) & (x2,y2):Rep_REAL(Q)"
- real_le_def
- "P <= (Q::real) == ~(Q < P)"
+ real_less_def:
+ "P<Q == \<exists>x1 y1 x2 y2. x1 + y2 < x2 + y1 &
+ (x1,y1):Rep_REAL(P) & (x2,y2):Rep_REAL(Q)"
+ real_le_def:
+ "P \<le> (Q::real) == ~(Q < P)"
syntax (xsymbols)
- Reals :: "'a set" ("\\<real>")
- Nats :: "'a set" ("\\<nat>")
+ Reals :: "'a set" ("\<real>")
+ Nats :: "'a set" ("\<nat>")
+
+
+(*** Proving that realrel is an equivalence relation ***)
+
+lemma preal_trans_lemma: "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |]
+ ==> x1 + y3 = x3 + y1"
+apply (rule_tac C = y2 in preal_add_right_cancel)
+apply (rotate_tac 1, drule sym)
+apply (simp add: preal_add_ac)
+apply (rule preal_add_left_commute [THEN subst])
+apply (rule_tac x1 = x1 in preal_add_assoc [THEN subst])
+apply (simp add: preal_add_ac)
+done
+
+(** Natural deduction for realrel **)
+
+lemma realrel_iff [simp]: "(((x1,y1),(x2,y2)): realrel) = (x1 + y2 = x2 + y1)"
+by (unfold realrel_def, blast)
+
+lemma realrel_refl: "(x,x): realrel"
+apply (case_tac "x")
+apply (simp add: realrel_def)
+done
+
+lemma equiv_realrel: "equiv UNIV realrel"
+apply (unfold equiv_def refl_def sym_def trans_def realrel_def)
+apply (fast elim!: sym preal_trans_lemma)
+done
+
+(* (realrel `` {x} = realrel `` {y}) = ((x,y) : realrel) *)
+lemmas equiv_realrel_iff =
+ eq_equiv_class_iff [OF equiv_realrel UNIV_I UNIV_I]
+
+declare equiv_realrel_iff [simp]
+
+lemma realrel_in_real [simp]: "realrel``{(x,y)}: REAL"
+by (unfold REAL_def realrel_def quotient_def, blast)
+
+lemma inj_on_Abs_REAL: "inj_on Abs_REAL REAL"
+apply (rule inj_on_inverseI)
+apply (erule Abs_REAL_inverse)
+done
+
+declare inj_on_Abs_REAL [THEN inj_on_iff, simp]
+declare Abs_REAL_inverse [simp]
+
+
+lemmas eq_realrelD = equiv_realrel [THEN [2] eq_equiv_class]
+
+lemma inj_Rep_REAL: "inj Rep_REAL"
+apply (rule inj_on_inverseI)
+apply (rule Rep_REAL_inverse)
+done
+
+(** real_of_preal: the injection from preal to real **)
+lemma inj_real_of_preal: "inj(real_of_preal)"
+apply (rule inj_onI)
+apply (unfold real_of_preal_def)
+apply (drule inj_on_Abs_REAL [THEN inj_onD])
+apply (rule realrel_in_real)+
+apply (drule eq_equiv_class)
+apply (rule equiv_realrel, blast)
+apply (simp add: realrel_def)
+done
+
+lemma eq_Abs_REAL:
+ "(!!x y. z = Abs_REAL(realrel``{(x,y)}) ==> P) ==> P"
+apply (rule_tac x1 = z in Rep_REAL [unfolded REAL_def, THEN quotientE])
+apply (drule_tac f = Abs_REAL in arg_cong)
+apply (case_tac "x")
+apply (simp add: Rep_REAL_inverse)
+done
+
+(**** real_minus: additive inverse on real ****)
+
+lemma real_minus_congruent:
+ "congruent realrel (%p. (%(x,y). realrel``{(y,x)}) p)"
+apply (unfold congruent_def, clarify)
+apply (simp add: preal_add_commute)
+done
+
+lemma real_minus:
+ "- (Abs_REAL(realrel``{(x,y)})) = Abs_REAL(realrel `` {(y,x)})"
+apply (unfold real_minus_def)
+apply (rule_tac f = Abs_REAL in arg_cong)
+apply (simp add: realrel_in_real [THEN Abs_REAL_inverse]
+ UN_equiv_class [OF equiv_realrel real_minus_congruent])
+done
+
+lemma real_minus_minus: "- (- z) = (z::real)"
+apply (rule_tac z = z in eq_Abs_REAL)
+apply (simp add: real_minus)
+done
+
+declare real_minus_minus [simp]
+
+lemma inj_real_minus: "inj(%r::real. -r)"
+apply (rule inj_onI)
+apply (drule_tac f = uminus in arg_cong)
+apply (simp add: real_minus_minus)
+done
+
+lemma real_minus_zero: "- 0 = (0::real)"
+apply (unfold real_zero_def)
+apply (simp add: real_minus)
+done
+
+declare real_minus_zero [simp]
+
+lemma real_minus_zero_iff: "(-x = 0) = (x = (0::real))"
+apply (rule_tac z = x in eq_Abs_REAL)
+apply (auto simp add: real_zero_def real_minus preal_add_ac)
+done
+
+declare real_minus_zero_iff [simp]
+
+(*** Congruence property for addition ***)
+
+lemma real_add_congruent2_lemma:
+ "[|a + ba = aa + b; ab + bc = ac + bb|]
+ ==> a + ab + (ba + bc) = aa + ac + (b + (bb::preal))"
+apply (simp add: preal_add_assoc)
+apply (rule preal_add_left_commute [of ab, THEN ssubst])
+apply (simp add: preal_add_assoc [symmetric])
+apply (simp add: preal_add_ac)
+done
+
+lemma real_add:
+ "Abs_REAL(realrel``{(x1,y1)}) + Abs_REAL(realrel``{(x2,y2)}) =
+ Abs_REAL(realrel``{(x1+x2, y1+y2)})"
+apply (simp add: real_add_def UN_UN_split_split_eq)
+apply (subst equiv_realrel [THEN UN_equiv_class2])
+apply (auto simp add: congruent2_def)
+apply (blast intro: real_add_congruent2_lemma)
+done
+
+lemma real_add_commute: "(z::real) + w = w + z"
+apply (rule_tac z = z in eq_Abs_REAL)
+apply (rule_tac z = w in eq_Abs_REAL)
+apply (simp add: preal_add_ac real_add)
+done
+
+lemma real_add_assoc: "((z1::real) + z2) + z3 = z1 + (z2 + z3)"
+apply (rule_tac z = z1 in eq_Abs_REAL)
+apply (rule_tac z = z2 in eq_Abs_REAL)
+apply (rule_tac z = z3 in eq_Abs_REAL)
+apply (simp add: real_add preal_add_assoc)
+done
+
+(*For AC rewriting*)
+lemma real_add_left_commute: "(x::real)+(y+z)=y+(x+z)"
+ apply (rule mk_left_commute [of "op +"])
+ apply (rule real_add_assoc)
+ apply (rule real_add_commute)
+ done
+
+
+(* real addition is an AC operator *)
+lemmas real_add_ac = real_add_assoc real_add_commute real_add_left_commute
+
+lemma real_add_zero_left: "(0::real) + z = z"
+apply (unfold real_of_preal_def real_zero_def)
+apply (rule_tac z = z in eq_Abs_REAL)
+apply (simp add: real_add preal_add_ac)
+done
+declare real_add_zero_left [simp]
+
+lemma real_add_zero_right: "z + (0::real) = z"
+by (simp add: real_add_commute)
+declare real_add_zero_right [simp]
+
+instance real :: plus_ac0
+ by (intro_classes,
+ (assumption |
+ rule real_add_commute real_add_assoc real_add_zero_left)+)
+
+
+lemma real_add_minus: "z + (-z) = (0::real)"
+apply (unfold real_zero_def)
+apply (rule_tac z = z in eq_Abs_REAL)
+apply (simp add: real_minus real_add preal_add_commute)
+done
+declare real_add_minus [simp]
+
+lemma real_add_minus_left: "(-z) + z = (0::real)"
+by (simp add: real_add_commute)
+declare real_add_minus_left [simp]
+
+
+lemma real_add_minus_cancel: "z + ((- z) + w) = (w::real)"
+by (simp add: real_add_assoc [symmetric])
+
+lemma real_minus_add_cancel: "(-z) + (z + w) = (w::real)"
+by (simp add: real_add_assoc [symmetric])
+
+declare real_add_minus_cancel [simp] real_minus_add_cancel [simp]
+
+lemma real_minus_ex: "\<exists>y. (x::real) + y = 0"
+by (blast intro: real_add_minus)
+
+lemma real_minus_ex1: "EX! y. (x::real) + y = 0"
+apply (auto intro: real_add_minus)
+apply (drule_tac f = "%x. ya+x" in arg_cong)
+apply (simp add: real_add_assoc [symmetric])
+apply (simp add: real_add_commute)
+done
+
+lemma real_minus_left_ex1: "EX! y. y + (x::real) = 0"
+apply (auto intro: real_add_minus_left)
+apply (drule_tac f = "%x. x+ya" in arg_cong)
+apply (simp add: real_add_assoc)
+apply (simp add: real_add_commute)
+done
+
+lemma real_add_minus_eq_minus: "x + y = (0::real) ==> x = -y"
+apply (cut_tac z = y in real_add_minus_left)
+apply (rule_tac x1 = y in real_minus_left_ex1 [THEN ex1E], blast)
+done
+
+lemma real_as_add_inverse_ex: "\<exists>(y::real). x = -y"
+apply (cut_tac x = x in real_minus_ex)
+apply (erule exE, drule real_add_minus_eq_minus, fast)
+done
+
+lemma real_minus_add_distrib: "-(x + y) = (-x) + (- y :: real)"
+apply (rule_tac z = x in eq_Abs_REAL)
+apply (rule_tac z = y in eq_Abs_REAL)
+apply (auto simp add: real_minus real_add)
+done
+
+declare real_minus_add_distrib [simp]
+
+lemma real_add_left_cancel: "((x::real) + y = x + z) = (y = z)"
+apply safe
+apply (drule_tac f = "%t. (-x) + t" in arg_cong)
+apply (simp add: real_add_assoc [symmetric])
+done
+
+lemma real_add_right_cancel: "(y + (x::real)= z + x) = (y = z)"
+by (simp add: real_add_commute real_add_left_cancel)
+
+lemma real_diff_0: "(0::real) - x = -x"
+by (simp add: real_diff_def)
+
+lemma real_diff_0_right: "x - (0::real) = x"
+by (simp add: real_diff_def)
+
+lemma real_diff_self: "x - x = (0::real)"
+by (simp add: real_diff_def)
+
+declare real_diff_0 [simp] real_diff_0_right [simp] real_diff_self [simp]
+
+
+(*** Congruence property for multiplication ***)
+
+lemma real_mult_congruent2_lemma: "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==>
+ x * x1 + y * y1 + (x * y2 + x2 * y) =
+ x * x2 + y * y2 + (x * y1 + x1 * y)"
+apply (simp add: preal_add_left_commute preal_add_assoc [symmetric] preal_add_mult_distrib2 [symmetric])
+apply (rule preal_mult_commute [THEN subst])
+apply (rule_tac y1 = x2 in preal_mult_commute [THEN subst])
+apply (simp add: preal_add_assoc preal_add_mult_distrib2 [symmetric])
+apply (simp add: preal_add_commute)
+done
+
+lemma real_mult_congruent2:
+ "congruent2 realrel (%p1 p2.
+ (%(x1,y1). (%(x2,y2). realrel``{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)"
+apply (rule equiv_realrel [THEN congruent2_commuteI], clarify)
+apply (unfold split_def)
+apply (simp add: preal_mult_commute preal_add_commute)
+apply (auto simp add: real_mult_congruent2_lemma)
+done
+
+lemma real_mult:
+ "Abs_REAL((realrel``{(x1,y1)})) * Abs_REAL((realrel``{(x2,y2)})) =
+ Abs_REAL(realrel `` {(x1*x2+y1*y2,x1*y2+x2*y1)})"
+apply (unfold real_mult_def)
+apply (simp add: equiv_realrel [THEN UN_equiv_class2] real_mult_congruent2)
+done
+
+lemma real_mult_commute: "(z::real) * w = w * z"
+apply (rule_tac z = z in eq_Abs_REAL)
+apply (rule_tac z = w in eq_Abs_REAL)
+apply (simp add: real_mult preal_add_ac preal_mult_ac)
+done
+
+lemma real_mult_assoc: "((z1::real) * z2) * z3 = z1 * (z2 * z3)"
+apply (rule_tac z = z1 in eq_Abs_REAL)
+apply (rule_tac z = z2 in eq_Abs_REAL)
+apply (rule_tac z = z3 in eq_Abs_REAL)
+apply (simp add: preal_add_mult_distrib2 real_mult preal_add_ac preal_mult_ac)
+done
+
+
+(*For AC rewriting*)
+lemma real_mult_left_commute: "(x::real)*(y*z)=y*(x*z)"
+ apply (rule mk_left_commute [of "op *"])
+ apply (rule real_mult_assoc)
+ apply (rule real_mult_commute)
+ done
+
+(* real multiplication is an AC operator *)
+lemmas real_mult_ac = real_mult_assoc real_mult_commute real_mult_left_commute
+
+lemma real_mult_1: "(1::real) * z = z"
+apply (unfold real_one_def pnat_one_def)
+apply (rule_tac z = z in eq_Abs_REAL)
+apply (simp add: real_mult preal_add_mult_distrib2 preal_mult_1_right preal_mult_ac preal_add_ac)
+done
+
+declare real_mult_1 [simp]
+
+lemma real_mult_1_right: "z * (1::real) = z"
+by (simp add: real_mult_commute)
+
+declare real_mult_1_right [simp]
+
+lemma real_mult_0: "0 * z = (0::real)"
+apply (unfold real_zero_def pnat_one_def)
+apply (rule_tac z = z in eq_Abs_REAL)
+apply (simp add: real_mult preal_add_mult_distrib2 preal_mult_1_right preal_mult_ac preal_add_ac)
+done
+
+lemma real_mult_0_right: "z * 0 = (0::real)"
+by (simp add: real_mult_commute real_mult_0)
+
+declare real_mult_0_right [simp] real_mult_0 [simp]
+
+lemma real_mult_minus_eq1: "(-x) * (y::real) = -(x * y)"
+apply (rule_tac z = x in eq_Abs_REAL)
+apply (rule_tac z = y in eq_Abs_REAL)
+apply (auto simp add: real_minus real_mult preal_mult_ac preal_add_ac)
+done
+declare real_mult_minus_eq1 [simp]
+
+lemmas real_minus_mult_eq1 = real_mult_minus_eq1 [symmetric, standard]
+
+lemma real_mult_minus_eq2: "x * (- y :: real) = -(x * y)"
+by (simp add: real_mult_commute [of x])
+declare real_mult_minus_eq2 [simp]
+
+lemmas real_minus_mult_eq2 = real_mult_minus_eq2 [symmetric, standard]
+
+lemma real_mult_minus_1: "(- (1::real)) * z = -z"
+by simp
+declare real_mult_minus_1 [simp]
+
+lemma real_mult_minus_1_right: "z * (- (1::real)) = -z"
+by (subst real_mult_commute, simp)
+declare real_mult_minus_1_right [simp]
+
+lemma real_minus_mult_cancel: "(-x) * (-y) = x * (y::real)"
+by simp
+
+declare real_minus_mult_cancel [simp]
+
+lemma real_minus_mult_commute: "(-x) * y = x * (- y :: real)"
+by simp
+
+(** Lemmas **)
+
+lemma real_add_assoc_cong: "(z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
+by (simp add: real_add_assoc [symmetric])
+
+lemma real_add_mult_distrib: "((z1::real) + z2) * w = (z1 * w) + (z2 * w)"
+apply (rule_tac z = z1 in eq_Abs_REAL)
+apply (rule_tac z = z2 in eq_Abs_REAL)
+apply (rule_tac z = w in eq_Abs_REAL)
+apply (simp add: preal_add_mult_distrib2 real_add real_mult preal_add_ac preal_mult_ac)
+done
+
+lemma real_add_mult_distrib2: "(w::real) * (z1 + z2) = (w * z1) + (w * z2)"
+by (simp add: real_mult_commute [of w] real_add_mult_distrib)
+
+lemma real_diff_mult_distrib: "((z1::real) - z2) * w = (z1 * w) - (z2 * w)"
+apply (unfold real_diff_def)
+apply (simp add: real_add_mult_distrib)
+done
+
+lemma real_diff_mult_distrib2: "(w::real) * (z1 - z2) = (w * z1) - (w * z2)"
+by (simp add: real_mult_commute [of w] real_diff_mult_distrib)
+
+(*** one and zero are distinct ***)
+lemma real_zero_not_eq_one: "0 ~= (1::real)"
+apply (unfold real_zero_def real_one_def)
+apply (auto simp add: preal_self_less_add_left [THEN preal_not_refl2])
+done
+
+(*** existence of inverse ***)
+(** lemma -- alternative definition of 0 **)
+lemma real_zero_iff: "0 = Abs_REAL (realrel `` {(x, x)})"
+apply (unfold real_zero_def)
+apply (auto simp add: preal_add_commute)
+done
+
+
+(*MOVE UP*)
+instance preal :: order
+ by (intro_classes,
+ (assumption |
+ rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+)
+
+lemma preal_le_linear: "x <= y | y <= (x::preal)"
+apply (insert preal_linear [of x y])
+apply (auto simp add: order_less_le)
+done
+
+instance preal :: linorder
+ by (intro_classes, rule preal_le_linear)
+
+
+lemma real_mult_inv_right_ex:
+ "!!(x::real). x ~= 0 ==> \<exists>y. x*y = (1::real)"
+apply (unfold real_zero_def real_one_def)
+apply (rule_tac z = x in eq_Abs_REAL)
+apply (cut_tac x = xa and y = y in linorder_less_linear)
+apply (auto dest!: preal_less_add_left_Ex simp add: real_zero_iff [symmetric])
+apply (rule_tac x = "Abs_REAL (realrel `` { (preal_of_prat (prat_of_pnat 1), pinv (D) + preal_of_prat (prat_of_pnat 1))}) " in exI)
+apply (rule_tac [2] x = "Abs_REAL (realrel `` { (pinv (D) + preal_of_prat (prat_of_pnat 1), preal_of_prat (prat_of_pnat 1))}) " in exI)
+apply (auto simp add: real_mult pnat_one_def preal_mult_1_right preal_add_mult_distrib2 preal_add_mult_distrib preal_mult_1 preal_mult_inv_right preal_add_ac preal_mult_ac)
+done
+
+lemma real_mult_inv_left_ex: "x ~= 0 ==> \<exists>y. y*x = (1::real)"
+apply (drule real_mult_inv_right_ex)
+apply (auto simp add: real_mult_commute)
+done
+
+lemma real_mult_inv_left: "x ~= 0 ==> inverse(x)*x = (1::real)"
+apply (unfold real_inverse_def)
+apply (frule real_mult_inv_left_ex, safe)
+apply (rule someI2, auto)
+done
+declare real_mult_inv_left [simp]
+
+lemma real_mult_inv_right: "x ~= 0 ==> x*inverse(x) = (1::real)"
+apply (subst real_mult_commute)
+apply (auto simp add: real_mult_inv_left)
+done
+declare real_mult_inv_right [simp]
+
+
+(*---------------------------------------------------------
+ Theorems for ordering
+ --------------------------------------------------------*)
+(* prove introduction and elimination rules for real_less *)
+
+(* real_less is a strong order i.e. nonreflexive and transitive *)
+
+(*** lemmas ***)
+lemma preal_lemma_eq_rev_sum: "!!(x::preal). [| x = y; x1 = y1 |] ==> x + y1 = x1 + y"
+by (simp add: preal_add_commute)
+
+lemma preal_add_left_commute_cancel: "!!(b::preal). x + (b + y) = x1 + (b + y1) ==> x + y = x1 + y1"
+by (simp add: preal_add_ac)
+
+lemma preal_lemma_for_not_refl: "!!(x::preal). [| x + y2a = x2a + y;
+ x + y2b = x2b + y |]
+ ==> x2a + y2b = x2b + y2a"
+apply (drule preal_lemma_eq_rev_sum, assumption)
+apply (erule_tac V = "x + y2b = x2b + y" in thin_rl)
+apply (simp add: preal_add_ac)
+apply (drule preal_add_left_commute_cancel)
+apply (simp add: preal_add_ac)
+done
+
+lemma real_less_not_refl: "~ (R::real) < R"
+apply (rule_tac z = R in eq_Abs_REAL)
+apply (auto simp add: real_less_def)
+apply (drule preal_lemma_for_not_refl, assumption, auto)
+done
+
+(*** y < y ==> P ***)
+lemmas real_less_irrefl = real_less_not_refl [THEN notE, standard]
+declare real_less_irrefl [elim!]
+
+lemma real_not_refl2: "!!(x::real). x < y ==> x ~= y"
+by (auto simp add: real_less_not_refl)
+
+(* lemma re-arranging and eliminating terms *)
+lemma preal_lemma_trans: "!! (a::preal). [| a + b = c + d;
+ x2b + d + (c + y2e) < a + y2b + (x2e + b) |]
+ ==> x2b + y2e < x2e + y2b"
+apply (simp add: preal_add_ac)
+apply (rule_tac C = "c+d" in preal_add_left_less_cancel)
+apply (simp add: preal_add_assoc [symmetric])
+done
+
+(** A MESS! heavy re-writing involved*)
+lemma real_less_trans: "!!(R1::real). [| R1 < R2; R2 < R3 |] ==> R1 < R3"
+apply (rule_tac z = R1 in eq_Abs_REAL)
+apply (rule_tac z = R2 in eq_Abs_REAL)
+apply (rule_tac z = R3 in eq_Abs_REAL)
+apply (auto simp add: real_less_def)
+apply (rule exI)+
+apply (rule conjI, rule_tac [2] conjI)
+ prefer 2 apply blast
+ prefer 2 apply blast
+apply (drule preal_lemma_for_not_refl, assumption)
+apply (blast dest: preal_add_less_mono intro: preal_lemma_trans)
+done
+
+lemma real_less_not_sym: "!! (R1::real). R1 < R2 ==> ~ (R2 < R1)"
+apply (rule notI)
+apply (drule real_less_trans, assumption)
+apply (simp add: real_less_not_refl)
+done
+
+(* [| x < y; ~P ==> y < x |] ==> P *)
+lemmas real_less_asym = real_less_not_sym [THEN contrapos_np, standard]
+
+lemma real_of_preal_add:
+ "real_of_preal ((z1::preal) + z2) =
+ real_of_preal z1 + real_of_preal z2"
+apply (unfold real_of_preal_def)
+apply (simp add: real_add preal_add_mult_distrib preal_mult_1 add: preal_add_ac)
+done
+
+lemma real_of_preal_mult:
+ "real_of_preal ((z1::preal) * z2) =
+ real_of_preal z1* real_of_preal z2"
+apply (unfold real_of_preal_def)
+apply (simp (no_asm_use) add: real_mult preal_add_mult_distrib2 preal_mult_1 preal_mult_1_right pnat_one_def preal_add_ac preal_mult_ac)
+done
+
+lemma real_of_preal_ExI:
+ "!!(x::preal). y < x ==>
+ \<exists>m. Abs_REAL (realrel `` {(x,y)}) = real_of_preal m"
+apply (unfold real_of_preal_def)
+apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_ac)
+done
+
+lemma real_of_preal_ExD:
+ "!!(x::preal). \<exists>m. Abs_REAL (realrel `` {(x,y)}) =
+ real_of_preal m ==> y < x"
+apply (unfold real_of_preal_def)
+apply (auto simp add: preal_add_commute preal_add_assoc)
+apply (simp add: preal_add_assoc [symmetric] preal_self_less_add_left)
+done
+
+lemma real_of_preal_iff: "(\<exists>m. Abs_REAL (realrel `` {(x,y)}) = real_of_preal m) = (y < x)"
+by (blast intro!: real_of_preal_ExI real_of_preal_ExD)
+
+(*** Gleason prop 9-4.4 p 127 ***)
+lemma real_of_preal_trichotomy:
+ "\<exists>m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)"
+apply (unfold real_of_preal_def real_zero_def)
+apply (rule_tac z = x in eq_Abs_REAL)
+apply (auto simp add: real_minus preal_add_ac)
+apply (cut_tac x = x and y = y in linorder_less_linear)
+apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_assoc [symmetric])
+apply (auto simp add: preal_add_commute)
+done
+
+lemma real_of_preal_trichotomyE: "!!P. [| !!m. x = real_of_preal m ==> P;
+ x = 0 ==> P;
+ !!m. x = -(real_of_preal m) ==> P |] ==> P"
+apply (cut_tac x = x in real_of_preal_trichotomy, auto)
+done
+
+lemma real_of_preal_lessD:
+ "real_of_preal m1 < real_of_preal m2 ==> m1 < m2"
+apply (unfold real_of_preal_def)
+apply (auto simp add: real_less_def preal_add_ac)
+apply (auto simp add: preal_add_assoc [symmetric])
+apply (auto simp add: preal_add_ac)
+done
+
+lemma real_of_preal_lessI: "m1 < m2 ==> real_of_preal m1 < real_of_preal m2"
+apply (drule preal_less_add_left_Ex)
+apply (auto simp add: real_of_preal_add real_of_preal_def real_less_def)
+apply (rule exI)+
+apply (rule conjI, rule_tac [2] conjI)
+ apply (rule_tac [2] refl)+
+apply (simp add: preal_self_less_add_left del: preal_add_less_iff2)
+done
+
+lemma real_of_preal_less_iff1: "(real_of_preal m1 < real_of_preal m2) = (m1 < m2)"
+by (blast intro: real_of_preal_lessI real_of_preal_lessD)
+
+declare real_of_preal_less_iff1 [simp]
+
+lemma real_of_preal_minus_less_self: "- real_of_preal m < real_of_preal m"
+apply (auto simp add: real_of_preal_def real_less_def real_minus)
+apply (rule exI)+
+apply (rule conjI, rule_tac [2] conjI)
+ apply (rule_tac [2] refl)+
+apply (simp (no_asm_use) add: preal_add_ac)
+apply (simp (no_asm_use) add: preal_self_less_add_right preal_add_assoc [symmetric])
+done
+
+lemma real_of_preal_minus_less_zero: "- real_of_preal m < 0"
+apply (unfold real_zero_def)
+apply (auto simp add: real_of_preal_def real_less_def real_minus)
+apply (rule exI)+
+apply (rule conjI, rule_tac [2] conjI)
+ apply (rule_tac [2] refl)+
+apply (simp (no_asm_use) add: preal_self_less_add_right preal_add_ac)
+done
+
+lemma real_of_preal_not_minus_gt_zero: "~ 0 < - real_of_preal m"
+apply (cut_tac real_of_preal_minus_less_zero)
+apply (fast dest: real_less_trans elim: real_less_irrefl)
+done
+
+lemma real_of_preal_zero_less: "0 < real_of_preal m"
+apply (unfold real_zero_def)
+apply (auto simp add: real_of_preal_def real_less_def real_minus)
+apply (rule exI)+
+apply (rule conjI, rule_tac [2] conjI)
+ apply (rule_tac [2] refl)+
+apply (simp (no_asm_use) add: preal_self_less_add_right preal_add_ac)
+done
+
+lemma real_of_preal_not_less_zero: "~ real_of_preal m < 0"
+apply (cut_tac real_of_preal_zero_less)
+apply (blast dest: real_less_trans elim: real_less_irrefl)
+done
+
+lemma real_minus_minus_zero_less: "0 < - (- real_of_preal m)"
+by (simp add: real_of_preal_zero_less)
+
+(* another lemma *)
+lemma real_of_preal_sum_zero_less:
+ "0 < real_of_preal m + real_of_preal m1"
+apply (unfold real_zero_def)
+apply (auto simp add: real_of_preal_def real_less_def real_add)
+apply (rule exI)+
+apply (rule conjI, rule_tac [2] conjI)
+ apply (rule_tac [2] refl)+
+apply (simp (no_asm_use) add: preal_add_ac)
+apply (simp (no_asm_use) add: preal_self_less_add_right preal_add_assoc [symmetric])
+done
+
+lemma real_of_preal_minus_less_all: "- real_of_preal m < real_of_preal m1"
+apply (auto simp add: real_of_preal_def real_less_def real_minus)
+apply (rule exI)+
+apply (rule conjI, rule_tac [2] conjI)
+ apply (rule_tac [2] refl)+
+apply (simp (no_asm_use) add: preal_add_ac)
+apply (simp (no_asm_use) add: preal_self_less_add_right preal_add_assoc [symmetric])
+done
+
+lemma real_of_preal_not_minus_gt_all: "~ real_of_preal m < - real_of_preal m1"
+apply (cut_tac real_of_preal_minus_less_all)
+apply (blast dest: real_less_trans elim: real_less_irrefl)
+done
+
+lemma real_of_preal_minus_less_rev1: "- real_of_preal m1 < - real_of_preal m2
+ ==> real_of_preal m2 < real_of_preal m1"
+apply (auto simp add: real_of_preal_def real_less_def real_minus)
+apply (rule exI)+
+apply (rule conjI, rule_tac [2] conjI)
+ apply (rule_tac [2] refl)+
+apply (auto simp add: preal_add_ac)
+apply (simp add: preal_add_assoc [symmetric])
+apply (auto simp add: preal_add_ac)
+done
+
+lemma real_of_preal_minus_less_rev2: "real_of_preal m1 < real_of_preal m2
+ ==> - real_of_preal m2 < - real_of_preal m1"
+apply (auto simp add: real_of_preal_def real_less_def real_minus)
+apply (rule exI)+
+apply (rule conjI, rule_tac [2] conjI)
+ apply (rule_tac [2] refl)+
+apply (auto simp add: preal_add_ac)
+apply (simp add: preal_add_assoc [symmetric])
+apply (auto simp add: preal_add_ac)
+done
+
+lemma real_of_preal_minus_less_rev_iff: "(- real_of_preal m1 < - real_of_preal m2) =
+ (real_of_preal m2 < real_of_preal m1)"
+apply (blast intro!: real_of_preal_minus_less_rev1 real_of_preal_minus_less_rev2)
+done
+
+declare real_of_preal_minus_less_rev_iff [simp]
+
+(*** linearity ***)
+lemma real_linear: "(x::real) < y | x = y | y < x"
+apply (rule_tac x = x in real_of_preal_trichotomyE)
+apply (rule_tac [!] x = y in real_of_preal_trichotomyE)
+apply (auto dest!: preal_le_anti_sym simp add: preal_less_le_iff real_of_preal_minus_less_zero real_of_preal_zero_less real_of_preal_minus_less_all)
+done
+
+lemma real_neq_iff: "!!w::real. (w ~= z) = (w<z | z<w)"
+by (cut_tac real_linear, blast)
+
+
+lemma real_linear_less2: "!!(R1::real). [| R1 < R2 ==> P; R1 = R2 ==> P;
+ R2 < R1 ==> P |] ==> P"
+apply (cut_tac x = R1 and y = R2 in real_linear, auto)
+done
+
+(*** Properties of <= ***)
+
+lemma real_leI: "~(w < z) ==> z \<le> (w::real)"
+
+apply (unfold real_le_def, assumption)
+done
+
+lemma real_leD: "z\<le>w ==> ~(w<(z::real))"
+by (unfold real_le_def, assumption)
+
+lemmas real_leE = real_leD [elim_format]
+
+lemma real_less_le_iff: "(~(w < z)) = (z \<le> (w::real))"
+by (blast intro!: real_leI real_leD)
+
+lemma not_real_leE: "~ z \<le> w ==> w<(z::real)"
+by (unfold real_le_def, blast)
+
+lemma real_le_imp_less_or_eq: "!!(x::real). x \<le> y ==> x < y | x = y"
+apply (unfold real_le_def)
+apply (cut_tac real_linear)
+apply (blast elim: real_less_irrefl real_less_asym)
+done
+
+lemma real_less_or_eq_imp_le: "z<w | z=w ==> z \<le>(w::real)"
+apply (unfold real_le_def)
+apply (cut_tac real_linear)
+apply (fast elim: real_less_irrefl real_less_asym)
+done
+
+lemma real_le_less: "(x \<le> (y::real)) = (x < y | x=y)"
+by (blast intro!: real_less_or_eq_imp_le dest!: real_le_imp_less_or_eq)
+
+lemma real_le_refl: "w \<le> (w::real)"
+by (simp add: real_le_less)
+
+lemma real_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::real)"
+apply (drule real_le_imp_less_or_eq)
+apply (drule real_le_imp_less_or_eq)
+apply (rule real_less_or_eq_imp_le)
+apply (blast intro: real_less_trans)
+done
+
+lemma real_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::real)"
+apply (drule real_le_imp_less_or_eq)
+apply (drule real_le_imp_less_or_eq)
+apply (fast elim: real_less_irrefl real_less_asym)
+done
+
+(* Axiom 'order_less_le' of class 'order': *)
+lemma real_less_le: "((w::real) < z) = (w \<le> z & w ~= z)"
+apply (simp add: real_le_def real_neq_iff)
+apply (blast elim!: real_less_asym)
+done
+
+instance real :: order
+ by (intro_classes,
+ (assumption |
+ rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+)
+
+(* Axiom 'linorder_linear' of class 'linorder': *)
+lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
+apply (simp add: real_le_less)
+apply (cut_tac real_linear, blast)
+done
+
+instance real :: linorder
+ by (intro_classes, rule real_le_linear)
+
+
+lemma real_minus_zero_less_iff: "(0 < -R) = (R < (0::real))"
+apply (rule_tac x = R in real_of_preal_trichotomyE)
+apply (auto simp add: real_of_preal_not_minus_gt_zero real_of_preal_not_less_zero real_of_preal_zero_less real_of_preal_minus_less_zero)
+done
+declare real_minus_zero_less_iff [simp]
+
+lemma real_minus_zero_less_iff2: "(-R < 0) = ((0::real) < R)"
+apply (rule_tac x = R in real_of_preal_trichotomyE)
+apply (auto simp add: real_of_preal_not_minus_gt_zero real_of_preal_not_less_zero real_of_preal_zero_less real_of_preal_minus_less_zero)
+done
+declare real_minus_zero_less_iff2 [simp]
+
+(*Alternative definition for real_less*)
+lemma real_less_add_positive_left_Ex: "R < S ==> \<exists>T::real. 0 < T & R + T = S"
+apply (rule_tac x = R in real_of_preal_trichotomyE)
+apply (rule_tac [!] x = S in real_of_preal_trichotomyE)
+apply (auto dest!: preal_less_add_left_Ex simp add: real_of_preal_not_minus_gt_all real_of_preal_add real_of_preal_not_less_zero real_less_not_refl real_of_preal_not_minus_gt_zero)
+apply (rule_tac x = "real_of_preal D" in exI)
+apply (rule_tac [2] x = "real_of_preal m+real_of_preal ma" in exI)
+apply (rule_tac [3] x = "real_of_preal D" in exI)
+apply (auto simp add: real_of_preal_zero_less real_of_preal_sum_zero_less real_add_assoc)
+done
+
+(** change naff name(s)! **)
+lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (-W::real))"
+apply (drule real_less_add_positive_left_Ex)
+apply (auto simp add: real_add_minus real_add_zero_right real_add_ac)
+done
+
+lemma real_lemma_change_eq_subj: "!!S::real. T = S + W ==> S = T + (-W)"
+by (simp add: real_add_ac)
+
+(* FIXME: long! *)
+lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) ==> (W < S)"
+apply (rule ccontr)
+apply (drule real_leI [THEN real_le_imp_less_or_eq])
+apply (auto simp add: real_less_not_refl)
+apply (drule real_less_add_positive_left_Ex, clarify, simp)
+apply (drule real_lemma_change_eq_subj, auto)
+apply (drule real_less_sum_gt_zero)
+apply (auto elim: real_less_asym simp add: real_add_left_commute [of W] real_add_ac)
+done
+
+lemma real_less_sum_gt_0_iff: "(0 < S + (-W::real)) = (W < S)"
+by (blast intro: real_less_sum_gt_zero real_sum_gt_zero_less)
+
+
+lemma real_less_eq_diff: "(x<y) = (x-y < (0::real))"
+apply (unfold real_diff_def)
+apply (subst real_minus_zero_less_iff [symmetric])
+apply (simp add: real_add_commute real_less_sum_gt_0_iff)
+done
+
+
+(*** Subtraction laws ***)
+
+lemma real_add_diff_eq: "x + (y - z) = (x + y) - (z::real)"
+by (simp add: real_diff_def real_add_ac)
+
+lemma real_diff_add_eq: "(x - y) + z = (x + z) - (y::real)"
+by (simp add: real_diff_def real_add_ac)
+
+lemma real_diff_diff_eq: "(x - y) - z = x - (y + (z::real))"
+by (simp add: real_diff_def real_add_ac)
+
+lemma real_diff_diff_eq2: "x - (y - z) = (x + z) - (y::real)"
+by (simp add: real_diff_def real_add_ac)
+
+lemma real_diff_less_eq: "(x-y < z) = (x < z + (y::real))"
+apply (subst real_less_eq_diff)
+apply (rule_tac y1 = z in real_less_eq_diff [THEN ssubst])
+apply (simp add: real_diff_def real_add_ac)
+done
+
+lemma real_less_diff_eq: "(x < z-y) = (x + (y::real) < z)"
+apply (subst real_less_eq_diff)
+apply (rule_tac y1 = "z-y" in real_less_eq_diff [THEN ssubst])
+apply (simp add: real_diff_def real_add_ac)
+done
+
+lemma real_diff_le_eq: "(x-y \<le> z) = (x \<le> z + (y::real))"
+apply (unfold real_le_def)
+apply (simp add: real_less_diff_eq)
+done
+
+lemma real_le_diff_eq: "(x \<le> z-y) = (x + (y::real) \<le> z)"
+apply (unfold real_le_def)
+apply (simp add: real_diff_less_eq)
+done
+
+lemma real_diff_eq_eq: "(x-y = z) = (x = z + (y::real))"
+apply (unfold real_diff_def)
+apply (auto simp add: real_add_assoc)
+done
+
+lemma real_eq_diff_eq: "(x = z-y) = (x + (y::real) = z)"
+apply (unfold real_diff_def)
+apply (auto simp add: real_add_assoc)
+done
+
+(*This list of rewrites simplifies (in)equalities by bringing subtractions
+ to the top and then moving negative terms to the other side.
+ Use with real_add_ac*)
+lemmas real_compare_rls =
+ real_diff_def [symmetric]
+ real_add_diff_eq real_diff_add_eq real_diff_diff_eq real_diff_diff_eq2
+ real_diff_less_eq real_less_diff_eq real_diff_le_eq real_le_diff_eq
+ real_diff_eq_eq real_eq_diff_eq
+
+
+(** For the cancellation simproc.
+ The idea is to cancel like terms on opposite sides by subtraction **)
+
+lemma real_less_eqI: "(x::real) - y = x' - y' ==> (x<y) = (x'<y')"
+apply (subst real_less_eq_diff)
+apply (rule_tac y1 = y in real_less_eq_diff [THEN ssubst], simp)
+done
+
+lemma real_le_eqI: "(x::real) - y = x' - y' ==> (y\<le>x) = (y'\<le>x')"
+apply (drule real_less_eqI)
+apply (simp add: real_le_def)
+done
+
+lemma real_eq_eqI: "(x::real) - y = x' - y' ==> (x=y) = (x'=y')"
+apply safe
+apply (simp_all add: real_eq_diff_eq real_diff_eq_eq)
+done
+
+
+ML
+{*
+val real_le_def = thm "real_le_def";
+val real_diff_def = thm "real_diff_def";
+val real_divide_def = thm "real_divide_def";
+val real_of_nat_def = thm "real_of_nat_def";
+
+val preal_trans_lemma = thm"preal_trans_lemma";
+val realrel_iff = thm"realrel_iff";
+val realrel_refl = thm"realrel_refl";
+val equiv_realrel = thm"equiv_realrel";
+val equiv_realrel_iff = thm"equiv_realrel_iff";
+val realrel_in_real = thm"realrel_in_real";
+val inj_on_Abs_REAL = thm"inj_on_Abs_REAL";
+val eq_realrelD = thm"eq_realrelD";
+val inj_Rep_REAL = thm"inj_Rep_REAL";
+val inj_real_of_preal = thm"inj_real_of_preal";
+val eq_Abs_REAL = thm"eq_Abs_REAL";
+val real_minus_congruent = thm"real_minus_congruent";
+val real_minus = thm"real_minus";
+val real_minus_minus = thm"real_minus_minus";
+val inj_real_minus = thm"inj_real_minus";
+val real_minus_zero = thm"real_minus_zero";
+val real_minus_zero_iff = thm"real_minus_zero_iff";
+val real_add_congruent2_lemma = thm"real_add_congruent2_lemma";
+val real_add = thm"real_add";
+val real_add_commute = thm"real_add_commute";
+val real_add_assoc = thm"real_add_assoc";
+val real_add_left_commute = thm"real_add_left_commute";
+val real_add_zero_left = thm"real_add_zero_left";
+val real_add_zero_right = thm"real_add_zero_right";
+val real_add_minus = thm"real_add_minus";
+val real_add_minus_left = thm"real_add_minus_left";
+val real_add_minus_cancel = thm"real_add_minus_cancel";
+val real_minus_add_cancel = thm"real_minus_add_cancel";
+val real_minus_ex = thm"real_minus_ex";
+val real_minus_ex1 = thm"real_minus_ex1";
+val real_minus_left_ex1 = thm"real_minus_left_ex1";
+val real_add_minus_eq_minus = thm"real_add_minus_eq_minus";
+val real_as_add_inverse_ex = thm"real_as_add_inverse_ex";
+val real_minus_add_distrib = thm"real_minus_add_distrib";
+val real_add_left_cancel = thm"real_add_left_cancel";
+val real_add_right_cancel = thm"real_add_right_cancel";
+val real_diff_0 = thm"real_diff_0";
+val real_diff_0_right = thm"real_diff_0_right";
+val real_diff_self = thm"real_diff_self";
+val real_mult_congruent2_lemma = thm"real_mult_congruent2_lemma";
+val real_mult_congruent2 = thm"real_mult_congruent2";
+val real_mult = thm"real_mult";
+val real_mult_commute = thm"real_mult_commute";
+val real_mult_assoc = thm"real_mult_assoc";
+val real_mult_left_commute = thm"real_mult_left_commute";
+val real_mult_1 = thm"real_mult_1";
+val real_mult_1_right = thm"real_mult_1_right";
+val real_mult_0 = thm"real_mult_0";
+val real_mult_0_right = thm"real_mult_0_right";
+val real_mult_minus_eq1 = thm"real_mult_minus_eq1";
+val real_minus_mult_eq1 = thm"real_minus_mult_eq1";
+val real_mult_minus_eq2 = thm"real_mult_minus_eq2";
+val real_minus_mult_eq2 = thm"real_minus_mult_eq2";
+val real_mult_minus_1 = thm"real_mult_minus_1";
+val real_mult_minus_1_right = thm"real_mult_minus_1_right";
+val real_minus_mult_cancel = thm"real_minus_mult_cancel";
+val real_minus_mult_commute = thm"real_minus_mult_commute";
+val real_add_assoc_cong = thm"real_add_assoc_cong";
+val real_add_mult_distrib = thm"real_add_mult_distrib";
+val real_add_mult_distrib2 = thm"real_add_mult_distrib2";
+val real_diff_mult_distrib = thm"real_diff_mult_distrib";
+val real_diff_mult_distrib2 = thm"real_diff_mult_distrib2";
+val real_zero_not_eq_one = thm"real_zero_not_eq_one";
+val real_zero_iff = thm"real_zero_iff";
+val preal_le_linear = thm"preal_le_linear";
+val real_mult_inv_right_ex = thm"real_mult_inv_right_ex";
+val real_mult_inv_left_ex = thm"real_mult_inv_left_ex";
+val real_mult_inv_left = thm"real_mult_inv_left";
+val real_mult_inv_right = thm"real_mult_inv_right";
+val preal_lemma_eq_rev_sum = thm"preal_lemma_eq_rev_sum";
+val preal_add_left_commute_cancel = thm"preal_add_left_commute_cancel";
+val preal_lemma_for_not_refl = thm"preal_lemma_for_not_refl";
+val real_less_not_refl = thm"real_less_not_refl";
+val real_less_irrefl = thm"real_less_irrefl";
+val real_not_refl2 = thm"real_not_refl2";
+val preal_lemma_trans = thm"preal_lemma_trans";
+val real_less_trans = thm"real_less_trans";
+val real_less_not_sym = thm"real_less_not_sym";
+val real_less_asym = thm"real_less_asym";
+val real_of_preal_add = thm"real_of_preal_add";
+val real_of_preal_mult = thm"real_of_preal_mult";
+val real_of_preal_ExI = thm"real_of_preal_ExI";
+val real_of_preal_ExD = thm"real_of_preal_ExD";
+val real_of_preal_iff = thm"real_of_preal_iff";
+val real_of_preal_trichotomy = thm"real_of_preal_trichotomy";
+val real_of_preal_trichotomyE = thm"real_of_preal_trichotomyE";
+val real_of_preal_lessD = thm"real_of_preal_lessD";
+val real_of_preal_lessI = thm"real_of_preal_lessI";
+val real_of_preal_less_iff1 = thm"real_of_preal_less_iff1";
+val real_of_preal_minus_less_self = thm"real_of_preal_minus_less_self";
+val real_of_preal_minus_less_zero = thm"real_of_preal_minus_less_zero";
+val real_of_preal_not_minus_gt_zero = thm"real_of_preal_not_minus_gt_zero";
+val real_of_preal_zero_less = thm"real_of_preal_zero_less";
+val real_of_preal_not_less_zero = thm"real_of_preal_not_less_zero";
+val real_minus_minus_zero_less = thm"real_minus_minus_zero_less";
+val real_of_preal_sum_zero_less = thm"real_of_preal_sum_zero_less";
+val real_of_preal_minus_less_all = thm"real_of_preal_minus_less_all";
+val real_of_preal_not_minus_gt_all = thm"real_of_preal_not_minus_gt_all";
+val real_of_preal_minus_less_rev1 = thm"real_of_preal_minus_less_rev1";
+val real_of_preal_minus_less_rev2 = thm"real_of_preal_minus_less_rev2";
+val real_of_preal_minus_less_rev_iff = thm"real_of_preal_minus_less_rev_iff";
+val real_linear = thm"real_linear";
+val real_neq_iff = thm"real_neq_iff";
+val real_linear_less2 = thm"real_linear_less2";
+val real_leI = thm"real_leI";
+val real_leD = thm"real_leD";
+val real_leE = thm"real_leE";
+val real_less_le_iff = thm"real_less_le_iff";
+val not_real_leE = thm"not_real_leE";
+val real_le_imp_less_or_eq = thm"real_le_imp_less_or_eq";
+val real_less_or_eq_imp_le = thm"real_less_or_eq_imp_le";
+val real_le_less = thm"real_le_less";
+val real_le_refl = thm"real_le_refl";
+val real_le_linear = thm"real_le_linear";
+val real_le_trans = thm"real_le_trans";
+val real_le_anti_sym = thm"real_le_anti_sym";
+val real_less_le = thm"real_less_le";
+val real_minus_zero_less_iff = thm"real_minus_zero_less_iff";
+val real_minus_zero_less_iff2 = thm"real_minus_zero_less_iff2";
+val real_less_add_positive_left_Ex = thm"real_less_add_positive_left_Ex";
+val real_less_sum_gt_zero = thm"real_less_sum_gt_zero";
+val real_lemma_change_eq_subj = thm"real_lemma_change_eq_subj";
+val real_sum_gt_zero_less = thm"real_sum_gt_zero_less";
+val real_less_sum_gt_0_iff = thm"real_less_sum_gt_0_iff";
+val real_less_eq_diff = thm"real_less_eq_diff";
+val real_add_diff_eq = thm"real_add_diff_eq";
+val real_diff_add_eq = thm"real_diff_add_eq";
+val real_diff_diff_eq = thm"real_diff_diff_eq";
+val real_diff_diff_eq2 = thm"real_diff_diff_eq2";
+val real_diff_less_eq = thm"real_diff_less_eq";
+val real_less_diff_eq = thm"real_less_diff_eq";
+val real_diff_le_eq = thm"real_diff_le_eq";
+val real_le_diff_eq = thm"real_le_diff_eq";
+val real_diff_eq_eq = thm"real_diff_eq_eq";
+val real_eq_diff_eq = thm"real_eq_diff_eq";
+val real_less_eqI = thm"real_less_eqI";
+val real_le_eqI = thm"real_le_eqI";
+val real_eq_eqI = thm"real_eq_eqI";
+
+val real_add_ac = thms"real_add_ac";
+val real_mult_ac = thms"real_mult_ac";
+val real_compare_rls = thms"real_compare_rls";
+*}
+
end
--- a/src/HOL/Real/RealInt.ML Thu Nov 27 10:47:55 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,138 +0,0 @@
-(* Title: RealInt.ML
- ID: $Id$
- Author: Jacques D. Fleuriot
- Copyright: 1999 University of Edinburgh
- Description: Embedding the integers in the reals
-*)
-
-
-Goalw [congruent_def]
- "congruent intrel (%p. (%(i,j). realrel `` \
-\ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \
-\ preal_of_prat (prat_of_pnat (pnat_of_nat j)))}) p)";
-by (auto_tac (claset(),
- simpset() addsimps [pnat_of_nat_add, prat_of_pnat_add RS sym,
- preal_of_prat_add RS sym]));
-qed "real_of_int_congruent";
-
-Goalw [real_of_int_def]
- "real (Abs_Integ (intrel `` {(i, j)})) = \
-\ Abs_REAL(realrel `` \
-\ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \
-\ preal_of_prat (prat_of_pnat (pnat_of_nat j)))})";
-by (res_inst_tac [("f","Abs_REAL")] arg_cong 1);
-by (simp_tac (simpset() addsimps [realrel_in_real RS Abs_REAL_inverse,
- [equiv_intrel, real_of_int_congruent] MRS UN_equiv_class]) 1);
-qed "real_of_int";
-
-Goal "inj(real :: int => real)";
-by (rtac injI 1);
-by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","y")] eq_Abs_Integ 1);
-by (auto_tac (claset() addSDs [inj_preal_of_prat RS injD,
- inj_prat_of_pnat RS injD, inj_pnat_of_nat RS injD],
- simpset() addsimps [real_of_int,preal_of_prat_add RS sym,
- prat_of_pnat_add RS sym,pnat_of_nat_add]));
-qed "inj_real_of_int";
-
-Goalw [int_def,real_zero_def] "real (int 0) = 0";
-by (simp_tac (simpset() addsimps [real_of_int, preal_add_commute]) 1);
-qed "real_of_int_zero";
-
-Goal "real (1::int) = (1::real)";
-by (stac (int_1 RS sym) 1);
-by (auto_tac (claset(),
- simpset() addsimps [int_def, real_one_def, real_of_int,
- preal_of_prat_add RS sym,pnat_two_eq,
- prat_of_pnat_add RS sym, pnat_one_iff RS sym]));
-qed "real_of_one";
-
-Goal "real (x::int) + real y = real (x + y)";
-by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","y")] eq_Abs_Integ 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_of_int, preal_of_prat_add RS sym,
- prat_of_pnat_add RS sym, zadd,real_add,
- pnat_of_nat_add] @ pnat_add_ac));
-qed "real_of_int_add";
-Addsimps [real_of_int_add RS sym];
-
-Goal "-real (x::int) = real (-x)";
-by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
-by (auto_tac (claset(), simpset() addsimps [real_of_int, real_minus,zminus]));
-qed "real_of_int_minus";
-Addsimps [real_of_int_minus RS sym];
-
-Goalw [zdiff_def,real_diff_def]
- "real (x::int) - real y = real (x - y)";
-by (simp_tac (HOL_ss addsimps [real_of_int_add, real_of_int_minus]) 1);
-qed "real_of_int_diff";
-Addsimps [real_of_int_diff RS sym];
-
-Goal "real (x::int) * real y = real (x * y)";
-by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","y")] eq_Abs_Integ 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_of_int, real_mult,zmult,
- preal_of_prat_mult RS sym,pnat_of_nat_mult,
- prat_of_pnat_mult RS sym,preal_of_prat_add RS sym,
- prat_of_pnat_add RS sym,pnat_of_nat_add] @
- mult_ac @ add_ac @ pnat_add_ac));
-qed "real_of_int_mult";
-Addsimps [real_of_int_mult RS sym];
-
-Goal "real (int (Suc n)) = real (int n) + (1::real)";
-by (simp_tac (simpset() addsimps [real_of_one RS sym, zadd_int] @
- zadd_ac) 1);
-qed "real_of_int_Suc";
-
-(* relating two of the embeddings *)
-Goal "real (int n) = real n";
-by (induct_tac "n" 1);
-by (ALLGOALS (simp_tac (HOL_ss addsimps [real_of_int_zero, real_of_nat_zero,
- real_of_int_Suc,real_of_nat_Suc])));
-by (Simp_tac 1);
-qed "real_of_int_real_of_nat";
-
-Goal "~neg z ==> real (nat z) = real z";
-by (asm_full_simp_tac (simpset() addsimps [not_neg_eq_ge_0, real_of_int_real_of_nat RS sym]) 1);
-qed "real_of_nat_real_of_int";
-
-Goal "(real x = 0) = (x = int 0)";
-by (auto_tac (claset() addIs [inj_real_of_int RS injD],
- HOL_ss addsimps [real_of_int_zero]));
-qed "real_of_int_zero_cancel";
-Addsimps [real_of_int_zero_cancel];
-
-Goal "real (x::int) < real y ==> x < y";
-by (rtac ccontr 1 THEN dtac (linorder_not_less RS iffD1) 1);
-by (auto_tac (claset(),
- simpset() addsimps [zle_iff_zadd, real_of_int_add RS sym,
- real_of_int_real_of_nat,
- linorder_not_le RS sym]));
-qed "real_of_int_less_cancel";
-
-Goal "(real (x::int) = real y) = (x = y)";
-by (blast_tac (claset() addSDs [inj_real_of_int RS injD]) 1);
-qed "real_of_int_inject";
-AddIffs [real_of_int_inject];
-
-Goal "x < y ==> (real (x::int) < real y)";
-by (full_simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
-by (auto_tac (claset() addSDs [real_of_int_less_cancel],
- simpset() addsimps [order_le_less]));
-qed "real_of_int_less_mono";
-
-Goal "(real (x::int) < real y) = (x < y)";
-by (blast_tac (claset() addDs [real_of_int_less_cancel]
- addIs [real_of_int_less_mono]) 1);
-qed "real_of_int_less_iff";
-AddIffs [real_of_int_less_iff];
-
-Goal "(real (x::int) <= real y) = (x <= y)";
-by (full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
-qed "real_of_int_le_iff";
-Addsimps [real_of_int_le_iff];
-
-Addsimps [real_of_one];
-
--- a/src/HOL/Real/RealInt.thy Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Real/RealInt.thy Fri Nov 28 12:09:37 2003 +0100
@@ -2,16 +2,146 @@
ID: $Id$
Author: Jacques D. Fleuriot
Copyright: 1999 University of Edinburgh
- Description: Embedding the integers in the reals
*)
-RealInt = RealOrd +
+header{*Embedding the Integers into the Reals*}
-defs
- (*overloaded*)
- real_of_int_def
+theory RealInt = RealOrd:
+
+defs (overloaded)
+ real_of_int_def:
"real z == Abs_REAL(UN (i,j): Rep_Integ z. realrel ``
{(preal_of_prat(prat_of_pnat(pnat_of_nat i)),
preal_of_prat(prat_of_pnat(pnat_of_nat j)))})"
+
+lemma real_of_int_congruent:
+ "congruent intrel (%p. (%(i,j). realrel ``
+ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)),
+ preal_of_prat (prat_of_pnat (pnat_of_nat j)))}) p)"
+apply (unfold congruent_def)
+apply (auto simp add: pnat_of_nat_add prat_of_pnat_add [symmetric] preal_of_prat_add [symmetric])
+done
+
+lemma real_of_int:
+ "real (Abs_Integ (intrel `` {(i, j)})) =
+ Abs_REAL(realrel ``
+ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)),
+ preal_of_prat (prat_of_pnat (pnat_of_nat j)))})"
+apply (unfold real_of_int_def)
+apply (rule_tac f = Abs_REAL in arg_cong)
+apply (simp add: realrel_in_real [THEN Abs_REAL_inverse]
+ UN_equiv_class [OF equiv_intrel real_of_int_congruent])
+done
+
+lemma inj_real_of_int: "inj(real :: int => real)"
+apply (rule inj_onI)
+apply (rule_tac z = x in eq_Abs_Integ)
+apply (rule_tac z = y in eq_Abs_Integ)
+apply (auto dest!: inj_preal_of_prat [THEN injD] inj_prat_of_pnat [THEN injD]
+ inj_pnat_of_nat [THEN injD]
+ simp add: real_of_int preal_of_prat_add [symmetric] prat_of_pnat_add [symmetric] pnat_of_nat_add)
+done
+
+lemma real_of_int_zero: "real (int 0) = 0"
+apply (unfold int_def real_zero_def)
+apply (simp add: real_of_int preal_add_commute)
+done
+
+lemma real_of_one: "real (1::int) = (1::real)"
+apply (subst int_1 [symmetric])
+apply (auto simp add: int_def real_one_def real_of_int preal_of_prat_add [symmetric] pnat_two_eq prat_of_pnat_add [symmetric] pnat_one_iff [symmetric])
+done
+
+lemma real_of_int_add: "real (x::int) + real y = real (x + y)"
+apply (rule_tac z = x in eq_Abs_Integ)
+apply (rule_tac z = y in eq_Abs_Integ)
+apply (auto simp add: real_of_int preal_of_prat_add [symmetric]
+ prat_of_pnat_add [symmetric] zadd real_add pnat_of_nat_add pnat_add_ac)
+done
+declare real_of_int_add [symmetric, simp]
+
+lemma real_of_int_minus: "-real (x::int) = real (-x)"
+apply (rule_tac z = x in eq_Abs_Integ)
+apply (auto simp add: real_of_int real_minus zminus)
+done
+declare real_of_int_minus [symmetric, simp]
+
+lemma real_of_int_diff:
+ "real (x::int) - real y = real (x - y)"
+apply (unfold zdiff_def real_diff_def)
+apply (simp only: real_of_int_add real_of_int_minus)
+done
+declare real_of_int_diff [symmetric, simp]
+
+lemma real_of_int_mult: "real (x::int) * real y = real (x * y)"
+apply (rule_tac z = x in eq_Abs_Integ)
+apply (rule_tac z = y in eq_Abs_Integ)
+apply (auto simp add: real_of_int real_mult zmult
+ preal_of_prat_mult [symmetric] pnat_of_nat_mult
+ prat_of_pnat_mult [symmetric] preal_of_prat_add [symmetric]
+ prat_of_pnat_add [symmetric] pnat_of_nat_add mult_ac add_ac pnat_add_ac)
+done
+declare real_of_int_mult [symmetric, simp]
+
+lemma real_of_int_Suc: "real (int (Suc n)) = real (int n) + (1::real)"
+by (simp add: real_of_one [symmetric] zadd_int zadd_ac)
+
+declare real_of_one [simp]
+
+(* relating two of the embeddings *)
+lemma real_of_int_real_of_nat: "real (int n) = real n"
+apply (induct_tac "n")
+apply (simp_all only: real_of_int_zero real_of_nat_zero real_of_int_Suc real_of_nat_Suc)
+done
+
+lemma real_of_nat_real_of_int: "~neg z ==> real (nat z) = real z"
+by (simp add: not_neg_eq_ge_0 real_of_int_real_of_nat [symmetric])
+
+lemma real_of_int_zero_cancel [simp]: "(real x = 0) = (x = int 0)"
+by (auto intro: inj_real_of_int [THEN injD]
+ simp only: real_of_int_zero)
+
+lemma real_of_int_less_cancel: "real (x::int) < real y ==> x < y"
+apply (rule ccontr, drule linorder_not_less [THEN iffD1])
+apply (auto simp add: zle_iff_zadd real_of_int_add [symmetric] real_of_int_real_of_nat linorder_not_le [symmetric])
+done
+
+lemma real_of_int_inject [iff]: "(real (x::int) = real y) = (x = y)"
+by (blast dest!: inj_real_of_int [THEN injD])
+
+lemma real_of_int_less_mono: "x < y ==> (real (x::int) < real y)"
+apply (simp add: linorder_not_le [symmetric])
+apply (auto dest!: real_of_int_less_cancel simp add: order_le_less)
+done
+
+lemma real_of_int_less_iff [iff]: "(real (x::int) < real y) = (x < y)"
+by (blast dest: real_of_int_less_cancel intro: real_of_int_less_mono)
+
+lemma real_of_int_le_iff [simp]: "(real (x::int) \<le> real y) = (x \<le> y)"
+by (simp add: linorder_not_less [symmetric])
+
+ML
+{*
+val real_of_int_congruent = thm"real_of_int_congruent";
+val real_of_int = thm"real_of_int";
+val inj_real_of_int = thm"inj_real_of_int";
+val real_of_int_zero = thm"real_of_int_zero";
+val real_of_one = thm"real_of_one";
+val real_of_int_add = thm"real_of_int_add";
+val real_of_int_minus = thm"real_of_int_minus";
+val real_of_int_diff = thm"real_of_int_diff";
+val real_of_int_mult = thm"real_of_int_mult";
+val real_of_int_Suc = thm"real_of_int_Suc";
+val real_of_int_real_of_nat = thm"real_of_int_real_of_nat";
+val real_of_nat_real_of_int = thm"real_of_nat_real_of_int";
+val real_of_int_zero_cancel = thm"real_of_int_zero_cancel";
+val real_of_int_less_cancel = thm"real_of_int_less_cancel";
+val real_of_int_inject = thm"real_of_int_inject";
+val real_of_int_less_mono = thm"real_of_int_less_mono";
+val real_of_int_less_iff = thm"real_of_int_less_iff";
+val real_of_int_le_iff = thm"real_of_int_le_iff";
+*}
+
+
end
--- a/src/HOL/Real/RealOrd.thy Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Real/RealOrd.thy Fri Nov 28 12:09:37 2003 +0100
@@ -8,20 +8,6 @@
theory RealOrd = RealDef:
-instance real :: order
- by (intro_classes,
- (assumption |
- rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+)
-
-instance real :: linorder
- by (intro_classes, rule real_le_linear)
-
-instance real :: plus_ac0
- by (intro_classes,
- (assumption |
- rule real_add_commute real_add_assoc real_add_zero_left)+)
-
-
defs (overloaded)
real_abs_def: "abs (r::real) == (if 0 \<le> r then r else -r)"
@@ -222,6 +208,110 @@
by (rule Ring_and_Field.zero_le_square)
+subsection{*Division Lemmas*}
+
+(** Inverse of zero! Useful to simplify certain equations **)
+
+lemma INVERSE_ZERO [simp]: "inverse 0 = (0::real)"
+apply (unfold real_inverse_def)
+apply (rule someI2)
+apply (auto simp add: real_zero_not_eq_one)
+done
+
+lemma DIVISION_BY_ZERO [simp]: "a / (0::real) = 0"
+by (simp add: real_divide_def INVERSE_ZERO)
+
+lemma real_mult_left_cancel: "(c::real) ~= 0 ==> (c*a=c*b) = (a=b)"
+apply auto
+done
+
+lemma real_mult_right_cancel: "(c::real) ~= 0 ==> (a*c=b*c) = (a=b)"
+apply (auto );
+done
+
+lemma real_mult_left_cancel_ccontr: "c*a ~= c*b ==> a ~= b"
+by auto
+
+lemma real_mult_right_cancel_ccontr: "a*c ~= b*c ==> a ~= b"
+by auto
+
+lemma real_inverse_not_zero: "x ~= 0 ==> inverse(x::real) ~= 0"
+ by (rule Ring_and_Field.nonzero_imp_inverse_nonzero)
+
+lemma real_mult_not_zero: "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::real)"
+apply (simp add: );
+done
+
+lemma real_inverse_inverse: "inverse(inverse (x::real)) = x"
+apply (case_tac "x=0", simp)
+apply (rule_tac c1 = "inverse x" in real_mult_right_cancel [THEN iffD1])
+apply (erule real_inverse_not_zero)
+apply (auto dest: real_inverse_not_zero)
+done
+declare real_inverse_inverse [simp]
+
+lemma real_inverse_1: "inverse((1::real)) = (1::real)"
+apply (unfold real_inverse_def)
+apply (cut_tac real_zero_not_eq_one [THEN not_sym, THEN real_mult_inv_left_ex])
+apply (auto simp add: real_zero_not_eq_one [THEN not_sym])
+done
+declare real_inverse_1 [simp]
+
+lemma real_minus_inverse: "inverse(-x) = -inverse(x::real)"
+apply (case_tac "x=0", simp)
+apply (rule_tac c1 = "-x" in real_mult_right_cancel [THEN iffD1])
+ prefer 2 apply (subst real_mult_inv_left, auto)
+done
+
+lemma real_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::real)"
+apply (case_tac "x=0", simp)
+apply (case_tac "y=0", simp)
+apply (frule_tac y = y in real_mult_not_zero, assumption)
+apply (rule_tac c1 = x in real_mult_left_cancel [THEN iffD1])
+apply (auto simp add: real_mult_assoc [symmetric])
+apply (rule_tac c1 = y in real_mult_left_cancel [THEN iffD1])
+apply (auto simp add: real_mult_left_commute)
+apply (simp add: real_mult_assoc [symmetric])
+done
+
+lemma real_times_divide1_eq: "(x::real) * (y/z) = (x*y)/z"
+by (simp add: real_divide_def real_mult_assoc)
+
+lemma real_times_divide2_eq: "(y/z) * (x::real) = (y*x)/z"
+by (simp add: real_divide_def real_mult_ac)
+
+declare real_times_divide1_eq [simp] real_times_divide2_eq [simp]
+
+lemma real_divide_divide1_eq: "(x::real) / (y/z) = (x*z)/y"
+by (simp add: real_divide_def real_inverse_distrib real_mult_ac)
+
+lemma real_divide_divide2_eq: "((x::real) / y) / z = x/(y*z)"
+by (simp add: real_divide_def real_inverse_distrib real_mult_assoc)
+
+declare real_divide_divide1_eq [simp] real_divide_divide2_eq [simp]
+
+(** As with multiplication, pull minus signs OUT of the / operator **)
+
+lemma real_minus_divide_eq: "(-x) / (y::real) = - (x/y)"
+by (simp add: real_divide_def)
+declare real_minus_divide_eq [simp]
+
+lemma real_divide_minus_eq: "(x / -(y::real)) = - (x/y)"
+by (simp add: real_divide_def real_minus_inverse)
+declare real_divide_minus_eq [simp]
+
+lemma real_add_divide_distrib: "(x+y)/(z::real) = x/z + y/z"
+by (simp add: real_divide_def real_add_mult_distrib)
+
+(*The following would e.g. convert (x+y)/2 to x/2 + y/2. Sometimes that
+ leads to cancellations in x or y, but is also prevents "multiplying out"
+ the 2 in e.g. (x+y)/2 = 5.
+
+Addsimps [inst "z" "number_of ?w" real_add_divide_distrib]
+**)
+
+
+
subsection{*An Embedding of the Naturals in the Reals*}
lemma real_of_posnat_one: "real_of_posnat 0 = (1::real)"
@@ -710,6 +800,26 @@
val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero";
val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff";
val real_of_nat_num_if = thm "real_of_nat_num_if";
+
+val INVERSE_ZERO = thm"INVERSE_ZERO";
+val DIVISION_BY_ZERO = thm"DIVISION_BY_ZERO";
+val real_mult_left_cancel = thm"real_mult_left_cancel";
+val real_mult_right_cancel = thm"real_mult_right_cancel";
+val real_mult_left_cancel_ccontr = thm"real_mult_left_cancel_ccontr";
+val real_mult_right_cancel_ccontr = thm"real_mult_right_cancel_ccontr";
+val real_inverse_not_zero = thm"real_inverse_not_zero";
+val real_mult_not_zero = thm"real_mult_not_zero";
+val real_inverse_inverse = thm"real_inverse_inverse";
+val real_inverse_1 = thm"real_inverse_1";
+val real_minus_inverse = thm"real_minus_inverse";
+val real_inverse_distrib = thm"real_inverse_distrib";
+val real_times_divide1_eq = thm"real_times_divide1_eq";
+val real_times_divide2_eq = thm"real_times_divide2_eq";
+val real_divide_divide1_eq = thm"real_divide_divide1_eq";
+val real_divide_divide2_eq = thm"real_divide_divide2_eq";
+val real_minus_divide_eq = thm"real_minus_divide_eq";
+val real_divide_minus_eq = thm"real_divide_minus_eq";
+val real_add_divide_distrib = thm"real_add_divide_distrib";
*}
end
--- a/src/HOL/Real/RealPow.thy Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Real/RealPow.thy Fri Nov 28 12:09:37 2003 +0100
@@ -6,10 +6,7 @@
*)
-theory RealPow = RealAbs:
-
-(*belongs to theory RealAbs*)
-lemmas [arith_split] = abs_split
+theory RealPow = RealArith:
instance real :: power ..
--- a/src/HOL/Ring_and_Field.thy Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Ring_and_Field.thy Fri Nov 28 12:09:37 2003 +0100
@@ -1,6 +1,7 @@
(* Title: HOL/Ring_and_Field.thy
ID: $Id$
Author: Gertrud Bauer and Markus Wenzel, TU Muenchen
+ Lawrence C Paulson, University of Cambridge
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
@@ -145,11 +146,11 @@
theorems mult_ac = mult_assoc mult_commute mult_left_commute
-lemma right_inverse [simp]: "a \<noteq> 0 ==> a * inverse (a::'a::field) = 1"
+lemma right_inverse [simp]:
+ assumes not0: "a ~= 0" shows "a * inverse (a::'a::field) = 1"
proof -
have "a * inverse a = inverse a * a" by (simp add: mult_ac)
- also assume "a \<noteq> 0"
- hence "inverse a * a = 1" by simp
+ also have "... = 1" using not0 by simp
finally show ?thesis .
qed
@@ -241,7 +242,7 @@
done
lemma le_imp_neg_le:
- assumes "a \<le> (b::'a::ordered_ring)" shows "-b \<le> -a"
+ assumes "a \<le> (b::'a::ordered_ring)" shows "-b \<le> -a"
proof -
have "-a+a \<le> -a+b"
by (rule add_left_mono)
@@ -485,9 +486,9 @@
text{*Cancellation of equalities with a common factor*}
lemma field_mult_cancel_right_lemma:
- assumes cnz: "c \<noteq> (0::'a::field)"
- and eq: "a*c = b*c"
- shows "a=b"
+ assumes cnz: "c \<noteq> (0::'a::field)"
+ and eq: "a*c = b*c"
+ shows "a=b"
proof -
have "(a * c) * inverse c = (b * c) * inverse c"
by (simp add: eq)
@@ -497,7 +498,7 @@
lemma field_mult_cancel_right:
"(a*c = b*c) = (c = (0::'a::field) | a=b)"
- proof (cases "c=0")
+ proof cases
assume "c=0" thus ?thesis by simp
next
assume "c\<noteq>0"
@@ -534,18 +535,17 @@
by (force dest: inverse_nonzero_imp_nonzero)
lemma nonzero_inverse_minus_eq:
- "a\<noteq>0 ==> inverse(-a) = -inverse(a::'a::field)";
+ assumes [simp]: "a\<noteq>0" shows "inverse(-a) = -inverse(a::'a::field)"
proof -
- assume "a\<noteq>0"
- hence "-a * inverse (- a) = -a * - inverse a"
+ have "-a * inverse (- a) = -a * - inverse a"
by simp
thus ?thesis
- by (simp only: field_mult_cancel_left, simp add: prems)
+ by (simp only: field_mult_cancel_left, simp)
qed
lemma inverse_minus_eq [simp]:
"inverse(-a) = -inverse(a::'a::{field,division_by_zero})";
- proof (cases "a=0")
+ proof cases
assume "a=0" thus ?thesis by (simp add: inverse_zero)
next
assume "a\<noteq>0"
@@ -553,10 +553,10 @@
qed
lemma nonzero_inverse_eq_imp_eq:
- assumes inveq: "inverse a = inverse b"
- and anz: "a \<noteq> 0"
- and bnz: "b \<noteq> 0"
- shows "a = (b::'a::field)"
+ assumes inveq: "inverse a = inverse b"
+ and anz: "a \<noteq> 0"
+ and bnz: "b \<noteq> 0"
+ shows "a = (b::'a::field)"
proof -
have "a * inverse b = a * inverse a"
by (simp add: inveq)
@@ -582,8 +582,7 @@
subsection {* Ordered Fields *}
lemma inverse_gt_0:
- assumes a_gt_0: "0 < a"
- shows "0 < inverse (a::'a::ordered_field)"
+ assumes a_gt_0: "0 < a" shows "0 < inverse (a::'a::ordered_field)"
proof -
have "0 < a * inverse a"
by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
@@ -597,9 +596,9 @@
simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
lemma inverse_le_imp_le:
- assumes invle: "inverse a \<le> inverse b"
- and apos: "0 < a"
- shows "b \<le> (a::'a::ordered_field)"
+ assumes invle: "inverse a \<le> inverse b"
+ and apos: "0 < a"
+ shows "b \<le> (a::'a::ordered_field)"
proof (rule classical)
assume "~ b \<le> a"
hence "a < b"
@@ -615,9 +614,9 @@
qed
lemma less_imp_inverse_less:
- assumes less: "a < b"
- and apos: "0 < a"
- shows "inverse b < inverse (a::'a::ordered_field)"
+ assumes less: "a < b"
+ and apos: "0 < a"
+ shows "inverse b < inverse (a::'a::ordered_field)"
proof (rule ccontr)
assume "~ inverse b < inverse a"
hence "inverse a \<le> inverse b"