[isabelle] Proofs that hang


In my current formalisation I have a relation which is created through some quite trivial rules. It's an equivalence relation, it is a congruence, it's idempotent and it has one or two more obscure rules. The problem is that these rules are inherently symmetric -- especially rules regarding associativity and commutativity of one of the operators and I am having a hard time to have Isabelel automatically verify proofs even though they are seemingly quite simple. Doing it by hand works, but it's a bit of a pain.

My question is basically if there is a way to reason about these types of relations automatically in Isabelle where the automatic tactics get stuck on symmetries.

Thank you for your time.

Jesper Bengtson

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