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