Quelle AC16_WO4.thy

Sprache: Isabelle

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

The proof of AC16(n, k) ==> WO4(n-k)

Tidied (using locales) by LCP
*)

theory AC16_WO4
imports AC16_lemmas
begin

(* ********************************************************************** *)
(* The case of finite set                                                 *)
(* ********************************************************************** *)

lemma lemma1:
     "[Finite(A); 0∈ nat]
      ==> ∃a f. Ord(a) ∧ domain(f) = a ∧
                (∪b∧ (∀b< m)"
  unfolding Finite_def
apply (erule bexE)
apply (drule eqpoll_sym [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]])
apply (erule exE)
apply (rule_tac x = n in exI)
apply (rule_tac x = "λi ∈ n. {f`i}" in exI)
apply (simp add: ltD bij_def surj_def)
apply (fast intro!: ltI nat_into_Ord lam_funtype [THEN domain_of_fun]
               singleton_eqpoll_1 [THEN eqpoll_imp_lepoll, THEN lepoll_trans]
                    nat_1_lepoll_iff [THEN iffD2]
          elim!: apply_type ltE)
done

(* ********************************************************************** *)
(* The case of infinite set                                               *)
(* ********************************************************************** *)

(* well_ord(x,r) \<Longrightarrow> well_ord({{y,z}. y \<in> x}, Something(x,z))  **)
lemmas well_ord_paired = paired_bij [THEN bij_is_inj, THEN well_ord_rvimage]

lemma lepoll_trans1: "[A < B; ¬ A < C] ==> ¬ B < C"
by (blast intro: lepoll_trans)

(* ********************************************************************** *)
(* There exists a well ordered set y such that ...                        *)
(* ********************************************************************** *)

lemmas lepoll_paired = paired_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll]

lemma lemma2: "∃y R. well_ord(y,R) ∧ x ∩ y = 0 ∧ ¬y < z ∧ ¬Finite(y)"
apply (rule_tac x = "{{a,x}. a ∈ nat ∪ Hartog (z) }" in exI)
apply (rule well_ord_Un [OF Ord_nat [THEN well_ord_Memrel]
                         Ord_Hartog [THEN well_ord_Memrel], THEN exE])
apply (blast intro!: Ord_Hartog well_ord_Memrel well_ord_paired
                      lepoll_trans1 [OF _ not_Hartog_lepoll_self]
                      lepoll_trans [OF subset_imp_lepoll lepoll_paired]
       elim!: nat_not_Finite [THEN notE]
       elim: mem_asym
       dest!: Un_upper1 [THEN subset_imp_lepoll, THEN lepoll_Finite]
              lepoll_paired [THEN lepoll_Finite])
done

lemma infinite_Un: "¬Finite(B) ==> ¬Finite(A ∪ B)"
by (blast intro: subset_Finite)

