[isabelle] Bugreport: sledgehammer confused by lemmas without names

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
        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)"
          lemma x: "blah (undefined :: 'a)" sorry
        instance nat :: foo apply default ..
        thm x
        -- blah undefined  [!]
        lemma "blubb ⟹ blah undefined" 
          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.


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.