--- 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
--- 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
--- 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;
--- 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)";
--- 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<z |] ==> 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 "";
*)
--- 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<z |] ==> 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 "";
-*)
--- 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)\<twosuperior> + (Im z)\<twosuperior>"
- by (simp add: real_power_two)
+ by (simp add: power2_eq_square)
lemma Im_conjg_self: "Im (z * conjg z) = 0"
by simp
--- 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";
--- 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
--- 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;
--- 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)\<twosuperior> = 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) \<le> 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) \<le> 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) \<le> (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) \<le> 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";
--- 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<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 "";
+
+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 "";
+
*)
+
+
+
--- 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<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 "";
-
-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 "";
-
-*)