Email Gateway (Aug 22 2022 at 12:40): Email Gateway (Aug 22 2022 at 12:40):From: "henning.seidler" <henning.seidler@mailbox.tu-berlin.de>
Dear Isabelle list,
Currently I am working quite a lot on low levels, so I wonder what is
the best way to have theories like Inductive.thy "linked", that is, when
clicking on a lemma, I move to that spot?
I tried setting the base theory to Pure, but then a lot of errors occurred.
Also, is there the possibility to fold exactly the proof of a lemma? In
my current settings only the first line of the statement remains.
On the other hand, regarding the content, I want to show something like
lemma "{ f::'a => 'b . True } \subseteq (UNIV::('a \times 'b ) set)"
I guess the solution uses curry or split in front of f, but I do not see
how.
Best regards,
Henning
signature.asc
Email Gateway (Aug 22 2022 at 12:41):From: Lars Hupel <hupel@in.tum.de>
Dear Henning,
Currently I am working quite a lot on low levels, so I wonder what is
the best way to have theories like Inductive.thy "linked", that is, when
clicking on a lemma, I move to that spot?
I tried setting the base theory to Pure, but then a lot of errors occurred.
you can start Isabelle/jEdit like this:
isabelle jedit -l Pure
or, as you probably did, change the image from "HOL" to "Pure" in the
Theories panel.
If you then want to use HOL stuff, import from
"~~/src/HOL/Main"
Then jEdit will load all the theories from HOL for you and you can
Ctrl-Click there as usual.
On the other hand, regarding the content, I want to show something like
lemma "{ f::'a => 'b . True } \subseteq (UNIV::('a \times 'b ) set)"
This looks like a type error to me ... You are comparing a set of
functions to a set of tuples.
In any case, your statement is trivial: Every set is a subset of UNIV
(see theorem "Set.subset_UNIV").
Cheers
Lars
Email Gateway (Aug 22 2022 at 12:41):From: Makarius <makarius@sketis.net>
Since the name "jEdit" has been used in the wrong sense twice on this
thread, here is the relevant quote from the Isabelle/jEdit manual:
➧[jEdit] is a sophisticated text editor⁋‹@{url
"http://www.jedit.org"}› implemented in Java⁋‹@{url
"http://www.java.com"}›. It is easily extensible by plugins written in
any language that works on the JVM. In the context of Isabelle this is
always Scala⁋‹@{url "http://www.scala-lang.org"}›.
➧[Isabelle/jEdit] is the main application of the PIDE framework and
the default user-interface for Isabelle. It targets both beginners and
experts. Technically, Isabelle/jEdit consists of the original jEdit
code base with minimal patches and a special plugin for Isabelle. This
is integrated as a desktop application for the main operating system
families: Linux, Windows, Mac OS X.
End-users of Isabelle download and run a standalone application that
exposes jEdit as a text editor on the surface. Thus there is
occasionally a tendency to apply the name ``jEdit'' to any of the
Isabelle Prover IDE aspects, without proper differentiation. When
discussing these PIDE building blocks in public forums, mailing lists,
or even scientific publications, it is particularly important to
distinguish Isabelle/ML versus Standard ML, Isabelle/Scala versus Scala,
Isabelle/jEdit versus jEdit.
The situation in Isabelle is very complex, but by mixing up names, it
becomes just one big bog that nobody understands anymore.
Makarius
Email Gateway (Aug 22 2022 at 12:41):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
I would like to add my grain of salt. At first, I thought the distinction between jEdit and Isabelle/jEdit was somewhat pedantic, but after years of being at the receiving end of bug reports and other comments about "metis" and "smt", and as an originator of material about it, I found that many misunderstandings are just waiting to happen.
To give one example: Metis (Joe Hurd's Metis ATP) is an automatic theorem prover for FOL that is designed to be sound and complete for that logic. "metis" is an Isabelle proof method that (1) translates HOL to FOL; (2) invokes Metis; (3) replays Metis inferences in Isabelle's kernel. Without appropriate context, statements like "metis is first-order" or "metis is higher-order" or "metis is buggy" are close to meaningless.
This having been said, I notice that nobody ever confused Nitpick and its backend Kodkod. I'm grateful I didn't call the tool Isabelle/Kodkod. ;)
Jasmin
Email Gateway (Aug 22 2022 at 12:41):From: Makarius <makarius@sketis.net>
Maybe that is because Kodkod is sufficiently unknown outside its Isabelle
context -- or maybe this just proves my ignorance about Kodkod.
The distinction of jEdit the text editor and Isabelle/jEdit the Prover IDE
is particularly important, because we need to do justice to both.
jEdit has its own profile as high-end text-editor, although its best of
time is probably over (after the founder left the project in 2006).
Thus it is particularly important to strengthen what is left of the jEdit
community, and not assimilate its name and declare it dead. It definitely
requires patience to get important changes through the jEdit tracker
system, but it usually works. It is better to have approx. 5 people still
maintaining jEdit on Sourceforge, instead of taking it over and doing it
by 1-2 people on the Isabelle side.
People who want to be lazy and use a short word, may call all Isabelle
tools just "Isabelle" and it will be usually right. So instead of "jEdit
checks a proof document", "Isabelle checks a proof document" will make
proper sense.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC