Re: [isabelle] Turnstile



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





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