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,
In , 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.
When I talk about "the most elementary possible inferences", I am
thinking of something like Metamath, which is apparently based
entirely on simple substitution rules. In other words, emphatically not
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and