0

1 
(* Title: ZF/ordinal.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


6 
For ordinal.thy. Ordinals in ZermeloFraenkel Set Theory


7 
*)


8 


9 
open Ord;


10 


11 
(*** Rules for Transset ***)


12 


13 
(** Two neat characterisations of Transset **)


14 


15 
goalw Ord.thy [Transset_def] "Transset(A) <> A<=Pow(A)";


16 
by (fast_tac ZF_cs 1);


17 
val Transset_iff_Pow = result();


18 


19 
goalw Ord.thy [Transset_def] "Transset(A) <> Union(succ(A)) = A";


20 
by (fast_tac (eq_cs addSEs [equalityE]) 1);


21 
val Transset_iff_Union_succ = result();


22 


23 
(** Consequences of downwards closure **)


24 


25 
goalw Ord.thy [Transset_def]


26 
"!!C a b. [ Transset(C); {a,b}: C ] ==> a:C & b: C";


27 
by (fast_tac ZF_cs 1);


28 
val Transset_doubleton_D = result();


29 


30 
val [prem1,prem2] = goalw Ord.thy [Pair_def]


31 
"[ Transset(C); <a,b>: C ] ==> a:C & b: C";


32 
by (cut_facts_tac [prem2] 1);


33 
by (fast_tac (ZF_cs addSDs [prem1 RS Transset_doubleton_D]) 1);


34 
val Transset_Pair_D = result();


35 


36 
val prem1::prems = goal Ord.thy


37 
"[ Transset(C); A*B <= C; b: B ] ==> A <= C";


38 
by (cut_facts_tac prems 1);


39 
by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1);


40 
val Transset_includes_domain = result();


41 


42 
val prem1::prems = goal Ord.thy


43 
"[ Transset(C); A*B <= C; a: A ] ==> B <= C";


44 
by (cut_facts_tac prems 1);


45 
by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1);


46 
val Transset_includes_range = result();


47 


48 
val [prem1,prem2] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def]


49 
"[ Transset(C); A+B <= C ] ==> A <= C & B <= C";


50 
br (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1;


51 
by (REPEAT (etac (prem1 RS Transset_includes_range) 1


52 
ORELSE resolve_tac [conjI, singletonI] 1));


53 
val Transset_includes_summands = result();


54 


55 
val [prem] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def]


56 
"Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";


57 
br (Int_Un_distrib RS ssubst) 1;


58 
by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1);


59 
val Transset_sum_Int_subset = result();


60 


61 
(** Closure properties **)


62 


63 
goalw Ord.thy [Transset_def] "Transset(0)";


64 
by (fast_tac ZF_cs 1);


65 
val Transset_0 = result();


66 


67 
goalw Ord.thy [Transset_def]


68 
"!!i j. [ Transset(i); Transset(j) ] ==> Transset(i Un j)";


69 
by (fast_tac ZF_cs 1);


70 
val Transset_Un = result();


71 


72 
goalw Ord.thy [Transset_def]


73 
"!!i j. [ Transset(i); Transset(j) ] ==> Transset(i Int j)";


74 
by (fast_tac ZF_cs 1);


75 
val Transset_Int = result();


76 


77 
goalw Ord.thy [Transset_def] "!!i. Transset(i) ==> Transset(succ(i))";


78 
by (fast_tac ZF_cs 1);


79 
val Transset_succ = result();


80 


81 
goalw Ord.thy [Transset_def] "!!i. Transset(i) ==> Transset(Pow(i))";


82 
by (fast_tac ZF_cs 1);


83 
val Transset_Pow = result();


84 


85 
goalw Ord.thy [Transset_def] "!!A. Transset(A) ==> Transset(Union(A))";


86 
by (fast_tac ZF_cs 1);


87 
val Transset_Union = result();


88 


89 
val [Transprem] = goalw Ord.thy [Transset_def]


90 
"[ !!i. i:A ==> Transset(i) ] ==> Transset(Union(A))";


91 
by (fast_tac (ZF_cs addEs [Transprem RS bspec RS subsetD]) 1);


92 
val Transset_Union_family = result();


93 


94 
val [prem,Transprem] = goalw Ord.thy [Transset_def]


95 
"[ j:A; !!i. i:A ==> Transset(i) ] ==> Transset(Inter(A))";


96 
by (cut_facts_tac [prem] 1);


97 
by (fast_tac (ZF_cs addEs [Transprem RS bspec RS subsetD]) 1);


