Email Gateway (Aug 18 2022 at 20:29): Email Gateway (Aug 18 2022 at 20:29):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Here's a template I created to look at how Isabelle decides to type and
parenthesize a formula in axiomatizations and definitions:
theorem show_info:
"(True) =
(True)"
by(auto)
thm show_info
Replace True with your formula. If you haven't imported "auto", then
replace "by(auto)" and "thm" with "oops". You might want these more
useful info commands above your working code to create different levels
of information overload:
--"INFO
BEGIN=================================================================="
--{notation Trueprop("Tr") notation "prop"("Pr")}
declare[[show_brackets=true]] declare[[show_sorts=false]]
declare[[names_long=false]] declare[[show_types=true]]
declare[[names_unique=true]] declare[[show_consts=true]]
--"INFO
END--------------------------------------------------------------------"
Giving advice is free, so I just go ahead attach iI.thy to this email. I
import it into my theories. It contains my default settings for the full
set of "declare" commands. Commented out are print and find commands, so
I don't have to look at isar-ref.pdf to remember what they are. There
are the jEdit command line options that control some printing modes.
There are also my default sledgehammer settings. I do this, and I get
all the provers:
sledgehammer supported_provers
I went back and briefly experimented with all the remote provers. I
eventually settled on these options:
sledgehammer_params [provers = "
e cvc3 metis smt spass z3 z3_tptp remote_e_sine remote_vampire
", slice=true, verbose=true, isar_proof=true, timeout=120]
The 120 second timeout solved the problem of not finding structured
proofs that I mentioned in another email.
Also, provers I wasn't using at the time of that email were "smt" and
"remote_e_sine". "smt" finds proofs just like "metis".
Following the instructions in the sledgehammer manual, I've used
"apply(auto)" prior to using sledgehammer. When I do that, proofs will
be found to finish the simplified goal by "smt" and "metis", along with
a structured proof to only finish the simplified goal.
"remote_e_sine" finds a short, structured proof that uses only the
necessary axioms. If I have the theorem after unnecessary axioms,
another structured proof is found which uses an unnecessary axiom, but
even after the unnecessary axioms, "remote_e_sine" finds the proof using
only the two necessary axioms.
I also figured out the simple fact (maybe from reading the sledgehammer
manual) that I can click on any of the highlighted text in the output
window, and it'll replace "sledgehammer" with that proof.
If I choose a "smt" or "metis" proof that's offered, it does indeed
finish the proof. If I choose a structured proof, it complains about an
unbound schematic variable, as shown in the attached screen shot.
Regards,
GB
unbound_sch_var_error.png
iI.thy
Email Gateway (Aug 18 2022 at 20:29):From: Lars Noschinski <noschinl@in.tum.de>
When you are using jEdit, then I suggest using Ctrl+Hover to get the
full names and types of constants, without making the term hardly
readable due to all the annotations.
Email Gateway (Aug 18 2022 at 20:30):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Gottfried,
Isar proofs are experimental, as mentioned in the Sledgehammer manual. We have a student currently working on improving them, and he will look into these kinds of issues. Hopefully the next Isabelle release will feature a revamped Isar proof output in Sledgehammer.
Other aspects of Sledgehammer should be more polished. If you run into any bugs with it, please send me an email so I can look into this. (I might otherwise miss bug reports when they hide in lengthy emails on public mailing lists.)
Regards,
Jasmin
Email Gateway (Aug 18 2022 at 20:30):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Okay. If I don't know how to use introduction and elimination rules to
replace metis steps, after the initial cheap thrill of a structured
proof, it's all kind of the same (though not really, if I'm looking for
some hints), and a single-line metis proof takes up less space anyway.
I should get lots of preliminary cheap thrills from using nitpick and
sledgehammer, while being able to delay the point at which I have to
start thinking, where I get an occasional (or frequent), unexpected
result that enlightens me.
Regards,
GB
Email Gateway (Aug 18 2022 at 20:30):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Alright, it's like Perl, where there's more than one way to do
something, except the Ctrl+Hover way also labels each of the component
part with additional information, such as axiom, theory fact, local
fact, bound variable, free variable, etc.
Thanks,
GB
Last updated: Apr 27 2024 at 01:05 UTC