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

```On Sat, 29 Jun 2013, Gottfried Barrow wrote:

```
```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.
```
```
Isabelle/Pure has sequents in the manner of Natural Deduction (with single conclusion) built-in, but they only serve foundational and implementation purposes.
```

When you state

theorem
assumes A and B
show C

```
you are claiming A, B |- C. The proof may refer to A and B in that context as local theorems.
```
```
Alternatively, you can play with local contexts and sequents derived within them more directly (and without global goals getting in the way) using Isar notepad:
```
begin
{
assume A and B
have C sorry
}
end

```
The following versions lets you peek at the internal sequent (using postfix notation for the "antecedent" due to Larry); the slightly nested proof fragment ensures that the hypothetical facts actually show up in the result:
```
begin
note [[show_hyps]]
{
assume A and B
then have C apply - sorry
thm this  -- "C [A, B]"
}
note `A ⟹ B ⟹ C`
end

```
After closing the block, the internal sequent is exported into the enclosing context, discharging the assumptions and turning them into visible Pure rule structure using ==>.
```
```
Likewise, the initial "theorem assumes A and B shows C" gives you the exported rule "A ==> B ==> C", not its sequent.
```

```
As a user of Isabelle/Pure (and HOL as application within it), you should never encounter the hypotheses of the internal sequents, only the exported versions with explicit rule structure.
```

Makarius```

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