src/ZF/Epsilon.thy
changeset 13203 fac77a839aa2
parent 13185 da61bfa0a391
child 13217 bc5dc2392578
     1.1 --- a/src/ZF/Epsilon.thy	Wed Jun 05 12:24:14 2002 +0200
     1.2 +++ b/src/ZF/Epsilon.thy	Wed Jun 05 15:34:55 2002 +0200
     1.3 @@ -66,7 +66,9 @@
     1.4     [| a: eclose(A);  !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) 
     1.5     |] ==> P(a) 
     1.6  *)
     1.7 -lemmas eclose_induct = Transset_induct [OF _ Transset_eclose]
     1.8 +lemmas eclose_induct =
     1.9 +     Transset_induct [OF _ Transset_eclose, induct set: eclose]
    1.10 +
    1.11  
    1.12  (*Epsilon induction*)
    1.13  lemma eps_induct:
    1.14 @@ -105,6 +107,9 @@
    1.15  apply (blast intro: arg_subset_eclose [THEN subsetD])
    1.16  done
    1.17  
    1.18 +(*fixed up for induct method*)
    1.19 +lemmas eclose_induct_down = eclose_induct_down [consumes 1]
    1.20 +
    1.21  lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X"
    1.22  apply (erule equalityI [OF eclose_least arg_subset_eclose])
    1.23  apply (rule subset_refl)
    1.24 @@ -327,6 +332,13 @@
    1.25  apply (auto simp add: OUnion_def); 
    1.26  done
    1.27  
    1.28 +lemma def_transrec2:
    1.29 +     "(!!x. f(x)==transrec2(x,a,b))
    1.30 +      ==> f(0) = a & 
    1.31 +          f(succ(i)) = b(i, f(i)) & 
    1.32 +          (Limit(K) --> f(K) = (UN j<K. f(j)))"
    1.33 +by (simp add: transrec2_Limit)
    1.34 +
    1.35  
    1.36  (** recursor -- better than nat_rec; the succ case has no type requirement! **)
    1.37