10648

1 
(* Title: HOL/Real/RealArith.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1999 University of Cambridge


5 


6 
Assorted facts that need binary literals and the arithmetic decision procedure


7 


8 
Also, common factor cancellation


9 
*)


10 


11 
(** Division and inverse **)


12 


13 
Goal "((#0::real) < inverse x) = (#0 < x)";


14 
by (case_tac "x=#0" 1);


15 
by (asm_simp_tac (HOL_ss addsimps [rename_numerals INVERSE_ZERO]) 1);


16 
by (auto_tac (claset() addDs [rename_numerals real_inverse_less_zero],


17 
simpset() addsimps [linorder_neq_iff,


18 
rename_numerals real_inverse_gt_zero]));


19 
qed "real_0_less_inverse_iff";


20 
AddIffs [real_0_less_inverse_iff];


21 


22 
Goal "(inverse x < (#0::real)) = (x < #0)";


23 
by (case_tac "x=#0" 1);


24 
by (asm_simp_tac (HOL_ss addsimps [rename_numerals INVERSE_ZERO]) 1);


25 
by (auto_tac (claset() addDs [rename_numerals real_inverse_less_zero],


26 
simpset() addsimps [linorder_neq_iff,


27 
rename_numerals real_inverse_gt_zero]));


28 
qed "real_inverse_less_0_iff";


29 
AddIffs [real_inverse_less_0_iff];


30 

10660

31 
Goal "((#0::real) <= inverse x) = (#0 <= x)";


32 
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);


33 
qed "real_0_le_inverse_iff";


34 
AddIffs [real_0_le_inverse_iff];


35 


36 
Goal "(inverse x <= (#0::real)) = (x <= #0)";


37 
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);


38 
qed "real_inverse_le_0_iff";


39 
AddIffs [real_inverse_le_0_iff];


40 

10648

41 
Goalw [real_divide_def] "x/(#0::real) = #0";


42 
by (stac (rename_numerals INVERSE_ZERO) 1);


43 
by (Simp_tac 1);


44 
qed "REAL_DIVIDE_ZERO";


45 


46 
(*generalize?*)


47 
Goal "((#0::real) < #1/x) = (#0 < x)";


48 
by (simp_tac (simpset() addsimps [real_divide_def]) 1);


49 
qed "real_0_less_recip_iff";


50 
AddIffs [real_0_less_recip_iff];


51 


52 
Goal "(#1/x < (#0::real)) = (x < #0)";


53 
by (simp_tac (simpset() addsimps [real_divide_def]) 1);


54 
qed "real_recip_less_0_iff";


55 
AddIffs [real_recip_less_0_iff];


56 


57 
Goal "inverse (x::real) = #1/x";


58 
by (simp_tac (simpset() addsimps [real_divide_def]) 1);


59 
qed "real_inverse_eq_divide";


60 


61 
Goal "(x::real)/#1 = x";


62 
by (simp_tac (simpset() addsimps [real_divide_def]) 1);


63 
qed "real_divide_1";


64 
Addsimps [real_divide_1];


65 


66 


67 
(**** Factor cancellation theorems for "real" ****)


68 


69 
(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,


70 
but not (yet?) for k*m < n*k. **)


71 


72 
bind_thm ("real_mult_minus_right", real_minus_mult_eq2 RS sym);


73 

10660

74 
Goal "(y < x) = ((x::real) < y)";


75 
by (arith_tac 1);


76 
qed "real_minus_less_minus";


77 

10648

78 
Goal "[ i<j; k < (0::real) ] ==> j*k < i*k";


79 
by (rtac (real_minus_less_minus RS iffD1) 1);


80 
by (auto_tac (claset(),


81 
simpset() delsimps [real_minus_mult_eq2 RS sym]


82 
addsimps [real_minus_mult_eq2]));


83 
qed "real_mult_less_mono1_neg";


84 


85 
Goal "[ i<j; k < (0::real) ] ==> k*j < k*i";


86 
by (rtac (real_minus_less_minus RS iffD1) 1);


87 
by (auto_tac (claset(),


88 
simpset() delsimps [real_minus_mult_eq1 RS sym]


89 
addsimps [real_minus_mult_eq1]));;


90 
qed "real_mult_less_mono2_neg";


91 


92 
Goal "[ i <= j; (0::real) <= k ] ==> i*k <= j*k";


93 
by (auto_tac (claset(),


94 
simpset() addsimps [order_le_less, real_mult_less_mono1]));


95 
qed "real_mult_le_mono1";


96 


97 
Goal "[ i <= j; k <= (0::real) ] ==> j*k <= i*k";


