--- a/NEWS Wed Jan 27 17:11:12 1999 +0100
+++ b/NEWS Wed Jan 27 17:11:39 1999 +0100
@@ -36,17 +36,17 @@
* There are now decision procedures for linear arithmetic over nat and int:
1. arith_tac copes with arbitrary formulae involving `=', `<', `<=', `+',
-`-', `Suc' and numerical constants; other subterms are treated as atomic;
-subformulae not involving type `nat' or `int' are ignored; quantified
-subformulae are ignored unless they are positive universal or negative
-existential. The tactic has to be invoked by hand and can be a little bit
-slow. In particular, the running time is exponential in the number of
-occurrences of `-' on `nat'.
+`-', `Suc', `min', `max' and numerical constants; other subterms are treated
+as atomic; subformulae not involving type `nat' or `int' are ignored;
+quantified subformulae are ignored unless they are positive universal or
+negative existential. The tactic has to be invoked by hand and can be a
+little bit slow. In particular, the running time is exponential in the number
+of occurrences of `min' and `max', and `-' on `nat'.
2. fast_arith_tac is a cut-down version of arith_tac: it only takes (negated)
(in)equalities among the premises and the conclusion into account (i.e. no
-compound formulae) and does not know about `-' on `nat'. It is fast and is
-used automatically by the simplifier.
+compound formulae) and does not know about `min' and `max', and `-' on
+`nat'. It is fast and is used automatically by the simplifier.
NB: At the moment, these decision procedures do not cope with mixed nat/int
formulae where the two parts interact, such as `m < n ==> int(m) < int(n)'.
--- a/src/HOL/Arith.ML Wed Jan 27 17:11:12 1999 +0100
+++ b/src/HOL/Arith.ML Wed Jan 27 17:11:39 1999 +0100
@@ -979,11 +979,14 @@
qed "nat_diff_split";
(* FIXME: K true should be replaced by a sensible test to speed things up
- in case there are lots of irrelevant terms involved
+ in case there are lots of irrelevant terms involved;
+ elimination of min/max can be optimized:
+ (max m n + k <= r) = (m+k <= r & n+k <= r)
+ (l <= min m n + k) = (l <= m+k & l <= n+k)
*)
val arith_tac =
- refute_tac (K true) (REPEAT o split_tac[nat_diff_split])
- ((REPEAT_DETERM o etac nat_neqE) THEN' fast_arith_tac);
+ refute_tac (K true) (REPEAT o split_tac[nat_diff_split,split_min,split_max])
+ ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac);
(*---------------------------------------------------------------------------*)
(* End of proof procedures. Now go and USE them! *)
--- a/src/HOL/Integ/Bin.ML Wed Jan 27 17:11:12 1999 +0100
+++ b/src/HOL/Integ/Bin.ML Wed Jan 27 17:11:39 1999 +0100
@@ -492,10 +492,11 @@
(* FIXME: K true should be replaced by a sensible test to speed things up
in case there are lots of irrelevant terms involved.
-*)
+
val arith_tac =
refute_tac (K true) (REPEAT o split_tac[nat_diff_split])
((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac);
+*)
(* Some test data
Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
--- a/src/HOL/Ord.ML Wed Jan 27 17:11:12 1999 +0100
+++ b/src/HOL/Ord.ML Wed Jan 27 17:11:39 1999 +0100
@@ -158,3 +158,13 @@
by (cut_facts_tac [linorder_linear] 1);
by (blast_tac (claset() addIs [order_trans]) 1);
qed "min_le_iff_disj";
+
+Goalw [min_def]
+ "P(min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))";
+by(Simp_tac 1);
+qed "split_min";
+
+Goalw [max_def]
+ "P(max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))";
+by(Simp_tac 1);
+qed "split_max";