Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/ZF/AC/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 4 kB

Quelle WO1_AC.thy Sprache: Isabelle

(*  Title:      ZF/AC/WO1_AC.thy
    Author:     Krzysztof Grabczewski

The proofs of WO1 \<Longrightarrow> AC1 and WO1 \<Longrightarrow> AC10(n) for n >= 1

The latter proof is referred to as clear by the Rubins.
However it seems to be quite complicated.
The formal proof presented below is a mechanisation of the proof
by Lawrence C. Paulson which is the following:

Assume WO1.  Let s be a set of infinite sets.

Suppose x \<in> s.  Then x is equipollent to |x| (by WO1), an infinite cardinal
call it K.  Since K = K \<oplus> K = |K+K| (by InfCard_cdouble_eq) there is an
isomorphism h \<in> bij(K+K, x).  (Here + means disjoint sum.)

So there is a partition of x into 2-element sets, namely

        {{h(Inl(i)), h(Inr(i))} . i \<in> K}

So for all x \<in> s the desired partition exists.  By AC1 (which follows from WO1)
there exists a function f that chooses a partition for each x \<in> s.  Therefore we
have AC10(2).

*)

theory WO1_AC
imports AC_Equiv
begin

(* ********************************************************************** *)
(* WO1 \<Longrightarrow> AC1                                                            *)
(* ********************************************************************** *)

theorem WO1_AC1: "WO1 \ AC1"
by (unfold AC1_def WO1_def, fast elim!: ex_choice_fun)

(* ********************************************************************** *)
(* WO1 \<Longrightarrow> AC10(n) (n >= 1)                                               *)
(* ********************************************************************** *)

lemma lemma1: "\WO1; \B \ A. \C \ D(B). P(C,B)\ \ \f. \B \ A. P(f`B,B)"
  unfolding WO1_def
apply (erule_tac x = "\({{C \ D (B) . P (C,B) }. B \ A}) " in allE)
apply (erule exE, drule ex_choice_fun, fast)
apply (erule exE)
apply (rule_tac x = "\x \ A. f`{C \ D (x) . P (C,x) }" in exI)
apply (simp, blast dest!: apply_type [OF _ RepFunI])
done

lemma lemma2_1: "\\Finite(B); WO1\ \ |B| + |B| \ B"
  unfolding WO1_def
apply (rule eqpoll_trans)
prefer 2 apply (fast elim!: well_ord_cardinal_eqpoll)
apply (rule eqpoll_sym [THEN eqpoll_trans])
apply (fast elim!: well_ord_cardinal_eqpoll)
apply (drule spec [of _ B])
apply (clarify dest!: eqpoll_imp_Finite_iff [OF well_ord_cardinal_eqpoll])
apply (simp add: cadd_def [symmetric]
            eqpoll_refl InfCard_cdouble_eq Card_cardinal Inf_Card_is_InfCard)
done

lemma lemma2_2:
     "f \ bij(D+D, B) \ {{f`Inl(i), f`Inr(i)}. i \ D} \ Pow(Pow(B))"
by (fast elim!: bij_is_fun [THEN apply_type])

lemma lemma2_3:
        "f \ bij(D+D, B) \ pairwise_disjoint({{f`Inl(i), f`Inr(i)}. i \ D})"
  unfolding pairwise_disjoint_def
apply (blast dest: bij_is_inj [THEN inj_apply_equality])
done

lemma lemma2_4:
     "\f \ bij(D+D, B); 1\n\
      \<Longrightarrow> sets_of_size_between({{f`Inl(i), f`Inr(i)}. i \<in> D}, 2, succ(n))"
apply (simp (no_asm_simp) add: sets_of_size_between_def succ_def)
apply (blast intro!: cons_lepoll_cong
            intro: singleton_eqpoll_1 [THEN eqpoll_imp_lepoll]
                   le_imp_subset [THEN subset_imp_lepoll]  lepoll_trans
            dest: bij_is_inj [THEN inj_apply_equality] elim!: mem_irrefl)
done

lemma lemma2_5:
     "f \ bij(D+D, B) \ \({{f`Inl(i), f`Inr(i)}. i \ D})=B"
  unfolding bij_def surj_def
apply (fast elim!: inj_is_fun [THEN apply_type])
done

lemma lemma2:
     "\WO1; \Finite(B); 1\n\
      \<Longrightarrow> \<exists>C \<in> Pow(Pow(B)). pairwise_disjoint(C) \<and>
                sets_of_size_between(C, 2, succ(n)) \<and>
                \<Union>(C)=B"
apply (drule lemma2_1 [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]],
       assumption)
apply (blast intro!: lemma2_2 lemma2_3 lemma2_4 lemma2_5)
done

theorem WO1_AC10: "\WO1; 1\n\ \ AC10(n)"
  unfolding AC10_def
apply (fast intro!: lemma1 elim!: lemma2)
done

end

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.