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

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:

        ------- (magic)
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.


Attachment: signature.asc
Description: This is a digitally signed message part

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