[isabelle] How to process chained facts in Eisbach method?



Dear all,

In my latest Isabelle theory development, I have been using the
recently added Eisbach technology. Thanks to Daniel, Makarius and Toby
for the work on this valuable addition to Isabelle.

After very quickly writing the essential functionality of my method, I
then unfortunately stumbled with the following issue:

I have defined a method `injectivity_solver` with Eisbach; what the
method does is not further relevant for my question.

I currently employ the method on certain goals (where disjoint_under
is a defined predicate, and ?comp and ?S are some fixed terms).

To make the chained facts F1 ... F3  part of the proof state the
Eisbach method acts on, I use `by - (injectivity_solver ...)` or
`apply - apply (injectivity_solver ...)` as follows:

  have "disjoint_under ?comp ?S" using F1 F2 F3 by - (injectivity_solver ...)
  have "disjoint_under ?comp ?S" using F1 F2 F3 apply - apply
(injectivity_solver ...)

However, the following fails:

  have "G" using F1 F2 F3 by m

I did not find a way to make the Eisbach method itself insert the
chained facts into the proof goal before applying the further methods
(by some simple experiments and by looking through the Eisbach
manual).

Available local Isabelle experts in the very close Munich area did not
have a quick answer at hand.

Hence, my questions here:

- Is there a simple way to process chained facts with the current
Eisbach technology?

- Is this feature request considered valuable for Eisbach?

For further details and experimentation, the described setup is in the
AFP entry Bell_Numbers_Spivey. The method is defined in lines 111f.
and invoked in lines 522, 543 and 554 of the Bell_Numbers theory file.

Best regards,

Lukas




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