From: Joachim Breitner <breitner@kit.edu>
Hi isabelle devs,
not very severe, as it is caused by the user doing strange things, but
nevertheless you might want to fix it. Consider this theory:
theory Test
imports Main
begin
consts blubb :: bool
consts blah :: "'a ⇒ bool"
lemma x: "blubb ⟹ blah undefined" sorry
thm x
-- blubb ⟹ blah undefined [!]
class foo =
assumes "(UNIV :: 'a set) = (UNIV :: 'a set)"
begin
lemma x: "blah (undefined :: 'a)" sorry
end
instance nat :: foo apply default ..
thm x
-- blah undefined [!]
lemma "blubb ⟹ blah undefined"
--sledgehammer
by (metis )
For the last lemma, sledgehammer suggests "by (metis )". It seems that
it finds a proof using the first lemma named x, but cannot print a name
for it (the single space there is indeed what sledgehammer suggests).
I’m not sure if such overwriting of a lemma with class should be allowed
or not, but if it should be allowed then maybe sledgehammer should print
an error instead.
Greetings,
Joachim
signature.asc
From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Joachim,
just for terminology: there is no »overwriting« of anything, but a
shadowing of (unqualified) names. The situation is not so artificial,
similar things occur in the Isabelle distribution theories. However I
have no idea what is going wrong with sledgehammer here.
Cheers,
Florian
signature.asc
From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Joachim,
Thanks for the report! I'll look into this.
Jasmin
Last updated: Nov 21 2024 at 12:39 UTC