*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Problems with Logic.mk_implies + compose_tac*From*: Matej Urbas <mu232 at cam.ac.uk>*Date*: Sun, 10 Jul 2011 23:14:06 +0100*Cc*: Isabelle Users Mailing List <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <alpine.LNX.1.10.1107102138080.20402@atbroy100.informatik.tu-muenchen.de>*References*: <1310215039.3708.28.camel@toncka.urbas.si> <alpine.LNX.1.10.1107102138080.20402@atbroy100.informatik.tu-muenchen.de>

On Sun, 2011-07-10 at 21:43 +0200, Makarius wrote: > This is all a bit indirect -- working against the natural flow of > reasoning in Isabelle/Pure. Sadly, there is specific demand for it. An external reasoner produces an 'inference step instance' of the form: sg2 ------- (magic) sg1 and I have to 'replace' sg1 with sg2, as it were. (While verifying this inference step instance with Isabelle's tactics.) > Note that compose_tac is outside the normal > rule composition paradigm, i.e. you are standing naked in the cold rain. I am sorry, but I do not understand this analogy. Could you please elaborate on why compose_tac is fragile? > When you have a structured goal with its own !! and ==> the canonical > proof enters that context and establishes the conclusion, e.g. see > SUBGOAL.FOCUS and similar (which are mentioned in the "implementation" > manual). Thank you very much. I will try and use this. Sadly, however, a quick glance at the documentation did not reveal a way to 'inject' my 'target term' (sg2) into the clockwork of FOCUS et al. It could be possible if I constructed my own instance of the 'focus' record. However, I would suspect expert users to frown at that thought -- am I right in assuming this? Still, why would be the type 'focus' specified concretely in the SUBGOAL signature if not intended for users to use? > There are sometimes reasons to bypass the primary structure, but it should > be only done if there are explicit reasons for it. My favourite internal > operation for that is Thm.compose_no_flatten, but that is not for the > faint-hearted. 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, it is hard to see right for wrong -- especially since there are no hints that could steer me away from the wrong path. Also, do you mind if I ask for a pointer to some documentation regarding the 'compose_no_flatten' function. It seems that Thomas' suggestion with 'protect' could be related to this one. Apologies for the length. Best, --- Matej

**Attachment:
signature.asc**

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

**Re: [isabelle] Problems with Logic.mk_implies + compose_tac***From:*Makarius

- 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