author | nipkow |

Wed Jan 27 17:11:39 1999 +0100 (1999-01-27) | |

changeset 6157 | 29942d3a1818 |

parent 6156 | 0d52e7cbff29 |

child 6158 | 981f96a598f5 |

arith_tac for min/max

NEWS | file | annotate | diff | revisions | |

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

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

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

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