I still struggle with this example, card {{0, 1, 2}}
is 1 whereby nitpick reports 2 ...
lemma
assumes ‹card (P :: nat set set) ≥ 2›
‹disjoint P›
shows ‹⋂P = {}›
proof -
have ‹finite P›
using assms(1) le_simps(2) by force
then obtain a b P' where
H: ‹a ≠ b› ‹a ∉ P'› ‹b ∉ P'› and
P: ‹P = {a,b} ∪ P'› and
fin: ‹finite P'›
using assms apply (induction P rule: finite_induct)
subgoal by auto
subgoal premises p for a A
using p apply auto
by (induction A rule: finite_induct)
(auto, metis, metis)
done
show ?thesis
using fin H assms(2) unfolding P
apply (induction P' rule: finite_induct)
apply (auto simp: disjoint_def)
done
qed
so it holds actually, it is really a wrong counterexample
(the proof can clearly be improved… auto, metis, metis
is a don't do that)
(and the obtain a b should actually come from two case distinctions… but the default case distinction is missing the a ∉ P'
in the assumption)
Thank you! Actually, the counterexample drove me crazy. Very hard for me to distinguish and identify the issue. Highly appreciate your support here :-)
Robert Soeldner has marked this topic as resolved.
Usually when you see "potentially spurious counterexample", the counterexample is really spurious
Note that disjoint_family_on is often better than disjoint
I.e. working with indexed families of sets instead of sets of sets
Last updated: Nov 11 2024 at 04:22 UTC