1.1 --- a/src/HOL/Complex/Complex.ML Thu Nov 27 10:47:55 2003 +0100
1.2 +++ b/src/HOL/Complex/Complex.ML Fri Nov 28 12:09:37 2003 +0100
1.3 @@ -594,7 +594,7 @@
1.4 qed "complex_of_real_minus";
1.5
1.6 Goal "complex_of_real(inverse x) = inverse(complex_of_real x)";
1.7 -by (real_div_undefined_case_tac "x=0" 1);
1.8 +by (case_tac "x=0" 1);
1.9 by (simp_tac (simpset() addsimps [DIVISION_BY_ZERO,COMPLEX_INVERSE_ZERO]) 1);
1.10 by (auto_tac (claset(),simpset() addsimps [complex_inverse,
1.11 complex_of_real_def,realpow_num_two,real_divide_def,
1.12 @@ -616,8 +616,8 @@
1.13
1.14 Goalw [complex_divide_def]
1.15 "complex_of_real x / complex_of_real y = complex_of_real(x/y)";
1.16 -by (real_div_undefined_case_tac "y=0" 1);
1.17 -by (simp_tac (simpset() addsimps [rename_numerals DIVISION_BY_ZERO,
1.18 +by (case_tac "y=0" 1);
1.19 +by (asm_simp_tac (simpset() addsimps [rename_numerals DIVISION_BY_ZERO,
1.20 COMPLEX_INVERSE_ZERO]) 1);
1.21 by (asm_simp_tac (simpset() addsimps [complex_of_real_mult RS sym,
1.22 complex_of_real_inverse,real_divide_def]) 1);
1.23 @@ -1273,7 +1273,7 @@
1.24 Addsimps [complex_of_real_zero_iff];
1.25
1.26 Goal "y ~= 0 ==> cos (arg(ii * complex_of_real y)) = 0";
1.27 -by (cut_inst_tac [("R1.0","y"),("R2.0","0")] real_linear 1);
1.28 +by (cut_inst_tac [("x","y"),("y","0")] linorder_less_linear 1);
1.29 by Auto_tac;
1.30 qed "cos_arg_i_mult_zero3";
1.31 Addsimps [cos_arg_i_mult_zero3];
1.32 @@ -1475,8 +1475,8 @@
1.33 Addsimps [cis_inverse];
1.34
1.35 Goal "inverse(rcis r a) = rcis (1/r) (-a)";
1.36 -by (real_div_undefined_case_tac "r=0" 1);
1.37 -by (simp_tac (simpset() addsimps [rename_numerals DIVISION_BY_ZERO,
1.38 +by (case_tac "r=0" 1);
1.39 +by (asm_simp_tac (simpset() addsimps [rename_numerals DIVISION_BY_ZERO,
1.40 COMPLEX_INVERSE_ZERO]) 1);
1.41 by (auto_tac (claset(),simpset() addsimps [complex_inverse_complex_split,
1.42 complex_add_mult_distrib2,complex_of_real_mult,rcis_def,cis_def,
1.43 @@ -1491,8 +1491,8 @@
1.44
1.45 Goalw [complex_divide_def]
1.46 "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)";
1.47 -by (real_div_undefined_case_tac "r2=0" 1);
1.48 -by (simp_tac (simpset() addsimps [rename_numerals DIVISION_BY_ZERO,
1.49 +by (case_tac "r2=0" 1);
1.50 +by (asm_simp_tac (simpset() addsimps [rename_numerals DIVISION_BY_ZERO,
1.51 COMPLEX_INVERSE_ZERO]) 1);
1.52 by (auto_tac (claset(),simpset() addsimps [rcis_inverse,rcis_mult,
1.53 real_diff_def]));
1.54 @@ -1578,7 +1578,7 @@
1.55 \ ==> arg(complex_of_real r * \
1.56 \ (complex_of_real(cos a) + ii * complex_of_real(sin a))) = a";
1.57 by Auto_tac;
1.58 -by (cut_inst_tac [("R1.0","0"),("R2.0","r")] real_linear 1);
1.59 +by (cut_inst_tac [("x","0"),("y","r")] linorder_less_linear 1);
1.60 by (auto_tac (claset(),simpset() addsimps (map (full_rename_numerals thy)
1.61 [rabs_eqI2,rabs_minus_eqI2,real_minus_rinv]) @ [real_divide_def,
1.62 real_minus_mult_eq2 RS sym] @ real_mult_ac));
2.1 --- a/src/HOL/Hyperreal/HRealAbs.thy Thu Nov 27 10:47:55 2003 +0100
2.2 +++ b/src/HOL/Hyperreal/HRealAbs.thy Fri Nov 28 12:09:37 2003 +0100
2.3 @@ -4,7 +4,7 @@
2.4 Description : Absolute value function for the hyperreals
2.5 *)
2.6
2.7 -HRealAbs = HyperArith + RealAbs +
2.8 +HRealAbs = HyperArith + RealArith +
2.9
2.10 defs
2.11 hrabs_def "abs r == if (0::hypreal) <=r then r else -r"
3.1 --- a/src/HOL/Hyperreal/Lim.ML Thu Nov 27 10:47:55 2003 +0100
3.2 +++ b/src/HOL/Hyperreal/Lim.ML Fri Nov 28 12:09:37 2003 +0100
3.3 @@ -1661,7 +1661,7 @@
3.4 by (asm_full_simp_tac (simpset() addsimps []) 1);
3.5 by (dres_inst_tac [("x","s")] spec 1);
3.6 by (Clarify_tac 1);
3.7 -by (cut_inst_tac [("R1.0","f x"),("R2.0","y")] real_linear 1);
3.8 +by (cut_inst_tac [("x","f x"),("y","y")] linorder_less_linear 1);
3.9 by Safe_tac;
3.10 by (dres_inst_tac [("x","ba - x")] spec 1);
3.11 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [abs_iff])));
4.1 --- a/src/HOL/Hyperreal/Lim.thy Thu Nov 27 10:47:55 2003 +0100
4.2 +++ b/src/HOL/Hyperreal/Lim.thy Fri Nov 28 12:09:37 2003 +0100
4.3 @@ -5,7 +5,7 @@
4.4 differentiation of real=>real functions
4.5 *)
4.6
4.7 -Lim = SEQ + RealAbs +
4.8 +Lim = SEQ + RealArith +
4.9
4.10 (*-----------------------------------------------------------------------
4.11 Limits, continuity and differentiation: standard and NS definitions
5.1 --- a/src/HOL/Hyperreal/MacLaurin.ML Thu Nov 27 10:47:55 2003 +0100
5.2 +++ b/src/HOL/Hyperreal/MacLaurin.ML Fri Nov 28 12:09:37 2003 +0100
5.3 @@ -317,7 +317,7 @@
5.4 by (induct_tac "n" 1);
5.5 by (Simp_tac 1);
5.6 by Auto_tac;
5.7 -by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
5.8 +by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);
5.9 by Auto_tac;
5.10 by (cut_inst_tac [("f","diff 0"),
5.11 ("diff","diff"),
6.1 --- a/src/HOL/Hyperreal/NthRoot.ML Thu Nov 27 10:47:55 2003 +0100
6.2 +++ b/src/HOL/Hyperreal/NthRoot.ML Fri Nov 28 12:09:37 2003 +0100
6.3 @@ -160,7 +160,7 @@
6.4 (* uniqueness of nth positive root *)
6.5 Goal "[| (0::real) < a; 0 < n |] ==> EX! r. 0 < r & r ^ n = a";
6.6 by (auto_tac (claset() addSIs [realpow_pos_nth],simpset()));
6.7 -by (cut_inst_tac [("R1.0","r"),("R2.0","y")] real_linear 1);
6.8 +by (cut_inst_tac [("x","r"),("y","y")] linorder_less_linear 1);
6.9 by (Auto_tac);
6.10 by (dres_inst_tac [("x","r")] realpow_less 1);
6.11 by (dres_inst_tac [("x","y")] realpow_less 4);
7.1 --- a/src/HOL/Hyperreal/SEQ.ML Thu Nov 27 10:47:55 2003 +0100
7.2 +++ b/src/HOL/Hyperreal/SEQ.ML Fri Nov 28 12:09:37 2003 +0100
7.3 @@ -859,8 +859,8 @@
7.4 by (res_inst_tac [("x","0")] exI 1);
7.5 by (Asm_full_simp_tac 1);
7.6 by (Step_tac 1);
7.7 -by (cut_inst_tac [("R1.0","abs (X (Suc n))"),("R2.0","abs(X m)")]
7.8 - real_linear 1);
7.9 +by (cut_inst_tac [("x","abs (X (Suc n))"),("y","abs(X m)")]
7.10 + linorder_less_linear 1);
7.11 by (Step_tac 1);
7.12 by (res_inst_tac [("x","m")] exI 1);
7.13 by (res_inst_tac [("x","m")] exI 2);
7.14 @@ -919,8 +919,8 @@
7.15 by (dtac lemmaCauchy 1);
7.16 by (cut_inst_tac [("M","M"),("X","X")] SUP_rabs_subseq 1);
7.17 by (Step_tac 1);
7.18 -by (cut_inst_tac [("R1.0","abs(X m)"),
7.19 - ("R2.0","1 + abs(X M)")] real_linear 1);
7.20 +by (cut_inst_tac [("x","abs(X m)"),
7.21 + ("y","1 + abs(X M)")] linorder_less_linear 1);
7.22 by (Step_tac 1);
7.23 by (dtac lemma_trans1 1 THEN assume_tac 1);
7.24 by (dtac lemma_trans2 3 THEN assume_tac 3);
8.1 --- a/src/HOL/Hyperreal/Transcendental.ML Thu Nov 27 10:47:55 2003 +0100
8.2 +++ b/src/HOL/Hyperreal/Transcendental.ML Fri Nov 28 12:09:37 2003 +0100
8.3 @@ -146,7 +146,7 @@
8.4 Goal "(~ (0::real) < x*x) = (x = 0)";
8.5 by Auto_tac;
8.6 by (rtac ccontr 1);
8.7 -by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
8.8 +by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);
8.9 by Auto_tac;
8.10 by (ftac (real_mult_order) 2);
8.11 by (asm_full_simp_tac (simpset() addsimps [real_0_less_mult_iff]) 1);
8.12 @@ -1675,7 +1675,7 @@
8.13 by (subgoal_tac "EX x. 0 <= x & x <= 2 & cos x = 0" 1);
8.14 by (rtac IVT2 2);
8.15 by (auto_tac (claset() addIs [DERIV_isCont,DERIV_cos],simpset ()));
8.16 -by (cut_inst_tac [("R1.0","xa"),("R2.0","y")] real_linear 1);
8.17 +by (cut_inst_tac [("x","xa"),("y","y")] linorder_less_linear 1);
8.18 by (rtac ccontr 1);
8.19 by (subgoal_tac "(ALL x. cos differentiable x) & \
8.20 \ (ALL x. isCont cos x)" 1);
8.21 @@ -1898,7 +1898,7 @@
8.22 by (rtac IVT2 2);
8.23 by (auto_tac (claset() addIs [order_less_imp_le,DERIV_isCont,DERIV_cos],
8.24 simpset ()));
8.25 -by (cut_inst_tac [("R1.0","xa"),("R2.0","y")] real_linear 1);
8.26 +by (cut_inst_tac [("x","xa"),("y","y")] linorder_less_linear 1);
8.27 by (rtac ccontr 1 THEN Auto_tac);
8.28 by (dres_inst_tac [("f","cos")] Rolle 1);
8.29 by (dres_inst_tac [("f","cos")] Rolle 5);
8.30 @@ -2171,7 +2171,7 @@
8.31 Goal "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y";
8.32 by (cut_inst_tac [("y","y")] lemma_tan_total1 1);
8.33 by (Auto_tac);
8.34 -by (cut_inst_tac [("R1.0","xa"),("R2.0","y")] real_linear 1);
8.35 +by (cut_inst_tac [("x","xa"),("y","y")] linorder_less_linear 1);
8.36 by (Auto_tac);
8.37 by (subgoal_tac "EX z. xa < z & z < y & DERIV tan z :> 0" 1);
8.38 by (subgoal_tac "EX z. y < z & z < xa & DERIV tan z :> 0" 3);
8.39 @@ -2628,7 +2628,7 @@
8.40 Addsimps [real_sqrt_sos_eq_one_iff];
8.41
8.42 Goalw [real_divide_def] "(((r::real) * a) / (r * r)) = a / r";
8.43 -by (real_div_undefined_case_tac "r=0" 1);
8.44 +by (case_tac "r=0" 1);
8.45 by (auto_tac (claset(),simpset() addsimps [real_inverse_distrib] @ real_mult_ac));
8.46 qed "real_divide_square_eq";
8.47 Addsimps [real_divide_square_eq];
8.48 @@ -2675,7 +2675,7 @@
8.49 qed "real_sqrt_sum_squares_gt_zero2";
8.50
8.51 Goal "x ~= 0 ==> 0 < sqrt(x ^ 2 + y ^ 2)";
8.52 -by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
8.53 +by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);
8.54 by (auto_tac (claset() addIs [real_sqrt_sum_squares_gt_zero2,
8.55 real_sqrt_sum_squares_gt_zero1],simpset() addsimps [realpow_num_two]));
8.56 qed "real_sqrt_sum_squares_gt_zero3";
8.57 @@ -2741,7 +2741,7 @@
8.58 (* was qed "lemma_real_mult_self_rinv_sqrt_squared5" *)
8.59
8.60 Goal "-(1::real)<= x / sqrt (x * x + y * y)";
8.61 -by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
8.62 +by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);
8.63 by (Step_tac 1);
8.64 by (rtac lemma_real_divide_sqrt_ge_minus_one2 1);
8.65 by (rtac lemma_real_divide_sqrt_ge_minus_one 3);
8.66 @@ -2757,7 +2757,7 @@
8.67 simplify (simpset()) cos_x_y_ge_minus_one1a];
8.68
8.69 Goal "x / sqrt (x * x + y * y) <= 1";
8.70 -by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
8.71 +by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);
8.72 by (Step_tac 1);
8.73 by (rtac lemma_real_divide_sqrt_le_one 1);
8.74 by (rtac lemma_real_divide_sqrt_le_one2 3);
8.75 @@ -2778,7 +2778,7 @@
8.76 Addsimps [[cos_x_y_ge_minus_one1a,cos_x_y_le_one2] MRS arcos_bounded];
8.77
8.78 Goal "-(1::real) <= abs(x) / sqrt (x * x + y * y)";
8.79 -by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
8.80 +by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);
8.81 by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2,abs_eqI2]));
8.82 by (dtac lemma_real_divide_sqrt_ge_minus_one 1 THEN Force_tac 1);
8.83 qed "cos_rabs_x_y_ge_minus_one";
8.84 @@ -2787,7 +2787,7 @@
8.85 simplify (simpset()) cos_rabs_x_y_ge_minus_one];
8.86
8.87 Goal "abs(x) / sqrt (x * x + y * y) <= 1";
8.88 -by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
8.89 +by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);
8.90 by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2,abs_eqI2]));
8.91 by (dtac lemma_real_divide_sqrt_ge_minus_one2 1 THEN Force_tac 1);
8.92 qed "cos_rabs_x_y_le_one";
8.93 @@ -2952,7 +2952,7 @@
8.94 qed "real_sum_squares_cancel2a";
8.95
8.96 Goal "[| x ~= 0; y < 0 |] ==> EX r a. x = r * cos a & y = r * sin a";
8.97 -by (cut_inst_tac [("R1.0","0"),("R2.0","x")] real_linear 1);
8.98 +by (cut_inst_tac [("x","0"),("y","x")] linorder_less_linear 1);
8.99 by Auto_tac;
8.100 by (res_inst_tac [("x","sqrt(x ^ 2 + y ^ 2)")] exI 1);
8.101 by (res_inst_tac [("x","arcsin(y / sqrt (x * x + y * y))")] exI 1);
8.102 @@ -2982,7 +2982,7 @@
8.103 by Auto_tac;
8.104 by (res_inst_tac [("x","y")] exI 1);
8.105 by (res_inst_tac [("x","pi/2")] exI 1 THEN Auto_tac);
8.106 -by (cut_inst_tac [("R1.0","0"),("R2.0","y")] real_linear 1);
8.107 +by (cut_inst_tac [("x","0"),("y","y")] linorder_less_linear 1);
8.108 by Auto_tac;
8.109 by (res_inst_tac [("x","x")] exI 2);
8.110 by (res_inst_tac [("x","0")] exI 2 THEN Auto_tac);
8.111 @@ -3176,7 +3176,7 @@
8.112
8.113 Goal "[| f -- c --> l; l ~= 0 |] \
8.114 \ ==> EX r. 0 < r & (ALL x. x ~= c & abs (c - x) < r --> f x ~= 0)";
8.115 -by (cut_inst_tac [("R1.0","l"),("R2.0","0")] real_linear 1);
8.116 +by (cut_inst_tac [("x","l"),("y","0")] linorder_less_linear 1);
8.117 by Auto_tac;
8.118 by (dtac LIM_fun_less_zero 1);
8.119 by (dtac LIM_fun_gt_zero 3);
9.1 --- a/src/HOL/Integ/IntDef.thy Thu Nov 27 10:47:55 2003 +0100
9.2 +++ b/src/HOL/Integ/IntDef.thy Fri Nov 28 12:09:37 2003 +0100
9.3 @@ -38,7 +38,7 @@
9.4 iszero :: "int => bool"
9.5 "iszero z == z = (0::int)"
9.6
9.7 -defs (*of overloaded constants*)
9.8 +defs (overloaded)
9.9
9.10 Zero_int_def: "0 == int 0"
9.11 One_int_def: "1 == int 1"
10.1 --- a/src/HOL/IsaMakefile Thu Nov 27 10:47:55 2003 +0100
10.2 +++ b/src/HOL/IsaMakefile Fri Nov 28 12:09:37 2003 +0100
10.3 @@ -141,10 +141,10 @@
10.4 Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \
10.5 Real/PRat.ML Real/PRat.thy \
10.6 Real/PReal.ML Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \
10.7 - Real/ROOT.ML Real/Real.thy Real/RealAbs.ML Real/RealAbs.thy \
10.8 + Real/ROOT.ML Real/Real.thy \
10.9 Real/RealArith0.ML Real/RealArith0.thy Real/real_arith0.ML \
10.10 Real/RealArith.thy Real/real_arith.ML Real/RealBin.ML \
10.11 - Real/RealBin.thy Real/RealDef.ML Real/RealDef.thy Real/RealInt.ML \
10.12 + Real/RealBin.thy Real/RealDef.thy \
10.13 Real/RealInt.thy Real/RealOrd.thy \
10.14 Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
10.15 Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \
11.1 --- a/src/HOL/Real/RealAbs.ML Thu Nov 27 10:47:55 2003 +0100
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,264 +0,0 @@
11.4 -(* Title : RealAbs.ML
11.5 - ID : $Id$
11.6 - Author : Jacques D. Fleuriot
11.7 - Copyright : 1998 University of Cambridge
11.8 - Description : Absolute value function for the reals
11.9 -*)
11.10 -
11.11 -
11.12 -(** abs (absolute value) **)
11.13 -
11.14 -Goalw [real_abs_def]
11.15 - "abs (number_of v :: real) = \
11.16 -\ (if neg (number_of v) then number_of (bin_minus v) \
11.17 -\ else number_of v)";
11.18 -by (simp_tac
11.19 - (simpset () addsimps
11.20 - bin_arith_simps@
11.21 - [minus_real_number_of, le_real_number_of_eq_not_less,
11.22 - less_real_number_of, real_of_int_le_iff]) 1);
11.23 -qed "abs_nat_number_of";
11.24 -
11.25 -Addsimps [abs_nat_number_of];
11.26 -
11.27 -Goalw [real_abs_def]
11.28 - "P(abs (x::real)) = ((0 <= x --> P x) & (x < 0 --> P(-x)))";
11.29 -by Auto_tac;
11.30 -qed "abs_split";
11.31 -
11.32 -
11.33 -(*----------------------------------------------------------------------------
11.34 - Properties of the absolute value function over the reals
11.35 - (adapted version of previously proved theorems about abs)
11.36 - ----------------------------------------------------------------------------*)
11.37 -
11.38 -Goalw [real_abs_def] "abs (r::real) = (if 0<=r then r else -r)";
11.39 -by Auto_tac;
11.40 -qed "abs_iff";
11.41 -
11.42 -Goalw [real_abs_def] "abs 0 = (0::real)";
11.43 -by Auto_tac;
11.44 -qed "abs_zero";
11.45 -Addsimps [abs_zero];
11.46 -
11.47 -Goalw [real_abs_def] "abs (1::real) = 1";
11.48 -by (Simp_tac 1);
11.49 -qed "abs_one";
11.50 -Addsimps [abs_one];
11.51 -
11.52 -Goalw [real_abs_def] "(0::real)<=x ==> abs x = x";
11.53 -by (Asm_simp_tac 1);
11.54 -qed "abs_eqI1";
11.55 -
11.56 -Goalw [real_abs_def] "(0::real) < x ==> abs x = x";
11.57 -by (Asm_simp_tac 1);
11.58 -qed "abs_eqI2";
11.59 -
11.60 -Goalw [real_abs_def,real_le_def] "x < (0::real) ==> abs x = -x";
11.61 -by (Asm_simp_tac 1);
11.62 -qed "abs_minus_eqI2";
11.63 -
11.64 -Goalw [real_abs_def] "x<=(0::real) ==> abs x = -x";
11.65 -by (Asm_simp_tac 1);
11.66 -qed "abs_minus_eqI1";
11.67 -
11.68 -Goalw [real_abs_def] "(0::real)<= abs x";
11.69 -by (Simp_tac 1);
11.70 -qed "abs_ge_zero";
11.71 -Addsimps [abs_ge_zero];
11.72 -
11.73 -Goalw [real_abs_def] "abs(abs x)=abs (x::real)";
11.74 -by (Simp_tac 1);
11.75 -qed "abs_idempotent";
11.76 -Addsimps [abs_idempotent];
11.77 -
11.78 -Goalw [real_abs_def] "(abs x = 0) = (x=(0::real))";
11.79 -by (Full_simp_tac 1);
11.80 -qed "abs_zero_iff";
11.81 -AddIffs [abs_zero_iff];
11.82 -
11.83 -Goalw [real_abs_def] "x<=abs (x::real)";
11.84 -by (Simp_tac 1);
11.85 -qed "abs_ge_self";
11.86 -
11.87 -Goalw [real_abs_def] "-x<=abs (x::real)";
11.88 -by (Simp_tac 1);
11.89 -qed "abs_ge_minus_self";
11.90 -
11.91 -Goalw [real_abs_def] "abs (x * y) = abs x * abs (y::real)";
11.92 -by (auto_tac (claset() addSDs [order_antisym],
11.93 - simpset() addsimps [real_0_le_mult_iff]));
11.94 -qed "abs_mult";
11.95 -
11.96 -Goalw [real_abs_def] "abs(inverse(x::real)) = inverse(abs(x))";
11.97 -by (real_div_undefined_case_tac "x=0" 1);
11.98 -by (auto_tac (claset(),
11.99 - simpset() addsimps [real_minus_inverse, real_le_less,
11.100 - INVERSE_ZERO, real_inverse_gt_0]));
11.101 -qed "abs_inverse";
11.102 -
11.103 -Goal "abs (x * inverse y) = (abs x) * inverse (abs (y::real))";
11.104 -by (asm_simp_tac (simpset() addsimps [abs_mult, abs_inverse]) 1);
11.105 -qed "abs_mult_inverse";
11.106 -
11.107 -Goalw [real_abs_def] "abs(x+y) <= abs x + abs (y::real)";
11.108 -by (Simp_tac 1);
11.109 -qed "abs_triangle_ineq";
11.110 -
11.111 -(*Unused, but perhaps interesting as an example*)
11.112 -Goal "abs(w + x + y + z) <= abs(w) + abs(x) + abs(y) + abs(z::real)";
11.113 -by (simp_tac (simpset() addsimps [abs_triangle_ineq RS order_trans]) 1);
11.114 -qed "abs_triangle_ineq_four";
11.115 -
11.116 -Goalw [real_abs_def] "abs(-x)=abs(x::real)";
11.117 -by (Simp_tac 1);
11.118 -qed "abs_minus_cancel";
11.119 -Addsimps [abs_minus_cancel];
11.120 -
11.121 -Goalw [real_abs_def] "abs(x + (-y)) = abs (y + (-(x::real)))";
11.122 -by (Simp_tac 1);
11.123 -qed "abs_minus_add_cancel";
11.124 -
11.125 -Goalw [real_abs_def] "abs(x + (-y)) <= abs x + abs (y::real)";
11.126 -by (Simp_tac 1);
11.127 -qed "abs_triangle_minus_ineq";
11.128 -
11.129 -Goalw [real_abs_def] "abs x < r --> abs y < s --> abs(x+y) < r+(s::real)";
11.130 -by (Simp_tac 1);
11.131 -qed_spec_mp "abs_add_less";
11.132 -
11.133 -Goalw [real_abs_def] "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)";
11.134 -by (Simp_tac 1);
11.135 -qed "abs_add_minus_less";
11.136 -
11.137 -(* lemmas manipulating terms *)
11.138 -Goal "((0::real)*x < r)=(0 < r)";
11.139 -by (Simp_tac 1);
11.140 -qed "real_mult_0_less";
11.141 -
11.142 -Goal "[| (0::real) < y; x < r; y*r < t*s |] ==> y*x < t*s";
11.143 -by (blast_tac (claset() addSIs [real_mult_less_mono2]
11.144 - addIs [order_less_trans]) 1);
11.145 -qed "real_mult_less_trans";
11.146 -
11.147 -Goal "[| (0::real)<=y; x < r; y*r < t*s; 0 < t*s|] ==> y*x < t*s";
11.148 -by (dtac order_le_imp_less_or_eq 1);
11.149 -by (fast_tac (HOL_cs addEs [real_mult_0_less RS iffD2,
11.150 - real_mult_less_trans]) 1);
11.151 -qed "real_mult_le_less_trans";
11.152 -
11.153 -Goal "[| abs x < r; abs y < s |] ==> abs(x*y) < r*(s::real)";
11.154 -by (simp_tac (simpset() addsimps [abs_mult]) 1);
11.155 -by (rtac real_mult_le_less_trans 1);
11.156 -by (rtac abs_ge_zero 1);
11.157 -by (assume_tac 1);
11.158 -by (rtac real_mult_order 2);
11.159 -by (auto_tac (claset() addSIs [real_mult_less_mono1, abs_ge_zero]
11.160 - addIs [order_le_less_trans],
11.161 - simpset()));
11.162 -qed "abs_mult_less";
11.163 -
11.164 -Goal "[| abs x < r; abs y < s |] ==> abs(x)*abs(y) < r*(s::real)";
11.165 -by (auto_tac (claset() addIs [abs_mult_less],
11.166 - simpset() addsimps [abs_mult RS sym]));
11.167 -qed "abs_mult_less2";
11.168 -
11.169 -Goal "abs(x) < r ==> (0::real) < r";
11.170 -by (blast_tac (claset() addSIs [order_le_less_trans,abs_ge_zero]) 1);
11.171 -qed "abs_less_gt_zero";
11.172 -
11.173 -Goalw [real_abs_def] "abs (-1) = (1::real)";
11.174 -by (Simp_tac 1);
11.175 -qed "abs_minus_one";
11.176 -Addsimps [abs_minus_one];
11.177 -
11.178 -Goalw [real_abs_def] "abs x =x | abs x = -(x::real)";
11.179 -by Auto_tac;
11.180 -qed "abs_disj";
11.181 -
11.182 -Goalw [real_abs_def] "(abs x < r) = (-r < x & x < (r::real))";
11.183 -by Auto_tac;
11.184 -qed "abs_interval_iff";
11.185 -
11.186 -Goalw [real_abs_def] "(abs x <= r) = (-r<=x & x<=(r::real))";
11.187 -by Auto_tac;
11.188 -qed "abs_le_interval_iff";
11.189 -
11.190 -Goalw [real_abs_def] "(0::real) < k ==> 0 < k + abs(x)";
11.191 -by Auto_tac;
11.192 -qed "abs_add_pos_gt_zero";
11.193 -
11.194 -Goalw [real_abs_def] "(0::real) < 1 + abs(x)";
11.195 -by Auto_tac;
11.196 -qed "abs_add_one_gt_zero";
11.197 -Addsimps [abs_add_one_gt_zero];
11.198 -
11.199 -Goalw [real_abs_def] "~ abs x < (0::real)";
11.200 -by Auto_tac;
11.201 -qed "abs_not_less_zero";
11.202 -Addsimps [abs_not_less_zero];
11.203 -
11.204 -Goal "abs h < abs y - abs x ==> abs (x + h) < abs (y::real)";
11.205 -by (auto_tac (claset() addIs [abs_triangle_ineq RS order_le_less_trans],
11.206 - simpset()));
11.207 -qed "abs_circle";
11.208 -
11.209 -Goalw [real_abs_def] "(abs x <= (0::real)) = (x = 0)";
11.210 -by Auto_tac;
11.211 -qed "abs_le_zero_iff";
11.212 -Addsimps [abs_le_zero_iff];
11.213 -
11.214 -Goal "((0::real) < abs x) = (x ~= 0)";
11.215 -by (simp_tac (simpset() addsimps [real_abs_def]) 1);
11.216 -by (arith_tac 1);
11.217 -qed "real_0_less_abs_iff";
11.218 -Addsimps [real_0_less_abs_iff];
11.219 -
11.220 -Goal "abs (real x) = real (x::nat)";
11.221 -by (auto_tac (claset() addIs [abs_eqI1],
11.222 - simpset() addsimps [real_of_nat_ge_zero]));
11.223 -qed "abs_real_of_nat_cancel";
11.224 -Addsimps [abs_real_of_nat_cancel];
11.225 -
11.226 -Goal "~ abs(x) + (1::real) < x";
11.227 -by (rtac real_leD 1);
11.228 -by (auto_tac (claset() addIs [abs_ge_self RS order_trans], simpset()));
11.229 -qed "abs_add_one_not_less_self";
11.230 -Addsimps [abs_add_one_not_less_self];
11.231 -
11.232 -(* used in vector theory *)
11.233 -Goal "abs(w + x + (y::real)) <= abs(w) + abs(x) + abs(y)";
11.234 -by (auto_tac (claset() addSIs [abs_triangle_ineq RS order_trans,
11.235 - real_add_left_le_mono1],
11.236 - simpset() addsimps [real_add_assoc]));
11.237 -qed "abs_triangle_ineq_three";
11.238 -
11.239 -Goalw [real_abs_def] "abs(x - y) < y ==> (0::real) < y";
11.240 -by (case_tac "0 <= x - y" 1);
11.241 -by Auto_tac;
11.242 -qed "abs_diff_less_imp_gt_zero";
11.243 -
11.244 -Goalw [real_abs_def] "abs(x - y) < x ==> (0::real) < x";
11.245 -by (case_tac "0 <= x - y" 1);
11.246 -by Auto_tac;
11.247 -qed "abs_diff_less_imp_gt_zero2";
11.248 -
11.249 -Goal "abs(x - y) < y ==> (0::real) < x";
11.250 -by (auto_tac (claset(),simpset() addsimps [abs_interval_iff]));
11.251 -qed "abs_diff_less_imp_gt_zero3";
11.252 -
11.253 -Goal "abs(x - y) < -y ==> x < (0::real)";
11.254 -by (auto_tac (claset(),simpset() addsimps [abs_interval_iff]));
11.255 -qed "abs_diff_less_imp_gt_zero4";
11.256 -
11.257 -Goalw [real_abs_def]
11.258 - "abs(x) <= abs(x + (-y)) + abs((y::real))";
11.259 -by Auto_tac;
11.260 -qed "abs_triangle_ineq_minus_cancel";
11.261 -
11.262 -Goal "abs ((x::real) + y + (-l + -m)) <= abs(x + -l) + abs(y + -m)";
11.263 -by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
11.264 -by (res_inst_tac [("x1","y")] (real_add_left_commute RS ssubst) 1);
11.265 -by (rtac (real_add_assoc RS subst) 1);
11.266 -by (rtac abs_triangle_ineq 1);
11.267 -qed "abs_sum_triangle_ineq";
12.1 --- a/src/HOL/Real/RealAbs.thy Thu Nov 27 10:47:55 2003 +0100
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,8 +0,0 @@
12.4 -(* Title : RealAbs.thy
12.5 - ID : $Id$
12.6 - Author : Jacques D. Fleuriot
12.7 - Copyright : 1998 University of Cambridge
12.8 - Description : Absolute value function for the reals
12.9 -*)
12.10 -
12.11 -RealAbs = RealArith
13.1 --- a/src/HOL/Real/RealArith.thy Thu Nov 27 10:47:55 2003 +0100
13.2 +++ b/src/HOL/Real/RealArith.thy Fri Nov 28 12:09:37 2003 +0100
13.3 @@ -3,4 +3,265 @@
13.4
13.5 setup real_arith_setup
13.6
13.7 +subsection{*Absolute Value Function for the Reals*}
13.8 +
13.9 +(** abs (absolute value) **)
13.10 +
13.11 +lemma abs_nat_number_of:
13.12 + "abs (number_of v :: real) =
13.13 + (if neg (number_of v) then number_of (bin_minus v)
13.14 + else number_of v)"
13.15 +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)
13.16 +done
13.17 +
13.18 +declare abs_nat_number_of [simp]
13.19 +
13.20 +lemma abs_split [arith_split]:
13.21 + "P(abs (x::real)) = ((0 <= x --> P x) & (x < 0 --> P(-x)))"
13.22 +apply (unfold real_abs_def, auto)
13.23 +done
13.24 +
13.25 +
13.26 +(*----------------------------------------------------------------------------
13.27 + Properties of the absolute value function over the reals
13.28 + (adapted version of previously proved theorems about abs)
13.29 + ----------------------------------------------------------------------------*)
13.30 +
13.31 +lemma abs_iff: "abs (r::real) = (if 0<=r then r else -r)"
13.32 +apply (unfold real_abs_def, auto)
13.33 +done
13.34 +
13.35 +lemma abs_zero: "abs 0 = (0::real)"
13.36 +by (unfold real_abs_def, auto)
13.37 +declare abs_zero [simp]
13.38 +
13.39 +lemma abs_one: "abs (1::real) = 1"
13.40 +by (unfold real_abs_def, simp)
13.41 +declare abs_one [simp]
13.42 +
13.43 +lemma abs_eqI1: "(0::real)<=x ==> abs x = x"
13.44 +by (unfold real_abs_def, simp)
13.45 +
13.46 +lemma abs_eqI2: "(0::real) < x ==> abs x = x"
13.47 +by (unfold real_abs_def, simp)
13.48 +
13.49 +lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x"
13.50 +by (unfold real_abs_def real_le_def, simp)
13.51 +
13.52 +lemma abs_minus_eqI1: "x<=(0::real) ==> abs x = -x"
13.53 +by (unfold real_abs_def, simp)
13.54 +
13.55 +lemma abs_ge_zero: "(0::real)<= abs x"
13.56 +by (unfold real_abs_def, simp)
13.57 +declare abs_ge_zero [simp]
13.58 +
13.59 +lemma abs_idempotent: "abs(abs x)=abs (x::real)"
13.60 +by (unfold real_abs_def, simp)
13.61 +declare abs_idempotent [simp]
13.62 +
13.63 +lemma abs_zero_iff: "(abs x = 0) = (x=(0::real))"
13.64 +by (unfold real_abs_def, simp)
13.65 +declare abs_zero_iff [iff]
13.66 +
13.67 +lemma abs_ge_self: "x<=abs (x::real)"
13.68 +by (unfold real_abs_def, simp)
13.69 +
13.70 +lemma abs_ge_minus_self: "-x<=abs (x::real)"
13.71 +by (unfold real_abs_def, simp)
13.72 +
13.73 +lemma abs_mult: "abs (x * y) = abs x * abs (y::real)"
13.74 +apply (unfold real_abs_def)
13.75 +apply (auto dest!: order_antisym simp add: real_0_le_mult_iff)
13.76 +done
13.77 +
13.78 +lemma abs_inverse: "abs(inverse(x::real)) = inverse(abs(x))"
13.79 +apply (unfold real_abs_def)
13.80 +apply (case_tac "x=0")
13.81 +apply (auto simp add: real_minus_inverse real_le_less INVERSE_ZERO real_inverse_gt_0)
13.82 +done
13.83 +
13.84 +lemma abs_mult_inverse: "abs (x * inverse y) = (abs x) * inverse (abs (y::real))"
13.85 +by (simp add: abs_mult abs_inverse)
13.86 +
13.87 +lemma abs_triangle_ineq: "abs(x+y) <= abs x + abs (y::real)"
13.88 +by (unfold real_abs_def, simp)
13.89 +
13.90 +(*Unused, but perhaps interesting as an example*)
13.91 +lemma abs_triangle_ineq_four: "abs(w + x + y + z) <= abs(w) + abs(x) + abs(y) + abs(z::real)"
13.92 +by (simp add: abs_triangle_ineq [THEN order_trans])
13.93 +
13.94 +lemma abs_minus_cancel: "abs(-x)=abs(x::real)"
13.95 +by (unfold real_abs_def, simp)
13.96 +declare abs_minus_cancel [simp]
13.97 +
13.98 +lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
13.99 +by (unfold real_abs_def, simp)
13.100 +
13.101 +lemma abs_triangle_minus_ineq: "abs(x + (-y)) <= abs x + abs (y::real)"
13.102 +by (unfold real_abs_def, simp)
13.103 +
13.104 +lemma abs_add_less [rule_format (no_asm)]: "abs x < r --> abs y < s --> abs(x+y) < r+(s::real)"
13.105 +by (unfold real_abs_def, simp)
13.106 +
13.107 +lemma abs_add_minus_less: "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)"
13.108 +by (unfold real_abs_def, simp)
13.109 +
13.110 +(* lemmas manipulating terms *)
13.111 +lemma real_mult_0_less: "((0::real)*x < r)=(0 < r)"
13.112 +by simp
13.113 +
13.114 +lemma real_mult_less_trans: "[| (0::real) < y; x < r; y*r < t*s |] ==> y*x < t*s"
13.115 +by (blast intro!: real_mult_less_mono2 intro: order_less_trans)
13.116 +
13.117 +(*USED ONLY IN NEXT THM*)
13.118 +lemma real_mult_le_less_trans:
13.119 + "[| (0::real)<=y; x < r; y*r < t*s; 0 < t*s|] ==> y*x < t*s"
13.120 +apply (drule order_le_imp_less_or_eq)
13.121 +apply (fast elim: real_mult_0_less [THEN iffD2] real_mult_less_trans)
13.122 +done
13.123 +
13.124 +lemma abs_mult_less: "[| abs x < r; abs y < s |] ==> abs(x*y) < r*(s::real)"
13.125 +apply (simp add: abs_mult)
13.126 +apply (rule real_mult_le_less_trans)
13.127 +apply (rule abs_ge_zero, assumption)
13.128 +apply (rule_tac [2] real_mult_order)
13.129 +apply (auto intro!: real_mult_less_mono1 abs_ge_zero intro: order_le_less_trans)
13.130 +done
13.131 +
13.132 +lemma abs_mult_less2: "[| abs x < r; abs y < s |] ==> abs(x)*abs(y) < r*(s::real)"
13.133 +by (auto intro: abs_mult_less simp add: abs_mult [symmetric])
13.134 +
13.135 +lemma abs_less_gt_zero: "abs(x) < r ==> (0::real) < r"
13.136 +by (blast intro!: order_le_less_trans abs_ge_zero)
13.137 +
13.138 +lemma abs_minus_one: "abs (-1) = (1::real)"
13.139 +by (unfold real_abs_def, simp)
13.140 +declare abs_minus_one [simp]
13.141 +
13.142 +lemma abs_disj: "abs x =x | abs x = -(x::real)"
13.143 +by (unfold real_abs_def, auto)
13.144 +
13.145 +lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))"
13.146 +by (unfold real_abs_def, auto)
13.147 +
13.148 +lemma abs_le_interval_iff: "(abs x <= r) = (-r<=x & x<=(r::real))"
13.149 +by (unfold real_abs_def, auto)
13.150 +
13.151 +lemma abs_add_pos_gt_zero: "(0::real) < k ==> 0 < k + abs(x)"
13.152 +by (unfold real_abs_def, auto)
13.153 +
13.154 +lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)"
13.155 +by (unfold real_abs_def, auto)
13.156 +declare abs_add_one_gt_zero [simp]
13.157 +
13.158 +lemma abs_not_less_zero: "~ abs x < (0::real)"
13.159 +by (unfold real_abs_def, auto)
13.160 +declare abs_not_less_zero [simp]
13.161 +
13.162 +lemma abs_circle: "abs h < abs y - abs x ==> abs (x + h) < abs (y::real)"
13.163 +by (auto intro: abs_triangle_ineq [THEN order_le_less_trans])
13.164 +
13.165 +lemma abs_le_zero_iff: "(abs x <= (0::real)) = (x = 0)"
13.166 +by (unfold real_abs_def, auto)
13.167 +declare abs_le_zero_iff [simp]
13.168 +
13.169 +lemma real_0_less_abs_iff: "((0::real) < abs x) = (x ~= 0)"
13.170 +by (simp add: real_abs_def, arith)
13.171 +declare real_0_less_abs_iff [simp]
13.172 +
13.173 +lemma abs_real_of_nat_cancel: "abs (real x) = real (x::nat)"
13.174 +by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero)
13.175 +declare abs_real_of_nat_cancel [simp]
13.176 +
13.177 +lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x"
13.178 +apply (rule real_leD)
13.179 +apply (auto intro: abs_ge_self [THEN order_trans])
13.180 +done
13.181 +declare abs_add_one_not_less_self [simp]
13.182 +
13.183 +(* used in vector theory *)
13.184 +lemma abs_triangle_ineq_three: "abs(w + x + (y::real)) <= abs(w) + abs(x) + abs(y)"
13.185 +by (auto intro!: abs_triangle_ineq [THEN order_trans] real_add_left_le_mono1 simp add: real_add_assoc)
13.186 +
13.187 +lemma abs_diff_less_imp_gt_zero: "abs(x - y) < y ==> (0::real) < y"
13.188 +apply (unfold real_abs_def)
13.189 +apply (case_tac "0 <= x - y", auto)
13.190 +done
13.191 +
13.192 +lemma abs_diff_less_imp_gt_zero2: "abs(x - y) < x ==> (0::real) < x"
13.193 +apply (unfold real_abs_def)
13.194 +apply (case_tac "0 <= x - y", auto)
13.195 +done
13.196 +
13.197 +lemma abs_diff_less_imp_gt_zero3: "abs(x - y) < y ==> (0::real) < x"
13.198 +by (auto simp add: abs_interval_iff)
13.199 +
13.200 +lemma abs_diff_less_imp_gt_zero4: "abs(x - y) < -y ==> x < (0::real)"
13.201 +by (auto simp add: abs_interval_iff)
13.202 +
13.203 +lemma abs_triangle_ineq_minus_cancel:
13.204 + "abs(x) <= abs(x + (-y)) + abs((y::real))"
13.205 +apply (unfold real_abs_def, auto)
13.206 +done
13.207 +
13.208 +lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) <= abs(x + -l) + abs(y + -m)"
13.209 +apply (simp add: real_add_assoc)
13.210 +apply (rule_tac x1 = y in real_add_left_commute [THEN ssubst])
13.211 +apply (rule real_add_assoc [THEN subst])
13.212 +apply (rule abs_triangle_ineq)
13.213 +done
13.214 +
13.215 +ML
13.216 +{*
13.217 +val abs_nat_number_of = thm"abs_nat_number_of";
13.218 +val abs_split = thm"abs_split";
13.219 +val abs_iff = thm"abs_iff";
13.220 +val abs_zero = thm"abs_zero";
13.221 +val abs_one = thm"abs_one";
13.222 +val abs_eqI1 = thm"abs_eqI1";
13.223 +val abs_eqI2 = thm"abs_eqI2";
13.224 +val abs_minus_eqI2 = thm"abs_minus_eqI2";
13.225 +val abs_minus_eqI1 = thm"abs_minus_eqI1";
13.226 +val abs_ge_zero = thm"abs_ge_zero";
13.227 +val abs_idempotent = thm"abs_idempotent";
13.228 +val abs_zero_iff = thm"abs_zero_iff";
13.229 +val abs_ge_self = thm"abs_ge_self";
13.230 +val abs_ge_minus_self = thm"abs_ge_minus_self";
13.231 +val abs_mult = thm"abs_mult";
13.232 +val abs_inverse = thm"abs_inverse";
13.233 +val abs_mult_inverse = thm"abs_mult_inverse";
13.234 +val abs_triangle_ineq = thm"abs_triangle_ineq";
13.235 +val abs_triangle_ineq_four = thm"abs_triangle_ineq_four";
13.236 +val abs_minus_cancel = thm"abs_minus_cancel";
13.237 +val abs_minus_add_cancel = thm"abs_minus_add_cancel";
13.238 +val abs_triangle_minus_ineq = thm"abs_triangle_minus_ineq";
13.239 +val abs_add_less = thm"abs_add_less";
13.240 +val abs_add_minus_less = thm"abs_add_minus_less";
13.241 +val real_mult_0_less = thm"real_mult_0_less";
13.242 +val real_mult_less_trans = thm"real_mult_less_trans";
13.243 +val real_mult_le_less_trans = thm"real_mult_le_less_trans";
13.244 +val abs_mult_less = thm"abs_mult_less";
13.245 +val abs_mult_less2 = thm"abs_mult_less2";
13.246 +val abs_less_gt_zero = thm"abs_less_gt_zero";
13.247 +val abs_minus_one = thm"abs_minus_one";
13.248 +val abs_disj = thm"abs_disj";
13.249 +val abs_interval_iff = thm"abs_interval_iff";
13.250 +val abs_le_interval_iff = thm"abs_le_interval_iff";
13.251 +val abs_add_pos_gt_zero = thm"abs_add_pos_gt_zero";
13.252 +val abs_add_one_gt_zero = thm"abs_add_one_gt_zero";
13.253 +val abs_not_less_zero = thm"abs_not_less_zero";
13.254 +val abs_circle = thm"abs_circle";
13.255 +val abs_le_zero_iff = thm"abs_le_zero_iff";
13.256 +val real_0_less_abs_iff = thm"real_0_less_abs_iff";
13.257 +val abs_real_of_nat_cancel = thm"abs_real_of_nat_cancel";
13.258 +val abs_add_one_not_less_self = thm"abs_add_one_not_less_self";
13.259 +val abs_triangle_ineq_three = thm"abs_triangle_ineq_three";
13.260 +val abs_diff_less_imp_gt_zero = thm"abs_diff_less_imp_gt_zero";
13.261 +val abs_diff_less_imp_gt_zero2 = thm"abs_diff_less_imp_gt_zero2";
13.262 +val abs_diff_less_imp_gt_zero3 = thm"abs_diff_less_imp_gt_zero3";
13.263 +val abs_diff_less_imp_gt_zero4 = thm"abs_diff_less_imp_gt_zero4";
13.264 +val abs_triangle_ineq_minus_cancel = thm"abs_triangle_ineq_minus_cancel";
13.265 +val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq";
13.266 +*}
13.267 +
13.268 end
14.1 --- a/src/HOL/Real/RealDef.ML Thu Nov 27 10:47:55 2003 +0100
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,1130 +0,0 @@
14.4 -(* Title : Real/RealDef.ML
14.5 - ID : $Id$
14.6 - Author : Jacques D. Fleuriot
14.7 - Copyright : 1998 University of Cambridge
14.8 - Description : The reals
14.9 -*)
14.10 -
14.11 -(*** Proving that realrel is an equivalence relation ***)
14.12 -
14.13 -Goal "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \
14.14 -\ ==> x1 + y3 = x3 + y1";
14.15 -by (res_inst_tac [("C","y2")] preal_add_right_cancel 1);
14.16 -by (rotate_tac 1 1 THEN dtac sym 1);
14.17 -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
14.18 -by (rtac (preal_add_left_commute RS subst) 1);
14.19 -by (res_inst_tac [("x1","x1")] (preal_add_assoc RS subst) 1);
14.20 -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
14.21 -qed "preal_trans_lemma";
14.22 -
14.23 -(** Natural deduction for realrel **)
14.24 -
14.25 -Goalw [realrel_def]
14.26 - "(((x1,y1),(x2,y2)): realrel) = (x1 + y2 = x2 + y1)";
14.27 -by (Blast_tac 1);
14.28 -qed "realrel_iff";
14.29 -
14.30 -Goalw [realrel_def]
14.31 - "[| x1 + y2 = x2 + y1 |] ==> ((x1,y1),(x2,y2)): realrel";
14.32 -by (Blast_tac 1);
14.33 -qed "realrelI";
14.34 -
14.35 -Goalw [realrel_def]
14.36 - "p: realrel --> (EX x1 y1 x2 y2. \
14.37 -\ p = ((x1,y1),(x2,y2)) & x1 + y2 = x2 + y1)";
14.38 -by (Blast_tac 1);
14.39 -qed "realrelE_lemma";
14.40 -
14.41 -val [major,minor] = Goal
14.42 - "[| p: realrel; \
14.43 -\ !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2)); x1+y2 = x2+y1 \
14.44 -\ |] ==> Q |] ==> Q";
14.45 -by (cut_facts_tac [major RS (realrelE_lemma RS mp)] 1);
14.46 -by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
14.47 -qed "realrelE";
14.48 -
14.49 -Goal "(x,x): realrel";
14.50 -by (case_tac "x" 1);
14.51 -by (asm_simp_tac (simpset() addsimps [realrel_def]) 1);
14.52 -qed "realrel_refl";
14.53 -
14.54 -Goalw [equiv_def, refl_def, sym_def, trans_def] "equiv UNIV realrel";
14.55 -by (fast_tac (claset() addSIs [realrelI, realrel_refl]
14.56 - addSEs [sym, realrelE, preal_trans_lemma]) 1);
14.57 -qed "equiv_realrel";
14.58 -
14.59 -(* (realrel `` {x} = realrel `` {y}) = ((x,y) : realrel) *)
14.60 -bind_thm ("equiv_realrel_iff",
14.61 - [equiv_realrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
14.62 -
14.63 -Goalw [REAL_def,realrel_def,quotient_def] "realrel``{(x,y)}: REAL";
14.64 -by (Blast_tac 1);
14.65 -qed "realrel_in_real";
14.66 -
14.67 -Goal "inj_on Abs_REAL REAL";
14.68 -by (rtac inj_on_inverseI 1);
14.69 -by (etac Abs_REAL_inverse 1);
14.70 -qed "inj_on_Abs_REAL";
14.71 -
14.72 -Addsimps [equiv_realrel_iff,inj_on_Abs_REAL RS inj_on_iff,
14.73 - realrel_iff, realrel_in_real, Abs_REAL_inverse];
14.74 -
14.75 -Addsimps [equiv_realrel RS eq_equiv_class_iff];
14.76 -bind_thm ("eq_realrelD", equiv_realrel RSN (2,eq_equiv_class));
14.77 -
14.78 -Goal "inj Rep_REAL";
14.79 -by (rtac inj_inverseI 1);
14.80 -by (rtac Rep_REAL_inverse 1);
14.81 -qed "inj_Rep_REAL";
14.82 -
14.83 -(** real_of_preal: the injection from preal to real **)
14.84 -Goal "inj(real_of_preal)";
14.85 -by (rtac injI 1);
14.86 -by (rewtac real_of_preal_def);
14.87 -by (dtac (inj_on_Abs_REAL RS inj_onD) 1);
14.88 -by (REPEAT (rtac realrel_in_real 1));
14.89 -by (dtac eq_equiv_class 1);
14.90 -by (rtac equiv_realrel 1);
14.91 -by (Blast_tac 1);
14.92 -by (asm_full_simp_tac (simpset() addsimps [realrel_def]) 1);
14.93 -qed "inj_real_of_preal";
14.94 -
14.95 -val [prem] = Goal
14.96 - "(!!x y. z = Abs_REAL(realrel``{(x,y)}) ==> P) ==> P";
14.97 -by (res_inst_tac [("x1","z")]
14.98 - (rewrite_rule [REAL_def] Rep_REAL RS quotientE) 1);
14.99 -by (dres_inst_tac [("f","Abs_REAL")] arg_cong 1);
14.100 -by (case_tac "x" 1);
14.101 -by (rtac prem 1);
14.102 -by (asm_full_simp_tac (simpset() addsimps [Rep_REAL_inverse]) 1);
14.103 -qed "eq_Abs_REAL";
14.104 -
14.105 -(**** real_minus: additive inverse on real ****)
14.106 -
14.107 -Goalw [congruent_def]
14.108 - "congruent realrel (%p. (%(x,y). realrel``{(y,x)}) p)";
14.109 -by (Clarify_tac 1);
14.110 -by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1);
14.111 -qed "real_minus_congruent";
14.112 -
14.113 -Goalw [real_minus_def]
14.114 - "- (Abs_REAL(realrel``{(x,y)})) = Abs_REAL(realrel `` {(y,x)})";
14.115 -by (res_inst_tac [("f","Abs_REAL")] arg_cong 1);
14.116 -by (simp_tac (simpset() addsimps [realrel_in_real RS Abs_REAL_inverse,
14.117 - [equiv_realrel, real_minus_congruent] MRS UN_equiv_class]) 1);
14.118 -qed "real_minus";
14.119 -
14.120 -Goal "- (- z) = (z::real)";
14.121 -by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
14.122 -by (asm_simp_tac (simpset() addsimps [real_minus]) 1);
14.123 -qed "real_minus_minus";
14.124 -
14.125 -Addsimps [real_minus_minus];
14.126 -
14.127 -Goal "inj(%r::real. -r)";
14.128 -by (rtac injI 1);
14.129 -by (dres_inst_tac [("f","uminus")] arg_cong 1);
14.130 -by (asm_full_simp_tac (simpset() addsimps [real_minus_minus]) 1);
14.131 -qed "inj_real_minus";
14.132 -
14.133 -Goalw [real_zero_def] "- 0 = (0::real)";
14.134 -by (simp_tac (simpset() addsimps [real_minus]) 1);
14.135 -qed "real_minus_zero";
14.136 -
14.137 -Addsimps [real_minus_zero];
14.138 -
14.139 -Goal "(-x = 0) = (x = (0::real))";
14.140 -by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
14.141 -by (auto_tac (claset(),
14.142 - simpset() addsimps [real_zero_def, real_minus] @ preal_add_ac));
14.143 -qed "real_minus_zero_iff";
14.144 -
14.145 -Addsimps [real_minus_zero_iff];
14.146 -
14.147 -(*** Congruence property for addition ***)
14.148 -Goalw [congruent2_def]
14.149 - "congruent2 realrel (%p1 p2. \
14.150 -\ (%(x1,y1). (%(x2,y2). realrel``{(x1+x2, y1+y2)}) p2) p1)";
14.151 -by (clarify_tac (claset() addSEs [realrelE]) 1);
14.152 -by (asm_simp_tac (simpset() addsimps [preal_add_assoc]) 1);
14.153 -by (res_inst_tac [("z1.1","x1a")] (preal_add_left_commute RS ssubst) 1);
14.154 -by (asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
14.155 -by (asm_simp_tac (simpset() addsimps preal_add_ac) 1);
14.156 -qed "real_add_congruent2";
14.157 -
14.158 -Goalw [real_add_def]
14.159 - "Abs_REAL(realrel``{(x1,y1)}) + Abs_REAL(realrel``{(x2,y2)}) = \
14.160 -\ Abs_REAL(realrel``{(x1+x2, y1+y2)})";
14.161 -by (simp_tac (simpset() addsimps
14.162 - [[equiv_realrel, real_add_congruent2] MRS UN_equiv_class2]) 1);
14.163 -qed "real_add";
14.164 -
14.165 -Goal "(z::real) + w = w + z";
14.166 -by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
14.167 -by (res_inst_tac [("z","w")] eq_Abs_REAL 1);
14.168 -by (asm_simp_tac (simpset() addsimps preal_add_ac @ [real_add]) 1);
14.169 -qed "real_add_commute";
14.170 -
14.171 -Goal "((z1::real) + z2) + z3 = z1 + (z2 + z3)";
14.172 -by (res_inst_tac [("z","z1")] eq_Abs_REAL 1);
14.173 -by (res_inst_tac [("z","z2")] eq_Abs_REAL 1);
14.174 -by (res_inst_tac [("z","z3")] eq_Abs_REAL 1);
14.175 -by (asm_simp_tac (simpset() addsimps [real_add, preal_add_assoc]) 1);
14.176 -qed "real_add_assoc";
14.177 -
14.178 -(*For AC rewriting*)
14.179 -Goal "(x::real)+(y+z)=y+(x+z)";
14.180 -by(rtac ([real_add_assoc,real_add_commute] MRS
14.181 - read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
14.182 -qed "real_add_left_commute";
14.183 -
14.184 -(* real addition is an AC operator *)
14.185 -bind_thms ("real_add_ac", [real_add_assoc,real_add_commute,real_add_left_commute]);
14.186 -
14.187 -Goalw [real_of_preal_def,real_zero_def] "(0::real) + z = z";
14.188 -by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
14.189 -by (asm_full_simp_tac (simpset() addsimps [real_add] @ preal_add_ac) 1);
14.190 -qed "real_add_zero_left";
14.191 -Addsimps [real_add_zero_left];
14.192 -
14.193 -Goal "z + (0::real) = z";
14.194 -by (simp_tac (simpset() addsimps [real_add_commute]) 1);
14.195 -qed "real_add_zero_right";
14.196 -Addsimps [real_add_zero_right];
14.197 -
14.198 -Goalw [real_zero_def] "z + (-z) = (0::real)";
14.199 -by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
14.200 -by (asm_full_simp_tac (simpset() addsimps [real_minus,
14.201 - real_add, preal_add_commute]) 1);
14.202 -qed "real_add_minus";
14.203 -Addsimps [real_add_minus];
14.204 -
14.205 -Goal "(-z) + z = (0::real)";
14.206 -by (simp_tac (simpset() addsimps [real_add_commute]) 1);
14.207 -qed "real_add_minus_left";
14.208 -Addsimps [real_add_minus_left];
14.209 -
14.210 -
14.211 -Goal "z + ((- z) + w) = (w::real)";
14.212 -by (simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
14.213 -qed "real_add_minus_cancel";
14.214 -
14.215 -Goal "(-z) + (z + w) = (w::real)";
14.216 -by (simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
14.217 -qed "real_minus_add_cancel";
14.218 -
14.219 -Addsimps [real_add_minus_cancel, real_minus_add_cancel];
14.220 -
14.221 -Goal "EX y. (x::real) + y = 0";
14.222 -by (blast_tac (claset() addIs [real_add_minus]) 1);
14.223 -qed "real_minus_ex";
14.224 -
14.225 -Goal "EX! y. (x::real) + y = 0";
14.226 -by (auto_tac (claset() addIs [real_add_minus],simpset()));
14.227 -by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
14.228 -by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
14.229 -by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
14.230 -qed "real_minus_ex1";
14.231 -
14.232 -Goal "EX! y. y + (x::real) = 0";
14.233 -by (auto_tac (claset() addIs [real_add_minus_left],simpset()));
14.234 -by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
14.235 -by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
14.236 -by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
14.237 -qed "real_minus_left_ex1";
14.238 -
14.239 -Goal "x + y = (0::real) ==> x = -y";
14.240 -by (cut_inst_tac [("z","y")] real_add_minus_left 1);
14.241 -by (res_inst_tac [("x1","y")] (real_minus_left_ex1 RS ex1E) 1);
14.242 -by (Blast_tac 1);
14.243 -qed "real_add_minus_eq_minus";
14.244 -
14.245 -Goal "EX (y::real). x = -y";
14.246 -by (cut_inst_tac [("x","x")] real_minus_ex 1);
14.247 -by (etac exE 1 THEN dtac real_add_minus_eq_minus 1);
14.248 -by (Fast_tac 1);
14.249 -qed "real_as_add_inverse_ex";
14.250 -
14.251 -Goal "-(x + y) = (-x) + (- y :: real)";
14.252 -by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
14.253 -by (res_inst_tac [("z","y")] eq_Abs_REAL 1);
14.254 -by (auto_tac (claset(),simpset() addsimps [real_minus,real_add]));
14.255 -qed "real_minus_add_distrib";
14.256 -
14.257 -Addsimps [real_minus_add_distrib];
14.258 -
14.259 -Goal "((x::real) + y = x + z) = (y = z)";
14.260 -by (Step_tac 1);
14.261 -by (dres_inst_tac [("f","%t. (-x) + t")] arg_cong 1);
14.262 -by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
14.263 -qed "real_add_left_cancel";
14.264 -
14.265 -Goal "(y + (x::real)= z + x) = (y = z)";
14.266 -by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1);
14.267 -qed "real_add_right_cancel";
14.268 -
14.269 -Goal "(0::real) - x = -x";
14.270 -by (simp_tac (simpset() addsimps [real_diff_def]) 1);
14.271 -qed "real_diff_0";
14.272 -
14.273 -Goal "x - (0::real) = x";
14.274 -by (simp_tac (simpset() addsimps [real_diff_def]) 1);
14.275 -qed "real_diff_0_right";
14.276 -
14.277 -Goal "x - x = (0::real)";
14.278 -by (simp_tac (simpset() addsimps [real_diff_def]) 1);
14.279 -qed "real_diff_self";
14.280 -
14.281 -Addsimps [real_diff_0, real_diff_0_right, real_diff_self];
14.282 -
14.283 -
14.284 -(*** Congruence property for multiplication ***)
14.285 -
14.286 -Goal "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==> \
14.287 -\ x * x1 + y * y1 + (x * y2 + x2 * y) = \
14.288 -\ x * x2 + y * y2 + (x * y1 + x1 * y)";
14.289 -by (asm_full_simp_tac (simpset() addsimps [preal_add_left_commute,
14.290 - preal_add_assoc RS sym,preal_add_mult_distrib2 RS sym]) 1);
14.291 -by (rtac (preal_mult_commute RS subst) 1);
14.292 -by (res_inst_tac [("y1","x2")] (preal_mult_commute RS subst) 1);
14.293 -by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc,
14.294 - preal_add_mult_distrib2 RS sym]) 1);
14.295 -by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1);
14.296 -qed "real_mult_congruent2_lemma";
14.297 -
14.298 -Goal
14.299 - "congruent2 realrel (%p1 p2. \
14.300 -\ (%(x1,y1). (%(x2,y2). realrel``{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)";
14.301 -by (rtac (equiv_realrel RS congruent2_commuteI) 1);
14.302 -by (Clarify_tac 1);
14.303 -by (rewtac split_def);
14.304 -by (asm_simp_tac (simpset() addsimps [preal_mult_commute,preal_add_commute]) 1);
14.305 -by (auto_tac (claset(),simpset() addsimps [real_mult_congruent2_lemma]));
14.306 -qed "real_mult_congruent2";
14.307 -
14.308 -Goalw [real_mult_def]
14.309 - "Abs_REAL((realrel``{(x1,y1)})) * Abs_REAL((realrel``{(x2,y2)})) = \
14.310 -\ Abs_REAL(realrel `` {(x1*x2+y1*y2,x1*y2+x2*y1)})";
14.311 -by (simp_tac (simpset() addsimps
14.312 - [[equiv_realrel, real_mult_congruent2] MRS UN_equiv_class2]) 1);
14.313 -qed "real_mult";
14.314 -
14.315 -Goal "(z::real) * w = w * z";
14.316 -by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
14.317 -by (res_inst_tac [("z","w")] eq_Abs_REAL 1);
14.318 -by (asm_simp_tac
14.319 - (simpset() addsimps [real_mult] @ preal_add_ac @ preal_mult_ac) 1);
14.320 -qed "real_mult_commute";
14.321 -
14.322 -Goal "((z1::real) * z2) * z3 = z1 * (z2 * z3)";
14.323 -by (res_inst_tac [("z","z1")] eq_Abs_REAL 1);
14.324 -by (res_inst_tac [("z","z2")] eq_Abs_REAL 1);
14.325 -by (res_inst_tac [("z","z3")] eq_Abs_REAL 1);
14.326 -by (asm_simp_tac (simpset() addsimps [preal_add_mult_distrib2,real_mult] @
14.327 - preal_add_ac @ preal_mult_ac) 1);
14.328 -qed "real_mult_assoc";
14.329 -
14.330 -Goal "(z1::real) * (z2 * z3) = z2 * (z1 * z3)";
14.331 -by(rtac ([real_mult_assoc,real_mult_commute] MRS
14.332 - read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
14.333 -qed "real_mult_left_commute";
14.334 -
14.335 -(* real multiplication is an AC operator *)
14.336 -bind_thms ("real_mult_ac",
14.337 - [real_mult_assoc, real_mult_commute, real_mult_left_commute]);
14.338 -
14.339 -Goalw [real_one_def,pnat_one_def] "(1::real) * z = z";
14.340 -by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
14.341 -by (asm_full_simp_tac
14.342 - (simpset() addsimps [real_mult,
14.343 - preal_add_mult_distrib2,preal_mult_1_right]
14.344 - @ preal_mult_ac @ preal_add_ac) 1);
14.345 -qed "real_mult_1";
14.346 -
14.347 -Addsimps [real_mult_1];
14.348 -
14.349 -Goal "z * (1::real) = z";
14.350 -by (simp_tac (simpset() addsimps [real_mult_commute]) 1);
14.351 -qed "real_mult_1_right";
14.352 -
14.353 -Addsimps [real_mult_1_right];
14.354 -
14.355 -Goalw [real_zero_def,pnat_one_def] "0 * z = (0::real)";
14.356 -by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
14.357 -by (asm_full_simp_tac (simpset() addsimps [real_mult,
14.358 - preal_add_mult_distrib2,preal_mult_1_right]
14.359 - @ preal_mult_ac @ preal_add_ac) 1);
14.360 -qed "real_mult_0";
14.361 -
14.362 -Goal "z * 0 = (0::real)";
14.363 -by (simp_tac (simpset() addsimps [real_mult_commute, real_mult_0]) 1);
14.364 -qed "real_mult_0_right";
14.365 -
14.366 -Addsimps [real_mult_0_right, real_mult_0];
14.367 -
14.368 -Goal "(-x) * (y::real) = -(x * y)";
14.369 -by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
14.370 -by (res_inst_tac [("z","y")] eq_Abs_REAL 1);
14.371 -by (auto_tac (claset(),
14.372 - simpset() addsimps [real_minus,real_mult]
14.373 - @ preal_mult_ac @ preal_add_ac));
14.374 -qed "real_mult_minus_eq1";
14.375 -Addsimps [real_mult_minus_eq1];
14.376 -
14.377 -bind_thm("real_minus_mult_eq1", real_mult_minus_eq1 RS sym);
14.378 -
14.379 -Goal "x * (- y :: real) = -(x * y)";
14.380 -by (simp_tac (simpset() addsimps [inst "z" "x" real_mult_commute]) 1);
14.381 -qed "real_mult_minus_eq2";
14.382 -Addsimps [real_mult_minus_eq2];
14.383 -
14.384 -bind_thm("real_minus_mult_eq2", real_mult_minus_eq2 RS sym);
14.385 -
14.386 -Goal "(- (1::real)) * z = -z";
14.387 -by (Simp_tac 1);
14.388 -qed "real_mult_minus_1";
14.389 -Addsimps [real_mult_minus_1];
14.390 -
14.391 -Goal "z * (- (1::real)) = -z";
14.392 -by (stac real_mult_commute 1);
14.393 -by (Simp_tac 1);
14.394 -qed "real_mult_minus_1_right";
14.395 -Addsimps [real_mult_minus_1_right];
14.396 -
14.397 -Goal "(-x) * (-y) = x * (y::real)";
14.398 -by (Simp_tac 1);
14.399 -qed "real_minus_mult_cancel";
14.400 -
14.401 -Addsimps [real_minus_mult_cancel];
14.402 -
14.403 -Goal "(-x) * y = x * (- y :: real)";
14.404 -by (Simp_tac 1);
14.405 -qed "real_minus_mult_commute";
14.406 -
14.407 -(** Lemmas **)
14.408 -
14.409 -Goal "(z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
14.410 -by (asm_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
14.411 -qed "real_add_assoc_cong";
14.412 -
14.413 -Goal "(z::real) + (v + w) = v + (z + w)";
14.414 -by (REPEAT (ares_tac [real_add_commute RS real_add_assoc_cong] 1));
14.415 -qed "real_add_assoc_swap";
14.416 -
14.417 -Goal "((z1::real) + z2) * w = (z1 * w) + (z2 * w)";
14.418 -by (res_inst_tac [("z","z1")] eq_Abs_REAL 1);
14.419 -by (res_inst_tac [("z","z2")] eq_Abs_REAL 1);
14.420 -by (res_inst_tac [("z","w")] eq_Abs_REAL 1);
14.421 -by (asm_simp_tac
14.422 - (simpset() addsimps [preal_add_mult_distrib2, real_add, real_mult] @
14.423 - preal_add_ac @ preal_mult_ac) 1);
14.424 -qed "real_add_mult_distrib";
14.425 -
14.426 -val real_mult_commute'= inst "z" "w" real_mult_commute;
14.427 -
14.428 -Goal "(w::real) * (z1 + z2) = (w * z1) + (w * z2)";
14.429 -by (simp_tac (simpset() addsimps [real_mult_commute',
14.430 - real_add_mult_distrib]) 1);
14.431 -qed "real_add_mult_distrib2";
14.432 -
14.433 -Goalw [real_diff_def] "((z1::real) - z2) * w = (z1 * w) - (z2 * w)";
14.434 -by (simp_tac (simpset() addsimps [real_add_mult_distrib]) 1);
14.435 -qed "real_diff_mult_distrib";
14.436 -
14.437 -Goal "(w::real) * (z1 - z2) = (w * z1) - (w * z2)";
14.438 -by (simp_tac (simpset() addsimps [real_mult_commute',
14.439 - real_diff_mult_distrib]) 1);
14.440 -qed "real_diff_mult_distrib2";
14.441 -
14.442 -(*** one and zero are distinct ***)
14.443 -Goalw [real_zero_def,real_one_def] "0 ~= (1::real)";
14.444 -by (auto_tac (claset(),
14.445 - simpset() addsimps [preal_self_less_add_left RS preal_not_refl2]));
14.446 -qed "real_zero_not_eq_one";
14.447 -
14.448 -(*** existence of inverse ***)
14.449 -(** lemma -- alternative definition of 0 **)
14.450 -Goalw [real_zero_def] "0 = Abs_REAL (realrel `` {(x, x)})";
14.451 -by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
14.452 -qed "real_zero_iff";
14.453 -
14.454 -Goalw [real_zero_def,real_one_def]
14.455 - "!!(x::real). x ~= 0 ==> EX y. x*y = (1::real)";
14.456 -by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
14.457 -by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1);
14.458 -by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
14.459 - simpset() addsimps [real_zero_iff RS sym]));
14.460 -by (res_inst_tac [("x",
14.461 - "Abs_REAL (realrel `` \
14.462 -\ {(preal_of_prat(prat_of_pnat 1), \
14.463 -\ pinv(D) + preal_of_prat(prat_of_pnat 1))})")] exI 1);
14.464 -by (res_inst_tac [("x",
14.465 - "Abs_REAL (realrel `` \
14.466 -\ {(pinv(D) + preal_of_prat(prat_of_pnat 1),\
14.467 -\ preal_of_prat(prat_of_pnat 1))})")] exI 2);
14.468 -by (auto_tac (claset(),
14.469 - simpset() addsimps [real_mult,
14.470 - pnat_one_def,preal_mult_1_right,preal_add_mult_distrib2,
14.471 - preal_add_mult_distrib,preal_mult_1,preal_mult_inv_right]
14.472 - @ preal_add_ac @ preal_mult_ac));
14.473 -qed "real_mult_inv_right_ex";
14.474 -
14.475 -Goal "x ~= 0 ==> EX y. y*x = (1::real)";
14.476 -by (dtac real_mult_inv_right_ex 1);
14.477 -by (auto_tac (claset(), simpset() addsimps [real_mult_commute]));
14.478 -qed "real_mult_inv_left_ex";
14.479 -
14.480 -Goalw [real_inverse_def] "x ~= 0 ==> inverse(x)*x = (1::real)";
14.481 -by (ftac real_mult_inv_left_ex 1);
14.482 -by (Step_tac 1);
14.483 -by (rtac someI2 1);
14.484 -by Auto_tac;
14.485 -qed "real_mult_inv_left";
14.486 -Addsimps [real_mult_inv_left];
14.487 -
14.488 -Goal "x ~= 0 ==> x*inverse(x) = (1::real)";
14.489 -by (stac real_mult_commute 1);
14.490 -by (auto_tac (claset(), simpset() addsimps [real_mult_inv_left]));
14.491 -qed "real_mult_inv_right";
14.492 -Addsimps [real_mult_inv_right];
14.493 -
14.494 -(** Inverse of zero! Useful to simplify certain equations **)
14.495 -
14.496 -Goalw [real_inverse_def] "inverse 0 = (0::real)";
14.497 -by (rtac someI2 1);
14.498 -by (auto_tac (claset(), simpset() addsimps [real_zero_not_eq_one]));
14.499 -qed "INVERSE_ZERO";
14.500 -
14.501 -Goal "a / (0::real) = 0";
14.502 -by (simp_tac (simpset() addsimps [real_divide_def, INVERSE_ZERO]) 1);
14.503 -qed "DIVISION_BY_ZERO";
14.504 -
14.505 -fun real_div_undefined_case_tac s i =
14.506 - case_tac s i THEN
14.507 - asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO, INVERSE_ZERO]) i;
14.508 -
14.509 -
14.510 -Goal "(c::real) ~= 0 ==> (c*a=c*b) = (a=b)";
14.511 -by Auto_tac;
14.512 -by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1);
14.513 -by (asm_full_simp_tac (simpset() addsimps real_mult_ac) 1);
14.514 -qed "real_mult_left_cancel";
14.515 -
14.516 -Goal "(c::real) ~= 0 ==> (a*c=b*c) = (a=b)";
14.517 -by (Step_tac 1);
14.518 -by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1);
14.519 -by (asm_full_simp_tac (simpset() addsimps real_mult_ac) 1);
14.520 -qed "real_mult_right_cancel";
14.521 -
14.522 -Goal "c*a ~= c*b ==> a ~= b";
14.523 -by Auto_tac;
14.524 -qed "real_mult_left_cancel_ccontr";
14.525 -
14.526 -Goal "a*c ~= b*c ==> a ~= b";
14.527 -by Auto_tac;
14.528 -qed "real_mult_right_cancel_ccontr";
14.529 -
14.530 -Goalw [real_inverse_def] "x ~= 0 ==> inverse(x::real) ~= 0";
14.531 -by (ftac real_mult_inv_left_ex 1);
14.532 -by (etac exE 1);
14.533 -by (rtac someI2 1);
14.534 -by (auto_tac (claset(),
14.535 - simpset() addsimps [real_mult_0, real_zero_not_eq_one]));
14.536 -qed "real_inverse_not_zero";
14.537 -
14.538 -Goal "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::real)";
14.539 -by (Step_tac 1);
14.540 -by (dres_inst_tac [("f","%z. inverse x*z")] arg_cong 1);
14.541 -by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
14.542 -qed "real_mult_not_zero";
14.543 -
14.544 -Goal "inverse(inverse (x::real)) = x";
14.545 -by (real_div_undefined_case_tac "x=0" 1);
14.546 -by (res_inst_tac [("c1","inverse x")] (real_mult_right_cancel RS iffD1) 1);
14.547 -by (etac real_inverse_not_zero 1);
14.548 -by (auto_tac (claset() addDs [real_inverse_not_zero],simpset()));
14.549 -qed "real_inverse_inverse";
14.550 -Addsimps [real_inverse_inverse];
14.551 -
14.552 -Goalw [real_inverse_def] "inverse((1::real)) = (1::real)";
14.553 -by (cut_facts_tac [real_zero_not_eq_one RS
14.554 - not_sym RS real_mult_inv_left_ex] 1);
14.555 -by (auto_tac (claset(),
14.556 - simpset() addsimps [real_zero_not_eq_one RS not_sym]));
14.557 -qed "real_inverse_1";
14.558 -Addsimps [real_inverse_1];
14.559 -
14.560 -Goal "inverse(-x) = -inverse(x::real)";
14.561 -by (real_div_undefined_case_tac "x=0" 1);
14.562 -by (res_inst_tac [("c1","-x")] (real_mult_right_cancel RS iffD1) 1);
14.563 -by (stac real_mult_inv_left 2);
14.564 -by Auto_tac;
14.565 -qed "real_minus_inverse";
14.566 -
14.567 -Goal "inverse(x*y) = inverse(x)*inverse(y::real)";
14.568 -by (real_div_undefined_case_tac "x=0" 1);
14.569 -by (real_div_undefined_case_tac "y=0" 1);
14.570 -by (forw_inst_tac [("y","y")] real_mult_not_zero 1 THEN assume_tac 1);
14.571 -by (res_inst_tac [("c1","x")] (real_mult_left_cancel RS iffD1) 1);
14.572 -by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym]));
14.573 -by (res_inst_tac [("c1","y")] (real_mult_left_cancel RS iffD1) 1);
14.574 -by (auto_tac (claset(),simpset() addsimps [real_mult_left_commute]));
14.575 -by (asm_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
14.576 -qed "real_inverse_distrib";
14.577 -
14.578 -Goal "(x::real) * (y/z) = (x*y)/z";
14.579 -by (simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 1);
14.580 -qed "real_times_divide1_eq";
14.581 -
14.582 -Goal "(y/z) * (x::real) = (y*x)/z";
14.583 -by (simp_tac (simpset() addsimps [real_divide_def]@real_mult_ac) 1);
14.584 -qed "real_times_divide2_eq";
14.585 -
14.586 -Addsimps [real_times_divide1_eq, real_times_divide2_eq];
14.587 -
14.588 -Goal "(x::real) / (y/z) = (x*z)/y";
14.589 -by (simp_tac (simpset() addsimps [real_divide_def, real_inverse_distrib]@
14.590 - real_mult_ac) 1);
14.591 -qed "real_divide_divide1_eq";
14.592 -
14.593 -Goal "((x::real) / y) / z = x/(y*z)";
14.594 -by (simp_tac (simpset() addsimps [real_divide_def, real_inverse_distrib,
14.595 - real_mult_assoc]) 1);
14.596 -qed "real_divide_divide2_eq";
14.597 -
14.598 -Addsimps [real_divide_divide1_eq, real_divide_divide2_eq];
14.599 -
14.600 -(** As with multiplication, pull minus signs OUT of the / operator **)
14.601 -
14.602 -Goal "(-x) / (y::real) = - (x/y)";
14.603 -by (simp_tac (simpset() addsimps [real_divide_def]) 1);
14.604 -qed "real_minus_divide_eq";
14.605 -Addsimps [real_minus_divide_eq];
14.606 -
14.607 -Goal "(x / -(y::real)) = - (x/y)";
14.608 -by (simp_tac (simpset() addsimps [real_divide_def, real_minus_inverse]) 1);
14.609 -qed "real_divide_minus_eq";
14.610 -Addsimps [real_divide_minus_eq];
14.611 -
14.612 -Goal "(x+y)/(z::real) = x/z + y/z";
14.613 -by (simp_tac (simpset() addsimps [real_divide_def, real_add_mult_distrib]) 1);
14.614 -qed "real_add_divide_distrib";
14.615 -
14.616 -(*The following would e.g. convert (x+y)/2 to x/2 + y/2. Sometimes that
14.617 - leads to cancellations in x or y, but is also prevents "multiplying out"
14.618 - the 2 in e.g. (x+y)/2 = 5.
14.619 -
14.620 -Addsimps [inst "z" "number_of ?w" real_add_divide_distrib];
14.621 -**)
14.622 -
14.623 -
14.624 -(*---------------------------------------------------------
14.625 - Theorems for ordering
14.626 - --------------------------------------------------------*)
14.627 -(* prove introduction and elimination rules for real_less *)
14.628 -
14.629 -(* real_less is a strong order i.e. nonreflexive and transitive *)
14.630 -
14.631 -(*** lemmas ***)
14.632 -Goal "!!(x::preal). [| x = y; x1 = y1 |] ==> x + y1 = x1 + y";
14.633 -by (asm_simp_tac (simpset() addsimps [preal_add_commute]) 1);
14.634 -qed "preal_lemma_eq_rev_sum";
14.635 -
14.636 -Goal "!!(b::preal). x + (b + y) = x1 + (b + y1) ==> x + y = x1 + y1";
14.637 -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
14.638 -qed "preal_add_left_commute_cancel";
14.639 -
14.640 -Goal "!!(x::preal). [| x + y2a = x2a + y; \
14.641 -\ x + y2b = x2b + y |] \
14.642 -\ ==> x2a + y2b = x2b + y2a";
14.643 -by (dtac preal_lemma_eq_rev_sum 1);
14.644 -by (assume_tac 1);
14.645 -by (thin_tac "x + y2b = x2b + y" 1);
14.646 -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
14.647 -by (dtac preal_add_left_commute_cancel 1);
14.648 -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
14.649 -qed "preal_lemma_for_not_refl";
14.650 -
14.651 -Goal "~ (R::real) < R";
14.652 -by (res_inst_tac [("z","R")] eq_Abs_REAL 1);
14.653 -by (auto_tac (claset(),simpset() addsimps [real_less_def]));
14.654 -by (dtac preal_lemma_for_not_refl 1);
14.655 -by (assume_tac 1);
14.656 -by Auto_tac;
14.657 -qed "real_less_not_refl";
14.658 -
14.659 -(*** y < y ==> P ***)
14.660 -bind_thm("real_less_irrefl", real_less_not_refl RS notE);
14.661 -AddSEs [real_less_irrefl];
14.662 -
14.663 -Goal "!!(x::real). x < y ==> x ~= y";
14.664 -by (auto_tac (claset(),simpset() addsimps [real_less_not_refl]));
14.665 -qed "real_not_refl2";
14.666 -
14.667 -(* lemma re-arranging and eliminating terms *)
14.668 -Goal "!! (a::preal). [| a + b = c + d; \
14.669 -\ x2b + d + (c + y2e) < a + y2b + (x2e + b) |] \
14.670 -\ ==> x2b + y2e < x2e + y2b";
14.671 -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
14.672 -by (res_inst_tac [("C","c+d")] preal_add_left_less_cancel 1);
14.673 -by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
14.674 -qed "preal_lemma_trans";
14.675 -
14.676 -(** heavy re-writing involved*)
14.677 -Goal "!!(R1::real). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
14.678 -by (res_inst_tac [("z","R1")] eq_Abs_REAL 1);
14.679 -by (res_inst_tac [("z","R2")] eq_Abs_REAL 1);
14.680 -by (res_inst_tac [("z","R3")] eq_Abs_REAL 1);
14.681 -by (auto_tac (claset(),simpset() addsimps [real_less_def]));
14.682 -by (REPEAT(rtac exI 1));
14.683 -by (EVERY[rtac conjI 1, rtac conjI 2]);
14.684 -by (REPEAT(Blast_tac 2));
14.685 -by (dtac preal_lemma_for_not_refl 1 THEN assume_tac 1);
14.686 -by (blast_tac (claset() addDs [preal_add_less_mono]
14.687 - addIs [preal_lemma_trans]) 1);
14.688 -qed "real_less_trans";
14.689 -
14.690 -Goal "!! (R1::real). R1 < R2 ==> ~ (R2 < R1)";
14.691 -by (rtac notI 1);
14.692 -by (dtac real_less_trans 1 THEN assume_tac 1);
14.693 -by (asm_full_simp_tac (simpset() addsimps [real_less_not_refl]) 1);
14.694 -qed "real_less_not_sym";
14.695 -
14.696 -(* [| x < y; ~P ==> y < x |] ==> P *)
14.697 -bind_thm ("real_less_asym", real_less_not_sym RS contrapos_np);
14.698 -
14.699 -Goalw [real_of_preal_def]
14.700 - "real_of_preal ((z1::preal) + z2) = \
14.701 -\ real_of_preal z1 + real_of_preal z2";
14.702 -by (asm_simp_tac (simpset() addsimps [real_add,
14.703 - preal_add_mult_distrib,preal_mult_1] addsimps preal_add_ac) 1);
14.704 -qed "real_of_preal_add";
14.705 -
14.706 -Goalw [real_of_preal_def]
14.707 - "real_of_preal ((z1::preal) * z2) = \
14.708 -\ real_of_preal z1* real_of_preal z2";
14.709 -by (full_simp_tac (simpset() addsimps [real_mult,
14.710 - preal_add_mult_distrib2,preal_mult_1,
14.711 - preal_mult_1_right,pnat_one_def]
14.712 - @ preal_add_ac @ preal_mult_ac) 1);
14.713 -qed "real_of_preal_mult";
14.714 -
14.715 -Goalw [real_of_preal_def]
14.716 - "!!(x::preal). y < x ==> \
14.717 -\ EX m. Abs_REAL (realrel `` {(x,y)}) = real_of_preal m";
14.718 -by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
14.719 - simpset() addsimps preal_add_ac));
14.720 -qed "real_of_preal_ExI";
14.721 -
14.722 -Goalw [real_of_preal_def]
14.723 - "!!(x::preal). EX m. Abs_REAL (realrel `` {(x,y)}) = \
14.724 -\ real_of_preal m ==> y < x";
14.725 -by (auto_tac (claset(),
14.726 - simpset() addsimps
14.727 - [preal_add_commute,preal_add_assoc]));
14.728 -by (asm_full_simp_tac (simpset() addsimps
14.729 - [preal_add_assoc RS sym,preal_self_less_add_left]) 1);
14.730 -qed "real_of_preal_ExD";
14.731 -
14.732 -Goal "(EX m. Abs_REAL (realrel `` {(x,y)}) = real_of_preal m) = (y < x)";
14.733 -by (blast_tac (claset() addSIs [real_of_preal_ExI,real_of_preal_ExD]) 1);
14.734 -qed "real_of_preal_iff";
14.735 -
14.736 -(*** Gleason prop 9-4.4 p 127 ***)
14.737 -Goalw [real_of_preal_def,real_zero_def]
14.738 - "EX m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)";
14.739 -by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
14.740 -by (auto_tac (claset(),simpset() addsimps [real_minus] @ preal_add_ac));
14.741 -by (cut_inst_tac [("r1.0","x"),("r2.0","y")] preal_linear 1);
14.742 -by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
14.743 - simpset() addsimps [preal_add_assoc RS sym]));
14.744 -by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
14.745 -qed "real_of_preal_trichotomy";
14.746 -
14.747 -Goal "!!P. [| !!m. x = real_of_preal m ==> P; \
14.748 -\ x = 0 ==> P; \
14.749 -\ !!m. x = -(real_of_preal m) ==> P |] ==> P";
14.750 -by (cut_inst_tac [("x","x")] real_of_preal_trichotomy 1);
14.751 -by Auto_tac;
14.752 -qed "real_of_preal_trichotomyE";
14.753 -
14.754 -Goalw [real_of_preal_def]
14.755 - "real_of_preal m1 < real_of_preal m2 ==> m1 < m2";
14.756 -by (auto_tac (claset(),simpset() addsimps [real_less_def] @ preal_add_ac));
14.757 -by (auto_tac (claset(),simpset() addsimps [preal_add_assoc RS sym]));
14.758 -by (auto_tac (claset(),simpset() addsimps preal_add_ac));
14.759 -qed "real_of_preal_lessD";
14.760 -
14.761 -Goal "m1 < m2 ==> real_of_preal m1 < real_of_preal m2";
14.762 -by (dtac preal_less_add_left_Ex 1);
14.763 -by (auto_tac (claset(),
14.764 - simpset() addsimps [real_of_preal_add,
14.765 - real_of_preal_def,real_less_def]));
14.766 -by (REPEAT(rtac exI 1));
14.767 -by (EVERY[rtac conjI 1, rtac conjI 2]);
14.768 -by (REPEAT(Blast_tac 2));
14.769 -by (simp_tac (simpset() addsimps [preal_self_less_add_left]
14.770 - delsimps [preal_add_less_iff2]) 1);
14.771 -qed "real_of_preal_lessI";
14.772 -
14.773 -Goal "(real_of_preal m1 < real_of_preal m2) = (m1 < m2)";
14.774 -by (blast_tac (claset() addIs [real_of_preal_lessI,real_of_preal_lessD]) 1);
14.775 -qed "real_of_preal_less_iff1";
14.776 -
14.777 -Addsimps [real_of_preal_less_iff1];
14.778 -
14.779 -Goal "- real_of_preal m < real_of_preal m";
14.780 -by (auto_tac (claset(),
14.781 - simpset() addsimps
14.782 - [real_of_preal_def,real_less_def,real_minus]));
14.783 -by (REPEAT(rtac exI 1));
14.784 -by (EVERY[rtac conjI 1, rtac conjI 2]);
14.785 -by (REPEAT(Blast_tac 2));
14.786 -by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
14.787 -by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
14.788 - preal_add_assoc RS sym]) 1);
14.789 -qed "real_of_preal_minus_less_self";
14.790 -
14.791 -Goalw [real_zero_def] "- real_of_preal m < 0";
14.792 -by (auto_tac (claset(),
14.793 - simpset() addsimps [real_of_preal_def,
14.794 - real_less_def,real_minus]));
14.795 -by (REPEAT(rtac exI 1));
14.796 -by (EVERY[rtac conjI 1, rtac conjI 2]);
14.797 -by (REPEAT(Blast_tac 2));
14.798 -by (full_simp_tac (simpset() addsimps
14.799 - [preal_self_less_add_right] @ preal_add_ac) 1);
14.800 -qed "real_of_preal_minus_less_zero";
14.801 -
14.802 -Goal "~ 0 < - real_of_preal m";
14.803 -by (cut_facts_tac [real_of_preal_minus_less_zero] 1);
14.804 -by (fast_tac (claset() addDs [real_less_trans]
14.805 - addEs [real_less_irrefl]) 1);
14.806 -qed "real_of_preal_not_minus_gt_zero";
14.807 -
14.808 -Goalw [real_zero_def] "0 < real_of_preal m";
14.809 -by (auto_tac (claset(),simpset() addsimps
14.810 - [real_of_preal_def,real_less_def,real_minus]));
14.811 -by (REPEAT(rtac exI 1));
14.812 -by (EVERY[rtac conjI 1, rtac conjI 2]);
14.813 -by (REPEAT(Blast_tac 2));
14.814 -by (full_simp_tac (simpset() addsimps
14.815 - [preal_self_less_add_right] @ preal_add_ac) 1);
14.816 -qed "real_of_preal_zero_less";
14.817 -
14.818 -Goal "~ real_of_preal m < 0";
14.819 -by (cut_facts_tac [real_of_preal_zero_less] 1);
14.820 -by (blast_tac (claset() addDs [real_less_trans]
14.821 - addEs [real_less_irrefl]) 1);
14.822 -qed "real_of_preal_not_less_zero";
14.823 -
14.824 -Goal "0 < - (- real_of_preal m)";
14.825 -by (simp_tac (simpset() addsimps
14.826 - [real_of_preal_zero_less]) 1);
14.827 -qed "real_minus_minus_zero_less";
14.828 -
14.829 -(* another lemma *)
14.830 -Goalw [real_zero_def]
14.831 - "0 < real_of_preal m + real_of_preal m1";
14.832 -by (auto_tac (claset(),
14.833 - simpset() addsimps [real_of_preal_def,
14.834 - real_less_def,real_add]));
14.835 -by (REPEAT(rtac exI 1));
14.836 -by (EVERY[rtac conjI 1, rtac conjI 2]);
14.837 -by (REPEAT(Blast_tac 2));
14.838 -by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
14.839 -by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
14.840 - preal_add_assoc RS sym]) 1);
14.841 -qed "real_of_preal_sum_zero_less";
14.842 -
14.843 -Goal "- real_of_preal m < real_of_preal m1";
14.844 -by (auto_tac (claset(),
14.845 - simpset() addsimps [real_of_preal_def,
14.846 - real_less_def,real_minus]));
14.847 -by (REPEAT(rtac exI 1));
14.848 -by (EVERY[rtac conjI 1, rtac conjI 2]);
14.849 -by (REPEAT(Blast_tac 2));
14.850 -by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
14.851 -by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
14.852 - preal_add_assoc RS sym]) 1);
14.853 -qed "real_of_preal_minus_less_all";
14.854 -
14.855 -Goal "~ real_of_preal m < - real_of_preal m1";
14.856 -by (cut_facts_tac [real_of_preal_minus_less_all] 1);
14.857 -by (blast_tac (claset() addDs [real_less_trans]
14.858 - addEs [real_less_irrefl]) 1);
14.859 -qed "real_of_preal_not_minus_gt_all";
14.860 -
14.861 -Goal "- real_of_preal m1 < - real_of_preal m2 \
14.862 -\ ==> real_of_preal m2 < real_of_preal m1";
14.863 -by (auto_tac (claset(),
14.864 - simpset() addsimps [real_of_preal_def,
14.865 - real_less_def,real_minus]));
14.866 -by (REPEAT(rtac exI 1));
14.867 -by (EVERY[rtac conjI 1, rtac conjI 2]);
14.868 -by (REPEAT(Blast_tac 2));
14.869 -by (auto_tac (claset(),simpset() addsimps preal_add_ac));
14.870 -by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
14.871 -by (auto_tac (claset(),simpset() addsimps preal_add_ac));
14.872 -qed "real_of_preal_minus_less_rev1";
14.873 -
14.874 -Goal "real_of_preal m1 < real_of_preal m2 \
14.875 -\ ==> - real_of_preal m2 < - real_of_preal m1";
14.876 -by (auto_tac (claset(),
14.877 - simpset() addsimps [real_of_preal_def,
14.878 - real_less_def,real_minus]));
14.879 -by (REPEAT(rtac exI 1));
14.880 -by (EVERY[rtac conjI 1, rtac conjI 2]);
14.881 -by (REPEAT(Blast_tac 2));
14.882 -by (auto_tac (claset(),simpset() addsimps preal_add_ac));
14.883 -by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
14.884 -by (auto_tac (claset(),simpset() addsimps preal_add_ac));
14.885 -qed "real_of_preal_minus_less_rev2";
14.886 -
14.887 -Goal "(- real_of_preal m1 < - real_of_preal m2) = \
14.888 -\ (real_of_preal m2 < real_of_preal m1)";
14.889 -by (blast_tac (claset() addSIs [real_of_preal_minus_less_rev1,
14.890 - real_of_preal_minus_less_rev2]) 1);
14.891 -qed "real_of_preal_minus_less_rev_iff";
14.892 -
14.893 -Addsimps [real_of_preal_minus_less_rev_iff];
14.894 -
14.895 -(*** linearity ***)
14.896 -Goal "(R1::real) < R2 | R1 = R2 | R2 < R1";
14.897 -by (res_inst_tac [("x","R1")] real_of_preal_trichotomyE 1);
14.898 -by (ALLGOALS(res_inst_tac [("x","R2")] real_of_preal_trichotomyE));
14.899 -by (auto_tac (claset() addSDs [preal_le_anti_sym],
14.900 - simpset() addsimps [preal_less_le_iff,real_of_preal_minus_less_zero,
14.901 - real_of_preal_zero_less,real_of_preal_minus_less_all]));
14.902 -qed "real_linear";
14.903 -
14.904 -Goal "!!w::real. (w ~= z) = (w<z | z<w)";
14.905 -by (cut_facts_tac [real_linear] 1);
14.906 -by (Blast_tac 1);
14.907 -qed "real_neq_iff";
14.908 -
14.909 -Goal "!!(R1::real). [| R1 < R2 ==> P; R1 = R2 ==> P; \
14.910 -\ R2 < R1 ==> P |] ==> P";
14.911 -by (cut_inst_tac [("R1.0","R1"),("R2.0","R2")] real_linear 1);
14.912 -by Auto_tac;
14.913 -qed "real_linear_less2";
14.914 -
14.915 -(*** Properties of <= ***)
14.916 -
14.917 -Goalw [real_le_def] "~(w < z) ==> z <= (w::real)";
14.918 -by (assume_tac 1);
14.919 -qed "real_leI";
14.920 -
14.921 -Goalw [real_le_def] "z<=w ==> ~(w<(z::real))";
14.922 -by (assume_tac 1);
14.923 -qed "real_leD";
14.924 -
14.925 -bind_thm ("real_leE", make_elim real_leD);
14.926 -
14.927 -Goal "(~(w < z)) = (z <= (w::real))";
14.928 -by (blast_tac (claset() addSIs [real_leI,real_leD]) 1);
14.929 -qed "real_less_le_iff";
14.930 -
14.931 -Goalw [real_le_def] "~ z <= w ==> w<(z::real)";
14.932 -by (Blast_tac 1);
14.933 -qed "not_real_leE";
14.934 -
14.935 -Goalw [real_le_def] "!!(x::real). x <= y ==> x < y | x = y";
14.936 -by (cut_facts_tac [real_linear] 1);
14.937 -by (blast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
14.938 -qed "real_le_imp_less_or_eq";
14.939 -
14.940 -Goalw [real_le_def] "z<w | z=w ==> z <=(w::real)";
14.941 -by (cut_facts_tac [real_linear] 1);
14.942 -by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
14.943 -qed "real_less_or_eq_imp_le";
14.944 -
14.945 -Goal "(x <= (y::real)) = (x < y | x=y)";
14.946 -by (REPEAT(ares_tac [iffI, real_less_or_eq_imp_le, real_le_imp_less_or_eq] 1));
14.947 -qed "real_le_less";
14.948 -
14.949 -Goal "w <= (w::real)";
14.950 -by (simp_tac (simpset() addsimps [real_le_less]) 1);
14.951 -qed "real_le_refl";
14.952 -
14.953 -(* Axiom 'linorder_linear' of class 'linorder': *)
14.954 -Goal "(z::real) <= w | w <= z";
14.955 -by (simp_tac (simpset() addsimps [real_le_less]) 1);
14.956 -by (cut_facts_tac [real_linear] 1);
14.957 -by (Blast_tac 1);
14.958 -qed "real_le_linear";
14.959 -
14.960 -Goal "[| i <= j; j <= k |] ==> i <= (k::real)";
14.961 -by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
14.962 - rtac real_less_or_eq_imp_le,
14.963 - blast_tac (claset() addIs [real_less_trans])]);
14.964 -qed "real_le_trans";
14.965 -
14.966 -Goal "[| z <= w; w <= z |] ==> z = (w::real)";
14.967 -by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
14.968 - fast_tac (claset() addEs [real_less_irrefl,real_less_asym])]);
14.969 -qed "real_le_anti_sym";
14.970 -
14.971 -Goal "[| ~ y < x; y ~= x |] ==> x < (y::real)";
14.972 -by (rtac not_real_leE 1);
14.973 -by (blast_tac (claset() addDs [real_le_imp_less_or_eq]) 1);
14.974 -qed "not_less_not_eq_real_less";
14.975 -
14.976 -(* Axiom 'order_less_le' of class 'order': *)
14.977 -Goal "((w::real) < z) = (w <= z & w ~= z)";
14.978 -by (simp_tac (simpset() addsimps [real_le_def, real_neq_iff]) 1);
14.979 -by (blast_tac (claset() addSEs [real_less_asym]) 1);
14.980 -qed "real_less_le";
14.981 -
14.982 -Goal "(0 < -R) = (R < (0::real))";
14.983 -by (res_inst_tac [("x","R")] real_of_preal_trichotomyE 1);
14.984 -by (auto_tac (claset(),
14.985 - simpset() addsimps [real_of_preal_not_minus_gt_zero,
14.986 - real_of_preal_not_less_zero,real_of_preal_zero_less,
14.987 - real_of_preal_minus_less_zero]));
14.988 -qed "real_minus_zero_less_iff";
14.989 -Addsimps [real_minus_zero_less_iff];
14.990 -
14.991 -Goal "(-R < 0) = ((0::real) < R)";
14.992 -by (res_inst_tac [("x","R")] real_of_preal_trichotomyE 1);
14.993 -by (auto_tac (claset(),
14.994 - simpset() addsimps [real_of_preal_not_minus_gt_zero,
14.995 - real_of_preal_not_less_zero,real_of_preal_zero_less,
14.996 - real_of_preal_minus_less_zero]));
14.997 -qed "real_minus_zero_less_iff2";
14.998 -Addsimps [real_minus_zero_less_iff2];
14.999 -
14.1000 -(*Alternative definition for real_less*)
14.1001 -Goal "R < S ==> EX T::real. 0 < T & R + T = S";
14.1002 -by (res_inst_tac [("x","R")] real_of_preal_trichotomyE 1);
14.1003 -by (ALLGOALS(res_inst_tac [("x","S")] real_of_preal_trichotomyE));
14.1004 -by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
14.1005 - simpset() addsimps [real_of_preal_not_minus_gt_all,
14.1006 - real_of_preal_add, real_of_preal_not_less_zero,
14.1007 - real_less_not_refl,
14.1008 - real_of_preal_not_minus_gt_zero]));
14.1009 -by (res_inst_tac [("x","real_of_preal D")] exI 1);
14.1010 -by (res_inst_tac [("x","real_of_preal m+real_of_preal ma")] exI 2);
14.1011 -by (res_inst_tac [("x","real_of_preal D")] exI 3);
14.1012 -by (auto_tac (claset(),
14.1013 - simpset() addsimps [real_of_preal_zero_less,
14.1014 - real_of_preal_sum_zero_less,real_add_assoc]));
14.1015 -qed "real_less_add_positive_left_Ex";
14.1016 -
14.1017 -(** change naff name(s)! **)
14.1018 -Goal "(W < S) ==> (0 < S + (-W::real))";
14.1019 -by (dtac real_less_add_positive_left_Ex 1);
14.1020 -by (auto_tac (claset(),
14.1021 - simpset() addsimps [real_add_minus,
14.1022 - real_add_zero_right] @ real_add_ac));
14.1023 -qed "real_less_sum_gt_zero";
14.1024 -
14.1025 -Goal "!!S::real. T = S + W ==> S = T + (-W)";
14.1026 -by (asm_simp_tac (simpset() addsimps real_add_ac) 1);
14.1027 -qed "real_lemma_change_eq_subj";
14.1028 -
14.1029 -(* FIXME: long! *)
14.1030 -Goal "(0 < S + (-W::real)) ==> (W < S)";
14.1031 -by (rtac ccontr 1);
14.1032 -by (dtac (real_leI RS real_le_imp_less_or_eq) 1);
14.1033 -by (auto_tac (claset(),
14.1034 - simpset() addsimps [real_less_not_refl]));
14.1035 -by (EVERY1[dtac real_less_add_positive_left_Ex, etac exE, etac conjE]);
14.1036 -by (Asm_full_simp_tac 1);
14.1037 -by (dtac real_lemma_change_eq_subj 1);
14.1038 -by Auto_tac;
14.1039 -by (dtac real_less_sum_gt_zero 1);
14.1040 -by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1);
14.1041 -by (EVERY1[rotate_tac 1, dtac (real_add_left_commute RS ssubst)]);
14.1042 -by (auto_tac (claset() addEs [real_less_asym], simpset()));
14.1043 -qed "real_sum_gt_zero_less";
14.1044 -
14.1045 -Goal "(0 < S + (-W::real)) = (W < S)";
14.1046 -by (blast_tac (claset() addIs [real_less_sum_gt_zero,
14.1047 - real_sum_gt_zero_less]) 1);
14.1048 -qed "real_less_sum_gt_0_iff";
14.1049 -
14.1050 -
14.1051 -Goalw [real_diff_def] "(x<y) = (x-y < (0::real))";
14.1052 -by (stac (real_minus_zero_less_iff RS sym) 1);
14.1053 -by (simp_tac (simpset() addsimps [real_add_commute,
14.1054 - real_less_sum_gt_0_iff]) 1);
14.1055 -qed "real_less_eq_diff";
14.1056 -
14.1057 -
14.1058 -(*** Subtraction laws ***)
14.1059 -
14.1060 -Goal "x + (y - z) = (x + y) - (z::real)";
14.1061 -by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
14.1062 -qed "real_add_diff_eq";
14.1063 -
14.1064 -Goal "(x - y) + z = (x + z) - (y::real)";
14.1065 -by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
14.1066 -qed "real_diff_add_eq";
14.1067 -
14.1068 -Goal "(x - y) - z = x - (y + (z::real))";
14.1069 -by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
14.1070 -qed "real_diff_diff_eq";
14.1071 -
14.1072 -Goal "x - (y - z) = (x + z) - (y::real)";
14.1073 -by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
14.1074 -qed "real_diff_diff_eq2";
14.1075 -
14.1076 -Goal "(x-y < z) = (x < z + (y::real))";
14.1077 -by (stac real_less_eq_diff 1);
14.1078 -by (res_inst_tac [("y1", "z")] (real_less_eq_diff RS ssubst) 1);
14.1079 -by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
14.1080 -qed "real_diff_less_eq";
14.1081 -
14.1082 -Goal "(x < z-y) = (x + (y::real) < z)";
14.1083 -by (stac real_less_eq_diff 1);
14.1084 -by (res_inst_tac [("y1", "z-y")] (real_less_eq_diff RS ssubst) 1);
14.1085 -by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
14.1086 -qed "real_less_diff_eq";
14.1087 -
14.1088 -Goalw [real_le_def] "(x-y <= z) = (x <= z + (y::real))";
14.1089 -by (simp_tac (simpset() addsimps [real_less_diff_eq]) 1);
14.1090 -qed "real_diff_le_eq";
14.1091 -
14.1092 -Goalw [real_le_def] "(x <= z-y) = (x + (y::real) <= z)";
14.1093 -by (simp_tac (simpset() addsimps [real_diff_less_eq]) 1);
14.1094 -qed "real_le_diff_eq";
14.1095 -
14.1096 -Goalw [real_diff_def] "(x-y = z) = (x = z + (y::real))";
14.1097 -by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
14.1098 -qed "real_diff_eq_eq";
14.1099 -
14.1100 -Goalw [real_diff_def] "(x = z-y) = (x + (y::real) = z)";
14.1101 -by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
14.1102 -qed "real_eq_diff_eq";
14.1103 -
14.1104 -(*This list of rewrites simplifies (in)equalities by bringing subtractions
14.1105 - to the top and then moving negative terms to the other side.
14.1106 - Use with real_add_ac*)
14.1107 -bind_thms ("real_compare_rls",
14.1108 - [symmetric real_diff_def,
14.1109 - real_add_diff_eq, real_diff_add_eq, real_diff_diff_eq, real_diff_diff_eq2,
14.1110 - real_diff_less_eq, real_less_diff_eq, real_diff_le_eq, real_le_diff_eq,
14.1111 - real_diff_eq_eq, real_eq_diff_eq]);
14.1112 -
14.1113 -
14.1114 -(** For the cancellation simproc.
14.1115 - The idea is to cancel like terms on opposite sides by subtraction **)
14.1116 -
14.1117 -Goal "(x::real) - y = x' - y' ==> (x<y) = (x'<y')";
14.1118 -by (stac real_less_eq_diff 1);
14.1119 -by (res_inst_tac [("y1", "y")] (real_less_eq_diff RS ssubst) 1);
14.1120 -by (Asm_simp_tac 1);
14.1121 -qed "real_less_eqI";
14.1122 -
14.1123 -Goal "(x::real) - y = x' - y' ==> (y<=x) = (y'<=x')";
14.1124 -by (dtac real_less_eqI 1);
14.1125 -by (asm_simp_tac (simpset() addsimps [real_le_def]) 1);
14.1126 -qed "real_le_eqI";
14.1127 -
14.1128 -Goal "(x::real) - y = x' - y' ==> (x=y) = (x'=y')";
14.1129 -by Safe_tac;
14.1130 -by (ALLGOALS
14.1131 - (asm_full_simp_tac
14.1132 - (simpset() addsimps [real_eq_diff_eq, real_diff_eq_eq])));
14.1133 -qed "real_eq_eqI";
15.1 --- a/src/HOL/Real/RealDef.thy Thu Nov 27 10:47:55 2003 +0100
15.2 +++ b/src/HOL/Real/RealDef.thy Fri Nov 28 12:09:37 2003 +0100
15.3 @@ -3,91 +3,1140 @@
15.4 Author : Jacques D. Fleuriot
15.5 Copyright : 1998 University of Cambridge
15.6 Description : The reals
15.7 -*)
15.8 +*)
15.9
15.10 -RealDef = PReal +
15.11 +theory RealDef = PReal:
15.12
15.13 -instance preal :: order (preal_le_refl,preal_le_trans,preal_le_anti_sym,
15.14 - preal_less_le)
15.15 +instance preal :: order
15.16 +proof qed
15.17 + (assumption |
15.18 + rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
15.19
15.20 constdefs
15.21 realrel :: "((preal * preal) * (preal * preal)) set"
15.22 - "realrel == {p. EX x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
15.23 + "realrel == {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
15.24
15.25 -typedef (REAL)
15.26 - real = "UNIV//realrel" (quotient_def)
15.27 +typedef (REAL) real = "UNIV//realrel"
15.28 + by (auto simp add: quotient_def)
15.29
15.30 +instance real :: ord ..
15.31 +instance real :: zero ..
15.32 +instance real :: one ..
15.33 +instance real :: plus ..
15.34 +instance real :: times ..
15.35 +instance real :: minus ..
15.36 +instance real :: inverse ..
15.37
15.38 -instance
15.39 - real :: {ord, zero, one, plus, times, minus, inverse}
15.40 -
15.41 -consts
15.42 +consts
15.43 (*Overloaded constants denoting the Nat and Real subsets of enclosing
15.44 types such as hypreal and complex*)
15.45 - Nats, Reals :: "'a set"
15.46 -
15.47 + Nats :: "'a set"
15.48 + Reals :: "'a set"
15.49 +
15.50 (*overloaded constant for injecting other types into "real"*)
15.51 - real :: 'a => real
15.52 + real :: "'a => real"
15.53
15.54
15.55 -defs
15.56 +defs (overloaded)
15.57
15.58 - real_zero_def
15.59 + real_zero_def:
15.60 "0 == Abs_REAL(realrel``{(preal_of_prat(prat_of_pnat 1),
15.61 preal_of_prat(prat_of_pnat 1))})"
15.62
15.63 - real_one_def
15.64 + real_one_def:
15.65 "1 == Abs_REAL(realrel``
15.66 {(preal_of_prat(prat_of_pnat 1) + preal_of_prat(prat_of_pnat 1),
15.67 preal_of_prat(prat_of_pnat 1))})"
15.68
15.69 - real_minus_def
15.70 + real_minus_def:
15.71 "- R == Abs_REAL(UN (x,y):Rep_REAL(R). realrel``{(y,x)})"
15.72
15.73 - real_diff_def
15.74 + real_diff_def:
15.75 "R - (S::real) == R + - S"
15.76
15.77 - real_inverse_def
15.78 + real_inverse_def:
15.79 "inverse (R::real) == (SOME S. (R = 0 & S = 0) | S * R = 1)"
15.80
15.81 - real_divide_def
15.82 + real_divide_def:
15.83 "R / (S::real) == R * inverse S"
15.84 -
15.85 +
15.86 constdefs
15.87
15.88 (** these don't use the overloaded "real" function: users don't see them **)
15.89 -
15.90 - real_of_preal :: preal => real
15.91 +
15.92 + real_of_preal :: "preal => real"
15.93 "real_of_preal m ==
15.94 Abs_REAL(realrel``{(m + preal_of_prat(prat_of_pnat 1),
15.95 preal_of_prat(prat_of_pnat 1))})"
15.96
15.97 - real_of_posnat :: nat => real
15.98 + real_of_posnat :: "nat => real"
15.99 "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"
15.100
15.101
15.102 -defs
15.103 +defs (overloaded)
15.104
15.105 - (*overloaded*)
15.106 - real_of_nat_def "real n == real_of_posnat n + (- 1)"
15.107 + real_of_nat_def: "real n == real_of_posnat n + (- 1)"
15.108
15.109 - real_add_def
15.110 + real_add_def:
15.111 "P+Q == Abs_REAL(UN p1:Rep_REAL(P). UN p2:Rep_REAL(Q).
15.112 (%(x1,y1). (%(x2,y2). realrel``{(x1+x2, y1+y2)}) p2) p1)"
15.113 -
15.114 - real_mult_def
15.115 +
15.116 + real_mult_def:
15.117 "P*Q == Abs_REAL(UN p1:Rep_REAL(P). UN p2:Rep_REAL(Q).
15.118 (%(x1,y1). (%(x2,y2). realrel``{(x1*x2+y1*y2,x1*y2+x2*y1)})
15.119 p2) p1)"
15.120
15.121 - real_less_def
15.122 - "P<Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 &
15.123 - (x1,y1):Rep_REAL(P) & (x2,y2):Rep_REAL(Q)"
15.124 - real_le_def
15.125 - "P <= (Q::real) == ~(Q < P)"
15.126 + real_less_def:
15.127 + "P<Q == \<exists>x1 y1 x2 y2. x1 + y2 < x2 + y1 &
15.128 + (x1,y1):Rep_REAL(P) & (x2,y2):Rep_REAL(Q)"
15.129 + real_le_def:
15.130 + "P \<le> (Q::real) == ~(Q < P)"
15.131
15.132 syntax (xsymbols)
15.133 - Reals :: "'a set" ("\\<real>")
15.134 - Nats :: "'a set" ("\\<nat>")
15.135 + Reals :: "'a set" ("\<real>")
15.136 + Nats :: "'a set" ("\<nat>")
15.137 +
15.138 +
15.139 +(*** Proving that realrel is an equivalence relation ***)
15.140 +
15.141 +lemma preal_trans_lemma: "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |]
15.142 + ==> x1 + y3 = x3 + y1"
15.143 +apply (rule_tac C = y2 in preal_add_right_cancel)
15.144 +apply (rotate_tac 1, drule sym)
15.145 +apply (simp add: preal_add_ac)
15.146 +apply (rule preal_add_left_commute [THEN subst])
15.147 +apply (rule_tac x1 = x1 in preal_add_assoc [THEN subst])
15.148 +apply (simp add: preal_add_ac)
15.149 +done
15.150 +
15.151 +(** Natural deduction for realrel **)
15.152 +
15.153 +lemma realrel_iff [simp]: "(((x1,y1),(x2,y2)): realrel) = (x1 + y2 = x2 + y1)"
15.154 +by (unfold realrel_def, blast)
15.155 +
15.156 +lemma realrel_refl: "(x,x): realrel"
15.157 +apply (case_tac "x")
15.158 +apply (simp add: realrel_def)
15.159 +done
15.160 +
15.161 +lemma equiv_realrel: "equiv UNIV realrel"
15.162 +apply (unfold equiv_def refl_def sym_def trans_def realrel_def)
15.163 +apply (fast elim!: sym preal_trans_lemma)
15.164 +done
15.165 +
15.166 +(* (realrel `` {x} = realrel `` {y}) = ((x,y) : realrel) *)
15.167 +lemmas equiv_realrel_iff =
15.168 + eq_equiv_class_iff [OF equiv_realrel UNIV_I UNIV_I]
15.169 +
15.170 +declare equiv_realrel_iff [simp]
15.171 +
15.172 +lemma realrel_in_real [simp]: "realrel``{(x,y)}: REAL"
15.173 +by (unfold REAL_def realrel_def quotient_def, blast)
15.174 +
15.175 +lemma inj_on_Abs_REAL: "inj_on Abs_REAL REAL"
15.176 +apply (rule inj_on_inverseI)
15.177 +apply (erule Abs_REAL_inverse)
15.178 +done
15.179 +
15.180 +declare inj_on_Abs_REAL [THEN inj_on_iff, simp]
15.181 +declare Abs_REAL_inverse [simp]
15.182 +
15.183 +
15.184 +lemmas eq_realrelD = equiv_realrel [THEN [2] eq_equiv_class]
15.185 +
15.186 +lemma inj_Rep_REAL: "inj Rep_REAL"
15.187 +apply (rule inj_on_inverseI)
15.188 +apply (rule Rep_REAL_inverse)
15.189 +done
15.190 +
15.191 +(** real_of_preal: the injection from preal to real **)
15.192 +lemma inj_real_of_preal: "inj(real_of_preal)"
15.193 +apply (rule inj_onI)
15.194 +apply (unfold real_of_preal_def)
15.195 +apply (drule inj_on_Abs_REAL [THEN inj_onD])
15.196 +apply (rule realrel_in_real)+
15.197 +apply (drule eq_equiv_class)
15.198 +apply (rule equiv_realrel, blast)
15.199 +apply (simp add: realrel_def)
15.200 +done
15.201 +
15.202 +lemma eq_Abs_REAL:
15.203 + "(!!x y. z = Abs_REAL(realrel``{(x,y)}) ==> P) ==> P"
15.204 +apply (rule_tac x1 = z in Rep_REAL [unfolded REAL_def, THEN quotientE])
15.205 +apply (drule_tac f = Abs_REAL in arg_cong)
15.206 +apply (case_tac "x")
15.207 +apply (simp add: Rep_REAL_inverse)
15.208 +done
15.209 +
15.210 +(**** real_minus: additive inverse on real ****)
15.211 +
15.212 +lemma real_minus_congruent:
15.213 + "congruent realrel (%p. (%(x,y). realrel``{(y,x)}) p)"
15.214 +apply (unfold congruent_def, clarify)
15.215 +apply (simp add: preal_add_commute)
15.216 +done
15.217 +
15.218 +lemma real_minus:
15.219 + "- (Abs_REAL(realrel``{(x,y)})) = Abs_REAL(realrel `` {(y,x)})"
15.220 +apply (unfold real_minus_def)
15.221 +apply (rule_tac f = Abs_REAL in arg_cong)
15.222 +apply (simp add: realrel_in_real [THEN Abs_REAL_inverse]
15.223 + UN_equiv_class [OF equiv_realrel real_minus_congruent])
15.224 +done
15.225 +
15.226 +lemma real_minus_minus: "- (- z) = (z::real)"
15.227 +apply (rule_tac z = z in eq_Abs_REAL)
15.228 +apply (simp add: real_minus)
15.229 +done
15.230 +
15.231 +declare real_minus_minus [simp]
15.232 +
15.233 +lemma inj_real_minus: "inj(%r::real. -r)"
15.234 +apply (rule inj_onI)
15.235 +apply (drule_tac f = uminus in arg_cong)
15.236 +apply (simp add: real_minus_minus)
15.237 +done
15.238 +
15.239 +lemma real_minus_zero: "- 0 = (0::real)"
15.240 +apply (unfold real_zero_def)
15.241 +apply (simp add: real_minus)
15.242 +done
15.243 +
15.244 +declare real_minus_zero [simp]
15.245 +
15.246 +lemma real_minus_zero_iff: "(-x = 0) = (x = (0::real))"
15.247 +apply (rule_tac z = x in eq_Abs_REAL)
15.248 +apply (auto simp add: real_zero_def real_minus preal_add_ac)
15.249 +done
15.250 +
15.251 +declare real_minus_zero_iff [simp]
15.252 +
15.253 +(*** Congruence property for addition ***)
15.254 +
15.255 +lemma real_add_congruent2_lemma:
15.256 + "[|a + ba = aa + b; ab + bc = ac + bb|]
15.257 + ==> a + ab + (ba + bc) = aa + ac + (b + (bb::preal))"
15.258 +apply (simp add: preal_add_assoc)
15.259 +apply (rule preal_add_left_commute [of ab, THEN ssubst])
15.260 +apply (simp add: preal_add_assoc [symmetric])
15.261 +apply (simp add: preal_add_ac)
15.262 +done
15.263 +
15.264 +lemma real_add:
15.265 + "Abs_REAL(realrel``{(x1,y1)}) + Abs_REAL(realrel``{(x2,y2)}) =
15.266 + Abs_REAL(realrel``{(x1+x2, y1+y2)})"
15.267 +apply (simp add: real_add_def UN_UN_split_split_eq)
15.268 +apply (subst equiv_realrel [THEN UN_equiv_class2])
15.269 +apply (auto simp add: congruent2_def)
15.270 +apply (blast intro: real_add_congruent2_lemma)
15.271 +done
15.272 +
15.273 +lemma real_add_commute: "(z::real) + w = w + z"
15.274 +apply (rule_tac z = z in eq_Abs_REAL)
15.275 +apply (rule_tac z = w in eq_Abs_REAL)
15.276 +apply (simp add: preal_add_ac real_add)
15.277 +done
15.278 +
15.279 +lemma real_add_assoc: "((z1::real) + z2) + z3 = z1 + (z2 + z3)"
15.280 +apply (rule_tac z = z1 in eq_Abs_REAL)
15.281 +apply (rule_tac z = z2 in eq_Abs_REAL)
15.282 +apply (rule_tac z = z3 in eq_Abs_REAL)
15.283 +apply (simp add: real_add preal_add_assoc)
15.284 +done
15.285 +
15.286 +(*For AC rewriting*)
15.287 +lemma real_add_left_commute: "(x::real)+(y+z)=y+(x+z)"
15.288 + apply (rule mk_left_commute [of "op +"])
15.289 + apply (rule real_add_assoc)
15.290 + apply (rule real_add_commute)
15.291 + done
15.292 +
15.293 +
15.294 +(* real addition is an AC operator *)
15.295 +lemmas real_add_ac = real_add_assoc real_add_commute real_add_left_commute
15.296 +
15.297 +lemma real_add_zero_left: "(0::real) + z = z"
15.298 +apply (unfold real_of_preal_def real_zero_def)
15.299 +apply (rule_tac z = z in eq_Abs_REAL)
15.300 +apply (simp add: real_add preal_add_ac)
15.301 +done
15.302 +declare real_add_zero_left [simp]
15.303 +
15.304 +lemma real_add_zero_right: "z + (0::real) = z"
15.305 +by (simp add: real_add_commute)
15.306 +declare real_add_zero_right [simp]
15.307 +
15.308 +instance real :: plus_ac0
15.309 + by (intro_classes,
15.310 + (assumption |
15.311 + rule real_add_commute real_add_assoc real_add_zero_left)+)
15.312 +
15.313 +
15.314 +lemma real_add_minus: "z + (-z) = (0::real)"
15.315 +apply (unfold real_zero_def)
15.316 +apply (rule_tac z = z in eq_Abs_REAL)
15.317 +apply (simp add: real_minus real_add preal_add_commute)
15.318 +done
15.319 +declare real_add_minus [simp]
15.320 +
15.321 +lemma real_add_minus_left: "(-z) + z = (0::real)"
15.322 +by (simp add: real_add_commute)
15.323 +declare real_add_minus_left [simp]
15.324 +
15.325 +
15.326 +lemma real_add_minus_cancel: "z + ((- z) + w) = (w::real)"
15.327 +by (simp add: real_add_assoc [symmetric])
15.328 +
15.329 +lemma real_minus_add_cancel: "(-z) + (z + w) = (w::real)"
15.330 +by (simp add: real_add_assoc [symmetric])
15.331 +
15.332 +declare real_add_minus_cancel [simp] real_minus_add_cancel [simp]
15.333 +
15.334 +lemma real_minus_ex: "\<exists>y. (x::real) + y = 0"
15.335 +by (blast intro: real_add_minus)
15.336 +
15.337 +lemma real_minus_ex1: "EX! y. (x::real) + y = 0"
15.338 +apply (auto intro: real_add_minus)
15.339 +apply (drule_tac f = "%x. ya+x" in arg_cong)
15.340 +apply (simp add: real_add_assoc [symmetric])
15.341 +apply (simp add: real_add_commute)
15.342 +done
15.343 +
15.344 +lemma real_minus_left_ex1: "EX! y. y + (x::real) = 0"
15.345 +apply (auto intro: real_add_minus_left)
15.346 +apply (drule_tac f = "%x. x+ya" in arg_cong)
15.347 +apply (simp add: real_add_assoc)
15.348 +apply (simp add: real_add_commute)
15.349 +done
15.350 +
15.351 +lemma real_add_minus_eq_minus: "x + y = (0::real) ==> x = -y"
15.352 +apply (cut_tac z = y in real_add_minus_left)
15.353 +apply (rule_tac x1 = y in real_minus_left_ex1 [THEN ex1E], blast)
15.354 +done
15.355 +
15.356 +lemma real_as_add_inverse_ex: "\<exists>(y::real). x = -y"
15.357 +apply (cut_tac x = x in real_minus_ex)
15.358 +apply (erule exE, drule real_add_minus_eq_minus, fast)
15.359 +done
15.360 +
15.361 +lemma real_minus_add_distrib: "-(x + y) = (-x) + (- y :: real)"
15.362 +apply (rule_tac z = x in eq_Abs_REAL)
15.363 +apply (rule_tac z = y in eq_Abs_REAL)
15.364 +apply (auto simp add: real_minus real_add)
15.365 +done
15.366 +
15.367 +declare real_minus_add_distrib [simp]
15.368 +
15.369 +lemma real_add_left_cancel: "((x::real) + y = x + z) = (y = z)"
15.370 +apply safe
15.371 +apply (drule_tac f = "%t. (-x) + t" in arg_cong)
15.372 +apply (simp add: real_add_assoc [symmetric])
15.373 +done
15.374 +
15.375 +lemma real_add_right_cancel: "(y + (x::real)= z + x) = (y = z)"
15.376 +by (simp add: real_add_commute real_add_left_cancel)
15.377 +
15.378 +lemma real_diff_0: "(0::real) - x = -x"
15.379 +by (simp add: real_diff_def)
15.380 +
15.381 +lemma real_diff_0_right: "x - (0::real) = x"
15.382 +by (simp add: real_diff_def)
15.383 +
15.384 +lemma real_diff_self: "x - x = (0::real)"
15.385 +by (simp add: real_diff_def)
15.386 +
15.387 +declare real_diff_0 [simp] real_diff_0_right [simp] real_diff_self [simp]
15.388 +
15.389 +
15.390 +(*** Congruence property for multiplication ***)
15.391 +
15.392 +lemma real_mult_congruent2_lemma: "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==>
15.393 + x * x1 + y * y1 + (x * y2 + x2 * y) =
15.394 + x * x2 + y * y2 + (x * y1 + x1 * y)"
15.395 +apply (simp add: preal_add_left_commute preal_add_assoc [symmetric] preal_add_mult_distrib2 [symmetric])
15.396 +apply (rule preal_mult_commute [THEN subst])
15.397 +apply (rule_tac y1 = x2 in preal_mult_commute [THEN subst])
15.398 +apply (simp add: preal_add_assoc preal_add_mult_distrib2 [symmetric])
15.399 +apply (simp add: preal_add_commute)
15.400 +done
15.401 +
15.402 +lemma real_mult_congruent2:
15.403 + "congruent2 realrel (%p1 p2.
15.404 + (%(x1,y1). (%(x2,y2). realrel``{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)"
15.405 +apply (rule equiv_realrel [THEN congruent2_commuteI], clarify)
15.406 +apply (unfold split_def)
15.407 +apply (simp add: preal_mult_commute preal_add_commute)
15.408 +apply (auto simp add: real_mult_congruent2_lemma)
15.409 +done
15.410 +
15.411 +lemma real_mult:
15.412 + "Abs_REAL((realrel``{(x1,y1)})) * Abs_REAL((realrel``{(x2,y2)})) =
15.413 + Abs_REAL(realrel `` {(x1*x2+y1*y2,x1*y2+x2*y1)})"
15.414 +apply (unfold real_mult_def)
15.415 +apply (simp add: equiv_realrel [THEN UN_equiv_class2] real_mult_congruent2)
15.416 +done
15.417 +
15.418 +lemma real_mult_commute: "(z::real) * w = w * z"
15.419 +apply (rule_tac z = z in eq_Abs_REAL)
15.420 +apply (rule_tac z = w in eq_Abs_REAL)
15.421 +apply (simp add: real_mult preal_add_ac preal_mult_ac)
15.422 +done
15.423 +
15.424 +lemma real_mult_assoc: "((z1::real) * z2) * z3 = z1 * (z2 * z3)"
15.425 +apply (rule_tac z = z1 in eq_Abs_REAL)
15.426 +apply (rule_tac z = z2 in eq_Abs_REAL)
15.427 +apply (rule_tac z = z3 in eq_Abs_REAL)
15.428 +apply (simp add: preal_add_mult_distrib2 real_mult preal_add_ac preal_mult_ac)
15.429 +done
15.430 +
15.431 +
15.432 +(*For AC rewriting*)
15.433 +lemma real_mult_left_commute: "(x::real)*(y*z)=y*(x*z)"
15.434 + apply (rule mk_left_commute [of "op *"])
15.435 + apply (rule real_mult_assoc)
15.436 + apply (rule real_mult_commute)
15.437 + done
15.438 +
15.439 +(* real multiplication is an AC operator *)
15.440 +lemmas real_mult_ac = real_mult_assoc real_mult_commute real_mult_left_commute
15.441 +
15.442 +lemma real_mult_1: "(1::real) * z = z"
15.443 +apply (unfold real_one_def pnat_one_def)
15.444 +apply (rule_tac z = z in eq_Abs_REAL)
15.445 +apply (simp add: real_mult preal_add_mult_distrib2 preal_mult_1_right preal_mult_ac preal_add_ac)
15.446 +done
15.447 +
15.448 +declare real_mult_1 [simp]
15.449 +
15.450 +lemma real_mult_1_right: "z * (1::real) = z"
15.451 +by (simp add: real_mult_commute)
15.452 +
15.453 +declare real_mult_1_right [simp]
15.454 +
15.455 +lemma real_mult_0: "0 * z = (0::real)"
15.456 +apply (unfold real_zero_def pnat_one_def)
15.457 +apply (rule_tac z = z in eq_Abs_REAL)
15.458 +apply (simp add: real_mult preal_add_mult_distrib2 preal_mult_1_right preal_mult_ac preal_add_ac)
15.459 +done
15.460 +
15.461 +lemma real_mult_0_right: "z * 0 = (0::real)"
15.462 +by (simp add: real_mult_commute real_mult_0)
15.463 +
15.464 +declare real_mult_0_right [simp] real_mult_0 [simp]
15.465 +
15.466 +lemma real_mult_minus_eq1: "(-x) * (y::real) = -(x * y)"
15.467 +apply (rule_tac z = x in eq_Abs_REAL)
15.468 +apply (rule_tac z = y in eq_Abs_REAL)
15.469 +apply (auto simp add: real_minus real_mult preal_mult_ac preal_add_ac)
15.470 +done
15.471 +declare real_mult_minus_eq1 [simp]
15.472 +
15.473 +lemmas real_minus_mult_eq1 = real_mult_minus_eq1 [symmetric, standard]
15.474 +
15.475 +lemma real_mult_minus_eq2: "x * (- y :: real) = -(x * y)"
15.476 +by (simp add: real_mult_commute [of x])
15.477 +declare real_mult_minus_eq2 [simp]
15.478 +
15.479 +lemmas real_minus_mult_eq2 = real_mult_minus_eq2 [symmetric, standard]
15.480 +
15.481 +lemma real_mult_minus_1: "(- (1::real)) * z = -z"
15.482 +by simp
15.483 +declare real_mult_minus_1 [simp]
15.484 +
15.485 +lemma real_mult_minus_1_right: "z * (- (1::real)) = -z"
15.486 +by (subst real_mult_commute, simp)
15.487 +declare real_mult_minus_1_right [simp]
15.488 +
15.489 +lemma real_minus_mult_cancel: "(-x) * (-y) = x * (y::real)"
15.490 +by simp
15.491 +
15.492 +declare real_minus_mult_cancel [simp]
15.493 +
15.494 +lemma real_minus_mult_commute: "(-x) * y = x * (- y :: real)"
15.495 +by simp
15.496 +
15.497 +(** Lemmas **)
15.498 +
15.499 +lemma real_add_assoc_cong: "(z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
15.500 +by (simp add: real_add_assoc [symmetric])
15.501 +
15.502 +lemma real_add_mult_distrib: "((z1::real) + z2) * w = (z1 * w) + (z2 * w)"
15.503 +apply (rule_tac z = z1 in eq_Abs_REAL)
15.504 +apply (rule_tac z = z2 in eq_Abs_REAL)
15.505 +apply (rule_tac z = w in eq_Abs_REAL)
15.506 +apply (simp add: preal_add_mult_distrib2 real_add real_mult preal_add_ac preal_mult_ac)
15.507 +done
15.508 +
15.509 +lemma real_add_mult_distrib2: "(w::real) * (z1 + z2) = (w * z1) + (w * z2)"
15.510 +by (simp add: real_mult_commute [of w] real_add_mult_distrib)
15.511 +
15.512 +lemma real_diff_mult_distrib: "((z1::real) - z2) * w = (z1 * w) - (z2 * w)"
15.513 +apply (unfold real_diff_def)
15.514 +apply (simp add: real_add_mult_distrib)
15.515 +done
15.516 +
15.517 +lemma real_diff_mult_distrib2: "(w::real) * (z1 - z2) = (w * z1) - (w * z2)"
15.518 +by (simp add: real_mult_commute [of w] real_diff_mult_distrib)
15.519 +
15.520 +(*** one and zero are distinct ***)
15.521 +lemma real_zero_not_eq_one: "0 ~= (1::real)"
15.522 +apply (unfold real_zero_def real_one_def)
15.523 +apply (auto simp add: preal_self_less_add_left [THEN preal_not_refl2])
15.524 +done
15.525 +
15.526 +(*** existence of inverse ***)
15.527 +(** lemma -- alternative definition of 0 **)
15.528 +lemma real_zero_iff: "0 = Abs_REAL (realrel `` {(x, x)})"
15.529 +apply (unfold real_zero_def)
15.530 +apply (auto simp add: preal_add_commute)
15.531 +done
15.532 +
15.533 +
15.534 +(*MOVE UP*)
15.535 +instance preal :: order
15.536 + by (intro_classes,
15.537 + (assumption |
15.538 + rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+)
15.539 +
15.540 +lemma preal_le_linear: "x <= y | y <= (x::preal)"
15.541 +apply (insert preal_linear [of x y])
15.542 +apply (auto simp add: order_less_le)
15.543 +done
15.544 +
15.545 +instance preal :: linorder
15.546 + by (intro_classes, rule preal_le_linear)
15.547 +
15.548 +
15.549 +lemma real_mult_inv_right_ex:
15.550 + "!!(x::real). x ~= 0 ==> \<exists>y. x*y = (1::real)"
15.551 +apply (unfold real_zero_def real_one_def)
15.552 +apply (rule_tac z = x in eq_Abs_REAL)
15.553 +apply (cut_tac x = xa and y = y in linorder_less_linear)
15.554 +apply (auto dest!: preal_less_add_left_Ex simp add: real_zero_iff [symmetric])
15.555 +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)
15.556 +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)
15.557 +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)
15.558 +done
15.559 +
15.560 +lemma real_mult_inv_left_ex: "x ~= 0 ==> \<exists>y. y*x = (1::real)"
15.561 +apply (drule real_mult_inv_right_ex)
15.562 +apply (auto simp add: real_mult_commute)
15.563 +done
15.564 +
15.565 +lemma real_mult_inv_left: "x ~= 0 ==> inverse(x)*x = (1::real)"
15.566 +apply (unfold real_inverse_def)
15.567 +apply (frule real_mult_inv_left_ex, safe)
15.568 +apply (rule someI2, auto)
15.569 +done
15.570 +declare real_mult_inv_left [simp]
15.571 +
15.572 +lemma real_mult_inv_right: "x ~= 0 ==> x*inverse(x) = (1::real)"
15.573 +apply (subst real_mult_commute)
15.574 +apply (auto simp add: real_mult_inv_left)
15.575 +done
15.576 +declare real_mult_inv_right [simp]
15.577 +
15.578 +
15.579 +(*---------------------------------------------------------
15.580 + Theorems for ordering
15.581 + --------------------------------------------------------*)
15.582 +(* prove introduction and elimination rules for real_less *)
15.583 +
15.584 +(* real_less is a strong order i.e. nonreflexive and transitive *)
15.585 +
15.586 +(*** lemmas ***)
15.587 +lemma preal_lemma_eq_rev_sum: "!!(x::preal). [| x = y; x1 = y1 |] ==> x + y1 = x1 + y"
15.588 +by (simp add: preal_add_commute)
15.589 +
15.590 +lemma preal_add_left_commute_cancel: "!!(b::preal). x + (b + y) = x1 + (b + y1) ==> x + y = x1 + y1"
15.591 +by (simp add: preal_add_ac)
15.592 +
15.593 +lemma preal_lemma_for_not_refl: "!!(x::preal). [| x + y2a = x2a + y;
15.594 + x + y2b = x2b + y |]
15.595 + ==> x2a + y2b = x2b + y2a"
15.596 +apply (drule preal_lemma_eq_rev_sum, assumption)
15.597 +apply (erule_tac V = "x + y2b = x2b + y" in thin_rl)
15.598 +apply (simp add: preal_add_ac)
15.599 +apply (drule preal_add_left_commute_cancel)
15.600 +apply (simp add: preal_add_ac)
15.601 +done
15.602 +
15.603 +lemma real_less_not_refl: "~ (R::real) < R"
15.604 +apply (rule_tac z = R in eq_Abs_REAL)
15.605 +apply (auto simp add: real_less_def)
15.606 +apply (drule preal_lemma_for_not_refl, assumption, auto)
15.607 +done
15.608 +
15.609 +(*** y < y ==> P ***)
15.610 +lemmas real_less_irrefl = real_less_not_refl [THEN notE, standard]
15.611 +declare real_less_irrefl [elim!]
15.612 +
15.613 +lemma real_not_refl2: "!!(x::real). x < y ==> x ~= y"
15.614 +by (auto simp add: real_less_not_refl)
15.615 +
15.616 +(* lemma re-arranging and eliminating terms *)
15.617 +lemma preal_lemma_trans: "!! (a::preal). [| a + b = c + d;
15.618 + x2b + d + (c + y2e) < a + y2b + (x2e + b) |]
15.619 + ==> x2b + y2e < x2e + y2b"
15.620 +apply (simp add: preal_add_ac)
15.621 +apply (rule_tac C = "c+d" in preal_add_left_less_cancel)
15.622 +apply (simp add: preal_add_assoc [symmetric])
15.623 +done
15.624 +
15.625 +(** A MESS! heavy re-writing involved*)
15.626 +lemma real_less_trans: "!!(R1::real). [| R1 < R2; R2 < R3 |] ==> R1 < R3"
15.627 +apply (rule_tac z = R1 in eq_Abs_REAL)
15.628 +apply (rule_tac z = R2 in eq_Abs_REAL)
15.629 +apply (rule_tac z = R3 in eq_Abs_REAL)
15.630 +apply (auto simp add: real_less_def)
15.631 +apply (rule exI)+
15.632 +apply (rule conjI, rule_tac [2] conjI)
15.633 + prefer 2 apply blast
15.634 + prefer 2 apply blast
15.635 +apply (drule preal_lemma_for_not_refl, assumption)
15.636 +apply (blast dest: preal_add_less_mono intro: preal_lemma_trans)
15.637 +done
15.638 +
15.639 +lemma real_less_not_sym: "!! (R1::real). R1 < R2 ==> ~ (R2 < R1)"
15.640 +apply (rule notI)
15.641 +apply (drule real_less_trans, assumption)
15.642 +apply (simp add: real_less_not_refl)
15.643 +done
15.644 +
15.645 +(* [| x < y; ~P ==> y < x |] ==> P *)
15.646 +lemmas real_less_asym = real_less_not_sym [THEN contrapos_np, standard]
15.647 +
15.648 +lemma real_of_preal_add:
15.649 + "real_of_preal ((z1::preal) + z2) =
15.650 + real_of_preal z1 + real_of_preal z2"
15.651 +apply (unfold real_of_preal_def)
15.652 +apply (simp add: real_add preal_add_mult_distrib preal_mult_1 add: preal_add_ac)
15.653 +done
15.654 +
15.655 +lemma real_of_preal_mult:
15.656 + "real_of_preal ((z1::preal) * z2) =
15.657 + real_of_preal z1* real_of_preal z2"
15.658 +apply (unfold real_of_preal_def)
15.659 +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)
15.660 +done
15.661 +
15.662 +lemma real_of_preal_ExI:
15.663 + "!!(x::preal). y < x ==>
15.664 + \<exists>m. Abs_REAL (realrel `` {(x,y)}) = real_of_preal m"
15.665 +apply (unfold real_of_preal_def)
15.666 +apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_ac)
15.667 +done
15.668 +
15.669 +lemma real_of_preal_ExD:
15.670 + "!!(x::preal). \<exists>m. Abs_REAL (realrel `` {(x,y)}) =
15.671 + real_of_preal m ==> y < x"
15.672 +apply (unfold real_of_preal_def)
15.673 +apply (auto simp add: preal_add_commute preal_add_assoc)
15.674 +apply (simp add: preal_add_assoc [symmetric] preal_self_less_add_left)
15.675 +done
15.676 +
15.677 +lemma real_of_preal_iff: "(\<exists>m. Abs_REAL (realrel `` {(x,y)}) = real_of_preal m) = (y < x)"
15.678 +by (blast intro!: real_of_preal_ExI real_of_preal_ExD)
15.679 +
15.680 +(*** Gleason prop 9-4.4 p 127 ***)
15.681 +lemma real_of_preal_trichotomy:
15.682 + "\<exists>m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)"
15.683 +apply (unfold real_of_preal_def real_zero_def)
15.684 +apply (rule_tac z = x in eq_Abs_REAL)
15.685 +apply (auto simp add: real_minus preal_add_ac)
15.686 +apply (cut_tac x = x and y = y in linorder_less_linear)
15.687 +apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_assoc [symmetric])
15.688 +apply (auto simp add: preal_add_commute)
15.689 +done
15.690 +
15.691 +lemma real_of_preal_trichotomyE: "!!P. [| !!m. x = real_of_preal m ==> P;
15.692 + x = 0 ==> P;
15.693 + !!m. x = -(real_of_preal m) ==> P |] ==> P"
15.694 +apply (cut_tac x = x in real_of_preal_trichotomy, auto)
15.695 +done
15.696 +
15.697 +lemma real_of_preal_lessD:
15.698 + "real_of_preal m1 < real_of_preal m2 ==> m1 < m2"
15.699 +apply (unfold real_of_preal_def)
15.700 +apply (auto simp add: real_less_def preal_add_ac)
15.701 +apply (auto simp add: preal_add_assoc [symmetric])
15.702 +apply (auto simp add: preal_add_ac)
15.703 +done
15.704 +
15.705 +lemma real_of_preal_lessI: "m1 < m2 ==> real_of_preal m1 < real_of_preal m2"
15.706 +apply (drule preal_less_add_left_Ex)
15.707 +apply (auto simp add: real_of_preal_add real_of_preal_def real_less_def)
15.708 +apply (rule exI)+
15.709 +apply (rule conjI, rule_tac [2] conjI)
15.710 + apply (rule_tac [2] refl)+
15.711 +apply (simp add: preal_self_less_add_left del: preal_add_less_iff2)
15.712 +done
15.713 +
15.714 +lemma real_of_preal_less_iff1: "(real_of_preal m1 < real_of_preal m2) = (m1 < m2)"
15.715 +by (blast intro: real_of_preal_lessI real_of_preal_lessD)
15.716 +
15.717 +declare real_of_preal_less_iff1 [simp]
15.718 +
15.719 +lemma real_of_preal_minus_less_self: "- real_of_preal m < real_of_preal m"
15.720 +apply (auto simp add: real_of_preal_def real_less_def real_minus)
15.721 +apply (rule exI)+
15.722 +apply (rule conjI, rule_tac [2] conjI)
15.723 + apply (rule_tac [2] refl)+
15.724 +apply (simp (no_asm_use) add: preal_add_ac)
15.725 +apply (simp (no_asm_use) add: preal_self_less_add_right preal_add_assoc [symmetric])
15.726 +done
15.727 +
15.728 +lemma real_of_preal_minus_less_zero: "- real_of_preal m < 0"
15.729 +apply (unfold real_zero_def)
15.730 +apply (auto simp add: real_of_preal_def real_less_def real_minus)
15.731 +apply (rule exI)+
15.732 +apply (rule conjI, rule_tac [2] conjI)
15.733 + apply (rule_tac [2] refl)+
15.734 +apply (simp (no_asm_use) add: preal_self_less_add_right preal_add_ac)
15.735 +done
15.736 +
15.737 +lemma real_of_preal_not_minus_gt_zero: "~ 0 < - real_of_preal m"
15.738 +apply (cut_tac real_of_preal_minus_less_zero)
15.739 +apply (fast dest: real_less_trans elim: real_less_irrefl)
15.740 +done
15.741 +
15.742 +lemma real_of_preal_zero_less: "0 < real_of_preal m"
15.743 +apply (unfold real_zero_def)
15.744 +apply (auto simp add: real_of_preal_def real_less_def real_minus)
15.745 +apply (rule exI)+
15.746 +apply (rule conjI, rule_tac [2] conjI)
15.747 + apply (rule_tac [2] refl)+
15.748 +apply (simp (no_asm_use) add: preal_self_less_add_right preal_add_ac)
15.749 +done
15.750 +
15.751 +lemma real_of_preal_not_less_zero: "~ real_of_preal m < 0"
15.752 +apply (cut_tac real_of_preal_zero_less)
15.753 +apply (blast dest: real_less_trans elim: real_less_irrefl)
15.754 +done
15.755 +
15.756 +lemma real_minus_minus_zero_less: "0 < - (- real_of_preal m)"
15.757 +by (simp add: real_of_preal_zero_less)
15.758 +
15.759 +(* another lemma *)
15.760 +lemma real_of_preal_sum_zero_less:
15.761 + "0 < real_of_preal m + real_of_preal m1"
15.762 +apply (unfold real_zero_def)
15.763 +apply (auto simp add: real_of_preal_def real_less_def real_add)
15.764 +apply (rule exI)+
15.765 +apply (rule conjI, rule_tac [2] conjI)
15.766 + apply (rule_tac [2] refl)+
15.767 +apply (simp (no_asm_use) add: preal_add_ac)
15.768 +apply (simp (no_asm_use) add: preal_self_less_add_right preal_add_assoc [symmetric])
15.769 +done
15.770 +
15.771 +lemma real_of_preal_minus_less_all: "- real_of_preal m < real_of_preal m1"
15.772 +apply (auto simp add: real_of_preal_def real_less_def real_minus)
15.773 +apply (rule exI)+
15.774 +apply (rule conjI, rule_tac [2] conjI)
15.775 + apply (rule_tac [2] refl)+
15.776 +apply (simp (no_asm_use) add: preal_add_ac)
15.777 +apply (simp (no_asm_use) add: preal_self_less_add_right preal_add_assoc [symmetric])
15.778 +done
15.779 +
15.780 +lemma real_of_preal_not_minus_gt_all: "~ real_of_preal m < - real_of_preal m1"
15.781 +apply (cut_tac real_of_preal_minus_less_all)
15.782 +apply (blast dest: real_less_trans elim: real_less_irrefl)
15.783 +done
15.784 +
15.785 +lemma real_of_preal_minus_less_rev1: "- real_of_preal m1 < - real_of_preal m2
15.786 + ==> real_of_preal m2 < real_of_preal m1"
15.787 +apply (auto simp add: real_of_preal_def real_less_def real_minus)
15.788 +apply (rule exI)+
15.789 +apply (rule conjI, rule_tac [2] conjI)
15.790 + apply (rule_tac [2] refl)+
15.791 +apply (auto simp add: preal_add_ac)
15.792 +apply (simp add: preal_add_assoc [symmetric])
15.793 +apply (auto simp add: preal_add_ac)
15.794 +done
15.795 +
15.796 +lemma real_of_preal_minus_less_rev2: "real_of_preal m1 < real_of_preal m2
15.797 + ==> - real_of_preal m2 < - real_of_preal m1"
15.798 +apply (auto simp add: real_of_preal_def real_less_def real_minus)
15.799 +apply (rule exI)+
15.800 +apply (rule conjI, rule_tac [2] conjI)
15.801 + apply (rule_tac [2] refl)+
15.802 +apply (auto simp add: preal_add_ac)
15.803 +apply (simp add: preal_add_assoc [symmetric])
15.804 +apply (auto simp add: preal_add_ac)
15.805 +done
15.806 +
15.807 +lemma real_of_preal_minus_less_rev_iff: "(- real_of_preal m1 < - real_of_preal m2) =
15.808 + (real_of_preal m2 < real_of_preal m1)"
15.809 +apply (blast intro!: real_of_preal_minus_less_rev1 real_of_preal_minus_less_rev2)
15.810 +done
15.811 +
15.812 +declare real_of_preal_minus_less_rev_iff [simp]
15.813 +
15.814 +(*** linearity ***)
15.815 +lemma real_linear: "(x::real) < y | x = y | y < x"
15.816 +apply (rule_tac x = x in real_of_preal_trichotomyE)
15.817 +apply (rule_tac [!] x = y in real_of_preal_trichotomyE)
15.818 +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)
15.819 +done
15.820 +
15.821 +lemma real_neq_iff: "!!w::real. (w ~= z) = (w<z | z<w)"
15.822 +by (cut_tac real_linear, blast)
15.823 +
15.824 +
15.825 +lemma real_linear_less2: "!!(R1::real). [| R1 < R2 ==> P; R1 = R2 ==> P;
15.826 + R2 < R1 ==> P |] ==> P"
15.827 +apply (cut_tac x = R1 and y = R2 in real_linear, auto)
15.828 +done
15.829 +
15.830 +(*** Properties of <= ***)
15.831 +
15.832 +lemma real_leI: "~(w < z) ==> z \<le> (w::real)"
15.833 +
15.834 +apply (unfold real_le_def, assumption)
15.835 +done
15.836 +
15.837 +lemma real_leD: "z\<le>w ==> ~(w<(z::real))"
15.838 +by (unfold real_le_def, assumption)
15.839 +
15.840 +lemmas real_leE = real_leD [elim_format]
15.841 +
15.842 +lemma real_less_le_iff: "(~(w < z)) = (z \<le> (w::real))"
15.843 +by (blast intro!: real_leI real_leD)
15.844 +
15.845 +lemma not_real_leE: "~ z \<le> w ==> w<(z::real)"
15.846 +by (unfold real_le_def, blast)
15.847 +
15.848 +lemma real_le_imp_less_or_eq: "!!(x::real). x \<le> y ==> x < y | x = y"
15.849 +apply (unfold real_le_def)
15.850 +apply (cut_tac real_linear)
15.851 +apply (blast elim: real_less_irrefl real_less_asym)
15.852 +done
15.853 +
15.854 +lemma real_less_or_eq_imp_le: "z<w | z=w ==> z \<le>(w::real)"
15.855 +apply (unfold real_le_def)
15.856 +apply (cut_tac real_linear)
15.857 +apply (fast elim: real_less_irrefl real_less_asym)
15.858 +done
15.859 +
15.860 +lemma real_le_less: "(x \<le> (y::real)) = (x < y | x=y)"
15.861 +by (blast intro!: real_less_or_eq_imp_le dest!: real_le_imp_less_or_eq)
15.862 +
15.863 +lemma real_le_refl: "w \<le> (w::real)"
15.864 +by (simp add: real_le_less)
15.865 +
15.866 +lemma real_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::real)"
15.867 +apply (drule real_le_imp_less_or_eq)
15.868 +apply (drule real_le_imp_less_or_eq)
15.869 +apply (rule real_less_or_eq_imp_le)
15.870 +apply (blast intro: real_less_trans)
15.871 +done
15.872 +
15.873 +lemma real_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::real)"
15.874 +apply (drule real_le_imp_less_or_eq)
15.875 +apply (drule real_le_imp_less_or_eq)
15.876 +apply (fast elim: real_less_irrefl real_less_asym)
15.877 +done
15.878 +
15.879 +(* Axiom 'order_less_le' of class 'order': *)
15.880 +lemma real_less_le: "((w::real) < z) = (w \<le> z & w ~= z)"
15.881 +apply (simp add: real_le_def real_neq_iff)
15.882 +apply (blast elim!: real_less_asym)
15.883 +done
15.884 +
15.885 +instance real :: order
15.886 + by (intro_classes,
15.887 + (assumption |
15.888 + rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+)
15.889 +
15.890 +(* Axiom 'linorder_linear' of class 'linorder': *)
15.891 +lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
15.892 +apply (simp add: real_le_less)
15.893 +apply (cut_tac real_linear, blast)
15.894 +done
15.895 +
15.896 +instance real :: linorder
15.897 + by (intro_classes, rule real_le_linear)
15.898 +
15.899 +
15.900 +lemma real_minus_zero_less_iff: "(0 < -R) = (R < (0::real))"
15.901 +apply (rule_tac x = R in real_of_preal_trichotomyE)
15.902 +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)
15.903 +done
15.904 +declare real_minus_zero_less_iff [simp]
15.905 +
15.906 +lemma real_minus_zero_less_iff2: "(-R < 0) = ((0::real) < R)"
15.907 +apply (rule_tac x = R in real_of_preal_trichotomyE)
15.908 +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)
15.909 +done
15.910 +declare real_minus_zero_less_iff2 [simp]
15.911 +
15.912 +(*Alternative definition for real_less*)
15.913 +lemma real_less_add_positive_left_Ex: "R < S ==> \<exists>T::real. 0 < T & R + T = S"
15.914 +apply (rule_tac x = R in real_of_preal_trichotomyE)
15.915 +apply (rule_tac [!] x = S in real_of_preal_trichotomyE)
15.916 +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)
15.917 +apply (rule_tac x = "real_of_preal D" in exI)
15.918 +apply (rule_tac [2] x = "real_of_preal m+real_of_preal ma" in exI)
15.919 +apply (rule_tac [3] x = "real_of_preal D" in exI)
15.920 +apply (auto simp add: real_of_preal_zero_less real_of_preal_sum_zero_less real_add_assoc)
15.921 +done
15.922 +
15.923 +(** change naff name(s)! **)
15.924 +lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (-W::real))"
15.925 +apply (drule real_less_add_positive_left_Ex)
15.926 +apply (auto simp add: real_add_minus real_add_zero_right real_add_ac)
15.927 +done
15.928 +
15.929 +lemma real_lemma_change_eq_subj: "!!S::real. T = S + W ==> S = T + (-W)"
15.930 +by (simp add: real_add_ac)
15.931 +
15.932 +(* FIXME: long! *)
15.933 +lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) ==> (W < S)"
15.934 +apply (rule ccontr)
15.935 +apply (drule real_leI [THEN real_le_imp_less_or_eq])
15.936 +apply (auto simp add: real_less_not_refl)
15.937 +apply (drule real_less_add_positive_left_Ex, clarify, simp)
15.938 +apply (drule real_lemma_change_eq_subj, auto)
15.939 +apply (drule real_less_sum_gt_zero)
15.940 +apply (auto elim: real_less_asym simp add: real_add_left_commute [of W] real_add_ac)
15.941 +done
15.942 +
15.943 +lemma real_less_sum_gt_0_iff: "(0 < S + (-W::real)) = (W < S)"
15.944 +by (blast intro: real_less_sum_gt_zero real_sum_gt_zero_less)
15.945 +
15.946 +
15.947 +lemma real_less_eq_diff: "(x<y) = (x-y < (0::real))"
15.948 +apply (unfold real_diff_def)
15.949 +apply (subst real_minus_zero_less_iff [symmetric])
15.950 +apply (simp add: real_add_commute real_less_sum_gt_0_iff)
15.951 +done
15.952 +
15.953 +
15.954 +(*** Subtraction laws ***)
15.955 +
15.956 +lemma real_add_diff_eq: "x + (y - z) = (x + y) - (z::real)"
15.957 +by (simp add: real_diff_def real_add_ac)
15.958 +
15.959 +lemma real_diff_add_eq: "(x - y) + z = (x + z) - (y::real)"
15.960 +by (simp add: real_diff_def real_add_ac)
15.961 +
15.962 +lemma real_diff_diff_eq: "(x - y) - z = x - (y + (z::real))"
15.963 +by (simp add: real_diff_def real_add_ac)
15.964 +
15.965 +lemma real_diff_diff_eq2: "x - (y - z) = (x + z) - (y::real)"
15.966 +by (simp add: real_diff_def real_add_ac)
15.967 +
15.968 +lemma real_diff_less_eq: "(x-y < z) = (x < z + (y::real))"
15.969 +apply (subst real_less_eq_diff)
15.970 +apply (rule_tac y1 = z in real_less_eq_diff [THEN ssubst])
15.971 +apply (simp add: real_diff_def real_add_ac)
15.972 +done
15.973 +
15.974 +lemma real_less_diff_eq: "(x < z-y) = (x + (y::real) < z)"
15.975 +apply (subst real_less_eq_diff)
15.976 +apply (rule_tac y1 = "z-y" in real_less_eq_diff [THEN ssubst])
15.977 +apply (simp add: real_diff_def real_add_ac)
15.978 +done
15.979 +
15.980 +lemma real_diff_le_eq: "(x-y \<le> z) = (x \<le> z + (y::real))"
15.981 +apply (unfold real_le_def)
15.982 +apply (simp add: real_less_diff_eq)
15.983 +done
15.984 +
15.985 +lemma real_le_diff_eq: "(x \<le> z-y) = (x + (y::real) \<le> z)"
15.986 +apply (unfold real_le_def)
15.987 +apply (simp add: real_diff_less_eq)
15.988 +done
15.989 +
15.990 +lemma real_diff_eq_eq: "(x-y = z) = (x = z + (y::real))"
15.991 +apply (unfold real_diff_def)
15.992 +apply (auto simp add: real_add_assoc)
15.993 +done
15.994 +
15.995 +lemma real_eq_diff_eq: "(x = z-y) = (x + (y::real) = z)"
15.996 +apply (unfold real_diff_def)
15.997 +apply (auto simp add: real_add_assoc)
15.998 +done
15.999 +
15.1000 +(*This list of rewrites simplifies (in)equalities by bringing subtractions
15.1001 + to the top and then moving negative terms to the other side.
15.1002 + Use with real_add_ac*)
15.1003 +lemmas real_compare_rls =
15.1004 + real_diff_def [symmetric]
15.1005 + real_add_diff_eq real_diff_add_eq real_diff_diff_eq real_diff_diff_eq2
15.1006 + real_diff_less_eq real_less_diff_eq real_diff_le_eq real_le_diff_eq
15.1007 + real_diff_eq_eq real_eq_diff_eq
15.1008 +
15.1009 +
15.1010 +(** For the cancellation simproc.
15.1011 + The idea is to cancel like terms on opposite sides by subtraction **)
15.1012 +
15.1013 +lemma real_less_eqI: "(x::real) - y = x' - y' ==> (x<y) = (x'<y')"
15.1014 +apply (subst real_less_eq_diff)
15.1015 +apply (rule_tac y1 = y in real_less_eq_diff [THEN ssubst], simp)
15.1016 +done
15.1017 +
15.1018 +lemma real_le_eqI: "(x::real) - y = x' - y' ==> (y\<le>x) = (y'\<le>x')"
15.1019 +apply (drule real_less_eqI)
15.1020 +apply (simp add: real_le_def)
15.1021 +done
15.1022 +
15.1023 +lemma real_eq_eqI: "(x::real) - y = x' - y' ==> (x=y) = (x'=y')"
15.1024 +apply safe
15.1025 +apply (simp_all add: real_eq_diff_eq real_diff_eq_eq)
15.1026 +done
15.1027 +
15.1028 +
15.1029 +ML
15.1030 +{*
15.1031 +val real_le_def = thm "real_le_def";
15.1032 +val real_diff_def = thm "real_diff_def";
15.1033 +val real_divide_def = thm "real_divide_def";
15.1034 +val real_of_nat_def = thm "real_of_nat_def";
15.1035 +
15.1036 +val preal_trans_lemma = thm"preal_trans_lemma";
15.1037 +val realrel_iff = thm"realrel_iff";
15.1038 +val realrel_refl = thm"realrel_refl";
15.1039 +val equiv_realrel = thm"equiv_realrel";
15.1040 +val equiv_realrel_iff = thm"equiv_realrel_iff";
15.1041 +val realrel_in_real = thm"realrel_in_real";
15.1042 +val inj_on_Abs_REAL = thm"inj_on_Abs_REAL";
15.1043 +val eq_realrelD = thm"eq_realrelD";
15.1044 +val inj_Rep_REAL = thm"inj_Rep_REAL";
15.1045 +val inj_real_of_preal = thm"inj_real_of_preal";
15.1046 +val eq_Abs_REAL = thm"eq_Abs_REAL";
15.1047 +val real_minus_congruent = thm"real_minus_congruent";
15.1048 +val real_minus = thm"real_minus";
15.1049 +val real_minus_minus = thm"real_minus_minus";
15.1050 +val inj_real_minus = thm"inj_real_minus";
15.1051 +val real_minus_zero = thm"real_minus_zero";
15.1052 +val real_minus_zero_iff = thm"real_minus_zero_iff";
15.1053 +val real_add_congruent2_lemma = thm"real_add_congruent2_lemma";
15.1054 +val real_add = thm"real_add";
15.1055 +val real_add_commute = thm"real_add_commute";
15.1056 +val real_add_assoc = thm"real_add_assoc";
15.1057 +val real_add_left_commute = thm"real_add_left_commute";
15.1058 +val real_add_zero_left = thm"real_add_zero_left";
15.1059 +val real_add_zero_right = thm"real_add_zero_right";
15.1060 +val real_add_minus = thm"real_add_minus";
15.1061 +val real_add_minus_left = thm"real_add_minus_left";
15.1062 +val real_add_minus_cancel = thm"real_add_minus_cancel";
15.1063 +val real_minus_add_cancel = thm"real_minus_add_cancel";
15.1064 +val real_minus_ex = thm"real_minus_ex";
15.1065 +val real_minus_ex1 = thm"real_minus_ex1";
15.1066 +val real_minus_left_ex1 = thm"real_minus_left_ex1";
15.1067 +val real_add_minus_eq_minus = thm"real_add_minus_eq_minus";
15.1068 +val real_as_add_inverse_ex = thm"real_as_add_inverse_ex";
15.1069 +val real_minus_add_distrib = thm"real_minus_add_distrib";
15.1070 +val real_add_left_cancel = thm"real_add_left_cancel";
15.1071 +val real_add_right_cancel = thm"real_add_right_cancel";
15.1072 +val real_diff_0 = thm"real_diff_0";
15.1073 +val real_diff_0_right = thm"real_diff_0_right";
15.1074 +val real_diff_self = thm"real_diff_self";
15.1075 +val real_mult_congruent2_lemma = thm"real_mult_congruent2_lemma";
15.1076 +val real_mult_congruent2 = thm"real_mult_congruent2";
15.1077 +val real_mult = thm"real_mult";
15.1078 +val real_mult_commute = thm"real_mult_commute";
15.1079 +val real_mult_assoc = thm"real_mult_assoc";
15.1080 +val real_mult_left_commute = thm"real_mult_left_commute";
15.1081 +val real_mult_1 = thm"real_mult_1";
15.1082 +val real_mult_1_right = thm"real_mult_1_right";
15.1083 +val real_mult_0 = thm"real_mult_0";
15.1084 +val real_mult_0_right = thm"real_mult_0_right";
15.1085 +val real_mult_minus_eq1 = thm"real_mult_minus_eq1";
15.1086 +val real_minus_mult_eq1 = thm"real_minus_mult_eq1";
15.1087 +val real_mult_minus_eq2 = thm"real_mult_minus_eq2";
15.1088 +val real_minus_mult_eq2 = thm"real_minus_mult_eq2";
15.1089 +val real_mult_minus_1 = thm"real_mult_minus_1";
15.1090 +val real_mult_minus_1_right = thm"real_mult_minus_1_right";
15.1091 +val real_minus_mult_cancel = thm"real_minus_mult_cancel";
15.1092 +val real_minus_mult_commute = thm"real_minus_mult_commute";
15.1093 +val real_add_assoc_cong = thm"real_add_assoc_cong";
15.1094 +val real_add_mult_distrib = thm"real_add_mult_distrib";
15.1095 +val real_add_mult_distrib2 = thm"real_add_mult_distrib2";
15.1096 +val real_diff_mult_distrib = thm"real_diff_mult_distrib";
15.1097 +val real_diff_mult_distrib2 = thm"real_diff_mult_distrib2";
15.1098 +val real_zero_not_eq_one = thm"real_zero_not_eq_one";
15.1099 +val real_zero_iff = thm"real_zero_iff";
15.1100 +val preal_le_linear = thm"preal_le_linear";
15.1101 +val real_mult_inv_right_ex = thm"real_mult_inv_right_ex";
15.1102 +val real_mult_inv_left_ex = thm"real_mult_inv_left_ex";
15.1103 +val real_mult_inv_left = thm"real_mult_inv_left";
15.1104 +val real_mult_inv_right = thm"real_mult_inv_right";
15.1105 +val preal_lemma_eq_rev_sum = thm"preal_lemma_eq_rev_sum";
15.1106 +val preal_add_left_commute_cancel = thm"preal_add_left_commute_cancel";
15.1107 +val preal_lemma_for_not_refl = thm"preal_lemma_for_not_refl";
15.1108 +val real_less_not_refl = thm"real_less_not_refl";
15.1109 +val real_less_irrefl = thm"real_less_irrefl";
15.1110 +val real_not_refl2 = thm"real_not_refl2";
15.1111 +val preal_lemma_trans = thm"preal_lemma_trans";
15.1112 +val real_less_trans = thm"real_less_trans";
15.1113 +val real_less_not_sym = thm"real_less_not_sym";
15.1114 +val real_less_asym = thm"real_less_asym";
15.1115 +val real_of_preal_add = thm"real_of_preal_add";
15.1116 +val real_of_preal_mult = thm"real_of_preal_mult";
15.1117 +val real_of_preal_ExI = thm"real_of_preal_ExI";
15.1118 +val real_of_preal_ExD = thm"real_of_preal_ExD";
15.1119 +val real_of_preal_iff = thm"real_of_preal_iff";
15.1120 +val real_of_preal_trichotomy = thm"real_of_preal_trichotomy";
15.1121 +val real_of_preal_trichotomyE = thm"real_of_preal_trichotomyE";
15.1122 +val real_of_preal_lessD = thm"real_of_preal_lessD";
15.1123 +val real_of_preal_lessI = thm"real_of_preal_lessI";
15.1124 +val real_of_preal_less_iff1 = thm"real_of_preal_less_iff1";
15.1125 +val real_of_preal_minus_less_self = thm"real_of_preal_minus_less_self";
15.1126 +val real_of_preal_minus_less_zero = thm"real_of_preal_minus_less_zero";
15.1127 +val real_of_preal_not_minus_gt_zero = thm"real_of_preal_not_minus_gt_zero";
15.1128 +val real_of_preal_zero_less = thm"real_of_preal_zero_less";
15.1129 +val real_of_preal_not_less_zero = thm"real_of_preal_not_less_zero";
15.1130 +val real_minus_minus_zero_less = thm"real_minus_minus_zero_less";
15.1131 +val real_of_preal_sum_zero_less = thm"real_of_preal_sum_zero_less";
15.1132 +val real_of_preal_minus_less_all = thm"real_of_preal_minus_less_all";
15.1133 +val real_of_preal_not_minus_gt_all = thm"real_of_preal_not_minus_gt_all";
15.1134 +val real_of_preal_minus_less_rev1 = thm"real_of_preal_minus_less_rev1";
15.1135 +val real_of_preal_minus_less_rev2 = thm"real_of_preal_minus_less_rev2";
15.1136 +val real_of_preal_minus_less_rev_iff = thm"real_of_preal_minus_less_rev_iff";
15.1137 +val real_linear = thm"real_linear";
15.1138 +val real_neq_iff = thm"real_neq_iff";
15.1139 +val real_linear_less2 = thm"real_linear_less2";
15.1140 +val real_leI = thm"real_leI";
15.1141 +val real_leD = thm"real_leD";
15.1142 +val real_leE = thm"real_leE";
15.1143 +val real_less_le_iff = thm"real_less_le_iff";
15.1144 +val not_real_leE = thm"not_real_leE";
15.1145 +val real_le_imp_less_or_eq = thm"real_le_imp_less_or_eq";
15.1146 +val real_less_or_eq_imp_le = thm"real_less_or_eq_imp_le";
15.1147 +val real_le_less = thm"real_le_less";
15.1148 +val real_le_refl = thm"real_le_refl";
15.1149 +val real_le_linear = thm"real_le_linear";
15.1150 +val real_le_trans = thm"real_le_trans";
15.1151 +val real_le_anti_sym = thm"real_le_anti_sym";
15.1152 +val real_less_le = thm"real_less_le";
15.1153 +val real_minus_zero_less_iff = thm"real_minus_zero_less_iff";
15.1154 +val real_minus_zero_less_iff2 = thm"real_minus_zero_less_iff2";
15.1155 +val real_less_add_positive_left_Ex = thm"real_less_add_positive_left_Ex";
15.1156 +val real_less_sum_gt_zero = thm"real_less_sum_gt_zero";
15.1157 +val real_lemma_change_eq_subj = thm"real_lemma_change_eq_subj";
15.1158 +val real_sum_gt_zero_less = thm"real_sum_gt_zero_less";
15.1159 +val real_less_sum_gt_0_iff = thm"real_less_sum_gt_0_iff";
15.1160 +val real_less_eq_diff = thm"real_less_eq_diff";
15.1161 +val real_add_diff_eq = thm"real_add_diff_eq";
15.1162 +val real_diff_add_eq = thm"real_diff_add_eq";
15.1163 +val real_diff_diff_eq = thm"real_diff_diff_eq";
15.1164 +val real_diff_diff_eq2 = thm"real_diff_diff_eq2";
15.1165 +val real_diff_less_eq = thm"real_diff_less_eq";
15.1166 +val real_less_diff_eq = thm"real_less_diff_eq";
15.1167 +val real_diff_le_eq = thm"real_diff_le_eq";
15.1168 +val real_le_diff_eq = thm"real_le_diff_eq";
15.1169 +val real_diff_eq_eq = thm"real_diff_eq_eq";
15.1170 +val real_eq_diff_eq = thm"real_eq_diff_eq";
15.1171 +val real_less_eqI = thm"real_less_eqI";
15.1172 +val real_le_eqI = thm"real_le_eqI";
15.1173 +val real_eq_eqI = thm"real_eq_eqI";
15.1174 +
15.1175 +val real_add_ac = thms"real_add_ac";
15.1176 +val real_mult_ac = thms"real_mult_ac";
15.1177 +val real_compare_rls = thms"real_compare_rls";
15.1178 +*}
15.1179 +
15.1180
15.1181 end
16.1 --- a/src/HOL/Real/RealInt.ML Thu Nov 27 10:47:55 2003 +0100
16.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
16.3 @@ -1,138 +0,0 @@
16.4 -(* Title: RealInt.ML
16.5 - ID: $Id$
16.6 - Author: Jacques D. Fleuriot
16.7 - Copyright: 1999 University of Edinburgh
16.8 - Description: Embedding the integers in the reals
16.9 -*)
16.10 -
16.11 -
16.12 -Goalw [congruent_def]
16.13 - "congruent intrel (%p. (%(i,j). realrel `` \
16.14 -\ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \
16.15 -\ preal_of_prat (prat_of_pnat (pnat_of_nat j)))}) p)";
16.16 -by (auto_tac (claset(),
16.17 - simpset() addsimps [pnat_of_nat_add, prat_of_pnat_add RS sym,
16.18 - preal_of_prat_add RS sym]));
16.19 -qed "real_of_int_congruent";
16.20 -
16.21 -Goalw [real_of_int_def]
16.22 - "real (Abs_Integ (intrel `` {(i, j)})) = \
16.23 -\ Abs_REAL(realrel `` \
16.24 -\ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \
16.25 -\ preal_of_prat (prat_of_pnat (pnat_of_nat j)))})";
16.26 -by (res_inst_tac [("f","Abs_REAL")] arg_cong 1);
16.27 -by (simp_tac (simpset() addsimps [realrel_in_real RS Abs_REAL_inverse,
16.28 - [equiv_intrel, real_of_int_congruent] MRS UN_equiv_class]) 1);
16.29 -qed "real_of_int";
16.30 -
16.31 -Goal "inj(real :: int => real)";
16.32 -by (rtac injI 1);
16.33 -by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
16.34 -by (res_inst_tac [("z","y")] eq_Abs_Integ 1);
16.35 -by (auto_tac (claset() addSDs [inj_preal_of_prat RS injD,
16.36 - inj_prat_of_pnat RS injD, inj_pnat_of_nat RS injD],
16.37 - simpset() addsimps [real_of_int,preal_of_prat_add RS sym,
16.38 - prat_of_pnat_add RS sym,pnat_of_nat_add]));
16.39 -qed "inj_real_of_int";
16.40 -
16.41 -Goalw [int_def,real_zero_def] "real (int 0) = 0";
16.42 -by (simp_tac (simpset() addsimps [real_of_int, preal_add_commute]) 1);
16.43 -qed "real_of_int_zero";
16.44 -
16.45 -Goal "real (1::int) = (1::real)";
16.46 -by (stac (int_1 RS sym) 1);
16.47 -by (auto_tac (claset(),
16.48 - simpset() addsimps [int_def, real_one_def, real_of_int,
16.49 - preal_of_prat_add RS sym,pnat_two_eq,
16.50 - prat_of_pnat_add RS sym, pnat_one_iff RS sym]));
16.51 -qed "real_of_one";
16.52 -
16.53 -Goal "real (x::int) + real y = real (x + y)";
16.54 -by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
16.55 -by (res_inst_tac [("z","y")] eq_Abs_Integ 1);
16.56 -by (auto_tac (claset(),
16.57 - simpset() addsimps [real_of_int, preal_of_prat_add RS sym,
16.58 - prat_of_pnat_add RS sym, zadd,real_add,
16.59 - pnat_of_nat_add] @ pnat_add_ac));
16.60 -qed "real_of_int_add";
16.61 -Addsimps [real_of_int_add RS sym];
16.62 -
16.63 -Goal "-real (x::int) = real (-x)";
16.64 -by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
16.65 -by (auto_tac (claset(), simpset() addsimps [real_of_int, real_minus,zminus]));
16.66 -qed "real_of_int_minus";
16.67 -Addsimps [real_of_int_minus RS sym];
16.68 -
16.69 -Goalw [zdiff_def,real_diff_def]
16.70 - "real (x::int) - real y = real (x - y)";
16.71 -by (simp_tac (HOL_ss addsimps [real_of_int_add, real_of_int_minus]) 1);
16.72 -qed "real_of_int_diff";
16.73 -Addsimps [real_of_int_diff RS sym];
16.74 -
16.75 -Goal "real (x::int) * real y = real (x * y)";
16.76 -by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
16.77 -by (res_inst_tac [("z","y")] eq_Abs_Integ 1);
16.78 -by (auto_tac (claset(),
16.79 - simpset() addsimps [real_of_int, real_mult,zmult,
16.80 - preal_of_prat_mult RS sym,pnat_of_nat_mult,
16.81 - prat_of_pnat_mult RS sym,preal_of_prat_add RS sym,
16.82 - prat_of_pnat_add RS sym,pnat_of_nat_add] @
16.83 - mult_ac @ add_ac @ pnat_add_ac));
16.84 -qed "real_of_int_mult";
16.85 -Addsimps [real_of_int_mult RS sym];
16.86 -
16.87 -Goal "real (int (Suc n)) = real (int n) + (1::real)";
16.88 -by (simp_tac (simpset() addsimps [real_of_one RS sym, zadd_int] @
16.89 - zadd_ac) 1);
16.90 -qed "real_of_int_Suc";
16.91 -
16.92 -(* relating two of the embeddings *)
16.93 -Goal "real (int n) = real n";
16.94 -by (induct_tac "n" 1);
16.95 -by (ALLGOALS (simp_tac (HOL_ss addsimps [real_of_int_zero, real_of_nat_zero,
16.96 - real_of_int_Suc,real_of_nat_Suc])));
16.97 -by (Simp_tac 1);
16.98 -qed "real_of_int_real_of_nat";
16.99 -
16.100 -Goal "~neg z ==> real (nat z) = real z";
16.101 -by (asm_full_simp_tac (simpset() addsimps [not_neg_eq_ge_0, real_of_int_real_of_nat RS sym]) 1);
16.102 -qed "real_of_nat_real_of_int";
16.103 -
16.104 -Goal "(real x = 0) = (x = int 0)";
16.105 -by (auto_tac (claset() addIs [inj_real_of_int RS injD],
16.106 - HOL_ss addsimps [real_of_int_zero]));
16.107 -qed "real_of_int_zero_cancel";
16.108 -Addsimps [real_of_int_zero_cancel];
16.109 -
16.110 -Goal "real (x::int) < real y ==> x < y";
16.111 -by (rtac ccontr 1 THEN dtac (linorder_not_less RS iffD1) 1);
16.112 -by (auto_tac (claset(),
16.113 - simpset() addsimps [zle_iff_zadd, real_of_int_add RS sym,
16.114 - real_of_int_real_of_nat,
16.115 - linorder_not_le RS sym]));
16.116 -qed "real_of_int_less_cancel";
16.117 -
16.118 -Goal "(real (x::int) = real y) = (x = y)";
16.119 -by (blast_tac (claset() addSDs [inj_real_of_int RS injD]) 1);
16.120 -qed "real_of_int_inject";
16.121 -AddIffs [real_of_int_inject];
16.122 -
16.123 -Goal "x < y ==> (real (x::int) < real y)";
16.124 -by (full_simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
16.125 -by (auto_tac (claset() addSDs [real_of_int_less_cancel],
16.126 - simpset() addsimps [order_le_less]));
16.127 -qed "real_of_int_less_mono";
16.128 -
16.129 -Goal "(real (x::int) < real y) = (x < y)";
16.130 -by (blast_tac (claset() addDs [real_of_int_less_cancel]
16.131 - addIs [real_of_int_less_mono]) 1);
16.132 -qed "real_of_int_less_iff";
16.133 -AddIffs [real_of_int_less_iff];
16.134 -
16.135 -Goal "(real (x::int) <= real y) = (x <= y)";
16.136 -by (full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
16.137 -qed "real_of_int_le_iff";
16.138 -Addsimps [real_of_int_le_iff];
16.139 -
16.140 -Addsimps [real_of_one];
16.141 -
17.1 --- a/src/HOL/Real/RealInt.thy Thu Nov 27 10:47:55 2003 +0100
17.2 +++ b/src/HOL/Real/RealInt.thy Fri Nov 28 12:09:37 2003 +0100
17.3 @@ -2,16 +2,146 @@
17.4 ID: $Id$
17.5 Author: Jacques D. Fleuriot
17.6 Copyright: 1999 University of Edinburgh
17.7 - Description: Embedding the integers in the reals
17.8 *)
17.9
17.10 -RealInt = RealOrd +
17.11 +header{*Embedding the Integers into the Reals*}
17.12
17.13 -defs
17.14 - (*overloaded*)
17.15 - real_of_int_def
17.16 +theory RealInt = RealOrd:
17.17 +
17.18 +defs (overloaded)
17.19 + real_of_int_def:
17.20 "real z == Abs_REAL(UN (i,j): Rep_Integ z. realrel ``
17.21 {(preal_of_prat(prat_of_pnat(pnat_of_nat i)),
17.22 preal_of_prat(prat_of_pnat(pnat_of_nat j)))})"
17.23
17.24 +
17.25 +lemma real_of_int_congruent:
17.26 + "congruent intrel (%p. (%(i,j). realrel ``
17.27 + {(preal_of_prat (prat_of_pnat (pnat_of_nat i)),
17.28 + preal_of_prat (prat_of_pnat (pnat_of_nat j)))}) p)"
17.29 +apply (unfold congruent_def)
17.30 +apply (auto simp add: pnat_of_nat_add prat_of_pnat_add [symmetric] preal_of_prat_add [symmetric])
17.31 +done
17.32 +
17.33 +lemma real_of_int:
17.34 + "real (Abs_Integ (intrel `` {(i, j)})) =
17.35 + Abs_REAL(realrel ``
17.36 + {(preal_of_prat (prat_of_pnat (pnat_of_nat i)),
17.37 + preal_of_prat (prat_of_pnat (pnat_of_nat j)))})"
17.38 +apply (unfold real_of_int_def)
17.39 +apply (rule_tac f = Abs_REAL in arg_cong)
17.40 +apply (simp add: realrel_in_real [THEN Abs_REAL_inverse]
17.41 + UN_equiv_class [OF equiv_intrel real_of_int_congruent])
17.42 +done
17.43 +
17.44 +lemma inj_real_of_int: "inj(real :: int => real)"
17.45 +apply (rule inj_onI)
17.46 +apply (rule_tac z = x in eq_Abs_Integ)
17.47 +apply (rule_tac z = y in eq_Abs_Integ)
17.48 +apply (auto dest!: inj_preal_of_prat [THEN injD] inj_prat_of_pnat [THEN injD]
17.49 + inj_pnat_of_nat [THEN injD]
17.50 + simp add: real_of_int preal_of_prat_add [symmetric] prat_of_pnat_add [symmetric] pnat_of_nat_add)
17.51 +done
17.52 +
17.53 +lemma real_of_int_zero: "real (int 0) = 0"
17.54 +apply (unfold int_def real_zero_def)
17.55 +apply (simp add: real_of_int preal_add_commute)
17.56 +done
17.57 +
17.58 +lemma real_of_one: "real (1::int) = (1::real)"
17.59 +apply (subst int_1 [symmetric])
17.60 +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])
17.61 +done
17.62 +
17.63 +lemma real_of_int_add: "real (x::int) + real y = real (x + y)"
17.64 +apply (rule_tac z = x in eq_Abs_Integ)
17.65 +apply (rule_tac z = y in eq_Abs_Integ)
17.66 +apply (auto simp add: real_of_int preal_of_prat_add [symmetric]
17.67 + prat_of_pnat_add [symmetric] zadd real_add pnat_of_nat_add pnat_add_ac)
17.68 +done
17.69 +declare real_of_int_add [symmetric, simp]
17.70 +
17.71 +lemma real_of_int_minus: "-real (x::int) = real (-x)"
17.72 +apply (rule_tac z = x in eq_Abs_Integ)
17.73 +apply (auto simp add: real_of_int real_minus zminus)
17.74 +done
17.75 +declare real_of_int_minus [symmetric, simp]
17.76 +
17.77 +lemma real_of_int_diff:
17.78 + "real (x::int) - real y = real (x - y)"
17.79 +apply (unfold zdiff_def real_diff_def)
17.80 +apply (simp only: real_of_int_add real_of_int_minus)
17.81 +done
17.82 +declare real_of_int_diff [symmetric, simp]
17.83 +
17.84 +lemma real_of_int_mult: "real (x::int) * real y = real (x * y)"
17.85 +apply (rule_tac z = x in eq_Abs_Integ)
17.86 +apply (rule_tac z = y in eq_Abs_Integ)
17.87 +apply (auto simp add: real_of_int real_mult zmult
17.88 + preal_of_prat_mult [symmetric] pnat_of_nat_mult
17.89 + prat_of_pnat_mult [symmetric] preal_of_prat_add [symmetric]
17.90 + prat_of_pnat_add [symmetric] pnat_of_nat_add mult_ac add_ac pnat_add_ac)
17.91 +done
17.92 +declare real_of_int_mult [symmetric, simp]
17.93 +
17.94 +lemma real_of_int_Suc: "real (int (Suc n)) = real (int n) + (1::real)"
17.95 +by (simp add: real_of_one [symmetric] zadd_int zadd_ac)
17.96 +
17.97 +declare real_of_one [simp]
17.98 +
17.99 +(* relating two of the embeddings *)
17.100 +lemma real_of_int_real_of_nat: "real (int n) = real n"
17.101 +apply (induct_tac "n")
17.102 +apply (simp_all only: real_of_int_zero real_of_nat_zero real_of_int_Suc real_of_nat_Suc)
17.103 +done
17.104 +
17.105 +lemma real_of_nat_real_of_int: "~neg z ==> real (nat z) = real z"
17.106 +by (simp add: not_neg_eq_ge_0 real_of_int_real_of_nat [symmetric])
17.107 +
17.108 +lemma real_of_int_zero_cancel [simp]: "(real x = 0) = (x = int 0)"
17.109 +by (auto intro: inj_real_of_int [THEN injD]
17.110 + simp only: real_of_int_zero)
17.111 +
17.112 +lemma real_of_int_less_cancel: "real (x::int) < real y ==> x < y"
17.113 +apply (rule ccontr, drule linorder_not_less [THEN iffD1])
17.114 +apply (auto simp add: zle_iff_zadd real_of_int_add [symmetric] real_of_int_real_of_nat linorder_not_le [symmetric])
17.115 +done
17.116 +
17.117 +lemma real_of_int_inject [iff]: "(real (x::int) = real y) = (x = y)"
17.118 +by (blast dest!: inj_real_of_int [THEN injD])
17.119 +
17.120 +lemma real_of_int_less_mono: "x < y ==> (real (x::int) < real y)"
17.121 +apply (simp add: linorder_not_le [symmetric])
17.122 +apply (auto dest!: real_of_int_less_cancel simp add: order_le_less)
17.123 +done
17.124 +
17.125 +lemma real_of_int_less_iff [iff]: "(real (x::int) < real y) = (x < y)"
17.126 +by (blast dest: real_of_int_less_cancel intro: real_of_int_less_mono)
17.127 +
17.128 +lemma real_of_int_le_iff [simp]: "(real (x::int) \<le> real y) = (x \<le> y)"
17.129 +by (simp add: linorder_not_less [symmetric])
17.130 +
17.131 +ML
17.132 +{*
17.133 +val real_of_int_congruent = thm"real_of_int_congruent";
17.134 +val real_of_int = thm"real_of_int";
17.135 +val inj_real_of_int = thm"inj_real_of_int";
17.136 +val real_of_int_zero = thm"real_of_int_zero";
17.137 +val real_of_one = thm"real_of_one";
17.138 +val real_of_int_add = thm"real_of_int_add";
17.139 +val real_of_int_minus = thm"real_of_int_minus";
17.140 +val real_of_int_diff = thm"real_of_int_diff";
17.141 +val real_of_int_mult = thm"real_of_int_mult";
17.142 +val real_of_int_Suc = thm"real_of_int_Suc";
17.143 +val real_of_int_real_of_nat = thm"real_of_int_real_of_nat";
17.144 +val real_of_nat_real_of_int = thm"real_of_nat_real_of_int";
17.145 +val real_of_int_zero_cancel = thm"real_of_int_zero_cancel";
17.146 +val real_of_int_less_cancel = thm"real_of_int_less_cancel";
17.147 +val real_of_int_inject = thm"real_of_int_inject";
17.148 +val real_of_int_less_mono = thm"real_of_int_less_mono";
17.149 +val real_of_int_less_iff = thm"real_of_int_less_iff";
17.150 +val real_of_int_le_iff = thm"real_of_int_le_iff";
17.151 +*}
17.152 +
17.153 +
17.154 end
18.1 --- a/src/HOL/Real/RealOrd.thy Thu Nov 27 10:47:55 2003 +0100
18.2 +++ b/src/HOL/Real/RealOrd.thy Fri Nov 28 12:09:37 2003 +0100
18.3 @@ -8,20 +8,6 @@
18.4
18.5 theory RealOrd = RealDef:
18.6
18.7 -instance real :: order
18.8 - by (intro_classes,
18.9 - (assumption |
18.10 - rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+)
18.11 -
18.12 -instance real :: linorder
18.13 - by (intro_classes, rule real_le_linear)
18.14 -
18.15 -instance real :: plus_ac0
18.16 - by (intro_classes,
18.17 - (assumption |
18.18 - rule real_add_commute real_add_assoc real_add_zero_left)+)
18.19 -
18.20 -
18.21 defs (overloaded)
18.22 real_abs_def: "abs (r::real) == (if 0 \<le> r then r else -r)"
18.23
18.24 @@ -222,6 +208,110 @@
18.25 by (rule Ring_and_Field.zero_le_square)
18.26
18.27
18.28 +subsection{*Division Lemmas*}
18.29 +
18.30 +(** Inverse of zero! Useful to simplify certain equations **)
18.31 +
18.32 +lemma INVERSE_ZERO [simp]: "inverse 0 = (0::real)"
18.33 +apply (unfold real_inverse_def)
18.34 +apply (rule someI2)
18.35 +apply (auto simp add: real_zero_not_eq_one)
18.36 +done
18.37 +
18.38 +lemma DIVISION_BY_ZERO [simp]: "a / (0::real) = 0"
18.39 +by (simp add: real_divide_def INVERSE_ZERO)
18.40 +
18.41 +lemma real_mult_left_cancel: "(c::real) ~= 0 ==> (c*a=c*b) = (a=b)"
18.42 +apply auto
18.43 +done
18.44 +
18.45 +lemma real_mult_right_cancel: "(c::real) ~= 0 ==> (a*c=b*c) = (a=b)"
18.46 +apply (auto );
18.47 +done
18.48 +
18.49 +lemma real_mult_left_cancel_ccontr: "c*a ~= c*b ==> a ~= b"
18.50 +by auto
18.51 +
18.52 +lemma real_mult_right_cancel_ccontr: "a*c ~= b*c ==> a ~= b"
18.53 +by auto
18.54 +
18.55 +lemma real_inverse_not_zero: "x ~= 0 ==> inverse(x::real) ~= 0"
18.56 + by (rule Ring_and_Field.nonzero_imp_inverse_nonzero)
18.57 +
18.58 +lemma real_mult_not_zero: "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::real)"
18.59 +apply (simp add: );
18.60 +done
18.61 +
18.62 +lemma real_inverse_inverse: "inverse(inverse (x::real)) = x"
18.63 +apply (case_tac "x=0", simp)
18.64 +apply (rule_tac c1 = "inverse x" in real_mult_right_cancel [THEN iffD1])
18.65 +apply (erule real_inverse_not_zero)
18.66 +apply (auto dest: real_inverse_not_zero)
18.67 +done
18.68 +declare real_inverse_inverse [simp]
18.69 +
18.70 +lemma real_inverse_1: "inverse((1::real)) = (1::real)"
18.71 +apply (unfold real_inverse_def)
18.72 +apply (cut_tac real_zero_not_eq_one [THEN not_sym, THEN real_mult_inv_left_ex])
18.73 +apply (auto simp add: real_zero_not_eq_one [THEN not_sym])
18.74 +done
18.75 +declare real_inverse_1 [simp]
18.76 +
18.77 +lemma real_minus_inverse: "inverse(-x) = -inverse(x::real)"
18.78 +apply (case_tac "x=0", simp)
18.79 +apply (rule_tac c1 = "-x" in real_mult_right_cancel [THEN iffD1])
18.80 + prefer 2 apply (subst real_mult_inv_left, auto)
18.81 +done
18.82 +
18.83 +lemma real_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::real)"
18.84 +apply (case_tac "x=0", simp)
18.85 +apply (case_tac "y=0", simp)
18.86 +apply (frule_tac y = y in real_mult_not_zero, assumption)
18.87 +apply (rule_tac c1 = x in real_mult_left_cancel [THEN iffD1])
18.88 +apply (auto simp add: real_mult_assoc [symmetric])
18.89 +apply (rule_tac c1 = y in real_mult_left_cancel [THEN iffD1])
18.90 +apply (auto simp add: real_mult_left_commute)
18.91 +apply (simp add: real_mult_assoc [symmetric])
18.92 +done
18.93 +
18.94 +lemma real_times_divide1_eq: "(x::real) * (y/z) = (x*y)/z"
18.95 +by (simp add: real_divide_def real_mult_assoc)
18.96 +
18.97 +lemma real_times_divide2_eq: "(y/z) * (x::real) = (y*x)/z"
18.98 +by (simp add: real_divide_def real_mult_ac)
18.99 +
18.100 +declare real_times_divide1_eq [simp] real_times_divide2_eq [simp]
18.101 +
18.102 +lemma real_divide_divide1_eq: "(x::real) / (y/z) = (x*z)/y"
18.103 +by (simp add: real_divide_def real_inverse_distrib real_mult_ac)
18.104 +
18.105 +lemma real_divide_divide2_eq: "((x::real) / y) / z = x/(y*z)"
18.106 +by (simp add: real_divide_def real_inverse_distrib real_mult_assoc)
18.107 +
18.108 +declare real_divide_divide1_eq [simp] real_divide_divide2_eq [simp]
18.109 +
18.110 +(** As with multiplication, pull minus signs OUT of the / operator **)
18.111 +
18.112 +lemma real_minus_divide_eq: "(-x) / (y::real) = - (x/y)"
18.113 +by (simp add: real_divide_def)
18.114 +declare real_minus_divide_eq [simp]
18.115 +
18.116 +lemma real_divide_minus_eq: "(x / -(y::real)) = - (x/y)"
18.117 +by (simp add: real_divide_def real_minus_inverse)
18.118 +declare real_divide_minus_eq [simp]
18.119 +
18.120 +lemma real_add_divide_distrib: "(x+y)/(z::real) = x/z + y/z"
18.121 +by (simp add: real_divide_def real_add_mult_distrib)
18.122 +
18.123 +(*The following would e.g. convert (x+y)/2 to x/2 + y/2. Sometimes that
18.124 + leads to cancellations in x or y, but is also prevents "multiplying out"
18.125 + the 2 in e.g. (x+y)/2 = 5.
18.126 +
18.127 +Addsimps [inst "z" "number_of ?w" real_add_divide_distrib]
18.128 +**)
18.129 +
18.130 +
18.131 +
18.132 subsection{*An Embedding of the Naturals in the Reals*}
18.133
18.134 lemma real_of_posnat_one: "real_of_posnat 0 = (1::real)"
18.135 @@ -710,6 +800,26 @@
18.136 val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero";
18.137 val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff";
18.138 val real_of_nat_num_if = thm "real_of_nat_num_if";
18.139 +
18.140 +val INVERSE_ZERO = thm"INVERSE_ZERO";
18.141 +val DIVISION_BY_ZERO = thm"DIVISION_BY_ZERO";
18.142 +val real_mult_left_cancel = thm"real_mult_left_cancel";
18.143 +val real_mult_right_cancel = thm"real_mult_right_cancel";
18.144 +val real_mult_left_cancel_ccontr = thm"real_mult_left_cancel_ccontr";
18.145 +val real_mult_right_cancel_ccontr = thm"real_mult_right_cancel_ccontr";
18.146 +val real_inverse_not_zero = thm"real_inverse_not_zero";
18.147 +val real_mult_not_zero = thm"real_mult_not_zero";
18.148 +val real_inverse_inverse = thm"real_inverse_inverse";
18.149 +val real_inverse_1 = thm"real_inverse_1";
18.150 +val real_minus_inverse = thm"real_minus_inverse";
18.151 +val real_inverse_distrib = thm"real_inverse_distrib";
18.152 +val real_times_divide1_eq = thm"real_times_divide1_eq";
18.153 +val real_times_divide2_eq = thm"real_times_divide2_eq";
18.154 +val real_divide_divide1_eq = thm"real_divide_divide1_eq";
18.155 +val real_divide_divide2_eq = thm"real_divide_divide2_eq";
18.156 +val real_minus_divide_eq = thm"real_minus_divide_eq";
18.157 +val real_divide_minus_eq = thm"real_divide_minus_eq";
18.158 +val real_add_divide_distrib = thm"real_add_divide_distrib";
18.159 *}
18.160
18.161 end
19.1 --- a/src/HOL/Real/RealPow.thy Thu Nov 27 10:47:55 2003 +0100
19.2 +++ b/src/HOL/Real/RealPow.thy Fri Nov 28 12:09:37 2003 +0100
19.3 @@ -6,10 +6,7 @@
19.4
19.5 *)
19.6
19.7 -theory RealPow = RealAbs:
19.8 -
19.9 -(*belongs to theory RealAbs*)
19.10 -lemmas [arith_split] = abs_split
19.11 +theory RealPow = RealArith:
19.12
19.13 instance real :: power ..
19.14
20.1 --- a/src/HOL/Ring_and_Field.thy Thu Nov 27 10:47:55 2003 +0100
20.2 +++ b/src/HOL/Ring_and_Field.thy Fri Nov 28 12:09:37 2003 +0100
20.3 @@ -1,6 +1,7 @@
20.4 (* Title: HOL/Ring_and_Field.thy
20.5 ID: $Id$
20.6 Author: Gertrud Bauer and Markus Wenzel, TU Muenchen
20.7 + Lawrence C Paulson, University of Cambridge
20.8 License: GPL (GNU GENERAL PUBLIC LICENSE)
20.9 *)
20.10
20.11 @@ -145,11 +146,11 @@
20.12
20.13 theorems mult_ac = mult_assoc mult_commute mult_left_commute
20.14
20.15 -lemma right_inverse [simp]: "a \<noteq> 0 ==> a * inverse (a::'a::field) = 1"
20.16 +lemma right_inverse [simp]:
20.17 + assumes not0: "a ~= 0" shows "a * inverse (a::'a::field) = 1"
20.18 proof -
20.19 have "a * inverse a = inverse a * a" by (simp add: mult_ac)
20.20 - also assume "a \<noteq> 0"
20.21 - hence "inverse a * a = 1" by simp
20.22 + also have "... = 1" using not0 by simp
20.23 finally show ?thesis .
20.24 qed
20.25
20.26 @@ -241,7 +242,7 @@
20.27 done
20.28
20.29 lemma le_imp_neg_le:
20.30 - assumes "a \<le> (b::'a::ordered_ring)" shows "-b \<le> -a"
20.31 + assumes "a \<le> (b::'a::ordered_ring)" shows "-b \<le> -a"
20.32 proof -
20.33 have "-a+a \<le> -a+b"
20.34 by (rule add_left_mono)
20.35 @@ -485,9 +486,9 @@
20.36
20.37 text{*Cancellation of equalities with a common factor*}
20.38 lemma field_mult_cancel_right_lemma:
20.39 - assumes cnz: "c \<noteq> (0::'a::field)"
20.40 - and eq: "a*c = b*c"
20.41 - shows "a=b"
20.42 + assumes cnz: "c \<noteq> (0::'a::field)"
20.43 + and eq: "a*c = b*c"
20.44 + shows "a=b"
20.45 proof -
20.46 have "(a * c) * inverse c = (b * c) * inverse c"
20.47 by (simp add: eq)
20.48 @@ -497,7 +498,7 @@
20.49
20.50 lemma field_mult_cancel_right:
20.51 "(a*c = b*c) = (c = (0::'a::field) | a=b)"
20.52 - proof (cases "c=0")
20.53 + proof cases
20.54 assume "c=0" thus ?thesis by simp
20.55 next
20.56 assume "c\<noteq>0"
20.57 @@ -534,18 +535,17 @@
20.58 by (force dest: inverse_nonzero_imp_nonzero)
20.59
20.60 lemma nonzero_inverse_minus_eq:
20.61 - "a\<noteq>0 ==> inverse(-a) = -inverse(a::'a::field)";
20.62 + assumes [simp]: "a\<noteq>0" shows "inverse(-a) = -inverse(a::'a::field)"
20.63 proof -
20.64 - assume "a\<noteq>0"
20.65 - hence "-a * inverse (- a) = -a * - inverse a"
20.66 + have "-a * inverse (- a) = -a * - inverse a"
20.67 by simp
20.68 thus ?thesis
20.69 - by (simp only: field_mult_cancel_left, simp add: prems)
20.70 + by (simp only: field_mult_cancel_left, simp)
20.71 qed
20.72
20.73 lemma inverse_minus_eq [simp]:
20.74 "inverse(-a) = -inverse(a::'a::{field,division_by_zero})";
20.75 - proof (cases "a=0")
20.76 + proof cases
20.77 assume "a=0" thus ?thesis by (simp add: inverse_zero)
20.78 next
20.79 assume "a\<noteq>0"
20.80 @@ -553,10 +553,10 @@
20.81 qed
20.82
20.83 lemma nonzero_inverse_eq_imp_eq:
20.84 - assumes inveq: "inverse a = inverse b"
20.85 - and anz: "a \<noteq> 0"
20.86 - and bnz: "b \<noteq> 0"
20.87 - shows "a = (b::'a::field)"
20.88 + assumes inveq: "inverse a = inverse b"
20.89 + and anz: "a \<noteq> 0"
20.90 + and bnz: "b \<noteq> 0"
20.91 + shows "a = (b::'a::field)"
20.92 proof -
20.93 have "a * inverse b = a * inverse a"
20.94 by (simp add: inveq)
20.95 @@ -582,8 +582,7 @@
20.96 subsection {* Ordered Fields *}
20.97
20.98 lemma inverse_gt_0:
20.99 - assumes a_gt_0: "0 < a"
20.100 - shows "0 < inverse (a::'a::ordered_field)"
20.101 + assumes a_gt_0: "0 < a" shows "0 < inverse (a::'a::ordered_field)"
20.102 proof -
20.103 have "0 < a * inverse a"
20.104 by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
20.105 @@ -597,9 +596,9 @@
20.106 simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
20.107
20.108 lemma inverse_le_imp_le:
20.109 - assumes invle: "inverse a \<le> inverse b"
20.110 - and apos: "0 < a"
20.111 - shows "b \<le> (a::'a::ordered_field)"
20.112 + assumes invle: "inverse a \<le> inverse b"
20.113 + and apos: "0 < a"
20.114 + shows "b \<le> (a::'a::ordered_field)"
20.115 proof (rule classical)
20.116 assume "~ b \<le> a"
20.117 hence "a < b"
20.118 @@ -615,9 +614,9 @@
20.119 qed
20.120
20.121 lemma less_imp_inverse_less:
20.122 - assumes less: "a < b"
20.123 - and apos: "0 < a"
20.124 - shows "inverse b < inverse (a::'a::ordered_field)"
20.125 + assumes less: "a < b"
20.126 + and apos: "0 < a"
20.127 + shows "inverse b < inverse (a::'a::ordered_field)"
20.128 proof (rule ccontr)
20.129 assume "~ inverse b < inverse a"
20.130 hence "inverse a \<le> inverse b"