# Re: [isabelle] Are unnamed theorems used by automatic methods or Sledgehammer?

On 8/25/2012 3:45 AM, Makarius wrote:

On Fri, 24 Aug 2012, Gottfried Barrow wrote:

Suppose I have an unnamed theorem:
theorem "<some formula that's true>" by(auto)

`Are automatic proof methods, or is Sledgehammer going to try and use
``that theorem to prove anything?
`

`When it is really unnamed and has not other attributes to declare it
``to the context, the system will not store the theorem anywhere. So
``other tools like sledgehammer should not be able to find it.
`

Makarius,

`Thanks. I'm restating definitions and axioms as lemmas to check my
``typing. I also might want to prove a theorem 10 additional ways. For
``performance, I don't want any of that to be used by Sledgehammer, or a
``proof method like "by(auto)".
`

`I restate a definition with `lemma "<some formula>" sorry`. I choose
``"sorry" over "oops" simply as a matter of style.
`

`I try to find a code style that looks good without hiding or converting
``things in LaTeX.
`

`If it's a 5 minute job, and you have 5 minutes to spare, can you give me
``some ML in a "ML{*...*}" that creates an outer-syntax-command synonym
``for "theorem"? It would be nice to have a two character synonym for
``"theorem".
`

`If you're taking Isar feature requests, it would be nice to be able to,
``in general, define outer-syntax-command synonyms.
`
I found these lines of code:
FILE: more_thm.ML
signature THM =
...
val corollaryK: string
FILE: isar_syn.ML
val _ = gen_theorem false Thm.corollaryK;
val _ = gen_theorem true Thm.corollaryK;
FILE: thm_deps.ML

` member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK]
``(Thm.legacy_get_kind th) andalso
`
I don't know enough ML to know how to use that information.
Regards,
GB

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