Re: [isabelle] Conjunctions commutative in function arguments?
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
nipkow at in.tum.de wrote:
> lemma conj_commute: "P & Q ==> Q & P" by auto
> is not a very useful lemma in your context. It is just not true that "A ==>
> B" implies "f A ==> f B", sorry. If you replace "==>" by "=" it becomes
> true. Hence the popularity of "=", one of the greatest inventions of
This archive was generated by a fusion of
Pipermail (Mailman edition) and