src/ZF/Epsilon.ML
author paulson
Fri Jan 29 17:08:20 1999 +0100 (1999-01-29)
changeset 6163 be8234f37e48
parent 6071 1b2392ac5752
child 8127 68c6159440f1
permissions -rw-r--r--
expandshort
     1 (*  Title:      ZF/epsilon.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Epsilon induction and recursion
     7 *)
     8 
     9 (*** Basic closure properties ***)
    10 
    11 Goalw [eclose_def] "A <= eclose(A)";
    12 by (rtac (nat_rec_0 RS equalityD2 RS subset_trans) 1);
    13 by (rtac (nat_0I RS UN_upper) 1);
    14 qed "arg_subset_eclose";
    15 
    16 val arg_into_eclose = arg_subset_eclose RS subsetD;
    17 
    18 Goalw [eclose_def,Transset_def] "Transset(eclose(A))";
    19 by (rtac (subsetI RS ballI) 1);
    20 by (etac UN_E 1);
    21 by (rtac (nat_succI RS UN_I) 1);
    22 by (assume_tac 1);
    23 by (etac (nat_rec_succ RS ssubst) 1);
    24 by (etac UnionI 1);
    25 by (assume_tac 1);
    26 qed "Transset_eclose";
    27 
    28 (* x : eclose(A) ==> x <= eclose(A) *)
    29 bind_thm ("eclose_subset",
    30     rewrite_rule [Transset_def] Transset_eclose RS bspec);
    31 
    32 (* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
    33 bind_thm ("ecloseD", eclose_subset RS subsetD);
    34 
    35 val arg_in_eclose_sing = arg_subset_eclose RS singleton_subsetD;
    36 val arg_into_eclose_sing = arg_in_eclose_sing RS ecloseD;
    37 
    38 (* This is epsilon-induction for eclose(A); see also eclose_induct_down...
    39    [| a: eclose(A);  !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) 
    40    |] ==> P(a) 
    41 *)
    42 bind_thm ("eclose_induct", Transset_eclose RSN (2, Transset_induct));
    43 
    44 (*Epsilon induction*)
    45 val prems = goal Epsilon.thy
    46     "[| !!x. ALL y:x. P(y) ==> P(x) |]  ==>  P(a)";
    47 by (rtac (arg_in_eclose_sing RS eclose_induct) 1);
    48 by (eresolve_tac prems 1);
    49 qed "eps_induct";
    50 
    51 (*Perform epsilon-induction on i. *)
    52 fun eps_ind_tac a = 
    53     EVERY' [res_inst_tac [("a",a)] eps_induct,
    54             rename_last_tac a ["1"]];
    55 
    56 
    57 (*** Leastness of eclose ***)
    58 
    59 (** eclose(A) is the least transitive set including A as a subset. **)
    60 
    61 Goalw [Transset_def]
    62     "[| Transset(X);  A<=X;  n: nat |] ==> \
    63 \             nat_rec(n, A, %m r. Union(r)) <= X";
    64 by (etac nat_induct 1);
    65 by (asm_simp_tac (simpset() addsimps [nat_rec_0]) 1);
    66 by (asm_simp_tac (simpset() addsimps [nat_rec_succ]) 1);
    67 by (Blast_tac 1);
    68 qed "eclose_least_lemma";
    69 
    70 Goalw [eclose_def]
    71      "[| Transset(X);  A<=X |] ==> eclose(A) <= X";
    72 by (rtac (eclose_least_lemma RS UN_least) 1);
    73 by (REPEAT (assume_tac 1));
    74 qed "eclose_least";
    75 
    76 (*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
    77 val [major,base,step] = goal Epsilon.thy
    78     "[| a: eclose(b);                                           \
    79 \       !!y.   [| y: b |] ==> P(y);                             \
    80 \       !!y z. [| y: eclose(b);  P(y);  z: y |] ==> P(z)        \
    81 \    |] ==> P(a)";
    82 by (rtac (major RSN (3, eclose_least RS subsetD RS CollectD2)) 1);
    83 by (rtac (CollectI RS subsetI) 2);
    84 by (etac (arg_subset_eclose RS subsetD) 2);
    85 by (etac base 2);
    86 by (rewtac Transset_def);
    87 by (blast_tac (claset() addIs [step,ecloseD]) 1);
    88 qed "eclose_induct_down";
    89 
    90 Goal "Transset(X) ==> eclose(X) = X";
    91 by (etac ([eclose_least, arg_subset_eclose] MRS equalityI) 1);
    92 by (rtac subset_refl 1);
    93 qed "Transset_eclose_eq_arg";
    94 
    95 
    96 (*** Epsilon recursion ***)
    97 
    98 (*Unused...*)
    99 Goal "[| A: eclose(B);  B: eclose(C) |] ==> A: eclose(C)";
   100 by (rtac ([Transset_eclose, eclose_subset] MRS eclose_least RS subsetD) 1);
   101 by (REPEAT (assume_tac 1));
   102 qed "mem_eclose_trans";
   103 
   104 (*Variant of the previous lemma in a useable form for the sequel*)
   105 Goal "[| A: eclose({B});  B: eclose({C}) |] ==> A: eclose({C})";
   106 by (rtac ([Transset_eclose, singleton_subsetI] MRS eclose_least RS subsetD) 1);
   107 by (REPEAT (assume_tac 1));
   108 qed "mem_eclose_sing_trans";
   109 
   110 Goalw [Transset_def]
   111     "[| Transset(i);  j:i |] ==> Memrel(i)-``{j} = j";
   112 by (blast_tac (claset() addSIs [MemrelI] addSEs [MemrelE]) 1);
   113 qed "under_Memrel";
   114 
   115 (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
   116 val under_Memrel_eclose = Transset_eclose RS under_Memrel;
   117 
   118 val wfrec_ssubst = standard (wf_Memrel RS wfrec RS ssubst);
   119 
   120 val [kmemj,jmemi] = goal Epsilon.thy
   121     "[| k:eclose({j});  j:eclose({i}) |] ==> \
   122 \    wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)";
   123 by (rtac (kmemj RS eclose_induct) 1);
   124 by (rtac wfrec_ssubst 1);
   125 by (rtac wfrec_ssubst 1);
   126 by (asm_simp_tac (simpset() addsimps [under_Memrel_eclose,
   127                                   jmemi RSN (2,mem_eclose_sing_trans)]) 1);
   128 qed "wfrec_eclose_eq";
   129 
   130 val [prem] = goal Epsilon.thy
   131     "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)";
   132 by (rtac (arg_in_eclose_sing RS wfrec_eclose_eq) 1);
   133 by (rtac (prem RS arg_into_eclose_sing) 1);
   134 qed "wfrec_eclose_eq2";
   135 
   136 Goalw [transrec_def]
   137     "transrec(a,H) = H(a, lam x:a. transrec(x,H))";
   138 by (rtac wfrec_ssubst 1);
   139 by (simp_tac (simpset() addsimps [wfrec_eclose_eq2, arg_in_eclose_sing,
   140                               under_Memrel_eclose]) 1);
   141 qed "transrec";
   142 
   143 (*Avoids explosions in proofs; resolve it with a meta-level definition.*)
   144 val rew::prems = goal Epsilon.thy
   145     "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))";
   146 by (rewtac rew);
   147 by (REPEAT (resolve_tac (prems@[transrec]) 1));
   148 qed "def_transrec";
   149 
   150 val prems = goal Epsilon.thy
   151     "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
   152 \    |]  ==> transrec(a,H) : B(a)";
   153 by (res_inst_tac [("i", "a")] (arg_in_eclose_sing RS eclose_induct) 1);
   154 by (stac transrec 1);
   155 by (REPEAT (ares_tac (prems @ [lam_type]) 1 ORELSE etac bspec 1));
   156 qed "transrec_type";
   157 
   158 Goal "Ord(i) ==> eclose({i}) <= succ(i)";
   159 by (etac (Ord_is_Transset RS Transset_succ RS eclose_least) 1);
   160 by (rtac (succI1 RS singleton_subsetI) 1);
   161 qed "eclose_sing_Ord";
   162 
   163 val prems = goal Epsilon.thy
   164     "[| j: i;  Ord(i);  \
   165 \       !!x u. [| x: i;  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
   166 \    |]  ==> transrec(j,H) : B(j)";
   167 by (rtac transrec_type 1);
   168 by (resolve_tac prems 1);
   169 by (rtac (Ord_in_Ord RS eclose_sing_Ord RS subsetD RS succE) 1);
   170 by (DEPTH_SOLVE (ares_tac prems 1 ORELSE eresolve_tac [ssubst,Ord_trans] 1));
   171 qed "Ord_transrec_type";
   172 
   173 (*** Rank ***)
   174 
   175 (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
   176 Goal "rank(a) = (UN y:a. succ(rank(y)))";
   177 by (stac (rank_def RS def_transrec) 1);
   178 by (Simp_tac 1);
   179 qed "rank";
   180 
   181 Goal "Ord(rank(a))";
   182 by (eps_ind_tac "a" 1);
   183 by (stac rank 1);
   184 by (rtac (Ord_succ RS Ord_UN) 1);
   185 by (etac bspec 1);
   186 by (assume_tac 1);
   187 qed "Ord_rank";
   188 Addsimps [Ord_rank];
   189 
   190 val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
   191 by (rtac (major RS trans_induct) 1);
   192 by (stac rank 1);
   193 by (asm_simp_tac (simpset() addsimps [Ord_equality]) 1);
   194 qed "rank_of_Ord";
   195 
   196 Goal "a:b ==> rank(a) < rank(b)";
   197 by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
   198 by (etac (UN_I RS ltI) 1);
   199 by (rtac Ord_UN 2);
   200 by Auto_tac;
   201 qed "rank_lt";
   202 
   203 val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) < rank(b)";
   204 by (rtac (major RS eclose_induct_down) 1);
   205 by (etac rank_lt 1);
   206 by (etac (rank_lt RS lt_trans) 1);
   207 by (assume_tac 1);
   208 qed "eclose_rank_lt";
   209 
   210 Goal "a<=b ==> rank(a) le rank(b)";
   211 by (rtac subset_imp_le 1);
   212 by (stac rank 1);
   213 by (stac rank 1);
   214 by Auto_tac;
   215 qed "rank_mono";
   216 
   217 Goal "rank(Pow(a)) = succ(rank(a))";
   218 by (rtac (rank RS trans) 1);
   219 by (rtac le_anti_sym 1);
   220 by (rtac UN_upper_le 2);
   221 by (rtac UN_least_le 1);
   222 by (auto_tac (claset() addIs [rank_mono], simpset()));
   223 qed "rank_Pow";
   224 
   225 Goal "rank(0) = 0";
   226 by (rtac (rank RS trans) 1);
   227 by (Blast_tac 1);
   228 qed "rank_0";
   229 
   230 Goal "rank(succ(x)) = succ(rank(x))";
   231 by (rtac (rank RS trans) 1);
   232 by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
   233 by (etac succE 1);
   234 by (Blast_tac 1);
   235 by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1);
   236 qed "rank_succ";
   237 
   238 Goal "rank(Union(A)) = (UN x:A. rank(x))";
   239 by (rtac equalityI 1);
   240 by (rtac (rank_mono RS le_imp_subset RS UN_least) 2);
   241 by (etac Union_upper 2);
   242 by (stac rank 1);
   243 by (rtac UN_least 1);
   244 by (etac UnionE 1);
   245 by (rtac subset_trans 1);
   246 by (etac (RepFunI RS Union_upper) 2);
   247 by (etac (rank_lt RS succ_leI RS le_imp_subset) 1);
   248 qed "rank_Union";
   249 
   250 Goal "rank(eclose(a)) = rank(a)";
   251 by (rtac le_anti_sym 1);
   252 by (rtac (arg_subset_eclose RS rank_mono) 2);
   253 by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1);
   254 by (rtac (Ord_rank RS UN_least_le) 1);
   255 by (etac (eclose_rank_lt RS succ_leI) 1);
   256 qed "rank_eclose";
   257 
   258 Goalw [Pair_def] "rank(a) < rank(<a,b>)";
   259 by (rtac (consI1 RS rank_lt RS lt_trans) 1);
   260 by (rtac (consI1 RS consI2 RS rank_lt) 1);
   261 qed "rank_pair1";
   262 
   263 Goalw [Pair_def] "rank(b) < rank(<a,b>)";
   264 by (rtac (consI1 RS consI2 RS rank_lt RS lt_trans) 1);
   265 by (rtac (consI1 RS consI2 RS rank_lt) 1);
   266 qed "rank_pair2";
   267 
   268 (*** Corollaries of leastness ***)
   269 
   270 Goal "A:B ==> eclose(A)<=eclose(B)";
   271 by (rtac (Transset_eclose RS eclose_least) 1);
   272 by (etac (arg_into_eclose RS eclose_subset) 1);
   273 qed "mem_eclose_subset";
   274 
   275 Goal "A<=B ==> eclose(A) <= eclose(B)";
   276 by (rtac (Transset_eclose RS eclose_least) 1);
   277 by (etac subset_trans 1);
   278 by (rtac arg_subset_eclose 1);
   279 qed "eclose_mono";
   280 
   281 (** Idempotence of eclose **)
   282 
   283 Goal "eclose(eclose(A)) = eclose(A)";
   284 by (rtac equalityI 1);
   285 by (rtac ([Transset_eclose, subset_refl] MRS eclose_least) 1);
   286 by (rtac arg_subset_eclose 1);
   287 qed "eclose_idem";
   288 
   289 (** Transfinite recursion for definitions based on the 
   290     three cases of ordinals **)
   291 
   292 Goal "transrec2(0,a,b) = a";
   293 by (rtac (transrec2_def RS def_transrec RS trans) 1);
   294 by (Simp_tac 1);
   295 qed "transrec2_0";
   296 
   297 Goal "(THE j. i=j) = i";
   298 by (Blast_tac 1);
   299 qed "THE_eq";
   300 
   301 Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
   302 by (rtac (transrec2_def RS def_transrec RS trans) 1);
   303 by (simp_tac (simpset() addsimps [succ_not_0, THE_eq, if_P]) 1);
   304 by (Blast_tac 1);
   305 qed "transrec2_succ";
   306 
   307 Goal "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
   308 by (rtac (transrec2_def RS def_transrec RS trans) 1);
   309 by (Simp_tac 1);
   310 by (blast_tac (claset() addSDs [Limit_has_0] addSEs [succ_LimitE]) 1);
   311 qed "transrec2_Limit";
   312 
   313 Addsimps [transrec2_0, transrec2_succ];
   314 
   315 
   316 (** recursor -- better than nat_rec; the succ case has no type requirement! **)
   317 
   318 (*NOT suitable for rewriting*)
   319 val lemma = recursor_def RS def_transrec RS trans;
   320 
   321 Goal "recursor(a,b,0) = a";
   322 by (rtac (nat_case_0 RS lemma) 1);
   323 qed "recursor_0";
   324 
   325 Goal "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))";
   326 by (rtac lemma 1);
   327 by (Simp_tac 1);
   328 qed "recursor_succ";
   329 
   330 
   331 (** rec: old version for compatibility **)
   332 
   333 Goalw [rec_def] "rec(0,a,b) = a";
   334 by (rtac recursor_0 1);
   335 qed "rec_0";
   336 
   337 Goalw [rec_def] "rec(succ(m),a,b) = b(m, rec(m,a,b))";
   338 by (rtac recursor_succ 1);
   339 qed "rec_succ";
   340 
   341 Addsimps [rec_0, rec_succ];
   342 
   343 val major::prems = Goal
   344     "[| n: nat;  \
   345 \       a: C(0);  \
   346 \       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  \
   347 \    |] ==> rec(n,a,b) : C(n)";
   348 by (rtac (major RS nat_induct) 1);
   349 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
   350 qed "rec_type";
   351