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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and