Email Gateway (Aug 18 2022 at 10:40): Email Gateway (Aug 18 2022 at 10:40):From: "jwang whu.edu.cn (jwang)" <jwang@whu.edu.cn>
When Isabelle was run , the error
-"/usr/local/ProofGeneral/generic/proof-autoloads.elc was not compiled
in Emacs "was show.Why is it?
Email Gateway (Aug 18 2022 at 10:40):From: Lucas Cavalcante <lu_cavalcante_@hotmail.com>
It happened with me once, but im not sure i remember what to do.Try open the file Makefile found at /usr/local/ProofGeneral and edit all fields containing xEmacs, changing it for Emacs. Im not sure its gonna fix your problem, but i remember many bugs were fix when ive tried it, and your message is very familiar. Then you must recompile.You could be more precise about your Emacs version, and bla bla bla. =)I also tried some versions of Emacs where the little Belle didt work. Probably your version simply dont support Belle.Regards,Lucas Cavalcante> > When Isabelle was run , the error> -"/usr/local/ProofGeneral/generic/proof-autoloads.elc was not compiled> in Emacs "was show.Why is it? > > *************
Encontre o que procura com mais eficiência! Instale já a Barra de Ferramentas com Windows Desktop Search GRÁTIS!
http://desktop.msn.com.br/
Email Gateway (Aug 18 2022 at 10:43):From: "jwang whu.edu.cn (jwang)" <jwang@whu.edu.cn>
When I click "Isabelle--start isabelle " of the emacs menu =
,emacs show the error:unknow logic "HOL" ,no heap file found =
in:/root/isabelle/heaps/polyml_x86-linux,/usr/local/Isabele2005/=
heaps/polyml_x86-linux. Why?
another,there is not "Settings" command in "Isabelle" menu=
item of the emacs menu,why?
Email Gateway (Aug 18 2022 at 10:43):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
jwang whu.edu.cn (jwang) wrote:
The easiest thing is probably just to remove all the compiled lisp files
(the .elc files). The reason is probably that the lisp files have been
compiled for xemacs.
lucas
Email Gateway (Aug 18 2022 at 10:43):From: Lucas Cavalcante <thesupervisar@gmail.com>
You must build the logics. Try
"sudo ./usr/local/Isabelle/build -a"
Regards,
Lucas Cavalcante
Email Gateway (Aug 18 2022 at 10:48):From: David Aspinall <da@inf.ed.ac.uk>
[ Here's a copy of the email message I sent off list. Note the GNU
Emacs/XEmacs switch in latest (development) versions. Also note use of
EMACS= to avoid editing Makefile. - David ]
jwang whu.edu.cn (jwang) wrote:
http://proofgeneral.inf.ed.ac.uk/FAQ
Q. Proof General fails to load with an error message on start-up:
error: "File `.../ProofGeneral/generic/proof-autoloads.elc' was
not compiled in Emacs"
What's wrong?
A. We distribute .elcs for GNU Emacs, so you will have to delete
them and (optionally) recompile for XEmacs. Using the Makefile:
Use 'make clean' to remove all .elc files.
Use 'make compile' to recompile .elc files.
Check that the Makefile sets EMACS to your Emacs executable
(or simply run 'make compile EMACS=emacs')
Email Gateway (Aug 18 2022 at 11:42):From: "jwang whu.edu.cn (jwang)" <jwang@whu.edu.cn>
hello,
Apply(simp) or by auto often is used to prove some theorems automatically,so we can not see the process of simplication and we only see the result of simplication.How to show the simplification process in Proof-General ,for example the rewrite rules used by the current simplification? Is there the command?
thanks
Jean
Email Gateway (Aug 18 2022 at 11:42):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
jwang whu.edu.cn (jwang) wrote:
Select in ProofGeneral menu: Isabelle -> Settings -> Trace simplifier
Attention! Output is verbose.
Note that you may also do single-step rewrites using the "unfold" and
"subst" methods and the "unfolding" keyword. See Isar Reference manual.
Florian
florian.haftmann.vcf
signature.asc
Email Gateway (Aug 19 2022 at 10:31):From: Lawrence Paulson <lp15@cam.ac.uk>
You will find documentation at
http://isabelle.in.tum.de/documentation.html
Start with the first one. For greater depth, or for reference, you could look at the second one. The remaining documents are specialised.
Isabelle/HOL refers to the higher-order logic instance of Isabelle, which practically everybody uses; Isar refers to the structured proof language in which proofs are written.
Larry Paulson
Email Gateway (Aug 19 2022 at 10:31):From: Walther Neuper <wneuper@ist.tugraz.at>
Copy and paste from PDF to jEdit works nicely, if you observe some
details (which will disappear soon, as we all hope). As an example,
given isar-ref.pdf p.3 copy&paste into this simple mail program:
notepad
begin
Via explicit name:
assume a: A
note a
Via implicit name:
assume A
note this
Via literal proposition (unification with results from the proof text):
assume A
note ‘A‘
assume x . B x
note ‘B a‘
note ‘B b‘
end
If you copy&paste this into jEdit, you easily remove the syntax errors by:
(1) identifying comments
(2) replace inappropriate apostrophs
(3) enclose terms and types by "" in case they consist of more than 1
character and look for dropped special characters,
which finally results in
notepad
begin
-- "Via explicit name:" (1)
assume a: A
note a
-- "Via implicit name:" (1)
assume A
note this
-- "Via literal proposition (unification with results from the proof
text):" (1)
assume A
note A (2)
assume "⋀x. B x" (3)
note B a (2)
note B b (2)
end
Hope this helps,
Walther
Email Gateway (Aug 19 2022 at 10:31):From: "C. Diekmann" <diekmann@in.tum.de>
You can copy and paste the following example into jEdit:
theory Scratch
imports Main
begin
datatype 'a myList = Nil | Cons 'a "'a myList"
fun app :: "'a myList => 'a myList => 'a myList" where
"app Nil ys = ys" |
"app (Cons x xs) ys = Cons x (app xs ys)"
fun rev :: "'a myList => 'a myList" where
"rev Nil = Nil" |
"rev (Cons x xs) = app (rev xs) (Cons x Nil)"
value "rev (Cons True (Cons False Nil))"
value "rev (Cons a (Cons b Nil))"
lemma app_Nil2 [simp]: "app xs Nil = xs"
apply(induction xs)
apply(auto)
done
lemma app_assoc [simp]: "app (app xs ys) zs = app xs (app ys zs)"
apply(induction xs)
apply(auto)
done
lemma rev_app [simp]: "rev (app xs ys) = app (rev ys) (rev xs)"
apply(induction xs)
apply(auto)
done
theorem rev_rev [simp]: "rev (rev xs) = xs"
apply(induction xs)
apply(auto)
done
end
make sure that you save it in a file called Scratch.thy
Cheers
Cornelius
Email Gateway (Aug 19 2022 at 10:31):From: Makarius <makarius@sketis.net>
My example for first exposure is Isabelle2013/src/HOL/ex/Seq.thy -- you
can open that file directly in Isabelle/jEdit. That is just a totally
arbitrary entry point to a huge amount of Isabelle material.
Copy-paste from latex-generated PDF is indeed a black art. To avoid it,
you can look through Isabelle2013/src/Doc/ although that material might
occasionally look a bit odd in source form.
Makarius
Email Gateway (Aug 19 2022 at 10:32):From: Christoph LANGE <math.semantic.web@gmail.com>
Hi Liu Jing,
welcome!
2013-03-01 12:27 liujing657949251:
However, what make me confused is, what is the difference between Isabelle/HOL and Isabelle/Isar?
Isabelle/HOL refers to higher-order logic as it is implemented within
Isabelle's logical framework.
Isabelle/Isar is a textbook-style syntax for proofs on the
logic-independent level.
And what syntax should I learn, Isabelle/Isar syntax or Isabelle/HOL syntax?
Both: the reference manual (invoke with "isabelle doc isar-ref" from the
command line) lists the former as "outer syntax" and the latter as
"inner syntax". Terms are given in the "inner syntax", which depends on
the logic you are using, i.e. HOL in your case.
Please tell me the specific tutorial I should learn.
"isabelle doc prog-prove" is your friend.
Here, I am learning the simple example, which is in appendix. Am I right?
I didn't have time to look into this, but indeed this is similar to the
example discussed in prog-prove. Note however that this is in the
"apply tactics" proof style, not using Isar.
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 10:44):From: liujing657949251 <liujing657949251@126.com>
Dear all proof lovers:
I am really new to Isabelle. Recently I hope to learn HOL and try to use automatic therom prover. So I download the Isabelle2013. Now I hope to use Isabelle/jEdit in Windows OS for therom proving. However, what make me confused is, what is the difference between Isabelle/HOL and Isabelle/Isar? And what syntax should I learn, Isabelle/Isar syntax or Isabelle/HOL syntax? Please tell me the specific tutorial I should learn.
Here, I am learning the simple example, which is in appendix. Am I right?
Thanks very much.
Liu Jing
Seq.thy
Email Gateway (Aug 19 2022 at 10:47):From: liujing657949251 <liujing657949251@126.com>
Dear all proof lovers:
I am really new to Isabelle. I hope to use Isabell/HOL for proving. Recently I am reading prog-prove in Isabelle.doc. Until now I have read half of it, but I am so puzzled that I really don't know how to combine the little examples in doc with the Isabelle/jEdit.
They are just some fragments in one proof, I guess. So what should I do next?
By the way, if I use Isabelle/jEdit, do I need study Isar in chapter 4 of the doc?
My tutor told me to read some little examples, but I usually do not know why some lemmas should be proved first or some else. I do not know why I read the doc, but it doesn't help me to these question.
So I really hope to know how to learn.
Thank you very much!
Best wishes!
Liu Jing
Email Gateway (Aug 19 2022 at 10:47):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Le Sat, 16 Mar 2013 10:34:00 +0100, liujing657949251
<liujing657949251@126.com> a écrit:
Dear all proof lovers:
I am really new to Isabelle. I hope to use Isabell/HOL for proving.
Recently I am reading prog-prove in Isabelle.doc. Until now I have read
half of it, but I am so puzzled that I really don't know how to combine
the little examples in doc with the Isabelle/jEdit.
When you read the PDF doc, see an interesting sample and then want to give
it a try in Isabelle/jEdit, be aware the text you may copy/past from the
PDF to jEdit, may often be incorrect. Better learn Isar, to be able to
input the samples directly in Isabelle/jEdit.
By the way, if I use Isabelle/jEdit, do I need study Isar in chapter 4
of the doc?
Isar is one of the thing which make Isabelle so relevant. So yes, you
really have to study Isar. Isar is for readable and expressive proof text
(and what's more readable is more trustable), close enough to what you may
see in some logic or maths books, although the concrete notation differs a
lot, the structure is a lot similar. Learn Isar if you don't want to have
proof looking like machine code.
Last updated: Apr 30 2024 at 01:06 UTC