src/ZF/Epsilon.thy
changeset 13269 3ba9be497c33
parent 13217 bc5dc2392578
child 13328 703de709a64b
     1.1 --- a/src/ZF/Epsilon.thy	Mon Jul 01 18:16:18 2002 +0200
     1.2 +++ b/src/ZF/Epsilon.thy	Tue Jul 02 13:28:08 2002 +0200
     1.3 @@ -181,6 +181,17 @@
     1.4  apply (rule succI1 [THEN singleton_subsetI])
     1.5  done
     1.6  
     1.7 +lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})"
     1.8 +apply (insert arg_subset_eclose [of "{i}"], simp) 
     1.9 +apply (frule eclose_subset, blast) 
    1.10 +done
    1.11 +
    1.12 +lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)"
    1.13 +apply (rule equalityI)
    1.14 +apply (erule eclose_sing_Ord)  
    1.15 +apply (rule succ_subset_eclose_sing) 
    1.16 +done
    1.17 +
    1.18  lemma Ord_transrec_type:
    1.19    assumes jini: "j: i"
    1.20        and ordi: "Ord(i)"
    1.21 @@ -291,8 +302,8 @@
    1.22    r = {<0,0>,<0,1>,<0,2>,...}.  Then f`0 = Union(f``{0}) = Union(nat) = nat,
    1.23    whose rank equals that of r.*)
    1.24  lemma rank_apply: "[|i : domain(f); function(f)|] ==> rank(f`i) < rank(f)"
    1.25 -apply (clarify );  
    1.26 -apply (simp add: function_apply_equality); 
    1.27 +apply clarify  
    1.28 +apply (simp add: function_apply_equality) 
    1.29  apply (blast intro: lt_trans rank_lt rank_pair2)
    1.30  done
    1.31  
    1.32 @@ -332,7 +343,7 @@
    1.33  lemma transrec2_Limit:
    1.34       "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"
    1.35  apply (rule transrec2_def [THEN def_transrec, THEN trans])
    1.36 -apply (auto simp add: OUnion_def); 
    1.37 +apply (auto simp add: OUnion_def) 
    1.38  done
    1.39  
    1.40  lemma def_transrec2: