src/ZF/Constructible/L_axioms.thy
 changeset 13493 5aa68c051725 parent 13440 cdde97e1db1c child 13496 6f0c57def6d5
```     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Mon Aug 12 17:59:57 2002 +0200
1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Mon Aug 12 18:01:44 2002 +0200
1.3 @@ -1464,6 +1464,41 @@
1.4               empty_reflection successor_reflection)
1.5  done
1.6
1.7 +subsubsection{*Finite Ordinals: The Predicate ``Is A Natural Number''*}
1.8 +
1.9 +(*     "finite_ordinal(M,a) ==
1.10 +	ordinal(M,a) & ~ limit_ordinal(M,a) &
1.11 +        (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))" *)
1.12 +constdefs finite_ordinal_fm :: "i=>i"
1.13 +    "finite_ordinal_fm(x) ==
1.14 +       And(ordinal_fm(x),
1.15 +          And(Neg(limit_ordinal_fm(x)),
1.16 +           Forall(Implies(Member(0,succ(x)),
1.17 +                          Neg(limit_ordinal_fm(0))))))"
1.18 +
1.19 +lemma finite_ordinal_type [TC]:
1.20 +     "x \<in> nat ==> finite_ordinal_fm(x) \<in> formula"
1.22 +
1.23 +lemma sats_finite_ordinal_fm [simp]:
1.24 +   "[| x \<in> nat; env \<in> list(A)|]
1.25 +    ==> sats(A, finite_ordinal_fm(x), env) <-> finite_ordinal(**A, nth(x,env))"
1.26 +by (simp add: finite_ordinal_fm_def sats_ordinal_fm' finite_ordinal_def)
1.27 +
1.28 +lemma finite_ordinal_iff_sats:
1.29 +      "[| nth(i,env) = x; nth(j,env) = y;
1.30 +          i \<in> nat; env \<in> list(A)|]
1.31 +       ==> finite_ordinal(**A, x) <-> sats(A, finite_ordinal_fm(i), env)"
1.32 +by simp
1.33 +
1.34 +theorem finite_ordinal_reflection:
1.35 +     "REFLECTS[\<lambda>x. finite_ordinal(L,f(x)),
1.36 +               \<lambda>i x. finite_ordinal(**Lset(i),f(x))]"
1.37 +apply (simp only: finite_ordinal_def setclass_simps)
1.38 +apply (intro FOL_reflections ordinal_reflection limit_ordinal_reflection)
1.39 +done
1.40 +
1.41 +
1.42  subsubsection{*Omega: The Set of Natural Numbers*}
1.43
1.44  (* omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x)) *)
```