author | wenzelm |
Mon, 08 May 2000 10:52:46 +0200 | |
changeset 8824 | ff207088cf0c |
parent 8123 | a71686059be0 |
child 9683 | f87c8c449018 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/AC_Equiv.ML |
991 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
991 | 4 |
|
5 |
*) |
|
6 |
||
1071 | 7 |
val WO_defs = [WO1_def, WO2_def, WO3_def, WO4_def, WO5_def, WO6_def, WO8_def]; |
8 |
||
9 |
val AC_defs = [AC0_def, AC1_def, AC2_def, AC3_def, AC4_def, AC5_def, |
|
10 |
AC6_def, AC7_def, AC8_def, AC9_def, AC10_def, AC11_def, |
|
11 |
AC12_def, AC13_def, AC14_def, AC15_def, AC16_def, |
|
12 |
AC17_def, AC18_def, AC19_def]; |
|
13 |
||
991 | 14 |
val AC_aux_defs = [pairwise_disjoint_def, sets_of_size_between_def]; |
1123 | 15 |
|
991 | 16 |
|
17 |
(* ********************************************************************** *) |
|
18 |
(* lemmas concerning FOL and pure ZF theory *) |
|
19 |
(* ********************************************************************** *) |
|
20 |
||
5137 | 21 |
Goal "(A->X)=0 ==> X=0"; |
5470 | 22 |
by (fast_tac (claset() addSIs [equals0I] addIs [lam_type]) 1); |
3731 | 23 |
qed "fun_space_emptyD"; |
991 | 24 |
|
25 |
(* used only in WO1_DC.ML *) |
|
26 |
(*Note simpler proof*) |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5265
diff
changeset
|
27 |
Goal "[| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; A<=Df; A<=Dg |] ==> f``A=g``A"; |
4091 | 28 |
by (asm_simp_tac (simpset() addsimps [image_fun]) 1); |
3731 | 29 |
qed "images_eq"; |
991 | 30 |
|
31 |
(* used in : AC10-AC15.ML AC16WO4.ML WO6WO1.ML *) |
|
32 |
(*I don't know where to put this one.*) |
|
33 |
goal Cardinal.thy |
|
34 |
"!!m A B. [| A lepoll succ(m); B<=A; B~=0 |] ==> A-B lepoll m"; |
|
1207 | 35 |
by (rtac not_emptyE 1 THEN (assume_tac 1)); |
7499 | 36 |
by (ftac singleton_subsetI 1); |
37 |
by (ftac subsetD 1 THEN (assume_tac 1)); |
|
991 | 38 |
by (res_inst_tac [("A2","A")] |
1057 | 39 |
(Diff_sing_lepoll RSN (2, subset_imp_lepoll RS lepoll_trans)) 1 |
1196 | 40 |
THEN (REPEAT (assume_tac 2))); |
2469 | 41 |
by (Fast_tac 1); |
3731 | 42 |
qed "Diff_lepoll"; |
991 | 43 |
|
44 |
(* ********************************************************************** *) |
|
45 |
(* lemmas concerning lepoll and eqpoll relations *) |
|
46 |
(* ********************************************************************** *) |
|
47 |
||
48 |
(* ********************************************************************** *) |
|
49 |
(* Theorems concerning ordinals *) |
|
50 |
(* ********************************************************************** *) |
|
51 |
||
52 |
(* lemma for ordertype_Int *) |
|
53 |
goalw Cardinal.thy [rvimage_def] "rvimage(A,id(A),r) = r Int A*A"; |
|
1207 | 54 |
by (rtac equalityI 1); |
3731 | 55 |
by Safe_tac; |
991 | 56 |
by (dres_inst_tac [("P","%a. <id(A)`xb,a>:r")] (id_conv RS subst) 1 |
1196 | 57 |
THEN (assume_tac 1)); |
991 | 58 |
by (dres_inst_tac [("P","%a. <a,ya>:r")] (id_conv RS subst) 1 |
1196 | 59 |
THEN (REPEAT (assume_tac 1))); |
4091 | 60 |
by (fast_tac (claset() addIs [id_conv RS ssubst]) 1); |
3731 | 61 |
qed "rvimage_id"; |
991 | 62 |
|
63 |
(* used only in Hartog.ML *) |
|
64 |
goal Cardinal.thy |
|
1461 | 65 |
"!!A r. well_ord(A,r) ==> ordertype(A, r Int A*A) = ordertype(A,r)"; |
991 | 66 |
by (res_inst_tac [("P","%a. ordertype(A,a)=ordertype(A,r)")] |
67 |
(rvimage_id RS subst) 1); |
|
68 |
by (eresolve_tac [id_bij RS bij_ordertype_vimage] 1); |
|
3731 | 69 |
qed "ordertype_Int"; |
991 | 70 |
|
71 |
(* used only in AC16_lemmas.ML *) |
|
72 |
goalw CardinalArith.thy [InfCard_def] |
|
1461 | 73 |
"!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)"; |
4091 | 74 |
by (asm_simp_tac (simpset() addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1); |
3731 | 75 |
qed "Inf_Card_is_InfCard"; |
1123 | 76 |
|
5068 | 77 |
Goal "(THE z. {x}={z}) = x"; |
5505 | 78 |
by (fast_tac (claset() addSEs [singleton_eq_iff RS iffD1 RS sym]) 1); |
3731 | 79 |
qed "the_element"; |
1123 | 80 |
|
5068 | 81 |
Goal "(lam x:A. {x}) : bij(A, {{x}. x:A})"; |
1123 | 82 |
by (res_inst_tac [("d","%z. THE x. z={x}")] lam_bijective 1); |
83 |
by (TRYALL (eresolve_tac [RepFunI, RepFunE])); |
|
4091 | 84 |
by (REPEAT (asm_full_simp_tac (simpset() addsimps [the_element]) 1)); |
3731 | 85 |
qed "lam_sing_bij"; |
1123 | 86 |
|
87 |
val [major,minor] = goal thy |
|
1461 | 88 |
"[| f : Pi(A,B); (!!x. x:A ==> B(x)<=C(x)) |] ==> f : Pi(A,C)"; |
4091 | 89 |
by (fast_tac (claset() addSIs [major RS Pi_type, minor RS subsetD, |
1461 | 90 |
major RS apply_type]) 1); |
3731 | 91 |
qed "Pi_weaken_type"; |
1123 | 92 |
|
93 |
val [major, minor] = goalw thy [inj_def] |
|
1461 | 94 |
"[| f:inj(A, B); (!!a. a:A ==> f`a : C) |] ==> f:inj(A,C)"; |
4091 | 95 |
by (fast_tac (claset() addSEs [minor] |
1461 | 96 |
addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1); |
3731 | 97 |
qed "inj_strengthen_type"; |
1123 | 98 |
|
5068 | 99 |
Goalw [Finite_def] "~Finite(nat)"; |
4091 | 100 |
by (fast_tac (claset() addSDs [eqpoll_imp_lepoll] |
1461 | 101 |
addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1); |
3731 | 102 |
qed "nat_not_Finite"; |
1196 | 103 |
|
104 |
val le_imp_lepoll = le_imp_subset RS subset_imp_lepoll; |
|
105 |
||
106 |
(* ********************************************************************** *) |
|
1461 | 107 |
(* Another elimination rule for EX! *) |
1196 | 108 |
(* ********************************************************************** *) |
109 |
||
5137 | 110 |
Goal "[| EX! x. P(x); P(x); P(y) |] ==> x=y"; |
1207 | 111 |
by (etac ex1E 1); |
1196 | 112 |
by (res_inst_tac [("b","xa")] (sym RSN (2, trans)) 1); |
2469 | 113 |
by (Fast_tac 1); |
114 |
by (Fast_tac 1); |
|
3731 | 115 |
qed "ex1_two_eq"; |
1196 | 116 |
|
117 |
(* ********************************************************************** *) |
|
1461 | 118 |
(* image of a surjection *) |
1196 | 119 |
(* ********************************************************************** *) |
120 |
||
5137 | 121 |
Goalw [surj_def] "f : surj(A, B) ==> f``A = B"; |
1207 | 122 |
by (etac CollectE 1); |
2496 | 123 |
by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 |
124 |
THEN (assume_tac 1)); |
|
4091 | 125 |
by (fast_tac (claset() addSEs [apply_type] addIs [equalityI]) 1); |
3731 | 126 |
qed "surj_image_eq"; |
1196 | 127 |
|
128 |
||
5137 | 129 |
Goal "succ(x) lepoll y ==> y ~= 0"; |
4091 | 130 |
by (fast_tac (claset() addSDs [lepoll_0_is_0]) 1); |
3731 | 131 |
qed "succ_lepoll_imp_not_empty"; |
1196 | 132 |
|
5137 | 133 |
Goal "x eqpoll succ(n) ==> x ~= 0"; |
4091 | 134 |
by (fast_tac (claset() addSEs [eqpoll_sym RS eqpoll_0_is_0 RS succ_neq_0]) 1); |
3731 | 135 |
qed "eqpoll_succ_imp_not_empty"; |
1196 | 136 |