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

On 6/29/2013 2:26 AM, Gottfried Barrow wrote:

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

`This is where a textbook would come in handy: "Sequents as Implemented
``in Isabelle/HOL using Isar Syntax, Along with Many Tedious Examples,
``Both Trivial and Advanced, and Likewise for Natural Deduction as
``Implemented in Isar, for the Working Unprofessional."
`

`It would say, "Here's a sequent, and here's its equivalent form using
``Isar in Isabelle/HOL. Here's another sequent, but this sequent is
``difficult to state in Isar. Here's yet another sequent, and you really
``can't express this sequent in Isar in Isabelle/HOL."
`

`There's a 3 page section in isar-ref.pdf titled "The sequent caclulus",
``page 201, which I guess will help me eventually figure it out.
`
It says,
For certain proofs in classical logic, it can not be called natural.
The sequent calculus, a generalization of natural deduction, is
easier to automate.

`If Isabelle/HOL is completely formulated as natural deduction, then I
``guess every Isar statement of Isabelle/HOL can be expressed as a sequent.
`

`But then on page 203, there's a section titled "Simulating sequents by
``natural deduction", and it says,
`
Isabelle can represent sequents directly, as in the object-logic LK.
But natural deduction is easier to work with, and most object-logics
employ it. Fortunately, we can simulate the sequent P1, ..., Pm |-
Q1, ..., Qn by the Isabelle formula P1 ==> ... ==> Pm ==> ~Q2 ==>
... ==> ~Qn ==> Q1 where the order of the assumptions and the choice
of Q1 are arbitrary.

`Here, the fact that the word "simulating" is being used, and the use of
``the phrase "Fortunately, we can simulate the sequent...", makes me think
``that I can't simulate certain sequents in Isabelle/HOL using Isar.
`

`Maybe the discussion on page 202 explaining the sequent analogue to the
``(-->I) will help me figure it out. It gives the rule as
`
P, Lambda |- Delta, Q
--------------------------------- (-->R)
Lambda |- Delta, P --> Q

`For any proved HOL theorem THM, I'm trying to figure out how to restate
``THM as a sequent which requires no assumptions, and do it using Isar.
`
I start with something trivial:
theorem TrueTrue:
"True"
by(rule TrueI)

`There doesn't appear to be any assumptions in TrueTrue, but there must
``be some assumptions because TrueTrue has to be proved by TrueI, which is
``not an exact restatement of TrueI, where TrueI resorts to using the
``axiom refl:
`
lemma TrueI: "True"
unfolding True_def by (rule refl)

`If TrueTrue is a theorem, then I say, "Surely I can express it as a
``sequent. But what is the sequent, and what is it in Isar?"
`

`I make an attempt to answer the question, but I use the sequent rule
``(-->R) as a template.
`

`I'm tempted to say the sequent is "|- True", but I say it's "|- True,
``TrueI". In Isar I say the sequent is
`
theorem TrueTrue_Restate:
"True"
by(rule TrueTrue)

`So I decide that TrueTrue_Restate is the sequent "|- True, TrueTrue",
``with there being a subtle difference between "|- True, TrueTrue" and "|-
``True, TrueI", with the difference being that TrueTrue_Restate is
``TrueTrue proving itself, which means it's using no assumptions. Using
``theorem names, it would be "|- TrueTrue, TrueI" versus "|- TrueTrue,
``TrueTrue_Restate" == "|- TrueTrue".
`

`But I'm jumping through hoops to try and fit sequent notation with Isar
``syntax. I'm trying to use "theorem" along with "by" or "proof" to prove
``that a theorem THM is a sequent of the form "|- P", meaning that it
``doesn't require any assumptions to be true. If I can do that, it's
``important. If I can't, it's not important.
`
Regards,
GB

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