44 (* ********************************************************************** *) |
44 (* ********************************************************************** *) |
45 |
45 |
46 goalw thy [wf_on_def, wf_def] |
46 goalw thy [wf_on_def, wf_def] |
47 "!!a. [| Ord(a); ~Finite(a) |] ==> ~wf[a](converse(Memrel(a)))"; |
47 "!!a. [| Ord(a); ~Finite(a) |] ==> ~wf[a](converse(Memrel(a)))"; |
48 by (dresolve_tac [nat_le_infinite_Ord RS le_imp_subset] 1 |
48 by (dresolve_tac [nat_le_infinite_Ord RS le_imp_subset] 1 |
49 THEN (atac 1)); |
49 THEN (assume_tac 1)); |
50 by (resolve_tac [notI] 1); |
50 by (resolve_tac [notI] 1); |
51 by (eres_inst_tac [("x","nat")] allE 1); |
51 by (eres_inst_tac [("x","nat")] allE 1); |
52 by (eresolve_tac [disjE] 1); |
52 by (eresolve_tac [disjE] 1); |
53 by (fast_tac (ZF_cs addSDs [nat_0I RSN (2,equals0D)]) 1); |
53 by (fast_tac (ZF_cs addSDs [nat_0I RSN (2,equals0D)]) 1); |
54 by (eresolve_tac [bexE] 1); |
54 by (eresolve_tac [bexE] 1); |
65 goal thy "!!A. [| well_ord(A,r); well_ord(A,converse(r)) |] \ |
65 goal thy "!!A. [| well_ord(A,r); well_ord(A,converse(r)) |] \ |
66 \ ==> well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r))))"; |
66 \ ==> well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r))))"; |
67 by (rtac ([ordertype_ord_iso RS ord_iso_sym RS ord_iso_rvimage_eq, |
67 by (rtac ([ordertype_ord_iso RS ord_iso_sym RS ord_iso_rvimage_eq, |
68 Memrel_type RS (subset_Int_iff RS iffD1)] |
68 Memrel_type RS (subset_Int_iff RS iffD1)] |
69 MRS trans RS subst) 1 |
69 MRS trans RS subst) 1 |
70 THEN (atac 1)); |
70 THEN (assume_tac 1)); |
71 by (rtac (rvimage_converse RS subst) 1); |
71 by (rtac (rvimage_converse RS subst) 1); |
72 by (etac (ordertype_ord_iso RS ord_iso_sym RS ord_iso_is_bij RS |
72 by (etac (ordertype_ord_iso RS ord_iso_sym RS ord_iso_is_bij RS |
73 bij_is_inj RS well_ord_rvimage) 1 |
73 bij_is_inj RS well_ord_rvimage) 1 |
74 THEN (atac 1)); |
74 THEN (assume_tac 1)); |
75 val well_ord_converse_Memrel = result(); |
75 val well_ord_converse_Memrel = result(); |
76 |
76 |
77 goalw thy [WO1_def] "!!Z. WO1 ==> ALL X. ~Finite(X) --> \ |
77 goalw thy [WO1_def] "!!Z. WO1 ==> ALL X. ~Finite(X) --> \ |
78 \ (EX R. well_ord(X,R) & ~well_ord(X,converse(R)))"; |
78 \ (EX R. well_ord(X,R) & ~well_ord(X,converse(R)))"; |
79 by (REPEAT (resolve_tac [allI,impI] 1)); |
79 by (REPEAT (resolve_tac [allI,impI] 1)); |
80 by (REPEAT (eresolve_tac [allE,exE] 1)); |
80 by (REPEAT (eresolve_tac [allE,exE] 1)); |
81 by (REPEAT (ares_tac [exI,conjI,notI] 1)); |
81 by (REPEAT (ares_tac [exI,conjI,notI] 1)); |
82 by (forward_tac [well_ord_converse_Memrel] 1 THEN (atac 1)); |
82 by (forward_tac [well_ord_converse_Memrel] 1 THEN (assume_tac 1)); |
83 by (forward_tac [Ord_ordertype RS converse_Memrel_not_well_ord] 1); |
83 by (forward_tac [Ord_ordertype RS converse_Memrel_not_well_ord] 1); |
84 by (contr_tac 2); |
84 by (contr_tac 2); |
85 by (fast_tac (empty_cs addSEs [ordertype_ord_iso RS ord_iso_is_bij RS |
85 by (fast_tac (empty_cs addSEs [ordertype_ord_iso RS ord_iso_is_bij RS |
86 bij_is_inj RS (exI RS (lepoll_def RS def_imp_iff RS iffD2)) |
86 bij_is_inj RS (exI RS (lepoll_def RS def_imp_iff RS iffD2)) |
87 RS lepoll_Finite] |
87 RS lepoll_Finite] |