Re: [isabelle] Turnstile

On Di, 2016-06-07 at 00:51 +0100, Mark Adams wrote:
> Dear list,
> Is there an equivalent to turnstile in Isabelle?  In good old
> mathematics and in other HOL systems, the turnstile (|-) has two roles:
> to indicate that a theorem has been proved, and to separate any
> assumptions of the theorem from its conclusion.
> In Isabelle2005, if you return a theorem in the read-eval-print-loop,
> then if it has one assumption 'P' and conclusion 'Q' then it gets
> printed as "Q [P]" (if the flag for showing hypotheses is set), but just
> as "Q" if there are no assumptions, and so this corresponds to the
> second role.
> But what about in more recent Isabelles?  I know that there's no
> read-eval-print-loop as such, and that in Isar scripts you write
> "theorem" before a formula, which is a bit like the first role but not
> quite because until the proof is complete it states the intention that
> the formula will be proved rather than that it has been proved.  Are
> there ways of displaying lists of theorems, and if so how are these
> presented?  I note that the printer for "Q [P]" is still there in the
> Isabelle Pure source.  If anyone could shed any light on all of this
> then I'd be most grateful.

The hypothesis are used in Isabelle merely internally, and the
standard-user should not see them. Theorems are presented as
meta-implications "P1==>...==>Pn==>Q", or, syntax-sugared "[| P1;...;Pn
|] ==> Q". This is also the way they are printed. 
In Isar, you can use the "thm" command to print (a list of) theorems.

To state a theorem, you can either use meta-implications, or the
"long-goal" format:
lemma foo:
  assumes P1 and ... and Pn
  shows Q

By the very design of Isabelle, every theorem has been proved (or has a
pending future proof attached [Makarius, correct me if I'm wrong
here ;)])


> Mark.

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