# HG changeset patch # User nipkow # Date 977421432 -3600 # Node ID 55c8367bab058061123938af555442085e0a6a59 # Parent 12b16641845558de0204ce60046a2f419be5ba76 rational linear arithmetic diff -r 12b166418455 -r 55c8367bab05 src/HOL/Real/RealArith.ML --- 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 < 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 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 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 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 ((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 (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 ((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 (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]; - - diff -r 12b166418455 -r 55c8367bab05 src/HOL/Real/RealArith.thy --- 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 diff -r 12b166418455 -r 55c8367bab05 src/HOL/Real/RealArith0.ML --- /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 < 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 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 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 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 ((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 (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 ((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 (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]; + + diff -r 12b166418455 -r 55c8367bab05 src/HOL/Real/RealArith0.thy --- /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 diff -r 12b166418455 -r 55c8367bab05 src/HOL/Real/real_arith.ML --- 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 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? *) diff -r 12b166418455 -r 55c8367bab05 src/HOL/Real/real_arith0.ML --- /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 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 ""; +*)