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.

Larry Paulson


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 )"
    proof -
      assume "f( P & Q )"
      from this conj_commute [of P Q]
      have "f( Q & P )" by simp
    qed






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