# HG changeset patch # User paulson # Date 1072093822 -3600 # Node ID f508492af9b44da5f1c14bfa5a5d337e7f1b40bd # Parent c0489217deb2d44d20860f753aaac6746dfff3ff moving HyperArith0.ML to other theories diff -r c0489217deb2 -r f508492af9b4 src/HOL/Hyperreal/HyperArith.thy --- 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 diff -r c0489217deb2 -r f508492af9b4 src/HOL/Hyperreal/HyperArith0.ML --- 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]; - diff -r c0489217deb2 -r f508492af9b4 src/HOL/Hyperreal/HyperOrd.thy --- 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"; diff -r c0489217deb2 -r f508492af9b4 src/HOL/Hyperreal/NSA.ML --- 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"; diff -r c0489217deb2 -r f508492af9b4 src/HOL/Hyperreal/SEQ.ML --- 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"; diff -r c0489217deb2 -r f508492af9b4 src/HOL/Hyperreal/Transcendental.ML --- 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); diff -r c0489217deb2 -r f508492af9b4 src/HOL/Hyperreal/hypreal_arith.ML --- 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 *) diff -r c0489217deb2 -r f508492af9b4 src/HOL/IsaMakefile --- 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\