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.21 +by (simp add: finite_ordinal_fm_def)
    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)) *)