Email Gateway (Aug 19 2022 at 14:51): Email Gateway (Aug 19 2022 at 14:51):From: Gottfried Barrow <igbi@gmx.com>
Florian,
This shows cntl-clicking has its limitation as an educational tool,
where some of what I say here doesn't exactly fit anything, because I'm
talking about both the pre-RC0 install I have, and the 2014-RC0 install.
But, with this pre-RC0 Isabelle, I have these:
thm "add_assoc" ([name "Groups.semigroup_add_class.add_assoc"])
thm "Groups.semigroup_add.add_assoc"
thm "Groups.semigroup_add_class.add_assoc"
All of those take me to
line 152:
class semigroup_add = plus +
assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b
After doing a lot of grepping to find where the "add" of "add.assoc" is
defined, I finally decided it had to be the following, since it doesn't
show up anywhere else:
line 156:
sublocale add!: semigroup plus
by default (fact add_assoc)
I could say it's obvious now, but it's not because I've read nothing
that tells me that "add!" defines "add" of "add.assoc". So, what's in
NEWS about "add.assoc" wouldn't have meant anything to me without a
little help about this.
Anyway, I kind of understanding the use of class with class, and that
class is a locale, and the use of locale with locale, but I haven't
understood the mixing of "locale" with "class" in Groups.thy, so if I
get a chance to work through Groups.thy, it could be I'll understand it
better with this knowledge.
Regards,
GB
Email Gateway (Aug 19 2022 at 14:52):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Gottfried,
if you want to inspect the theories in HOL-Main interactively, you can
do so by e.g.
isabelle jedit -l Pure src/HOL/Groups.thy
Admittedly »cntl-clicking« has its limitations in the presence of »multi
dimensions« which enter the game through locale interpretation. But to
get a rough idea what is pulled in by »interpretation« or »sublocale«,
issue »print_theorems« directly afterwards.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 14:54):From: Gottfried Barrow <igbi@gmx.com>
On 14-07-12 14:27, Florian Haftmann wrote:
if you want to inspect the theories in HOL-Main interactively, you can
do so by e.g.isabelle jedit -l Pure src/HOL/Groups.thy
I've seen that several times, but I always forget about it, so now I've
made me a batch file to remind me how to look at single files like that.
Admittedly »cntl-clicking« has its limitations in the presence of »multi
dimensions« which enter the game through locale interpretation. But to
get a rough idea what is pulled in by »interpretation« or »sublocale«,
issue »print_theorems« directly afterwards.
In a roundabout way that's helped make things a little clearer.
The learning curve of Isabelle isn't linear. It is better described as
discontinuous everywhere, so I do searches in docs to find the
particular use of some syntax, and then go forwards or backwards.
I haven't find anything like "sublocale add!:", but I finally made the
connection to things like "sublocale partial_order < dual!:". Type
classes are fairly straight forward, and I have uses for them, but
locales aren't as straight forward, and I haven't used them much.
It's not obvious that "interpretation" and "sublocale" should go
together. For anyone who hasn't found it, there's this additional PDF
about locales by Clemens Ballarin, published in 2014:
http://www4.in.tum.de/~ballarin/publications/jar2013.pdf
of http://www4.in.tum.de/~ballarin/publications/index.html
Regards,
GB
Email Gateway (Aug 19 2022 at 15:18):From: Gottfried Barrow <igbi@gmx.com>
Hi,
There's "Groups.semigroup_add.add_assoc", followed in Groups.thy by
"hide_fact add_assoc". The "hide_fact" is new in Groups.thy and causes
an error in a proof.
The proof passes even through there's an error 'Undefined fact:
"add_assoc"'. I attach a screen shot showing the error.
Trying to fix that problem, I ran Sledgehammer and have a more serious
problem, which is that Cygwin temp files can't be deleted, which causes
the prover process to terminate. I'll put that that in another email.
Regards,
GB
Hidden_add_assoc_error.png
Email Gateway (Aug 19 2022 at 15:19):From: Peter Lammich <lammich@in.tum.de>
You have to watch out for the error markers. If there is an error marker
somewhere, you're theory has not passed through. To get an overview of
error markers, use the theory-panel, there you see a tiny red bar on
every theory that has been processed and contains an error. Mark the
little check-boxes in the theory-panel to ensure that a theory gets
processed.
Additionally, you might see a red mark on the right-hand side of the
text area in the theory file, that can be used to navigate to the error
location in the text buffer, where you see a squiggly red line that
indicates the exact position of the error.
To get a more definite answer on whether your stuff contains errors or
not, you have to use "isabelle build".
Email Gateway (Aug 19 2022 at 15:19):From: Gottfried Barrow <igbi@gmx.com>
On 14-07-09 14:40, Peter Lammich wrote:
You have to watch out for the error markers. If there is an error marker
somewhere, you're theory has not passed through. To get an overview of
error markers, use the theory-panel, there you see a tiny red bar on
every theory that has been processed and contains an error. Mark the
little check-boxes in the theory-panel to ensure that a theory gets
processed.
Peter,
Okay. I guess I've been conditioned by the PIDE to think that there's
something wrong when a proof goal has been proved, yet there's an error
in the "apply" or "by" statement.
That normally doesn't happen. Normally, if "apply" or "by" is marked red
because of an error, the proof goal isn't proved. But, I can adapt, if I
can remember to. In this case, multiple things were going wrong due to
the changes with Isabelle2014-RC0.
Thanks,
GB
Additionally, you might see a red mark on the right-hand side of the
text area in the theory file, that can be used to navigate to the error
location in the text buffer, where you see a squiggly red line that
indicates the exact position of the error.To get a more definite answer on whether your stuff contains errors or
not, you have to use "isabelle build".--
PeterOn Mi, 2014-07-09 at 14:11 -0500, Gottfried Barrow wrote:
Hi,
There's "Groups.semigroup_add.add_assoc", followed in Groups.thy by
"hide_fact add_assoc". The "hide_fact" is new in Groups.thy and causes
an error in a proof.The proof passes even through there's an error 'Undefined fact:
"add_assoc"'. I attach a screen shot showing the error.Trying to fix that problem, I ran Sledgehammer and have a more serious
problem, which is that Cygwin temp files can't be deleted, which causes
the prover process to terminate. I'll put that that in another email.Regards,
GB
Email Gateway (Aug 19 2022 at 15:20):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Gottfried,
this is a misunderstanding. The canonical name for associativity of
plus is now add.assoc, cf. NEWS.
The add_assoc you have stumbled over is just a device to bootstrap the
locale / type class hierarchy.
Hope this helps,
Florian
signature.asc
Last updated: Apr 25 2024 at 20:15 UTC