Email Gateway (Aug 17 2022 at 13:46): Email Gateway (Aug 17 2022 at 13:46):From: Lawrence Paulson <lp15@cam.ac.uk>
Schematic variables can be replaced by any well-formed term, and
there are no guarantees that this will be done in an elegant or
minimal way. You get the first proof that was found. It would be nice
if blast allowed backtracking over different proofs, but to obtain
reasonable performance it's necessary to prune the search space.
Larry Paulson
Email Gateway (Aug 17 2022 at 13:46):From: Tim Freeman <tim@fungible.com>
I downloaded Isabelle2005 just now following the installation
instructions at
http://www.cl.cam.ac.uk/Research/HVG/Isabelle/installation.html
and if I start my "ToyList.thy" file with
theory ToyList
imports PreList
begin
lemma bug: "?A & ?B & ?XYZZY \<longrightarrow> ?XYZZY" by blast
and go to the end and press control-c control-enter, I see this in the
response window:
lemma bug: ?A & ?B & gcd (?m, ?n) dvd ?n --> gcd (?m, ?n) dvd ?n
I had expected it to say:
lemma bug: ?A & ?B & ?XYZZY --> ?XYZZY
I was surprised by the intruction of the "gcd" operator. If I change
"blast" to "auto", I do get the output I expected.
Email Gateway (Aug 17 2022 at 13:46):From: Peter <views@gmx.de>
Tim Freeman wrote:
I'm getting similiar results, with Main imported instead of PreList:
theory Scratch
imports Main
begin
lemma bug: "?A & ?B & ?XYZZY --> ?XYZZY" by blast
outputs:
lemma bug: ?A & ?B & [] \<in> lists ?Aa --> [] \<in> lists ?Aa
Email Gateway (Aug 17 2022 at 13:46):From: Tjark Weber <tjark.weber@gmx.de>
Peter,
as Larry already wrote, schematic variables can be replaced by any well-formed
term. If you find the above behavior surprising, maybe you just want to
input your lemma using free variables (without the question marks), e.g.
lemma foo: "A & B & XYZZY --> XYZZY" by blast
NB: Isabelle issues a warning "Goal statement contains unbound schematic
variable(s)" for the "bug" lemma.
Best,
Tjark
Last updated: May 03 2024 at 08:18 UTC