Email Gateway (Aug 17 2022 at 13:46): Email Gateway (Aug 17 2022 at 13:46):From: nipkow@in.tum.de
lemma "f ( P & Q ) ==> f ( Q & P )"
Unfortunately this is not entirely trivial. It is known as "congruence
closure", because you propagate (nontrivial) equalities up through a
term. Isabelle does not do this automatically (although for fixed equational
laws it could, with some additional work). However, in your case it is
possible to circumvent the problem: add conj_commte (commutativity of
&) as a simp rule to simp or auto. The section on permutative simplification
in the tutorial explains the details.
Tobias Nipkow
Email Gateway (Aug 17 2022 at 14:15):From: Robert Lamar <rlamar@stetson.edu>
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
Last updated: May 03 2024 at 04:19 UTC