(* ********************************************************************** *)
(* There is a v \<in> s(u) such that k \<lesssim> x \<inter> y (in our case succ(k))    *)
(* The idea of the proof is the following \<in>                               *)
(* Suppose not, i.e. every element of s(u) has exactly k-1 elements of y   *)
(* Thence y is less than or equipollent to {v \<in> Pow(x). v \<approx> n#-k}      *)
(*   We have obtained this result in two steps \<in>                          *)
(*   1. y is less than or equipollent to {v \<in> s(u). a \<subseteq> v}                  *)
(*      where a is certain k-2 element subset of y                        *)
(*   2. {v \<in> s(u). a \<subseteq> v} is less than or equipollent                       *)
(*      to {v \<in> Pow(x). v \<approx> n-k}                                       *)
(* ********************************************************************** *)

(*Proof simplified by LCP*)
lemma succ_not_lepoll_lemma:
     "[¬(∃x ∈ A. f`x=y); f ∈ inj(A, B); y ∈ B]
      ==> (λa ∈ succ(A). if(a=A, y, f`a)) ∈ inj(succ(A), B)"
apply (rule_tac d = "λz. if (z=y, A, converse (f) `z) " in lam_injective)
apply (force simp add: inj_is_fun [THEN apply_type])
(*this preliminary simplification prevents looping somehow*)
apply (simp (no_asm_simp))
apply force
done

lemma succ_not_lepoll_imp_eqpoll: "[¬A ≈ B; A < B] ==> succ(A) < B"
  unfolding lepoll_def eqpoll_def bij_def surj_def
apply (fast elim!: succ_not_lepoll_lemma inj_is_fun)
done

(* ********************************************************************** *)
(* There is a k-2 element subset of y                                     *)
(* ********************************************************************** *)

lemmas ordertype_eqpoll =
       ordermap_bij [THEN exI [THEN eqpoll_def [THEN def_imp_iff, THEN iffD2]]]

lemma cons_cons_subset:
     "[a ⊆ y; b ∈ y-a; u ∈ x] ==> cons(b, cons(u, a)) ∈ Pow(x ∪ y)"
by fast

lemma cons_cons_eqpoll:
     "[a ≈ k; a ⊆ y; b ∈ y-a; u ∈ x; x ∩ y = 0]
      ==> cons(b, cons(u, a)) ≈ succ(succ(k))"
by (fast intro!: cons_eqpoll_succ)

lemma set_eq_cons:
     "[succ(k) ≈ A; k ≈ B; B ⊆ A; a ∈ A-B; k ∈ nat] ==> A = cons(a, B)"
apply (rule equalityI)
prefer 2 apply fast
apply (rule Diff_eq_0_iff [THEN iffD1])
apply (rule equals0I)
apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
apply (drule eqpoll_sym [THEN cons_eqpoll_succ], fast)
apply (drule cons_eqpoll_succ, fast)
apply (fast elim!: lepoll_trans [THEN lepoll_trans, THEN succ_lepoll_natE,
         OF eqpoll_sym [THEN eqpoll_imp_lepoll] subset_imp_lepoll])
done

lemma cons_eqE: "[cons(x,a) = cons(y,a); x ∉ a] ==> x = y "
by (fast elim!: equalityE)

lemma eq_imp_Int_eq: "A = B ==> A ∩ C = B ∩ C"
by blast

(* ********************************************************************** *)
(* some arithmetic                                                        *)
(* ********************************************************************** *)

lemma eqpoll_sum_imp_Diff_lepoll_lemma [rule_format]:
     "[k ∈ nat; m ∈ nat]
      ==> ∀A B. A ≈ k #+ m ∧ k < B ∧ B ⊆ A ⟶ A-B < m"
apply (induct_tac "k")
apply (simp add: add_0)
apply (blast intro: eqpoll_imp_lepoll lepoll_trans
                    Diff_subset [THEN subset_imp_lepoll])
apply (intro allI impI)
apply (rule succ_lepoll_imp_not_empty [THEN not_emptyE], fast)
apply (erule_tac x = "A - {xa}" in allE)
apply (erule_tac x = "B - {xa}" in allE)
apply (erule impE)
apply (simp add: add_succ)
apply (fast intro!: Diff_sing_eqpoll lepoll_Diff_sing)
apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp)
apply blast
done

lemma eqpoll_sum_imp_Diff_lepoll:
     "[A ≈ succ(k #+ m); B ⊆ A; succ(k) < B; k ∈ nat; m ∈ nat]
      ==> A-B < m"
apply (simp only: add_succ [symmetric])
apply (blast intro: eqpoll_sum_imp_Diff_lepoll_lemma)
done

(* ********************************************************************** *)
(* similar properties for \<approx>                                          *)
(* ********************************************************************** *)

lemma eqpoll_sum_imp_Diff_eqpoll_lemma [rule_format]:
     "[k ∈ nat; m ∈ nat]
      ==> ∀A B. A ≈ k #+ m ∧ k ≈ B ∧ B ⊆ A ⟶ A-B ≈ m"
apply (induct_tac "k")
apply (force dest!: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_0_is_0])
apply (intro allI impI)
apply (rule succ_lepoll_imp_not_empty [THEN not_emptyE])
apply (fast elim!: eqpoll_imp_lepoll)
apply (erule_tac x = "A - {xa}" in allE)
apply (erule_tac x = "B - {xa}" in allE)
apply (erule impE)
apply (force intro: eqpoll_sym intro!: Diff_sing_eqpoll)
apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp)
apply blast
done

