*To*: Mark Adams <mark at proof-technologies.com>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Turnstile*From*: Makarius <makarius at sketis.net>*Date*: Tue, 7 Jun 2016 15:03:40 +0200*In-reply-to*: <060e1d65714a40aa7da9cc5e79c29866@webmail.names.co.uk>*References*: <060e1d65714a40aa7da9cc5e79c29866@webmail.names.co.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

On 07/06/16 01:51, Mark Adams wrote: > 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. See also chapter 2 about "Primitive logic" of the "implementation" manual. It explains the role of the Pure logic as framework for higher-order natural deduction in various object-logics, where HOL is the main example. The turnstile is there, but it belongs to the system infrastructure for local context management, and thus is hardly ever encountered in user tools and applications. > 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. Isabelle2005 is mainly of historic interest and no longer used in serious applications. It is remarkable in being the last version of Isabelle that still has remains from the 1990s, so it is possible to pretend that it resembles "other HOL systems". Note that the Isar concepts have already taken over the lead in Isabelle around 2002. Thus Isabelle2005 is just for prolonged nostalgy: one needs to go back to Isabelle98 to be authentic. Anyway, Q [P] is just Larry Paulson's notation for P |- Q. The context P is only informative when there is something wrong in the internal context management, so it is not printed by default, and when printed it is done in non-intrusive postfix notation. > But what about in more recent Isabelles? I know that there's no > read-eval-print-loop as such, and that in Isar scripts Isar is about structured proof *documents* or proof *texts*, not "scripts". It is important to use the proper terminology to get some idea how things work. Isabelle is a document-oriented proof composition tool, with timeless and stateless continuous checking. > "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. The 'theorem' command is more than an old-fashioned "goal" statement. It builds up a context and states conclusions from that context: the result is a Pure rule. This is ubiquitious in the Isabelle/Isar documentation, e.g. "isar-ref" or "implementation" manual. > 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. Here is an example for current Isabelle2016: theorem test: fixes x y z :: 'a assumes "x = y" and "y = z" shows "x = z" and "z = x" using assms by simp_all ML ‹ val thms = @{thms test}; map (fn thm => (Thm.hyps_of thm, Thm.prop_of thm)) thms; › The hyps are empty, because the result lives in a global context. Here is an example with a local context: context fixes x y z :: 'a assumes asms: "x = y" "y = z" begin theorem test': "x = z" and "z = x" using asms by simp_all ML ‹ val thms = @{thms test'}; map (fn thm => (Thm.hyps_of thm, Thm.prop_of thm)) thms; › end ML ‹ val thms = @{thms test'}; map (fn thm => (Thm.hyps_of thm, Thm.prop_of thm)) thms; › Hyps are potentially non-empty in the local context, and empty outside of it. Note that hyps record aspects of the proof in the thm object. This is also the reason why in recent years, hyps are hardly ever printed: this would lead to non-determinism, depending on the the accidental state of a future proof process that might fail or finish only later. Makarius

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

- Previous by Date: Re: [isabelle] Turnstile
- Next by Date: Re: [isabelle] Turnstile
- Previous by Thread: Re: [isabelle] Turnstile
- Next by Thread: [isabelle] how to use core to Isabelle to translate this code?
- 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