author paulson Fri, 16 Jun 2000 13:28:26 +0200 changeset 9080 67ca888af420 parent 9079 8e9b7095bf59 child 9081 d54b2c41fe0e
fixed the installation of linear arithmetic for the reals
 src/HOL/Real/RealBin.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Real/RealBin.ML	Fri Jun 16 13:21:17 2000 +0200
+++ b/src/HOL/Real/RealBin.ML	Fri Jun 16 13:28:26 2000 +0200
@@ -153,59 +153,6 @@
done in Integ/NatBin.ML*)

-(*  Author:     Tobias Nipkow, TU Muenchen
-
-Instantiate linear arithmetic decision procedure for the reals.
-FIXME: multiplication with constants (eg #2 * x) does not work yet.
-Solution: there should be a simproc for combining coefficients.
-*)
-
-let
-
-(* reduce contradictory <= to False *)
-val simps = [order_less_irrefl,zero_eq_numeral_0,one_eq_numeral_1,
-  mult_real_number_of,eq_real_number_of,less_real_number_of,
-  le_real_number_of_eq_not_less];
-
-val simprocs = [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
-
-  map (fn s => prove_goal thy s
-                 (fn prems => [cut_facts_tac prems 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)"];
-
-in
-LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("RealDef.real",false)]
-end;
-
-let
-val real_arith_simproc_pats =
-  map (fn s => Thm.read_cterm (Theory.sign_of thy) (s, HOLogic.boolT))
-      ["(m::real) < n","(m::real) <= n", "(m::real) = n"];
-
-val fast_real_arith_simproc = mk_simproc
-  "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover;
-in
-end;
-
-

@@ -251,15 +198,15 @@
(** Combining of literal coefficients in sums of products **)

Goal "(x < y) = (x-y < (#0::real))";
-by Auto_tac;
+by (simp_tac (simpset() addsimps [real_diff_less_eq]) 1);
qed "real_less_iff_diff_less_0";

Goal "(x = y) = (x-y = (#0::real))";
-by Auto_tac;
+by (simp_tac (simpset() addsimps [real_diff_eq_eq]) 1);
qed "real_eq_iff_diff_eq_0";

Goal "(x <= y) = (x-y <= (#0::real))";
-by Auto_tac;
+by (simp_tac (simpset() addsimps [real_diff_le_eq]) 1);
qed "real_le_iff_diff_le_0";

@@ -600,22 +547,26 @@

-(*** decision procedure for linear arithmetic ***)
-
(*---------------------------------------------------------------------------*)
(* Linear arithmetic                                                         *)
(*---------------------------------------------------------------------------*)

-(*
-Instantiation of the generic linear arithmetic package for real.
+(* Instantiation of the generic linear arithmetic package for type real. *)
+
+(*  Author:     Tobias Nipkow, TU Muenchen
*)

-(* Update parameters of arithmetic prover *)
let

(* reduce contradictory <= to False *)
+val simps = [order_less_irrefl, zero_eq_numeral_0, one_eq_numeral_1,
+	     mult_real_number_of, eq_real_number_of, less_real_number_of,
+	     le_real_number_of_eq_not_less, real_diff_def,
+
-    real_diff_def ::
map (rename_numerals thy)
@@ -626,23 +577,30 @@
val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@
Real_Numeral_Simprocs.cancel_numerals;

+
-  map (fn s => prove_goal RealBin.thy s
-                 (fn prems => [cut_facts_tac prems 1,
+  map (fn s => prove_goal thy 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)",
+     "(i < j) & (k < l)   ==> i + k < j + (l::real)"];

in