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



> On 27 May 2016, at 1:48 AM, Makarius <makarius at sketis.net> wrote:
>
> 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.

I agree that this makes sense, this is similar to the solution I proposed to Christian Sternagel's issue a few weeks ago. It's unclear whether it should override the "using" slot or augment it, though.

>
> At this stage it is independently of Eisbach.

I'm not sure if this is what you were suggesting, but I think that the named_theorems idea would work in conjunction with the proposed "use" combinator.

i.e.

method foo uses other_rules = (rule baz, use using_rules other_rules in simp)

Where the initial invocation of the "rule" method always has an empty "using" slot (and so will predictably only apply the "baz" rule), but it gets chained into "simp" via the special "using_rules" fact, and is augmented with any given "other_rules".

Does that make sense?

>
>
>       Makarius
>


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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