lemma eqpoll_sum_imp_Diff_eqpoll:
     "[A ≈ succ(k #+ m); B ⊆ A; succ(k) ≈ B; k ∈ nat; m ∈ nat]
      ==> A-B ≈ m"
apply (simp only: add_succ [symmetric])
apply (blast intro: eqpoll_sum_imp_Diff_eqpoll_lemma)
done

(* ********************************************************************** *)
(* LL can be well ordered                                                 *)
(* ********************************************************************** *)

lemma subsets_lepoll_0_eq_unit: "{x ∈ Pow(X). x < 0} = {0}"
by (fast dest!: lepoll_0_is_0 intro!: lepoll_refl)

lemma subsets_lepoll_succ:
     "n ∈ nat ==> {z ∈ Pow(y). z < succ(n)} =
                  {z ∈ Pow(y). z < n} ∪ {z ∈ Pow(y). z ≈ succ(n)}"
by (blast intro: leI le_imp_lepoll nat_into_Ord
                    lepoll_trans eqpoll_imp_lepoll
          dest!: lepoll_succ_disj)

lemma Int_empty:
     "n ∈ nat ==> {z ∈ Pow(y). z < n} ∩ {z ∈ Pow(y). z ≈ succ(n)} = 0"
by (blast intro: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans]
                 succ_lepoll_natE)

locale AC16 =
  fixes x and y and k and l and m and t_n and R and MM and LL and GG and s
  defines k_def:     "k ≡ succ(l)"
      and MM_def:    "MM ≡ {v ∈ t_n. succ(k) < v ∩ y}"
      and LL_def:    "LL ≡ {v ∩ y. v ∈ MM}"
      and GG_def:    "GG ≡ λv ∈ LL. (THE w. w ∈ MM ∧ v ⊆ w) - v"
      and s_def:     "s(u) ≡ {v ∈ t_n. u ∈ v ∧ k < v ∩ y}"
  assumes all_ex:    "∀z ∈ {z ∈ Pow(x ∪ y) . z ≈ succ(k)}.
                       ∃! w. w ∈ t_n ∧ z ⊆ w "
    and disjoint[iff]:  "x ∩ y = 0"
    and "includes":  "t_n ⊆ {v ∈ Pow(x ∪ y). v ≈ succ(k #+ m)}"
    and WO_R[iff]:      "well_ord(y,R)"
    and lnat[iff]:      "l ∈ nat"
    and mnat[iff]:      "m ∈ nat"
    and mpos[iff]:      "0
    and Infinite[iff]:  "¬ Finite(y)"
    and noLepoll:  "¬ y < {v ∈ Pow(x). v ≈ m}"
begin

lemma knat [iff]: "k ∈ nat"
by (simp add: k_def)

(* ********************************************************************** *)
(*   1. y is less than or equipollent to {v \<in> s(u). a \<subseteq> v}                *)
(*      where a is certain k-2 element subset of y                        *)
(* ********************************************************************** *)

