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

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

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:
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:
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.


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