
Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/ZF/AC/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 23 kB

Quelle WO6_WO1.thy

Sprache: Isabelle

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

Proofs needed to state that formulations WO1,...,WO6 are all equivalent.
The only hard one is WO6 ==> WO1.

Every proof (except WO6 ==> WO1 and WO1 ==> WO2) are described as "clear"
by Rubin & Rubin (page 2).
They refer reader to a book by Gödel to see the proof WO1 ==> WO2.
Fortunately order types made this proof also very easy.
*)

theory WO6_WO1
imports Cardinal_aux
begin

(* Auxiliary definitions used in proof *)
definition
  NN  :: "i ==> i"  where
    "NN(y) ≡ {m ∈ nat. ∃a. ∃f. Ord(a) ∧ domain(f)=a ∧
                        (∪b∧ (∀b< m)}"

definition
  uu  :: "[i, i, i, i] ==> i"  where
    "uu(f, beta, gamma, delta) ≡ (f`beta * f`gamma) ∩ f`delta"

(** Definitions for case 1 **)
definition
  vv1 :: "[i, i, i] ==> i"  where
     "vv1(f,m,b) ≡
           let g = μ g. (∃d. Ord(d) ∧ (domain(uu(f,b,g,d)) ≠ 0 ∧
                                 domain(uu(f,b,g,d)) < m));
               d = μ d. domain(uu(f,b,g,d)) ≠ 0 ∧
                            domain(uu(f,b,g,d)) < m
           in if f`b ≠ 0 then domain(uu(f,b,g,d)) else 0"

definition
  ww1 :: "[i, i, i] ==> i"  where
     "ww1(f,m,b) ≡ f`b - vv1(f,m,b)"

definition
  gg1 :: "[i, i, i] ==> i"  where
     "gg1(f,a,m) ≡ λb ∈ a++a. if b

(** Definitions for case 2 **)
definition
  vv2 :: "[i, i, i, i] ==> i"  where
     "vv2(f,b,g,s) ≡
           if f`g ≠ 0 then {uu(f, b, g, μ d. uu(f,b,g,d) ≠ 0)`s} else 0"

definition
  ww2 :: "[i, i, i, i] ==> i"  where
     "ww2(f,b,g,s) ≡ f`g - vv2(f,b,g,s)"

definition
  gg2 :: "[i, i, i, i] ==> i"  where
     "gg2(f,a,b,s) ≡
              λg ∈ a++a. if g

lemma WO2_WO3: "WO2 ==> WO3"
by (unfold WO2_def WO3_def, fast)

(* ********************************************************************** *)

lemma WO3_WO1: "WO3 ==> WO1"
  unfolding eqpoll_def WO1_def WO3_def
apply (intro allI)
apply (drule_tac x=A in spec)
apply (blast intro: bij_is_inj well_ord_rvimage
                    well_ord_Memrel [THEN well_ord_subset])
done

(* ********************************************************************** *)

lemma WO1_WO2: "WO1 ==> WO2"
  unfolding eqpoll_def WO1_def WO2_def
apply (blast intro!: Ord_ordertype ordermap_bij)
done

(* ********************************************************************** *)

lemma lam_sets: "f ∈ A->B ==> (λx ∈ A. {f`x}): A -> {{b}. b ∈ B}"
by (fast intro!: lam_type apply_type)

lemma surj_imp_eq': "f ∈ surj(A,B) ==> (∪a ∈ A. {f`a}) = B"
  unfolding surj_def
apply (fast elim!: apply_type)
done

lemma surj_imp_eq: "[f ∈ surj(A,B); Ord(A)] ==> (∪a
by (fast dest!: surj_imp_eq' intro!: ltI elim!: ltE)

lemma WO1_WO4: "WO1 ==> WO4(1)"
  unfolding WO1_def WO4_def
apply (rule allI)
apply (erule_tac x = A in allE)
apply (erule exE)
apply (intro exI conjI)
apply (erule Ord_ordertype)
apply (erule ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, THEN lam_sets, THEN domain_of_fun])
apply (simp_all add: singleton_eqpoll_1 eqpoll_imp_lepoll Ord_ordertype
       ordermap_bij [THEN bij_converse_bij, THEN bij_is_surj, THEN surj_imp_eq]
       ltD)
