*To*: Matej Urbas <mu232 at cam.ac.uk>*Subject*: Re: [isabelle] Problems with Logic.mk_implies + compose_tac*From*: Makarius <makarius at sketis.net>*Date*: Mon, 11 Jul 2011 11:39:24 +0200 (CEST)*Cc*: Isabelle Users Mailing List <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <1310215039.3708.28.camel@toncka.urbas.si>*References*: <1310215039.3708.28.camel@toncka.urbas.si>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Sun, 10 Jul 2011, Matej Urbas wrote:

My particular use case dictates behaviour as was previously described.Frankly, I do not mind how I achieve it. The initially mentioned method(with compose_tac) was just the first one I discovered. I must admit, itis hard to see right for wrong -- especially since there are no hintsthat could steer me away from the wrong path.Also, do you mind if I ask for a pointer to some documentation regardingthe 'compose_no_flatten' function. It seems that Thomas' suggestion with'protect' could be related to this one.

Sadly, there is specific demand for it. An external reasoner produces an'inference step instance' of the form:sg2 ------- (magic) sg1and I have to 'replace' sg1 with sg2, as it were. (While verifying thisinference step instance with Isabelle's tactics.)

I am having a bit of problems using 'compose_tac' with an intermediate theorem (produced with mk_implies + Goal.prove).

The next step is to use interThm in 'compose_tac', which is applied on the original goal sg1: compose_tac (false, interThm, 1) i which fails.

Makarius

**Follow-Ups**:**Re: [isabelle] Problems with Logic.mk_implies + compose_tac***From:*Sascha Boehme

**References**:**[isabelle] Problems with Logic.mk_implies + compose_tac***From:*Matej Urbas

- Previous by Date: Re: [isabelle] Problems with Logic.mk_implies + compose_tac
- Next by Date: Re: [isabelle] Problems with Logic.mk_implies + compose_tac
- Previous by Thread: Re: [isabelle] Problems with Logic.mk_implies + compose_tac
- Next by Thread: Re: [isabelle] Problems with Logic.mk_implies + compose_tac
- Cl-isabelle-users July 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list