19 (* ********************************************************************** *) |
19 (* ********************************************************************** *) |
20 (* It is easy to see that WO7 is equivalent to (**) *) |
20 (* It is easy to see that WO7 is equivalent to (**) *) |
21 (* ********************************************************************** *) |
21 (* ********************************************************************** *) |
22 |
22 |
23 lemma WO7_iff_LEMMA: "WO7 \<longleftrightarrow> LEMMA" |
23 lemma WO7_iff_LEMMA: "WO7 \<longleftrightarrow> LEMMA" |
24 apply (unfold WO7_def LEMMA_def) |
24 unfolding WO7_def LEMMA_def |
25 apply (blast intro: Finite_well_ord_converse) |
25 apply (blast intro: Finite_well_ord_converse) |
26 done |
26 done |
27 |
27 |
28 (* ********************************************************************** *) |
28 (* ********************************************************************** *) |
29 (* It is also easy to show that LEMMA implies WO1. *) |
29 (* It is also easy to show that LEMMA implies WO1. *) |
30 (* ********************************************************************** *) |
30 (* ********************************************************************** *) |
31 |
31 |
32 lemma LEMMA_imp_WO1: "LEMMA \<Longrightarrow> WO1" |
32 lemma LEMMA_imp_WO1: "LEMMA \<Longrightarrow> WO1" |
33 apply (unfold WO1_def LEMMA_def Finite_def eqpoll_def) |
33 unfolding WO1_def LEMMA_def Finite_def eqpoll_def |
34 apply (blast intro!: well_ord_rvimage [OF bij_is_inj nat_implies_well_ord]) |
34 apply (blast intro!: well_ord_rvimage [OF bij_is_inj nat_implies_well_ord]) |
35 done |
35 done |
36 |
36 |
37 (* ********************************************************************** *) |
37 (* ********************************************************************** *) |
38 (* The Rubins' proof of the other implication is contained within the *) |
38 (* The Rubins' proof of the other implication is contained within the *) |
47 (* gives the conclusion. *) |
47 (* gives the conclusion. *) |
48 (* ********************************************************************** *) |
48 (* ********************************************************************** *) |
49 |
49 |
50 lemma converse_Memrel_not_wf_on: |
50 lemma converse_Memrel_not_wf_on: |
51 "\<lbrakk>Ord(a); \<not>Finite(a)\<rbrakk> \<Longrightarrow> \<not>wf[a](converse(Memrel(a)))" |
51 "\<lbrakk>Ord(a); \<not>Finite(a)\<rbrakk> \<Longrightarrow> \<not>wf[a](converse(Memrel(a)))" |
52 apply (unfold wf_on_def wf_def) |
52 unfolding wf_on_def wf_def |
53 apply (drule nat_le_infinite_Ord [THEN le_imp_subset], assumption) |
53 apply (drule nat_le_infinite_Ord [THEN le_imp_subset], assumption) |
54 apply (rule notI) |
54 apply (rule notI) |
55 apply (erule_tac x = nat in allE, blast) |
55 apply (erule_tac x = nat in allE, blast) |
56 done |
56 done |
57 |
57 |
100 by (unfold WO1_def WO8_def, fast) |
100 by (unfold WO1_def WO8_def, fast) |
101 |
101 |
102 |
102 |
103 (* The implication "WO8 \<Longrightarrow> WO1": a faithful image of Rubin \<and> Rubin's proof*) |
103 (* The implication "WO8 \<Longrightarrow> WO1": a faithful image of Rubin \<and> Rubin's proof*) |
104 lemma WO8_WO1: "WO8 \<Longrightarrow> WO1" |
104 lemma WO8_WO1: "WO8 \<Longrightarrow> WO1" |
105 apply (unfold WO1_def WO8_def) |
105 unfolding WO1_def WO8_def |
106 apply (rule allI) |
106 apply (rule allI) |
107 apply (erule_tac x = "{{x}. x \<in> A}" in allE) |
107 apply (erule_tac x = "{{x}. x \<in> A}" in allE) |
108 apply (erule impE) |
108 apply (erule impE) |
109 apply (rule_tac x = "\<lambda>a \<in> {{x}. x \<in> A}. THE x. a={x}" in exI) |
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) |
110 apply (force intro!: lam_type simp add: singleton_eq_iff the_equality) |