Re: [isabelle] Export of proofs from Isabelle in "fully-expanded" form



On Thu, 12 Jan 2006, Robin Green wrote:

A question about transforming Isabelle proofs into really elementary, long-winded form:

In [2], I found a tantalising hint which suggests that this feature became available in Isabelle 99:

See Stefan Berghofer's thesis for a slightly more up-to-date report on proof terms (based on lambda calculus) for Isabelle/Pure. The Introduction and chapter 2 should give you some idea how this looks like.

  Stefan Berghofer. Proofs, Programs and Executable Specifications in
  Higher Order Logic. Ph.D. thesis, Institut für Informatik, Technische
  Universität München, 2003.
  http://www4.in.tum.de/~berghofe/papers/phd.pdf


When I talk about "the most elementary possible inferences", I am thinking of something like Metamath[1], which is apparently based entirely on simple substitution rules. In other words, emphatically not (non-trivial) tactics.

I would consider the Metamath format slightly low-level, with adhoc handling of bound variable scopes; lambda calculus provides a more abstract and clean notion of variable binding and substitution.

Also note that the actual primary proof format for Isabelle is that of the Isar proof language, which admits writing proofs in a human-readable fashion. Needless to say, everything will end up as a primitive internal proof object eventually, but normally these are getting too large to inspect them directly. This is why humans would normally stay at the level of Isabelle/Isar proof documents -- printed in LaTeX/PDF.


	Makarius


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