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:

       ------- (magic)

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

which fails.

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 into HOL.)


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