Quelle AC15_WO6.thy Sprache: Isabelle

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

The proofs needed to state that AC10, ..., AC15 are equivalent to the rest.
We need the following:

WO1 \<Longrightarrow> AC10(n) \<Longrightarrow> AC11 \<Longrightarrow> AC12 \<Longrightarrow> AC15 \<Longrightarrow> WO6

In order to add the formulations AC13 and AC14 we need:

AC10(succ(n)) \<Longrightarrow> AC13(n) \<Longrightarrow> AC14 \<Longrightarrow> AC15

or

AC1 \<Longrightarrow> AC13(1);  AC13(m) \<Longrightarrow> AC13(n) \<Longrightarrow> AC14 \<Longrightarrow> AC15    (m\<le>n)

So we don't have to prove all implications of both cases.
Moreover we don't need to prove AC13(1) \<Longrightarrow> AC1 and AC11 \<Longrightarrow> AC14 as
Rubin & Rubin do.
*)

theory AC15_WO6
imports HH Cardinal_aux
begin

(* ********************************************************************** *)
(* Lemmas used in the proofs in which the conclusion is AC13, AC14        *)
(* or AC15                                                                *)
(*  - cons_times_nat_not_Finite                                           *)
(*  - ex_fun_AC13_AC15                                                    *)
(* ********************************************************************** *)

lemma lepoll_Sigma: "A\0 \ B \ A*B"
  unfolding lepoll_def
apply (erule not_emptyE)
apply (rule_tac x = "\z \ B. \x,z\" in exI)
apply (fast intro!: snd_conv lam_injective)
done

lemma cons_times_nat_not_Finite:
     "0\A \ \B \ {cons(0,x*nat). x \ A}. \Finite(B)"
apply clarify
apply (rule nat_not_Finite [THEN notE] )
apply (subgoal_tac "x \ 0")
apply (blast intro: lepoll_Sigma [THEN lepoll_Finite])+
done

lemma lemma1: "\\(C)=A; a \ A\ \ \B \ C. a \ B \ B \ A"
by fast

lemma lemma2:
        "\pairwise_disjoint(A); B \ A; C \ A; a \ B; a \ C\ \ B=C"
by (unfold pairwise_disjoint_def, blast)

lemma lemma3:
     "\B \ {cons(0, x*nat). x \ A}. pairwise_disjoint(f`B) \
             sets_of_size_between(f`B, 2, n) \<and> \<Union>(f`B)=B
     \<Longrightarrow> \<forall>B \<in> A. \<exists>! u. u \<in> f`cons(0, B*nat) \<and> u \<subseteq> cons(0, B*nat) \<and>
             0 \<in> u \<and> 2 \<lesssim> u \<and> u \<lesssim> n"
  unfolding sets_of_size_between_def
apply (rule ballI)
apply (erule_tac x="cons(0, B*nat)" in ballE)
apply (blast dest: lemma1 intro!: lemma2, blast)
done

lemma lemma4: "\A \ i; Ord(i)\ \ {P(a). a \ A} \ i"
  unfolding lepoll_def
apply (erule exE)
apply (rule_tac x = "\x \ RepFun(A,P). \ j. \a\A. x=P(a) \ f`a=j"
       in exI)
apply (rule_tac d = "\y. P (converse (f) `y) " in lam_injective)
apply (erule RepFunE)
apply (frule inj_is_fun [THEN apply_type], assumption)
apply (fast intro: LeastI2 elim!: Ord_in_Ord inj_is_fun [THEN apply_type])
apply (erule RepFunE)
apply (rule LeastI2)
  apply fast
apply (fast elim!: Ord_in_Ord inj_is_fun [THEN apply_type])
apply (fast elim: sym left_inverse [THEN ssubst])
done

lemma lemma5_1:
     "\B \ A; 2 \ u(B)\ \ (\x \ A. {fst(x). x \ u(x)-{0}})`B \ 0"
apply simp
apply (fast dest: lepoll_Diff_sing
            elim: lepoll_trans [THEN succ_lepoll_natE] ssubst
            intro!: lepoll_refl)
done

