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.