author  paulson 
Thu, 10 Sep 1998 17:42:44 +0200  
changeset 5470  855654b691db 
parent 5325  f7a5e06adea1 
child 5505  b0856ff6fc69 
permissions  rwrr 
1461  1 
(* Title: ZF/AC/AC_Equiv.ML 
991  2 
ID: $Id$ 
1461  3 
Author: Krzysztof Grabczewski 
991  4 

5 
*) 

6 

7 

8 
open AC_Equiv; 

9 

1071  10 
val WO_defs = [WO1_def, WO2_def, WO3_def, WO4_def, WO5_def, WO6_def, WO8_def]; 
11 

12 
val AC_defs = [AC0_def, AC1_def, AC2_def, AC3_def, AC4_def, AC5_def, 

13 
AC6_def, AC7_def, AC8_def, AC9_def, AC10_def, AC11_def, 

14 
AC12_def, AC13_def, AC14_def, AC15_def, AC16_def, 

15 
AC17_def, AC18_def, AC19_def]; 

16 

991  17 
val AC_aux_defs = [pairwise_disjoint_def, sets_of_size_between_def]; 
1123  18 

991  19 
(* ******************************************** *) 
20 

21 
(* Theorems analogous to ones presented in "ZF/Ordinal.ML" *) 

22 

23 
(* lemma for nat_le_imp_lepoll *) 

24 
val [prem] = goalw Cardinal.thy [lepoll_def] 

25 
"m:nat ==> ALL n: nat. m le n > m lepoll n"; 

26 
by (nat_ind_tac "m" [prem] 1); 

4091  27 
by (fast_tac (claset() addSIs [le_imp_subset RS id_subset_inj]) 1); 
991  28 
by (rtac ballI 1); 
29 
by (eres_inst_tac [("n","n")] natE 1); 

4091  30 
by (asm_simp_tac (simpset() addsimps [inj_def, succI1 RS Pi_empty2]) 1); 
31 
by (fast_tac (claset() addSIs [le_imp_subset RS id_subset_inj]) 1); 

3731  32 
qed "nat_le_imp_lepoll_lemma"; 
991  33 

34 
(* used in : AC10AC15.ML WO1WO6.ML WO6WO1.ML*) 

35 
val nat_le_imp_lepoll = nat_le_imp_lepoll_lemma RS bspec RS mp > standard; 

36 

37 
(* ********************************************************************** *) 

38 
(* lemmas concerning FOL and pure ZF theory *) 

39 
(* ********************************************************************** *) 

40 

5137  41 
Goal "(A>X)=0 ==> X=0"; 
5470  42 
by (fast_tac (claset() addSIs [equals0I] addIs [lam_type]) 1); 
3731  43 
qed "fun_space_emptyD"; 
991  44 

45 
(* used only in WO1_DC.ML *) 

46 
(*Note simpler proof*) 

5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5265
diff
changeset

47 
Goal "[ ALL x:A. f`x=g`x; f:Df>Cf; g:Dg>Cg; A<=Df; A<=Dg ] ==> f``A=g``A"; 
4091  48 
by (asm_simp_tac (simpset() addsimps [image_fun]) 1); 
3731  49 
qed "images_eq"; 
991  50 

51 
(* used in : AC10AC15.ML AC16WO4.ML WO6WO1.ML *) 

