--- a/src/HOL/IsaMakefile Wed Dec 10 15:59:34 2003 +0100
+++ b/src/HOL/IsaMakefile Wed Dec 10 16:47:50 2003 +0100
@@ -141,7 +141,7 @@
Real/PRat.ML Real/PRat.thy \
Real/PReal.ML Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \
Real/ROOT.ML Real/Real.thy \
- Real/RealArith0.ML Real/RealArith0.thy Real/real_arith0.ML \
+ Real/RealArith0.thy Real/real_arith0.ML \
Real/RealArith.thy Real/real_arith.ML Real/RealBin.ML \
Real/RealBin.thy Real/RealDef.thy \
Real/RealInt.thy Real/RealOrd.thy \
--- a/src/HOL/Real/RealArith0.ML Wed Dec 10 15:59:34 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,214 +0,0 @@
-(* Title: HOL/Real/RealArith.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1999 University of Cambridge
-
-Common factor cancellation
-*)
-
-val real_inverse_eq_divide = thm"real_inverse_eq_divide";
-val real_mult_less_cancel2 = thm"real_mult_less_cancel2";
-val real_mult_le_cancel2 = thm"real_mult_le_cancel2";
-val real_mult_less_cancel1 = thm"real_mult_less_cancel1";
-val real_mult_le_cancel1 = thm"real_mult_le_cancel1";
-val real_mult_eq_cancel1 = thm"real_mult_eq_cancel1";
-val real_mult_eq_cancel2 = thm"real_mult_eq_cancel2";
-val real_mult_div_cancel1 = thm"real_mult_div_cancel1";
-val real_mult_div_cancel_disj = thm"real_mult_div_cancel_disj";
-
-
-local
- open Real_Numeral_Simprocs
-in
-
-val rel_real_number_of = [eq_real_number_of, less_real_number_of,
- le_real_number_of_eq_not_less]
-
-structure CancelNumeralFactorCommon =
- struct
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
- val trans_tac = trans_tac
- val norm_tac =
- ALLGOALS (simp_tac (HOL_ss addsimps real_minus_from_mult_simps @ mult_1s))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps real_mult_ac))
- val numeral_simp_tac =
- ALLGOALS (simp_tac (HOL_ss addsimps rel_real_number_of@bin_simps))
- val simplify_meta_eq = simplify_meta_eq
- end
-
-structure DivCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "HOL.divide"
- val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
- val cancel = real_mult_div_cancel1 RS trans
- val neg_exchanges = false
-)
-
-structure EqCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
- val cancel = real_mult_eq_cancel1 RS trans
- val neg_exchanges = false
-)
-
-structure LessCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "op <"
- val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT
- val cancel = real_mult_less_cancel1 RS trans
- val neg_exchanges = true
-)
-
-structure LeCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "op <="
- val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT
- val cancel = real_mult_le_cancel1 RS trans
- val neg_exchanges = true
-)
-
-val real_cancel_numeral_factors_relations =
- map prep_simproc
- [("realeq_cancel_numeral_factor",
- ["(l::real) * m = n", "(l::real) = m * n"],
- EqCancelNumeralFactor.proc),
- ("realless_cancel_numeral_factor",
- ["(l::real) * m < n", "(l::real) < m * n"],
- LessCancelNumeralFactor.proc),
- ("realle_cancel_numeral_factor",
- ["(l::real) * m <= n", "(l::real) <= m * n"],
- LeCancelNumeralFactor.proc)]
-
-val real_cancel_numeral_factors_divide = prep_simproc
- ("realdiv_cancel_numeral_factor",
- ["((l::real) * m) / n", "(l::real) / (m * n)",
- "((number_of v)::real) / (number_of w)"],
- DivCancelNumeralFactor.proc)
-
-val real_cancel_numeral_factors =
- real_cancel_numeral_factors_relations @
- [real_cancel_numeral_factors_divide]
-
-end;
-
-Addsimprocs real_cancel_numeral_factors;
-
-
-(*examples:
-print_depth 22;
-set timing;
-set trace_simp;
-fun test s = (Goal s; by (Simp_tac 1));
-
-test "0 <= (y::real) * -2";
-test "9*x = 12 * (y::real)";
-test "(9*x) / (12 * (y::real)) = z";
-test "9*x < 12 * (y::real)";
-test "9*x <= 12 * (y::real)";
-
-test "-99*x = 132 * (y::real)";
-test "(-99*x) / (132 * (y::real)) = z";
-test "-99*x < 132 * (y::real)";
-test "-99*x <= 132 * (y::real)";
-
-test "999*x = -396 * (y::real)";
-test "(999*x) / (-396 * (y::real)) = z";
-test "999*x < -396 * (y::real)";
-test "999*x <= -396 * (y::real)";
-
-test "(- ((2::real) * x) <= 2 * y)";
-test "-99*x = -81 * (y::real)";
-test "(-99*x) / (-81 * (y::real)) = z";
-test "-99*x <= -81 * (y::real)";
-test "-99*x < -81 * (y::real)";
-
-test "-2 * x = -1 * (y::real)";
-test "-2 * x = -(y::real)";
-test "(-2 * x) / (-1 * (y::real)) = z";
-test "-2 * x < -(y::real)";
-test "-2 * x <= -1 * (y::real)";
-test "-x < -23 * (y::real)";
-test "-x <= -23 * (y::real)";
-*)
-
-
-(** Declarations for ExtractCommonTerm **)
-
-local
- open Real_Numeral_Simprocs
-in
-
-structure CancelFactorCommon =
- struct
- val mk_sum = long_mk_prod
- val dest_sum = dest_prod
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff
- val find_first = find_first []
- val trans_tac = trans_tac
- val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@real_mult_ac))
- end;
-
-structure EqCancelFactor = ExtractCommonTermFun
- (open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
- val simplify_meta_eq = cancel_simplify_meta_eq real_mult_eq_cancel1
-);
-
-
-structure DivideCancelFactor = ExtractCommonTermFun
- (open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "HOL.divide"
- val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
- val simplify_meta_eq = cancel_simplify_meta_eq real_mult_div_cancel_disj
-);
-
-val real_cancel_factor =
- map prep_simproc
- [("real_eq_cancel_factor", ["(l::real) * m = n", "(l::real) = m * n"], EqCancelFactor.proc),
- ("real_divide_cancel_factor", ["((l::real) * m) / n", "(l::real) / (m * n)"],
- DivideCancelFactor.proc)];
-
-end;
-
-Addsimprocs real_cancel_factor;
-
-
-(*examples:
-print_depth 22;
-set timing;
-set trace_simp;
-fun test s = (Goal s; by (Asm_simp_tac 1));
-
-test "x*k = k*(y::real)";
-test "k = k*(y::real)";
-test "a*(b*c) = (b::real)";
-test "a*(b*c) = d*(b::real)*(x*a)";
-
-
-test "(x*k) / (k*(y::real)) = (uu::real)";
-test "(k) / (k*(y::real)) = (uu::real)";
-test "(a*(b*c)) / ((b::real)) = (uu::real)";
-test "(a*(b*c)) / (d*(b::real)*(x*a)) = (uu::real)";
-
-(*FIXME: what do we do about this?*)
-test "a*(b*c)/(y*z) = d*(b::real)*(x*a)/z";
-*)
-
-val real_inverse_less_iff = thm"real_inverse_less_iff";
-val real_inverse_le_iff = thm"real_inverse_le_iff";
-
-val pos_real_less_divide_eq = thm"pos_less_divide_eq";
-val pos_real_divide_less_eq = thm"pos_divide_less_eq";
-val pos_real_le_divide_eq = thm"pos_le_divide_eq";
-val pos_real_divide_le_eq = thm"pos_divide_le_eq";
--- a/src/HOL/Real/real_arith.ML Wed Dec 10 15:59:34 2003 +0100
+++ b/src/HOL/Real/real_arith.ML Wed Dec 10 16:47:50 2003 +0100
@@ -1,22 +1,238 @@
(* Title: HOL/Real/real_arith.ML
ID: $Id$
Author: Tobias Nipkow, TU Muenchen
- Copyright 1999 TU Muenchen
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
-Augmentation of real linear arithmetic with rational coefficient handling
+Simprocs: Common factor cancellation & Rational coefficient handling
*)
-val real_divide_1 = thm"real_divide_1";
+
+(** Misc ML bindings **)
+
+val real_inverse_less_iff = thm"real_inverse_less_iff";
+val real_inverse_le_iff = thm"real_inverse_le_iff";
+
+val pos_real_less_divide_eq = thm"pos_less_divide_eq";
+val pos_real_divide_less_eq = thm"pos_divide_less_eq";
+val pos_real_le_divide_eq = thm"pos_le_divide_eq";
+val pos_real_divide_le_eq = thm"pos_divide_le_eq";
+
+
+(****Common factor cancellation****)
+
+val real_inverse_eq_divide = thm"real_inverse_eq_divide";
+val real_mult_less_cancel2 = thm"real_mult_less_cancel2";
+val real_mult_le_cancel2 = thm"real_mult_le_cancel2";
+val real_mult_less_cancel1 = thm"real_mult_less_cancel1";
+val real_mult_le_cancel1 = thm"real_mult_le_cancel1";
+val real_mult_eq_cancel1 = thm"real_mult_eq_cancel1";
+val real_mult_eq_cancel2 = thm"real_mult_eq_cancel2";
+val real_mult_div_cancel1 = thm"real_mult_div_cancel1";
+val real_mult_div_cancel_disj = thm"real_mult_div_cancel_disj";
+
local
+ open Real_Numeral_Simprocs
+in
+
+val rel_real_number_of = [eq_real_number_of, less_real_number_of,
+ le_real_number_of_eq_not_less]
+
+structure CancelNumeralFactorCommon =
+ struct
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val trans_tac = trans_tac
+ val norm_tac =
+ ALLGOALS (simp_tac (HOL_ss addsimps real_minus_from_mult_simps @ mult_1s))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps real_mult_ac))
+ val numeral_simp_tac =
+ ALLGOALS (simp_tac (HOL_ss addsimps rel_real_number_of@bin_simps))
+ val simplify_meta_eq = simplify_meta_eq
+ end
+
+structure DivCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+ val prove_conv = Bin_Simprocs.prove_conv
+ val mk_bal = HOLogic.mk_binop "HOL.divide"
+ val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
+ val cancel = real_mult_div_cancel1 RS trans
+ val neg_exchanges = false
+)
+
+structure EqCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+ val prove_conv = Bin_Simprocs.prove_conv
+ val mk_bal = HOLogic.mk_eq
+ val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
+ val cancel = real_mult_eq_cancel1 RS trans
+ val neg_exchanges = false
+)
+
+structure LessCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+ val prove_conv = Bin_Simprocs.prove_conv
+ val mk_bal = HOLogic.mk_binrel "op <"
+ val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT
+ val cancel = real_mult_less_cancel1 RS trans
+ val neg_exchanges = true
+)
+
+structure LeCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+ val prove_conv = Bin_Simprocs.prove_conv
+ val mk_bal = HOLogic.mk_binrel "op <="
+ val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT
+ val cancel = real_mult_le_cancel1 RS trans
+ val neg_exchanges = true
+)
+
+val real_cancel_numeral_factors_relations =
+ map prep_simproc
+ [("realeq_cancel_numeral_factor",
+ ["(l::real) * m = n", "(l::real) = m * n"],
+ EqCancelNumeralFactor.proc),
+ ("realless_cancel_numeral_factor",
+ ["(l::real) * m < n", "(l::real) < m * n"],
+ LessCancelNumeralFactor.proc),
+ ("realle_cancel_numeral_factor",
+ ["(l::real) * m <= n", "(l::real) <= m * n"],
+ LeCancelNumeralFactor.proc)]
+
+val real_cancel_numeral_factors_divide = prep_simproc
+ ("realdiv_cancel_numeral_factor",
+ ["((l::real) * m) / n", "(l::real) / (m * n)",
+ "((number_of v)::real) / (number_of w)"],
+ DivCancelNumeralFactor.proc)
+
+val real_cancel_numeral_factors =
+ real_cancel_numeral_factors_relations @
+ [real_cancel_numeral_factors_divide]
+
+end;
+
+Addsimprocs real_cancel_numeral_factors;
+
+
+(*examples:
+print_depth 22;
+set timing;
+set trace_simp;
+fun test s = (Goal s; by (Simp_tac 1));
+
+test "0 <= (y::real) * -2";
+test "9*x = 12 * (y::real)";
+test "(9*x) / (12 * (y::real)) = z";
+test "9*x < 12 * (y::real)";
+test "9*x <= 12 * (y::real)";
+
+test "-99*x = 132 * (y::real)";
+test "(-99*x) / (132 * (y::real)) = z";
+test "-99*x < 132 * (y::real)";
+test "-99*x <= 132 * (y::real)";
+
+test "999*x = -396 * (y::real)";
+test "(999*x) / (-396 * (y::real)) = z";
+test "999*x < -396 * (y::real)";
+test "999*x <= -396 * (y::real)";
+
+test "(- ((2::real) * x) <= 2 * y)";
+test "-99*x = -81 * (y::real)";
+test "(-99*x) / (-81 * (y::real)) = z";
+test "-99*x <= -81 * (y::real)";
+test "-99*x < -81 * (y::real)";
+
+test "-2 * x = -1 * (y::real)";
+test "-2 * x = -(y::real)";
+test "(-2 * x) / (-1 * (y::real)) = z";
+test "-2 * x < -(y::real)";
+test "-2 * x <= -1 * (y::real)";
+test "-x < -23 * (y::real)";
+test "-x <= -23 * (y::real)";
+*)
+
+
+(** Declarations for ExtractCommonTerm **)
+
+local
+ open Real_Numeral_Simprocs
+in
+
+structure CancelFactorCommon =
+ struct
+ val mk_sum = long_mk_prod
+ val dest_sum = dest_prod
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff
+ val find_first = find_first []
+ val trans_tac = trans_tac
+ val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@real_mult_ac))
+ end;
+
+structure EqCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+ val prove_conv = Bin_Simprocs.prove_conv
+ val mk_bal = HOLogic.mk_eq
+ val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
+ val simplify_meta_eq = cancel_simplify_meta_eq real_mult_eq_cancel1
+);
+
+
+structure DivideCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+ val prove_conv = Bin_Simprocs.prove_conv
+ val mk_bal = HOLogic.mk_binop "HOL.divide"
+ val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
+ val simplify_meta_eq = cancel_simplify_meta_eq real_mult_div_cancel_disj
+);
+
+val real_cancel_factor =
+ map prep_simproc
+ [("real_eq_cancel_factor", ["(l::real) * m = n", "(l::real) = m * n"], EqCancelFactor.proc),
+ ("real_divide_cancel_factor", ["((l::real) * m) / n", "(l::real) / (m * n)"],
+ DivideCancelFactor.proc)];
+
+end;
+
+Addsimprocs real_cancel_factor;
+
+
+(*examples:
+print_depth 22;
+set timing;
+set trace_simp;
+fun test s = (Goal s; by (Asm_simp_tac 1));
+
+test "x*k = k*(y::real)";
+test "k = k*(y::real)";
+test "a*(b*c) = (b::real)";
+test "a*(b*c) = d*(b::real)*(x*a)";
+
+
+test "(x*k) / (k*(y::real)) = (uu::real)";
+test "(k) / (k*(y::real)) = (uu::real)";
+test "(a*(b*c)) / ((b::real)) = (uu::real)";
+test "(a*(b*c)) / (d*(b::real)*(x*a)) = (uu::real)";
+
+(*FIXME: what do we do about this?*)
+test "a*(b*c)/(y*z) = d*(b::real)*(x*a)/z";
+*)
+
+(****Augmentation of real linear arithmetic with
+ rational coefficient handling****)
+
+val divide_1 = thm"divide_1";
val times_divide_eq_left = thm"times_divide_eq_left";
val times_divide_eq_right = thm"times_divide_eq_right";
+local
+
(* reduce contradictory <= to False *)
val simps = [True_implies_equals,
inst "w" "number_of ?v" real_add_mult_distrib2,
- real_divide_1,times_divide_eq_right,times_divide_eq_left];
+ divide_1,times_divide_eq_right,times_divide_eq_left];
val simprocs = [real_cancel_numeral_factors_divide];