# HG changeset patch
# User nipkow
# Date 917453499 -3600
# Node ID 29942d3a1818fd413d512447a97dcc013d453478
# Parent  0d52e7cbff29204d58dd3ec74b1a7d4f0a1be06b
arith_tac for min/max

diff -r 0d52e7cbff29 -r 29942d3a1818 NEWS
--- 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)'.
diff -r 0d52e7cbff29 -r 29942d3a1818 src/HOL/Arith.ML
--- 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!                             *)
diff -r 0d52e7cbff29 -r 29942d3a1818 src/HOL/Integ/Bin.ML
--- 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";
diff -r 0d52e7cbff29 -r 29942d3a1818 src/HOL/Ord.ML
--- 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";