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

On 7/1/2013 2:44 PM, Makarius wrote:
The following versions lets you peek at the internal sequent (using postfix notation for the "antecedent" due to Larry); the slightly nested proof fragment ensures that the hypothetical facts actually show up in the result:

  note [[show_hyps]] ...
After closing the block, the internal sequent is exported into the enclosing context, discharging the assumptions and turning them into visible Pure rule structure using ==>.

Likewise, the initial "theorem assumes A and B shows C" gives you the exported rule "A ==> B ==> C", not its sequent.

As a user of Isabelle/Pure (and HOL as application within it), you should never encounter the hypotheses of the internal sequents, only the exported versions with explicit rule structure.


Thanks for the explanation, and the tips. It sounds complicated, and like we wouldn't want to be writing sequents that reflect accurately what's happening at the low level.

I'll be using "using [[show_hyps]]" to look at what the assumptions are for a given fact.

I'm interested in sequents notation as a means to add some concise, high-level, more-explicit notation to natural deduction notation, one of those notations being Fitch diagrams, but, in general, mixing sequent notation with natural deduction notation as shown by the docs linked to my last email.

So I start with the sequent conjunction introduction rule on page 38 of Larry's "Logic and Computation":

   The conjunction introduction rule becomes

   Gamma |- A  Delta |- B
   Gamma, Delta |- A & B

   The conclusion depends upon every assumption of A and of B.

I try to stay as true as I can, but staying true becomes relative to the Isar syntax available, and the fact that there are multiple ways to state a theorem.

I define <i(conjI,a,a> to be a list in the manner of Gamma and Delta. The onus is on the interested reader to figure out the details. After all, Gamma and Delta aren't exactly loaded with details. It turns that <i(conjI,a,a> also conveniently corresponds with the sequence of Isar commands apply(intro conjI), apply(assumption), by(assumption).

At least to myself, I can now say things like, "Please consider |- "[|A;B|] ==> A & B", <i(conjI,a,a>..."

Instead of, "Please consider the theorem "[|A;B|] ==> A & B" which is proved by the sequence of commands apply(intro conjI), apply(assumption), by(assumption).

That's the idea. The implementation will never be perfect, but it could be useful as a part of other things, at least for a while. Backward proofs are very concise, so this kind of things looks like it's matching up very nicely with short backwards proofs. Forward, structured proofs aren't that concise, so it wouldn't work for that. But it could work for proof steps within a structured proof, and a backward proof also can tell a person how to do a forward proof.

I attached a screen shot and a PDF showing my notation experiments.


Attachment: 130701_sequent_stuff.png
Description: PNG image

Attachment: 130701_sequent_stuff.pdf
Description: Adobe PDF document

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