1(*  Title:      ZF/AC/WO1_WO7.thy
2    Author:     Lawrence C Paulson, CU Computer Laboratory
3    Copyright   1998  University of Cambridge
4
5WO7 \<longleftrightarrow> LEMMA \<longleftrightarrow> WO1 (Rubin & Rubin p. 5)
6LEMMA is the sentence denoted by (**)
7
8Also, WO1 \<longleftrightarrow> WO8
9*)
10
11theory WO1_WO7
12imports AC_Equiv
13begin
14
15definition
16    "LEMMA ==
17     \<forall>X. ~Finite(X) \<longrightarrow> (\<exists>R. well_ord(X,R) & ~well_ord(X,converse(R)))"
18
19(* ********************************************************************** *)
20(* It is easy to see that WO7 is equivalent to (**)                       *)
21(* ********************************************************************** *)
22
23lemma WO7_iff_LEMMA: "WO7 \<longleftrightarrow> LEMMA"
24apply (unfold WO7_def LEMMA_def)
25apply (blast intro: Finite_well_ord_converse)
26done
27
28(* ********************************************************************** *)
29(* It is also easy to show that LEMMA implies WO1.                        *)
30(* ********************************************************************** *)
31
32lemma LEMMA_imp_WO1: "LEMMA ==> WO1"
33apply (unfold WO1_def LEMMA_def Finite_def eqpoll_def)
34apply (blast intro!: well_ord_rvimage [OF bij_is_inj nat_implies_well_ord])
35done
36
37(* ********************************************************************** *)
38(* The Rubins' proof of the other implication is contained within the     *)
39(* following sentence \<in>                                                   *)
40(* "... each infinite ordinal is well ordered by < but not by >."         *)
41(* This statement can be proved by the following two theorems.            *)
42(* But moreover we need to show similar property for any well ordered     *)
43(* infinite set. It is not very difficult thanks to Isabelle order types  *)
44(* We show that if a set is well ordered by some relation and by its     *)
45(* converse, then apropriate order type is well ordered by the converse   *)
46(* of it's membership relation, which in connection with the previous     *)
47(* gives the conclusion.                                                  *)
48(* ********************************************************************** *)
49
50lemma converse_Memrel_not_wf_on: 
51    "[| Ord(a); ~Finite(a) |] ==> ~wf[a](converse(Memrel(a)))"
52apply (unfold wf_on_def wf_def)
53apply (drule nat_le_infinite_Ord [THEN le_imp_subset], assumption)
54apply (rule notI)
55apply (erule_tac x = nat in allE, blast)
56done
57
58lemma converse_Memrel_not_well_ord: 
59    "[| Ord(a); ~Finite(a) |] ==> ~well_ord(a,converse(Memrel(a)))"
60apply (unfold well_ord_def)
61apply (blast dest: converse_Memrel_not_wf_on)
62done
63
64lemma well_ord_rvimage_ordertype:
65     "well_ord(A,r) \<Longrightarrow>
66       rvimage (ordertype(A,r), converse(ordermap(A,r)),r) =
67       Memrel(ordertype(A,r))" 
68by (blast intro: ordertype_ord_iso [THEN ord_iso_sym] ord_iso_rvimage_eq
69             Memrel_type [THEN subset_Int_iff [THEN iffD1]] trans)
70
71lemma well_ord_converse_Memrel:
72     "[| well_ord(A,r); well_ord(A,converse(r)) |]   
73      ==> well_ord(ordertype(A,r), converse(Memrel(ordertype(A,r))))" 
74apply (subst well_ord_rvimage_ordertype [symmetric], assumption) 
75apply (rule rvimage_converse [THEN subst])
76apply (blast intro: ordertype_ord_iso ord_iso_sym ord_iso_is_bij
77                    bij_is_inj well_ord_rvimage)
78done
79
80lemma WO1_imp_LEMMA: "WO1 ==> LEMMA"
81apply (unfold WO1_def LEMMA_def, clarify) 
82apply (blast dest: well_ord_converse_Memrel
83                   Ord_ordertype [THEN converse_Memrel_not_well_ord]
84             intro: ordertype_ord_iso ord_iso_is_bij bij_is_inj lepoll_Finite
85                    lepoll_def [THEN def_imp_iff, THEN iffD2] )
86done
87
88lemma WO1_iff_WO7: "WO1 \<longleftrightarrow> WO7"
89apply (simp add: WO7_iff_LEMMA)
90apply (blast intro: LEMMA_imp_WO1 WO1_imp_LEMMA)
91done
92
93
94
95(* ********************************************************************** *)
96(*            The proof of WO8 \<longleftrightarrow> WO1 (Rubin & Rubin p. 6)               *)
97(* ********************************************************************** *)
98
99lemma WO1_WO8: "WO1 ==> WO8"
100by (unfold WO1_def WO8_def, fast)
101
102
103(* The implication "WO8 ==> WO1": a faithful image of Rubin & Rubin's proof*)
104lemma WO8_WO1: "WO8 ==> WO1"
105apply (unfold WO1_def WO8_def)
106apply (rule allI)
107apply (erule_tac x = "{{x}. x \<in> A}" in allE)
108apply (erule impE)
109 apply (rule_tac x = "\<lambda>a \<in> {{x}. x \<in> A}. THE x. a={x}" in exI)
110 apply (force intro!: lam_type simp add: singleton_eq_iff the_equality)
111apply (blast intro: lam_sing_bij bij_is_inj well_ord_rvimage)
112done
113
114end
115