# 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:
`
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:
`
notepad
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.*