*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Turnstile*From*: Peter Lammich <lammich at in.tum.de>*Date*: Tue, 07 Jun 2016 08:53:55 +0200*In-reply-to*: <060e1d65714a40aa7da9cc5e79c29866@webmail.names.co.uk>*References*: <060e1d65714a40aa7da9cc5e79c29866@webmail.names.co.uk>

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 ;)]) -- Peter > > Mark.

**Follow-Ups**:**Re: [isabelle] Turnstile***From:*Makarius

**References**:**[isabelle] Turnstile***From:*Mark Adams

- Previous by Date: [isabelle] core-to-isabelle installation error
- Next by Date: Re: [isabelle] Turnstile
- Previous by Thread: [isabelle] Turnstile
- Next by Thread: Re: [isabelle] Turnstile
- Cl-isabelle-users June 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list