converted Epsilon to Isar
authorpaulson
Sat May 18 22:22:23 2002 +0200 (2002-05-18)
changeset 13164dfc399c684e4
parent 13163 e320a52ff711
child 13165 31d020705aff
converted Epsilon to Isar
src/ZF/Epsilon.ML
src/ZF/Epsilon.thy
src/ZF/IsaMakefile
     1.1 --- a/src/ZF/Epsilon.ML	Sat May 18 20:08:17 2002 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,363 +0,0 @@
     1.4 -(*  Title:      ZF/epsilon.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1993  University of Cambridge
     1.8 -
     1.9 -Epsilon induction and recursion
    1.10 -*)
    1.11 -
    1.12 -(*** Basic closure properties ***)
    1.13 -
    1.14 -Goalw [eclose_def] "A <= eclose(A)";
    1.15 -by (rtac (nat_rec_0 RS equalityD2 RS subset_trans) 1);
    1.16 -by (rtac (nat_0I RS UN_upper) 1);
    1.17 -qed "arg_subset_eclose";
    1.18 -
    1.19 -bind_thm ("arg_into_eclose", arg_subset_eclose RS subsetD);
    1.20 -
    1.21 -Goalw [eclose_def,Transset_def] "Transset(eclose(A))";
    1.22 -by (rtac (subsetI RS ballI) 1);
    1.23 -by (etac UN_E 1);
    1.24 -by (rtac (nat_succI RS UN_I) 1);
    1.25 -by (assume_tac 1);
    1.26 -by (etac (nat_rec_succ RS ssubst) 1);
    1.27 -by (etac UnionI 1);
    1.28 -by (assume_tac 1);
    1.29 -qed "Transset_eclose";
    1.30 -
    1.31 -(* x : eclose(A) ==> x <= eclose(A) *)
    1.32 -bind_thm ("eclose_subset",
    1.33 -    rewrite_rule [Transset_def] Transset_eclose RS bspec);
    1.34 -
    1.35 -(* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
    1.36 -bind_thm ("ecloseD", eclose_subset RS subsetD);
    1.37 -
    1.38 -bind_thm ("arg_in_eclose_sing", arg_subset_eclose RS singleton_subsetD);
    1.39 -bind_thm ("arg_into_eclose_sing", arg_in_eclose_sing RS ecloseD);
    1.40 -
    1.41 -(* This is epsilon-induction for eclose(A); see also eclose_induct_down...
    1.42 -   [| a: eclose(A);  !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) 
    1.43 -   |] ==> P(a) 
    1.44 -*)
    1.45 -bind_thm ("eclose_induct", Transset_eclose RSN (2, Transset_induct));
    1.46 -
    1.47 -(*Epsilon induction*)
    1.48 -val prems = Goal
    1.49 -    "[| !!x. ALL y:x. P(y) ==> P(x) |]  ==>  P(a)";
    1.50 -by (rtac (arg_in_eclose_sing RS eclose_induct) 1);
    1.51 -by (eresolve_tac prems 1);
    1.52 -qed "eps_induct";
    1.53 -
    1.54 -(*Perform epsilon-induction on i. *)
    1.55 -fun eps_ind_tac a = 
    1.56 -    EVERY' [res_inst_tac [("a",a)] eps_induct,
    1.57 -            rename_last_tac a ["1"]];
    1.58 -
    1.59 -
    1.60 -(*** Leastness of eclose ***)
    1.61 -
    1.62 -(** eclose(A) is the least transitive set including A as a subset. **)
    1.63 -
    1.64 -Goalw [Transset_def]
    1.65 -    "[| Transset(X);  A<=X;  n: nat |] ==> \
    1.66 -\             nat_rec(n, A, %m r. Union(r)) <= X";
    1.67 -by (etac nat_induct 1);
    1.68 -by (asm_simp_tac (simpset() addsimps [nat_rec_0]) 1);
    1.69 -by (asm_simp_tac (simpset() addsimps [nat_rec_succ]) 1);
    1.70 -by (Blast_tac 1);
    1.71 -qed "eclose_least_lemma";
    1.72 -
    1.73 -Goalw [eclose_def]
    1.74 -     "[| Transset(X);  A<=X |] ==> eclose(A) <= X";
    1.75 -by (rtac (eclose_least_lemma RS UN_least) 1);
    1.76 -by (REPEAT (assume_tac 1));
    1.77 -qed "eclose_least";
    1.78 -
    1.79 -(*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
    1.80 -val [major,base,step] = Goal
    1.81 -    "[| a: eclose(b);                                           \
    1.82 -\       !!y.   [| y: b |] ==> P(y);                             \
    1.83 -\       !!y z. [| y: eclose(b);  P(y);  z: y |] ==> P(z)        \
    1.84 -\    |] ==> P(a)";
    1.85 -by (rtac (major RSN (3, eclose_least RS subsetD RS CollectD2)) 1);
    1.86 -by (rtac (CollectI RS subsetI) 2);
    1.87 -by (etac (arg_subset_eclose RS subsetD) 2);
    1.88 -by (etac base 2);
    1.89 -by (rewtac Transset_def);
    1.90 -by (blast_tac (claset() addIs [step,ecloseD]) 1);
    1.91 -qed "eclose_induct_down";
    1.92 -
    1.93 -Goal "Transset(X) ==> eclose(X) = X";
    1.94 -by (etac ([eclose_least, arg_subset_eclose] MRS equalityI) 1);
    1.95 -by (rtac subset_refl 1);
    1.96 -qed "Transset_eclose_eq_arg";
    1.97 -
    1.98 -
    1.99 -(*** Epsilon recursion ***)
   1.100 -
   1.101 -(*Unused...*)
   1.102 -Goal "[| A: eclose(B);  B: eclose(C) |] ==> A: eclose(C)";
   1.103 -by (rtac ([Transset_eclose, eclose_subset] MRS eclose_least RS subsetD) 1);
   1.104 -by (REPEAT (assume_tac 1));
   1.105 -qed "mem_eclose_trans";
   1.106 -
   1.107 -(*Variant of the previous lemma in a useable form for the sequel*)
   1.108 -Goal "[| A: eclose({B});  B: eclose({C}) |] ==> A: eclose({C})";
   1.109 -by (rtac ([Transset_eclose, singleton_subsetI] MRS eclose_least RS subsetD) 1);
   1.110 -by (REPEAT (assume_tac 1));
   1.111 -qed "mem_eclose_sing_trans";
   1.112 -
   1.113 -Goalw [Transset_def] "[| Transset(i);  j:i |] ==> Memrel(i)-``{j} = j";
   1.114 -by (Blast_tac 1);
   1.115 -qed "under_Memrel";
   1.116 -
   1.117 -(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
   1.118 -bind_thm ("under_Memrel_eclose", Transset_eclose RS under_Memrel);
   1.119 -
   1.120 -bind_thm ("wfrec_ssubst", standard (wf_Memrel RS wfrec RS ssubst));
   1.121 -
   1.122 -val [kmemj,jmemi] = goal (the_context ())
   1.123 -    "[| k:eclose({j});  j:eclose({i}) |] ==> \
   1.124 -\    wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)";
   1.125 -by (rtac (kmemj RS eclose_induct) 1);
   1.126 -by (rtac wfrec_ssubst 1);
   1.127 -by (rtac wfrec_ssubst 1);
   1.128 -by (asm_simp_tac (simpset() addsimps [under_Memrel_eclose,
   1.129 -                                  jmemi RSN (2,mem_eclose_sing_trans)]) 1);
   1.130 -qed "wfrec_eclose_eq";
   1.131 -
   1.132 -Goal
   1.133 -    "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)";
   1.134 -by (rtac (arg_in_eclose_sing RS wfrec_eclose_eq) 1);
   1.135 -by (etac arg_into_eclose_sing 1);
   1.136 -qed "wfrec_eclose_eq2";
   1.137 -
   1.138 -Goalw [transrec_def]
   1.139 -    "transrec(a,H) = H(a, lam x:a. transrec(x,H))";
   1.140 -by (rtac wfrec_ssubst 1);
   1.141 -by (simp_tac (simpset() addsimps [wfrec_eclose_eq2, arg_in_eclose_sing,
   1.142 -                              under_Memrel_eclose]) 1);
   1.143 -qed "transrec";
   1.144 -
   1.145 -(*Avoids explosions in proofs; resolve it with a meta-level definition.*)
   1.146 -val rew::prems = Goal
   1.147 -    "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))";
   1.148 -by (rewtac rew);
   1.149 -by (REPEAT (resolve_tac (prems@[transrec]) 1));
   1.150 -qed "def_transrec";
   1.151 -
   1.152 -val prems = Goal
   1.153 -    "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
   1.154 -\    |]  ==> transrec(a,H) : B(a)";
   1.155 -by (res_inst_tac [("i", "a")] (arg_in_eclose_sing RS eclose_induct) 1);
   1.156 -by (stac transrec 1);
   1.157 -by (REPEAT (ares_tac (prems @ [lam_type]) 1 ORELSE etac bspec 1));
   1.158 -qed "transrec_type";
   1.159 -
   1.160 -Goal "Ord(i) ==> eclose({i}) <= succ(i)";
   1.161 -by (etac (Ord_is_Transset RS Transset_succ RS eclose_least) 1);
   1.162 -by (rtac (succI1 RS singleton_subsetI) 1);
   1.163 -qed "eclose_sing_Ord";
   1.164 -
   1.165 -val prems = Goal
   1.166 -    "[| j: i;  Ord(i);  \
   1.167 -\       !!x u. [| x: i;  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
   1.168 -\    |]  ==> transrec(j,H) : B(j)";
   1.169 -by (rtac transrec_type 1);
   1.170 -by (resolve_tac prems 1);
   1.171 -by (rtac (Ord_in_Ord RS eclose_sing_Ord RS subsetD RS succE) 1);
   1.172 -by (DEPTH_SOLVE (ares_tac prems 1 ORELSE eresolve_tac [ssubst,Ord_trans] 1));
   1.173 -qed "Ord_transrec_type";
   1.174 -
   1.175 -(*** Rank ***)
   1.176 -
   1.177 -(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
   1.178 -Goal "rank(a) = (UN y:a. succ(rank(y)))";
   1.179 -by (stac (rank_def RS def_transrec) 1);
   1.180 -by (Simp_tac 1);
   1.181 -qed "rank";
   1.182 -
   1.183 -Goal "Ord(rank(a))";
   1.184 -by (eps_ind_tac "a" 1);
   1.185 -by (stac rank 1);
   1.186 -by (rtac (Ord_succ RS Ord_UN) 1);
   1.187 -by (etac bspec 1);
   1.188 -by (assume_tac 1);
   1.189 -qed "Ord_rank";
   1.190 -Addsimps [Ord_rank];
   1.191 -
   1.192 -Goal "Ord(i) ==> rank(i) = i";
   1.193 -by (etac trans_induct 1);
   1.194 -by (stac rank 1);
   1.195 -by (asm_simp_tac (simpset() addsimps [Ord_equality]) 1);
   1.196 -qed "rank_of_Ord";
   1.197 -
   1.198 -Goal "a:b ==> rank(a) < rank(b)";
   1.199 -by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
   1.200 -by (etac (UN_I RS ltI) 1);
   1.201 -by (rtac Ord_UN 2);
   1.202 -by Auto_tac;
   1.203 -qed "rank_lt";
   1.204 -
   1.205 -Goal "a: eclose(b) ==> rank(a) < rank(b)";
   1.206 -by (etac eclose_induct_down 1);
   1.207 -by (etac rank_lt 1);
   1.208 -by (etac (rank_lt RS lt_trans) 1);
   1.209 -by (assume_tac 1);
   1.210 -qed "eclose_rank_lt";
   1.211 -
   1.212 -Goal "a<=b ==> rank(a) le rank(b)";
   1.213 -by (rtac subset_imp_le 1);
   1.214 -by (stac rank 1);
   1.215 -by (stac rank 1);
   1.216 -by Auto_tac;
   1.217 -qed "rank_mono";
   1.218 -
   1.219 -Goal "rank(Pow(a)) = succ(rank(a))";
   1.220 -by (rtac (rank RS trans) 1);
   1.221 -by (rtac le_anti_sym 1);
   1.222 -by (rtac UN_upper_le 2);
   1.223 -by (rtac UN_least_le 1);
   1.224 -by (auto_tac (claset() addIs [rank_mono], simpset() addsimps [Ord_UN]));
   1.225 -qed "rank_Pow";
   1.226 -
   1.227 -Goal "rank(0) = 0";
   1.228 -by (rtac (rank RS trans) 1);
   1.229 -by (Blast_tac 1);
   1.230 -qed "rank_0";
   1.231 -
   1.232 -Goal "rank(succ(x)) = succ(rank(x))";
   1.233 -by (rtac (rank RS trans) 1);
   1.234 -by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
   1.235 -by (etac succE 1);
   1.236 -by (Blast_tac 1);
   1.237 -by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1);
   1.238 -qed "rank_succ";
   1.239 -Addsimps [rank_0, rank_succ];
   1.240 -
   1.241 -Goal "rank(Union(A)) = (UN x:A. rank(x))";
   1.242 -by (rtac equalityI 1);
   1.243 -by (rtac (rank_mono RS le_imp_subset RS UN_least) 2);
   1.244 -by (etac Union_upper 2);
   1.245 -by (stac rank 1);
   1.246 -by (rtac UN_least 1);
   1.247 -by (etac UnionE 1);
   1.248 -by (rtac subset_trans 1);
   1.249 -by (etac (RepFunI RS Union_upper) 2);
   1.250 -by (etac (rank_lt RS succ_leI RS le_imp_subset) 1);
   1.251 -qed "rank_Union";
   1.252 -
   1.253 -Goal "rank(eclose(a)) = rank(a)";
   1.254 -by (rtac le_anti_sym 1);
   1.255 -by (rtac (arg_subset_eclose RS rank_mono) 2);
   1.256 -by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1);
   1.257 -by (rtac (Ord_rank RS UN_least_le) 1);
   1.258 -by (etac (eclose_rank_lt RS succ_leI) 1);
   1.259 -qed "rank_eclose";
   1.260 -
   1.261 -Goalw [Pair_def] "rank(a) < rank(<a,b>)";
   1.262 -by (rtac (consI1 RS rank_lt RS lt_trans) 1);
   1.263 -by (rtac (consI1 RS consI2 RS rank_lt) 1);
   1.264 -qed "rank_pair1";
   1.265 -
   1.266 -Goalw [Pair_def] "rank(b) < rank(<a,b>)";
   1.267 -by (rtac (consI1 RS consI2 RS rank_lt RS lt_trans) 1);
   1.268 -by (rtac (consI1 RS consI2 RS rank_lt) 1);
   1.269 -qed "rank_pair2";
   1.270 -
   1.271 -(*Not clear how to remove the P(a) condition, since the "then" part
   1.272 -  must refer to "a"*)
   1.273 -Goal "P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)";
   1.274 -by (asm_simp_tac (simpset() addsimps [the_0, the_equality2]) 1);
   1.275 -qed "the_equality_if";
   1.276 -
   1.277 -(*The premise is needed not just to fix i but to ensure f~=0*)
   1.278 -Goalw [apply_def] "i : domain(f) ==> rank(f`i) < rank(f)";
   1.279 -by (Clarify_tac 1);
   1.280 -by (subgoal_tac "rank(y) < rank(f)" 1);
   1.281 -by (blast_tac (claset() addIs [lt_trans, rank_lt, rank_pair2]) 2);
   1.282 -by (subgoal_tac "0 < rank(f)" 1);
   1.283 -by (etac (Ord_rank RS Ord_0_le RS lt_trans1) 2);
   1.284 -by (asm_simp_tac (simpset() addsimps [the_equality_if]) 1);
   1.285 -qed "rank_apply";
   1.286 -
   1.287 -
   1.288 -(*** Corollaries of leastness ***)
   1.289 -
   1.290 -Goal "A:B ==> eclose(A)<=eclose(B)";
   1.291 -by (rtac (Transset_eclose RS eclose_least) 1);
   1.292 -by (etac (arg_into_eclose RS eclose_subset) 1);
   1.293 -qed "mem_eclose_subset";
   1.294 -
   1.295 -Goal "A<=B ==> eclose(A) <= eclose(B)";
   1.296 -by (rtac (Transset_eclose RS eclose_least) 1);
   1.297 -by (etac subset_trans 1);
   1.298 -by (rtac arg_subset_eclose 1);
   1.299 -qed "eclose_mono";
   1.300 -
   1.301 -(** Idempotence of eclose **)
   1.302 -
   1.303 -Goal "eclose(eclose(A)) = eclose(A)";
   1.304 -by (rtac equalityI 1);
   1.305 -by (rtac ([Transset_eclose, subset_refl] MRS eclose_least) 1);
   1.306 -by (rtac arg_subset_eclose 1);
   1.307 -qed "eclose_idem";
   1.308 -
   1.309 -(** Transfinite recursion for definitions based on the 
   1.310 -    three cases of ordinals **)
   1.311 -
   1.312 -Goal "transrec2(0,a,b) = a";
   1.313 -by (rtac (transrec2_def RS def_transrec RS trans) 1);
   1.314 -by (Simp_tac 1);
   1.315 -qed "transrec2_0";
   1.316 -
   1.317 -Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
   1.318 -by (rtac (transrec2_def RS def_transrec RS trans) 1);
   1.319 -by (simp_tac (simpset() addsimps [the_equality, if_P]) 1);
   1.320 -qed "transrec2_succ";
   1.321 -
   1.322 -Goal "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
   1.323 -by (rtac (transrec2_def RS def_transrec RS trans) 1);
   1.324 -by (Simp_tac 1);
   1.325 -by (blast_tac (claset() addSDs [Limit_has_0] addSEs [succ_LimitE]) 1);
   1.326 -qed "transrec2_Limit";
   1.327 -
   1.328 -Addsimps [transrec2_0, transrec2_succ];
   1.329 -
   1.330 -
   1.331 -(** recursor -- better than nat_rec; the succ case has no type requirement! **)
   1.332 -
   1.333 -(*NOT suitable for rewriting*)
   1.334 -val lemma = recursor_def RS def_transrec RS trans;
   1.335 -
   1.336 -Goal "recursor(a,b,0) = a";
   1.337 -by (rtac (nat_case_0 RS lemma) 1);
   1.338 -qed "recursor_0";
   1.339 -
   1.340 -Goal "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))";
   1.341 -by (rtac lemma 1);
   1.342 -by (Simp_tac 1);
   1.343 -qed "recursor_succ";
   1.344 -
   1.345 -
   1.346 -(** rec: old version for compatibility **)
   1.347 -
   1.348 -Goalw [rec_def] "rec(0,a,b) = a";
   1.349 -by (rtac recursor_0 1);
   1.350 -qed "rec_0";
   1.351 -
   1.352 -Goalw [rec_def] "rec(succ(m),a,b) = b(m, rec(m,a,b))";
   1.353 -by (rtac recursor_succ 1);
   1.354 -qed "rec_succ";
   1.355 -
   1.356 -Addsimps [rec_0, rec_succ];
   1.357 -
   1.358 -val major::prems = Goal
   1.359 -    "[| n: nat;  \
   1.360 -\       a: C(0);  \
   1.361 -\       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  \
   1.362 -\    |] ==> rec(n,a,b) : C(n)";
   1.363 -by (rtac (major RS nat_induct) 1);
   1.364 -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
   1.365 -qed "rec_type";
   1.366 -
     2.1 --- a/src/ZF/Epsilon.thy	Sat May 18 20:08:17 2002 +0200
     2.2 +++ b/src/ZF/Epsilon.thy	Sat May 18 22:22:23 2002 +0200
     2.3 @@ -6,18 +6,19 @@
     2.4  Epsilon induction and recursion
     2.5  *)
     2.6  
     2.7 -Epsilon = Nat + mono +
     2.8 +theory Epsilon = Nat + mono:
     2.9 +
    2.10  constdefs
    2.11 -  eclose    :: i=>i
    2.12 +  eclose    :: "i=>i"
    2.13      "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
    2.14  
    2.15 -  transrec  :: [i, [i,i]=>i] =>i
    2.16 +  transrec  :: "[i, [i,i]=>i] =>i"
    2.17      "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
    2.18   
    2.19 -  rank      :: i=>i
    2.20 +  rank      :: "i=>i"
    2.21      "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
    2.22  
    2.23 -  transrec2 :: [i, i, [i,i]=>i] =>i
    2.24 +  transrec2 :: "[i, i, [i,i]=>i] =>i"
    2.25      "transrec2(k, a, b) ==                     
    2.26         transrec(k, 
    2.27                  %i r. if(i=0, a, 
    2.28 @@ -25,10 +26,394 @@
    2.29                             b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
    2.30                             UN j<i. r`j)))"
    2.31  
    2.32 -    recursor  :: [i, [i,i]=>i, i]=>i
    2.33 -     "recursor(a,b,k) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
    2.34 +  recursor  :: "[i, [i,i]=>i, i]=>i"
    2.35 +    "recursor(a,b,k) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
    2.36 +
    2.37 +  rec  :: "[i, i, [i,i]=>i]=>i"
    2.38 +    "rec(k,a,b) == recursor(a,b,k)"
    2.39 +
    2.40 +
    2.41 +(*** Basic closure properties ***)
    2.42 +
    2.43 +lemma arg_subset_eclose: "A <= eclose(A)"
    2.44 +apply (unfold eclose_def)
    2.45 +apply (rule nat_rec_0 [THEN equalityD2, THEN subset_trans])
    2.46 +apply (rule nat_0I [THEN UN_upper])
    2.47 +done
    2.48 +
    2.49 +lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD, standard]
    2.50 +
    2.51 +lemma Transset_eclose: "Transset(eclose(A))"
    2.52 +apply (unfold eclose_def Transset_def)
    2.53 +apply (rule subsetI [THEN ballI])
    2.54 +apply (erule UN_E)
    2.55 +apply (rule nat_succI [THEN UN_I], assumption)
    2.56 +apply (erule nat_rec_succ [THEN ssubst])
    2.57 +apply (erule UnionI, assumption)
    2.58 +done
    2.59 +
    2.60 +(* x : eclose(A) ==> x <= eclose(A) *)
    2.61 +lemmas eclose_subset =  
    2.62 +       Transset_eclose [unfolded Transset_def, THEN bspec, standard]
    2.63 +
    2.64 +(* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
    2.65 +lemmas ecloseD = eclose_subset [THEN subsetD, standard]
    2.66 +
    2.67 +lemmas arg_in_eclose_sing = arg_subset_eclose [THEN singleton_subsetD]
    2.68 +lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD, standard]
    2.69 +
    2.70 +(* This is epsilon-induction for eclose(A); see also eclose_induct_down...
    2.71 +   [| a: eclose(A);  !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) 
    2.72 +   |] ==> P(a) 
    2.73 +*)
    2.74 +lemmas eclose_induct = Transset_induct [OF _ Transset_eclose]
    2.75 +
    2.76 +(*Epsilon induction*)
    2.77 +lemma eps_induct:
    2.78 +    "[| !!x. ALL y:x. P(y) ==> P(x) |]  ==>  P(a)"
    2.79 +by (rule arg_in_eclose_sing [THEN eclose_induct], blast) 
    2.80 +
    2.81 +
    2.82 +(*** Leastness of eclose ***)
    2.83 +
    2.84 +(** eclose(A) is the least transitive set including A as a subset. **)
    2.85 +
    2.86 +lemma eclose_least_lemma: 
    2.87 +    "[| Transset(X);  A<=X;  n: nat |] ==> nat_rec(n, A, %m r. Union(r)) <= X"
    2.88 +apply (unfold Transset_def)
    2.89 +apply (erule nat_induct) 
    2.90 +apply (simp add: nat_rec_0)
    2.91 +apply (simp add: nat_rec_succ, blast)
    2.92 +done
    2.93 +
    2.94 +lemma eclose_least: 
    2.95 +     "[| Transset(X);  A<=X |] ==> eclose(A) <= X"
    2.96 +apply (unfold eclose_def)
    2.97 +apply (rule eclose_least_lemma [THEN UN_least], assumption+)
    2.98 +done
    2.99 +
   2.100 +(*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
   2.101 +lemma eclose_induct_down: 
   2.102 +    "[| a: eclose(b);                                            
   2.103 +        !!y.   [| y: b |] ==> P(y);                              
   2.104 +        !!y z. [| y: eclose(b);  P(y);  z: y |] ==> P(z)         
   2.105 +     |] ==> P(a)"
   2.106 +apply (rule eclose_least [THEN subsetD, THEN CollectD2, of "eclose(b)"])
   2.107 +  prefer 3 apply assumption
   2.108 + apply (unfold Transset_def) 
   2.109 + apply (blast intro: ecloseD)
   2.110 +apply (blast intro: arg_subset_eclose [THEN subsetD])
   2.111 +done
   2.112 +
   2.113 +lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X"
   2.114 +apply (erule equalityI [OF eclose_least arg_subset_eclose])
   2.115 +apply (rule subset_refl)
   2.116 +done
   2.117 +
   2.118 +
   2.119 +(*** Epsilon recursion ***)
   2.120 +
   2.121 +(*Unused...*)
   2.122 +lemma mem_eclose_trans: "[| A: eclose(B);  B: eclose(C) |] ==> A: eclose(C)"
   2.123 +by (rule eclose_least [OF Transset_eclose eclose_subset, THEN subsetD], 
   2.124 +    assumption+)
   2.125 +
   2.126 +(*Variant of the previous lemma in a useable form for the sequel*)
   2.127 +lemma mem_eclose_sing_trans:
   2.128 +     "[| A: eclose({B});  B: eclose({C}) |] ==> A: eclose({C})"
   2.129 +by (rule eclose_least [OF Transset_eclose singleton_subsetI, THEN subsetD], 
   2.130 +    assumption+)
   2.131 +
   2.132 +lemma under_Memrel: "[| Transset(i);  j:i |] ==> Memrel(i)-``{j} = j"
   2.133 +by (unfold Transset_def, blast)
   2.134 +
   2.135 +(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
   2.136 +lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel, standard]
   2.137 +
   2.138 +lemmas wfrec_ssubst = wf_Memrel [THEN wfrec, THEN ssubst]
   2.139 +
   2.140 +lemma wfrec_eclose_eq:
   2.141 +    "[| k:eclose({j});  j:eclose({i}) |] ==>  
   2.142 +     wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)"
   2.143 +apply (erule eclose_induct)
   2.144 +apply (rule wfrec_ssubst)
   2.145 +apply (rule wfrec_ssubst)
   2.146 +apply (simp add: under_Memrel_eclose mem_eclose_sing_trans [of _ j i])
   2.147 +done
   2.148 +
   2.149 +lemma wfrec_eclose_eq2: 
   2.150 +    "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)"
   2.151 +apply (rule arg_in_eclose_sing [THEN wfrec_eclose_eq])
   2.152 +apply (erule arg_into_eclose_sing)
   2.153 +done
   2.154 +
   2.155 +lemma transrec: "transrec(a,H) = H(a, lam x:a. transrec(x,H))"
   2.156 +apply (unfold transrec_def)
   2.157 +apply (rule wfrec_ssubst)
   2.158 +apply (simp add: wfrec_eclose_eq2 arg_in_eclose_sing under_Memrel_eclose)
   2.159 +done
   2.160 +
   2.161 +(*Avoids explosions in proofs; resolve it with a meta-level definition.*)
   2.162 +lemma def_transrec:
   2.163 +    "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))"
   2.164 +apply simp
   2.165 +apply (rule transrec)
   2.166 +done
   2.167 +
   2.168 +lemma transrec_type:
   2.169 +    "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x) |]
   2.170 +     ==> transrec(a,H) : B(a)"
   2.171 +apply (rule_tac i = "a" in arg_in_eclose_sing [THEN eclose_induct])
   2.172 +apply (subst transrec)
   2.173 +apply (simp add: lam_type) 
   2.174 +done
   2.175 +
   2.176 +lemma eclose_sing_Ord: "Ord(i) ==> eclose({i}) <= succ(i)"
   2.177 +apply (erule Ord_is_Transset [THEN Transset_succ, THEN eclose_least])
   2.178 +apply (rule succI1 [THEN singleton_subsetI])
   2.179 +done
   2.180 +
   2.181 +lemma Ord_transrec_type:
   2.182 +  assumes jini: "j: i"
   2.183 +      and ordi: "Ord(i)"
   2.184 +      and minor: " !!x u. [| x: i;  u: Pi(x,B) |] ==> H(x,u) : B(x)"
   2.185 +  shows "transrec(j,H) : B(j)"
   2.186 +apply (rule transrec_type)
   2.187 +apply (insert jini ordi)
   2.188 +apply (blast intro!: minor
   2.189 +             intro: Ord_trans 
   2.190 +             dest: Ord_in_Ord [THEN eclose_sing_Ord, THEN subsetD])
   2.191 +done
   2.192 +
   2.193 +(*** Rank ***)
   2.194 +
   2.195 +(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
   2.196 +lemma rank: "rank(a) = (UN y:a. succ(rank(y)))"
   2.197 +by (subst rank_def [THEN def_transrec], simp)
   2.198 +
   2.199 +lemma Ord_rank [simp]: "Ord(rank(a))"
   2.200 +apply (rule_tac a="a" in eps_induct) 
   2.201 +apply (subst rank)
   2.202 +apply (rule Ord_succ [THEN Ord_UN])
   2.203 +apply (erule bspec, assumption)
   2.204 +done
   2.205 +
   2.206 +lemma rank_of_Ord: "Ord(i) ==> rank(i) = i"
   2.207 +apply (erule trans_induct)
   2.208 +apply (subst rank)
   2.209 +apply (simp add: Ord_equality)
   2.210 +done
   2.211 +
   2.212 +lemma rank_lt: "a:b ==> rank(a) < rank(b)"
   2.213 +apply (rule_tac a1 = "b" in rank [THEN ssubst])
   2.214 +apply (erule UN_I [THEN ltI])
   2.215 +apply (rule_tac [2] Ord_UN, auto)
   2.216 +done
   2.217 +
   2.218 +lemma eclose_rank_lt: "a: eclose(b) ==> rank(a) < rank(b)"
   2.219 +apply (erule eclose_induct_down)
   2.220 +apply (erule rank_lt)
   2.221 +apply (erule rank_lt [THEN lt_trans], assumption)
   2.222 +done
   2.223  
   2.224 -    rec  :: [i, i, [i,i]=>i]=>i
   2.225 -     "rec(k,a,b) ==  recursor(a,b,k)"
   2.226 +lemma rank_mono: "a<=b ==> rank(a) le rank(b)"
   2.227 +apply (rule subset_imp_le)
   2.228 +apply (subst rank)
   2.229 +apply (subst rank, auto)
   2.230 +done
   2.231 +
   2.232 +lemma rank_Pow: "rank(Pow(a)) = succ(rank(a))"
   2.233 +apply (rule rank [THEN trans])
   2.234 +apply (rule le_anti_sym)
   2.235 +apply (rule_tac [2] UN_upper_le)
   2.236 +apply (rule UN_least_le)
   2.237 +apply (auto intro: rank_mono simp add: Ord_UN)
   2.238 +done
   2.239 +
   2.240 +lemma rank_0 [simp]: "rank(0) = 0"
   2.241 +by (rule rank [THEN trans], blast)
   2.242 +
   2.243 +lemma rank_succ [simp]: "rank(succ(x)) = succ(rank(x))"
   2.244 +apply (rule rank [THEN trans])
   2.245 +apply (rule equalityI [OF UN_least succI1 [THEN UN_upper]])
   2.246 +apply (erule succE, blast)
   2.247 +apply (erule rank_lt [THEN leI, THEN succ_leI, THEN le_imp_subset])
   2.248 +done
   2.249 +
   2.250 +lemma rank_Union: "rank(Union(A)) = (UN x:A. rank(x))"
   2.251 +apply (rule equalityI)
   2.252 +apply (rule_tac [2] rank_mono [THEN le_imp_subset, THEN UN_least])
   2.253 +apply (erule_tac [2] Union_upper)
   2.254 +apply (subst rank)
   2.255 +apply (rule UN_least)
   2.256 +apply (erule UnionE)
   2.257 +apply (rule subset_trans)
   2.258 +apply (erule_tac [2] RepFunI [THEN Union_upper])
   2.259 +apply (erule rank_lt [THEN succ_leI, THEN le_imp_subset])
   2.260 +done
   2.261 +
   2.262 +lemma rank_eclose: "rank(eclose(a)) = rank(a)"
   2.263 +apply (rule le_anti_sym)
   2.264 +apply (rule_tac [2] arg_subset_eclose [THEN rank_mono])
   2.265 +apply (rule_tac a1 = "eclose (a) " in rank [THEN ssubst])
   2.266 +apply (rule Ord_rank [THEN UN_least_le])
   2.267 +apply (erule eclose_rank_lt [THEN succ_leI])
   2.268 +done
   2.269 +
   2.270 +lemma rank_pair1: "rank(a) < rank(<a,b>)"
   2.271 +apply (unfold Pair_def)
   2.272 +apply (rule consI1 [THEN rank_lt, THEN lt_trans])
   2.273 +apply (rule consI1 [THEN consI2, THEN rank_lt])
   2.274 +done
   2.275 +
   2.276 +lemma rank_pair2: "rank(b) < rank(<a,b>)"
   2.277 +apply (unfold Pair_def)
   2.278 +apply (rule consI1 [THEN consI2, THEN rank_lt, THEN lt_trans])
   2.279 +apply (rule consI1 [THEN consI2, THEN rank_lt])
   2.280 +done
   2.281 +
   2.282 +(*Not clear how to remove the P(a) condition, since the "then" part
   2.283 +  must refer to "a"*)
   2.284 +lemma the_equality_if:
   2.285 +     "P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)"
   2.286 +by (simp add: the_0 the_equality2)
   2.287 +
   2.288 +(*The premise is needed not just to fix i but to ensure f~=0*)
   2.289 +lemma rank_apply: "i : domain(f) ==> rank(f`i) < rank(f)"
   2.290 +apply (unfold apply_def, clarify)
   2.291 +apply (subgoal_tac "rank (y) < rank (f) ")
   2.292 +prefer 2 apply (blast intro: lt_trans rank_lt rank_pair2)
   2.293 +apply (subgoal_tac "0 < rank (f) ")
   2.294 +apply (erule_tac [2] Ord_rank [THEN Ord_0_le, THEN lt_trans1])
   2.295 +apply (simp add: the_equality_if)
   2.296 +done
   2.297 +
   2.298 +
   2.299 +(*** Corollaries of leastness ***)
   2.300 +
   2.301 +lemma mem_eclose_subset: "A:B ==> eclose(A)<=eclose(B)"
   2.302 +apply (rule Transset_eclose [THEN eclose_least])
   2.303 +apply (erule arg_into_eclose [THEN eclose_subset])
   2.304 +done
   2.305 +
   2.306 +lemma eclose_mono: "A<=B ==> eclose(A) <= eclose(B)"
   2.307 +apply (rule Transset_eclose [THEN eclose_least])
   2.308 +apply (erule subset_trans)
   2.309 +apply (rule arg_subset_eclose)
   2.310 +done
   2.311 +
   2.312 +(** Idempotence of eclose **)
   2.313 +
   2.314 +lemma eclose_idem: "eclose(eclose(A)) = eclose(A)"
   2.315 +apply (rule equalityI)
   2.316 +apply (rule eclose_least [OF Transset_eclose subset_refl])
   2.317 +apply (rule arg_subset_eclose)
   2.318 +done
   2.319 +
   2.320 +(** Transfinite recursion for definitions based on the 
   2.321 +    three cases of ordinals **)
   2.322 +
   2.323 +lemma transrec2_0 [simp]: "transrec2(0,a,b) = a"
   2.324 +by (rule transrec2_def [THEN def_transrec, THEN trans], simp)
   2.325 +
   2.326 +lemma transrec2_succ [simp]: "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))"
   2.327 +apply (rule transrec2_def [THEN def_transrec, THEN trans])
   2.328 +apply (simp add: the_equality if_P)
   2.329 +done
   2.330 +
   2.331 +lemma transrec2_Limit:
   2.332 +     "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"
   2.333 +apply (rule transrec2_def [THEN def_transrec, THEN trans], simp)
   2.334 +apply (blast dest!: Limit_has_0 elim!: succ_LimitE)
   2.335 +done
   2.336 +
   2.337 +
   2.338 +(** recursor -- better than nat_rec; the succ case has no type requirement! **)
   2.339 +
   2.340 +(*NOT suitable for rewriting*)
   2.341 +lemmas recursor_lemma = recursor_def [THEN def_transrec, THEN trans]
   2.342 +
   2.343 +lemma recursor_0: "recursor(a,b,0) = a"
   2.344 +by (rule nat_case_0 [THEN recursor_lemma])
   2.345 +
   2.346 +lemma recursor_succ: "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))"
   2.347 +by (rule recursor_lemma, simp)
   2.348 +
   2.349 +
   2.350 +(** rec: old version for compatibility **)
   2.351 +
   2.352 +lemma rec_0 [simp]: "rec(0,a,b) = a"
   2.353 +apply (unfold rec_def)
   2.354 +apply (rule recursor_0)
   2.355 +done
   2.356 +
   2.357 +lemma rec_succ [simp]: "rec(succ(m),a,b) = b(m, rec(m,a,b))"
   2.358 +apply (unfold rec_def)
   2.359 +apply (rule recursor_succ)
   2.360 +done
   2.361 +
   2.362 +lemma rec_type:
   2.363 +    "[| n: nat;   
   2.364 +        a: C(0);   
   2.365 +        !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m)) |]
   2.366 +     ==> rec(n,a,b) : C(n)"
   2.367 +apply (erule nat_induct, auto)
   2.368 +done
   2.369 +
   2.370 +ML
   2.371 +{*
   2.372 +val arg_subset_eclose = thm "arg_subset_eclose";
   2.373 +val arg_into_eclose = thm "arg_into_eclose";
   2.374 +val Transset_eclose = thm "Transset_eclose";
   2.375 +val eclose_subset = thm "eclose_subset";
   2.376 +val ecloseD = thm "ecloseD";
   2.377 +val arg_in_eclose_sing = thm "arg_in_eclose_sing";
   2.378 +val arg_into_eclose_sing = thm "arg_into_eclose_sing";
   2.379 +val eclose_induct = thm "eclose_induct";
   2.380 +val eps_induct = thm "eps_induct";
   2.381 +val eclose_least_lemma = thm "eclose_least_lemma";
   2.382 +val eclose_least = thm "eclose_least";
   2.383 +val eclose_induct_down = thm "eclose_induct_down";
   2.384 +val Transset_eclose_eq_arg = thm "Transset_eclose_eq_arg";
   2.385 +val mem_eclose_trans = thm "mem_eclose_trans";
   2.386 +val mem_eclose_sing_trans = thm "mem_eclose_sing_trans";
   2.387 +val under_Memrel = thm "under_Memrel";
   2.388 +val under_Memrel_eclose = thm "under_Memrel_eclose";
   2.389 +val wfrec_ssubst = thm "wfrec_ssubst";
   2.390 +val wfrec_eclose_eq = thm "wfrec_eclose_eq";
   2.391 +val wfrec_eclose_eq2 = thm "wfrec_eclose_eq2";
   2.392 +val transrec = thm "transrec";
   2.393 +val def_transrec = thm "def_transrec";
   2.394 +val transrec_type = thm "transrec_type";
   2.395 +val eclose_sing_Ord = thm "eclose_sing_Ord";
   2.396 +val Ord_transrec_type = thm "Ord_transrec_type";
   2.397 +val rank = thm "rank";
   2.398 +val Ord_rank = thm "Ord_rank";
   2.399 +val rank_of_Ord = thm "rank_of_Ord";
   2.400 +val rank_lt = thm "rank_lt";
   2.401 +val eclose_rank_lt = thm "eclose_rank_lt";
   2.402 +val rank_mono = thm "rank_mono";
   2.403 +val rank_Pow = thm "rank_Pow";
   2.404 +val rank_0 = thm "rank_0";
   2.405 +val rank_succ = thm "rank_succ";
   2.406 +val rank_Union = thm "rank_Union";
   2.407 +val rank_eclose = thm "rank_eclose";
   2.408 +val rank_pair1 = thm "rank_pair1";
   2.409 +val rank_pair2 = thm "rank_pair2";
   2.410 +val the_equality_if = thm "the_equality_if";
   2.411 +val rank_apply = thm "rank_apply";
   2.412 +val mem_eclose_subset = thm "mem_eclose_subset";
   2.413 +val eclose_mono = thm "eclose_mono";
   2.414 +val eclose_idem = thm "eclose_idem";
   2.415 +val transrec2_0 = thm "transrec2_0";
   2.416 +val transrec2_succ = thm "transrec2_succ";
   2.417 +val transrec2_Limit = thm "transrec2_Limit";
   2.418 +val recursor_lemma = thm "recursor_lemma";
   2.419 +val recursor_0 = thm "recursor_0";
   2.420 +val recursor_succ = thm "recursor_succ";
   2.421 +val rec_0 = thm "rec_0";
   2.422 +val rec_succ = thm "rec_succ";
   2.423 +val rec_type = thm "rec_type";
   2.424 +*}
   2.425  
   2.426  end
     3.1 --- a/src/ZF/IsaMakefile	Sat May 18 20:08:17 2002 +0200
     3.2 +++ b/src/ZF/IsaMakefile	Sat May 18 22:22:23 2002 +0200
     3.3 @@ -31,7 +31,7 @@
     3.4  $(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.ML	\
     3.5    ArithSimp.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy		\
     3.6    CardinalArith.ML CardinalArith.thy Cardinal_AC.thy \
     3.7 -  Datatype.ML Datatype.thy Epsilon.ML Epsilon.thy Finite.ML Finite.thy	\
     3.8 +  Datatype.ML Datatype.thy Epsilon.thy Finite.ML Finite.thy	\
     3.9    Fixedpt.ML Fixedpt.thy Inductive.ML Inductive.thy 	\
    3.10    InfDatatype.thy Integ/Bin.ML Integ/Bin.thy Integ/EquivClass.ML	\
    3.11    Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy	\
    3.12 @@ -39,8 +39,7 @@
    3.13    Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy	\
    3.14    Main_ZFC.ML Main_ZFC.thy	\
    3.15    Nat.ML Nat.thy Order.thy OrderArith.thy	\
    3.16 -  OrderType.thy Ordinal.thy OrdQuant.ML OrdQuant.thy \
    3.17 -  Perm.ML Perm.thy	\
    3.18 +  OrderType.thy Ordinal.thy OrdQuant.ML OrdQuant.thy Perm.ML Perm.thy	\
    3.19    QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML	\
    3.20    Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
    3.21    Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\