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

*To*: cl-isabelle-users at lists.cam.ac.uk
*Subject*: Re: [isabelle] How do I write the sequent |- P in Isar using theorem
*From*: Gottfried Barrow <gottfried.barrow at gmx.com>
*Date*: Mon, 01 Jul 2013 02:02:32 -0500
*In-reply-to*: <51CF3A8E.7000805@gmx.com>
*References*: <51CE8C40.6020808@gmx.com> <51CF3A8E.7000805@gmx.com>
*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

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.*