Re: [isabelle] How do I write the sequent |- P in Isar using theorem
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] How do I write the sequent |- P in Isar using theorem
- From: Gottfried Barrow <gottfried.barrow at gmx.com>
- Date: Mon, 01 Jul 2013 02:02:32 -0500
- In-reply-to: <51CF3A8E.email@example.com>
- References: <51CE8C40.firstname.lastname@example.org> <51CF3A8E.email@example.com>
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0
On 6/29/2013 2:50 PM, Gottfried Barrow wrote:
On 6/29/2013 2:26 AM, Gottfried Barrow wrote:
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
I'm trying to make some connections between logic vocabulary and Isar.
The right search words are "sequent style natural deduction", or
something similar, and throw in an "isabelle" to find what's specific to
Isabelle, or ":
(Rules of the Game link)
(Natural Deduction in ISABELLE: Single-step proofs based on Sequent
(Natural Deduction with Gentzen Sequents)
(Section 2.2 A sequent calculus for natural deduction)
I think HOL4 notation corrupted my mind with things like this: "|- !f g
x. (f o g) x = f(g x)"
And then from a 1990 Isabelle user's manual it says:
"Theorems and axioms can be regarded as rules with no premises, so
let us speak just of rules."
So if we can speak of theorems as things without premises, I should be
able to combine sequent notation with Isar syntax, like writing
|- "A ==> B ==> (A & B)", ConjI
and get away with it, so I can emphasize the things I want to emphasize,
where because by(intro conjI) is the single proof command needed, then
ConjI must be qualified to representative the premises needed to prove
"A ==> B ==> (A & B)".
You gotta have those basic logic books to keep you from going astray too
far, when you have to answer most of your own questions. I finally found
what must have been vaguely in my mind:
"Remark 1.12 Indeed, this example indicates that we may transform
any proof of /phi1, phi2, ..., phi_n |- psi/ in such a way into a
proof of the theorem
|- phi1 --> (phi2 -->..."
I think I saw someone from the HOL4 group say something like that on
this list over a year ago, probably Ramana.
This archive was generated by a fusion of
Pipermail (Mailman edition) and