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

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



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