Email Gateway (Nov 16 2022 at 19:31): Email Gateway (Nov 16 2022 at 19:31):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hello,
I noticed the following behavior: If I have a theorem /test///that uses
/sorry/, then /thm_oracles test/ should (and usually does) mention
/skip_proof/ to indicate that /sorry /was used. (And any other oracles
that were used.)
However, when using the Types_To_Sets, the use of /sorry/ can be hidden.
For example:
lemma test: ‹∃Rep Abs. type_definition Rep Abs {0::nat} ⟹ 1=2› sorry
lemmas test2 = test[cancel_type_definition]
thm_oracles test2( Only shows the oracle
/cancel_type_definition/ not /skip_proof///*) *
The likely reason for this is that
/Local_Typedef.cancel_type_definition/ takes the given theorem, checks
whether it is suitable to derive the desired theorem, and then throws it
away and only returns the desired theorem, created via oracle. The
result is that the original theorem and its proof are lost from the
proofterms.
This also has negative effects on a hypothetical external proofchecker
(or proof-translator). If the original proofterm was still available, it
could replay the proof of that and check externally whether
/cancel_type_definition///did the right thing. (For example, I am
working on a converter to Lean. In the calculus of constructions, what
Types_To_Sets does it most likely provable, but one does need the full
proof them.)
I see two possible fixes:
Extend the datatype of proofterms in Isabelle such that the
constructor /Proofterm.Oracle/ has an additional argument of type
/thm list/ that can track all theorems that went into the oracle.
This would be very nice because it would provide a general framework
for oracles that has assumptions. But it needs changing the format
of proofterms and is not a local change to Types_To_Sets.
Or, change Types_To_Sets only: Change the ML function
/cancel_type_definition_cterm/ /thm/ such that// when /thm/ is of
the form /∃Rep Abs. type_definition Rep Abs S ==> P/, it returns not
/P/ as it does now, but instead /(//∃Rep Abs. type_definition Rep
Abs S ==> P) ==> P/. And then change /cancel_type_definition/ so
that it discharges the assumption using the theorem that was input.
Logically, this is not "more sound" than what is done previously,
but it makes sure the original theorem is still to be found in the
proofterm (and /thm_oracles/ finds it.) If needed, I could help out
this fix.
Best wishes,
Dominique.
Last updated: Apr 27 2024 at 01:05 UTC