98 
by (auto_tac (claset(),


99 
simpset() addsimps [order_le_less, real_mult_less_mono1_neg]));


100 
qed "real_mult_le_mono1_neg";


101 


102 
Goal "[ i <= j; (0::real) <= k ] ==> k*i <= k*j";


103 
by (dtac real_mult_le_mono1 1);


104 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [real_mult_commute])));


105 
qed "real_mult_le_mono2";


106 


107 
Goal "[ i <= j; k <= (0::real) ] ==> k*j <= k*i";


108 
by (dtac real_mult_le_mono1_neg 1);


109 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [real_mult_commute])));


110 
qed "real_mult_le_mono2_neg";


111 


112 
Goal "(m*k < n*k) = (((#0::real) < k & m<n)  (k < #0 & n<m))";


113 
by (case_tac "k = (0::real)" 1);


114 
by (auto_tac (claset(),


115 
simpset() addsimps [linorder_neq_iff,


116 
real_mult_less_mono1, real_mult_less_mono1_neg]));


117 
by (auto_tac (claset(),


118 
simpset() addsimps [linorder_not_less,


119 
inst "y1" "m*k" (linorder_not_le RS sym),


120 
inst "y1" "m" (linorder_not_le RS sym)]));


121 
by (TRYALL (etac notE));


122 
by (auto_tac (claset(),


123 
simpset() addsimps [order_less_imp_le, real_mult_le_mono1,


124 
real_mult_le_mono1_neg]));


125 
qed "real_mult_less_cancel2";


126 


127 
Goal "(m*k <= n*k) = (((#0::real) < k > m<=n) & (k < #0 > n<=m))";


128 
by (simp_tac (simpset() addsimps [linorder_not_less RS sym,


129 
real_mult_less_cancel2]) 1);


130 
qed "real_mult_le_cancel2";


131 


132 
Goal "(k*m < k*n) = (((#0::real) < k & m<n)  (k < #0 & n<m))";


133 
by (simp_tac (simpset() addsimps [inst "z" "k" real_mult_commute,


134 
real_mult_less_cancel2]) 1);


135 
qed "real_mult_less_cancel1";


136 


137 
Goal "!!k::real. (k*m <= k*n) = ((#0 < k > m<=n) & (k < #0 > n<=m))";


138 
by (simp_tac (simpset() addsimps [linorder_not_less RS sym,


139 
real_mult_less_cancel1]) 1);


140 
qed "real_mult_le_cancel1";


141 


142 
Goal "!!k::real. (k*m = k*n) = (k = #0  m=n)";


143 
by (case_tac "k=0" 1);


144 
by (auto_tac (claset(), simpset() addsimps [real_mult_left_cancel]));


145 
qed "real_mult_eq_cancel1";


146 


147 
Goal "!!k::real. (m*k = n*k) = (k = #0  m=n)";


148 
by (case_tac "k=0" 1);


149 
by (auto_tac (claset(), simpset() addsimps [real_mult_right_cancel]));


150 
qed "real_mult_eq_cancel2";


151 


152 
Goal "!!k::real. k~=#0 ==> (k*m) / (k*n) = (m/n)";


153 
by (asm_simp_tac


154 
(simpset() addsimps [real_divide_def, real_inverse_distrib]) 1);


155 
by (subgoal_tac "k * m * (inverse k * inverse n) = \


156 
\ (k * inverse k) * (m * inverse n)" 1);


157 
by (asm_full_simp_tac (simpset() addsimps []) 1);


158 
by (asm_full_simp_tac (HOL_ss addsimps real_mult_ac) 1);


159 
qed "real_mult_div_cancel1";


160 


161 


162 
local


163 
open Real_Numeral_Simprocs


164 
in


165 


166 
val rel_real_number_of = [eq_real_number_of, less_real_number_of,


167 
le_real_number_of_eq_not_less];


168 


169 
structure CancelNumeralFactorCommon =


170 
struct


171 
val mk_coeff = mk_coeff


172 
val dest_coeff = dest_coeff 1


173 
val trans_tac = trans_tac


174 
val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_plus_1s))


175 
THEN ALLGOALS


176 
(simp_tac


177 
(HOL_ss addsimps [eq_real_number_of,


178 
real_mult_minus_right RS sym]@


179 
[mult_real_number_of, real_mult_number_of_left]@bin_simps@real_mult_ac))


180 
val numeral_simp_tac =


181 
ALLGOALS (simp_tac (HOL_ss addsimps rel_real_number_of@bin_simps))


182 
val simplify_meta_eq = simplify_meta_eq


183 
end


184 


185 
structure DivCancelNumeralFactor = CancelNumeralFactorFun


