src/ZF/Ord.ML
author lcp
Fri Sep 17 16:16:38 1993 +0200 (1993-09-17)
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 15 6c6d2f6e3185
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
     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 Zermelo-Fraenkel 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 well-founded.
   191   Proof idea: show A<=B by applying the foundation axiom to A-B *)
   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 'less-than 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 addsimps [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 addsimps [subset_Un_iff RS iffD1]) 1);
   360 by (rtac (Un_commute RS ssubst) 1);
   361 by (asm_simp_tac (ZF_ss addsimps [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 addsimps [subset_Int_iff RS iffD1]) 1);
   368 by (rtac (Int_commute RS ssubst) 1);
   369 by (asm_simp_tac (ZF_ss addsimps [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();