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