Re: [isabelle] Conjunctions commutative in function arguments?
I'm afraid that this proof doesn't follow logically, since in general
P ==> Q does not imply f P ==> f Q.
On 2 Mar 2006, at 11:03, Robert Lamar wrote:
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 archive was generated by a fusion of
Pipermail (Mailman edition) and