Email Gateway (Aug 19 2022 at 08:23): Email Gateway (Aug 19 2022 at 08:23):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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?
Thanks,
GB
Email Gateway (Aug 19 2022 at 08:23):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 08:24):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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
Email Gateway (Aug 19 2022 at 08:25):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 19 2022 at 08:25):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 8/27/2012 4:21 PM, Makarius wrote:
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.
It was only about style. Some keywords I like or don't mind, but "oops"
and "sorry" don't quite fit in. It's not a problem because I don't think
I'll be postponing or abandoning proofs much in the documents I give
people, and I can strip some things out.
I was going to make a feeble appeal for freedom of keyword syntax,
similar to how we have freedom of notation with Isar, but I decided it's
the standardized keywords that give the language a common feel from
document to document. If you were to let people redefine keywords, there
would be major fragmentation of the language, which would make the
language harder to learn, and you would get blamed for it.
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.
Readability is huge with me, but it takes a lot of experimenting to find
the balance between using brevity for clarity, and using verboseness for
clarity.
Regards,
GB
Last updated: Apr 23 2024 at 16:19 UTC