Re: [isabelle] Conjunctions commutative in function arguments?



>    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





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