Email Gateway (Aug 22 2022 at 20:21): Email Gateway (Aug 22 2022 at 20:21):From: Dominique Unruh <unruh@ut.ee>
Hi,
when Isabelle generates proofterms, those contain the all steps
necessary for replaying the proof, except when class instantiations
(OFCLASS(...)) are involved. In this case, a proofterm contains the
constructor OfClass(T,c) (OfClass of typ * class) to represent the proof
of the theorem OFCLASS(T,c). This is justified because the OFCLASS(T,c)
theorem was proven using an instance proof. However, I could not find
out where I can access the proofterm of instance proof. How can one
retrieve that proofterm (within Isabelle/ML) so that a complete replay
of a proofterm is possible?
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 20:21):From: Makarius <makarius@sketis.net>
The original proofterm implementation from around 2000 by Stefan
Berghofer did not support type class proofs at all: the applications did
not require it.
In March 2010, I've revisited that together with Stefan, but we did not
get it fully through: some rudiments of it are still in Isabelle2019,
but it requires more work to finish.
Included is a minimal example. If you open it in Isabelle/jEdit together
with $ISABELLE_HOME/src/Pure/ROOT.ML you can follow the definitions in
Isabelle/ML.
Incidently, I am presently in the process to revisit all that. So there
is some chance that Isabelle2020 will be more complete in that respect.
(Right now I am facing certain performance problems that are to be
expected whenever the old proofterm can is opened again.)
Makarius
Scratch.thy
Last updated: Apr 26 2024 at 08:19 UTC