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

On Sat, 25 Aug 2012, Gottfried Barrow wrote:

I'm restating definitions and axioms as lemmas to check my typing.

For plain propositions you can also use the 'prop' command.

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)".

Proof methods lile auto, blast, fast, simp etc. only use what you declare explicitly as simp, intro, elim, dest, iff etc. Appendix A.4 of the isar-ref manual has a small table on that.

Sledgehammer is a bit different in going through the whole environment of named facts, but I reckon it won't find anything that does not have a name.

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 don't think it would be a good idea to introduce aliases for existing commands, especially very short ones. If you want to be fast in typing it is better to figure out some jEdit plugins that do the job. The Sidekick completion is already there; it has some plugin options to make it more aggressive. Other plugins like superabbrevs or yet unknown ones might do even more for you.

Line noise that is hacked into the computer is better not stored in the text you produce, unless you never want anyone to read it, maintain it, work with it elsewise.

Some people have come up with proof languages based on single letter commands, or even non-letter commands in the spirit of APL. I am fond of typing fast, but not of reading what looks like mouse droppings on the screen.


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