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