re-organisation of Real/RealArith0.ML; more `Isar scripts
authorpaulson
Sun Dec 07 16:30:06 2003 +0100 (2003-12-07)
changeset 14284f1abe67c448a
parent 14283 516358ca7b42
child 14285 92ed032e83a1
re-organisation of Real/RealArith0.ML; more `Isar scripts
src/HOL/Hyperreal/Transcendental.ML
src/HOL/Integ/Bin.thy
src/HOL/Real/RealArith0.ML
src/HOL/Real/RealArith0.thy
src/HOL/Real/RealOrd.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Hyperreal/Transcendental.ML	Sat Dec 06 07:52:17 2003 +0100
     1.2 +++ b/src/HOL/Hyperreal/Transcendental.ML	Sun Dec 07 16:30:06 2003 +0100
     1.3 @@ -1732,7 +1732,9 @@
     1.4  
     1.5  Goal "0 < pi";
     1.6  by (multr_by_tac "inverse 2" 1);
     1.7 -by Auto_tac;
     1.8 +by (Simp_tac 1);
     1.9 +by (cut_facts_tac [pi_half_gt_zero] 1);
    1.10 +by (full_simp_tac (HOL_ss addsimps [thm"mult_left_zero", real_divide_def]) 1);
    1.11  qed "pi_gt_zero";
    1.12  Addsimps [pi_gt_zero];
    1.13  Addsimps [(pi_gt_zero RS real_not_refl2) RS not_sym];
    1.14 @@ -1842,8 +1844,9 @@
    1.15  
    1.16  Goal "[| 0 < x; x < pi/2 |] ==> 0 < sin x";
    1.17  by (rtac sin_gt_zero 1);
    1.18 -by (rtac real_less_trans 2 THEN assume_tac 2);
    1.19 -by Auto_tac;
    1.20 +by (assume_tac 1); 
    1.21 +by (rtac real_less_trans 1 THEN assume_tac 1);
    1.22 +by (rtac pi_half_less_two 1); 
    1.23  qed "sin_gt_zero2";
    1.24  
    1.25  Goal "[| - pi/2 < x; x < 0 |] ==> sin x < 0";
    1.26 @@ -1854,13 +1857,22 @@
    1.27  by Auto_tac;
    1.28  qed "sin_less_zero";
    1.29  
    1.30 +Goal "pi < 4";
    1.31 +by (cut_facts_tac [pi_half_less_two] 1);
    1.32 +by Auto_tac; 
    1.33 +qed "pi_less_4";
    1.34 +
    1.35  Goal "[| 0 < x; x < pi/2 |] ==> 0 < cos x";
    1.36 +by (cut_facts_tac [pi_less_4] 1);
    1.37  by (cut_inst_tac [("f","cos"),("a","0"),("b","x"),("y","0")] IVT2_objl 1);
    1.38  by (Step_tac 1);
    1.39  by (cut_facts_tac [cos_is_zero] 5);
    1.40  by (Step_tac 5);
    1.41  by (dres_inst_tac [("x","xa")] spec 5);
    1.42  by (dres_inst_tac [("x","pi/2")] spec 5);
    1.43 +by (force_tac (claset(), simpset() addsimps []) 1); 
    1.44 +by (force_tac (claset(), simpset() addsimps []) 1); 
    1.45 +by (force_tac (claset(), simpset() addsimps []) 1); 
    1.46  by (auto_tac (claset() addSDs [ pi_half_less_two RS order_less_trans, 
    1.47      CLAIM "~ m <= n ==> n < (m::real)"]
    1.48      addIs [DERIV_isCont,DERIV_cos],simpset()));
    1.49 @@ -2323,7 +2335,7 @@
    1.50  qed "tan_arctan";
    1.51  
    1.52  Goal "- (pi/2) < arctan y  & arctan y < pi/2";
    1.53 -by (Auto_tac);
    1.54 +by (asm_full_simp_tac (HOL_ss addsimps [arctan]) 1); 
    1.55  qed "arctan_bounded";
    1.56  
    1.57  Goal "- (pi/2) < arctan y";
    1.58 @@ -2331,7 +2343,7 @@
    1.59  qed "arctan_lbound";
    1.60  
    1.61  Goal "arctan y < pi/2";
    1.62 -by (Auto_tac);
    1.63 +by (asm_full_simp_tac (HOL_ss addsimps [arctan]) 1); 
    1.64  qed "arctan_ubound";
    1.65  
    1.66  Goalw [arctan_def]
    1.67 @@ -2842,10 +2854,13 @@
    1.68  Goal "[| 0 < x * x + y * y; \
    1.69  \       1 - cos xa ^ 2 = (y / sqrt (x * x + y * y)) ^ 2 \
    1.70  \     |] ==> cos xa ^ 2 = (x / sqrt (x * x + y * y)) ^ 2";
    1.71 -by (auto_tac (claset(),simpset() addsimps [realpow_divide,
    1.72 -    real_sqrt_gt_zero_pow2,realpow_two_eq_mult RS sym]));
    1.73 +by (auto_tac (claset(),
    1.74 +    simpset() addsimps [realpow_divide,
    1.75 +          real_sqrt_gt_zero_pow2,realpow_two_eq_mult RS sym]));
    1.76  by (rtac (real_add_commute RS subst) 1);
    1.77 -by (auto_tac (claset() addIs [lemma_divide_rearrange],simpset()));
    1.78 +by (rtac lemma_divide_rearrange 1); 
    1.79 +by (asm_full_simp_tac (simpset() addsimps []) 1);
    1.80 +by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);  
    1.81  qed "lemma_sin_cos_eq";
    1.82  
    1.83  Goal "[| x ~= 0; \
    1.84 @@ -2863,18 +2878,6 @@
    1.85      delsimps [realpow_Suc]));
    1.86  qed "sin_x_y_disj";
    1.87  
    1.88 -(*
    1.89 -Goal "(x / sqrt (x * x + y * y)) ^ 2 = (x * x) / (x * x + y * y)";
    1.90 -by Auto_tac;
    1.91 -val lemma = result();
    1.92 -Addsimps [lemma];
    1.93 -
    1.94 -Goal "(x / sqrt (x * x + y * y)) *  (x / sqrt (x * x + y * y)) = \
    1.95 -\        (x * x) / (x * x + y * y)";
    1.96 -val lemma_too = result();
    1.97 -Addsimps [lemma_too];
    1.98 -*)
    1.99 -
   1.100  Goal "y ~= 0 ==> x / sqrt (x * x + y * y) ~= -(1::real)";
   1.101  by Auto_tac;
   1.102  by (dres_inst_tac [("f","%x. x ^ 2")] arg_cong 1);
     2.1 --- a/src/HOL/Integ/Bin.thy	Sat Dec 06 07:52:17 2003 +0100
     2.2 +++ b/src/HOL/Integ/Bin.thy	Sun Dec 07 16:30:06 2003 +0100
     2.3 @@ -242,6 +242,9 @@
     2.4  declare zero_le_divide_iff [of "number_of w", standard, simp]
     2.5  declare divide_le_0_iff [of "number_of w", standard, simp]
     2.6  
     2.7 +(*Replaces "inverse #nn" by 1/#nn *)
     2.8 +declare inverse_eq_divide [of "number_of w", standard, simp]
     2.9 +
    2.10  text{*These laws simplify inequalities, moving unary minus from a term
    2.11  into the literal.*}
    2.12  declare less_minus_iff [of "number_of v", standard, simp]
     3.1 --- a/src/HOL/Real/RealArith0.ML	Sat Dec 06 07:52:17 2003 +0100
     3.2 +++ b/src/HOL/Real/RealArith0.ML	Sun Dec 07 16:30:06 2003 +0100
     3.3 @@ -207,290 +207,33 @@
     3.4  test "a*(b*c)/(y*z) = d*(b::real)*(x*a)/z";
     3.5  *)
     3.6  
     3.7 -
     3.8 -(*** Simplification of inequalities involving literal divisors ***)
     3.9 -
    3.10 -Goal "0<z ==> ((x::real) <= y/z) = (x*z <= y)";
    3.11 -by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
    3.12 -by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
    3.13 -by (etac ssubst 1);
    3.14 -by (stac real_mult_le_cancel2 1);
    3.15 -by (Asm_simp_tac 1);
    3.16 -qed "pos_real_le_divide_eq";
    3.17 -Addsimps [inst "z" "number_of ?w" pos_real_le_divide_eq];
    3.18 -
    3.19 -Goal "z<0 ==> ((x::real) <= y/z) = (y <= x*z)";
    3.20 -by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
    3.21 -by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
    3.22 -by (etac ssubst 1);
    3.23 -by (stac real_mult_le_cancel2 1);
    3.24 -by (Asm_simp_tac 1);
    3.25 -qed "neg_real_le_divide_eq";
    3.26 -Addsimps [inst "z" "number_of ?w" neg_real_le_divide_eq];
    3.27 -
    3.28 -Goal "0<z ==> (y/z <= (x::real)) = (y <= x*z)";
    3.29 -by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
    3.30 -by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
    3.31 -by (etac ssubst 1);
    3.32 -by (stac real_mult_le_cancel2 1);
    3.33 -by (Asm_simp_tac 1);
    3.34 -qed "pos_real_divide_le_eq";
    3.35 -Addsimps [inst "z" "number_of ?w" pos_real_divide_le_eq];
    3.36 -
    3.37 -Goal "z<0 ==> (y/z <= (x::real)) = (x*z <= y)";
    3.38 -by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
    3.39 -by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
    3.40 -by (etac ssubst 1);
    3.41 -by (stac real_mult_le_cancel2 1);
    3.42 -by (Asm_simp_tac 1);
    3.43 -qed "neg_real_divide_le_eq";
    3.44 -Addsimps [inst "z" "number_of ?w" neg_real_divide_le_eq];
    3.45 -
    3.46 -Goal "0<z ==> ((x::real) < y/z) = (x*z < y)";
    3.47 -by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
    3.48 -by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
    3.49 -by (etac ssubst 1);
    3.50 -by (stac real_mult_less_cancel2 1);
    3.51 -by (Asm_simp_tac 1);
    3.52 -qed "pos_real_less_divide_eq";
    3.53 -Addsimps [inst "z" "number_of ?w" pos_real_less_divide_eq];
    3.54 -
    3.55 -Goal "z<0 ==> ((x::real) < y/z) = (y < x*z)";
    3.56 -by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
    3.57 -by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
    3.58 -by (etac ssubst 1);
    3.59 -by (stac real_mult_less_cancel2 1);
    3.60 -by (Asm_simp_tac 1);
    3.61 -qed "neg_real_less_divide_eq";
    3.62 -Addsimps [inst "z" "number_of ?w" neg_real_less_divide_eq];
    3.63 -
    3.64 -Goal "0<z ==> (y/z < (x::real)) = (y < x*z)";
    3.65 -by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
    3.66 -by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
    3.67 -by (etac ssubst 1);
    3.68 -by (stac real_mult_less_cancel2 1);
    3.69 -by (Asm_simp_tac 1);
    3.70 -qed "pos_real_divide_less_eq";
    3.71 -Addsimps [inst "z" "number_of ?w" pos_real_divide_less_eq];
    3.72 -
    3.73 -Goal "z<0 ==> (y/z < (x::real)) = (x*z < y)";
    3.74 -by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
    3.75 -by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
    3.76 -by (etac ssubst 1);
    3.77 -by (stac real_mult_less_cancel2 1);
    3.78 -by (Asm_simp_tac 1);
    3.79 -qed "neg_real_divide_less_eq";
    3.80 -Addsimps [inst "z" "number_of ?w" neg_real_divide_less_eq];
    3.81 -
    3.82 -Goal "z~=0 ==> ((x::real) = y/z) = (x*z = y)";
    3.83 -by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1);
    3.84 -by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
    3.85 -by (etac ssubst 1);
    3.86 -by (stac real_mult_eq_cancel2 1);
    3.87 -by (Asm_simp_tac 1);
    3.88 -qed "real_eq_divide_eq";
    3.89 -Addsimps [inst "z" "number_of ?w" real_eq_divide_eq];
    3.90 -
    3.91 -Goal "z~=0 ==> (y/z = (x::real)) = (y = x*z)";
    3.92 -by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1);
    3.93 -by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
    3.94 -by (etac ssubst 1);
    3.95 -by (stac real_mult_eq_cancel2 1);
    3.96 -by (Asm_simp_tac 1);
    3.97 -qed "real_divide_eq_eq";
    3.98 -Addsimps [inst "z" "number_of ?w" real_divide_eq_eq];
    3.99 -
   3.100 -Goal "(m/k = n/k) = (k = 0 | m = (n::real))";
   3.101 -by (case_tac "k=0" 1);
   3.102 -by (asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1);
   3.103 -by (asm_simp_tac (simpset() addsimps [real_divide_eq_eq, real_eq_divide_eq,
   3.104 -                                      real_mult_eq_cancel2]) 1);
   3.105 -qed "real_divide_eq_cancel2";
   3.106 -
   3.107 -Goal "(k/m = k/n) = (k = 0 | m = (n::real))";
   3.108 -by (case_tac "m=0 | n = 0" 1);
   3.109 -by (auto_tac (claset(),
   3.110 -              simpset() addsimps [DIVISION_BY_ZERO, real_divide_eq_eq,
   3.111 -                                  real_eq_divide_eq, real_mult_eq_cancel1]));
   3.112 -qed "real_divide_eq_cancel1";
   3.113 -
   3.114 -Goal "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)";
   3.115 -by (auto_tac (claset() addIs [real_inverse_less_swap], simpset()));
   3.116 -qed "real_inverse_less_iff";
   3.117 -
   3.118 -Goal "[| 0 < r; 0 < x|] ==> (inverse x <= inverse r) = (r <= (x::real))";
   3.119 -by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
   3.120 -                                      real_inverse_less_iff]) 1);
   3.121 -qed "real_inverse_le_iff";
   3.122 -
   3.123 -(** Division by 1, -1 **)
   3.124 -
   3.125 -Goal "(x::real)/1 = x";
   3.126 -by (simp_tac (simpset() addsimps [real_divide_def]) 1);
   3.127 -qed "real_divide_1";
   3.128 -Addsimps [real_divide_1];
   3.129 -
   3.130 -Goal "x/-1 = -(x::real)";
   3.131 -by (Simp_tac 1);
   3.132 -qed "real_divide_minus1";
   3.133 -Addsimps [real_divide_minus1];
   3.134 -
   3.135 -Goal "-1/(x::real) = - (1/x)";
   3.136 -by (simp_tac (simpset() addsimps [real_divide_def, real_minus_inverse]) 1);
   3.137 -qed "real_minus1_divide";
   3.138 -Addsimps [real_minus1_divide];
   3.139 -
   3.140 -Goal "[| (0::real) < d1; 0 < d2 |] ==> EX e. 0 < e & e < d1 & e < d2";
   3.141 -by (res_inst_tac [("x","(min d1 d2)/2")] exI 1);
   3.142 -by (asm_simp_tac (simpset() addsimps [min_def]) 1);
   3.143 -qed "real_lbound_gt_zero";
   3.144 +val real_add_minus_iff = thm"real_add_minus_iff";
   3.145 +val real_add_eq_0_iff = thm"real_add_eq_0_iff";
   3.146 +val real_add_less_0_iff = thm"real_add_less_0_iff";
   3.147 +val real_0_less_add_iff = thm"real_0_less_add_iff";
   3.148 +val real_add_le_0_iff = thm"real_add_le_0_iff";
   3.149 +val real_0_le_add_iff = thm"real_0_le_add_iff";
   3.150 +val real_0_less_diff_iff = thm"real_0_less_diff_iff";
   3.151 +val real_0_le_diff_iff = thm"real_0_le_diff_iff";
   3.152 +val real_divide_eq_cancel2 = thm"real_divide_eq_cancel2";
   3.153 +val real_divide_eq_cancel1 = thm"real_divide_eq_cancel1";
   3.154 +val real_inverse_less_iff = thm"real_inverse_less_iff";
   3.155 +val real_inverse_le_iff = thm"real_inverse_le_iff";
   3.156 +val real_divide_1 = thm"real_divide_1";
   3.157 +val real_divide_minus1 = thm"real_divide_minus1";
   3.158 +val real_minus1_divide = thm"real_minus1_divide";
   3.159 +val real_lbound_gt_zero = thm"real_lbound_gt_zero";
   3.160 +val real_less_half_sum = thm"real_less_half_sum";
   3.161 +val real_gt_half_sum = thm"real_gt_half_sum";
   3.162 +val real_dense = thm"real_dense";
   3.163  
   3.164 -Goal "(inverse x = inverse y) = (x = (y::real))";
   3.165 -by (case_tac "x=0 | y=0" 1);
   3.166 -by (auto_tac (claset(),
   3.167 -              simpset() addsimps [real_inverse_eq_divide,
   3.168 -                                  DIVISION_BY_ZERO]));
   3.169 -by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1);
   3.170 -by (Asm_full_simp_tac 1);
   3.171 -qed "real_inverse_eq_iff";
   3.172 -Addsimps [real_inverse_eq_iff];
   3.173 -
   3.174 -Goal "(z/x = z/y) = (z = 0 | x = (y::real))";
   3.175 -by (case_tac "x=0 | y=0" 1);
   3.176 -by (auto_tac (claset(),
   3.177 -              simpset() addsimps [DIVISION_BY_ZERO]));
   3.178 -by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1);
   3.179 -by Auto_tac;
   3.180 -qed "real_divide_eq_iff";
   3.181 -Addsimps [real_divide_eq_iff];
   3.182 -
   3.183 -
   3.184 -(*** General rewrites to improve automation, like those for type "int" ***)
   3.185 -
   3.186 -(** The next several equations can make the simplifier loop! **)
   3.187 -
   3.188 -Goal "(x < - y) = (y < - (x::real))";
   3.189 -by Auto_tac;
   3.190 -qed "real_less_minus";
   3.191 -
   3.192 -Goal "(- x < y) = (- y < (x::real))";
   3.193 -by Auto_tac;
   3.194 -qed "real_minus_less";
   3.195 -
   3.196 -Goal "(x <= - y) = (y <= - (x::real))";
   3.197 -by Auto_tac;
   3.198 -qed "real_le_minus";
   3.199 -
   3.200 -Goal "(- x <= y) = (- y <= (x::real))";
   3.201 -by Auto_tac;
   3.202 -qed "real_minus_le";
   3.203 -
   3.204 -Goal "(x = - y) = (y = - (x::real))";
   3.205 -by Auto_tac;
   3.206 -qed "real_equation_minus";
   3.207 -
   3.208 -Goal "(- x = y) = (- (y::real) = x)";
   3.209 -by Auto_tac;
   3.210 -qed "real_minus_equation";
   3.211 -
   3.212 -
   3.213 -Goal "(x + - a = (0::real)) = (x=a)";
   3.214 -by (arith_tac 1);
   3.215 -qed "real_add_minus_iff";
   3.216 -Addsimps [real_add_minus_iff];
   3.217 -
   3.218 -Goal "(-b = -a) = (b = (a::real))";
   3.219 -by (arith_tac 1);
   3.220 -qed "real_minus_eq_cancel";
   3.221 -Addsimps [real_minus_eq_cancel];
   3.222 -
   3.223 -
   3.224 -(*Distributive laws for literals*)
   3.225 -Addsimps (map (inst "w" "number_of ?v")
   3.226 -          [real_add_mult_distrib, real_add_mult_distrib2,
   3.227 -           real_diff_mult_distrib, real_diff_mult_distrib2]);
   3.228 -
   3.229 -Addsimps (map (inst "x" "number_of ?v")
   3.230 -          [real_less_minus, real_le_minus, real_equation_minus]);
   3.231 -Addsimps (map (inst "y" "number_of ?v")
   3.232 -          [real_minus_less, real_minus_le, real_minus_equation]);
   3.233 -
   3.234 -(*Equations and inequations involving 1*)
   3.235 -Addsimps (map (simplify (simpset()) o inst "x" "1")
   3.236 -          [real_less_minus, real_le_minus, real_equation_minus]);
   3.237 -Addsimps (map (simplify (simpset()) o inst "y" "1")
   3.238 -          [real_minus_less, real_minus_le, real_minus_equation]);
   3.239 -
   3.240 -(*** Simprules combining x+y and 0 ***)
   3.241 -
   3.242 -Goal "(x+y = (0::real)) = (y = -x)";
   3.243 -by Auto_tac;
   3.244 -qed "real_add_eq_0_iff";
   3.245 -AddIffs [real_add_eq_0_iff];
   3.246 -
   3.247 -Goal "(x+y < (0::real)) = (y < -x)";
   3.248 -by Auto_tac;
   3.249 -qed "real_add_less_0_iff";
   3.250 -AddIffs [real_add_less_0_iff];
   3.251 -
   3.252 -Goal "((0::real) < x+y) = (-x < y)";
   3.253 -by Auto_tac;
   3.254 -qed "real_0_less_add_iff";
   3.255 -AddIffs [real_0_less_add_iff];
   3.256 -
   3.257 -Goal "(x+y <= (0::real)) = (y <= -x)";
   3.258 -by Auto_tac;
   3.259 -qed "real_add_le_0_iff";
   3.260 -AddIffs [real_add_le_0_iff];
   3.261 -
   3.262 -Goal "((0::real) <= x+y) = (-x <= y)";
   3.263 -by Auto_tac;
   3.264 -qed "real_0_le_add_iff";
   3.265 -AddIffs [real_0_le_add_iff];
   3.266 -
   3.267 -
   3.268 -(** Simprules combining x-y and 0; see also real_less_iff_diff_less_0, etc.,
   3.269 -    in RealBin
   3.270 -**)
   3.271 -
   3.272 -Goal "((0::real) < x-y) = (y < x)";
   3.273 -by Auto_tac;
   3.274 -qed "real_0_less_diff_iff";
   3.275 -AddIffs [real_0_less_diff_iff];
   3.276 -
   3.277 -Goal "((0::real) <= x-y) = (y <= x)";
   3.278 -by Auto_tac;
   3.279 -qed "real_0_le_diff_iff";
   3.280 -AddIffs [real_0_le_diff_iff];
   3.281 -
   3.282 -(*
   3.283 -FIXME: we should have this, as for type int, but many proofs would break.
   3.284 -It replaces x+-y by x-y.
   3.285 -Addsimps [symmetric real_diff_def];
   3.286 -*)
   3.287 -
   3.288 -Goal "-(x-y) = y - (x::real)";
   3.289 -by (arith_tac 1);
   3.290 -qed "real_minus_diff_eq";
   3.291 -Addsimps [real_minus_diff_eq];
   3.292 -
   3.293 -
   3.294 -(*** Density of the Reals ***)
   3.295 -
   3.296 -Goal "x < y ==> x < (x+y) / (2::real)";
   3.297 -by Auto_tac;
   3.298 -qed "real_less_half_sum";
   3.299 -
   3.300 -Goal "x < y ==> (x+y)/(2::real) < y";
   3.301 -by Auto_tac;
   3.302 -qed "real_gt_half_sum";
   3.303 -
   3.304 -Goal "x < y ==> EX r::real. x < r & r < y";
   3.305 -by (blast_tac (claset() addSIs [real_less_half_sum, real_gt_half_sum]) 1);
   3.306 -qed "real_dense";
   3.307 -
   3.308 -
   3.309 -(*Replaces "inverse #nn" by 1/#nn *)
   3.310 -Addsimps [inst "x" "number_of ?w" real_inverse_eq_divide];
   3.311 -
   3.312 -
   3.313 +val pos_real_less_divide_eq = thm"pos_real_less_divide_eq";
   3.314 +val neg_real_less_divide_eq = thm"neg_real_less_divide_eq";
   3.315 +val pos_real_divide_less_eq = thm"pos_real_divide_less_eq";
   3.316 +val neg_real_divide_less_eq = thm"neg_real_divide_less_eq";
   3.317 +val pos_real_le_divide_eq = thm"pos_real_le_divide_eq";
   3.318 +val neg_real_le_divide_eq = thm"neg_real_le_divide_eq";
   3.319 +val pos_real_divide_le_eq = thm"pos_real_divide_le_eq";
   3.320 +val neg_real_divide_le_eq = thm"neg_real_divide_le_eq";
   3.321 +val real_eq_divide_eq = thm"real_eq_divide_eq";
   3.322 +val real_divide_eq_eq = thm"real_divide_eq_eq";
     4.1 --- a/src/HOL/Real/RealArith0.thy	Sat Dec 06 07:52:17 2003 +0100
     4.2 +++ b/src/HOL/Real/RealArith0.thy	Sun Dec 07 16:30:06 2003 +0100
     4.3 @@ -1,6 +1,8 @@
     4.4  theory RealArith0 = RealBin
     4.5  files "real_arith0.ML":
     4.6  
     4.7 +(*FIXME: move results further down to Ring_and_Field*)
     4.8 +
     4.9  setup real_arith_setup
    4.10  
    4.11  subsection{*Facts that need the Arithmetic Decision Procedure*}
    4.12 @@ -54,6 +56,215 @@
    4.13       "(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)"
    4.14    by (rule Ring_and_Field.mult_divide_cancel_eq_if) 
    4.15  
    4.16 +subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
    4.17 +
    4.18 +lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)"
    4.19 +by arith
    4.20 +
    4.21 +lemma real_add_eq_0_iff [iff]: "(x+y = (0::real)) = (y = -x)"
    4.22 +by auto
    4.23 +
    4.24 +lemma real_add_less_0_iff [iff]: "(x+y < (0::real)) = (y < -x)"
    4.25 +by auto
    4.26 +
    4.27 +lemma real_0_less_add_iff [iff]: "((0::real) < x+y) = (-x < y)"
    4.28 +by auto
    4.29 +
    4.30 +lemma real_add_le_0_iff [iff]: "(x+y \<le> (0::real)) = (y \<le> -x)"
    4.31 +by auto
    4.32 +
    4.33 +lemma real_0_le_add_iff [iff]: "((0::real) \<le> x+y) = (-x \<le> y)"
    4.34 +by auto
    4.35 +
    4.36 +
    4.37 +(** Simprules combining x-y and 0; see also real_less_iff_diff_less_0, etc.,
    4.38 +    in RealBin
    4.39 +**)
    4.40 +
    4.41 +lemma real_0_less_diff_iff [iff]: "((0::real) < x-y) = (y < x)"
    4.42 +by auto
    4.43 +
    4.44 +lemma real_0_le_diff_iff [iff]: "((0::real) \<le> x-y) = (y \<le> x)"
    4.45 +by auto
    4.46 +
    4.47 +(*
    4.48 +FIXME: we should have this, as for type int, but many proofs would break.
    4.49 +It replaces x+-y by x-y.
    4.50 +Addsimps [symmetric real_diff_def]
    4.51 +*)
    4.52 +
    4.53 +
    4.54 +(*FIXME: move most of these to Ring_and_Field*)
    4.55 +
    4.56 +subsection{*Simplification of Inequalities Involving Literal Divisors*}
    4.57 +
    4.58 +lemma pos_real_le_divide_eq: "0<z ==> ((x::real) \<le> y/z) = (x*z \<le> y)"
    4.59 +apply (subgoal_tac " (x*z \<le> y) = (x*z \<le> (y/z) *z) ")
    4.60 + prefer 2 apply (simp add: real_divide_def real_mult_assoc) 
    4.61 +apply (erule ssubst)
    4.62 +apply (subst real_mult_le_cancel2, simp)
    4.63 +done
    4.64 +
    4.65 +lemma neg_real_le_divide_eq: "z<0 ==> ((x::real) \<le> y/z) = (y \<le> x*z)"
    4.66 +apply (subgoal_tac " (y \<le> x*z) = ((y/z) *z \<le> x*z) ")
    4.67 + prefer 2 apply (simp add: real_divide_def real_mult_assoc)
    4.68 +apply (erule ssubst)
    4.69 +apply (subst real_mult_le_cancel2, simp)
    4.70 +done
    4.71 +
    4.72 +lemma real_le_divide_eq:
    4.73 +  "((x::real) \<le> y/z) = (if 0<z then x*z \<le> y
    4.74 +                        else if z<0 then y \<le> x*z
    4.75 +                        else x\<le>0)"
    4.76 +apply (case_tac "z=0", simp) 
    4.77 +apply (simp add: pos_real_le_divide_eq neg_real_le_divide_eq) 
    4.78 +done
    4.79 +
    4.80 +declare real_le_divide_eq [of _ _ "number_of w", standard, simp]
    4.81 +
    4.82 +lemma pos_real_divide_le_eq: "0<z ==> (y/z \<le> (x::real)) = (y \<le> x*z)"
    4.83 +apply (subgoal_tac " (y \<le> x*z) = ((y/z) *z \<le> x*z) ")
    4.84 + prefer 2 apply (simp add: real_divide_def real_mult_assoc)
    4.85 +apply (erule ssubst)
    4.86 +apply (subst real_mult_le_cancel2, simp)
    4.87 +done
    4.88 +
    4.89 +lemma neg_real_divide_le_eq: "z<0 ==> (y/z \<le> (x::real)) = (x*z \<le> y)"
    4.90 +apply (subgoal_tac " (x*z \<le> y) = (x*z \<le> (y/z) *z) ")
    4.91 + prefer 2 apply (simp add: real_divide_def real_mult_assoc)
    4.92 +apply (erule ssubst)
    4.93 +apply (subst real_mult_le_cancel2, simp)
    4.94 +done
    4.95 +
    4.96 +
    4.97 +lemma real_divide_le_eq:
    4.98 +  "(y/z \<le> (x::real)) = (if 0<z then y \<le> x*z
    4.99 +                        else if z<0 then x*z \<le> y
   4.100 +                        else 0 \<le> x)"
   4.101 +apply (case_tac "z=0", simp) 
   4.102 +apply (simp add: pos_real_divide_le_eq neg_real_divide_le_eq) 
   4.103 +done
   4.104 +
   4.105 +declare real_divide_le_eq [of _ "number_of w", standard, simp]
   4.106  
   4.107  
   4.108 +lemma pos_real_less_divide_eq: "0<z ==> ((x::real) < y/z) = (x*z < y)"
   4.109 +apply (subgoal_tac " (x*z < y) = (x*z < (y/z) *z) ")
   4.110 + prefer 2 apply (simp add: real_divide_def real_mult_assoc)
   4.111 +apply (erule ssubst)
   4.112 +apply (subst real_mult_less_cancel2, simp)
   4.113 +done
   4.114 +
   4.115 +lemma neg_real_less_divide_eq: "z<0 ==> ((x::real) < y/z) = (y < x*z)"
   4.116 +apply (subgoal_tac " (y < x*z) = ((y/z) *z < x*z) ")
   4.117 + prefer 2 apply (simp add: real_divide_def real_mult_assoc)
   4.118 +apply (erule ssubst)
   4.119 +apply (subst real_mult_less_cancel2, simp)
   4.120 +done
   4.121 +
   4.122 +lemma real_less_divide_eq:
   4.123 +  "((x::real) < y/z) = (if 0<z then x*z < y
   4.124 +                        else if z<0 then y < x*z
   4.125 +                        else x<0)"
   4.126 +apply (case_tac "z=0", simp) 
   4.127 +apply (simp add: pos_real_less_divide_eq neg_real_less_divide_eq) 
   4.128 +done
   4.129 +
   4.130 +declare real_less_divide_eq [of _ _ "number_of w", standard, simp]
   4.131 +
   4.132 +lemma pos_real_divide_less_eq: "0<z ==> (y/z < (x::real)) = (y < x*z)"
   4.133 +apply (subgoal_tac " (y < x*z) = ((y/z) *z < x*z) ")
   4.134 + prefer 2 apply (simp add: real_divide_def real_mult_assoc)
   4.135 +apply (erule ssubst)
   4.136 +apply (subst real_mult_less_cancel2, simp)
   4.137 +done
   4.138 +
   4.139 +lemma neg_real_divide_less_eq: "z<0 ==> (y/z < (x::real)) = (x*z < y)"
   4.140 +apply (subgoal_tac " (x*z < y) = (x*z < (y/z) *z) ")
   4.141 + prefer 2 apply (simp add: real_divide_def real_mult_assoc)
   4.142 +apply (erule ssubst)
   4.143 +apply (subst real_mult_less_cancel2, simp)
   4.144 +done
   4.145 +
   4.146 +lemma real_divide_less_eq:
   4.147 +  "(y/z < (x::real)) = (if 0<z then y < x*z
   4.148 +                        else if z<0 then x*z < y
   4.149 +                        else 0 < x)"
   4.150 +apply (case_tac "z=0", simp) 
   4.151 +apply (simp add: pos_real_divide_less_eq neg_real_divide_less_eq) 
   4.152 +done
   4.153 +
   4.154 +declare real_divide_less_eq [of _ "number_of w", standard, simp]
   4.155 +
   4.156 +lemma nonzero_real_eq_divide_eq: "z\<noteq>0 ==> ((x::real) = y/z) = (x*z = y)"
   4.157 +apply (subgoal_tac " (x*z = y) = (x*z = (y/z) *z) ")
   4.158 + prefer 2 apply (simp add: real_divide_def real_mult_assoc)
   4.159 +apply (erule ssubst)
   4.160 +apply (subst real_mult_eq_cancel2, simp)
   4.161 +done
   4.162 +
   4.163 +lemma real_eq_divide_eq:
   4.164 +  "((x::real) = y/z) = (if z\<noteq>0 then x*z = y else x=0)"
   4.165 +by (simp add: nonzero_real_eq_divide_eq) 
   4.166 +
   4.167 +declare real_eq_divide_eq [of _ _ "number_of w", standard, simp]
   4.168 +
   4.169 +lemma nonzero_real_divide_eq_eq: "z\<noteq>0 ==> (y/z = (x::real)) = (y = x*z)"
   4.170 +apply (subgoal_tac " (y = x*z) = ((y/z) *z = x*z) ")
   4.171 + prefer 2 apply (simp add: real_divide_def real_mult_assoc)
   4.172 +apply (erule ssubst)
   4.173 +apply (subst real_mult_eq_cancel2, simp)
   4.174 +done
   4.175 +
   4.176 +lemma real_divide_eq_eq:
   4.177 +  "(y/z = (x::real)) = (if z\<noteq>0 then y = x*z else x=0)"
   4.178 +by (simp add: nonzero_real_divide_eq_eq) 
   4.179 +
   4.180 +declare real_divide_eq_eq [of _ "number_of w", standard, simp]
   4.181 +
   4.182 +lemma real_divide_eq_cancel2: "(m/k = n/k) = (k = 0 | m = (n::real))"
   4.183 +apply (case_tac "k=0", simp) 
   4.184 +apply (simp add:divide_inverse) 
   4.185 +done
   4.186 +
   4.187 +lemma real_divide_eq_cancel1: "(k/m = k/n) = (k = 0 | m = (n::real))" 
   4.188 +by (force simp add: real_divide_eq_eq real_eq_divide_eq)
   4.189 +
   4.190 +lemma real_inverse_less_iff:
   4.191 +     "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)"
   4.192 +by (rule Ring_and_Field.inverse_less_iff_less)
   4.193 +
   4.194 +lemma real_inverse_le_iff:
   4.195 +     "[| 0 < r; 0 < x|] ==> (inverse x \<le> inverse r) = (r \<le> (x::real))"
   4.196 +by (rule Ring_and_Field.inverse_le_iff_le)
   4.197 +
   4.198 +
   4.199 +(** Division by 1, -1 **)
   4.200 +
   4.201 +lemma real_divide_1: "(x::real)/1 = x"
   4.202 +by (simp add: real_divide_def)
   4.203 +
   4.204 +lemma real_divide_minus1 [simp]: "x/-1 = -(x::real)"
   4.205 +by simp
   4.206 +
   4.207 +lemma real_minus1_divide [simp]: "-1/(x::real) = - (1/x)"
   4.208 +by (simp add: real_divide_def real_minus_inverse)
   4.209 +
   4.210 +lemma real_lbound_gt_zero:
   4.211 +     "[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2"
   4.212 +apply (rule_tac x = " (min d1 d2) /2" in exI)
   4.213 +apply (simp add: min_def)
   4.214 +done
   4.215 +
   4.216 +(*** Density of the Reals ***)
   4.217 +
   4.218 +lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)"
   4.219 +by auto
   4.220 +
   4.221 +lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"
   4.222 +by auto
   4.223 +
   4.224 +lemma real_dense: "x < y ==> \<exists>r::real. x < r & r < y"
   4.225 +by (blast intro!: real_less_half_sum real_gt_half_sum)
   4.226 +
   4.227  end
     5.1 --- a/src/HOL/Real/RealOrd.thy	Sat Dec 06 07:52:17 2003 +0100
     5.2 +++ b/src/HOL/Real/RealOrd.thy	Sun Dec 07 16:30:06 2003 +0100
     5.3 @@ -360,16 +360,9 @@
     5.4  lemma real_le_add_right_cancel: "!!(A::real). A + C \<le> B + C ==> A \<le> B"
     5.5    by (rule Ring_and_Field.add_le_imp_le_right)
     5.6  
     5.7 -		lemma add_le_imp_le_left:
     5.8 -		      "c + a \<le> c + b ==> a \<le> (b::'a::ordered_ring)"
     5.9 -		by simp
    5.10 -
    5.11  lemma real_le_add_left_cancel: "!!(A::real). C + A \<le> C + B ==> A \<le> B"
    5.12    by (rule (*Ring_and_Field.*)add_le_imp_le_left)
    5.13  
    5.14 -lemma real_minus_diff_eq: "- (z - y) = y - (z::real)"
    5.15 -  by (rule Ring_and_Field.minus_diff_eq)
    5.16 -
    5.17  lemma real_add_right_cancel_less [simp]: "(v+z < w+z) = (v < (w::real))"
    5.18    by (rule Ring_and_Field.add_less_cancel_right)
    5.19  
    5.20 @@ -910,7 +903,6 @@
    5.21  val real_sum_gt_zero_less = thm"real_sum_gt_zero_less";
    5.22  val real_less_sum_gt_0_iff = thm"real_less_sum_gt_0_iff";
    5.23  
    5.24 -val real_minus_diff_eq = thm "real_minus_diff_eq";
    5.25  val real_gt_zero_preal_Ex = thm "real_gt_zero_preal_Ex";
    5.26  val real_gt_preal_preal_Ex = thm "real_gt_preal_preal_Ex";
    5.27  val real_ge_preal_preal_Ex = thm "real_ge_preal_preal_Ex";
     6.1 --- a/src/HOL/Ring_and_Field.thy	Sat Dec 06 07:52:17 2003 +0100
     6.2 +++ b/src/HOL/Ring_and_Field.thy	Sun Dec 07 16:30:06 2003 +0100
     6.3 @@ -901,6 +901,9 @@
     6.4        (if c=0 then 0 else a / (b::'a::{field,division_by_zero}))"
     6.5    by (simp add: mult_divide_cancel_left)
     6.6  
     6.7 +lemma divide_1 [simp]: "a/1 = (a::'a::field)"
     6.8 +  by (simp add: divide_inverse [OF not_sym])
     6.9 +
    6.10  
    6.11  subsection {* Ordered Fields *}
    6.12  
    6.13 @@ -1088,5 +1091,4 @@
    6.14       "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
    6.15  by (simp add: divide_inverse_zero field_mult_eq_0_iff)
    6.16  
    6.17 -
    6.18  end