Email Gateway (Aug 22 2022 at 19:02): Email Gateway (Aug 22 2022 at 19:02):From: Makarius <makarius@sketis.net>
This thread is still open. In the first round of inspection, I did not
get to the bottom of it. It might well be that Eisbach simply does not
support such locality of proof methods. I might be able to say more
after another round of inspection.
Makarius
Email Gateway (Aug 22 2022 at 19:02):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Thanks a lot for looking into that. At the moment, I have some
workarounds in place, but it would be nice to be able to get rid of
those.
In the past I already successfully used Eisbach methods defined within
locales and referring to locale-local things. So Eisbach seems to
support such methods in general.
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 19:03):From: Gerwin.Klein@data61.csiro.au
I can confirm that it was at least the intention that Eisbach should work smoothly with locales and that you can define methods inside locales referring to local facts. There might still be unintended interactions (potentially fundamentally) in how everything plays together esp after export, though.
Cheers,
Gerwin
Email Gateway (Aug 22 2022 at 19:07):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hello!
I’ve defined a proof method using Eisbach within a locale. When invoking
this method, Isabelle seems to sometimes pick it from the wrong locale
interpretation. Consider the following minimal example:
theory Locale_Methods
imports Main "HOL-Eisbach.Eisbach"
begin
locale l =
fixes n :: nat
begin
method m = (rule trans [of _ n _])
end
locale l' = p: l
begin
lemma 1: "n = n"
proof p.m
oops
sublocale s: l "Suc n" .
lemma 2: "n = n"
proof p.m
oops
end
end
The method m defined within the locale l replaces a goal of the form
i = j by the two goals i = n and n = j. Positioning the cursor
behind proof p.m within lemma 1 shows that the expected goals,
n = n and another n = n, have been generated. Positioning the cursor
behind proof p.m in lemma 2 should show the same goals, but in fact
the goals n = Suc n and Suc n = n are presented. Apparently the
proof method s.m has been picked.
Is this a bug in action, or is there another explanation for this
behavior? How can I access p.m after having declared the
sublocale s?
I’m using Isabelle2018.
All the best,
Wolfgang
P.S.: I’ve asked this question also on StackOverflow at
https://stackoverflow.com/questions/54543072, but I ask it here as well
because I didn’t receive an answer on StackOverflow.
Last updated: Apr 19 2024 at 12:27 UTC