[isabelle] efficiency



Hi All,

I am trying to prove a goal P knowing:

a implies P ; b implies P ;  c implies P ; a \/ b \/ c

Each term a, b and c are of the form u /\ v.
The conclusion P is of the form u /\ (x \/ y \/ z ...).
But this should not matter for the proof.

With small formulae, auto or force work. But otherwise they both never terminate.

Does anyone know what I should use instead of "auto" or "force" to solve this kind of goal ?
I tried safe but it is not better.

Thanks a lot,
Julien


--
Julien Schmaltz                Saarland University
Computer Science Department    Institute for Computer Architecture
Phone: +49 (0)681 302 2419     Fax: +49 (0)681 302 4290
Email: julien at cs.uni-sb.de     WWW: http://www-wjp.cs.uni-sb.de/







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