|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
taylors.prf
Sprache: Unknown
|
|
(* 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 &
(\<Union>b<a. f`b) = y & (\<forall>b<a. f`b \<lesssim> 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 = \<mu> g. (\<exists>d. Ord(d) & (domain(uu(f,b,g,d)) \<noteq> 0 &
domain(uu(f,b,g,d)) \<lesssim> m));
d = \<mu> d. domain(uu(f,b,g,d)) \<noteq> 0 &
domain(uu(f,b,g,d)) \<lesssim> m
in if f`b \<noteq> 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 \<noteq> 0 then {uu(f, b, g, \<mu> d. uu(f,b,g,d) \<noteq> 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) ==
\<lambda>g \<in> a++a. if g<a then vv2(f,b,g,s) else ww2(f,b,g--a,s)"
lemma WO2_WO3: "WO2 ==> WO3"
by (unfold WO2_def WO3_def, fast)
(* ********************************************************************** *)
lemma WO3_WO1: "WO3 ==> WO1"
apply (unfold 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"
apply (unfold 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"
apply (unfold 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)"
apply (unfold 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)"
apply (unfold 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<i & k = i ++ (k--i) & (k--i)<j)"
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 ==> \bgd 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:
"\bgd m
==> (\<forall>b<a. f`b \<noteq> 0 \<longrightarrow>
(\<exists>g<a. \<exists>d<a. u(f,b,g,d) \<noteq> 0 & u(f,b,g,d) \<prec> m))
| (\<exists>b<a. f`b \<noteq> 0 & (\<forall>g<a. \<forall>d<a. u(f,b,g,d) \<noteq> 0 \<longrightarrow>
u(f,b,g,d) \<approx> m))"
apply (unfold lesspoll_def)
apply (blast del: equalityI)
done
(* ********************************************************************** *)
(* Lemmas used in both cases *)
(* ********************************************************************** *)
lemma UN_oadd: "Ord(a) ==> (\bb 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 |] ==> (\bb
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 = (\<mu> a. \<exists>x. Ord(x) & P(a, x)) |]
==> P(Least_a, \<mu> 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)) \<lesssim> m"] for f b m
lemma gg1_lepoll_m:
"[| Ord(a); m \ nat;
\<forall>b<a. f`b \<noteq>0 \<longrightarrow>
(\<exists>g<a. \<exists>d<a. domain(uu(f,b,g,d)) \<noteq> 0 &
domain(uu(f,b,g,d)) \<lesssim> m);
\<forall>b<a. f`b \<lesssim> succ(m); b<a++a |]
==> gg1(f,a,m)`b \<lesssim> 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:
"[| b0; f`g\0;
y*y \<subseteq> y; (\<Union>b<a. f`b)=y |]
==> \<exists>d<a. uu(f,b,g,d) \<noteq> 0"
by (unfold uu_def, blast)
lemma uu_not_empty:
"[| b0; f`g\0; y*y \ y; (\b
==> uu(f,b,g,\<mu> d. (uu(f,b,g,d) \<noteq> 0)) \<noteq> 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:
"[| b0; f`g\0; y*y \ y; (\b
==> (\<mu> d. uu(f,b,g,d) \<noteq> 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:
"[| \gd0 \
domain(uu(f, b, g, d)) \<approx> succ(m);
\<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;
(\<Union>b<a. f`b)=y; b<a; g<a; d<a;
f`b\<noteq>0; f`g\<noteq>0; m \<in> nat; s \<in> f`b |]
==> uu(f, b, g, \<mu> d. uu(f,b,g,d)\<noteq>0) \<in> 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:
"[| \gd0 \
domain(uu(f, b, g, d)) \<approx> succ(m);
\<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;
(\<Union>b<a. f`b)=y; b<a; g<a; m \<in> nat; s \<in> f`b |]
==> vv2(f,b,g,s) \<subseteq> 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:
"[| \gd 0 \
domain(uu(f,b,g,d)) \<approx> succ(m);
\<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;
(\<Union>b<a. f`b)=y; Ord(a); m \<in> nat; s \<in> f`b; b<a |]
==> (\<Union>g<a++a. gg2(f,a,b,s) ` g) = y"
apply (unfold 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"
apply (unfold 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) \<lesssim> m"
apply (unfold 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:
"[| \gd 0 \
domain(uu(f,b,g,d)) \<approx> succ(m);
\<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;
(\<Union>b<a. f`b)=y; b<a; s \<in> f`b; m \<in> nat; m\<noteq> 0; g<a++a |]
==> gg2(f,a,b,s) ` g \<lesssim> 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)"
apply (unfold 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 \<union> r*r) \<subseteq> rec(m, x, %k r. r \<union> 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 ==> NN(y) \<noteq> 0 *)
(* * reverse induction which lets us infer that 1 \<in> NN(y) *)
(* * 1 \<in> NN(y) ==> y can be well-ordered *)
(* ********************************************************************** *)
(* ********************************************************************** *)
(* WO6 ==> 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) ==> 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` (\<mu> 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)"
apply (unfold 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\<noteq>0 \<longrightarrow> P(n) \<longrightarrow> P(1)"
by (erule nat_induct, blast+)
lemma rev_induct:
"[| n \ nat; P(n); n\0;
!!m. [| m \<in> nat; m\<noteq>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 ==> WO1" *)
(* ********************************************************************** *)
(* another helpful lemma *)
lemma NN_y_0: "0 \ NN(y) ==> y=0"
apply (unfold NN_def)
apply (fast intro!: equalityI dest!: lepoll_0_is_0 elim: subst)
done
lemma WO6_imp_WO1: "WO6 ==> WO1"
apply (unfold 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
¤ Dauer der Verarbeitung: 0.111 Sekunden
(vorverarbeitet)
¤
|
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.
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
|
|
|
|
|
