# HG changeset patch # User webertj # Date 1187457928 -7200 # Node ID 83afe527504d6f99c6aa4cb36870f55d9e52ab7a # Parent a207114007c62317903d0fbe94a9c2c33de7e769 fixed a bug in demult: -a in (-a * b) is no longer treated as atomic diff -r a207114007c6 -r 83afe527504d src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Sat Aug 18 17:42:39 2007 +0200 +++ b/src/HOL/Tools/lin_arith.ML Sat Aug 18 19:25:28 2007 +0200 @@ -140,93 +140,88 @@ (* Decomposition of terms *) (*internal representation of linear (in-)equations*) -type decompT = ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool); +type decompT = + ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool); fun nT (Type ("fun", [N, _])) = (N = HOLogic.natT) | nT _ = false; fun add_atom (t : term) (m : Rat.rat) (p : (term * Rat.rat) list, i : Rat.rat) : (term * Rat.rat) list * Rat.rat = - case AList.lookup (op =) p t of NONE => ((t, m) :: p, i) - | SOME n => (AList.update (op =) (t, Rat.add n m) p, i); + case AList.lookup (op =) p t of + NONE => ((t, m) :: p, i) + | SOME n => (AList.update (op =) (t, Rat.add n m) p, i); -exception Zero; +(* decompose nested multiplications, bracketing them to the right and combining + all their coefficients -fun rat_of_term (numt, dent) = - let - val num = HOLogic.dest_numeral numt - val den = HOLogic.dest_numeral dent - in - if den = 0 then raise Zero else Rat.rat_of_quotient (num, den) - end; + inj_consts: list of constants to be ignored when encountered + (e.g. arithmetic type conversions that preserve value) -(*Warning: in rare cases number_of encloses a non-numeral, - in which case dest_numeral raises TERM; hence all the handles below. - Same for Suc-terms that turn out not to be numerals - - although the simplifier should eliminate those anyway ...*) -fun number_of_Sucs (Const ("Suc", _) $ n) : int = - number_of_Sucs n + 1 - | number_of_Sucs t = - if HOLogic.is_zero t then 0 else raise TERM ("number_of_Sucs", []); + m: multiplicity associated with the entire product -(*decompose nested multiplications, bracketing them to the right and combining - all their coefficients*) + returns either (SOME term, associated multiplicity) or (NONE, constant) +*) fun demult (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat = let - fun demult ((mC as Const (@{const_name HOL.times}, _)) $ s $ t, m) = ( - (case s of - Const ("Numeral.number_class.number_of", _) $ n => - demult (t, Rat.mult m (Rat.rat_of_int (HOLogic.dest_numeral n))) - | Const (@{const_name HOL.uminus}, _) $ (Const ("Numeral.number_class.number_of", _) $ n) => - demult (t, Rat.mult m (Rat.rat_of_int (~(HOLogic.dest_numeral n)))) - | Const (@{const_name Suc}, _) $ _ => - demult (t, Rat.mult m (Rat.rat_of_int (HOLogic.dest_nat s))) - | Const (@{const_name HOL.times}, _) $ s1 $ s2 => + fun demult ((mC as Const (@{const_name HOL.times}, _)) $ s $ t, m) = + (case s of Const (@{const_name HOL.times}, _) $ s1 $ s2 => + (* bracketing to the right: '(s1 * s2) * t' becomes 's1 * (s2 * t)' *) demult (mC $ s1 $ (mC $ s2 $ t), m) - | Const (@{const_name HOL.divide}, _) $ numt $ - (Const ("Numeral.number_class.number_of", _) $ dent) => - let - val den = HOLogic.dest_numeral dent - in - if den = 0 then - raise Zero - else - demult (mC $ numt $ t, Rat.mult m (Rat.inv (Rat.rat_of_int den))) - end - | _ => - atomult (mC, s, t, m) - ) handle TERM _ => atomult (mC, s, t, m) - ) - | demult (atom as Const(@{const_name HOL.divide}, _) $ t $ - (Const ("Numeral.number_class.number_of", _) $ dent), m) = - (let - val den = HOLogic.dest_numeral dent - in - if den = 0 then - raise Zero - else - demult (t, Rat.mult m (Rat.inv (Rat.rat_of_int den))) - end handle TERM _ => (SOME atom, m)) + | _ => + (* product 's * t', where either factor can be 'NONE' *) + (case demult (s, m) of + (SOME s', m') => + (case demult (t, m') of + (SOME t', m'') => (SOME (mC $ s' $ t'), m'') + | (NONE, m'') => (SOME s', m'')) + | (NONE, m') => demult (t, m'))) + | demult ((mC as Const (@{const_name HOL.divide}, _)) $ s $ t, m) = + (* FIXME: Shouldn't we simplify nested quotients, e.g. '(s/t)/u' could + become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ? Note that + if we choose to do so here, the simpset used by arith must be able to + perform the same simplifications. *) + (* FIXME: Currently we treat the numerator as atomic unless the + denominator can be reduced to a numeric constant. It might be better + to demult the numerator in any case, and invent a new term of the form + '1 / t' if the numerator can be reduced, but the denominator cannot. *) + (* FIXME: Currently we even treat the whole fraction as atomic unless the + denominator can be reduced to a numeric constant. It might be better + to use the partially reduced denominator (i.e. 's / (2* t)' could be + demult'ed to 's / t' with multiplicity .5). This would require a + very simple change only below, but it breaks existing proofs. *) + (* quotient 's / t', where the denominator t can be NONE *) + (* Note: will raise Rat.DIVZERO iff m' is Rat.zero *) + (case demult (t, Rat.one) of + (SOME _, _) => (SOME (mC $ s $ t), m) + | (NONE, m') => apsnd (Rat.mult (Rat.inv m')) (demult (s, m))) + (* terms that evaluate to numeric constants *) + | demult (Const (@{const_name HOL.uminus}, _) $ t, m) = demult (t, Rat.neg m) | demult (Const (@{const_name HOL.zero}, _), m) = (NONE, Rat.zero) | demult (Const (@{const_name HOL.one}, _), m) = (NONE, m) + (*Warning: in rare cases number_of encloses a non-numeral, + in which case dest_numeral raises TERM; hence all the handles below. + Same for Suc-terms that turn out not to be numerals - + although the simplifier should eliminate those anyway ...*) | demult (t as Const ("Numeral.number_class.number_of", _) $ n, m) = - ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_numeral n))) - handle TERM _ => (SOME t, m)) - | demult (Const (@{const_name HOL.uminus}, _) $ t, m) = demult (t, Rat.neg m) + ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_numeral n))) + handle TERM _ => (SOME t, m)) + | demult (t as Const (@{const_name Suc}, _) $ _, m) = + ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_nat t))) + handle TERM _ => (SOME t, m)) + (* injection constants are ignored *) | demult (t as Const f $ x, m) = - (if member (op =) inj_consts f then SOME x else SOME t, m) + if member (op =) inj_consts f then demult (x, m) else (SOME t, m) + (* everything else is considered atomic *) | demult (atom, m) = (SOME atom, m) -and - atomult (mC, atom, t, m) = ( - case demult (t, m) of (NONE, m') => (SOME atom, m') - | (SOME t', m') => (SOME (mC $ atom $ t'), m') - ) in demult end; fun decomp0 (inj_consts : (string * typ) list) (rel : string, lhs : term, rhs : term) : ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat) option = let - (* Turn term into list of summand * multiplicity plus a constant *) + (* Turns a term 'all' and associated multiplicity 'm' into a list 'p' of + summands and associated multiplicities, plus a constant 'i' (with implicit + multiplicity 1) *) fun poly (Const (@{const_name HOL.plus}, _) $ s $ t, m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = poly (s, m, poly (t, m, pi)) | poly (all as Const (@{const_name HOL.minus}, T) $ s $ t, m, pi) = @@ -264,7 +259,7 @@ | @{const_name HOL.less_eq} => SOME (p, i, "<=", q, j) | "op =" => SOME (p, i, "=", q, j) | _ => NONE -end handle Zero => NONE; +end handle Rat.DIVZERO => NONE; fun of_lin_arith_sort thy U = Sign.of_sort thy (U, ["Ring_and_Field.ordered_idom"]); diff -r a207114007c6 -r 83afe527504d src/HOL/ex/Arith_Examples.thy --- a/src/HOL/ex/Arith_Examples.thy Sat Aug 18 17:42:39 2007 +0200 +++ b/src/HOL/ex/Arith_Examples.thy Sat Aug 18 19:25:28 2007 +0200 @@ -130,6 +130,12 @@ apply (tactic {* lin_arith_pre_tac @{context} 1 *}) oops +lemma "-(i::int) * 1 = 0 ==> i = 0" + by (tactic {* fast_arith_tac @{context} 1 *}) + +lemma "[| (0::int) < abs i; abs i * 1 < abs i * j |] ==> 1 < abs i * j" + by (tactic {* fast_arith_tac @{context} 1 *}) + subsection {* Meta-Logic *}