# 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.*