summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 27 Jan 1999 17:11:39 +0100 | |

changeset 6157 | 29942d3a1818 |

parent 6156 | 0d52e7cbff29 |

child 6158 | 981f96a598f5 |

arith_tac for min/max

NEWS | file | annotate | diff | comparison | revisions | |

src/HOL/Arith.ML | file | annotate | diff | comparison | revisions | |

src/HOL/Integ/Bin.ML | file | annotate | diff | comparison | revisions | |

src/HOL/Ord.ML | file | annotate | diff | comparison | revisions |

--- 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";