Email Gateway (Aug 22 2022 at 18:58): Email Gateway (Aug 22 2022 at 18:58):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’m wondering about the behavior of unused_thms:
Consider the following Isabelle theory.
locale Foo =
fixes x :: int
assumes x3: "x < 3"
begin
lemma x4: "x < 4" using x3 by auto
lemma x5: "x < 5"
proof -
have "x < 4" by (rule x4)
also have "... < 5" by simp
finally show ?thesis .
qed
end
Clearly, x5 is not used at this point,
but x4 is used in the proof for x5.
Therefore, unused_thms reports correctly that only x5 is unused.
However, if I now add a global interpretation
global_interpretation Global_Foo: Foo 2
by (unfold_locales, auto)
then unused_thms now reports that both x4 and x5 (of Global_Foo.x4) are unused.
Is this intended, or can one prevent this behavior?
Cheers,
René
Email Gateway (Aug 22 2022 at 18:58):From: Tobias Nipkow <nipkow@in.tum.de>
My understanding is that unused_thms works only after a fashion. As you noticed.
I personally found it works well but locales may be a trouble spot.
Tobias
smime.p7s
Last updated: Apr 26 2024 at 16:20 UTC