# HG changeset patch # User paulson # Date 1073922335 -3600 # Node ID a8b1a44d82642dc7e5755253a68c86cf53bb6fb8 # Parent cd3ef10d02be19cf5f45e60e11cda636fe7f4380 Modified real arithmetic simplification diff -r cd3ef10d02be -r a8b1a44d8264 src/HOL/Hyperreal/HyperArith.thy --- a/src/HOL/Hyperreal/HyperArith.thy Mon Jan 12 14:35:07 2004 +0100 +++ b/src/HOL/Hyperreal/HyperArith.thy Mon Jan 12 16:45:35 2004 +0100 @@ -1,5 +1,4 @@ - -theory HyperArith = HyperArith0 +theory HyperArith = HyperBin files "hypreal_arith.ML": setup hypreal_arith_setup diff -r cd3ef10d02be -r a8b1a44d8264 src/HOL/Hyperreal/HyperArith0.thy --- a/src/HOL/Hyperreal/HyperArith0.thy Mon Jan 12 14:35:07 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -theory HyperArith0 = HyperBin -files "hypreal_arith0.ML": - -setup hypreal_arith_setup - -end diff -r cd3ef10d02be -r a8b1a44d8264 src/HOL/Hyperreal/HyperBin.ML --- a/src/HOL/Hyperreal/HyperBin.ML Mon Jan 12 14:35:07 2004 +0100 +++ b/src/HOL/Hyperreal/HyperBin.ML Mon Jan 12 16:45:35 2004 +0100 @@ -344,7 +344,7 @@ val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq [hypreal_add_zero_left, hypreal_add_zero_right, - mult_left_zero, mult_right_zero, mult_1, mult_1_right]; + mult_zero_left, mult_zero_right, mult_1, mult_1_right]; val prep_simproc = Real_Numeral_Simprocs.prep_simproc; diff -r cd3ef10d02be -r a8b1a44d8264 src/HOL/Hyperreal/Transcendental.ML --- a/src/HOL/Hyperreal/Transcendental.ML Mon Jan 12 14:35:07 2004 +0100 +++ b/src/HOL/Hyperreal/Transcendental.ML Mon Jan 12 16:45:35 2004 +0100 @@ -12,8 +12,6 @@ res_inst_tac [("z",x)] cancel_thm i end; -val mult_less_cancel_left = thm"mult_less_cancel_left"; - Goalw [root_def] "root (Suc n) 0 = 0"; by (safe_tac (claset() addSIs [some_equality,power_0_Suc] addSEs [realpow_zero_zero])); @@ -125,16 +123,8 @@ simpset() delsimps [realpow_Suc])); qed "real_pow_sqrt_eq_sqrt_pow"; -Goal "0 <= x ==> sqrt(x) ^ 2 = sqrt(abs(x ^ 2))"; -by (asm_full_simp_tac (simpset() addsimps [real_pow_sqrt_eq_sqrt_pow]) 1); -by (stac numeral_2_eq_2 1); -by (asm_full_simp_tac (simpset()delsimps [realpow_Suc]) 1); -qed "real_pow_sqrt_eq_sqrt_abs_pow"; - Goal "0 <= x ==> sqrt(x) ^ 2 = sqrt(abs(x) ^ 2)"; -by (asm_full_simp_tac (simpset() addsimps [real_pow_sqrt_eq_sqrt_abs_pow]) 1); -by (stac numeral_2_eq_2 1); -by (asm_full_simp_tac (simpset()delsimps [realpow_Suc]) 1); +by (asm_full_simp_tac (simpset() addsimps [real_pow_sqrt_eq_sqrt_pow]) 1); qed "real_pow_sqrt_eq_sqrt_abs_pow2"; Goal "0 <= x ==> sqrt(x) ^ 2 = abs(x)"; @@ -613,7 +603,7 @@ \ ==> f -- 0 --> 0"; by (Auto_tac); by (subgoal_tac "0 <= K" 1); -by (dres_inst_tac [("x","k*inverse 2")] spec 2); +by (dres_inst_tac [("x","k/2")] spec 2); by (ftac real_less_half_sum 2); by (dtac real_gt_half_sum 2); by (auto_tac (claset(),simpset() addsimps [abs_eqI2])); @@ -1620,11 +1610,8 @@ qed "sin_gt_zero1"; Goal "[| 0 < x; x < 2 |] ==> cos (2 * x) < 1"; -by (auto_tac (claset(), - simpset() addsimps [cos_squared_eq, - minus_add_distrib RS sym, neg_less_0_iff_less,sin_gt_zero1, - real_add_order,zero_less_power,cos_double] - delsimps [realpow_Suc,minus_add_distrib])); +by (cut_inst_tac [("x","x")] sin_gt_zero1 1); +by (auto_tac (claset(), simpset() addsimps [cos_squared_eq, cos_double])); qed "cos_double_less_one"; Goal "(%n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) \ @@ -1736,7 +1723,7 @@ by (multr_by_tac "inverse 2" 1); by (Simp_tac 1); by (cut_facts_tac [pi_half_gt_zero] 1); -by (full_simp_tac (HOL_ss addsimps [thm"mult_left_zero", real_divide_def]) 1); +by (full_simp_tac (HOL_ss addsimps [mult_zero_left, real_divide_def]) 1); qed "pi_gt_zero"; Addsimps [pi_gt_zero]; Addsimps [(pi_gt_zero RS real_not_refl2) RS not_sym]; @@ -2066,11 +2053,11 @@ "[| cos x ~= 0; cos y ~= 0 |] \ \ ==> 1 - tan(x)*tan(y) = cos (x + y)/(cos x * cos y)"; by (auto_tac (claset(), - simpset() delsimps [thm"Ring_and_Field.inverse_mult_distrib"] + simpset() delsimps [inverse_mult_distrib] addsimps [inverse_mult_distrib RS sym] @ mult_ac)); by (res_inst_tac [("c1","cos x * cos y")] (real_mult_right_cancel RS subst) 1); by (auto_tac (claset(), - simpset() delsimps [thm"Ring_and_Field.inverse_mult_distrib"] + simpset() delsimps [inverse_mult_distrib] addsimps [mult_assoc, left_diff_distrib,cos_add])); val lemma_tan_add1 = result(); Addsimps [lemma_tan_add1]; @@ -2123,7 +2110,7 @@ Goalw [real_divide_def] "(%x. cos(x)/sin(x)) -- pi/2 --> 0"; -by (res_inst_tac [("a1","1")] ((mult_left_zero) RS subst) 1); +by (res_inst_tac [("a1","1")] ((mult_zero_left) RS subst) 1); by (rtac LIM_mult2 1); by (rtac (inverse_1 RS subst) 2); by (rtac LIM_inverse 2); @@ -2837,7 +2824,7 @@ \ |] ==> sin xa ^ 2 = (y / sqrt (x * x + y * y)) ^ 2"; by (auto_tac (claset() addIs [lemma_divide_rearrange],simpset() addsimps [realpow_divide,real_sqrt_gt_zero_pow2, - real_power_two RS sym])); + power2_eq_square RS sym])); qed "lemma_cos_sin_eq"; Goal "[| 0 < x * x + y * y; \ @@ -2845,7 +2832,7 @@ \ |] ==> cos xa ^ 2 = (x / sqrt (x * x + y * y)) ^ 2"; by (auto_tac (claset(), simpset() addsimps [realpow_divide, - real_sqrt_gt_zero_pow2,real_power_two RS sym])); + real_sqrt_gt_zero_pow2,power2_eq_square RS sym])); by (rtac (real_add_commute RS subst) 1); by (rtac lemma_divide_rearrange 1); by (asm_full_simp_tac (simpset() addsimps []) 1); @@ -2867,19 +2854,16 @@ delsimps [realpow_Suc])); qed "sin_x_y_disj"; +(*FIXME: remove real_sqrt_gt_zero_pow2*) +Goal "0 <= x ==> sqrt(x) ^ 2 = x"; +by (asm_full_simp_tac (simpset() addsimps [real_sqrt_pow_abs,abs_if]) 1); +qed "real_sqrt_ge_zero_pow2"; + Goal "y ~= 0 ==> x / sqrt (x * x + y * y) ~= -(1::real)"; by Auto_tac; -by (dres_inst_tac [("f","%x. x ^ 2")] arg_cong 1); -by (auto_tac (claset(),simpset() addsimps [realpow_divide, - real_power_two RS sym])); -by (forw_inst_tac [("x","x")] real_sum_squares_not_zero2 1); -by (asm_full_simp_tac (HOL_ss addsimps [real_power_two RS sym]) 1); -by (forw_inst_tac [("c1","x ^ 2 + y ^ 2")] - (real_mult_right_cancel RS iffD2) 1); -by (assume_tac 1); -by (dres_inst_tac [("y","x ^ 2 + y ^ 2"),("x","x ^ 2")] - (CLAIM "y ~= (0::real) ==> (x/y) * y= x") 1); -by Auto_tac; +by (dres_inst_tac [("f","%x. x ^ 2")] arg_cong 1); +by (asm_full_simp_tac (simpset() addsimps [power_divide,thm"real_mult_self_sum_ge_zero",real_sqrt_ge_zero_pow2]) 1); +by (asm_full_simp_tac (simpset() addsimps [inst "a" "1" divide_eq_eq, power2_eq_square] addsplits [split_if_asm]) 1); qed "cos_not_eq_minus_one"; Goalw [arcos_def] @@ -2894,7 +2878,7 @@ Goalw [real_divide_def] "x ~= 0 ==> x / sqrt (x * x + y * y) ~= 0"; by (forw_inst_tac [("y3","y")] (real_sqrt_sum_squares_gt_zero3 RS real_not_refl2 RS not_sym RS nonzero_imp_inverse_nonzero) 1); -by (auto_tac (claset(),simpset() addsimps [real_power_two])); +by (auto_tac (claset(),simpset() addsimps [power2_eq_square])); qed "lemma_cos_not_eq_zero"; Goal "[| x ~= 0; \ @@ -2918,7 +2902,7 @@ by (auto_tac (claset(),simpset() addsimps [abs_eqI2])); by (dres_inst_tac [("y","y")] real_sqrt_sum_squares_gt_zero3 1); by (auto_tac (claset(),simpset() addsimps [zero_less_mult_iff, - real_divide_def,real_power_two])); + real_divide_def,power2_eq_square])); qed "real_sqrt_divide_less_zero"; Goal "[| x ~= 0; 0 < y |] ==> EX r a. x = r * cos a & y = r * sin a"; @@ -2927,7 +2911,7 @@ by Auto_tac; by (dres_inst_tac [("y2","y")] (real_sqrt_sum_squares_gt_zero3 RS real_not_refl2 RS not_sym) 1); -by (auto_tac (claset(),simpset() addsimps [real_power_two])); +by (auto_tac (claset(),simpset() addsimps [power2_eq_square])); by (rewtac arcos_def); by (cut_inst_tac [("x1","x"),("y1","y")] ([cos_x_y_ge_minus_one,cos_x_y_le_one] MRS cos_total) 1); @@ -2937,7 +2921,7 @@ by (ftac sin_x_y_disj 1 THEN Blast_tac 1); by (dres_inst_tac [("y2","y")] (real_sqrt_sum_squares_gt_zero3 RS real_not_refl2 RS not_sym) 1); -by (auto_tac (claset(),simpset() addsimps [real_power_two])); +by (auto_tac (claset(),simpset() addsimps [power2_eq_square])); by (dtac sin_ge_zero 1 THEN assume_tac 1); by (dres_inst_tac [("x","x")] real_sqrt_divide_less_zero 1 THEN Auto_tac); qed "polar_ex1"; @@ -2952,7 +2936,7 @@ by (res_inst_tac [("x","sqrt(x ^ 2 + y ^ 2)")] exI 1); by (res_inst_tac [("x","arcsin(y / sqrt (x * x + y * y))")] exI 1); by (auto_tac (claset() addDs [real_sum_squares_cancel2a], - simpset() addsimps [real_power_two])); + simpset() addsimps [power2_eq_square])); by (rewtac arcsin_def); by (cut_inst_tac [("x1","x"),("y1","y")] ([cos_x_y_ge_minus_one1a, cos_x_y_le_one2] MRS sin_total) 1); @@ -2987,7 +2971,6 @@ Goal "abs x <= sqrt (x ^ 2 + y ^ 2)"; by (res_inst_tac [("n","1")] realpow_increasing 1); by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2 RS sym])); -by (simp_tac (simpset() addsimps [numeral_2_eq_2]) 1); qed "real_sqrt_ge_abs1"; Goal "abs y <= sqrt (x ^ 2 + y ^ 2)"; diff -r cd3ef10d02be -r a8b1a44d8264 src/HOL/Hyperreal/hypreal_arith.ML --- a/src/HOL/Hyperreal/hypreal_arith.ML Mon Jan 12 14:35:07 2004 +0100 +++ b/src/HOL/Hyperreal/hypreal_arith.ML Mon Jan 12 16:45:35 2004 +0100 @@ -3,9 +3,12 @@ Author: Tobias Nipkow, TU Muenchen Copyright 1999 TU Muenchen -Simprocs: Common factor cancellation & Rational coefficient handling +Simprocs for common factor cancellation & Rational coefficient handling + +Instantiation of the generic linear arithmetic package for type hypreal. *) + (****Common factor cancellation****) local @@ -197,38 +200,126 @@ *) -(****Augmentation of real linear arithmetic with - rational coefficient handling****) +(****Instantiation of the generic linear arithmetic package****) + +val hypreal_mult_left_mono = + read_instantiate_sg(sign_of HyperBin.thy) [("a","?a::hypreal")] + mult_left_mono; + local (* reduce contradictory <= to False *) +val add_rules = + [order_less_irrefl, hypreal_numeral_0_eq_0, hypreal_numeral_1_eq_1, + add_hypreal_number_of, minus_hypreal_number_of, diff_hypreal_number_of, + mult_hypreal_number_of, eq_hypreal_number_of, less_hypreal_number_of, + le_hypreal_number_of_eq_not_less, hypreal_diff_def, + minus_add_distrib, minus_minus, mult_assoc, minus_zero, + hypreal_add_zero_left, hypreal_add_zero_right, + hypreal_add_minus, hypreal_add_minus_left, + mult_zero_left, mult_zero_right, + mult_1, mult_1_right, + hypreal_mult_minus_1, hypreal_mult_minus_1_right]; + +val mono_ss = simpset() addsimps + [add_mono, add_strict_mono, + hypreal_add_less_le_mono,hypreal_add_le_less_mono]; + +val add_mono_thms_hypreal = + 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::hypreal)", + "(i = j) & (k <= l) ==> i + k <= j + (l::hypreal)", + "(i <= j) & (k = l) ==> i + k <= j + (l::hypreal)", + "(i = j) & (k = l) ==> i + k = j + (l::hypreal)", + "(i < j) & (k = l) ==> i + k < j + (l::hypreal)", + "(i = j) & (k < l) ==> i + k < j + (l::hypreal)", + "(i < j) & (k <= l) ==> i + k < j + (l::hypreal)", + "(i <= j) & (k < l) ==> i + k < j + (l::hypreal)", + "(i < j) & (k < l) ==> i + k < j + (l::hypreal)"]; + +val simprocs = [Hyperreal_Times_Assoc.conv, + Hyperreal_Numeral_Simprocs.combine_numerals, + hypreal_cancel_numeral_factors_divide]@ + Hyperreal_Numeral_Simprocs.cancel_numerals @ + Hyperreal_Numeral_Simprocs.eval_numerals; + +(* reduce contradictory <= to False *) val simps = [True_implies_equals, inst "a" "(number_of ?v)::hypreal" right_distrib, divide_1,times_divide_eq_right,times_divide_eq_left]; -val simprocs = [hypreal_cancel_numeral_factors_divide]; - fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; val hypreal_mult_mono_thms = [(rotate_prems 1 hypreal_mult_less_mono2, cvar(hypreal_mult_less_mono2, hd(prems_of hypreal_mult_less_mono2))), - (mult_left_mono, - cvar(mult_left_mono, hd(tl(prems_of mult_left_mono))))] + (hypreal_mult_left_mono, + cvar(hypreal_mult_left_mono, hd(tl(prems_of hypreal_mult_left_mono))))] in +val fast_hypreal_arith_simproc = + Simplifier.simproc (Theory.sign_of (the_context ())) + "fast_hypreal_arith" + ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"] + Fast_Arith.lin_arith_prover; + val hypreal_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 = add_mono_thms @ add_mono_thms_hypreal, mult_mono_thms = mult_mono_thms @ hypreal_mult_mono_thms, - inj_thms = inj_thms, - lessD = lessD, - simpset = simpset addsimps simps addsimprocs simprocs})]; + inj_thms = inj_thms, (*FIXME: add hypreal*) + lessD = lessD, (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*) + simpset = simpset addsimps add_rules + addsimps simps + addsimprocs simprocs}), + arith_discrete ("HyperDef.hypreal",false), + Simplifier.change_simpset_of (op addsimprocs) [fast_hypreal_arith_simproc]]; end; -(* -Procedure "assoc_fold" needed? + +(* Some test data [omitting examples that assume the ordering to be discrete!] +Goal "!!a::hypreal. [| a <= b; c <= d; x+y a+c <= b+d"; +by (fast_arith_tac 1); +qed ""; + +Goal "!!a::hypreal. [| a <= b; b+b <= c |] ==> a+a <= c"; +by (fast_arith_tac 1); +qed ""; + +Goal "!!a::hypreal. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"; +by (fast_arith_tac 1); +qed ""; + +Goal "!!a::hypreal. 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::hypreal. [| 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::hypreal. [| 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::hypreal. [| 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::hypreal. [| 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::hypreal. [| 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 ""; *) diff -r cd3ef10d02be -r a8b1a44d8264 src/HOL/Hyperreal/hypreal_arith0.ML --- a/src/HOL/Hyperreal/hypreal_arith0.ML Mon Jan 12 14:35:07 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,115 +0,0 @@ -(* Title: HOL/Hyperreal/hypreal_arith.ML - ID: $Id$ - Author: Tobias Nipkow, TU Muenchen - Copyright 1999 TU Muenchen - -Instantiation of the generic linear arithmetic package for type hypreal. -*) - -local - -(* reduce contradictory <= to False *) -val add_rules = - [order_less_irrefl, hypreal_numeral_0_eq_0, hypreal_numeral_1_eq_1, - add_hypreal_number_of, minus_hypreal_number_of, diff_hypreal_number_of, - mult_hypreal_number_of, eq_hypreal_number_of, less_hypreal_number_of, - le_hypreal_number_of_eq_not_less, hypreal_diff_def, - minus_add_distrib, minus_minus, mult_assoc, minus_zero, - hypreal_add_zero_left, hypreal_add_zero_right, - hypreal_add_minus, hypreal_add_minus_left, - mult_left_zero, mult_right_zero, - mult_1, mult_1_right, - hypreal_mult_minus_1, hypreal_mult_minus_1_right]; - -val simprocs = [Hyperreal_Times_Assoc.conv, - Hyperreal_Numeral_Simprocs.combine_numerals]@ - Hyperreal_Numeral_Simprocs.cancel_numerals @ - Hyperreal_Numeral_Simprocs.eval_numerals; - -val mono_ss = simpset() addsimps - [add_mono, add_strict_mono, - hypreal_add_less_le_mono,hypreal_add_le_less_mono]; - -val add_mono_thms_hypreal = - 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::hypreal)", - "(i = j) & (k <= l) ==> i + k <= j + (l::hypreal)", - "(i <= j) & (k = l) ==> i + k <= j + (l::hypreal)", - "(i = j) & (k = l) ==> i + k = j + (l::hypreal)", - "(i < j) & (k = l) ==> i + k < j + (l::hypreal)", - "(i = j) & (k < l) ==> i + k < j + (l::hypreal)", - "(i < j) & (k <= l) ==> i + k < j + (l::hypreal)", - "(i <= j) & (k < l) ==> i + k < j + (l::hypreal)", - "(i < j) & (k < l) ==> i + k < j + (l::hypreal)"]; - -fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; - -val hypreal_mult_mono_thms = - [(rotate_prems 1 hypreal_mult_less_mono2, - cvar(hypreal_mult_less_mono2, hd(prems_of hypreal_mult_less_mono2))), - (mult_left_mono, - cvar(mult_left_mono, hd(tl(prems_of mult_left_mono))))] - -in - -val fast_hypreal_arith_simproc = - Simplifier.simproc (Theory.sign_of (the_context ())) - "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"] - Fast_Arith.lin_arith_prover; - -val hypreal_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_hypreal, - mult_mono_thms = mult_mono_thms @ hypreal_mult_mono_thms, - inj_thms = inj_thms, (*FIXME: add hypreal*) - lessD = lessD, (*We don't change LA_Data_Ref.lessD because the hypreal ordering is dense!*) - simpset = simpset addsimps add_rules addsimprocs simprocs}), - arith_discrete ("HyperDef.hypreal",false), - Simplifier.change_simpset_of (op addsimprocs) [fast_hypreal_arith_simproc]]; - -end; - - -(* Some test data [omitting examples that assume the ordering to be discrete!] -Goal "!!a::hypreal. [| a <= b; c <= d; x+y a+c <= b+d"; -by (fast_arith_tac 1); -qed ""; - -Goal "!!a::hypreal. [| a <= b; b+b <= c |] ==> a+a <= c"; -by (fast_arith_tac 1); -qed ""; - -Goal "!!a::hypreal. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"; -by (fast_arith_tac 1); -qed ""; - -Goal "!!a::hypreal. 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::hypreal. [| 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::hypreal. [| 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::hypreal. [| 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::hypreal. [| 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::hypreal. [| 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 ""; -*) diff -r cd3ef10d02be -r a8b1a44d8264 src/HOL/Real/Complex_Numbers.thy --- a/src/HOL/Real/Complex_Numbers.thy Mon Jan 12 14:35:07 2004 +0100 +++ b/src/HOL/Real/Complex_Numbers.thy Mon Jan 12 16:45:35 2004 +0100 @@ -126,9 +126,9 @@ thus ?thesis by rule (insert ge, arith+) qed with neq show "Re (inverse w * w) = Re 1" - by (simp add: inverse_complex_def real_power_two add_divide_distrib [symmetric]) + by (simp add: inverse_complex_def power2_eq_square add_divide_distrib [symmetric]) from neq show "Im (inverse w * w) = Im 1" - by (simp add: inverse_complex_def real_power_two + by (simp add: inverse_complex_def power2_eq_square mult_ac add_divide_distrib [symmetric]) qed qed @@ -164,7 +164,7 @@ by (simp add: conjg_def) lemma Re_conjg_self: "Re (z * conjg z) = (Re z)\ + (Im z)\" - by (simp add: real_power_two) + by (simp add: power2_eq_square) lemma Im_conjg_self: "Im (z * conjg z) = 0" by simp diff -r cd3ef10d02be -r a8b1a44d8264 src/HOL/Real/RealArith.thy --- a/src/HOL/Real/RealArith.thy Mon Jan 12 14:35:07 2004 +0100 +++ b/src/HOL/Real/RealArith.thy Mon Jan 12 16:45:35 2004 +0100 @@ -1,4 +1,4 @@ -theory RealArith = RealArith0 +theory RealArith = RealBin files ("real_arith.ML"): use "real_arith.ML" @@ -149,8 +149,6 @@ val real_dense = thm"real_dense"; val abs_nat_number_of = thm"abs_nat_number_of"; -val abs_split = thm"abs_split"; -val abs_zero = thm"abs_zero"; val abs_eqI1 = thm"abs_eqI1"; val abs_eqI2 = thm"abs_eqI2"; val abs_minus_eqI2 = thm"abs_minus_eqI2"; diff -r cd3ef10d02be -r a8b1a44d8264 src/HOL/Real/RealArith0.thy --- a/src/HOL/Real/RealArith0.thy Mon Jan 12 14:35:07 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -theory RealArith0 = RealBin -files "real_arith0.ML": - -setup real_arith_setup - -end diff -r cd3ef10d02be -r a8b1a44d8264 src/HOL/Real/RealBin.ML --- a/src/HOL/Real/RealBin.ML Mon Jan 12 14:35:07 2004 +0100 +++ b/src/HOL/Real/RealBin.ML Mon Jan 12 16:45:35 2004 +0100 @@ -361,7 +361,7 @@ val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq [add_0, add_0_right, - mult_left_zero, mult_right_zero, mult_1, mult_1_right]; + mult_zero_left, mult_zero_right, mult_1, mult_1_right]; fun prep_simproc (name, pats, proc) = Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc; diff -r cd3ef10d02be -r a8b1a44d8264 src/HOL/Real/RealPow.thy --- a/src/HOL/Real/RealPow.thy Mon Jan 12 14:35:07 2004 +0100 +++ b/src/HOL/Real/RealPow.thy Mon Jan 12 16:45:35 2004 +0100 @@ -148,10 +148,6 @@ declare power_real_number_of [of _ "number_of w", standard, simp] -lemma real_power_two: "(r::real)\ = r * r" - by (simp add: numeral_2_eq_2) - - subsection{*Various Other Theorems*} text{*Used several times in Hyperreal/Transcendental.ML*} @@ -213,17 +209,17 @@ lemma realpow_two_sum_zero_iff [simp]: "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)" apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 - simp add: real_power_two) + simp add: power2_eq_square) done lemma realpow_two_le_add_order [simp]: "(0::real) \ u ^ 2 + v ^ 2" apply (rule real_le_add_order) -apply (auto simp add: real_power_two) +apply (auto simp add: power2_eq_square) done lemma realpow_two_le_add_order2 [simp]: "(0::real) \ u ^ 2 + v ^ 2 + w ^ 2" apply (rule real_le_add_order)+ -apply (auto simp add: real_power_two) +apply (auto simp add: power2_eq_square) done lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y" @@ -241,7 +237,7 @@ by (rule_tac j = 0 in real_le_trans, auto) lemma realpow_square_minus_le [simp]: "-(u ^ 2) \ (x::real) ^ 2" -by (auto simp add: real_power_two) +by (auto simp add: power2_eq_square) lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))" by (case_tac "n", auto) @@ -259,7 +255,7 @@ done lemma zero_le_x_squared [simp]: "(0::real) \ x^2" -by (simp add: real_power_two) +by (simp add: power2_eq_square) @@ -294,7 +290,6 @@ val zero_le_realpow_abs = thm "zero_le_realpow_abs"; val real_of_int_power = thm "real_of_int_power"; val power_real_number_of = thm "power_real_number_of"; -val real_power_two = thm "real_power_two"; val real_sum_squares_cancel_a = thm "real_sum_squares_cancel_a"; val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2"; val real_squared_diff_one_factored = thm "real_squared_diff_one_factored"; diff -r cd3ef10d02be -r a8b1a44d8264 src/HOL/Real/real_arith.ML --- a/src/HOL/Real/real_arith.ML Mon Jan 12 14:35:07 2004 +0100 +++ b/src/HOL/Real/real_arith.ML Mon Jan 12 16:45:35 2004 +0100 @@ -1,9 +1,11 @@ -(* Title: HOL/Real/real_arith.ML +(* Title: HOL/Real/real_arith0.ML ID: $Id$ Author: Tobias Nipkow, TU Muenchen - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1999 TU Muenchen -Simprocs: Common factor cancellation & Rational coefficient handling +Simprocs for common factor cancellation & Rational coefficient handling + +Instantiation of the generic linear arithmetic package for type real. *) @@ -207,17 +209,52 @@ test "a*(b*c)/(y*z) = d*(b::real)*(x*a)/z"; *) -(****Augmentation of real linear arithmetic with - rational coefficient handling****) + + +(****Instantiation of the generic linear arithmetic package****) + +val add_zero_left = thm"Ring_and_Field.add_0"; +val add_zero_right = thm"Ring_and_Field.add_0_right"; + +val real_mult_left_mono = + read_instantiate_sg(sign_of RealBin.thy) [("a","?a::real")] mult_left_mono; + local (* reduce contradictory <= to False *) -val simps = [True_implies_equals, - inst "a" "(number_of ?v)::real" right_distrib, - divide_1,times_divide_eq_right,times_divide_eq_left]; +val add_rules = + [order_less_irrefl, real_numeral_0_eq_0, real_numeral_1_eq_1, + real_minus_1_eq_m1, + 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, + minus_add_distrib, minus_minus, mult_assoc, minus_zero, + add_zero_left, add_zero_right, left_minus, right_minus, + mult_zero_left, mult_zero_right, mult_1, mult_1_right, + minus_mult_left RS sym, minus_mult_right RS sym]; + +val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals, + real_cancel_numeral_factors_divide]@ + Real_Numeral_Simprocs.cancel_numerals @ + Real_Numeral_Simprocs.eval_numerals; -val simprocs = [real_cancel_numeral_factors_divide]; +val mono_ss = simpset() addsimps + [add_mono,add_strict_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)"]; fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; @@ -227,18 +264,93 @@ (real_mult_left_mono, cvar(real_mult_left_mono, hd(tl(prems_of real_mult_left_mono))))] +(* reduce contradictory <= to False *) +val simps = [True_implies_equals, + inst "a" "(number_of ?v)::real" right_distrib, + divide_1,times_divide_eq_right,times_divide_eq_left]; + in +val fast_real_arith_simproc = Simplifier.simproc (Theory.sign_of (the_context ())) + "fast_real_arith" ["(m::real) < n","(m::real) <= n", "(m::real) = n"] + 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 = add_mono_thms @ add_mono_thms_real, mult_mono_thms = mult_mono_thms @ real_mult_mono_thms, - inj_thms = inj_thms, - lessD = lessD, - simpset = simpset addsimps simps addsimprocs simprocs})]; + inj_thms = inj_thms, (*FIXME: add real*) + lessD = lessD, (*Can't change LA_Data_Ref.lessD: the reals are dense!*) + simpset = simpset addsimps add_rules + addsimps simps + addsimprocs simprocs}), + arith_discrete ("RealDef.real",false), + Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]]; + +(* some thms for injection nat => real: +real_of_nat_zero +?zero_eq_numeral_0 +real_of_nat_add +*) end; -(* -Procedure "assoc_fold" needed? + +(* 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 ""; + +Goal "a<=b ==> a < b+(1::real)"; +by (fast_arith_tac 1); +qed ""; + +Goal "a<=b ==> a-(3::real) < b"; +by (fast_arith_tac 1); +qed ""; + +Goal "a<=b ==> a-(1::real) < b"; +by (fast_arith_tac 1); +qed ""; + *) + + + diff -r cd3ef10d02be -r a8b1a44d8264 src/HOL/Real/real_arith0.ML --- a/src/HOL/Real/real_arith0.ML Mon Jan 12 14:35:07 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,139 +0,0 @@ -(* Title: HOL/Real/real_arith0.ML - ID: $Id$ - Author: Tobias Nipkow, TU Muenchen - Copyright 1999 TU Muenchen - -Instantiation of the generic linear arithmetic package for type real. -*) - -val add_zero_left = thm"Ring_and_Field.add_0"; -val add_zero_right = thm"Ring_and_Field.add_0_right"; - -val real_mult_left_mono = - read_instantiate_sg(sign_of RealBin.thy) [("a","?a::real")] mult_left_mono; - - -local - -(* reduce contradictory <= to False *) -val add_rules = - [order_less_irrefl, real_numeral_0_eq_0, real_numeral_1_eq_1, - real_minus_1_eq_m1, - 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, - minus_add_distrib, minus_minus, mult_assoc, minus_zero, - add_zero_left, add_zero_right, left_minus, right_minus, - mult_left_zero, mult_right_zero, mult_1, mult_1_right, - minus_mult_left RS sym, minus_mult_right RS sym]; - -val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@ - Real_Numeral_Simprocs.cancel_numerals @ - Real_Numeral_Simprocs.eval_numerals; - -val mono_ss = simpset() addsimps - [add_mono,add_strict_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)"]; - -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_left_mono, - cvar(real_mult_left_mono, hd(tl(prems_of real_mult_left_mono))))] - -in - -val fast_real_arith_simproc = Simplifier.simproc (Theory.sign_of (the_context ())) - "fast_real_arith" ["(m::real) < n","(m::real) <= n", "(m::real) = n"] - 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 - addsimprocs simprocs}), - arith_discrete ("RealDef.real",false), - Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]]; - -(* some thms for injection nat => real: -real_of_nat_zero -?zero_eq_numeral_0 -real_of_nat_add -*) - -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 ""; - -Goal "a<=b ==> a < b+(1::real)"; -by (fast_arith_tac 1); -qed ""; - -Goal "a<=b ==> a-(3::real) < b"; -by (fast_arith_tac 1); -qed ""; - -Goal "a<=b ==> a-(1::real) < b"; -by (fast_arith_tac 1); -qed ""; - -*)