Would you expect something like this to work?
lemma conj_commute: "P & Q ==> Q & P" by auto
lemma "f ( P & Q ) ==> f ( Q & P )"
assume "f( P & Q )"
from this conj_commute [of P Q]
have "f( Q & P )" by simp
This is less terse, but it is more similar to the methods I am using in my proof. It fails as well, I am afraid.
On Thu 3/2/2006 5:43 AM, Larry Paulson wrote:
| The lemma "conj_commute" expresses commutativity of the conjunction
| operator. You should be able to prove your theorem with something like
| simp add: conj_commute
| Larry Paulson