Re: [isabelle] Conjunctions commutative in function arguments?



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


On 1 Mar 2006, at 21:24, Robert Lamar wrote:

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.






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