--- a/src/HOL/Hyperreal/HyperArith.thy Mon Dec 22 12:50:01 2003 +0100
+++ b/src/HOL/Hyperreal/HyperArith.thy Mon Dec 22 12:50:22 2003 +0100
@@ -1,6 +1,22 @@
+
theory HyperArith = HyperArith0
files "hypreal_arith.ML":
setup hypreal_arith_setup
+subsubsection{*Division By @{term 1} and @{term "-1"}*}
+
+lemma hypreal_divide_minus1 [simp]: "x/-1 = -(x::hypreal)"
+by simp
+
+lemma hypreal_minus1_divide [simp]: "-1/(x::hypreal) = - (1/x)"
+by (simp add: hypreal_divide_def hypreal_minus_inverse)
+
+
+(*
+FIXME: we should have this, as for type int, but many proofs would break.
+It replaces x+-y by x-y.
+Addsimps [symmetric hypreal_diff_def]
+*)
+
end
--- a/src/HOL/Hyperreal/HyperArith0.ML Mon Dec 22 12:50:01 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,311 +0,0 @@
-(* Title: HOL/Hyperreal/HyperRealArith0.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
-*)
-
-local
- open Hyperreal_Numeral_Simprocs
-in
-
-val rel_hypreal_number_of = [eq_hypreal_number_of, less_hypreal_number_of,
- le_hypreal_number_of_eq_not_less];
-
-structure CancelNumeralFactorCommon =
- struct
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
- val trans_tac = Real_Numeral_Simprocs.trans_tac
- val norm_tac =
- ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps @ mult_1s))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_mult_ac))
- val numeral_simp_tac =
- ALLGOALS (simp_tac (HOL_ss addsimps rel_hypreal_number_of@bin_simps))
- val simplify_meta_eq = simplify_meta_eq
- end
-
-structure DivCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "HOL.divide"
- val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT
- val cancel = mult_divide_cancel_left RS trans
- val neg_exchanges = false
-)
-
-structure EqCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" hyprealT
- val cancel = mult_cancel_left RS trans
- val neg_exchanges = false
-)
-
-structure LessCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "op <"
- val dest_bal = HOLogic.dest_bin "op <" hyprealT
- val cancel = mult_less_cancel_left RS trans
- val neg_exchanges = true
-)
-
-structure LeCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "op <="
- val dest_bal = HOLogic.dest_bin "op <=" hyprealT
- val cancel = mult_le_cancel_left RS trans
- val neg_exchanges = true
-)
-
-val hypreal_cancel_numeral_factors_relations =
- map prep_simproc
- [("hyprealeq_cancel_numeral_factor",
- ["(l::hypreal) * m = n", "(l::hypreal) = m * n"],
- EqCancelNumeralFactor.proc),
- ("hyprealless_cancel_numeral_factor",
- ["(l::hypreal) * m < n", "(l::hypreal) < m * n"],
- LessCancelNumeralFactor.proc),
- ("hyprealle_cancel_numeral_factor",
- ["(l::hypreal) * m <= n", "(l::hypreal) <= m * n"],
- LeCancelNumeralFactor.proc)];
-
-val hypreal_cancel_numeral_factors_divide = prep_simproc
- ("hyprealdiv_cancel_numeral_factor",
- ["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)",
- "((number_of v)::hypreal) / (number_of w)"],
- DivCancelNumeralFactor.proc);
-
-val hypreal_cancel_numeral_factors =
- hypreal_cancel_numeral_factors_relations @
- [hypreal_cancel_numeral_factors_divide];
-
-end;
-
-Addsimprocs hypreal_cancel_numeral_factors;
-
-
-(*examples:
-print_depth 22;
-set timing;
-set trace_simp;
-fun test s = (Goal s; by (Simp_tac 1));
-
-test "0 <= (y::hypreal) * -2";
-test "9*x = 12 * (y::hypreal)";
-test "(9*x) / (12 * (y::hypreal)) = z";
-test "9*x < 12 * (y::hypreal)";
-test "9*x <= 12 * (y::hypreal)";
-
-test "-99*x = 123 * (y::hypreal)";
-test "(-99*x) / (123 * (y::hypreal)) = z";
-test "-99*x < 123 * (y::hypreal)";
-test "-99*x <= 123 * (y::hypreal)";
-
-test "999*x = -396 * (y::hypreal)";
-test "(999*x) / (-396 * (y::hypreal)) = z";
-test "999*x < -396 * (y::hypreal)";
-test "999*x <= -396 * (y::hypreal)";
-
-test "-99*x = -81 * (y::hypreal)";
-test "(-99*x) / (-81 * (y::hypreal)) = z";
-test "-99*x <= -81 * (y::hypreal)";
-test "-99*x < -81 * (y::hypreal)";
-
-test "-2 * x = -1 * (y::hypreal)";
-test "-2 * x = -(y::hypreal)";
-test "(-2 * x) / (-1 * (y::hypreal)) = z";
-test "-2 * x < -(y::hypreal)";
-test "-2 * x <= -1 * (y::hypreal)";
-test "-x < -23 * (y::hypreal)";
-test "-x <= -23 * (y::hypreal)";
-*)
-
-
-(** Declarations for ExtractCommonTerm **)
-
-local
- open Hyperreal_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 = Real_Numeral_Simprocs.trans_tac
- val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@hypreal_mult_ac))
- end;
-
-structure EqCancelFactor = ExtractCommonTermFun
- (open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" hyprealT
- val simplify_meta_eq = cancel_simplify_meta_eq mult_cancel_left
-);
-
-
-structure DivideCancelFactor = ExtractCommonTermFun
- (open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "HOL.divide"
- val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT
- val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if
-);
-
-val hypreal_cancel_factor =
- map prep_simproc
- [("hypreal_eq_cancel_factor", ["(l::hypreal) * m = n", "(l::hypreal) = m * n"],
- EqCancelFactor.proc),
- ("hypreal_divide_cancel_factor", ["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)"],
- DivideCancelFactor.proc)];
-
-end;
-
-Addsimprocs hypreal_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::hypreal)";
-test "k = k*(y::hypreal)";
-test "a*(b*c) = (b::hypreal)";
-test "a*(b*c) = d*(b::hypreal)*(x*a)";
-
-
-test "(x*k) / (k*(y::hypreal)) = (uu::hypreal)";
-test "(k) / (k*(y::hypreal)) = (uu::hypreal)";
-test "(a*(b*c)) / ((b::hypreal)) = (uu::hypreal)";
-test "(a*(b*c)) / (d*(b::hypreal)*(x*a)) = (uu::hypreal)";
-
-(*FIXME: what do we do about this?*)
-test "a*(b*c)/(y*z) = d*(b::hypreal)*(x*a)/z";
-*)
-
-
-
-(** Division by 1, -1 **)
-
-Goal "x/-1 = -(x::hypreal)";
-by (Simp_tac 1);
-qed "hypreal_divide_minus1";
-Addsimps [hypreal_divide_minus1];
-
-Goal "-1/(x::hypreal) = - (1/x)";
-by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1);
-qed "hypreal_minus1_divide";
-Addsimps [hypreal_minus1_divide];
-
-
-(*** General rewrites to improve automation, like those for type "int" ***)
-
-(** The next several equations can make the simplifier loop! **)
-
-Goal "(x < - y) = (y < - (x::hypreal))";
-by Auto_tac;
-qed "hypreal_less_minus";
-
-Goal "(- x < y) = (- y < (x::hypreal))";
-by Auto_tac;
-qed "hypreal_minus_less";
-
-Goal "(x <= - y) = (y <= - (x::hypreal))";
-by Auto_tac;
-qed "hypreal_le_minus";
-
-Goal "(- x <= y) = (- y <= (x::hypreal))";
-by Auto_tac;
-qed "hypreal_minus_le";
-
-Goal "(x = - y) = (y = - (x::hypreal))";
-by Auto_tac;
-qed "hypreal_equation_minus";
-
-Goal "(- x = y) = (- (y::hypreal) = x)";
-by Auto_tac;
-qed "hypreal_minus_equation";
-
-Goal "(x + - a = (0::hypreal)) = (x=a)";
-by (arith_tac 1);
-qed "hypreal_add_minus_iff";
-Addsimps [hypreal_add_minus_iff];
-
-Goal "(-b = -a) = (b = (a::hypreal))";
-by (arith_tac 1);
-qed "hypreal_minus_eq_cancel";
-Addsimps [hypreal_minus_eq_cancel];
-
-Goal "(-s <= -r) = ((r::hypreal) <= s)";
-by (stac hypreal_minus_le 1);
-by (Simp_tac 1);
-qed "hypreal_le_minus_iff";
-Addsimps [hypreal_le_minus_iff];
-
-
-(*** Simprules combining x+y and 0 ***)
-
-Goal "(x+y = (0::hypreal)) = (y = -x)";
-by Auto_tac;
-qed "hypreal_add_eq_0_iff";
-AddIffs [hypreal_add_eq_0_iff];
-
-Goal "(x+y < (0::hypreal)) = (y < -x)";
-by Auto_tac;
-qed "hypreal_add_less_0_iff";
-AddIffs [hypreal_add_less_0_iff];
-
-Goal "((0::hypreal) < x+y) = (-x < y)";
-by Auto_tac;
-qed "hypreal_0_less_add_iff";
-AddIffs [hypreal_0_less_add_iff];
-
-Goal "(x+y <= (0::hypreal)) = (y <= -x)";
-by Auto_tac;
-qed "hypreal_add_le_0_iff";
-AddIffs [hypreal_add_le_0_iff];
-
-Goal "((0::hypreal) <= x+y) = (-x <= y)";
-by Auto_tac;
-qed "hypreal_0_le_add_iff";
-AddIffs [hypreal_0_le_add_iff];
-
-
-(** Simprules combining x-y and 0; see also hypreal_less_iff_diff_less_0 etc
- in HyperBin
-**)
-
-Goal "((0::hypreal) < x-y) = (y < x)";
-by Auto_tac;
-qed "hypreal_0_less_diff_iff";
-AddIffs [hypreal_0_less_diff_iff];
-
-Goal "((0::hypreal) <= x-y) = (y <= x)";
-by Auto_tac;
-qed "hypreal_0_le_diff_iff";
-AddIffs [hypreal_0_le_diff_iff];
-
-(*
-FIXME: we should have this, as for type int, but many proofs would break.
-It replaces x+-y by x-y.
-Addsimps [symmetric hypreal_diff_def];
-*)
-
-Goal "-(x-y) = y - (x::hypreal)";
-by (arith_tac 1);
-qed "hypreal_minus_diff_eq";
-Addsimps [hypreal_minus_diff_eq];
-
--- a/src/HOL/Hyperreal/HyperOrd.thy Mon Dec 22 12:50:01 2003 +0100
+++ b/src/HOL/Hyperreal/HyperOrd.thy Mon Dec 22 12:50:22 2003 +0100
@@ -415,9 +415,6 @@
val hrabs_def = thm "hrabs_def";
val hypreal_hrabs = thm "hypreal_hrabs";
-val hypreal_add_cancel_21 = thm"hypreal_add_cancel_21";
-val hypreal_add_cancel_end = thm"hypreal_add_cancel_end";
-val hypreal_minus_diff_eq = thm"hypreal_minus_diff_eq";
val hypreal_less_swap_iff = thm"hypreal_less_swap_iff";
val hypreal_gt_zero_iff = thm"hypreal_gt_zero_iff";
val hypreal_add_less_mono1 = thm"hypreal_add_less_mono1";
--- a/src/HOL/Hyperreal/NSA.ML Mon Dec 22 12:50:01 2003 +0100
+++ b/src/HOL/Hyperreal/NSA.ML Mon Dec 22 12:50:22 2003 +0100
@@ -1551,9 +1551,11 @@
by Auto_tac;
qed "hypreal_of_real_less_Infinitesimal_le_zero";
-(*used once, in NSDERIV_inverse*)
+(*used once, in Lim/NSDERIV_inverse*)
Goal "[| h: Infinitesimal; x ~= 0 |] ==> hypreal_of_real x + h ~= 0";
by Auto_tac;
+by (subgoal_tac "h = - hypreal_of_real x" 1);
+by Auto_tac;
qed "Infinitesimal_add_not_zero";
Goal "x*x + y*y : Infinitesimal ==> x*x : Infinitesimal";
--- a/src/HOL/Hyperreal/SEQ.ML Mon Dec 22 12:50:01 2003 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML Mon Dec 22 12:50:22 2003 +0100
@@ -1131,7 +1131,7 @@
by (forw_inst_tac [("x","f n")] real_inverse_gt_0 1);
by (asm_simp_tac (simpset() addsimps [abs_eqI2]) 1);
by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1);
-by (auto_tac (claset() addIs [real_inverse_less_iff RS iffD2],
+by (auto_tac (claset() addIs [inverse_less_iff_less RS iffD2],
simpset() delsimps [thm"Ring_and_Field.inverse_inverse_eq"]));
qed "LIMSEQ_inverse_zero";
--- a/src/HOL/Hyperreal/Transcendental.ML Mon Dec 22 12:50:01 2003 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML Mon Dec 22 12:50:22 2003 +0100
@@ -2157,7 +2157,7 @@
by (Asm_simp_tac 1);
by (dres_inst_tac [("x","(pi/2) - e")] spec 1);
by (auto_tac (claset(),simpset() addsimps [abs_eqI2,tan_def]));
-by (rtac (real_inverse_less_iff RS iffD1) 1);
+by (rtac (inverse_less_iff_less RS iffD1) 1);
by (auto_tac (claset(),simpset() addsimps [real_divide_def]));
by (rtac (real_mult_order) 1);
by (subgoal_tac "0 < sin e" 3);
--- a/src/HOL/Hyperreal/hypreal_arith.ML Mon Dec 22 12:50:01 2003 +0100
+++ b/src/HOL/Hyperreal/hypreal_arith.ML Mon Dec 22 12:50:22 2003 +0100
@@ -1,11 +1,205 @@
-(* Title: HOL/Real/hypreal_arith.ML
+(* Title: HOL/Hyperreal/hypreal_arith.ML
ID: $Id$
Author: Tobias Nipkow, TU Muenchen
Copyright 1999 TU Muenchen
-Augmentation of hypreal linear arithmetic with rational coefficient handling
+Simprocs: Common factor cancellation & Rational coefficient handling
*)
+(****Common factor cancellation****)
+
+local
+ open Hyperreal_Numeral_Simprocs
+in
+
+val rel_hypreal_number_of = [eq_hypreal_number_of, less_hypreal_number_of,
+ le_hypreal_number_of_eq_not_less];
+
+structure CancelNumeralFactorCommon =
+ struct
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val trans_tac = Real_Numeral_Simprocs.trans_tac
+ val norm_tac =
+ ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps @ mult_1s))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_mult_ac))
+ val numeral_simp_tac =
+ ALLGOALS (simp_tac (HOL_ss addsimps rel_hypreal_number_of@bin_simps))
+ val simplify_meta_eq = simplify_meta_eq
+ end
+
+structure DivCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+ val prove_conv = Bin_Simprocs.prove_conv
+ val mk_bal = HOLogic.mk_binop "HOL.divide"
+ val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT
+ val cancel = mult_divide_cancel_left RS trans
+ val neg_exchanges = false
+)
+
+structure EqCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+ val prove_conv = Bin_Simprocs.prove_conv
+ val mk_bal = HOLogic.mk_eq
+ val dest_bal = HOLogic.dest_bin "op =" hyprealT
+ val cancel = mult_cancel_left RS trans
+ val neg_exchanges = false
+)
+
+structure LessCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+ val prove_conv = Bin_Simprocs.prove_conv
+ val mk_bal = HOLogic.mk_binrel "op <"
+ val dest_bal = HOLogic.dest_bin "op <" hyprealT
+ val cancel = mult_less_cancel_left RS trans
+ val neg_exchanges = true
+)
+
+structure LeCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+ val prove_conv = Bin_Simprocs.prove_conv
+ val mk_bal = HOLogic.mk_binrel "op <="
+ val dest_bal = HOLogic.dest_bin "op <=" hyprealT
+ val cancel = mult_le_cancel_left RS trans
+ val neg_exchanges = true
+)
+
+val hypreal_cancel_numeral_factors_relations =
+ map prep_simproc
+ [("hyprealeq_cancel_numeral_factor",
+ ["(l::hypreal) * m = n", "(l::hypreal) = m * n"],
+ EqCancelNumeralFactor.proc),
+ ("hyprealless_cancel_numeral_factor",
+ ["(l::hypreal) * m < n", "(l::hypreal) < m * n"],
+ LessCancelNumeralFactor.proc),
+ ("hyprealle_cancel_numeral_factor",
+ ["(l::hypreal) * m <= n", "(l::hypreal) <= m * n"],
+ LeCancelNumeralFactor.proc)];
+
+val hypreal_cancel_numeral_factors_divide = prep_simproc
+ ("hyprealdiv_cancel_numeral_factor",
+ ["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)",
+ "((number_of v)::hypreal) / (number_of w)"],
+ DivCancelNumeralFactor.proc);
+
+val hypreal_cancel_numeral_factors =
+ hypreal_cancel_numeral_factors_relations @
+ [hypreal_cancel_numeral_factors_divide];
+
+end;
+
+Addsimprocs hypreal_cancel_numeral_factors;
+
+
+(*examples:
+print_depth 22;
+set timing;
+set trace_simp;
+fun test s = (Goal s; by (Simp_tac 1));
+
+test "0 <= (y::hypreal) * -2";
+test "9*x = 12 * (y::hypreal)";
+test "(9*x) / (12 * (y::hypreal)) = z";
+test "9*x < 12 * (y::hypreal)";
+test "9*x <= 12 * (y::hypreal)";
+
+test "-99*x = 123 * (y::hypreal)";
+test "(-99*x) / (123 * (y::hypreal)) = z";
+test "-99*x < 123 * (y::hypreal)";
+test "-99*x <= 123 * (y::hypreal)";
+
+test "999*x = -396 * (y::hypreal)";
+test "(999*x) / (-396 * (y::hypreal)) = z";
+test "999*x < -396 * (y::hypreal)";
+test "999*x <= -396 * (y::hypreal)";
+
+test "-99*x = -81 * (y::hypreal)";
+test "(-99*x) / (-81 * (y::hypreal)) = z";
+test "-99*x <= -81 * (y::hypreal)";
+test "-99*x < -81 * (y::hypreal)";
+
+test "-2 * x = -1 * (y::hypreal)";
+test "-2 * x = -(y::hypreal)";
+test "(-2 * x) / (-1 * (y::hypreal)) = z";
+test "-2 * x < -(y::hypreal)";
+test "-2 * x <= -1 * (y::hypreal)";
+test "-x < -23 * (y::hypreal)";
+test "-x <= -23 * (y::hypreal)";
+*)
+
+
+(** Declarations for ExtractCommonTerm **)
+
+local
+ open Hyperreal_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 = Real_Numeral_Simprocs.trans_tac
+ val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@hypreal_mult_ac))
+ end;
+
+structure EqCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+ val prove_conv = Bin_Simprocs.prove_conv
+ val mk_bal = HOLogic.mk_eq
+ val dest_bal = HOLogic.dest_bin "op =" hyprealT
+ val simplify_meta_eq = cancel_simplify_meta_eq mult_cancel_left
+);
+
+
+structure DivideCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+ val prove_conv = Bin_Simprocs.prove_conv
+ val mk_bal = HOLogic.mk_binop "HOL.divide"
+ val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT
+ val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if
+);
+
+val hypreal_cancel_factor =
+ map prep_simproc
+ [("hypreal_eq_cancel_factor", ["(l::hypreal) * m = n", "(l::hypreal) = m * n"],
+ EqCancelFactor.proc),
+ ("hypreal_divide_cancel_factor", ["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)"],
+ DivideCancelFactor.proc)];
+
+end;
+
+Addsimprocs hypreal_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::hypreal)";
+test "k = k*(y::hypreal)";
+test "a*(b*c) = (b::hypreal)";
+test "a*(b*c) = d*(b::hypreal)*(x*a)";
+
+
+test "(x*k) / (k*(y::hypreal)) = (uu::hypreal)";
+test "(k) / (k*(y::hypreal)) = (uu::hypreal)";
+test "(a*(b*c)) / ((b::hypreal)) = (uu::hypreal)";
+test "(a*(b*c)) / (d*(b::hypreal)*(x*a)) = (uu::hypreal)";
+
+(*FIXME: what do we do about this?*)
+test "a*(b*c)/(y*z) = d*(b::hypreal)*(x*a)/z";
+*)
+
+
+(****Augmentation of real linear arithmetic with
+ rational coefficient handling****)
+
local
(* reduce contradictory <= to False *)
--- a/src/HOL/IsaMakefile Mon Dec 22 12:50:01 2003 +0100
+++ b/src/HOL/IsaMakefile Mon Dec 22 12:50:22 2003 +0100
@@ -150,7 +150,7 @@
Hyperreal/Fact.ML Hyperreal/Fact.thy\
Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML\
Hyperreal/HRealAbs.thy Hyperreal/HSeries.ML Hyperreal/HSeries.thy\
- Hyperreal/HyperArith0.ML Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\
+ Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\
Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy \
Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\
Hyperreal/HyperOrd.thy Hyperreal/HyperPow.ML\