Email Gateway (Aug 23 2022 at 08:47): Email Gateway (Aug 23 2022 at 08:47):From: "David E. Narvaez" <den9562@rit.edu>
Hi,
Consider the following toy lemma:
--8<--
definition abset :: "nat set"
where "abset ≡ {0, 1}"
lemma ballbug:
fixes f :: "nat ⇒ bool"
assumes foo: "∀a∈abset. ∀b∈abset. (f a) ∨ (f b)"
shows False
proof-
have abset0: "0 ∈ abset" by (eval)
have abset1: "1 ∈ abset" by (eval)
from foo have "∀b∈abset. (f 0) ∨ (f b)" using abset0 ..
from foo have "(f 0) ∨ (f 1)" using abset0 abset1 by (auto)
from foo have "(f 0) ∨ (f 1)" using abset0 abset1
proof
-->8--
You can see that in
from foo have "∀b∈abset. (f 0) ∨ (f b)" using abset0 ..
the ball ∀a∈abset was successfully eliminated by abset0. You can also see that
both balls were eliminated by auto in
from foo have "(f 0) ∨ (f 1)" using abset0 abset1 by (auto)
But when I try to prove the last line, I get
Failed to apply initial proof method:
using this:
∀a∈abset. ∀b∈abset. f a ∨ f b
0 ∈ abset
1 ∈ abset
goal (1 subgoal):
Also, this would not work
from foo have "(f 0) ∨ (f 1)" using abset0 abset1 ..
So I wonder: what are the proof and the .. commands doing that they can
successfully deal with one ball but not with two consecutive applications of
whatever rule they are using? And what rule (or rules) are they using in the
successful cases? (It would be good in general to have a way to ask Isar what
it has done in one step, this has been brought up before in this list[0].) If
you could give me an example in an apply-style proof of what rules are being
applied and how, that would be great.
Thanks in advance for your help.
[0] https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-August/
msg00166.html
Last updated: Nov 21 2024 at 12:39 UTC