186 
(open CancelNumeralFactorCommon


187 
val prove_conv = prove_conv "realdiv_cancel_numeral_factor"


188 
val mk_bal = HOLogic.mk_binop "HOL.divide"


189 
val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT


190 
val cancel = real_mult_div_cancel1 RS trans


191 
val neg_exchanges = false


192 
)


193 


194 
structure EqCancelNumeralFactor = CancelNumeralFactorFun


195 
(open CancelNumeralFactorCommon


196 
val prove_conv = prove_conv "realeq_cancel_numeral_factor"


197 
val mk_bal = HOLogic.mk_eq


198 
val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT


199 
val cancel = real_mult_eq_cancel1 RS trans


200 
val neg_exchanges = false


201 
)


202 


203 
structure LessCancelNumeralFactor = CancelNumeralFactorFun


204 
(open CancelNumeralFactorCommon


205 
val prove_conv = prove_conv "realless_cancel_numeral_factor"


206 
val mk_bal = HOLogic.mk_binrel "op <"


207 
val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT


208 
val cancel = real_mult_less_cancel1 RS trans


209 
val neg_exchanges = true


210 
)


211 


212 
structure LeCancelNumeralFactor = CancelNumeralFactorFun


213 
(open CancelNumeralFactorCommon


214 
val prove_conv = prove_conv "realle_cancel_numeral_factor"


215 
val mk_bal = HOLogic.mk_binrel "op <="


216 
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT


217 
val cancel = real_mult_le_cancel1 RS trans


218 
val neg_exchanges = true


219 
)


220 


221 
val real_cancel_numeral_factors =


222 
map prep_simproc


223 
[("realeq_cancel_numeral_factors",


224 
prep_pats ["(l::real) * m = n", "(l::real) = m * n"],


225 
EqCancelNumeralFactor.proc),


226 
("realless_cancel_numeral_factors",


227 
prep_pats ["(l::real) * m < n", "(l::real) < m * n"],


228 
LessCancelNumeralFactor.proc),


229 
("realle_cancel_numeral_factors",


230 
prep_pats ["(l::real) * m <= n", "(l::real) <= m * n"],


231 
LeCancelNumeralFactor.proc),


232 
("realdiv_cancel_numeral_factors",


233 
prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)"],


234 
DivCancelNumeralFactor.proc)];


235 


236 
end;


237 


238 
Addsimprocs real_cancel_numeral_factors;


239 


240 


241 
(*examples:


242 
print_depth 22;


243 
set timing;


244 
set trace_simp;


245 
fun test s = (Goal s; by (Simp_tac 1));


246 


247 
test "#0 <= (y::real) * #2";


248 
test "#9*x = #12 * (y::real)";


249 
test "(#9*x) / (#12 * (y::real)) = z";


250 
test "#9*x < #12 * (y::real)";


251 
test "#9*x <= #12 * (y::real)";


252 


253 
test "#99*x = #132 * (y::real)";


254 
test "(#99*x) / (#132 * (y::real)) = z";


255 
test "#99*x < #132 * (y::real)";


256 
test "#99*x <= #132 * (y::real)";


257 


258 
test "#999*x = #396 * (y::real)";


259 
test "(#999*x) / (#396 * (y::real)) = z";


260 
test "#999*x < #396 * (y::real)";


261 
test "#999*x <= #396 * (y::real)";


262 


263 
test "#99*x = #81 * (y::real)";


264 
test "(#99*x) / (#81 * (y::real)) = z";


265 
test "#99*x <= #81 * (y::real)";


266 
test "#99*x < #81 * (y::real)";


267 


268 
test "#2 * x = #1 * (y::real)";


269 
test "#2 * x = (y::real)";


270 
test "(#2 * x) / (#1 * (y::real)) = z";


271 
test "#2 * x < (y::real)";


272 
test "#2 * x <= #1 * (y::real)";


273 
test "x < #23 * (y::real)";


274 
test "x <= #23 * (y::real)";


275 
*)


276 


277 
(*** Simplification of inequalities involving literal divisors ***)


278 


279 
Goal "#0<z ==> ((x::real) <= y/z) = (x*z <= y)";


280 
by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);


281 
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);


282 
by (etac ssubst 1);


283 
by (stac real_mult_le_cancel2 1);


284 
by (Asm_simp_tac 1);


285 
qed "pos_real_le_divide_eq";


286 
Addsimps [inst "z" "number_of ?w" pos_real_le_divide_eq];


287 


288 
Goal "z<#0 ==> ((x::real) <= y/z) = (y <= x*z)";


289 
by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);


290 
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);


291 
by (etac ssubst 1);


292 
by (stac real_mult_le_cancel2 1);


293 
by (Asm_simp_tac 1);


