combining Real/{RealArith0,real_arith}.ML
authorpaulson
Wed, 10 Dec 2003 16:47:50 +0100
changeset 14289 deb8e1e62002
parent 14288 d149e3cbdb39
child 14290 84fda1b39947
combining Real/{RealArith0,real_arith}.ML
src/HOL/IsaMakefile
src/HOL/Real/RealArith0.ML
src/HOL/Real/real_arith.ML
--- 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];