arith_tac for min/max
authornipkow
Wed Jan 27 17:11:39 1999 +0100 (1999-01-27)
changeset 615729942d3a1818
parent 6156 0d52e7cbff29
child 6158 981f96a598f5
arith_tac for min/max
NEWS
src/HOL/Arith.ML
src/HOL/Integ/Bin.ML
src/HOL/Ord.ML
     1.1 --- a/NEWS	Wed Jan 27 17:11:12 1999 +0100
     1.2 +++ b/NEWS	Wed Jan 27 17:11:39 1999 +0100
     1.3 @@ -36,17 +36,17 @@
     1.4  * There are now decision procedures for linear arithmetic over nat and int:
     1.5  
     1.6  1. arith_tac copes with arbitrary formulae involving `=', `<', `<=', `+',
     1.7 -`-', `Suc' and numerical constants; other subterms are treated as atomic;
     1.8 -subformulae not involving type `nat' or `int' are ignored; quantified
     1.9 -subformulae are ignored unless they are positive universal or negative
    1.10 -existential. The tactic has to be invoked by hand and can be a little bit
    1.11 -slow. In particular, the running time is exponential in the number of
    1.12 -occurrences of `-' on `nat'.
    1.13 +`-', `Suc', `min', `max' and numerical constants; other subterms are treated
    1.14 +as atomic; subformulae not involving type `nat' or `int' are ignored;
    1.15 +quantified subformulae are ignored unless they are positive universal or
    1.16 +negative existential. The tactic has to be invoked by hand and can be a
    1.17 +little bit slow. In particular, the running time is exponential in the number
    1.18 +of occurrences of `min' and `max', and `-' on `nat'.
    1.19  
    1.20  2. fast_arith_tac is a cut-down version of arith_tac: it only takes (negated)
    1.21  (in)equalities among the premises and the conclusion into account (i.e. no
    1.22 -compound formulae) and does not know about `-' on `nat'. It is fast and is
    1.23 -used automatically by the simplifier.
    1.24 +compound formulae) and does not know about `min' and `max', and `-' on
    1.25 +`nat'. It is fast and is used automatically by the simplifier.
    1.26  
    1.27  NB: At the moment, these decision procedures do not cope with mixed nat/int
    1.28  formulae where the two parts interact, such as `m < n ==> int(m) < int(n)'.
     2.1 --- a/src/HOL/Arith.ML	Wed Jan 27 17:11:12 1999 +0100
     2.2 +++ b/src/HOL/Arith.ML	Wed Jan 27 17:11:39 1999 +0100
     2.3 @@ -979,11 +979,14 @@
     2.4  qed "nat_diff_split";
     2.5  
     2.6  (* FIXME: K true should be replaced by a sensible test to speed things up
     2.7 -   in case there are lots of irrelevant terms involved
     2.8 +   in case there are lots of irrelevant terms involved;
     2.9 +   elimination of min/max can be optimized:
    2.10 +   (max m n + k <= r) = (m+k <= r & n+k <= r)
    2.11 +   (l <= min m n + k) = (l <= m+k & l <= n+k)
    2.12  *)
    2.13  val arith_tac =
    2.14 -  refute_tac (K true) (REPEAT o split_tac[nat_diff_split])
    2.15 -             ((REPEAT_DETERM o etac nat_neqE) THEN' fast_arith_tac);
    2.16 +  refute_tac (K true) (REPEAT o split_tac[nat_diff_split,split_min,split_max])
    2.17 +             ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac);
    2.18  
    2.19  (*---------------------------------------------------------------------------*)
    2.20  (* End of proof procedures. Now go and USE them!                             *)
     3.1 --- a/src/HOL/Integ/Bin.ML	Wed Jan 27 17:11:12 1999 +0100
     3.2 +++ b/src/HOL/Integ/Bin.ML	Wed Jan 27 17:11:39 1999 +0100
     3.3 @@ -492,10 +492,11 @@
     3.4  
     3.5  (* FIXME: K true should be replaced by a sensible test to speed things up
     3.6     in case there are lots of irrelevant terms involved.
     3.7 -*)
     3.8 +
     3.9  val arith_tac =
    3.10    refute_tac (K true) (REPEAT o split_tac[nat_diff_split])
    3.11               ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac);
    3.12 +*)
    3.13  
    3.14  (* Some test data
    3.15  Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
     4.1 --- a/src/HOL/Ord.ML	Wed Jan 27 17:11:12 1999 +0100
     4.2 +++ b/src/HOL/Ord.ML	Wed Jan 27 17:11:39 1999 +0100
     4.3 @@ -158,3 +158,13 @@
     4.4  by (cut_facts_tac [linorder_linear] 1);
     4.5  by (blast_tac (claset() addIs [order_trans]) 1);
     4.6  qed "min_le_iff_disj";
     4.7 +
     4.8 +Goalw [min_def]
     4.9 + "P(min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))";
    4.10 +by(Simp_tac 1);
    4.11 +qed "split_min";
    4.12 +
    4.13 +Goalw [max_def]
    4.14 + "P(max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))";
    4.15 +by(Simp_tac 1);
    4.16 +qed "split_max";