Email Gateway (Sep 30 2021 at 09:48): Email Gateway (Sep 30 2021 at 09:48):From: Simon Roßkopf <rosskops@in.tum.de>
Hello,
when working with proof terms I noticed some curious behavior in
combination with rule attributes (e.g. OF, rule_format...). Consider the
following (contrived) example (In session HOL-Proofs):
lemma l[OF TrueI]: "True ⟹ P"
by (simp add: P_def) (* theorem l: P *)
full_prf l (* l ∙ TrueI *)
The proof of l seems to depend on l itself, but closer inspection showed
that in this l hides another proof for the lemma before the application
of the rule attribute. This intermediate result has, as far as I know,
no name or way to refer to it. I am therefore confused why the proofterm
uses the name of the eventual result for it, instead of for example an
empty name field.
Running Stefan Berghofer's proofchecker seems to support this being
unintended, as it complains about a "Duplicate use of theorem name"
(final/intermediate result) for the lemma l. That it is finds a proof
for the intermediate result, but from the name would expect one for the
final result.
Is this intended behavior and if yes, is it possible to identify such
"intermediate" named steps in a proofterm?
Best regards,
Simon
Last updated: Jul 15 2022 at 23:21 UTC