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)
>
> Thanks,
>
>   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 
rules:

lemmas linear_rews =
  add_assoc add_commute
  diff_def minus_add_distrib
  minus_minus minus_zero

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.

- Brian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.