294 
qed "neg_real_le_divide_eq";


295 
Addsimps [inst "z" "number_of ?w" neg_real_le_divide_eq];


296 


297 
Goal "#0<z ==> (y/z <= (x::real)) = (y <= x*z)";


298 
by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);


299 
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);


300 
by (etac ssubst 1);


301 
by (stac real_mult_le_cancel2 1);


302 
by (Asm_simp_tac 1);


303 
qed "pos_real_divide_le_eq";


304 
Addsimps [inst "z" "number_of ?w" pos_real_divide_le_eq];


305 


306 
Goal "z<#0 ==> (y/z <= (x::real)) = (x*z <= y)";


307 
by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);


308 
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);


309 
by (etac ssubst 1);


310 
by (stac real_mult_le_cancel2 1);


311 
by (Asm_simp_tac 1);


312 
qed "neg_real_divide_le_eq";


313 
Addsimps [inst "z" "number_of ?w" neg_real_divide_le_eq];


314 


315 
Goal "#0<z ==> ((x::real) < y/z) = (x*z < y)";


316 
by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);


317 
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);


318 
by (etac ssubst 1);


319 
by (stac real_mult_less_cancel2 1);


320 
by (Asm_simp_tac 1);


321 
qed "pos_real_less_divide_eq";


322 
Addsimps [inst "z" "number_of ?w" pos_real_less_divide_eq];


323 


324 
Goal "z<#0 ==> ((x::real) < y/z) = (y < x*z)";


325 
by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);


326 
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);


327 
by (etac ssubst 1);


328 
by (stac real_mult_less_cancel2 1);


329 
by (Asm_simp_tac 1);


330 
qed "neg_real_less_divide_eq";


331 
Addsimps [inst "z" "number_of ?w" neg_real_less_divide_eq];


332 


333 
Goal "#0<z ==> (y/z < (x::real)) = (y < x*z)";


334 
by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);


335 
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);


336 
by (etac ssubst 1);


337 
by (stac real_mult_less_cancel2 1);


338 
by (Asm_simp_tac 1);


339 
qed "pos_real_divide_less_eq";


340 
Addsimps [inst "z" "number_of ?w" pos_real_divide_less_eq];


341 


342 
Goal "z<#0 ==> (y/z < (x::real)) = (x*z < y)";


343 
by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);


344 
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);


345 
by (etac ssubst 1);


346 
by (stac real_mult_less_cancel2 1);


347 
by (Asm_simp_tac 1);


348 
qed "neg_real_divide_less_eq";


349 
Addsimps [inst "z" "number_of ?w" neg_real_divide_less_eq];


350 


351 
Goal "z~=#0 ==> ((x::real) = y/z) = (x*z = y)";


352 
by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1);


353 
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);


354 
by (etac ssubst 1);


355 
by (stac real_mult_eq_cancel2 1);


356 
by (Asm_simp_tac 1);


357 
qed "real_eq_divide_eq";


358 
Addsimps [inst "z" "number_of ?w" real_eq_divide_eq];


359 


360 
Goal "z~=#0 ==> (y/z = (x::real)) = (y = x*z)";


361 
by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1);


362 
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);


363 
by (etac ssubst 1);


364 
by (stac real_mult_eq_cancel2 1);


365 
by (Asm_simp_tac 1);


366 
qed "real_divide_eq_eq";


367 
Addsimps [inst "z" "number_of ?w" real_divide_eq_eq];


368 


369 


370 
(** Moved from RealOrd.ML to use #0 **)


371 


372 
Goal "[ #0 < r; #0 < x] ==> (inverse x < inverse (r::real)) = (r < x)";


373 
by (auto_tac (claset() addIs [real_inverse_less_swap], simpset()));


374 
by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1);


375 
by (res_inst_tac [("t","x")] (real_inverse_inverse RS subst) 1);


376 
by (auto_tac (claset() addIs [real_inverse_less_swap],


377 
simpset() delsimps [real_inverse_inverse]


378 
addsimps [real_inverse_gt_zero]));


379 
qed "real_inverse_less_iff";


380 


381 
Goal "[ #0 < r; #0 < x] ==> (inverse x <= inverse r) = (r <= (x::real))";


382 
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,


383 
real_inverse_less_iff]) 1);


384 
qed "real_inverse_le_iff";


385 

10669

386 
Goal "[ (#0::real) < d1; #0 < d2 ] ==> EX e. #0 < e & e < d1 & e < d2";


387 
by (res_inst_tac [("x","(min d1 d2)/#2")] exI 1);


388 
by (asm_simp_tac (simpset() addsimps [min_def]) 1);


389 
qed "real_lbound_gt_zero";
