Email Gateway (Aug 19 2022 at 10:48): Email Gateway (Aug 19 2022 at 10:48):From: Colin Farquhar <cif30@hw.ac.uk>
Hi,
I’m currently trying to do some experiments using proof terms in Isabelle,
but I’m having some difficulty getting it to work. I’m working in the
HOL-Proofs heap. To illustrate, if I have the simple lemma:
theory ProofTermTest
imports Main
begin
lemma t: "A ∧ B --> A"
apply (rule impI)
apply (elim conjE)
apply assumption
done
Then
prf t
full_prf t
gives the error message “reconstruct_proof: minimal proof object”.
I also had a go at the ML level, but
ML{*
val prf = Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of @{thm
"t"};));
Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf);
*}
only prints `?’.
Does anyone have any experience working with proof terms and if so, can you
point out where I’m going wrong?
Thanks,
Colin Farquhar
PhD Student
Dependable Systems Group
School of Mathematical and Computer Sciences
Heriot-Watt University
Sunday Times Scottish University of the Year 2011-2013
Top in the UK for student experience
Fourth university in the UK and top in Scotland (National Student Survey 2012)
We invite research leaders and ambitious early career researchers to
join us in leading and driving research in key inter-disciplinary themes.
Please see www.hw.ac.uk/researchleaders for further information and how
to apply.
Heriot-Watt University is a Scottish charity
registered under charity number SC000278.
Email Gateway (Aug 19 2022 at 10:48):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Colin,
you must both
a) base your work in HOL-Proofs rather than HOL
b) and, at the beginning of your theory, tun proof recording on using
ML_val {* proofs := 2 *}
See the section on proof terms in the (old) Isabelle reference manual
available by
isabelle doc ref
Hope this helps,
Florian
signature.asc
Last updated: Apr 25 2024 at 20:15 UTC