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



On Sat, 29 Jun 2013, Gottfried Barrow wrote:

I'm trying to make some connections between logic vocabulary and Isar.

From https://en.wikipedia.org/wiki/Sequent, I get the sentence

  On the other hand an empty antecedent is assumed to be true, i.e.,
  |- Sigma means that Sigma follows without any assumptions...

I'm trying to determine the right connection between sequent assumptions and the meta-logic operator "==>", and how to restate a proved theorem with Isar, THM, to accurately represent the sequent ( |- THM).

Say I have a sequent (A, B |- C), then I'm wanting to say that the following Isar is a correct translation of that sequent:

theorem
 assumes A and B
 shows C

For any theorem THM I've proved in Isar, I'm trying to trivially restate it as a sequent, |- THM, but have the restatement have some meaning, not be an exact restatement.

Isabelle/Pure has sequents in the manner of Natural Deduction (with single conclusion) built-in, but they only serve foundational and implementation purposes.


When you state

  theorem
    assumes A and B
    show C

you are claiming A, B |- C. The proof may refer to A and B in that context as local theorems.

Alternatively, you can play with local contexts and sequents derived within them more directly (and without global goals getting in the way) using Isar notepad:

  notepad
  begin
    {
      assume A and B
      have C sorry
    }
  end

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:

notepad
begin
  note [[show_hyps]]
  {
    assume A and B
    then have C apply - sorry
    thm this  -- "C [A, B]"
  }
  note `A ⟹ B ⟹ C`
end

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.


	Makarius


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