52 
(*I don't know where to put this one.*) 

53 
goal Cardinal.thy 

54 
"!!m A B. [ A lepoll succ(m); B<=A; B~=0 ] ==> AB lepoll m"; 

1207  55 
by (rtac not_emptyE 1 THEN (assume_tac 1)); 
991  56 
by (forward_tac [singleton_subsetI] 1); 
1196  57 
by (forward_tac [subsetD] 1 THEN (assume_tac 1)); 
991  58 
by (res_inst_tac [("A2","A")] 
1057  59 
(Diff_sing_lepoll RSN (2, subset_imp_lepoll RS lepoll_trans)) 1 
1196  60 
THEN (REPEAT (assume_tac 2))); 
2469  61 
by (Fast_tac 1); 
3731  62 
qed "Diff_lepoll"; 
991  63 

64 
(* ********************************************************************** *) 

65 
(* lemmas concerning lepoll and eqpoll relations *) 

66 
(* ********************************************************************** *) 

67 

68 
(* ********************************************************************** *) 

69 
(* Theorems concerning ordinals *) 

70 
(* ********************************************************************** *) 

71 

72 
(* lemma for ordertype_Int *) 

73 
goalw Cardinal.thy [rvimage_def] "rvimage(A,id(A),r) = r Int A*A"; 

1207  74 
by (rtac equalityI 1); 
3731  75 
by Safe_tac; 
991  76 
by (dres_inst_tac [("P","%a. <id(A)`xb,a>:r")] (id_conv RS subst) 1 
1196  77 
THEN (assume_tac 1)); 
991  78 
by (dres_inst_tac [("P","%a. <a,ya>:r")] (id_conv RS subst) 1 
1196  79 
THEN (REPEAT (assume_tac 1))); 
4091  80 
by (fast_tac (claset() addIs [id_conv RS ssubst]) 1); 
3731  81 
qed "rvimage_id"; 
991  82 

83 
(* used only in Hartog.ML *) 

84 
goal Cardinal.thy 

1461  85 
"!!A r. well_ord(A,r) ==> ordertype(A, r Int A*A) = ordertype(A,r)"; 
991  86 
by (res_inst_tac [("P","%a. ordertype(A,a)=ordertype(A,r)")] 
87 
(rvimage_id RS subst) 1); 

88 
by (eresolve_tac [id_bij RS bij_ordertype_vimage] 1); 

3731  89 
qed "ordertype_Int"; 
991  90 

91 
(* used only in AC16_lemmas.ML *) 

92 
goalw CardinalArith.thy [InfCard_def] 

1461  93 
"!!i. [ ~Finite(i); Card(i) ] ==> InfCard(i)"; 
4091  94 
by (asm_simp_tac (simpset() addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1); 
3731  95 
qed "Inf_Card_is_InfCard"; 
1123  96 

5068  97 
Goal "(THE z. {x}={z}) = x"; 
4091  98 
by (fast_tac (claset() addSIs [the_equality] 
1461  99 
addSEs [singleton_eq_iff RS iffD1 RS sym]) 1); 
3731  100 
qed "the_element"; 
1123  101 

5068  102 
Goal "(lam x:A. {x}) : bij(A, {{x}. x:A})"; 
1123  103 
by (res_inst_tac [("d","%z. THE x. z={x}")] lam_bijective 1); 
104 
by (TRYALL (eresolve_tac [RepFunI, RepFunE])); 

4091  105 
by (REPEAT (asm_full_simp_tac (simpset() addsimps [the_element]) 1)); 
3731  106 
qed "lam_sing_bij"; 
1123  107 

108 
val [major,minor] = goal thy 

1461  109 
"[ f : Pi(A,B); (!!x. x:A ==> B(x)<=C(x)) ] ==> f : Pi(A,C)"; 
4091  110 
by (fast_tac (claset() addSIs [major RS Pi_type, minor RS subsetD, 
1461  111 
major RS apply_type]) 1); 
3731  112 
qed "Pi_weaken_type"; 
1123  113 

114 
val [major, minor] = goalw thy [inj_def] 

1461  115 
"[ f:inj(A, B); (!!a. a:A ==> f`a : C) ] ==> f:inj(A,C)"; 
4091  116 
by (fast_tac (claset() addSEs [minor] 
1461  117 
addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1); 
3731  118 
qed "inj_strengthen_type"; 
1123  119 

5137  120 
Goalw [Finite_def] "n:nat ==> Finite(n)"; 
4091  121 
by (fast_tac (claset() addSIs [eqpoll_refl]) 1); 
3731  122 
qed "nat_into_Finite"; 
1196  123 

5068  124 
Goalw [Finite_def] "~Finite(nat)"; 
4091  125 
by (fast_tac (claset() addSDs [eqpoll_imp_lepoll] 
1461  126 
addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1); 
3731  127 
qed "nat_not_Finite"; 
1196  128 

129 
val le_imp_lepoll = le_imp_subset RS subset_imp_lepoll; 

130 

131 
(* ********************************************************************** *) 

1461  132 
(* Another elimination rule for EX! *) 
1196  133 
(* ********************************************************************** *) 
134 

5137  135 
Goal "[ EX! x. P(x); P(x); P(y) ] ==> x=y"; 
1207  136 
by (etac ex1E 1); 
1196  137 
by (res_inst_tac [("b","xa")] (sym RSN (2, trans)) 1); 
2469  138 
by (Fast_tac 1); 
139 
by (Fast_tac 1); 

3731  140 
qed "ex1_two_eq"; 
1196  141 

142 
(* ********************************************************************** *) 

1461  143 
(* image of a surjection *) 
1196  144 
(* ********************************************************************** *) 
145 

5137  146 
Goalw [surj_def] "f : surj(A, B) ==> f``A = B"; 
1207  147 
by (etac CollectE 1); 
2496  148 
by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 
149 
THEN (assume_tac 1)); 

4091  150 
by (fast_tac (claset() addSEs [apply_type] addIs [equalityI]) 1); 
3731  151 
qed "surj_image_eq"; 
1196  152 

153 

5137  154 
Goal "succ(x) lepoll y ==> y ~= 0"; 
4091  155 
by (fast_tac (claset() addSDs [lepoll_0_is_0]) 1); 
3731  156 
qed "succ_lepoll_imp_not_empty"; 
1196  157 

5137  158 
Goal "x eqpoll succ(n) ==> x ~= 0"; 
4091  159 
by (fast_tac (claset() addSEs [eqpoll_sym RS eqpoll_0_is_0 RS succ_neq_0]) 1); 
3731  160 
qed "eqpoll_succ_imp_not_empty"; 
1196  161 