lemma lemma5_2:
     "\B \ A; u(B) \ cons(0, B*nat)\
      \<Longrightarrow> (\<lambda>x \<in> A. {fst(x). x \<in> u(x)-{0}})`B \<subseteq> B"
apply auto
done

lemma lemma5_3:
     "\n \ nat; B \ A; 0 \ u(B); u(B) \ succ(n)\
      \<Longrightarrow> (\<lambda>x \<in> A. {fst(x). x \<in> u(x)-{0}})`B \<lesssim> n"
apply simp
apply (fast elim!: Diff_lepoll [THEN lemma4 [OF _ nat_into_Ord]])
done

lemma ex_fun_AC13_AC15:
     "\\B \ {cons(0, x*nat). x \ A}.
                pairwise_disjoint(f`B) \<and>
                sets_of_size_between(f`B, 2, succ(n)) \<and> \<Union>(f`B)=B;
         n \<in> nat\<rbrakk>
      \<Longrightarrow> \<exists>f. \<forall>B \<in> A. f`B \<noteq> 0 \<and> f`B \<subseteq> B \<and> f`B \<lesssim> n"
by (fast del: subsetI notI
         dest!: lemma3 theI intro!: lemma5_1 lemma5_2 lemma5_3)

(* ********************************************************************** *)
(* The target proofs                                                      *)
(* ********************************************************************** *)

(* ********************************************************************** *)
(* AC10(n) \<Longrightarrow> AC11                                                       *)
(* ********************************************************************** *)

theorem AC10_AC11: "\n \ nat; 1\n; AC10(n)\ \ AC11"
by (unfold AC10_def AC11_def, blast)

(* ********************************************************************** *)
(* AC11 \<Longrightarrow> AC12                                                          *)
(* ********************************************************************** *)

theorem AC11_AC12: "AC11 \ AC12"
by (unfold AC10_def AC11_def AC11_def AC12_def, blast)

(* ********************************************************************** *)
(* AC12 \<Longrightarrow> AC15                                                          *)
(* ********************************************************************** *)

theorem AC12_AC15: "AC12 \ AC15"
  unfolding AC12_def AC15_def
apply (blast del: ballI
             intro!: cons_times_nat_not_Finite ex_fun_AC13_AC15)
done

(* ********************************************************************** *)
(* AC15 \<Longrightarrow> WO6                                                           *)
(* ********************************************************************** *)

lemma OUN_eq_UN: "Ord(x) \ (\aa \ x. F(a))"
by (fast intro!: ltI dest!: ltD)

lemma AC15_WO6_aux1:
     "\x \ Pow(A)-{0}. f`x\0 \ f`x \ x \ f`x \ m
      \<Longrightarrow> (\<Union>i<\<mu> x. HH(f,A,x)={A}. HH(f,A,i)) = A"
apply (simp add: Ord_Least [THEN OUN_eq_UN])
apply (rule equalityI)
apply (fast dest!: less_Least_subset_x)
apply (blast del: subsetI
           intro!: f_subsets_imp_UN_HH_eq_x [THEN Diff_eq_0_iff [THEN iffD1]])
done

lemma AC15_WO6_aux2:
     "\x \ Pow(A)-{0}. f`x\0 \ f`x \ x \ f`x \ m
      \<Longrightarrow> \<forall>x < (\<mu> x. HH(f,A,x)={A}). HH(f,A,x) \<lesssim> m"
apply (rule oallI)
apply (drule ltD [THEN less_Least_subset_x])
apply (frule HH_subset_imp_eq)
apply (erule ssubst)
apply (blast dest!: HH_subset_x_imp_subset_Diff_UN [THEN not_emptyI2])
        (*but can't use del: DiffE despite the obvious conflict*)
done

theorem AC15_WO6: "AC15 \ WO6"
  unfolding AC15_def WO6_def
apply (rule allI)
apply (erule_tac x = "Pow (A) -{0}" in allE)
apply (erule impE, fast)
apply (elim bexE conjE exE)
apply (rule bexI)
apply (rule conjI, assumption)
apply (rule_tac x = "\ i. HH (f,A,i) ={A}" in exI)
apply (rule_tac x = "\j \ (\ i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
apply (simp_all add: ltD)
apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun]
            elim!: less_Least_subset_x AC15_WO6_aux1 AC15_WO6_aux2)
done

(* ********************************************************************** *)
(* The proof needed in the first case, not in the second                  *)
(* ********************************************************************** *)

(* ********************************************************************** *)
(* AC10(n) \<Longrightarrow> AC13(n-1)  if 2\<le>n                                       *)
(*                                                                        *)
(* Because of the change to the formal definition of AC10(n) we prove     *)
(* the following obviously equivalent theorem \<in>                           *)
(* AC10(n) implies AC13(n) for (1\<le>n)                                   *)
(* ********************************************************************** *)

theorem AC10_AC13: "\n \ nat; 1\n; AC10(n)\ \ AC13(n)"
apply (unfold AC10_def AC13_def, safe)
apply (erule allE)
apply (erule impE [OF _ cons_times_nat_not_Finite], assumption)
apply (fast elim!: impE [OF _ cons_times_nat_not_Finite]
            dest!: ex_fun_AC13_AC15)
done

(* ********************************************************************** *)
(* The proofs needed in the second case, not in the first                 *)
(* ********************************************************************** *)

(* ********************************************************************** *)
(* AC1 \<Longrightarrow> AC13(1)                                                        *)
(* ********************************************************************** *)

lemma AC1_AC13: "AC1 \ AC13(1)"
  unfolding AC1_def AC13_def
apply (rule allI)
apply (erule allE)
apply (rule impI)
apply (drule mp, assumption)
apply (elim exE)
apply (rule_tac x = "\x \ A. {f`x}" in exI)
apply (simp add: singleton_eqpoll_1 [THEN eqpoll_imp_lepoll])
done

(* ********************************************************************** *)
(* AC13(m) \<Longrightarrow> AC13(n) for m \<subseteq> n                                         *)
(* ********************************************************************** *)

lemma AC13_mono: "\m\n; AC13(m)\ \ AC13(n)"
  unfolding AC13_def
apply (drule le_imp_lepoll)
apply (fast elim!: lepoll_trans)
done

(* ********************************************************************** *)
(* The proofs necessary for both cases                                    *)
(* ********************************************************************** *)

(* ********************************************************************** *)
(* AC13(n) \<Longrightarrow> AC14  if 1 \<subseteq> n                                            *)
(* ********************************************************************** *)

theorem AC13_AC14: "\n \ nat; 1\n; AC13(n)\ \ AC14"
by (unfold AC13_def AC14_def, auto)

(* ********************************************************************** *)
(* AC14 \<Longrightarrow> AC15                                                          *)
(* ********************************************************************** *)

theorem AC14_AC15: "AC14 \ AC15"
by (unfold AC13_def AC14_def AC15_def, fast)

(* ********************************************************************** *)
(* The redundant proofs; however cited by Rubin & Rubin                   *)
(* ********************************************************************** *)

(* ********************************************************************** *)
(* AC13(1) \<Longrightarrow> AC1                                                        *)
(* ********************************************************************** *)

lemma lemma_aux: "\A\0; A \ 1\ \ \a. A={a}"
by (fast elim!: not_emptyE lepoll_1_is_sing)

lemma AC13_AC1_lemma:
     "\B \ A. f(B)\0 \ f(B)<=B \ f(B) \ 1
      \<Longrightarrow> (\<lambda>x \<in> A. THE y. f(x)={y}) \<in> (\<Prod>X \<in> A. X)"
apply (rule lam_type)
apply (drule bspec, assumption)
apply (elim conjE)
apply (erule lemma_aux [THEN exE], assumption)
apply (simp add: the_equality)
done

theorem AC13_AC1: "AC13(1) \ AC1"
  unfolding AC13_def AC1_def
apply (fast elim!: AC13_AC1_lemma)
done

(* ********************************************************************** *)
(* AC11 \<Longrightarrow> AC14                                                          *)
(* ********************************************************************** *)

theorem AC11_AC14: "AC11 \ AC14"
  unfolding AC11_def AC14_def
apply (fast intro!: AC10_AC13)
done

end

quality92%

¤ Dauer der Verarbeitung: 0.17 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.