src/ZF/Constructible/Normal.thy
changeset 21404 eb85850d3eb7
parent 21233 5a5c8ea5f66a
child 32960 69916a850301
     1.1 --- a/src/ZF/Constructible/Normal.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/ZF/Constructible/Normal.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -19,13 +19,15 @@
     1.4  subsection {*Closed and Unbounded (c.u.) Classes of Ordinals*}
     1.5  
     1.6  definition
     1.7 -  Closed :: "(i=>o) => o"
     1.8 +  Closed :: "(i=>o) => o" where
     1.9      "Closed(P) == \<forall>I. I \<noteq> 0 --> (\<forall>i\<in>I. Ord(i) \<and> P(i)) --> P(\<Union>(I))"
    1.10  
    1.11 -  Unbounded :: "(i=>o) => o"
    1.12 +definition
    1.13 +  Unbounded :: "(i=>o) => o" where
    1.14      "Unbounded(P) == \<forall>i. Ord(i) --> (\<exists>j. i<j \<and> P(j))"
    1.15  
    1.16 -  Closed_Unbounded :: "(i=>o) => o"
    1.17 +definition
    1.18 +  Closed_Unbounded :: "(i=>o) => o" where
    1.19      "Closed_Unbounded(P) == Closed(P) \<and> Unbounded(P)"
    1.20  
    1.21  
    1.22 @@ -201,16 +203,19 @@
    1.23  subsection {*Normal Functions*} 
    1.24  
    1.25  definition
    1.26 -  mono_le_subset :: "(i=>i) => o"
    1.27 +  mono_le_subset :: "(i=>i) => o" where
    1.28      "mono_le_subset(M) == \<forall>i j. i\<le>j --> M(i) \<subseteq> M(j)"
    1.29  
    1.30 -  mono_Ord :: "(i=>i) => o"
    1.31 +definition
    1.32 +  mono_Ord :: "(i=>i) => o" where
    1.33      "mono_Ord(F) == \<forall>i j. i<j --> F(i) < F(j)"
    1.34  
    1.35 -  cont_Ord :: "(i=>i) => o"
    1.36 +definition
    1.37 +  cont_Ord :: "(i=>i) => o" where
    1.38      "cont_Ord(F) == \<forall>l. Limit(l) --> F(l) = (\<Union>i<l. F(i))"
    1.39  
    1.40 -  Normal :: "(i=>i) => o"
    1.41 +definition
    1.42 +  Normal :: "(i=>i) => o" where
    1.43      "Normal(F) == mono_Ord(F) \<and> cont_Ord(F)"
    1.44  
    1.45  
    1.46 @@ -373,7 +378,7 @@
    1.47        normal function, by @{thm [source] Normal_imp_fp_Unbounded}.
    1.48  *}
    1.49  definition
    1.50 -  normalize :: "[i=>i, i] => i"
    1.51 +  normalize :: "[i=>i, i] => i" where
    1.52      "normalize(F,a) == transrec2(a, F(0), \<lambda>x r. F(succ(x)) Un succ(r))"
    1.53  
    1.54  
    1.55 @@ -425,7 +430,7 @@
    1.56  numbers.*}
    1.57  
    1.58  definition
    1.59 -  Aleph :: "i => i"
    1.60 +  Aleph :: "i => i" where
    1.61      "Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))"
    1.62  
    1.63  notation (xsymbols)