Re: [isabelle] Conjunctions commutative in function arguments?



Title: RE: [isabelle] Conjunctions commutative in function arguments?

Would you expect something like this to work?

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

    lemma "f ( P & Q ) ==> f ( Q & P )"
    proof -
      assume "f( P & Q )"
      from this conj_commute [of P Q]
      have "f( Q & P )" by simp
    qed

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.

Robert Lamar


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
|



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