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.


	Makarius





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