Email Gateway (Aug 18 2022 at 13:42): Email Gateway (Aug 18 2022 at 13:42):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Patrick,
as a convenience, note that usually is it most appropriate to post
generic questions to the isabelle-users@cl.cam.ac.uk mailing list.
i'm coming with my mail to you because i have a problem and question
about Isabelle prover.i've read you books and papers about Isabelle's
Logic HOL, and old Introduction to Isabelle, but i don't understand :
You should definitely stay away from these two manuals ;-) which are
really outdated; the definite entrance point to get a little acquainted
with HOL is the "Tutorial on Isabelle/HOL".
1- About the installation, i've try to install Isabelle on my computer,
but it is so difficult to me.It is ask me "Emacs package" and when i
install Emacs package, it is look about Emacs version: i don't
undrestand why and how can i do to have a complete Isabelle's
installation? the OS on my computer is Ubuntu.
Hmmm... the GNU emacs coming with Ubuntu should be suitable (AFAIK at
least since version 8.04 -- you can find out your version using "less
/etc/issue" on the shell). A "sudo apt-get install emacs" should do the
job.
2- what is proofGeneral? Isawin? and what is their utility on Isabelle
process?
ProofGeneral is an extension to emacs which provides a simple user
interface to isabelle. The other possibility is to work on a tty
command line interface; I'm almost sure this is not what you want...
3- my next question is about HOL which is using in Isabelle.i don't know
if HOL is a Theorie or an logic using to developpe theories?
HOL is short for Higher-Order Logic and is one of the calculi the
Isabelle Distribution is equipped with; it is the most popular and of
Isabelle logics and sometimes even used synonymously, but be aware that
there are other implementations of HOL around.
To answer your question in particular: in Isabelle there is no
difference between theories which "implement" a logic and theories which
"build upon" an implemented logic -- technically they are the same. As
the tutorial says, for beginners the way to start is to use the existing
precompiled HOL session and base the first development on it:
theory Foo
imports Main
begin
...
4-my last preocupation is aboutTactic and Tactical, Goal and Subgoal
Dont't hesitate to ask further questions.
Hope this helps
Florian
signature.asc
Last updated: May 03 2024 at 12:27 UTC