Re: [isabelle] Conjunctions commutative in function arguments?
On Thursday 02 March 2006 13:14, Viktor Kuncak wrote:
> Speaking of equality, what is a robust way to prove combinations of
> linear arithmetic and uninterpreted function symbols?
> For example, we would like to prove this simple lemma:
> (g (j - (2::int)) :: int) = g ((-2::int) + j)
> Viktor and Karen
One possibility is to use a set of rewrite rules that put expressions
involving plus and minus into a canonical form. Here is a possible set of
lemmas linear_rews =
Using (simp add: linear_rews) will convert subtraction into addition and
negation, push negation inward as far as possible, and sort all of the added
terms according to the standard term ordering. With your example lemma, the
result is that both sides become syntactically equal, so you don't need to
apply any separate congruence rules.
This archive was generated by a fusion of
Pipermail (Mailman edition) and