done

(* ********************************************************************** *)

lemma WO4_mono: "[m≤n; WO4(m)] ==> WO4(n)"
  unfolding WO4_def
apply (blast dest!: spec intro: lepoll_trans [OF _ le_imp_lepoll])
done

(* ********************************************************************** *)

lemma WO4_WO5: "[m ∈ nat; 1≤m; WO4(m)] ==> WO5"
by (unfold WO4_def WO5_def, blast)

(* ********************************************************************** *)

lemma WO5_WO6: "WO5 ==> WO6"
by (unfold WO4_def WO5_def WO6_def, blast)

(* **********************************************************************
The proof of "WO6 ==> WO1". Simplified by L C Paulson.

From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin,
pages 2-5
************************************************************************* *)

lemma lt_oadd_odiff_disj:
      "[k < i++j; Ord(i); Ord(j)]
       ==> k < i | (¬ k∧ k = i ++ (k--i) ∧ (k--i)
apply (rule_tac i = k and j = i in Ord_linear2)
prefer 4
   apply (drule odiff_lt_mono2, assumption)
   apply (simp add: oadd_odiff_inverse odiff_oadd_inverse)
apply (auto elim!: lt_Ord)
done

(* ********************************************************************** *)
(* The most complicated part of the proof - lemma ii - p. 2-4             *)
(* ********************************************************************** *)

(* ********************************************************************** *)
(* some properties of relation uu(beta, gamma, delta) - p. 2              *)
(* ********************************************************************** *)

lemma domain_uu_subset: "domain(uu(f,b,g,d)) ⊆ f`b"
by (unfold uu_def, blast)

lemma quant_domain_uu_lepoll_m:
     "∀b< m ==> ∀b∀g∀d< m"
by (blast intro: domain_uu_subset [THEN subset_imp_lepoll] lepoll_trans)

lemma uu_subset1: "uu(f,b,g,d) ⊆ f`b * f`g"
by (unfold uu_def, blast)

lemma uu_subset2: "uu(f,b,g,d) ⊆ f`d"
by (unfold uu_def, blast)

lemma uu_lepoll_m: "[∀b< m; d] ==> uu(f,b,g,d) < m"
by (blast intro: uu_subset2 [THEN subset_imp_lepoll] lepoll_trans)

(* ********************************************************************** *)
(* Two cases for lemma ii                                                 *)
(* ********************************************************************** *)
lemma cases:
     "∀b∀g∀d< m
      ==> (∀b≠ 0 ⟶
                  (∃g∃d≠ 0 ∧ u(f,b,g,d) ≺ m))
        | (∃b≠ 0 ∧ (∀g∀d≠ 0 ⟶
                                        u(f,b,g,d) ≈ m))"
  unfolding lesspoll_def
apply (blast del: equalityI)
done

(* ********************************************************************** *)
(* Lemmas used in both cases                                              *)
(* ********************************************************************** *)
lemma UN_oadd: "Ord(a) ==> (∪b∪b∪ C(a++b))"
by (blast intro: ltI lt_oadd1 oadd_lt_mono2 dest!: lt_oadd_disj)

(* ********************************************************************** *)
(* Case 1: lemmas                                                        *)
(* ********************************************************************** *)

lemma vv1_subset: "vv1(f,m,b) ⊆ f`b"
by (simp add: vv1_def Let_def domain_uu_subset)

(* ********************************************************************** *)
(* Case 1: Union of images is the whole "y"                              *)
(* ********************************************************************** *)
lemma UN_gg1_eq:
  "[Ord(a); m ∈ nat] ==> (∪b∪b
by (simp add: gg1_def UN_oadd lt_oadd1 oadd_le_self [THEN le_imp_not_lt]
              lt_Ord odiff_oadd_inverse ltD vv1_subset [THEN Diff_partition]
              ww1_def)

lemma domain_gg1: "domain(gg1(f,a,m)) = a++a"
by (simp add: lam_funtype [THEN domain_of_fun] gg1_def)

(* ********************************************************************** *)
(* every value of defined function is less than or equipollent to m       *)
(* ********************************************************************** *)
lemma nested_LeastI:
     "[P(a, b); Ord(a); Ord(b);
         Least_a = (μ a. ∃x. Ord(x) ∧ P(a, x))]
      ==> P(Least_a, μ b. P(Least_a, b))"
