Re: [isabelle] How do I write the sequent |- P in Isar using theorem



On 6/29/2013 2:50 PM, Gottfried Barrow wrote:
On 6/29/2013 2:26 AM, Gottfried Barrow wrote:
I'm trying to make some connections between logic vocabulary and Isar.
Basically, I'm trying to sync up sequents notation with equivalent Isar syntax being used with Isabelle/HOL. I wouldn't care about sequents, but sequents are something that's resorted to a lot in many logic textbooks.

The right search words are "sequent style natural deduction", or something similar, and throw in an "isabelle" to find what's specific to Isabelle, or ":

(Isabelle specific)
http://www.inf.ed.ac.uk/teaching/courses/ar/slides/index.html

(Rules of the Game link)
http://www.cogsys.wiai.uni-bamberg.de/teaching/ss07/hs_rc/

(Natural Deduction in ISABELLE: Single-step proofs based on Sequent Notation link)
http://www.gdi.uni-bamberg.de/personnel/aguado/publications.htm

(Natural Deduction with Gentzen Sequents)
http://www.ling.ohio-state.edu/~scott/teaching/2012/winter/280/

(Section 2.2 A sequent calculus for natural deduction)
http://books.google.com/books/about/Logic_and_Computation.html?id=8cyTbKWDKqgC

I think HOL4 notation corrupted my mind with things like this: "|- !f g x. (f o g) x = f(g x)"

And then from a 1990 Isabelle user's manual it says:

   "Theorems and axioms can be regarded as rules with no premises, so
   let us speak just of rules."

So if we can speak of theorems as things without premises, I should be able to combine sequent notation with Isar syntax, like writing

   |- "A ==> B ==> (A & B)", ConjI

and get away with it, so I can emphasize the things I want to emphasize, where because by(intro conjI) is the single proof command needed, then ConjI must be qualified to representative the premises needed to prove "A ==> B ==> (A & B)".

You gotta have those basic logic books to keep you from going astray too far, when you have to answer most of your own questions. I finally found what must have been vaguely in my mind:

   "Remark 1.12 Indeed, this example indicates that we may transform
   any proof of /phi1, phi2, ..., phi_n |- psi/ in such a way into a
   proof of the theorem
   |- phi1 --> (phi2 -->..."

http://www.cs.bham.ac.uk/research/projects/lics/

I think I saw someone from the HOL4 group say something like that on this list over a year ago, probably Ramana.

Regards,
GB





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