Florian Sextl (Feb 14 2023 at 07:53): Florian Sextl (Feb 14 2023 at 07:53):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.
Christian Pardillo Laursen (Feb 15 2023 at 15:26):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: Apr 28 2024 at 01:11 UTC