src/ZF/Epsilon.thy
author paulson
Tue Jul 09 23:05:26 2002 +0200 (2002-07-09)
changeset 13328 703de709a64b
parent 13269 3ba9be497c33
child 13356 c9cfe1638bf2
permissions -rw-r--r--
better document preparation
     1 (*  Title:      ZF/epsilon.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 *)
     7 
     8 header{*Epsilon Induction and Recursion*}
     9 
    10 theory Epsilon = Nat + mono:
    11 
    12 constdefs
    13   eclose    :: "i=>i"
    14     "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
    15 
    16   transrec  :: "[i, [i,i]=>i] =>i"
    17     "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
    18  
    19   rank      :: "i=>i"
    20     "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
    21 
    22   transrec2 :: "[i, i, [i,i]=>i] =>i"
    23     "transrec2(k, a, b) ==                     
    24        transrec(k, 
    25                 %i r. if(i=0, a, 
    26                         if(EX j. i=succ(j),        
    27                            b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
    28                            UN j<i. r`j)))"
    29 
    30   recursor  :: "[i, [i,i]=>i, i]=>i"
    31     "recursor(a,b,k) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
    32 
    33   rec  :: "[i, i, [i,i]=>i]=>i"
    34     "rec(k,a,b) == recursor(a,b,k)"
    35 
    36 
    37 (*** Basic closure properties ***)
    38 
    39 lemma arg_subset_eclose: "A <= eclose(A)"
    40 apply (unfold eclose_def)
    41 apply (rule nat_rec_0 [THEN equalityD2, THEN subset_trans])
    42 apply (rule nat_0I [THEN UN_upper])
    43 done
    44 
    45 lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD, standard]
    46 
    47 lemma Transset_eclose: "Transset(eclose(A))"
    48 apply (unfold eclose_def Transset_def)
    49 apply (rule subsetI [THEN ballI])
    50 apply (erule UN_E)
    51 apply (rule nat_succI [THEN UN_I], assumption)
    52 apply (erule nat_rec_succ [THEN ssubst])
    53 apply (erule UnionI, assumption)
    54 done
    55 
    56 (* x : eclose(A) ==> x <= eclose(A) *)
    57 lemmas eclose_subset =  
    58        Transset_eclose [unfolded Transset_def, THEN bspec, standard]
    59 
    60 (* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
    61 lemmas ecloseD = eclose_subset [THEN subsetD, standard]
    62 
    63 lemmas arg_in_eclose_sing = arg_subset_eclose [THEN singleton_subsetD]
    64 lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD, standard]
    65 
    66 (* This is epsilon-induction for eclose(A); see also eclose_induct_down...
    67    [| a: eclose(A);  !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) 
    68    |] ==> P(a) 
    69 *)
    70 lemmas eclose_induct =
    71      Transset_induct [OF _ Transset_eclose, induct set: eclose]
    72 
    73 
    74 (*Epsilon induction*)
    75 lemma eps_induct:
    76     "[| !!x. ALL y:x. P(y) ==> P(x) |]  ==>  P(a)"
    77 by (rule arg_in_eclose_sing [THEN eclose_induct], blast) 
    78 
    79 
    80 (*** Leastness of eclose ***)
    81 
    82 (** eclose(A) is the least transitive set including A as a subset. **)
    83 
    84 lemma eclose_least_lemma: 
    85     "[| Transset(X);  A<=X;  n: nat |] ==> nat_rec(n, A, %m r. Union(r)) <= X"
    86 apply (unfold Transset_def)
    87 apply (erule nat_induct) 
    88 apply (simp add: nat_rec_0)
    89 apply (simp add: nat_rec_succ, blast)
    90 done
    91 
    92 lemma eclose_least: 
    93      "[| Transset(X);  A<=X |] ==> eclose(A) <= X"
    94 apply (unfold eclose_def)
    95 apply (rule eclose_least_lemma [THEN UN_least], assumption+)
    96 done
    97 
    98 (*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
    99 lemma eclose_induct_down: 
   100     "[| a: eclose(b);                                            
   101         !!y.   [| y: b |] ==> P(y);                              
   102         !!y z. [| y: eclose(b);  P(y);  z: y |] ==> P(z)         
   103      |] ==> P(a)"
   104 apply (rule eclose_least [THEN subsetD, THEN CollectD2, of "eclose(b)"])
   105   prefer 3 apply assumption
   106  apply (unfold Transset_def) 
   107  apply (blast intro: ecloseD)
   108 apply (blast intro: arg_subset_eclose [THEN subsetD])
   109 done
   110 
   111 (*fixed up for induct method*)
   112 lemmas eclose_induct_down = eclose_induct_down [consumes 1]
   113 
   114 lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X"
   115 apply (erule equalityI [OF eclose_least arg_subset_eclose])
   116 apply (rule subset_refl)
   117 done
   118 
   119 
   120 (*** Epsilon recursion ***)
   121 
   122 (*Unused...*)
   123 lemma mem_eclose_trans: "[| A: eclose(B);  B: eclose(C) |] ==> A: eclose(C)"
   124 by (rule eclose_least [OF Transset_eclose eclose_subset, THEN subsetD], 
   125     assumption+)
   126 
   127 (*Variant of the previous lemma in a useable form for the sequel*)
   128 lemma mem_eclose_sing_trans:
   129      "[| A: eclose({B});  B: eclose({C}) |] ==> A: eclose({C})"
   130 by (rule eclose_least [OF Transset_eclose singleton_subsetI, THEN subsetD], 
   131     assumption+)
   132 
   133 lemma under_Memrel: "[| Transset(i);  j:i |] ==> Memrel(i)-``{j} = j"
   134 by (unfold Transset_def, blast)
   135 
   136 lemma lt_Memrel: "j < i ==> Memrel(i) -`` {j} = j"
   137 by (simp add: lt_def Ord_def under_Memrel) 
   138 
   139 (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
   140 lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel, standard]
   141 
   142 lemmas wfrec_ssubst = wf_Memrel [THEN wfrec, THEN ssubst]
   143 
   144 lemma wfrec_eclose_eq:
   145     "[| k:eclose({j});  j:eclose({i}) |] ==>  
   146      wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)"
   147 apply (erule eclose_induct)
   148 apply (rule wfrec_ssubst)
   149 apply (rule wfrec_ssubst)
   150 apply (simp add: under_Memrel_eclose mem_eclose_sing_trans [of _ j i])
   151 done
   152 
   153 lemma wfrec_eclose_eq2: 
   154     "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)"
   155 apply (rule arg_in_eclose_sing [THEN wfrec_eclose_eq])
   156 apply (erule arg_into_eclose_sing)
   157 done
   158 
   159 lemma transrec: "transrec(a,H) = H(a, lam x:a. transrec(x,H))"
   160 apply (unfold transrec_def)
   161 apply (rule wfrec_ssubst)
   162 apply (simp add: wfrec_eclose_eq2 arg_in_eclose_sing under_Memrel_eclose)
   163 done
   164 
   165 (*Avoids explosions in proofs; resolve it with a meta-level definition.*)
   166 lemma def_transrec:
   167     "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))"
   168 apply simp
   169 apply (rule transrec)
   170 done
   171 
   172 lemma transrec_type:
   173     "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x) |]
   174      ==> transrec(a,H) : B(a)"
   175 apply (rule_tac i = "a" in arg_in_eclose_sing [THEN eclose_induct])
   176 apply (subst transrec)
   177 apply (simp add: lam_type) 
   178 done
   179 
   180 lemma eclose_sing_Ord: "Ord(i) ==> eclose({i}) <= succ(i)"
   181 apply (erule Ord_is_Transset [THEN Transset_succ, THEN eclose_least])
   182 apply (rule succI1 [THEN singleton_subsetI])
   183 done
   184 
   185 lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})"
   186 apply (insert arg_subset_eclose [of "{i}"], simp) 
   187 apply (frule eclose_subset, blast) 
   188 done
   189 
   190 lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)"
   191 apply (rule equalityI)
   192 apply (erule eclose_sing_Ord)  
   193 apply (rule succ_subset_eclose_sing) 
   194 done
   195 
   196 lemma Ord_transrec_type:
   197   assumes jini: "j: i"
   198       and ordi: "Ord(i)"
   199       and minor: " !!x u. [| x: i;  u: Pi(x,B) |] ==> H(x,u) : B(x)"
   200   shows "transrec(j,H) : B(j)"
   201 apply (rule transrec_type)
   202 apply (insert jini ordi)
   203 apply (blast intro!: minor
   204              intro: Ord_trans 
   205              dest: Ord_in_Ord [THEN eclose_sing_Ord, THEN subsetD])
   206 done
   207 
   208 (*** Rank ***)
   209 
   210 (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
   211 lemma rank: "rank(a) = (UN y:a. succ(rank(y)))"
   212 by (subst rank_def [THEN def_transrec], simp)
   213 
   214 lemma Ord_rank [simp]: "Ord(rank(a))"
   215 apply (rule_tac a="a" in eps_induct) 
   216 apply (subst rank)
   217 apply (rule Ord_succ [THEN Ord_UN])
   218 apply (erule bspec, assumption)
   219 done
   220 
   221 lemma rank_of_Ord: "Ord(i) ==> rank(i) = i"
   222 apply (erule trans_induct)
   223 apply (subst rank)
   224 apply (simp add: Ord_equality)
   225 done
   226 
   227 lemma rank_lt: "a:b ==> rank(a) < rank(b)"
   228 apply (rule_tac a1 = "b" in rank [THEN ssubst])
   229 apply (erule UN_I [THEN ltI])
   230 apply (rule_tac [2] Ord_UN, auto)
   231 done
   232 
   233 lemma eclose_rank_lt: "a: eclose(b) ==> rank(a) < rank(b)"
   234 apply (erule eclose_induct_down)
   235 apply (erule rank_lt)
   236 apply (erule rank_lt [THEN lt_trans], assumption)
   237 done
   238 
   239 lemma rank_mono: "a<=b ==> rank(a) le rank(b)"
   240 apply (rule subset_imp_le)
   241 apply (subst rank)
   242 apply (subst rank, auto)
   243 done
   244 
   245 lemma rank_Pow: "rank(Pow(a)) = succ(rank(a))"
   246 apply (rule rank [THEN trans])
   247 apply (rule le_anti_sym)
   248 apply (rule_tac [2] UN_upper_le)
   249 apply (rule UN_least_le)
   250 apply (auto intro: rank_mono simp add: Ord_UN)
   251 done
   252 
   253 lemma rank_0 [simp]: "rank(0) = 0"
   254 by (rule rank [THEN trans], blast)
   255 
   256 lemma rank_succ [simp]: "rank(succ(x)) = succ(rank(x))"
   257 apply (rule rank [THEN trans])
   258 apply (rule equalityI [OF UN_least succI1 [THEN UN_upper]])
   259 apply (erule succE, blast)
   260 apply (erule rank_lt [THEN leI, THEN succ_leI, THEN le_imp_subset])
   261 done
   262 
   263 lemma rank_Union: "rank(Union(A)) = (UN x:A. rank(x))"
   264 apply (rule equalityI)
   265 apply (rule_tac [2] rank_mono [THEN le_imp_subset, THEN UN_least])
   266 apply (erule_tac [2] Union_upper)
   267 apply (subst rank)
   268 apply (rule UN_least)
   269 apply (erule UnionE)
   270 apply (rule subset_trans)
   271 apply (erule_tac [2] RepFunI [THEN Union_upper])
   272 apply (erule rank_lt [THEN succ_leI, THEN le_imp_subset])
   273 done
   274 
   275 lemma rank_eclose: "rank(eclose(a)) = rank(a)"
   276 apply (rule le_anti_sym)
   277 apply (rule_tac [2] arg_subset_eclose [THEN rank_mono])
   278 apply (rule_tac a1 = "eclose (a) " in rank [THEN ssubst])
   279 apply (rule Ord_rank [THEN UN_least_le])
   280 apply (erule eclose_rank_lt [THEN succ_leI])
   281 done
   282 
   283 lemma rank_pair1: "rank(a) < rank(<a,b>)"
   284 apply (unfold Pair_def)
   285 apply (rule consI1 [THEN rank_lt, THEN lt_trans])
   286 apply (rule consI1 [THEN consI2, THEN rank_lt])
   287 done
   288 
   289 lemma rank_pair2: "rank(b) < rank(<a,b>)"
   290 apply (unfold Pair_def)
   291 apply (rule consI1 [THEN consI2, THEN rank_lt, THEN lt_trans])
   292 apply (rule consI1 [THEN consI2, THEN rank_lt])
   293 done
   294 
   295 (*Not clear how to remove the P(a) condition, since the "then" part
   296   must refer to "a"*)
   297 lemma the_equality_if:
   298      "P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)"
   299 by (simp add: the_0 the_equality2)
   300 
   301 (*The first premise not only fixs i but ensures f~=0.
   302   The second premise is now essential.  Consider otherwise the relation 
   303   r = {<0,0>,<0,1>,<0,2>,...}.  Then f`0 = Union(f``{0}) = Union(nat) = nat,
   304   whose rank equals that of r.*)
   305 lemma rank_apply: "[|i : domain(f); function(f)|] ==> rank(f`i) < rank(f)"
   306 apply clarify  
   307 apply (simp add: function_apply_equality) 
   308 apply (blast intro: lt_trans rank_lt rank_pair2)
   309 done
   310 
   311 
   312 (*** Corollaries of leastness ***)
   313 
   314 lemma mem_eclose_subset: "A:B ==> eclose(A)<=eclose(B)"
   315 apply (rule Transset_eclose [THEN eclose_least])
   316 apply (erule arg_into_eclose [THEN eclose_subset])
   317 done
   318 
   319 lemma eclose_mono: "A<=B ==> eclose(A) <= eclose(B)"
   320 apply (rule Transset_eclose [THEN eclose_least])
   321 apply (erule subset_trans)
   322 apply (rule arg_subset_eclose)
   323 done
   324 
   325 (** Idempotence of eclose **)
   326 
   327 lemma eclose_idem: "eclose(eclose(A)) = eclose(A)"
   328 apply (rule equalityI)
   329 apply (rule eclose_least [OF Transset_eclose subset_refl])
   330 apply (rule arg_subset_eclose)
   331 done
   332 
   333 (** Transfinite recursion for definitions based on the 
   334     three cases of ordinals **)
   335 
   336 lemma transrec2_0 [simp]: "transrec2(0,a,b) = a"
   337 by (rule transrec2_def [THEN def_transrec, THEN trans], simp)
   338 
   339 lemma transrec2_succ [simp]: "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))"
   340 apply (rule transrec2_def [THEN def_transrec, THEN trans])
   341 apply (simp add: the_equality if_P)
   342 done
   343 
   344 lemma transrec2_Limit:
   345      "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"
   346 apply (rule transrec2_def [THEN def_transrec, THEN trans])
   347 apply (auto simp add: OUnion_def) 
   348 done
   349 
   350 lemma def_transrec2:
   351      "(!!x. f(x)==transrec2(x,a,b))
   352       ==> f(0) = a & 
   353           f(succ(i)) = b(i, f(i)) & 
   354           (Limit(K) --> f(K) = (UN j<K. f(j)))"
   355 by (simp add: transrec2_Limit)
   356 
   357 
   358 (** recursor -- better than nat_rec; the succ case has no type requirement! **)
   359 
   360 (*NOT suitable for rewriting*)
   361 lemmas recursor_lemma = recursor_def [THEN def_transrec, THEN trans]
   362 
   363 lemma recursor_0: "recursor(a,b,0) = a"
   364 by (rule nat_case_0 [THEN recursor_lemma])
   365 
   366 lemma recursor_succ: "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))"
   367 by (rule recursor_lemma, simp)
   368 
   369 
   370 (** rec: old version for compatibility **)
   371 
   372 lemma rec_0 [simp]: "rec(0,a,b) = a"
   373 apply (unfold rec_def)
   374 apply (rule recursor_0)
   375 done
   376 
   377 lemma rec_succ [simp]: "rec(succ(m),a,b) = b(m, rec(m,a,b))"
   378 apply (unfold rec_def)
   379 apply (rule recursor_succ)
   380 done
   381 
   382 lemma rec_type:
   383     "[| n: nat;   
   384         a: C(0);   
   385         !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m)) |]
   386      ==> rec(n,a,b) : C(n)"
   387 by (erule nat_induct, auto)
   388 
   389 ML
   390 {*
   391 val arg_subset_eclose = thm "arg_subset_eclose";
   392 val arg_into_eclose = thm "arg_into_eclose";
   393 val Transset_eclose = thm "Transset_eclose";
   394 val eclose_subset = thm "eclose_subset";
   395 val ecloseD = thm "ecloseD";
   396 val arg_in_eclose_sing = thm "arg_in_eclose_sing";
   397 val arg_into_eclose_sing = thm "arg_into_eclose_sing";
   398 val eclose_induct = thm "eclose_induct";
   399 val eps_induct = thm "eps_induct";
   400 val eclose_least = thm "eclose_least";
   401 val eclose_induct_down = thm "eclose_induct_down";
   402 val Transset_eclose_eq_arg = thm "Transset_eclose_eq_arg";
   403 val mem_eclose_trans = thm "mem_eclose_trans";
   404 val mem_eclose_sing_trans = thm "mem_eclose_sing_trans";
   405 val under_Memrel = thm "under_Memrel";
   406 val under_Memrel_eclose = thm "under_Memrel_eclose";
   407 val wfrec_ssubst = thm "wfrec_ssubst";
   408 val wfrec_eclose_eq = thm "wfrec_eclose_eq";
   409 val wfrec_eclose_eq2 = thm "wfrec_eclose_eq2";
   410 val transrec = thm "transrec";
   411 val def_transrec = thm "def_transrec";
   412 val transrec_type = thm "transrec_type";
   413 val eclose_sing_Ord = thm "eclose_sing_Ord";
   414 val Ord_transrec_type = thm "Ord_transrec_type";
   415 val rank = thm "rank";
   416 val Ord_rank = thm "Ord_rank";
   417 val rank_of_Ord = thm "rank_of_Ord";
   418 val rank_lt = thm "rank_lt";
   419 val eclose_rank_lt = thm "eclose_rank_lt";
   420 val rank_mono = thm "rank_mono";
   421 val rank_Pow = thm "rank_Pow";
   422 val rank_0 = thm "rank_0";
   423 val rank_succ = thm "rank_succ";
   424 val rank_Union = thm "rank_Union";
   425 val rank_eclose = thm "rank_eclose";
   426 val rank_pair1 = thm "rank_pair1";
   427 val rank_pair2 = thm "rank_pair2";
   428 val the_equality_if = thm "the_equality_if";
   429 val rank_apply = thm "rank_apply";
   430 val mem_eclose_subset = thm "mem_eclose_subset";
   431 val eclose_mono = thm "eclose_mono";
   432 val eclose_idem = thm "eclose_idem";
   433 val transrec2_0 = thm "transrec2_0";
   434 val transrec2_succ = thm "transrec2_succ";
   435 val transrec2_Limit = thm "transrec2_Limit";
   436 val recursor_0 = thm "recursor_0";
   437 val recursor_succ = thm "recursor_succ";
   438 val rec_0 = thm "rec_0";
   439 val rec_succ = thm "rec_succ";
   440 val rec_type = thm "rec_type";
   441 *}
   442 
   443 end