author | paulson |
Mon, 03 May 1999 11:19:08 +0200 | |
changeset 6566 | 7ed743d18af7 |
parent 6070 | 032babd0120b |
child 7499 | 23e090051cb8 |
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 |
||
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 |
(* lemmas concerning FOL and pure ZF theory *) |
|
22 |
(* ********************************************************************** *) |
|
23 |
||
5137 | 24 |
Goal "(A->X)=0 ==> X=0"; |
5470 | 25 |
by (fast_tac (claset() addSIs [equals0I] addIs [lam_type]) 1); |
3731 | 26 |
qed "fun_space_emptyD"; |
991 | 27 |
|
28 |
(* used only in WO1_DC.ML *) |
|
29 |
(*Note simpler proof*) |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5265
diff
changeset
|
30 |
Goal "[| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; A<=Df; A<=Dg |] ==> f``A=g``A"; |
4091 | 31 |
by (asm_simp_tac (simpset() addsimps [image_fun]) 1); |
3731 | 32 |
qed "images_eq"; |
991 | 33 |
|
34 |
(* used in : AC10-AC15.ML AC16WO4.ML WO6WO1.ML *) |
|
35 |
(*I don't know where to put this one.*) |
|
36 |
goal Cardinal.thy |
|
37 |
"!!m A B. [| A lepoll succ(m); B<=A; B~=0 |] ==> A-B lepoll m"; |
|
1207 | 38 |
by (rtac not_emptyE 1 THEN (assume_tac 1)); |
991 | 39 |
by (forward_tac [singleton_subsetI] 1); |
1196 | 40 |
by (forward_tac [subsetD] 1 THEN (assume_tac 1)); |
991 | 41 |
by (res_inst_tac [("A2","A")] |
1057 | 42 |
(Diff_sing_lepoll RSN (2, subset_imp_lepoll RS lepoll_trans)) 1 |
1196 | 43 |
THEN (REPEAT (assume_tac 2))); |
2469 | 44 |
by (Fast_tac 1); |
3731 | 45 |
qed "Diff_lepoll"; |
991 | 46 |
|
47 |
(* ********************************************************************** *) |
|
48 |
(* lemmas concerning lepoll and eqpoll relations *) |
|
49 |
(* ********************************************************************** *) |
|
50 |
||
51 |
(* ********************************************************************** *) |
|
52 |
(* Theorems concerning ordinals *) |
|
53 |
(* ********************************************************************** *) |
|
54 |
||
55 |
(* lemma for ordertype_Int *) |
|
56 |
goalw Cardinal.thy [rvimage_def] "rvimage(A,id(A),r) = r Int A*A"; |
|
1207 | 57 |
by (rtac equalityI 1); |
3731 | 58 |
by Safe_tac; |
991 | 59 |
by (dres_inst_tac [("P","%a. <id(A)`xb,a>:r")] (id_conv RS subst) 1 |
1196 | 60 |
THEN (assume_tac 1)); |
991 | 61 |
by (dres_inst_tac [("P","%a. <a,ya>:r")] (id_conv RS subst) 1 |
1196 | 62 |
THEN (REPEAT (assume_tac 1))); |
4091 | 63 |
by (fast_tac (claset() addIs [id_conv RS ssubst]) 1); |
3731 | 64 |
qed "rvimage_id"; |
991 | 65 |
|
66 |
(* used only in Hartog.ML *) |
|
67 |
goal Cardinal.thy |
|
1461 | 68 |
"!!A r. well_ord(A,r) ==> ordertype(A, r Int A*A) = ordertype(A,r)"; |
991 | 69 |
by (res_inst_tac [("P","%a. ordertype(A,a)=ordertype(A,r)")] |
70 |
(rvimage_id RS subst) 1); |
|
71 |
by (eresolve_tac [id_bij RS bij_ordertype_vimage] 1); |
|
3731 | 72 |
qed "ordertype_Int"; |
991 | 73 |
|
74 |
(* used only in AC16_lemmas.ML *) |
|
75 |
goalw CardinalArith.thy [InfCard_def] |
|
1461 | 76 |
"!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)"; |
4091 | 77 |
by (asm_simp_tac (simpset() addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1); |
3731 | 78 |
qed "Inf_Card_is_InfCard"; |
1123 | 79 |
|
5068 | 80 |
Goal "(THE z. {x}={z}) = x"; |
5505 | 81 |
by (fast_tac (claset() addSEs [singleton_eq_iff RS iffD1 RS sym]) 1); |
3731 | 82 |
qed "the_element"; |
1123 | 83 |
|
5068 | 84 |
Goal "(lam x:A. {x}) : bij(A, {{x}. x:A})"; |
1123 | 85 |
by (res_inst_tac [("d","%z. THE x. z={x}")] lam_bijective 1); |
86 |
by (TRYALL (eresolve_tac [RepFunI, RepFunE])); |
|
4091 | 87 |
by (REPEAT (asm_full_simp_tac (simpset() addsimps [the_element]) 1)); |
3731 | 88 |
qed "lam_sing_bij"; |
1123 | 89 |
|
90 |
val [major,minor] = goal thy |
|
1461 | 91 |
"[| f : Pi(A,B); (!!x. x:A ==> B(x)<=C(x)) |] ==> f : Pi(A,C)"; |
4091 | 92 |
by (fast_tac (claset() addSIs [major RS Pi_type, minor RS subsetD, |
1461 | 93 |
major RS apply_type]) 1); |
3731 | 94 |
qed "Pi_weaken_type"; |
1123 | 95 |
|
96 |
val [major, minor] = goalw thy [inj_def] |
|
1461 | 97 |
"[| f:inj(A, B); (!!a. a:A ==> f`a : C) |] ==> f:inj(A,C)"; |
4091 | 98 |
by (fast_tac (claset() addSEs [minor] |
1461 | 99 |
addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1); |
3731 | 100 |
qed "inj_strengthen_type"; |
1123 | 101 |
|
5137 | 102 |
Goalw [Finite_def] "n:nat ==> Finite(n)"; |
4091 | 103 |
by (fast_tac (claset() addSIs [eqpoll_refl]) 1); |
3731 | 104 |
qed "nat_into_Finite"; |
1196 | 105 |
|
5068 | 106 |
Goalw [Finite_def] "~Finite(nat)"; |
4091 | 107 |
by (fast_tac (claset() addSDs [eqpoll_imp_lepoll] |
1461 | 108 |
addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1); |
3731 | 109 |
qed "nat_not_Finite"; |
1196 | 110 |
|
111 |
val le_imp_lepoll = le_imp_subset RS subset_imp_lepoll; |
|
112 |
||
113 |
(* ********************************************************************** *) |
|
1461 | 114 |
(* Another elimination rule for EX! *) |
1196 | 115 |
(* ********************************************************************** *) |
116 |
||
5137 | 117 |
Goal "[| EX! x. P(x); P(x); P(y) |] ==> x=y"; |
1207 | 118 |
by (etac ex1E 1); |
1196 | 119 |
by (res_inst_tac [("b","xa")] (sym RSN (2, trans)) 1); |
2469 | 120 |
by (Fast_tac 1); |
121 |
by (Fast_tac 1); |
|
3731 | 122 |
qed "ex1_two_eq"; |
1196 | 123 |
|
124 |
(* ********************************************************************** *) |
|
1461 | 125 |
(* image of a surjection *) |
1196 | 126 |
(* ********************************************************************** *) |
127 |
||
5137 | 128 |
Goalw [surj_def] "f : surj(A, B) ==> f``A = B"; |
1207 | 129 |
by (etac CollectE 1); |
2496 | 130 |
by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 |
131 |
THEN (assume_tac 1)); |
|
4091 | 132 |
by (fast_tac (claset() addSEs [apply_type] addIs [equalityI]) 1); |
3731 | 133 |
qed "surj_image_eq"; |
1196 | 134 |
|
135 |
||
5137 | 136 |
Goal "succ(x) lepoll y ==> y ~= 0"; |
4091 | 137 |
by (fast_tac (claset() addSDs [lepoll_0_is_0]) 1); |
3731 | 138 |
qed "succ_lepoll_imp_not_empty"; |
1196 | 139 |
|
5137 | 140 |
Goal "x eqpoll succ(n) ==> x ~= 0"; |
4091 | 141 |
by (fast_tac (claset() addSEs [eqpoll_sym RS eqpoll_0_is_0 RS succ_neq_0]) 1); |
3731 | 142 |
qed "eqpoll_succ_imp_not_empty"; |
1196 | 143 |