[isabelle] Bugreport: sledgehammer confused by lemmas without names

[Joachim Breitner]

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

--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.info.uni-karlsruhe.de/~breitner

[Florian Haftmann]

Hi Joachim,

> 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.

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

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

[Jasmin Blanchette]

Hi Joachim,

> 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.

Thanks for the report! I'll look into this.

Jasmin