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