[isabelle] finite order allows maxima



Dear all,

in need (of a particular instance of) the following obvious fact:

lemma (in order) fin_max: "finite A ⟹ a ∈ A ⟹ ∃ s ∈ A. a ≤ s ∧  (∀ b ∈ A. s ≤ b ⟶ s = b)"

I have proved it for myself (see below). I wonder whether it can be obtained somehow more directly from Main.

Best regards

Stepan

proof (induct "card {b ∈ A. a < b}" arbitrary: a rule: nat_less_induct)
  case 1
  have IH: "⋀ x. x ∈ A ⟹ card {b ∈ A. x < b} < card {b ∈ A. a < b} ⟹ ∃s∈A. x ≤ s ∧ (∀b∈A. s ≤ b ⟶ s = b)"
    by (simp add: "1.hyps" ‹finite A›)
  then show ?case
  proof (cases "∀b∈A. a ≤ b ⟶ a = b")
    assume "∀b∈A. a ≤ b ⟶ a = b"
    thus ?thesis
      using ‹a ∈ A› by blast
  next
    assume "¬ (∀b∈A. a ≤ b ⟶ a = b)"
    then obtain a' where "a' ∈ A" and "a < a'"
      using local.antisym_conv1 by blast
    have "{b ∈ A. a' < b} ⊂ {b ∈ A. a < b}" (is "?Ma' ⊂  ?Ma")
    proof-
      have "a' ∈ ?Ma" and "a' ∉ ?Ma'" and "⋀ c. c ∈ ?Ma' ⟹ c ∈ ?Ma"
        using ‹a < a'› ‹a' ∈ A› by auto
      thus "?Ma' ⊂  ?Ma"
        by blast
    qed
    hence card: "card {b ∈ A. a' < b} < card {b ∈ A. a < b}"
      by (simp add: ‹finite A› psubset_card_mono)
    then obtain s where "s ∈ A" "a' ≤ s ∧ (∀b∈A. s ≤ b ⟶ s = b)"
      using IH[OF ‹a' ∈ A› card] by blast
    hence "a ≤ s ∧ (∀b∈A. s ≤ b ⟶ s = b)"
      using ‹a < a'› by auto
    thus ?thesis
      using ‹s ∈ A› by blast
  qed
qed


--
Tento e-mail byl zkontrolován na viry programem AVG.
http://www.avg.cz





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.