[isabelle] Conjunctions commutative in function arguments?



Title: Conjunctions commutative in function arguments?

Are there special considerations for conjunctions and other basic (or otherwise) logical operators when they are included as arguments to functions?  Currently I am running into a wall on a proof that may be characterized by the failure of the folowing result.  The conjecture

    lemma "f ( P & Q ) ==> f ( Q & P )"

will not be proved by simp, auto, or blast, but

    lemma "P & Q ==> Q & P" by auto

is evaluated without complaint.

Am I missing something basic?  Any thoughts on this question would be appreciated.

Robert



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