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