I want to prove the following lemma:

```
lemma "⟦finite A; P {}⟧ ⟹ ∃E⊆A. P E ∧ (∄T. T⊆A ∧ P T ∧ E ⊂ T)"
```

The intuitive proof would be that the subset lattice of A is finite and therefore we can always find a locally maximal subset satisfying P (as at least the empty set satisfies it). It would only be a local maximum as P does not necessarily hold for A.

Unfortunately, I have no idea how to translate this proof idea to Isabelle. Is there any kind of "induction" on finite subset lattices available?

I'd expect to have the empty set as the bottom element as the base case and some kind of induction step going a step up in the lattice.

You can use fact Finite_Set.finite_has_maximal, which they prove using induction rule finite_psubset_induct. Here's a quick proof of your lemma:

```
lemma "⟦finite A; P {}⟧ ⟹ ∃E⊆A. P E ∧ (∄T. T⊆A ∧ P T ∧ E ⊂ T)"
proof -
assume *: "finite A" "P {}"
have "∃m∈{x. x ⊆ A ∧ P x}. ∀b∈{x. x ⊆ A ∧ P x}. m ⊆ b ⟶ m = b"
apply (rule finite_has_maximal)
using * by auto
then show ?thesis
by (simp add: psubset_eq, metis)
qed
```

Thank you very much, that's exactly what I was looking for!

I didn't expect the proof to be that straightforward, but finite_has_maximal and finite_psubset_induct are really helpful.

Last updated: Dec 07 2023 at 20:16 UTC