lemma Diff_Finite_eqpoll: "[l ≈ a; a ⊆ y] ==> y - a ≈ y"
apply (insert WO_R Infinite lnat)
apply (rule eqpoll_trans)
apply (rule Diff_lesspoll_eqpoll_Card)
apply (erule well_ord_cardinal_eqpoll [THEN eqpoll_sym])
apply (blast intro: lesspoll_trans1
            intro!: Card_cardinal
                    Card_cardinal [THEN Card_is_Ord, THEN nat_le_infinite_Ord,
                                   THEN le_imp_lepoll]
            dest: well_ord_cardinal_eqpoll
                   eqpoll_sym  eqpoll_imp_lepoll
                   n_lesspoll_nat [THEN lesspoll_trans2]
                   well_ord_cardinal_eqpoll [THEN eqpoll_sym,
                          THEN eqpoll_imp_lepoll, THEN lepoll_infinite])+
done

lemma s_subset: "s(u) ⊆ t_n"
by (unfold s_def, blast)

lemma sI:
      "[w ∈ t_n; cons(b,cons(u,a)) ⊆ w; a ⊆ y; b ∈ y-a; l ≈ a]
       ==> w ∈ s(u)"
  unfolding s_def succ_def k_def
apply (blast intro!: eqpoll_imp_lepoll [THEN cons_lepoll_cong]
             intro: subset_imp_lepoll lepoll_trans)
done

lemma in_s_imp_u_in: "v ∈ s(u) ==> u ∈ v"
by (unfold s_def, blast)

lemma ex1_superset_a:
     "[l ≈ a; a ⊆ y; b ∈ y - a; u ∈ x]
      ==> ∃! c. c ∈ s(u) ∧ a ⊆ c ∧ b ∈ c"
apply (rule all_ex [simplified k_def, THEN ballE])
apply (erule ex1E)
apply (rule_tac a = w in ex1I, blast intro: sI)
apply (blast dest: s_subset [THEN subsetD] in_s_imp_u_in)
apply (blast del: PowI
             intro!: cons_cons_subset eqpoll_sym [THEN cons_cons_eqpoll])
done

lemma the_eq_cons:
     "[∀v ∈ s(u). succ(l) ≈ v ∩ y;
         l ≈ a; a ⊆ y; b ∈ y - a; u ∈ x]
      ==> (THE c. c ∈ s(u) ∧ a ⊆ c ∧ b ∈ c) ∩ y = cons(b, a)"
apply (frule ex1_superset_a [THEN theI], assumption+)
apply (rule set_eq_cons)
apply (fast+)
done

lemma y_lepoll_subset_s:
     "[∀v ∈ s(u). succ(l) ≈ v ∩ y;
         l ≈ a; a ⊆ y; u ∈ x]
      ==> y < {v ∈ s(u). a ⊆ v}"
apply (rule Diff_Finite_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll,
                                THEN lepoll_trans],  fast+)
apply (rule_tac  f3 = "λb ∈ y-a. THE c. c ∈ s (u) ∧ a ⊆ c ∧ b ∈ c"
        in exI [THEN lepoll_def [THEN def_imp_iff, THEN iffD2]])
apply (simp add: inj_def)
apply (rule conjI)
apply (rule lam_type)
apply (frule ex1_superset_a [THEN theI], fast+, clarify)
apply (rule cons_eqE [of _ a])
apply (drule_tac A = "THE c. P (c)" and C = y for P in eq_imp_Int_eq)
apply (simp_all add: the_eq_cons)
done

(* ********************************************************************** *)
(* back to the second part                                                *)
(* ********************************************************************** *)

(*relies on the disjointness of x, y*)
lemma x_imp_not_y [dest]: "a ∈ x ==> a ∉ y"
by (blast dest:  disjoint [THEN equalityD1, THEN subsetD, OF IntI])

lemma w_Int_eq_w_Diff:
     "w ⊆ x ∪ y ==> w ∩ (x - {u}) = w - cons(u, w ∩ y)"
by blast

lemma w_Int_eqpoll_m:
     "[w ∈ {v ∈ s(u). a ⊆ v};
         l ≈ a; u ∈ x;
         ∀v ∈ s(u). succ(l) ≈ v ∩ y]
      ==> w ∩ (x - {u}) ≈ m"
