Email Gateway (Aug 19 2022 at 14:39): Email Gateway (Aug 19 2022 at 14:39):From: "Farquhar, Colin I" <cif30@hw.ac.uk>
Dear Isabelle List,
I'm having some trouble getting the information I need from some proof terms. Specifically, I'm trying to find the sub-goals generated by each rule application. Take for example the lemma below:
lemma test: "A ⟶ A ⟶ A ∧ A"
apply (rule impI)
apply (rule impI)
apply (rule conjI)
apply assumption
apply assumption
done
The "full_prf" command gives the proof term thm.HOL.impI ⋅ ?A ⋅ ?A ⟶ ?A ∧ ?A ∙ (ΛH: ?A. thm.HOL.impI ⋅ ?A ⋅ ?A ∧ ?A ∙ (ΛHa: ?A. conjI ⋅ ?A ⋅ ?A ∙ H ∙ H)). While this does show what I'm looking for, I'm trying to present it in a different format. I have already written functions which look at the nuts and bolts of a proof term and extract information about the rules used, but I can't find the equivalent information about the goals. I've looked at the construction of full_prf and followed the chain of functions back a few steps, but haven't had much luck. I believe the information I'm looking for is used in the reconstruction of the proof, but haven't found it yet. Am I looking in the right place? If not, can anyone give me a nudge in the right direction?
Thanks for any help you can offer.
Colin Farquhar
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.
Last updated: Apr 27 2024 at 01:05 UTC