Re: [isabelle] help



On 03/17/2013 08:25 PM, Yannick Duchêne (Hibou57) wrote:
Le Sat, 16 Mar 2013 10:34:00 +0100, liujing657949251 <liujing657949251 at 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.

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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.