apply (erule CollectE)
apply (subst w_Int_eq_w_Diff)
apply (fast dest!: s_subset [THEN subsetD]
                   "includes" [simplified k_def, THEN subsetD])
apply (blast dest: s_subset [THEN subsetD]
                   "includes" [simplified k_def, THEN subsetD]
             dest: eqpoll_sym [THEN cons_eqpoll_succ, THEN eqpoll_sym]
                   in_s_imp_u_in
            intro!: eqpoll_sum_imp_Diff_eqpoll)
done

(* ********************************************************************** *)
(*   2. {v \<in> s(u). a \<subseteq> v} is less than or equipollent                       *)
(*      to {v \<in> Pow(x). v \<approx> n-k}                                       *)
(* ********************************************************************** *)

lemma eqpoll_m_not_empty: "a ≈ m ==> a ≠ 0"
apply (insert mpos)
apply (fast elim!: zero_lt_natE dest!: eqpoll_succ_imp_not_empty)
done

lemma cons_cons_in:
     "[z ∈ xa ∩ (x - {u}); l ≈ a; a ⊆ y; u ∈ x]
      ==> ∃! w. w ∈ t_n ∧ cons(z, cons(u, a)) ⊆ w"
apply (rule all_ex [THEN bspec])
  unfolding k_def
apply (fast intro!: cons_eqpoll_succ elim: eqpoll_sym)
done

lemma subset_s_lepoll_w:
     "[∀v ∈ s(u). succ(l) ≈ v ∩ y; a ⊆ y; l ≈ a; u ∈ x]
      ==> {v ∈ s(u). a ⊆ v} < {v ∈ Pow(x). v ≈ m}"
apply (rule_tac f3 = "λw ∈ {v ∈ s (u) . a ⊆ v}. w ∩ (x - {u})"
       in exI [THEN lepoll_def [THEN def_imp_iff, THEN iffD2]])
apply (simp add: inj_def)
apply (intro conjI lam_type CollectI)
  apply fast
apply (blast intro: w_Int_eqpoll_m)
apply (intro ballI impI)
(** LEVEL 8 **)
apply (rule w_Int_eqpoll_m [THEN eqpoll_m_not_empty, THEN not_emptyE])
apply (blast, assumption+)
apply (drule equalityD1 [THEN subsetD], assumption)
apply (frule cons_cons_in, assumption+)
apply (blast dest: ex1_two_eq intro: s_subset [THEN subsetD] in_s_imp_u_in)+
done

(* ********************************************************************** *)
(* well_ord_subsets_lepoll_n                                              *)
(* ********************************************************************** *)

lemma well_ord_subsets_eqpoll_n:
     "n ∈ nat ==> ∃S. well_ord({z ∈ Pow(y) . z ≈ succ(n)}, S)"
apply (rule WO_R [THEN well_ord_infinite_subsets_eqpoll_X,
                  THEN eqpoll_def [THEN def_imp_iff, THEN iffD1], THEN exE])
apply (fast intro: bij_is_inj [THEN well_ord_rvimage])+
done

lemma well_ord_subsets_lepoll_n:
     "n ∈ nat ==> ∃R. well_ord({z ∈ Pow(y). z < n}, R)"
apply (induct_tac "n")
apply (force intro!: well_ord_unit simp add: subsets_lepoll_0_eq_unit)
apply (erule exE)
apply (rule well_ord_subsets_eqpoll_n [THEN exE], assumption)
apply (simp add: subsets_lepoll_succ)
apply (drule well_ord_radd, assumption)
apply (erule Int_empty [THEN disj_Un_eqpoll_sum,
                  THEN eqpoll_def [THEN def_imp_iff, THEN iffD1], THEN exE])
apply (fast elim!: bij_is_inj [THEN well_ord_rvimage])
done

lemma LL_subset: "LL ⊆ {z ∈ Pow(y). z < succ(k #+ m)}"
  unfolding LL_def MM_def
