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)
```