apply (erule ssubst)
apply (rule_tac Q = "λz. P (z, μ b. P (z, b))" in LeastI2)
apply (fast elim!: LeastI)+
done

lemmas nested_Least_instance =
       nested_LeastI [of "λg d. domain(uu(f,b,g,d)) ≠ 0 ∧
                                domain(uu(f,b,g,d)) < m"] for f b m

lemma gg1_lepoll_m:
     "[Ord(a); m ∈ nat;
         ∀b≠0 ⟶
             (∃g∃d≠ 0 ∧
                          domain(uu(f,b,g,d)) < m);
         ∀b< succ(m); b]
      ==> gg1(f,a,m)`b < m"
apply (simp add: gg1_def empty_lepollI)
apply (safe dest!: lt_oadd_odiff_disj)
(*Case b<a   \<in> show vv1(f,m,b) \<lesssim> m *)
apply (simp add: vv1_def Let_def empty_lepollI)
apply (fast intro: nested_Least_instance [THEN conjunct2]
             elim!: lt_Ord)
(*Case a\<le>b \<in> show ww1(f,m,b--a) \<lesssim> m *)
apply (simp add: ww1_def empty_lepollI)
apply (case_tac "f` (b--a) = 0", simp add: empty_lepollI)
apply (rule Diff_lepoll, blast)
apply (rule vv1_subset)
apply (drule ospec [THEN mp], assumption+)
apply (elim oexE conjE)
apply (simp add: vv1_def Let_def lt_Ord nested_Least_instance [THEN conjunct1])
done

(* ********************************************************************** *)
(* Case 2: lemmas                                                        *)
(* ********************************************************************** *)

(* ********************************************************************** *)
(* Case 2: vv2_subset                                                    *)
(* ********************************************************************** *)

lemma ex_d_uu_not_empty:
     "[b≠0; f`g≠0;
         y*y ⊆ y; (∪b]
      ==> ∃d≠ 0"
by (unfold uu_def, blast)

lemma uu_not_empty:
     "[b≠0; f`g≠0; y*y ⊆ y; (∪b]
      ==> uu(f,b,g,μ d. (uu(f,b,g,d) ≠ 0)) ≠ 0"
apply (drule ex_d_uu_not_empty, assumption+)
apply (fast elim!: LeastI lt_Ord)
done

lemma not_empty_rel_imp_domain: "[r ⊆ A*B; r≠0] ==> domain(r)≠0"
by blast

lemma Least_uu_not_empty_lt_a:
     "[b≠0; f`g≠0; y*y ⊆ y; (∪b]
      ==> (μ d. uu(f,b,g,d) ≠ 0) < a"
apply (erule ex_d_uu_not_empty [THEN oexE], assumption+)
apply (blast intro: Least_le [THEN lt_trans1] lt_Ord)
done

lemma subset_Diff_sing: "[B ⊆ A; a∉B] ==> B ⊆ A-{a}"
by blast

(*Could this be proved more directly?*)
lemma supset_lepoll_imp_eq:
     "[A < m; m < B; B ⊆ A; m ∈ nat] ==> A=B"