98 
val Transset_Inter_family = result();


99 


100 
(*** Natural Deduction rules for Ord ***)


101 


102 
val prems = goalw Ord.thy [Ord_def]


103 
"[ Transset(i); !!x. x:i ==> Transset(x) ] ==> Ord(i) ";


104 
by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));


105 
val OrdI = result();


106 


107 
val [major] = goalw Ord.thy [Ord_def]


108 
"Ord(i) ==> Transset(i)";


109 
by (rtac (major RS conjunct1) 1);


110 
val Ord_is_Transset = result();


111 


112 
val [major,minor] = goalw Ord.thy [Ord_def]


113 
"[ Ord(i); j:i ] ==> Transset(j) ";


114 
by (rtac (minor RS (major RS conjunct2 RS bspec)) 1);


115 
val Ord_contains_Transset = result();


116 


117 
(*** Lemmas for ordinals ***)


118 


119 
goalw Ord.thy [Ord_def,Transset_def] "!!i j. [ Ord(i); j:i ] ==> Ord(j) ";


120 
by (fast_tac ZF_cs 1);


121 
val Ord_in_Ord = result();


122 


123 
goal Ord.thy "!!i j. [ Ord(i); Transset(j); j<=i ] ==> Ord(j)";


124 
by (REPEAT (ares_tac [OrdI] 1


125 
ORELSE eresolve_tac [Ord_contains_Transset, subsetD] 1));


126 
val Ord_subset_Ord = result();


127 


128 
goalw Ord.thy [Ord_def,Transset_def] "!!i j. [ j:i; Ord(i) ] ==> j<=i";


129 
by (fast_tac ZF_cs 1);


130 
val OrdmemD = result();


131 


132 
goal Ord.thy "!!i j k. [ i:j; j:k; Ord(k) ] ==> i:k";


133 
by (REPEAT (ares_tac [OrdmemD RS subsetD] 1));


134 
val Ord_trans = result();


135 


136 
goal Ord.thy "!!i j. [ i:j; Ord(j) ] ==> succ(i) <= j";


137 
by (REPEAT (ares_tac [OrdmemD RSN (2,succ_subsetI)] 1));


138 
val Ord_succ_subsetI = result();


139 


140 


141 
(*** The construction of ordinals: 0, succ, Union ***)


142 


143 
goal Ord.thy "Ord(0)";


144 
by (REPEAT (ares_tac [OrdI,Transset_0] 1 ORELSE etac emptyE 1));


145 
val Ord_0 = result();


146 


147 
goal Ord.thy "!!i. Ord(i) ==> Ord(succ(i))";


148 
by (REPEAT (ares_tac [OrdI,Transset_succ] 1


149 
ORELSE eresolve_tac [succE,ssubst,Ord_is_Transset,


150 
Ord_contains_Transset] 1));


151 
val Ord_succ = result();


152 


153 
val nonempty::prems = goal Ord.thy


154 
"[ j:A; !!i. i:A ==> Ord(i) ] ==> Ord(Inter(A))";


155 
by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1);


156 
by (rtac Ord_is_Transset 1);


157 
by (REPEAT (ares_tac ([Ord_contains_Transset,nonempty]@prems) 1


158 
ORELSE etac InterD 1));


159 
val Ord_Inter = result();


160 


161 
val jmemA::prems = goal Ord.thy


162 
"[ j:A; !!x. x:A ==> Ord(B(x)) ] ==> Ord(INT x:A. B(x))";


163 
by (rtac (jmemA RS RepFunI RS Ord_Inter) 1);


164 
by (etac RepFunE 1);


165 
by (etac ssubst 1);


166 
by (eresolve_tac prems 1);


167 
val Ord_INT = result();


168 


169 


170 
(*** Natural Deduction rules for Memrel ***)


171 


172 
goalw Ord.thy [Memrel_def] "<a,b> : Memrel(A) <> a:b & a:A & b:A";


173 
by (fast_tac ZF_cs 1);


174 
val Memrel_iff = result();


175 


176 
val prems = goal Ord.thy "[ a: b; a: A; b: A ] ==> <a,b> : Memrel(A)";


177 
by (REPEAT (resolve_tac (prems@[conjI, Memrel_iff RS iffD2]) 1));


178 
val MemrelI = result();


179 


180 
val [major,minor] = goal Ord.thy


