*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Bugreport: sledgehammer confused by lemmas without names*From*: Joachim Breitner <breitner at kit.edu>*Date*: Thu, 18 Oct 2012 11:18:21 +0200

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

**Follow-Ups**:**Re: [isabelle] Bugreport: sledgehammer confused by lemmas without names***From:*Florian Haftmann

**Re: [isabelle] Bugreport: sledgehammer confused by lemmas without names***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] Status of "eval" method
- Next by Date: Re: [isabelle] Bugreport: sledgehammer confused by lemmas without names
- Previous by Thread: [isabelle] ICTAC 2014: call for organisers
- Next by Thread: Re: [isabelle] Bugreport: sledgehammer confused by lemmas without names
- Cl-isabelle-users October 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list