apply (erule natE)
apply (fast dest!: lepoll_0_is_0 intro!: equalityI)
apply (safe intro!: equalityI)
apply (rule ccontr)
apply (rule succ_lepoll_natE)
apply (erule lepoll_trans)
apply (rule lepoll_trans)
  apply (erule subset_Diff_sing [THEN subset_imp_lepoll], assumption)
apply (rule Diff_sing_lepoll, assumption+)
done

lemma uu_Least_is_fun:
     "[∀g∀d≠0 ⟶
          domain(uu(f, b, g, d)) ≈ succ(m);
          ∀b< succ(m); y*y ⊆ y;
          (∪b
          f`b≠0; f`g≠0; m ∈ nat; s ∈ f`b]
      ==> uu(f, b, g, μ d. uu(f,b,g,d)≠0) ∈ f`b -> f`g"
apply (drule_tac x2=g in ospec [THEN ospec, THEN mp])
   apply (rule_tac [3] not_empty_rel_imp_domain [OF uu_subset1 uu_not_empty])
        apply (rule_tac [2] Least_uu_not_empty_lt_a, assumption+)
apply (rule rel_is_fun)
    apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll])
   apply (erule uu_lepoll_m)
   apply (rule Least_uu_not_empty_lt_a, assumption+)
apply (rule uu_subset1)
apply (rule supset_lepoll_imp_eq [OF _ eqpoll_sym [THEN eqpoll_imp_lepoll]])
apply (fast intro!: domain_uu_subset)+
done

lemma vv2_subset:
     "[∀g∀d≠0 ⟶
                       domain(uu(f, b, g, d)) ≈ succ(m);
         ∀b< succ(m); y*y ⊆ y;
         (∪b∈ nat; s ∈ f`b]
      ==> vv2(f,b,g,s) ⊆ f`g"
apply (simp add: vv2_def)
apply (blast intro: uu_Least_is_fun [THEN apply_type])
done

(* ********************************************************************** *)
(* Case 2: Union of images is the whole "y"                              *)
(* ********************************************************************** *)
lemma UN_gg2_eq:
     "[∀g∀d≠ 0 ⟶
               domain(uu(f,b,g,d)) ≈ succ(m);
         ∀b< succ(m); y*y ⊆ y;
         (∪b∈ nat; s ∈ f`b; b]
      ==> (∪g
  unfolding gg2_def
apply (drule sym)
apply (simp add: ltD UN_oadd  oadd_le_self [THEN le_imp_not_lt]
                 lt_Ord odiff_oadd_inverse ww2_def
                 vv2_subset [THEN Diff_partition])
done

lemma domain_gg2: "domain(gg2(f,a,b,s)) = a++a"
by (simp add: lam_funtype [THEN domain_of_fun] gg2_def)

(* ********************************************************************** *)
(* every value of defined function is less than or equipollent to m       *)
(* ********************************************************************** *)

lemma vv2_lepoll: "[m ∈ nat; m≠0] ==> vv2(f,b,g,s) < m"
  unfolding vv2_def
apply (simp add: empty_lepollI)
apply (fast dest!: le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_0_is_0]
       intro!: singleton_eqpoll_1 [THEN eqpoll_imp_lepoll, THEN lepoll_trans]
               not_lt_imp_le [THEN le_imp_subset, THEN subset_imp_lepoll]
               nat_into_Ord nat_1I)
done

lemma ww2_lepoll:
    "[∀b< succ(m); g∈ nat; vv2(f,b,g,d) ⊆ f`g]
     ==> ww2(f,b,g,d) < m"
  unfolding ww2_def
apply (case_tac "f`g = 0")
apply (simp add: empty_lepollI)
apply (drule ospec, assumption)
apply (rule Diff_lepoll, assumption+)
apply (simp add: vv2_def not_emptyI)
done

