Email Gateway (Aug 19 2022 at 15:37): Email Gateway (Aug 19 2022 at 15:37):From: Holden Lee <hl422@cam.ac.uk>
At a certain point in my proof I have the goal
m = 0 ==> N = 0 ==> card {l. l = [] ∧ (∀n∈set l. n = 0)} = Suc 0
OK, Isabelle failed to do this with auto so I inserted some statements
before:
have l: "{l::int list. l = [] ∧ (∀n∈set l. n = 0)} = {[]}"
by auto
hence l2: "card {l::int list. l = [] ∧ (∀n∈set l. n = 0)} = 1"
by auto
Now apply (insert l2, auto) gives
m = 0 ==>
N = 0 ==>
card {l. l = [] ∧ (∀n∈set l. n = 0)} = Suc 0 ==> card {l. l = [] ∧
(∀n∈set l. n = 0)} = Suc 0
The two statements are exactly the same (I checked the color of the
variables too, anyway they're all bound). try0 fails and sledgehammer
hangs. What gives?
-Holden
Email Gateway (Aug 19 2022 at 15:38):From: Holden Lee <hl422@cam.ac.uk>
Never mind: it turned out one of the statements is l::nat list instead.
Still, sneaky...
-Holden
Email Gateway (Aug 19 2022 at 15:38):From: Johannes Hölzl <hoelzl@in.tum.de>
Btw, you can proof this with the simplifier by:
simp cong: conj_cong
Then
{l. l = [] ∧ (∀n∈set l. n = 0)}
= with conj_cong
{l. l = [] ∧ (∀n∈set []. n = 0)}
=
{[]}
Last updated: Apr 20 2024 at 16:18 UTC