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)

Thanks,

  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
> mathematics.
> 
> Tobias
> 





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