lemma gg2_lepoll_m:
     "[∀g∀d≠ 0 ⟶
                      domain(uu(f,b,g,d)) ≈ succ(m);
         ∀b< succ(m); y*y ⊆ y;
         (∪b∈ f`b; m ∈ nat; m≠ 0; g]
      ==> gg2(f,a,b,s) ` g < m"
apply (simp add: gg2_def empty_lepollI)
apply (safe elim!: lt_Ord2 dest!: lt_oadd_odiff_disj)
apply (simp add: vv2_lepoll)
apply (simp add: ww2_lepoll vv2_subset)
done

(* ********************************************************************** *)
(* lemma ii                                                               *)
(* ********************************************************************** *)
lemma lemma_ii: "[succ(m) ∈ NN(y); y*y ⊆ y; m ∈ nat; m≠0] ==> m ∈ NN(y)"
  unfolding NN_def
apply (elim CollectE exE conjE)
apply (rule quant_domain_uu_lepoll_m [THEN cases, THEN disjE], assumption)
(* case 1 *)
apply (simp add: lesspoll_succ_iff)
apply (rule_tac x = "a++a" in exI)
apply (fast intro!: Ord_oadd domain_gg1 UN_gg1_eq gg1_lepoll_m)
(* case 2 *)
apply (elim oexE conjE)
apply (rule_tac A = "f`B" for B in not_emptyE, assumption)
apply (rule CollectI)
apply (erule succ_natD)
apply (rule_tac x = "a++a" in exI)
apply (rule_tac x = "gg2 (f,a,b,x) " in exI)
apply (simp add: Ord_oadd domain_gg2 UN_gg2_eq gg2_lepoll_m)
done

(* ********************************************************************** *)
(* lemma iv - p. 4:                                                       *)
(* For every set x there is a set y such that   x \<union> (y * y) \<subseteq> y         *)
(* ********************************************************************** *)

(* The leading \<forall>-quantifier looks odd but makes the proofs shorter
   (used only in the following two lemmas)                          *)

lemma z_n_subset_z_succ_n:
     "∀n ∈ nat. rec(n, x, λk r. r ∪ r*r) ⊆ rec(succ(n), x, λk r. r ∪ r*r)"
by (fast intro: rec_succ [THEN ssubst])

lemma le_subsets:
     "[∀n ∈ nat. f(n)<=f(succ(n)); n≤m; n ∈ nat; m ∈ nat]
      ==> f(n)<=f(m)"
apply (erule_tac P = "n≤m" in rev_mp)
apply (rule_tac P = "λz. n≤z ⟶ f (n) ⊆ f (z) " in nat_induct)
apply (auto simp add: le_iff)
done

lemma le_imp_rec_subset:
     "[n≤m; m ∈ nat]
      ==> rec(n, x, λk r. r ∪ r*r) ⊆ rec(m, x, λk r. r ∪ r*r)"
apply (rule z_n_subset_z_succ_n [THEN le_subsets])
apply (blast intro: lt_nat_in_nat)+
done

lemma lemma_iv: "∃y. x ∪ y*y ⊆ y"
apply (rule_tac x = "∪n ∈ nat. rec (n, x, λk r. r ∪ r*r) " in exI)
apply safe
apply (rule nat_0I [THEN UN_I], simp)
apply (rule_tac a = "succ (n ∪ na) " in UN_I)
apply (erule Un_nat_type [THEN nat_succI], assumption)
apply (auto intro: le_imp_rec_subset [THEN subsetD]
            intro!: Un_upper1_le Un_upper2_le Un_nat_type
            elim!: nat_into_Ord)
done

(* ********************************************************************** *)
(* Rubin & Rubin wrote,                                                   *)
(* "It follows from (ii) and mathematical induction that if y*y \<subseteq> y then *)
(* y can be well-ordered"                                                 *)

(* In fact we have to prove                                               *)
(*      * WO6 \<Longrightarrow> NN(y) \<noteq> 0                                              *)
(*      * reverse induction which lets us infer that 1 \<in> NN(y)            *)
(*      * 1 \<in> NN(y) \<Longrightarrow> y can be well-ordered                             *)
(* ********************************************************************** *)

(* ********************************************************************** *)
(*      WO6 \<Longrightarrow> NN(y) \<noteq> 0                                                *)
(* ********************************************************************** *)

lemma WO6_imp_NN_not_empty: "WO6 ==> NN(y) ≠ 0"
by (unfold WO6_def NN_def, clarify, blast)

(* ********************************************************************** *)
(*      1 \<in> NN(y) \<Longrightarrow> y can be well-ordered                               *)
(* ********************************************************************** *)

lemma lemma1:
     "[(∪b∈ y; ∀b< 1; Ord(a)] ==> ∃c
by (fast elim!: lepoll_1_is_sing)

lemma lemma2:
     "[(∪b∈ y; ∀b< 1; Ord(a)]
      ==> f` (μ i. f`i = {x}) = {x}"
apply (drule lemma1, assumption+)
apply (fast elim!: lt_Ord intro: LeastI)
done

lemma NN_imp_ex_inj: "1 ∈ NN(y) ==> ∃a f. Ord(a) ∧ f ∈ inj(y, a)"
  unfolding NN_def
apply (elim CollectE exE conjE)
apply (rule_tac x = a in exI)
apply (rule_tac x = "λx ∈ y. μ i. f`i = {x}" in exI)
apply (rule conjI, assumption)
apply (rule_tac d = "λi. THE x. x ∈ f`i" in lam_injective)
apply (drule lemma1, assumption+)
apply (fast elim!: Least_le [THEN lt_trans1, THEN ltD] lt_Ord)
apply (rule lemma2 [THEN ssubst], assumption+, blast)
done

lemma y_well_ord: "[y*y ⊆ y; 1 ∈ NN(y)] ==> ∃r. well_ord(y, r)"
apply (drule NN_imp_ex_inj)
apply (fast elim!: well_ord_rvimage [OF _ well_ord_Memrel])
done

(* ********************************************************************** *)
(*      reverse induction which lets us infer that 1 \<in> NN(y)              *)
(* ********************************************************************** *)

lemma rev_induct_lemma [rule_format]:
     "[n ∈ nat; ∧m. [m ∈ nat; m≠0; P(succ(m))] ==> P(m)]
      ==> n≠0 ⟶ P(n) ⟶ P(1)"
by (erule nat_induct, blast+)

lemma rev_induct:
     "[n ∈ nat; P(n); n≠0;
         ∧m. [m ∈ nat; m≠0; P(succ(m))] ==> P(m)]
      ==> P(1)"
by (rule rev_induct_lemma, blast+)

lemma NN_into_nat: "n ∈ NN(y) ==> n ∈ nat"
by (simp add: NN_def)

lemma lemma3: "[n ∈ NN(y); y*y ⊆ y; n≠0] ==> 1 ∈ NN(y)"
apply (rule rev_induct [OF NN_into_nat], assumption+)
apply (rule lemma_ii, assumption+)
done

(* ********************************************************************** *)
(* Main theorem "WO6 \<Longrightarrow> WO1"                                             *)
(* ********************************************************************** *)

(* another helpful lemma *)
lemma NN_y_0: "0 ∈ NN(y) ==> y=0"
  unfolding NN_def
apply (fast intro!: equalityI dest!: lepoll_0_is_0 elim: subst)
done

lemma WO6_imp_WO1: "WO6 ==> WO1"
  unfolding WO1_def
apply (rule allI)
apply (case_tac "A=0")
apply (fast intro!: well_ord_Memrel nat_0I [THEN nat_into_Ord])
apply (rule_tac x = A in lemma_iv [elim_format])
apply (erule exE)
apply (drule WO6_imp_NN_not_empty)
apply (erule Un_subset_iff [THEN iffD1, THEN conjE])
apply (erule_tac A = "NN (y) " in not_emptyE)
apply (frule y_well_ord)
apply (fast intro!: lemma3 dest!: NN_y_0 elim!: not_emptyE)
apply (fast elim: well_ord_subset)
done

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet am 2026-04-26) ¤

*© Formatika GbR, Deutschland

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.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.