apply (insert "includes")
apply (blast intro: subset_imp_lepoll eqpoll_imp_lepoll lepoll_trans)
done

lemma well_ord_LL: "∃S. well_ord(LL,S)"
apply (rule well_ord_subsets_lepoll_n [THEN exE, of "succ(k#+m)"])
apply simp
apply (blast intro: well_ord_subset [OF _ LL_subset])
done

(* ********************************************************************** *)
(* every element of LL is a contained in exactly one element of MM        *)
(* ********************************************************************** *)

lemma unique_superset_in_MM:
     "v ∈ LL ==> ∃! w. w ∈ MM ∧ v ⊆ w"
apply (unfold MM_def LL_def, safe, fast)
apply (rule lepoll_imp_eqpoll_subset [THEN exE], assumption)
apply (rule_tac x = x in all_ex [THEN ballE])
apply (blast intro: eqpoll_sym)+
done

(* ********************************************************************** *)
(* The function GG satisfies the conditions of WO4                        *)
(* ********************************************************************** *)

(* ********************************************************************** *)
(* The union of appropriate values is the whole x                         *)
(* ********************************************************************** *)

lemma Int_in_LL: "w ∈ MM ==> w ∩ y ∈ LL"
by (unfold LL_def, fast)

lemma in_LL_eq_Int:
     "v ∈ LL ==> v = (THE x. x ∈ MM ∧ v ⊆ x) ∩ y"
apply (unfold LL_def, clarify)
apply (subst unique_superset_in_MM [THEN the_equality2])
apply (auto simp add: Int_in_LL)
done

lemma unique_superset1: "a ∈ LL ==> (THE x. x ∈ MM ∧ a ⊆ x) ∈ MM"
by (erule unique_superset_in_MM [THEN theI, THEN conjunct1])

lemma the_in_MM_subset:
     "v ∈ LL ==> (THE x. x ∈ MM ∧ v ⊆ x) ⊆ x ∪ y"
apply (drule unique_superset1)
  unfolding MM_def
apply (fast dest!: unique_superset1 "includes" [THEN subsetD])
done

lemma GG_subset: "v ∈ LL ==> GG ` v ⊆ x"
  unfolding GG_def
apply (frule the_in_MM_subset)
apply (frule in_LL_eq_Int)
apply (force elim: equalityE)
done

lemma nat_lepoll_ordertype: "nat < ordertype(y, R)"
apply (rule nat_le_infinite_Ord [THEN le_imp_lepoll])
apply (rule Ord_ordertype [OF WO_R])
apply (rule ordertype_eqpoll [THEN eqpoll_imp_lepoll, THEN lepoll_infinite])
apply (rule WO_R)
apply (rule Infinite)
done

lemma ex_subset_eqpoll_n: "n ∈ nat ==> ∃z. z ⊆ y ∧ n ≈ z"
apply (erule nat_lepoll_imp_ex_eqpoll_n)
apply (rule lepoll_trans [OF nat_lepoll_ordertype])
apply (rule ordertype_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll])
apply (rule WO_R)
done

lemma exists_proper_in_s: "u ∈ x ==> ∃v ∈ s(u). succ(k) < v ∩ y"
apply (rule ccontr)
apply (subgoal_tac "∀v ∈ s (u) . k ≈ v ∩ y")
prefer 2 apply (simp add: s_def, blast intro: succ_not_lepoll_imp_eqpoll)
  unfolding k_def
apply (insert all_ex "includes" lnat)
apply (rule ex_subset_eqpoll_n [THEN exE], assumption)
apply (rule noLepoll [THEN notE])
apply (blast intro: lepoll_trans [OF y_lepoll_subset_s subset_s_lepoll_w])
done

lemma exists_in_MM: "u ∈ x ==> ∃w ∈ MM. u ∈ w"
apply (erule exists_proper_in_s [THEN bexE])
apply (unfold MM_def s_def, fast)
done

