Re: [isabelle] Problems with Logic.mk_implies + compose_tac
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, 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.
When I hear "dictates", I am almost certain that it only accidental to the
attempts so far to get this done quickly, and not inherent to the problem.
I reckon that we can safely forget any tricks with "compose_no_flatten" or
"protect" for the rest of this thread, and use the natural Isabelle rule
composition schemes instead.
Sadly, there is specific demand for it. An external reasoner produces an
'inference step instance' of the form:
and I have to 'replace' sg1 with sg2, as it were. (While verifying this
inference 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
Above you say "While verifying this inference step instance with
Isabelle's tactics". If this is so, then it is natural to stay within the
regular framework, as these tactics do anyway. What is the purpose of
mk_implies + Goal.prove? Normally you can just work in-place, by
addressing the subgoal using SUBGOAL, or on an isolated state via
SELECT_GOAL or Subgoal.FOCUS.
If the "magic" above is by a totally alien tool, you can also apply
Object_Logic.full_atomize_tac first, then work on a close HOL proposition,
then apply the result using plain resolve_tac. (A common trap is to get
types too general in examples, then the statement cannot be internalized
This archive was generated by a fusion of
Pipermail (Mailman edition) and