Email Gateway (Aug 22 2022 at 13:25): Email Gateway (Aug 22 2022 at 13:25):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
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
Email Gateway (Aug 22 2022 at 13:25):From: Daniel Matichuk <Daniel.Matichuk@nicta.com.au>
Hi Lukas,
Email Gateway (Aug 22 2022 at 13:26):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 22 2022 at 13:27):From: Daniel Matichuk <Daniel.Matichuk@nicta.com.au>
On 27 May 2016, at 1:48 AM, Makarius <makarius@sketis.net> wrote:
On 23/05/16 02:50, Daniel Matichuk wrote:
>On 21 May 2016, at 7:08 PM, Lukas Bulwahn <lukas.bulwahn@gmail.com<mailto:lukas.bulwahn@gmail.com>> wrote:
In my latest Isabelle theory development, I have been using the
recently added Eisbach technology.I have defined a method
injectivity_solverwith 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.
Last updated: Apr 20 2024 at 08:16 UTC