181 
"[ <a,b> : Memrel(A); \


182 
\ [ a: A; b: A; a:b ] ==> P \


183 
\ ] ==> P";


184 
by (rtac (major RS (Memrel_iff RS iffD1) RS conjE) 1);


185 
by (etac conjE 1);


186 
by (rtac minor 1);


187 
by (REPEAT (assume_tac 1));


188 
val MemrelE = result();


189 


190 
(*The membership relation (as a set) is wellfounded.


191 
Proof idea: show A<=B by applying the foundation axiom to AB *)


192 
goalw Ord.thy [wf_def] "wf(Memrel(A))";


193 
by (EVERY1 [rtac (foundation RS disjE RS allI),


194 
etac disjI1,


195 
etac bexE,


196 
rtac (impI RS allI RS bexI RS disjI2),


197 
etac MemrelE,


198 
etac bspec,


199 
REPEAT o assume_tac]);


200 
val wf_Memrel = result();


201 


202 
(*** Transfinite induction ***)


203 


204 
(*Epsilon induction over a transitive set*)


205 
val major::prems = goalw Ord.thy [Transset_def]


206 
"[ i: k; Transset(k); \


207 
\ !!x.[ x: k; ALL y:x. P(y) ] ==> P(x) \


208 
\ ] ==> P(i)";


209 
by (rtac (major RS (wf_Memrel RS wf_induct2)) 1);


210 
by (fast_tac (ZF_cs addEs [MemrelE]) 1);


211 
by (resolve_tac prems 1);


212 
by (assume_tac 1);


213 
by (cut_facts_tac prems 1);


214 
by (fast_tac (ZF_cs addIs [MemrelI]) 1);


215 
val Transset_induct = result();


216 


217 
(*Induction over an ordinal*)


218 
val Ord_induct = Ord_is_Transset RSN (2, Transset_induct);


219 


220 
(*Induction over the class of ordinals  a useful corollary of Ord_induct*)


221 
val [major,indhyp] = goal Ord.thy


222 
"[ Ord(i); \


223 
\ !!x.[ Ord(x); ALL y:x. P(y) ] ==> P(x) \


224 
\ ] ==> P(i)";


225 
by (rtac (major RS Ord_succ RS (succI1 RS Ord_induct)) 1);


226 
by (rtac indhyp 1);


227 
by (rtac (major RS Ord_succ RS Ord_in_Ord) 1);


228 
by (REPEAT (assume_tac 1));


229 
val trans_induct = result();


230 


231 
(*Perform induction on i, then prove the Ord(i) subgoal using prems. *)


232 
fun trans_ind_tac a prems i =


233 
EVERY [res_inst_tac [("i",a)] trans_induct i,


234 
rename_last_tac a ["1"] (i+1),


235 
ares_tac prems i];


236 


237 


238 
(*** Fundamental properties of the epsilon ordering (< on ordinals) ***)


239 


240 
(*Finds contradictions for the following proof*)


241 
val Ord_trans_tac = EVERY' [etac notE, etac Ord_trans, REPEAT o atac];


242 


243 
(** Proving that "member" is a linear ordering on the ordinals **)


244 


245 
val prems = goal Ord.thy


246 
"Ord(i) ==> (ALL j. Ord(j) > i:j  i=j  j:i)";


247 
by (trans_ind_tac "i" prems 1);


248 
by (rtac (impI RS allI) 1);


249 
by (trans_ind_tac "j" [] 1);


250 
by (DEPTH_SOLVE (swap_res_tac [disjCI,equalityI,subsetI] 1


251 
ORELSE ball_tac 1


252 
ORELSE eresolve_tac [impE,disjE,allE] 1


253 
ORELSE hyp_subst_tac 1


254 
ORELSE Ord_trans_tac 1));


255 
val Ord_linear_lemma = result();


256 


257 
val ordi::ordj::prems = goal Ord.thy


258 
"[ Ord(i); Ord(j); i:j ==> P; i=j ==> P; j:i ==> P ] \


259 
\ ==> P";


260 
by (rtac (ordi RS Ord_linear_lemma RS spec RS impE) 1);


261 
by (rtac ordj 1);


262 
by (REPEAT (eresolve_tac (prems@[asm_rl,disjE]) 1));


263 
val Ord_linear = result();


264 


265 
val prems = goal Ord.thy


266 
"[ Ord(i); Ord(j); i<=j ==> P; j<=i ==> P ] \


