# 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
• 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

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)

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