src/ZF/Main_ZF.thy
changeset 46953 2b6e55924af3
parent 46820 c656222c4dc1
child 58871 c399ae4b836f
     1.1 --- a/src/ZF/Main_ZF.thy	Thu Mar 15 15:54:22 2012 +0000
     1.2 +++ b/src/ZF/Main_ZF.thy	Thu Mar 15 16:35:02 2012 +0000
     1.3 @@ -23,21 +23,21 @@
     1.4    iterates_omega  ("(_^\<omega> '(_'))" [60,1000] 60)
     1.5  
     1.6  lemma iterates_triv:
     1.7 -     "[| n\<in>nat;  F(x) = x |] ==> F^n (x) = x"  
     1.8 +     "[| n\<in>nat;  F(x) = x |] ==> F^n (x) = x"
     1.9  by (induct n rule: nat_induct, simp_all)
    1.10  
    1.11  lemma iterates_type [TC]:
    1.12 -     "[| n:nat;  a: A; !!x. x:A ==> F(x) \<in> A |] 
    1.13 -      ==> F^n (a) \<in> A"  
    1.14 +     "[| n \<in> nat;  a \<in> A; !!x. x \<in> A ==> F(x) \<in> A |]
    1.15 +      ==> F^n (a) \<in> A"
    1.16  by (induct n rule: nat_induct, simp_all)
    1.17  
    1.18  lemma iterates_omega_triv:
    1.19 -    "F(x) = x ==> F^\<omega> (x) = x" 
    1.20 -by (simp add: iterates_omega_def iterates_triv) 
    1.21 +    "F(x) = x ==> F^\<omega> (x) = x"
    1.22 +by (simp add: iterates_omega_def iterates_triv)
    1.23  
    1.24  lemma Ord_iterates [simp]:
    1.25 -     "[| n\<in>nat;  !!i. Ord(i) ==> Ord(F(i));  Ord(x) |] 
    1.26 -      ==> Ord(F^n (x))"  
    1.27 +     "[| n\<in>nat;  !!i. Ord(i) ==> Ord(F(i));  Ord(x) |]
    1.28 +      ==> Ord(F^n (x))"
    1.29  by (induct n rule: nat_induct, simp_all)
    1.30  
    1.31  lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))"
    1.32 @@ -46,12 +46,12 @@
    1.33  
    1.34  subsection{* Transfinite Recursion *}
    1.35  
    1.36 -text{*Transfinite recursion for definitions based on the 
    1.37 +text{*Transfinite recursion for definitions based on the
    1.38      three cases of ordinals*}
    1.39  
    1.40  definition
    1.41    transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where
    1.42 -    "transrec3(k, a, b, c) ==                     
    1.43 +    "transrec3(k, a, b, c) ==
    1.44         transrec(k, \<lambda>x r.
    1.45           if x=0 then a
    1.46           else if Limit(x) then c(x, \<lambda>y\<in>x. r`y)
    1.47 @@ -65,7 +65,7 @@
    1.48  by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
    1.49  
    1.50  lemma transrec3_Limit:
    1.51 -     "Limit(i) ==> 
    1.52 +     "Limit(i) ==>
    1.53        transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))"
    1.54  by (rule transrec3_def [THEN def_transrec, THEN trans], force)
    1.55