--- a/src/HOL/Real/RealArith.ML Thu Dec 21 18:53:32 2000 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,655 +0,0 @@
-(* Title: HOL/Real/RealArith.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1999 University of Cambridge
-
-Assorted facts that need binary literals and the arithmetic decision procedure
-
-Also, common factor cancellation
-*)
-
-(** Division and inverse **)
-
-Goal "#0/x = (#0::real)";
-by (simp_tac (simpset() addsimps [real_divide_def]) 1);
-qed "real_0_divide";
-Addsimps [real_0_divide];
-
-Goal "((#0::real) < inverse x) = (#0 < x)";
-by (case_tac "x=#0" 1);
-by (asm_simp_tac (HOL_ss addsimps [rename_numerals INVERSE_ZERO]) 1);
-by (auto_tac (claset() addDs [rename_numerals real_inverse_less_zero],
- simpset() addsimps [linorder_neq_iff,
- rename_numerals real_inverse_gt_zero]));
-qed "real_0_less_inverse_iff";
-AddIffs [real_0_less_inverse_iff];
-
-Goal "(inverse x < (#0::real)) = (x < #0)";
-by (case_tac "x=#0" 1);
-by (asm_simp_tac (HOL_ss addsimps [rename_numerals INVERSE_ZERO]) 1);
-by (auto_tac (claset() addDs [rename_numerals real_inverse_less_zero],
- simpset() addsimps [linorder_neq_iff,
- rename_numerals real_inverse_gt_zero]));
-qed "real_inverse_less_0_iff";
-AddIffs [real_inverse_less_0_iff];
-
-Goal "((#0::real) <= inverse x) = (#0 <= x)";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
-qed "real_0_le_inverse_iff";
-AddIffs [real_0_le_inverse_iff];
-
-Goal "(inverse x <= (#0::real)) = (x <= #0)";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
-qed "real_inverse_le_0_iff";
-AddIffs [real_inverse_le_0_iff];
-
-Goalw [real_divide_def] "x/(#0::real) = #0";
-by (stac (rename_numerals INVERSE_ZERO) 1);
-by (Simp_tac 1);
-qed "REAL_DIVIDE_ZERO";
-
-(*generalize?*)
-Goal "((#0::real) < #1/x) = (#0 < x)";
-by (simp_tac (simpset() addsimps [real_divide_def]) 1);
-qed "real_0_less_recip_iff";
-AddIffs [real_0_less_recip_iff];
-
-Goal "(#1/x < (#0::real)) = (x < #0)";
-by (simp_tac (simpset() addsimps [real_divide_def]) 1);
-qed "real_recip_less_0_iff";
-AddIffs [real_recip_less_0_iff];
-
-Goal "inverse (x::real) = #1/x";
-by (simp_tac (simpset() addsimps [real_divide_def]) 1);
-qed "real_inverse_eq_divide";
-
-Goal "((#0::real) < x/y) = (#0 < x & #0 < y | x < #0 & y < #0)";
-by (simp_tac (simpset() addsimps [real_divide_def, real_0_less_mult_iff]) 1);
-qed "real_0_less_divide_iff";
-Addsimps [inst "x" "number_of ?w" real_0_less_divide_iff];
-
-Goal "(x/y < (#0::real)) = (#0 < x & y < #0 | x < #0 & #0 < y)";
-by (simp_tac (simpset() addsimps [real_divide_def, real_mult_less_0_iff]) 1);
-qed "real_divide_less_0_iff";
-Addsimps [inst "x" "number_of ?w" real_divide_less_0_iff];
-
-Goal "((#0::real) <= x/y) = ((x <= #0 | #0 <= y) & (#0 <= x | y <= #0))";
-by (simp_tac (simpset() addsimps [real_divide_def, real_0_le_mult_iff]) 1);
-by Auto_tac;
-qed "real_0_le_divide_iff";
-Addsimps [inst "x" "number_of ?w" real_0_le_divide_iff];
-
-Goal "(x/y <= (#0::real)) = ((x <= #0 | y <= #0) & (#0 <= x | #0 <= y))";
-by (simp_tac (simpset() addsimps [real_divide_def, real_mult_le_0_iff]) 1);
-by Auto_tac;
-qed "real_divide_le_0_iff";
-Addsimps [inst "x" "number_of ?w" real_divide_le_0_iff];
-
-Goal "(inverse(x::real) = #0) = (x = #0)";
-by (auto_tac (claset(), simpset() addsimps [rename_numerals INVERSE_ZERO]));
-by (rtac ccontr 1);
-by (blast_tac (claset() addDs [rename_numerals real_inverse_not_zero]) 1);
-qed "real_inverse_zero_iff";
-AddIffs [real_inverse_zero_iff];
-
-Goal "(x/y = #0) = (x=#0 | y=(#0::real))";
-by (auto_tac (claset(), simpset() addsimps [real_divide_def]));
-qed "real_divide_eq_0_iff";
-AddIffs [real_divide_eq_0_iff];
-
-
-(**** Factor cancellation theorems for "real" ****)
-
-(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
- but not (yet?) for k*m < n*k. **)
-
-bind_thm ("real_mult_minus_right", real_minus_mult_eq2 RS sym);
-
-Goal "(-y < -x) = ((x::real) < y)";
-by (arith_tac 1);
-qed "real_minus_less_minus";
-Addsimps [real_minus_less_minus];
-
-Goal "[| i<j; k < (0::real) |] ==> j*k < i*k";
-by (rtac (real_minus_less_minus RS iffD1) 1);
-by (auto_tac (claset(),
- simpset() delsimps [real_minus_mult_eq2 RS sym]
- addsimps [real_minus_mult_eq2]));
-qed "real_mult_less_mono1_neg";
-
-Goal "[| i<j; k < (0::real) |] ==> k*j < k*i";
-by (rtac (real_minus_less_minus RS iffD1) 1);
-by (auto_tac (claset(),
- simpset() delsimps [real_minus_mult_eq1 RS sym]
- addsimps [real_minus_mult_eq1]));;
-qed "real_mult_less_mono2_neg";
-
-Goal "[| i <= j; (0::real) <= k |] ==> i*k <= j*k";
-by (auto_tac (claset(),
- simpset() addsimps [order_le_less, real_mult_less_mono1]));
-qed "real_mult_le_mono1";
-
-Goal "[| i <= j; k <= (0::real) |] ==> j*k <= i*k";
-by (auto_tac (claset(),
- simpset() addsimps [order_le_less, real_mult_less_mono1_neg]));
-qed "real_mult_le_mono1_neg";
-
-Goal "[| i <= j; (0::real) <= k |] ==> k*i <= k*j";
-by (dtac real_mult_le_mono1 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [real_mult_commute])));
-qed "real_mult_le_mono2";
-
-Goal "[| i <= j; k <= (0::real) |] ==> k*j <= k*i";
-by (dtac real_mult_le_mono1_neg 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [real_mult_commute])));
-qed "real_mult_le_mono2_neg";
-
-Goal "(m*k < n*k) = (((#0::real) < k & m<n) | (k < #0 & n<m))";
-by (case_tac "k = (0::real)" 1);
-by (auto_tac (claset(),
- simpset() addsimps [linorder_neq_iff,
- real_mult_less_mono1, real_mult_less_mono1_neg]));
-by (auto_tac (claset(),
- simpset() addsimps [linorder_not_less,
- inst "y1" "m*k" (linorder_not_le RS sym),
- inst "y1" "m" (linorder_not_le RS sym)]));
-by (TRYALL (etac notE));
-by (auto_tac (claset(),
- simpset() addsimps [order_less_imp_le, real_mult_le_mono1,
- real_mult_le_mono1_neg]));
-qed "real_mult_less_cancel2";
-
-Goal "(m*k <= n*k) = (((#0::real) < k --> m<=n) & (k < #0 --> n<=m))";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
- real_mult_less_cancel2]) 1);
-qed "real_mult_le_cancel2";
-
-Goal "(k*m < k*n) = (((#0::real) < k & m<n) | (k < #0 & n<m))";
-by (simp_tac (simpset() addsimps [inst "z" "k" real_mult_commute,
- real_mult_less_cancel2]) 1);
-qed "real_mult_less_cancel1";
-
-Goal "!!k::real. (k*m <= k*n) = ((#0 < k --> m<=n) & (k < #0 --> n<=m))";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
- real_mult_less_cancel1]) 1);
-qed "real_mult_le_cancel1";
-
-Goal "!!k::real. (k*m = k*n) = (k = #0 | m=n)";
-by (case_tac "k=0" 1);
-by (auto_tac (claset(), simpset() addsimps [real_mult_left_cancel]));
-qed "real_mult_eq_cancel1";
-
-Goal "!!k::real. (m*k = n*k) = (k = #0 | m=n)";
-by (case_tac "k=0" 1);
-by (auto_tac (claset(), simpset() addsimps [real_mult_right_cancel]));
-qed "real_mult_eq_cancel2";
-
-Goal "!!k::real. k~=#0 ==> (k*m) / (k*n) = (m/n)";
-by (asm_simp_tac
- (simpset() addsimps [real_divide_def, real_inverse_distrib]) 1);
-by (subgoal_tac "k * m * (inverse k * inverse n) = \
-\ (k * inverse k) * (m * inverse n)" 1);
-by (asm_full_simp_tac (simpset() addsimps []) 1);
-by (asm_full_simp_tac (HOL_ss addsimps real_mult_ac) 1);
-qed "real_mult_div_cancel1";
-
-(*For ExtractCommonTerm*)
-Goal "(k*m) / (k*n) = (if k = (#0::real) then #0 else m/n)";
-by (simp_tac (simpset() addsimps [real_mult_div_cancel1]) 1);
-qed "real_mult_div_cancel_disj";
-
-
-local
- open Real_Numeral_Simprocs
-in
-
-val rel_real_number_of = [eq_real_number_of, less_real_number_of,
- le_real_number_of_eq_not_less];
-
-structure CancelNumeralFactorCommon =
- struct
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
- val trans_tac = trans_tac
- val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_plus_1s))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
- THEN ALLGOALS
- (simp_tac
- (HOL_ss addsimps [eq_real_number_of, mult_real_number_of,
- real_mult_number_of_left]@
- real_minus_from_mult_simps @ real_mult_ac))
- val numeral_simp_tac =
- ALLGOALS (simp_tac (HOL_ss addsimps rel_real_number_of@bin_simps))
- val simplify_meta_eq = simplify_meta_eq
- end
-
-structure DivCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
- val prove_conv = prove_conv "realdiv_cancel_numeral_factor"
- val mk_bal = HOLogic.mk_binop "HOL.divide"
- val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
- val cancel = real_mult_div_cancel1 RS trans
- val neg_exchanges = false
-)
-
-structure EqCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
- val prove_conv = prove_conv "realeq_cancel_numeral_factor"
- val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
- val cancel = real_mult_eq_cancel1 RS trans
- val neg_exchanges = false
-)
-
-structure LessCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
- val prove_conv = prove_conv "realless_cancel_numeral_factor"
- val mk_bal = HOLogic.mk_binrel "op <"
- val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT
- val cancel = real_mult_less_cancel1 RS trans
- val neg_exchanges = true
-)
-
-structure LeCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
- val prove_conv = prove_conv "realle_cancel_numeral_factor"
- val mk_bal = HOLogic.mk_binrel "op <="
- val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT
- val cancel = real_mult_le_cancel1 RS trans
- val neg_exchanges = true
-)
-
-val real_cancel_numeral_factors =
- map prep_simproc
- [("realeq_cancel_numeral_factor",
- prep_pats ["(l::real) * m = n", "(l::real) = m * n"],
- EqCancelNumeralFactor.proc),
- ("realless_cancel_numeral_factor",
- prep_pats ["(l::real) * m < n", "(l::real) < m * n"],
- LessCancelNumeralFactor.proc),
- ("realle_cancel_numeral_factor",
- prep_pats ["(l::real) * m <= n", "(l::real) <= m * n"],
- LeCancelNumeralFactor.proc),
- ("realdiv_cancel_numeral_factor",
- prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)"],
- DivCancelNumeralFactor.proc)];
-
-end;
-
-Addsimprocs real_cancel_numeral_factors;
-
-
-(*examples:
-print_depth 22;
-set timing;
-set trace_simp;
-fun test s = (Goal s; by (Simp_tac 1));
-
-test "#0 <= (y::real) * #-2";
-test "#9*x = #12 * (y::real)";
-test "(#9*x) / (#12 * (y::real)) = z";
-test "#9*x < #12 * (y::real)";
-test "#9*x <= #12 * (y::real)";
-
-test "#-99*x = #132 * (y::real)";
-test "(#-99*x) / (#132 * (y::real)) = z";
-test "#-99*x < #132 * (y::real)";
-test "#-99*x <= #132 * (y::real)";
-
-test "#999*x = #-396 * (y::real)";
-test "(#999*x) / (#-396 * (y::real)) = z";
-test "#999*x < #-396 * (y::real)";
-test "#999*x <= #-396 * (y::real)";
-
-test "#-99*x = #-81 * (y::real)";
-test "(#-99*x) / (#-81 * (y::real)) = z";
-test "#-99*x <= #-81 * (y::real)";
-test "#-99*x < #-81 * (y::real)";
-
-test "#-2 * x = #-1 * (y::real)";
-test "#-2 * x = -(y::real)";
-test "(#-2 * x) / (#-1 * (y::real)) = z";
-test "#-2 * x < -(y::real)";
-test "#-2 * x <= #-1 * (y::real)";
-test "-x < #-23 * (y::real)";
-test "-x <= #-23 * (y::real)";
-*)
-
-
-(** Declarations for ExtractCommonTerm **)
-
-local
- open Real_Numeral_Simprocs
-in
-
-structure CancelFactorCommon =
- struct
- val mk_sum = long_mk_prod
- val dest_sum = dest_prod
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff
- val find_first = find_first []
- val trans_tac = trans_tac
- val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@real_mult_ac))
- end;
-
-structure EqCancelFactor = ExtractCommonTermFun
- (open CancelFactorCommon
- val prove_conv = prove_conv "real_eq_cancel_factor"
- val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
- val simplify_meta_eq = cancel_simplify_meta_eq real_mult_eq_cancel1
-);
-
-
-structure DivideCancelFactor = ExtractCommonTermFun
- (open CancelFactorCommon
- val prove_conv = prove_conv "real_divide_cancel_factor"
- val mk_bal = HOLogic.mk_binop "HOL.divide"
- val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
- val simplify_meta_eq = cancel_simplify_meta_eq real_mult_div_cancel_disj
-);
-
-val real_cancel_factor =
- map prep_simproc
- [("real_eq_cancel_factor",
- prep_pats ["(l::real) * m = n", "(l::real) = m * n"],
- EqCancelFactor.proc),
- ("real_divide_cancel_factor",
- prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)"],
- DivideCancelFactor.proc)];
-
-end;
-
-Addsimprocs real_cancel_factor;
-
-
-(*examples:
-print_depth 22;
-set timing;
-set trace_simp;
-fun test s = (Goal s; by (Asm_simp_tac 1));
-
-test "x*k = k*(y::real)";
-test "k = k*(y::real)";
-test "a*(b*c) = (b::real)";
-test "a*(b*c) = d*(b::real)*(x*a)";
-
-
-test "(x*k) / (k*(y::real)) = (uu::real)";
-test "(k) / (k*(y::real)) = (uu::real)";
-test "(a*(b*c)) / ((b::real)) = (uu::real)";
-test "(a*(b*c)) / (d*(b::real)*(x*a)) = (uu::real)";
-
-(*FIXME: what do we do about this?*)
-test "a*(b*c)/(y*z) = d*(b::real)*(x*a)/z";
-*)
-
-
-(*** Simplification of inequalities involving literal divisors ***)
-
-Goal "#0<z ==> ((x::real) <= y/z) = (x*z <= y)";
-by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
-qed "pos_real_le_divide_eq";
-Addsimps [inst "z" "number_of ?w" pos_real_le_divide_eq];
-
-Goal "z<#0 ==> ((x::real) <= y/z) = (y <= x*z)";
-by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
-qed "neg_real_le_divide_eq";
-Addsimps [inst "z" "number_of ?w" neg_real_le_divide_eq];
-
-Goal "#0<z ==> (y/z <= (x::real)) = (y <= x*z)";
-by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
-qed "pos_real_divide_le_eq";
-Addsimps [inst "z" "number_of ?w" pos_real_divide_le_eq];
-
-Goal "z<#0 ==> (y/z <= (x::real)) = (x*z <= y)";
-by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
-qed "neg_real_divide_le_eq";
-Addsimps [inst "z" "number_of ?w" neg_real_divide_le_eq];
-
-Goal "#0<z ==> ((x::real) < y/z) = (x*z < y)";
-by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
-qed "pos_real_less_divide_eq";
-Addsimps [inst "z" "number_of ?w" pos_real_less_divide_eq];
-
-Goal "z<#0 ==> ((x::real) < y/z) = (y < x*z)";
-by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
-qed "neg_real_less_divide_eq";
-Addsimps [inst "z" "number_of ?w" neg_real_less_divide_eq];
-
-Goal "#0<z ==> (y/z < (x::real)) = (y < x*z)";
-by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
-qed "pos_real_divide_less_eq";
-Addsimps [inst "z" "number_of ?w" pos_real_divide_less_eq];
-
-Goal "z<#0 ==> (y/z < (x::real)) = (x*z < y)";
-by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
-qed "neg_real_divide_less_eq";
-Addsimps [inst "z" "number_of ?w" neg_real_divide_less_eq];
-
-Goal "z~=#0 ==> ((x::real) = y/z) = (x*z = y)";
-by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_eq_cancel2 1);
-by (Asm_simp_tac 1);
-qed "real_eq_divide_eq";
-Addsimps [inst "z" "number_of ?w" real_eq_divide_eq];
-
-Goal "z~=#0 ==> (y/z = (x::real)) = (y = x*z)";
-by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_eq_cancel2 1);
-by (Asm_simp_tac 1);
-qed "real_divide_eq_eq";
-Addsimps [inst "z" "number_of ?w" real_divide_eq_eq];
-
-Goal "(m/k = n/k) = (k = #0 | m = (n::real))";
-by (case_tac "k=#0" 1);
-by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO]) 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_eq_eq, real_eq_divide_eq,
- real_mult_eq_cancel2]) 1);
-qed "real_divide_eq_cancel2";
-
-Goal "(k/m = k/n) = (k = #0 | m = (n::real))";
-by (case_tac "m=#0 | n = #0" 1);
-by (auto_tac (claset(),
- simpset() addsimps [REAL_DIVIDE_ZERO, real_divide_eq_eq,
- real_eq_divide_eq, real_mult_eq_cancel1]));
-qed "real_divide_eq_cancel1";
-
-(*Moved from RealOrd.ML to use #0 *)
-Goal "[| #0 < r; #0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)";
-by (auto_tac (claset() addIs [real_inverse_less_swap], simpset()));
-by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1);
-by (res_inst_tac [("t","x")] (real_inverse_inverse RS subst) 1);
-by (auto_tac (claset() addIs [real_inverse_less_swap],
- simpset() delsimps [real_inverse_inverse]
- addsimps [real_inverse_gt_zero]));
-qed "real_inverse_less_iff";
-
-Goal "[| #0 < r; #0 < x|] ==> (inverse x <= inverse r) = (r <= (x::real))";
-by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
- real_inverse_less_iff]) 1);
-qed "real_inverse_le_iff";
-
-(** Division by 1, -1 **)
-
-Goal "(x::real)/#1 = x";
-by (simp_tac (simpset() addsimps [real_divide_def]) 1);
-qed "real_divide_1";
-Addsimps [real_divide_1];
-
-Goal "x/#-1 = -(x::real)";
-by (Simp_tac 1);
-qed "real_divide_minus1";
-Addsimps [real_divide_minus1];
-
-Goal "#-1/(x::real) = - (#1/x)";
-by (simp_tac (simpset() addsimps [real_divide_def, real_minus_inverse]) 1);
-qed "real_minus1_divide";
-Addsimps [real_minus1_divide];
-
-Goal "[| (#0::real) < d1; #0 < d2 |] ==> EX e. #0 < e & e < d1 & e < d2";
-by (res_inst_tac [("x","(min d1 d2)/#2")] exI 1);
-by (asm_simp_tac (simpset() addsimps [min_def]) 1);
-qed "real_lbound_gt_zero";
-
-
-(*** General rewrites to improve automation, like those for type "int" ***)
-
-(** The next several equations can make the simplifier loop! **)
-
-Goal "(x < - y) = (y < - (x::real))";
-by Auto_tac;
-qed "real_less_minus";
-
-Goal "(- x < y) = (- y < (x::real))";
-by Auto_tac;
-qed "real_minus_less";
-
-Goal "(x <= - y) = (y <= - (x::real))";
-by Auto_tac;
-qed "real_le_minus";
-
-Goal "(- x <= y) = (- y <= (x::real))";
-by Auto_tac;
-qed "real_minus_le";
-
-Goal "(x = - y) = (y = - (x::real))";
-by Auto_tac;
-qed "real_equation_minus";
-
-Goal "(- x = y) = (- (y::real) = x)";
-by Auto_tac;
-qed "real_minus_equation";
-
-
-Goal "(x + - a = (#0::real)) = (x=a)";
-by (arith_tac 1);
-qed "real_add_minus_iff";
-Addsimps [real_add_minus_iff];
-
-Goal "(-b = -a) = (b = (a::real))";
-by (arith_tac 1);
-qed "real_minus_eq_cancel";
-Addsimps [real_minus_eq_cancel];
-
-
-(*Distributive laws for literals*)
-Addsimps (map (inst "w" "number_of ?v")
- [real_add_mult_distrib, real_add_mult_distrib2,
- real_diff_mult_distrib, real_diff_mult_distrib2]);
-
-Addsimps (map (inst "x" "number_of ?v")
- [real_less_minus, real_le_minus, real_equation_minus]);
-Addsimps (map (inst "y" "number_of ?v")
- [real_minus_less, real_minus_le, real_minus_equation]);
-
-
-(*** Simprules combining x+y and #0 ***)
-
-Goal "(x+y = (#0::real)) = (y = -x)";
-by Auto_tac;
-qed "real_add_eq_0_iff";
-AddIffs [real_add_eq_0_iff];
-
-Goal "(x+y < (#0::real)) = (y < -x)";
-by Auto_tac;
-qed "real_add_less_0_iff";
-AddIffs [real_add_less_0_iff];
-
-Goal "((#0::real) < x+y) = (-x < y)";
-by Auto_tac;
-qed "real_0_less_add_iff";
-AddIffs [real_0_less_add_iff];
-
-Goal "(x+y <= (#0::real)) = (y <= -x)";
-by Auto_tac;
-qed "real_add_le_0_iff";
-AddIffs [real_add_le_0_iff];
-
-Goal "((#0::real) <= x+y) = (-x <= y)";
-by Auto_tac;
-qed "real_0_le_add_iff";
-AddIffs [real_0_le_add_iff];
-
-
-(** Simprules combining x-y and #0; see also real_less_iff_diff_less_0, etc.,
- in RealBin
-**)
-
-Goal "((#0::real) < x-y) = (y < x)";
-by Auto_tac;
-qed "real_0_less_diff_iff";
-AddIffs [real_0_less_diff_iff];
-
-Goal "((#0::real) <= x-y) = (y <= x)";
-by Auto_tac;
-qed "real_0_le_diff_iff";
-AddIffs [real_0_le_diff_iff];
-
-(*
-?? still needed ??
-Addsimps [symmetric real_diff_def];
-*)
-
-Goal "-(x-y) = y - (x::real)";
-by (arith_tac 1);
-qed "real_minus_diff_eq";
-Addsimps [real_minus_diff_eq];
-
-
-(*** Density of the Reals ***)
-
-Goal "x < y ==> x < (x+y) / (#2::real)";
-by Auto_tac;
-qed "real_less_half_sum";
-
-Goal "x < y ==> (x+y)/(#2::real) < y";
-by Auto_tac;
-qed "real_gt_half_sum";
-
-Goal "x < y ==> EX r::real. x < r & r < y";
-by (blast_tac (claset() addSIs [real_less_half_sum, real_gt_half_sum]) 1);
-qed "real_dense";
-
-
-(*Replaces "inverse #nn" by #1/#nn *)
-Addsimps [inst "x" "number_of ?w" real_inverse_eq_divide];
-
-
--- a/src/HOL/Real/RealArith.thy Thu Dec 21 18:53:32 2000 +0100
+++ b/src/HOL/Real/RealArith.thy Thu Dec 21 18:57:12 2000 +0100
@@ -1,4 +1,4 @@
-theory RealArith = RealBin
+theory RealArith = RealArith0
files "real_arith.ML":
setup real_arith_setup
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/RealArith0.ML Thu Dec 21 18:57:12 2000 +0100
@@ -0,0 +1,655 @@
+(* Title: HOL/Real/RealArith.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1999 University of Cambridge
+
+Assorted facts that need binary literals and the arithmetic decision procedure
+
+Also, common factor cancellation
+*)
+
+(** Division and inverse **)
+
+Goal "#0/x = (#0::real)";
+by (simp_tac (simpset() addsimps [real_divide_def]) 1);
+qed "real_0_divide";
+Addsimps [real_0_divide];
+
+Goal "((#0::real) < inverse x) = (#0 < x)";
+by (case_tac "x=#0" 1);
+by (asm_simp_tac (HOL_ss addsimps [rename_numerals INVERSE_ZERO]) 1);
+by (auto_tac (claset() addDs [rename_numerals real_inverse_less_zero],
+ simpset() addsimps [linorder_neq_iff,
+ rename_numerals real_inverse_gt_zero]));
+qed "real_0_less_inverse_iff";
+AddIffs [real_0_less_inverse_iff];
+
+Goal "(inverse x < (#0::real)) = (x < #0)";
+by (case_tac "x=#0" 1);
+by (asm_simp_tac (HOL_ss addsimps [rename_numerals INVERSE_ZERO]) 1);
+by (auto_tac (claset() addDs [rename_numerals real_inverse_less_zero],
+ simpset() addsimps [linorder_neq_iff,
+ rename_numerals real_inverse_gt_zero]));
+qed "real_inverse_less_0_iff";
+AddIffs [real_inverse_less_0_iff];
+
+Goal "((#0::real) <= inverse x) = (#0 <= x)";
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+qed "real_0_le_inverse_iff";
+AddIffs [real_0_le_inverse_iff];
+
+Goal "(inverse x <= (#0::real)) = (x <= #0)";
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+qed "real_inverse_le_0_iff";
+AddIffs [real_inverse_le_0_iff];
+
+Goalw [real_divide_def] "x/(#0::real) = #0";
+by (stac (rename_numerals INVERSE_ZERO) 1);
+by (Simp_tac 1);
+qed "REAL_DIVIDE_ZERO";
+
+(*generalize?*)
+Goal "((#0::real) < #1/x) = (#0 < x)";
+by (simp_tac (simpset() addsimps [real_divide_def]) 1);
+qed "real_0_less_recip_iff";
+AddIffs [real_0_less_recip_iff];
+
+Goal "(#1/x < (#0::real)) = (x < #0)";
+by (simp_tac (simpset() addsimps [real_divide_def]) 1);
+qed "real_recip_less_0_iff";
+AddIffs [real_recip_less_0_iff];
+
+Goal "inverse (x::real) = #1/x";
+by (simp_tac (simpset() addsimps [real_divide_def]) 1);
+qed "real_inverse_eq_divide";
+
+Goal "((#0::real) < x/y) = (#0 < x & #0 < y | x < #0 & y < #0)";
+by (simp_tac (simpset() addsimps [real_divide_def, real_0_less_mult_iff]) 1);
+qed "real_0_less_divide_iff";
+Addsimps [inst "x" "number_of ?w" real_0_less_divide_iff];
+
+Goal "(x/y < (#0::real)) = (#0 < x & y < #0 | x < #0 & #0 < y)";
+by (simp_tac (simpset() addsimps [real_divide_def, real_mult_less_0_iff]) 1);
+qed "real_divide_less_0_iff";
+Addsimps [inst "x" "number_of ?w" real_divide_less_0_iff];
+
+Goal "((#0::real) <= x/y) = ((x <= #0 | #0 <= y) & (#0 <= x | y <= #0))";
+by (simp_tac (simpset() addsimps [real_divide_def, real_0_le_mult_iff]) 1);
+by Auto_tac;
+qed "real_0_le_divide_iff";
+Addsimps [inst "x" "number_of ?w" real_0_le_divide_iff];
+
+Goal "(x/y <= (#0::real)) = ((x <= #0 | y <= #0) & (#0 <= x | #0 <= y))";
+by (simp_tac (simpset() addsimps [real_divide_def, real_mult_le_0_iff]) 1);
+by Auto_tac;
+qed "real_divide_le_0_iff";
+Addsimps [inst "x" "number_of ?w" real_divide_le_0_iff];
+
+Goal "(inverse(x::real) = #0) = (x = #0)";
+by (auto_tac (claset(), simpset() addsimps [rename_numerals INVERSE_ZERO]));
+by (rtac ccontr 1);
+by (blast_tac (claset() addDs [rename_numerals real_inverse_not_zero]) 1);
+qed "real_inverse_zero_iff";
+AddIffs [real_inverse_zero_iff];
+
+Goal "(x/y = #0) = (x=#0 | y=(#0::real))";
+by (auto_tac (claset(), simpset() addsimps [real_divide_def]));
+qed "real_divide_eq_0_iff";
+AddIffs [real_divide_eq_0_iff];
+
+
+(**** Factor cancellation theorems for "real" ****)
+
+(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
+ but not (yet?) for k*m < n*k. **)
+
+bind_thm ("real_mult_minus_right", real_minus_mult_eq2 RS sym);
+
+Goal "(-y < -x) = ((x::real) < y)";
+by (arith_tac 1);
+qed "real_minus_less_minus";
+Addsimps [real_minus_less_minus];
+
+Goal "[| i<j; k < (0::real) |] ==> j*k < i*k";
+by (rtac (real_minus_less_minus RS iffD1) 1);
+by (auto_tac (claset(),
+ simpset() delsimps [real_minus_mult_eq2 RS sym]
+ addsimps [real_minus_mult_eq2]));
+qed "real_mult_less_mono1_neg";
+
+Goal "[| i<j; k < (0::real) |] ==> k*j < k*i";
+by (rtac (real_minus_less_minus RS iffD1) 1);
+by (auto_tac (claset(),
+ simpset() delsimps [real_minus_mult_eq1 RS sym]
+ addsimps [real_minus_mult_eq1]));;
+qed "real_mult_less_mono2_neg";
+
+Goal "[| i <= j; (0::real) <= k |] ==> i*k <= j*k";
+by (auto_tac (claset(),
+ simpset() addsimps [order_le_less, real_mult_less_mono1]));
+qed "real_mult_le_mono1";
+
+Goal "[| i <= j; k <= (0::real) |] ==> j*k <= i*k";
+by (auto_tac (claset(),
+ simpset() addsimps [order_le_less, real_mult_less_mono1_neg]));
+qed "real_mult_le_mono1_neg";
+
+Goal "[| i <= j; (0::real) <= k |] ==> k*i <= k*j";
+by (dtac real_mult_le_mono1 1);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [real_mult_commute])));
+qed "real_mult_le_mono2";
+
+Goal "[| i <= j; k <= (0::real) |] ==> k*j <= k*i";
+by (dtac real_mult_le_mono1_neg 1);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [real_mult_commute])));
+qed "real_mult_le_mono2_neg";
+
+Goal "(m*k < n*k) = (((#0::real) < k & m<n) | (k < #0 & n<m))";
+by (case_tac "k = (0::real)" 1);
+by (auto_tac (claset(),
+ simpset() addsimps [linorder_neq_iff,
+ real_mult_less_mono1, real_mult_less_mono1_neg]));
+by (auto_tac (claset(),
+ simpset() addsimps [linorder_not_less,
+ inst "y1" "m*k" (linorder_not_le RS sym),
+ inst "y1" "m" (linorder_not_le RS sym)]));
+by (TRYALL (etac notE));
+by (auto_tac (claset(),
+ simpset() addsimps [order_less_imp_le, real_mult_le_mono1,
+ real_mult_le_mono1_neg]));
+qed "real_mult_less_cancel2";
+
+Goal "(m*k <= n*k) = (((#0::real) < k --> m<=n) & (k < #0 --> n<=m))";
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
+ real_mult_less_cancel2]) 1);
+qed "real_mult_le_cancel2";
+
+Goal "(k*m < k*n) = (((#0::real) < k & m<n) | (k < #0 & n<m))";
+by (simp_tac (simpset() addsimps [inst "z" "k" real_mult_commute,
+ real_mult_less_cancel2]) 1);
+qed "real_mult_less_cancel1";
+
+Goal "!!k::real. (k*m <= k*n) = ((#0 < k --> m<=n) & (k < #0 --> n<=m))";
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
+ real_mult_less_cancel1]) 1);
+qed "real_mult_le_cancel1";
+
+Goal "!!k::real. (k*m = k*n) = (k = #0 | m=n)";
+by (case_tac "k=0" 1);
+by (auto_tac (claset(), simpset() addsimps [real_mult_left_cancel]));
+qed "real_mult_eq_cancel1";
+
+Goal "!!k::real. (m*k = n*k) = (k = #0 | m=n)";
+by (case_tac "k=0" 1);
+by (auto_tac (claset(), simpset() addsimps [real_mult_right_cancel]));
+qed "real_mult_eq_cancel2";
+
+Goal "!!k::real. k~=#0 ==> (k*m) / (k*n) = (m/n)";
+by (asm_simp_tac
+ (simpset() addsimps [real_divide_def, real_inverse_distrib]) 1);
+by (subgoal_tac "k * m * (inverse k * inverse n) = \
+\ (k * inverse k) * (m * inverse n)" 1);
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (asm_full_simp_tac (HOL_ss addsimps real_mult_ac) 1);
+qed "real_mult_div_cancel1";
+
+(*For ExtractCommonTerm*)
+Goal "(k*m) / (k*n) = (if k = (#0::real) then #0 else m/n)";
+by (simp_tac (simpset() addsimps [real_mult_div_cancel1]) 1);
+qed "real_mult_div_cancel_disj";
+
+
+local
+ open Real_Numeral_Simprocs
+in
+
+val rel_real_number_of = [eq_real_number_of, less_real_number_of,
+ le_real_number_of_eq_not_less];
+
+structure CancelNumeralFactorCommon =
+ struct
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val trans_tac = trans_tac
+ val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_plus_1s))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
+ THEN ALLGOALS
+ (simp_tac
+ (HOL_ss addsimps [eq_real_number_of, mult_real_number_of,
+ real_mult_number_of_left]@
+ real_minus_from_mult_simps @ real_mult_ac))
+ val numeral_simp_tac =
+ ALLGOALS (simp_tac (HOL_ss addsimps rel_real_number_of@bin_simps))
+ val simplify_meta_eq = simplify_meta_eq
+ end
+
+structure DivCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+ val prove_conv = prove_conv "realdiv_cancel_numeral_factor"
+ val mk_bal = HOLogic.mk_binop "HOL.divide"
+ val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
+ val cancel = real_mult_div_cancel1 RS trans
+ val neg_exchanges = false
+)
+
+structure EqCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+ val prove_conv = prove_conv "realeq_cancel_numeral_factor"
+ val mk_bal = HOLogic.mk_eq
+ val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
+ val cancel = real_mult_eq_cancel1 RS trans
+ val neg_exchanges = false
+)
+
+structure LessCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+ val prove_conv = prove_conv "realless_cancel_numeral_factor"
+ val mk_bal = HOLogic.mk_binrel "op <"
+ val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT
+ val cancel = real_mult_less_cancel1 RS trans
+ val neg_exchanges = true
+)
+
+structure LeCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+ val prove_conv = prove_conv "realle_cancel_numeral_factor"
+ val mk_bal = HOLogic.mk_binrel "op <="
+ val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT
+ val cancel = real_mult_le_cancel1 RS trans
+ val neg_exchanges = true
+)
+
+val real_cancel_numeral_factors =
+ map prep_simproc
+ [("realeq_cancel_numeral_factor",
+ prep_pats ["(l::real) * m = n", "(l::real) = m * n"],
+ EqCancelNumeralFactor.proc),
+ ("realless_cancel_numeral_factor",
+ prep_pats ["(l::real) * m < n", "(l::real) < m * n"],
+ LessCancelNumeralFactor.proc),
+ ("realle_cancel_numeral_factor",
+ prep_pats ["(l::real) * m <= n", "(l::real) <= m * n"],
+ LeCancelNumeralFactor.proc),
+ ("realdiv_cancel_numeral_factor",
+ prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)"],
+ DivCancelNumeralFactor.proc)];
+
+end;
+
+Addsimprocs real_cancel_numeral_factors;
+
+
+(*examples:
+print_depth 22;
+set timing;
+set trace_simp;
+fun test s = (Goal s; by (Simp_tac 1));
+
+test "#0 <= (y::real) * #-2";
+test "#9*x = #12 * (y::real)";
+test "(#9*x) / (#12 * (y::real)) = z";
+test "#9*x < #12 * (y::real)";
+test "#9*x <= #12 * (y::real)";
+
+test "#-99*x = #132 * (y::real)";
+test "(#-99*x) / (#132 * (y::real)) = z";
+test "#-99*x < #132 * (y::real)";
+test "#-99*x <= #132 * (y::real)";
+
+test "#999*x = #-396 * (y::real)";
+test "(#999*x) / (#-396 * (y::real)) = z";
+test "#999*x < #-396 * (y::real)";
+test "#999*x <= #-396 * (y::real)";
+
+test "#-99*x = #-81 * (y::real)";
+test "(#-99*x) / (#-81 * (y::real)) = z";
+test "#-99*x <= #-81 * (y::real)";
+test "#-99*x < #-81 * (y::real)";
+
+test "#-2 * x = #-1 * (y::real)";
+test "#-2 * x = -(y::real)";
+test "(#-2 * x) / (#-1 * (y::real)) = z";
+test "#-2 * x < -(y::real)";
+test "#-2 * x <= #-1 * (y::real)";
+test "-x < #-23 * (y::real)";
+test "-x <= #-23 * (y::real)";
+*)
+
+
+(** Declarations for ExtractCommonTerm **)
+
+local
+ open Real_Numeral_Simprocs
+in
+
+structure CancelFactorCommon =
+ struct
+ val mk_sum = long_mk_prod
+ val dest_sum = dest_prod
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff
+ val find_first = find_first []
+ val trans_tac = trans_tac
+ val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@real_mult_ac))
+ end;
+
+structure EqCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+ val prove_conv = prove_conv "real_eq_cancel_factor"
+ val mk_bal = HOLogic.mk_eq
+ val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
+ val simplify_meta_eq = cancel_simplify_meta_eq real_mult_eq_cancel1
+);
+
+
+structure DivideCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+ val prove_conv = prove_conv "real_divide_cancel_factor"
+ val mk_bal = HOLogic.mk_binop "HOL.divide"
+ val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
+ val simplify_meta_eq = cancel_simplify_meta_eq real_mult_div_cancel_disj
+);
+
+val real_cancel_factor =
+ map prep_simproc
+ [("real_eq_cancel_factor",
+ prep_pats ["(l::real) * m = n", "(l::real) = m * n"],
+ EqCancelFactor.proc),
+ ("real_divide_cancel_factor",
+ prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)"],
+ DivideCancelFactor.proc)];
+
+end;
+
+Addsimprocs real_cancel_factor;
+
+
+(*examples:
+print_depth 22;
+set timing;
+set trace_simp;
+fun test s = (Goal s; by (Asm_simp_tac 1));
+
+test "x*k = k*(y::real)";
+test "k = k*(y::real)";
+test "a*(b*c) = (b::real)";
+test "a*(b*c) = d*(b::real)*(x*a)";
+
+
+test "(x*k) / (k*(y::real)) = (uu::real)";
+test "(k) / (k*(y::real)) = (uu::real)";
+test "(a*(b*c)) / ((b::real)) = (uu::real)";
+test "(a*(b*c)) / (d*(b::real)*(x*a)) = (uu::real)";
+
+(*FIXME: what do we do about this?*)
+test "a*(b*c)/(y*z) = d*(b::real)*(x*a)/z";
+*)
+
+
+(*** Simplification of inequalities involving literal divisors ***)
+
+Goal "#0<z ==> ((x::real) <= y/z) = (x*z <= y)";
+by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (etac ssubst 1);
+by (stac real_mult_le_cancel2 1);
+by (Asm_simp_tac 1);
+qed "pos_real_le_divide_eq";
+Addsimps [inst "z" "number_of ?w" pos_real_le_divide_eq];
+
+Goal "z<#0 ==> ((x::real) <= y/z) = (y <= x*z)";
+by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (etac ssubst 1);
+by (stac real_mult_le_cancel2 1);
+by (Asm_simp_tac 1);
+qed "neg_real_le_divide_eq";
+Addsimps [inst "z" "number_of ?w" neg_real_le_divide_eq];
+
+Goal "#0<z ==> (y/z <= (x::real)) = (y <= x*z)";
+by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (etac ssubst 1);
+by (stac real_mult_le_cancel2 1);
+by (Asm_simp_tac 1);
+qed "pos_real_divide_le_eq";
+Addsimps [inst "z" "number_of ?w" pos_real_divide_le_eq];
+
+Goal "z<#0 ==> (y/z <= (x::real)) = (x*z <= y)";
+by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (etac ssubst 1);
+by (stac real_mult_le_cancel2 1);
+by (Asm_simp_tac 1);
+qed "neg_real_divide_le_eq";
+Addsimps [inst "z" "number_of ?w" neg_real_divide_le_eq];
+
+Goal "#0<z ==> ((x::real) < y/z) = (x*z < y)";
+by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (etac ssubst 1);
+by (stac real_mult_less_cancel2 1);
+by (Asm_simp_tac 1);
+qed "pos_real_less_divide_eq";
+Addsimps [inst "z" "number_of ?w" pos_real_less_divide_eq];
+
+Goal "z<#0 ==> ((x::real) < y/z) = (y < x*z)";
+by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (etac ssubst 1);
+by (stac real_mult_less_cancel2 1);
+by (Asm_simp_tac 1);
+qed "neg_real_less_divide_eq";
+Addsimps [inst "z" "number_of ?w" neg_real_less_divide_eq];
+
+Goal "#0<z ==> (y/z < (x::real)) = (y < x*z)";
+by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (etac ssubst 1);
+by (stac real_mult_less_cancel2 1);
+by (Asm_simp_tac 1);
+qed "pos_real_divide_less_eq";
+Addsimps [inst "z" "number_of ?w" pos_real_divide_less_eq];
+
+Goal "z<#0 ==> (y/z < (x::real)) = (x*z < y)";
+by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (etac ssubst 1);
+by (stac real_mult_less_cancel2 1);
+by (Asm_simp_tac 1);
+qed "neg_real_divide_less_eq";
+Addsimps [inst "z" "number_of ?w" neg_real_divide_less_eq];
+
+Goal "z~=#0 ==> ((x::real) = y/z) = (x*z = y)";
+by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (etac ssubst 1);
+by (stac real_mult_eq_cancel2 1);
+by (Asm_simp_tac 1);
+qed "real_eq_divide_eq";
+Addsimps [inst "z" "number_of ?w" real_eq_divide_eq];
+
+Goal "z~=#0 ==> (y/z = (x::real)) = (y = x*z)";
+by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (etac ssubst 1);
+by (stac real_mult_eq_cancel2 1);
+by (Asm_simp_tac 1);
+qed "real_divide_eq_eq";
+Addsimps [inst "z" "number_of ?w" real_divide_eq_eq];
+
+Goal "(m/k = n/k) = (k = #0 | m = (n::real))";
+by (case_tac "k=#0" 1);
+by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO]) 1);
+by (asm_simp_tac (simpset() addsimps [real_divide_eq_eq, real_eq_divide_eq,
+ real_mult_eq_cancel2]) 1);
+qed "real_divide_eq_cancel2";
+
+Goal "(k/m = k/n) = (k = #0 | m = (n::real))";
+by (case_tac "m=#0 | n = #0" 1);
+by (auto_tac (claset(),
+ simpset() addsimps [REAL_DIVIDE_ZERO, real_divide_eq_eq,
+ real_eq_divide_eq, real_mult_eq_cancel1]));
+qed "real_divide_eq_cancel1";
+
+(*Moved from RealOrd.ML to use #0 *)
+Goal "[| #0 < r; #0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)";
+by (auto_tac (claset() addIs [real_inverse_less_swap], simpset()));
+by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1);
+by (res_inst_tac [("t","x")] (real_inverse_inverse RS subst) 1);
+by (auto_tac (claset() addIs [real_inverse_less_swap],
+ simpset() delsimps [real_inverse_inverse]
+ addsimps [real_inverse_gt_zero]));
+qed "real_inverse_less_iff";
+
+Goal "[| #0 < r; #0 < x|] ==> (inverse x <= inverse r) = (r <= (x::real))";
+by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
+ real_inverse_less_iff]) 1);
+qed "real_inverse_le_iff";
+
+(** Division by 1, -1 **)
+
+Goal "(x::real)/#1 = x";
+by (simp_tac (simpset() addsimps [real_divide_def]) 1);
+qed "real_divide_1";
+Addsimps [real_divide_1];
+
+Goal "x/#-1 = -(x::real)";
+by (Simp_tac 1);
+qed "real_divide_minus1";
+Addsimps [real_divide_minus1];
+
+Goal "#-1/(x::real) = - (#1/x)";
+by (simp_tac (simpset() addsimps [real_divide_def, real_minus_inverse]) 1);
+qed "real_minus1_divide";
+Addsimps [real_minus1_divide];
+
+Goal "[| (#0::real) < d1; #0 < d2 |] ==> EX e. #0 < e & e < d1 & e < d2";
+by (res_inst_tac [("x","(min d1 d2)/#2")] exI 1);
+by (asm_simp_tac (simpset() addsimps [min_def]) 1);
+qed "real_lbound_gt_zero";
+
+
+(*** General rewrites to improve automation, like those for type "int" ***)
+
+(** The next several equations can make the simplifier loop! **)
+
+Goal "(x < - y) = (y < - (x::real))";
+by Auto_tac;
+qed "real_less_minus";
+
+Goal "(- x < y) = (- y < (x::real))";
+by Auto_tac;
+qed "real_minus_less";
+
+Goal "(x <= - y) = (y <= - (x::real))";
+by Auto_tac;
+qed "real_le_minus";
+
+Goal "(- x <= y) = (- y <= (x::real))";
+by Auto_tac;
+qed "real_minus_le";
+
+Goal "(x = - y) = (y = - (x::real))";
+by Auto_tac;
+qed "real_equation_minus";
+
+Goal "(- x = y) = (- (y::real) = x)";
+by Auto_tac;
+qed "real_minus_equation";
+
+
+Goal "(x + - a = (#0::real)) = (x=a)";
+by (arith_tac 1);
+qed "real_add_minus_iff";
+Addsimps [real_add_minus_iff];
+
+Goal "(-b = -a) = (b = (a::real))";
+by (arith_tac 1);
+qed "real_minus_eq_cancel";
+Addsimps [real_minus_eq_cancel];
+
+
+(*Distributive laws for literals*)
+Addsimps (map (inst "w" "number_of ?v")
+ [real_add_mult_distrib, real_add_mult_distrib2,
+ real_diff_mult_distrib, real_diff_mult_distrib2]);
+
+Addsimps (map (inst "x" "number_of ?v")
+ [real_less_minus, real_le_minus, real_equation_minus]);
+Addsimps (map (inst "y" "number_of ?v")
+ [real_minus_less, real_minus_le, real_minus_equation]);
+
+
+(*** Simprules combining x+y and #0 ***)
+
+Goal "(x+y = (#0::real)) = (y = -x)";
+by Auto_tac;
+qed "real_add_eq_0_iff";
+AddIffs [real_add_eq_0_iff];
+
+Goal "(x+y < (#0::real)) = (y < -x)";
+by Auto_tac;
+qed "real_add_less_0_iff";
+AddIffs [real_add_less_0_iff];
+
+Goal "((#0::real) < x+y) = (-x < y)";
+by Auto_tac;
+qed "real_0_less_add_iff";
+AddIffs [real_0_less_add_iff];
+
+Goal "(x+y <= (#0::real)) = (y <= -x)";
+by Auto_tac;
+qed "real_add_le_0_iff";
+AddIffs [real_add_le_0_iff];
+
+Goal "((#0::real) <= x+y) = (-x <= y)";
+by Auto_tac;
+qed "real_0_le_add_iff";
+AddIffs [real_0_le_add_iff];
+
+
+(** Simprules combining x-y and #0; see also real_less_iff_diff_less_0, etc.,
+ in RealBin
+**)
+
+Goal "((#0::real) < x-y) = (y < x)";
+by Auto_tac;
+qed "real_0_less_diff_iff";
+AddIffs [real_0_less_diff_iff];
+
+Goal "((#0::real) <= x-y) = (y <= x)";
+by Auto_tac;
+qed "real_0_le_diff_iff";
+AddIffs [real_0_le_diff_iff];
+
+(*
+?? still needed ??
+Addsimps [symmetric real_diff_def];
+*)
+
+Goal "-(x-y) = y - (x::real)";
+by (arith_tac 1);
+qed "real_minus_diff_eq";
+Addsimps [real_minus_diff_eq];
+
+
+(*** Density of the Reals ***)
+
+Goal "x < y ==> x < (x+y) / (#2::real)";
+by Auto_tac;
+qed "real_less_half_sum";
+
+Goal "x < y ==> (x+y)/(#2::real) < y";
+by Auto_tac;
+qed "real_gt_half_sum";
+
+Goal "x < y ==> EX r::real. x < r & r < y";
+by (blast_tac (claset() addSIs [real_less_half_sum, real_gt_half_sum]) 1);
+qed "real_dense";
+
+
+(*Replaces "inverse #nn" by #1/#nn *)
+Addsimps [inst "x" "number_of ?w" real_inverse_eq_divide];
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/RealArith0.thy Thu Dec 21 18:57:12 2000 +0100
@@ -0,0 +1,6 @@
+theory RealArith0 = RealBin
+files "real_arith0.ML":
+
+setup real_arith_setup
+
+end
--- a/src/HOL/Real/real_arith.ML Thu Dec 21 18:53:32 2000 +0100
+++ b/src/HOL/Real/real_arith.ML Thu Dec 21 18:57:12 2000 +0100
@@ -3,49 +3,16 @@
Author: Tobias Nipkow, TU Muenchen
Copyright 1999 TU Muenchen
-Instantiation of the generic linear arithmetic package for type real.
+Augmentation of real linear arithmetic with rational coefficient handling
*)
local
(* reduce contradictory <= to False *)
-val simps = [order_less_irrefl, zero_eq_numeral_0, one_eq_numeral_1,
- add_real_number_of, minus_real_number_of, diff_real_number_of,
- mult_real_number_of, eq_real_number_of, less_real_number_of,
- le_real_number_of_eq_not_less, real_diff_def,
- real_minus_add_distrib, real_minus_minus];
-
-val add_rules =
- map rename_numerals
- [real_add_zero_left, real_add_zero_right,
- real_add_minus, real_add_minus_left,
- real_mult_0, real_mult_0_right,
- real_mult_1, real_mult_1_right,
- real_mult_minus_1, real_mult_minus_1_right];
-
-val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@
- Real_Numeral_Simprocs.cancel_numerals(* @ real_cancel_numeral_factors*);
+val simps = [True_implies_equals,inst "w" "number_of ?v" real_add_mult_distrib2,
+ real_divide_1,real_times_divide1_eq,real_times_divide2_eq];
-val mono_ss = simpset() addsimps
- [real_add_le_mono,real_add_less_mono,
- real_add_less_le_mono,real_add_le_less_mono];
-
-val add_mono_thms_real =
- map (fn s => prove_goal (the_context ()) s
- (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1]))
- ["(i <= j) & (k <= l) ==> i + k <= j + (l::real)",
- "(i = j) & (k <= l) ==> i + k <= j + (l::real)",
- "(i <= j) & (k = l) ==> i + k <= j + (l::real)",
- "(i = j) & (k = l) ==> i + k = j + (l::real)",
- "(i < j) & (k = l) ==> i + k < j + (l::real)",
- "(i = j) & (k < l) ==> i + k < j + (l::real)",
- "(i < j) & (k <= l) ==> i + k < j + (l::real)",
- "(i <= j) & (k < l) ==> i + k < j + (l::real)",
- "(i < j) & (k < l) ==> i + k < j + (l::real)"];
-
-val real_arith_simproc_pats =
- map (fn s => Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.boolT))
- ["(m::real) < n","(m::real) <= n", "(m::real) = n"];
+val simprocs = [hd(rev real_cancel_numeral_factors)];
fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
@@ -57,63 +24,16 @@
in
-val fast_real_arith_simproc = mk_simproc
- "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover;
-
val real_arith_setup =
[Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
- {add_mono_thms = add_mono_thms @ add_mono_thms_real,
+ {add_mono_thms = add_mono_thms,
mult_mono_thms = mult_mono_thms @ real_mult_mono_thms,
- inj_thms = inj_thms, (*FIXME: add real*)
- lessD = lessD, (*We don't change LA_Data_Ref.lessD because the real ordering is dense!*)
- simpset = simpset addsimps (True_implies_equals :: add_rules @ simps)
- addsimprocs simprocs
- addcongs [if_weak_cong]}),
- arith_discrete ("RealDef.real",false),
- Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]];
+ inj_thms = inj_thms,
+ lessD = lessD,
+ simpset = simpset addsimps simps addsimprocs simprocs})];
end;
-
-(* Some test data [omitting examples that assume the ordering to be discrete!]
-Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
-by (fast_arith_tac 1);
-qed "";
-
-Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
-by (fast_arith_tac 1);
-qed "";
-
-Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j";
-by (fast_arith_tac 1);
-qed "";
-
-Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
-by (arith_tac 1);
-qed "";
-
-Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\ ==> a <= l";
-by (fast_arith_tac 1);
-qed "";
-
-Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\ ==> a+a+a+a <= l+l+l+l";
-by (fast_arith_tac 1);
-qed "";
-
-Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\ ==> a+a+a+a+a <= l+l+l+l+i";
-by (fast_arith_tac 1);
-qed "";
-
-Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\ ==> a+a+a+a+a+a <= l+l+l+l+i+l";
-by (fast_arith_tac 1);
-qed "";
-
-Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\ ==> #6*a <= #5*l+i";
-by (fast_arith_tac 1);
-qed "";
+(*
+Procedure "assoc_fold" needed?
*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/real_arith0.ML Thu Dec 21 18:57:12 2000 +0100
@@ -0,0 +1,118 @@
+(* Title: HOL/Real/real_arith.ML
+ ID: $Id$
+ Author: Tobias Nipkow, TU Muenchen
+ Copyright 1999 TU Muenchen
+
+Instantiation of the generic linear arithmetic package for type real.
+*)
+
+local
+
+(* reduce contradictory <= to False *)
+val simps = [order_less_irrefl, zero_eq_numeral_0, one_eq_numeral_1,
+ add_real_number_of, minus_real_number_of, diff_real_number_of,
+ mult_real_number_of, eq_real_number_of, less_real_number_of,
+ le_real_number_of_eq_not_less, real_diff_def,
+ real_minus_add_distrib, real_minus_minus, real_mult_assoc];
+
+val add_rules =
+ map rename_numerals
+ [real_add_zero_left, real_add_zero_right,
+ real_add_minus, real_add_minus_left,
+ real_mult_0, real_mult_0_right,
+ real_mult_1, real_mult_1_right,
+ real_mult_minus_1, real_mult_minus_1_right];
+
+val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@
+ Real_Numeral_Simprocs.cancel_numerals(* @ real_cancel_numeral_factors*);
+
+val mono_ss = simpset() addsimps
+ [real_add_le_mono,real_add_less_mono,
+ real_add_less_le_mono,real_add_le_less_mono];
+
+val add_mono_thms_real =
+ map (fn s => prove_goal (the_context ()) s
+ (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1]))
+ ["(i <= j) & (k <= l) ==> i + k <= j + (l::real)",
+ "(i = j) & (k <= l) ==> i + k <= j + (l::real)",
+ "(i <= j) & (k = l) ==> i + k <= j + (l::real)",
+ "(i = j) & (k = l) ==> i + k = j + (l::real)",
+ "(i < j) & (k = l) ==> i + k < j + (l::real)",
+ "(i = j) & (k < l) ==> i + k < j + (l::real)",
+ "(i < j) & (k <= l) ==> i + k < j + (l::real)",
+ "(i <= j) & (k < l) ==> i + k < j + (l::real)",
+ "(i < j) & (k < l) ==> i + k < j + (l::real)"];
+
+val real_arith_simproc_pats =
+ map (fn s => Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.boolT))
+ ["(m::real) < n","(m::real) <= n", "(m::real) = n"];
+
+fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
+
+val real_mult_mono_thms =
+ [(rotate_prems 1 real_mult_less_mono2,
+ cvar(real_mult_less_mono2, hd(prems_of real_mult_less_mono2))),
+ (real_mult_le_mono2,
+ cvar(real_mult_le_mono2, hd(tl(prems_of real_mult_le_mono2))))]
+
+in
+
+val fast_real_arith_simproc = mk_simproc
+ "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover;
+
+val real_arith_setup =
+ [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
+ {add_mono_thms = add_mono_thms @ add_mono_thms_real,
+ mult_mono_thms = mult_mono_thms @ real_mult_mono_thms,
+ inj_thms = inj_thms, (*FIXME: add real*)
+ lessD = lessD, (*We don't change LA_Data_Ref.lessD because the real ordering is dense!*)
+ simpset = simpset addsimps (add_rules @ simps)
+ addsimprocs simprocs}),
+ arith_discrete ("RealDef.real",false),
+ Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]];
+
+end;
+
+
+(* Some test data [omitting examples that assume the ordering to be discrete!]
+Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
+by (fast_arith_tac 1);
+qed "";
+
+Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
+by (fast_arith_tac 1);
+qed "";
+
+Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j";
+by (fast_arith_tac 1);
+qed "";
+
+Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
+by (arith_tac 1);
+qed "";
+
+Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\ ==> a <= l";
+by (fast_arith_tac 1);
+qed "";
+
+Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\ ==> a+a+a+a <= l+l+l+l";
+by (fast_arith_tac 1);
+qed "";
+
+Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\ ==> a+a+a+a+a <= l+l+l+l+i";
+by (fast_arith_tac 1);
+qed "";
+
+Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\ ==> a+a+a+a+a+a <= l+l+l+l+i+l";
+by (fast_arith_tac 1);
+qed "";
+
+Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\ ==> #6*a <= #5*l+i";
+by (fast_arith_tac 1);
+qed "";
+*)