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



Hi Lukas,


On 21 May 2016, at 7:08 PM, Lukas Bulwahn <lukas.bulwahn at gmail.com<mailto:lukas.bulwahn at gmail.com>> wrote:

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?

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.

I believe your problem is similar to one that Simon Wimmer had about a month ago. The solution I proposed for him (quoted below) was to write a small wrapper around the method which would insert the chained facts into the goal state, similar to the SIMPLE_METHOD tactical combinator.

Hi Simon,

Eisbach methods arenât really structured or unstructured, they inherit that from the methods they comprise. This behaviour comes from how the combinators work, i.e. if you write â(-, rule)â then the âruleâ invocation gets the using context. There is certainly a case for treating this more explicitly in Eisbach: I was never convinced one way or the other what a sensible default should be.

My understanding is that you want to hide the âusingâ context from the Eisbach method, choosing instead to insert it into the goal state first. You are always free to write your own higher-order method in order to do this sort of fiddling:

method_setup simple_method =
âMethod_Closure.method_text >> (fn m => fn ctxt => fn facts =>
  let
    val insert' = Method.Basic (K (Method.insert facts))
    val m' = Method.Combinator (Method.no<http://method.no>_combinator_info, Method.Then, [insert', m])
  in Method_Closure.method_evaluate m' ctxt [] end)â

method use_spec = simple_method âerule specâ

lemma
 assumes P: "âx. P x"
 shows "P x"
 using P
 by use_spec

-Dan



- 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.


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



________________________________

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.