author | wenzelm |
Mon, 16 Nov 1998 10:41:08 +0100 | |
changeset 5869 | b279a84ac11c |
parent 5505 | b0856ff6fc69 |
child 6070 | 032babd0120b |
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 |
(* 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 : AC10-AC15.ML WO1-WO6.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 : AC10-AC15.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 |] ==> A-B 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"; |
5505 | 98 |
by (fast_tac (claset() addSEs [singleton_eq_iff RS iffD1 RS sym]) 1); |
3731 | 99 |
qed "the_element"; |
1123 | 100 |
|
5068 | 101 |
Goal "(lam x:A. {x}) : bij(A, {{x}. x:A})"; |
1123 | 102 |
by (res_inst_tac [("d","%z. THE x. z={x}")] lam_bijective 1); |
103 |
by (TRYALL (eresolve_tac [RepFunI, RepFunE])); |
|
4091 | 104 |
by (REPEAT (asm_full_simp_tac (simpset() addsimps [the_element]) 1)); |
3731 | 105 |
qed "lam_sing_bij"; |
1123 | 106 |
|
107 |
val [major,minor] = goal thy |
|
1461 | 108 |
"[| f : Pi(A,B); (!!x. x:A ==> B(x)<=C(x)) |] ==> f : Pi(A,C)"; |
4091 | 109 |
by (fast_tac (claset() addSIs [major RS Pi_type, minor RS subsetD, |
1461 | 110 |
major RS apply_type]) 1); |
3731 | 111 |
qed "Pi_weaken_type"; |
1123 | 112 |
|
113 |
val [major, minor] = goalw thy [inj_def] |
|
1461 | 114 |
"[| f:inj(A, B); (!!a. a:A ==> f`a : C) |] ==> f:inj(A,C)"; |
4091 | 115 |
by (fast_tac (claset() addSEs [minor] |
1461 | 116 |
addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1); |
3731 | 117 |
qed "inj_strengthen_type"; |
1123 | 118 |
|
5137 | 119 |
Goalw [Finite_def] "n:nat ==> Finite(n)"; |
4091 | 120 |
by (fast_tac (claset() addSIs [eqpoll_refl]) 1); |
3731 | 121 |
qed "nat_into_Finite"; |
1196 | 122 |
|
5068 | 123 |
Goalw [Finite_def] "~Finite(nat)"; |
4091 | 124 |
by (fast_tac (claset() addSDs [eqpoll_imp_lepoll] |
1461 | 125 |
addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1); |
3731 | 126 |
qed "nat_not_Finite"; |
1196 | 127 |
|
128 |
val le_imp_lepoll = le_imp_subset RS subset_imp_lepoll; |
|
129 |
||
130 |
(* ********************************************************************** *) |
|
1461 | 131 |
(* Another elimination rule for EX! *) |
1196 | 132 |
(* ********************************************************************** *) |
133 |
||
5137 | 134 |
Goal "[| EX! x. P(x); P(x); P(y) |] ==> x=y"; |
1207 | 135 |
by (etac ex1E 1); |
1196 | 136 |
by (res_inst_tac [("b","xa")] (sym RSN (2, trans)) 1); |
2469 | 137 |
by (Fast_tac 1); |
138 |
by (Fast_tac 1); |
|
3731 | 139 |
qed "ex1_two_eq"; |
1196 | 140 |
|
141 |
(* ********************************************************************** *) |
|
1461 | 142 |
(* image of a surjection *) |
1196 | 143 |
(* ********************************************************************** *) |
144 |
||
5137 | 145 |
Goalw [surj_def] "f : surj(A, B) ==> f``A = B"; |
1207 | 146 |
by (etac CollectE 1); |
2496 | 147 |
by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 |
148 |
THEN (assume_tac 1)); |
|
4091 | 149 |
by (fast_tac (claset() addSEs [apply_type] addIs [equalityI]) 1); |
3731 | 150 |
qed "surj_image_eq"; |
1196 | 151 |
|
152 |
||
5137 | 153 |
Goal "succ(x) lepoll y ==> y ~= 0"; |
4091 | 154 |
by (fast_tac (claset() addSDs [lepoll_0_is_0]) 1); |
3731 | 155 |
qed "succ_lepoll_imp_not_empty"; |
1196 | 156 |
|
5137 | 157 |
Goal "x eqpoll succ(n) ==> x ~= 0"; |
4091 | 158 |
by (fast_tac (claset() addSEs [eqpoll_sym RS eqpoll_0_is_0 RS succ_neq_0]) 1); |
3731 | 159 |
qed "eqpoll_succ_imp_not_empty"; |
1196 | 160 |