Re: [isabelle] How to process chained facts in Eisbach method?
On 23/05/16 02:50, Daniel Matichuk wrote:
> On 21 May 2016, at 7:08 PM, Lukas Bulwahn <lukas.bulwahn at gmail.com<mailto:lukas.bulwahn at gmail.com>> wrote:
> In my latest Isabelle theory development, I have been using the
> recently added Eisbach technology.
> I have defined a method `injectivity_solver` with Eisbach; what the
> method does is not further relevant for my question.
> Hence, my questions here:
> - Is there a simple way to process chained facts with the current
> Eisbach technology?
> This is a known limitation of Eisbach. The current design choice was to have the inner methods
> in an Eisbach method simply inherit the chained facts, but I think we're getting some evidence that this is not the expected or desired behaviour.
> - Is this feature request considered valuable for Eisbach?
> Yes, I think this is a good discussion to have. My current thinking is to instead bind all of the chained facts in the Eisbach method as a special named_theorem, that you can choose to insert, discard, or pass on to further methods.
How about a general Isar method combinator that manipulates the "using"
slot? E.g. called "use":
by (use facts in simp)
by (use facts in auto simp: ...)
by (use [[simproc foo]] in simp)
That would cover many similar situations that have accumulated in the
past few years.
At this stage it is independently of Eisbach.
This archive was generated by a fusion of
Pipermail (Mailman edition) and