Email Gateway (Aug 19 2022 at 09:00): Email Gateway (Aug 19 2022 at 09:00):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
Email Gateway (Aug 19 2022 at 09:00):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
Email Gateway (Aug 19 2022 at 09:00):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Joachim,
Thanks for the report! I'll look into this.
Jasmin
Last updated: Apr 19 2024 at 04:17 UTC