Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Bugreport: sledgehammer confused by lemmas wit...


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Nov 21 2024 at 12:39 UTC