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

• To: isabelle-users <isabelle-users at cl.cam.ac.uk>
• Subject: [isabelle] How do I write the sequent |- P in Isar using theorem
• From: Gottfried Barrow <gottfried.barrow at gmx.com>
• Date: Sat, 29 Jun 2013 02:26:56 -0500
• User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

```Hi,

I'm trying to make some connections between logic vocabulary and Isar.

From https://en.wikipedia.org/wiki/Sequent, I get the sentence

On the other hand an empty antecedent is assumed to be true, i.e.,
|- Sigma means that Sigma follows without any assumptions...

```
I'm trying to determine the right connection between sequent assumptions and the meta-logic operator "==>", and how to restate a proved theorem with Isar, THM, to accurately represent the sequent ( |- THM).
```
```
Say I have a sequent (A, B |- C), then I'm wanting to say that the following Isar is a correct translation of that sequent:
```
theorem
assumes A and B
shows C

```
For any theorem THM I've proved in Isar, I'm trying to trivially restate it as a sequent, |- THM, but have the restatement have some meaning, not be an exact restatement.
```
For example, say I prove this:

theorem iffIi_1:
assumes "A --> B" and "B --> A"
shows "A =  B"
<proof>

```
I'd like to restate the theorem using the identifier iffIi_1, but as I said above, I don't know how, so I restate it like this:
```
theorem iffIi_2:
"(A --> B) ==> (B --> A) ==> (A = B)"
by(rule iffIi)

```
Here, I want to say that this represents the sequent ( |- "(A --> B) ==> (B --> A) ==> (A = B)" ).
```
```
I've been thinking that the statements of iffIi_1 and iffIi_2 must be exactly the same, but now I try the following and it doesn't work:
```
theorem
assumes "A --> B" and "B --> A"
shows "A = B"
by(rule iffIi)

```
I had started thinking `assumes "A --> B" and "B --> A"` was synonymous with "(A --> B) ==> (B --> A)".
```
Regards,
GB

```

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