267 
\ ==> P";


268 
by (res_inst_tac [("i","i"),("j","j")] Ord_linear 1);


269 
by (DEPTH_SOLVE (ares_tac (prems@[subset_refl]) 1


270 
ORELSE eresolve_tac [asm_rl,OrdmemD,ssubst] 1));


271 
val Ord_subset = result();


272 


273 
goal Ord.thy "!!i j. [ j<=i; ~ i<=j; Ord(i); Ord(j) ] ==> j:i";


274 
by (etac Ord_linear 1);


275 
by (REPEAT (ares_tac [subset_refl] 1


276 
ORELSE eresolve_tac [notE,OrdmemD,ssubst] 1));


277 
val Ord_member = result();


278 


279 
val [prem] = goal Ord.thy "Ord(i) ==> 0: succ(i)";


280 
by (rtac (empty_subsetI RS Ord_member) 1);


281 
by (fast_tac ZF_cs 1);


282 
by (rtac (prem RS Ord_succ) 1);


283 
by (rtac Ord_0 1);


284 
val Ord_0_mem_succ = result();


285 


286 
goal Ord.thy "!!i j. [ Ord(i); Ord(j) ] ==> j:i <> j<=i & ~(i<=j)";


287 
by (rtac iffI 1);


288 
by (rtac conjI 1);


289 
by (etac OrdmemD 1);


290 
by (rtac (mem_anti_refl RS notI) 2);


291 
by (etac subsetD 2);


292 
by (REPEAT (eresolve_tac [asm_rl, conjE, Ord_member] 1));


293 
val Ord_member_iff = result();


294 


295 
goal Ord.thy "!!i. Ord(i) ==> 0:i <> ~ i=0";


296 
be (Ord_0 RSN (2,Ord_member_iff) RS iff_trans) 1;


297 
by (fast_tac eq_cs 1);


298 
val Ord_0_member_iff = result();


299 


300 
(** For ordinals, i: succ(j) means 'lessthan or equals' **)


301 


302 
goal Ord.thy "!!i j. [ j<=i; Ord(i); Ord(j) ] ==> j : succ(i)";


303 
by (rtac Ord_member 1);


304 
by (REPEAT (ares_tac [Ord_succ] 3));


305 
by (rtac (mem_anti_refl RS notI) 2);


306 
by (etac subsetD 2);


307 
by (ALLGOALS (fast_tac ZF_cs));


308 
val member_succI = result();


309 


310 
goalw Ord.thy [Transset_def,Ord_def]


311 
"!!i j. [ i : succ(j); Ord(j) ] ==> i<=j";


312 
by (fast_tac ZF_cs 1);


313 
val member_succD = result();


314 


315 
goal Ord.thy "!!i j. [ Ord(i); Ord(j) ] ==> j:succ(i) <> j<=i";


316 
by (fast_tac (subset_cs addSEs [member_succI, member_succD]) 1);


317 
val member_succ_iff = result();


318 


319 
goal Ord.thy


320 
"!!i j. [ Ord(i); Ord(j) ] ==> i<=succ(j) <> i<=j  i=succ(j)";


321 
by (ASM_SIMP_TAC (ZF_ss addrews [member_succ_iff RS iff_sym, Ord_succ]) 1);


322 
by (fast_tac ZF_cs 1);


323 
val subset_succ_iff = result();


324 


325 
goal Ord.thy "!!i j. [ i:succ(j); j:k; Ord(k) ] ==> i:k";


326 
by (fast_tac (ZF_cs addEs [Ord_trans]) 1);


327 
val Ord_trans1 = result();


328 


329 
goal Ord.thy "!!i j. [ i:j; j:succ(k); Ord(k) ] ==> i:k";


330 
by (fast_tac (ZF_cs addEs [Ord_trans]) 1);


331 
val Ord_trans2 = result();


332 


333 
goal Ord.thy "!!i jk. [ i:j; j<=k; Ord(k) ] ==> i:k";


334 
by (fast_tac (ZF_cs addEs [Ord_trans]) 1);


335 
val Ord_transsub2 = result();


336 


337 
goal Ord.thy "!!i j. [ i:j; Ord(j) ] ==> succ(i) : succ(j)";


338 
by (rtac member_succI 1);


339 
by (REPEAT (ares_tac [subsetI,Ord_succ,Ord_in_Ord] 1


340 
ORELSE eresolve_tac [succE,Ord_trans,ssubst] 1));