lemma exists_in_LL: "u ∈ x ==> ∃w ∈ LL. u ∈ GG`w"
apply (rule exists_in_MM [THEN bexE], assumption)
apply (rule bexI)
apply (erule_tac [2] Int_in_LL)
  unfolding GG_def
apply (simp add: Int_in_LL)
apply (subst unique_superset_in_MM [THEN the_equality2])
apply (fast elim!: Int_in_LL)+
done

lemma OUN_eq_x: "well_ord(LL,S) ==>
      (∪b
apply (rule equalityI)
apply (rule subsetI)
apply (erule OUN_E)
apply (rule GG_subset [THEN subsetD])
prefer 2 apply assumption
apply (blast intro: ltD  ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun,
                                       THEN apply_type])
apply (rule subsetI)
apply (erule exists_in_LL [THEN bexE])
apply (force intro: ltI [OF _ Ord_ordertype]
                    ordermap_type [THEN apply_type]
             simp add: ordermap_bij [THEN bij_is_inj, THEN left_inverse])
done

(* ********************************************************************** *)
(* Every element of the family is less than or equipollent to n-k (m)     *)
(* ********************************************************************** *)

lemma in_MM_eqpoll_n: "w ∈ MM ==> w ≈ succ(k #+ m)"
  unfolding MM_def
apply (fast dest: "includes" [THEN subsetD])
done

lemma in_LL_eqpoll_n: "w ∈ LL ==> succ(k) < w"
by (unfold LL_def MM_def, fast)

lemma in_LL: "w ∈ LL ==> w ⊆ (THE x. x ∈ MM ∧ w ⊆ x)"
by (erule subset_trans [OF in_LL_eq_Int [THEN equalityD1] Int_lower1])

lemma all_in_lepoll_m:
      "well_ord(LL,S) ==>
       ∀b< m"
  unfolding GG_def
apply (rule oallI)
apply (simp add: ltD ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, THEN apply_type])
apply (insert "includes")
apply (rule eqpoll_sum_imp_Diff_lepoll)
apply (blast del: subsetI
             dest!: ltD
             intro!: eqpoll_sum_imp_Diff_lepoll in_LL_eqpoll_n
             intro: in_LL   unique_superset1 [THEN in_MM_eqpoll_n]
                    ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun,
                                  THEN apply_type])+
done

lemma "conclusion":
     "∃a f. Ord(a) ∧ domain(f) = a ∧ (∪b∧ (∀b< m)"
apply (rule well_ord_LL [THEN exE])
apply (rename_tac S)
apply (rule_tac x = "ordertype (LL,S)" in exI)
apply (rule_tac x = "λb ∈ ordertype(LL,S).
                      GG ` (converse (ordermap (LL,S)) ` b)"  in exI)
apply (simp add: ltD)
apply (blast intro: lam_funtype [THEN domain_of_fun]
                    Ord_ordertype  OUN_eq_x  all_in_lepoll_m [THEN ospec])
done

end

(* ********************************************************************** *)
(* The main theorem AC16(n, k) \<Longrightarrow> WO4(n-k)                               *)
(* ********************************************************************** *)

theorem AC16_WO4:
     "[AC_Equiv.AC16(k #+ m, k); 0 < k; 0 < m; k ∈ nat; m ∈ nat] ==> WO4(m)"
  unfolding AC_Equiv.AC16_def WO4_def
apply (rule allI)
apply (case_tac "Finite (A)")
apply (rule lemma1, assumption+)
apply (cut_tac lemma2)
apply (elim exE conjE)
apply (erule_tac x = "A ∪ y" in allE)
apply (frule infinite_Un, drule mp, assumption)
apply (erule zero_lt_natE, assumption, clarify)
apply (blast intro: AC16.conclusion [OF AC16.intro])
done

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet am 2026-04-25) ¤

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.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.