# HG changeset patch # User paulson # Date 1070017777 -3600 # Node ID 502a7c95de73c21eba24c313bf1ed42ee1c2476b # Parent 5cf13e80be0e0b653e60f1b16de1755f23ee47e4 conversion of some Real theories to Isar scripts diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Complex/Complex.ML --- 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)); diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Hyperreal/HRealAbs.thy --- 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" diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Hyperreal/Lim.ML --- 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]))); diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Hyperreal/Lim.thy --- 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 diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Hyperreal/MacLaurin.ML --- 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"), diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Hyperreal/NthRoot.ML --- 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); diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Hyperreal/SEQ.ML --- 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); diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Hyperreal/Transcendental.ML --- 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); diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Integ/IntDef.thy --- 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" diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/IsaMakefile --- 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 \ diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Real/RealAbs.ML --- 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"; diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Real/RealAbs.thy --- 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 diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Real/RealArith.thy --- 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 diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Real/RealDef.ML --- 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 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 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 (x (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"; diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Real/RealDef.thy --- 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. \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 - "Px1 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)" syntax (xsymbols) - Reals :: "'a set" ("\\") - Nats :: "'a set" ("\\") + Reals :: "'a set" ("\") + Nats :: "'a set" ("\") + + +(*** 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: "\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: "\(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 ==> \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 ==> \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 ==> + \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). \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: "(\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: + "\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 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 \ (w::real)" + +apply (unfold real_le_def, assumption) +done + +lemma real_leD: "z\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 \ (w::real))" +by (blast intro!: real_leI real_leD) + +lemma not_real_leE: "~ z \ w ==> w<(z::real)" +by (unfold real_le_def, blast) + +lemma real_le_imp_less_or_eq: "!!(x::real). x \ 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 z \(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 \ (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 \ (w::real)" +by (simp add: real_le_less) + +lemma real_le_trans: "[| i \ j; j \ k |] ==> i \ (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 \ w; w \ 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 \ 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) \ w | w \ 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 ==> \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 z) = (x \ z + (y::real))" +apply (unfold real_le_def) +apply (simp add: real_less_diff_eq) +done + +lemma real_le_diff_eq: "(x \ z-y) = (x + (y::real) \ 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'\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 diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Real/RealInt.ML --- 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]; - diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Real/RealInt.thy --- 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) \ real y) = (x \ 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 diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Real/RealOrd.thy --- 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 \ 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 diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Real/RealPow.thy --- 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 .. diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Ring_and_Field.thy --- 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 \ 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 \ 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 \ (b::'a::ordered_ring)" shows "-b \ -a" + assumes "a \ (b::'a::ordered_ring)" shows "-b \ -a" proof - have "-a+a \ -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 \ (0::'a::field)" - and eq: "a*c = b*c" - shows "a=b" + assumes cnz: "c \ (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\0" @@ -534,18 +535,17 @@ by (force dest: inverse_nonzero_imp_nonzero) lemma nonzero_inverse_minus_eq: - "a\0 ==> inverse(-a) = -inverse(a::'a::field)"; + assumes [simp]: "a\0" shows "inverse(-a) = -inverse(a::'a::field)" proof - - assume "a\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\0" @@ -553,10 +553,10 @@ qed lemma nonzero_inverse_eq_imp_eq: - assumes inveq: "inverse a = inverse b" - and anz: "a \ 0" - and bnz: "b \ 0" - shows "a = (b::'a::field)" + assumes inveq: "inverse a = inverse b" + and anz: "a \ 0" + and bnz: "b \ 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 \ inverse b" - and apos: "0 < a" - shows "b \ (a::'a::ordered_field)" + assumes invle: "inverse a \ inverse b" + and apos: "0 < a" + shows "b \ (a::'a::ordered_field)" proof (rule classical) assume "~ b \ 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 \ inverse b"