341 
val succ_mem_succI = result();


342 


343 
goal Ord.thy "!!i j. [ succ(i) : succ(j); Ord(j) ] ==> i:j";


344 
by (REPEAT (eresolve_tac [asm_rl, make_elim member_succD, succ_subsetE] 1));


345 
val succ_mem_succE = result();


346 


347 
goal Ord.thy "!!i j. Ord(j) ==> succ(i) : succ(j) <> i:j";


348 
by (REPEAT (ares_tac [iffI,succ_mem_succI,succ_mem_succE] 1));


349 
val succ_mem_succ_iff = result();


350 


351 
goal Ord.thy "!!i j. [ i<=j; Ord(i); Ord(j) ] ==> succ(i) <= succ(j)";


352 
by (rtac (member_succI RS succ_mem_succI RS member_succD) 1);


353 
by (REPEAT (ares_tac [Ord_succ] 1));


354 
val Ord_succ_mono = result();


355 


356 
goal Ord.thy "!!i j k. [ i:k; j:k; Ord(k) ] ==> i Un j : k";


357 
by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);


358 
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));


359 
by (ASM_SIMP_TAC (ZF_ss addrews [subset_Un_iff RS iffD1]) 1);


360 
by (rtac (Un_commute RS ssubst) 1);


361 
by (ASM_SIMP_TAC (ZF_ss addrews [subset_Un_iff RS iffD1]) 1);


362 
val Ord_member_UnI = result();


363 


364 
goal Ord.thy "!!i j k. [ i:k; j:k; Ord(k) ] ==> i Int j : k";


365 
by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);


366 
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));


367 
by (ASM_SIMP_TAC (ZF_ss addrews [subset_Int_iff RS iffD1]) 1);


368 
by (rtac (Int_commute RS ssubst) 1);


369 
by (ASM_SIMP_TAC (ZF_ss addrews [subset_Int_iff RS iffD1]) 1);


370 
val Ord_member_IntI = result();


371 


372 


373 
(*** Results about limits ***)


374 


375 
val prems = goal Ord.thy "[ !!i. i:A ==> Ord(i) ] ==> Ord(Union(A))";


376 
by (rtac (Ord_is_Transset RS Transset_Union_family RS OrdI) 1);


377 
by (REPEAT (etac UnionE 1 ORELSE ares_tac ([Ord_contains_Transset]@prems) 1));


378 
val Ord_Union = result();


379 


380 
val prems = goal Ord.thy "[ !!x. x:A ==> Ord(B(x)) ] ==> Ord(UN x:A. B(x))";


381 
by (rtac Ord_Union 1);


382 
by (etac RepFunE 1);


383 
by (etac ssubst 1);


384 
by (eresolve_tac prems 1);


385 
val Ord_UN = result();


386 


387 
(*The upper bound must be a successor ordinal 


388 
consider that (UN i:nat.i)=nat although nat is an upper bound of each i*)


389 
val [ordi,limit] = goal Ord.thy


390 
"[ Ord(i); !!y. y:A ==> f(y): succ(i) ] ==> (UN y:A. f(y)) : succ(i)";


391 
by (rtac (member_succD RS UN_least RS member_succI) 1);


392 
by (REPEAT (ares_tac [ordi, Ord_UN, ordi RS Ord_succ RS Ord_in_Ord,


393 
limit] 1));


394 
val sup_least = result();


395 


396 
val [jmemi,ordi,limit] = goal Ord.thy


397 
"[ j: i; Ord(i); !!y. y:A ==> f(y): j ] ==> (UN y:A. succ(f(y))) : i";


398 
by (cut_facts_tac [jmemi RS (ordi RS Ord_in_Ord)] 1);


399 
by (rtac (sup_least RS Ord_trans2) 1);


400 
by (REPEAT (ares_tac [jmemi, ordi, succ_mem_succI, limit] 1));


401 
val sup_least2 = result();


402 


403 
goal Ord.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i";


404 
by (fast_tac (eq_cs addSEs [Ord_trans1]) 1);


405 
val Ord_equality = result();


406 


407 
(*Holds for all transitive sets, not just ordinals*)


408 
goal Ord.thy "!!i. Ord(i) ==> Union(i) <= i";


409 
by (fast_tac (ZF_cs addSEs [Ord_trans]) 1);


410 
val Ord_Union_subset = result();
