Re: [isabelle] help



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

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ SePublica Workshop @ ESWC 2013.  Montpellier, France, 26-30 May.
  Deadline 4 Mar; http://sepublica.mywikipaper.org
→ Intelligent Computer Mathematics, 7–12 Jul, Bath, UK; Deadline 8 Mar
  http://cicm-conference.org/2013/
→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
  3–5 April 2013, Exeter, UK.  3 Hands-on Tutorials on Economics
  http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/





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