src/ZF/Constructible/Relative.thy
changeset 13269 3ba9be497c33
parent 13268 240509babf00
child 13290 28ce81eff3de
     1.1 --- a/src/ZF/Constructible/Relative.thy	Mon Jul 01 18:16:18 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Jul 02 13:28:08 2002 +0200
     1.3 @@ -2,11 +2,6 @@
     1.4  
     1.5  theory Relative = Main:
     1.6  
     1.7 -(*func.thy*)
     1.8 -lemma succ_fun_eq: "succ(n) -> B = (\<Union>f \<in> n->B. \<Union>b\<in>B. {cons(<n,b>, f)})"
     1.9 -by (simp add: succ_def mem_not_refl cons_fun_eq)
    1.10 -
    1.11 -
    1.12  subsection{* Relativized versions of standard set-theoretic concepts *}
    1.13  
    1.14  constdefs
    1.15 @@ -899,6 +894,13 @@
    1.16       "n \<in> nat ==> M(n)"
    1.17  by (induct n rule: nat_induct, simp_all)
    1.18  
    1.19 +lemma (in M_axioms) nat_case_closed:
    1.20 +  "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
    1.21 +apply (case_tac "k=0", simp) 
    1.22 +apply (case_tac "\<exists>m. k = succ(m)", force)
    1.23 +apply (simp add: nat_case_def) 
    1.24 +done
    1.25 +
    1.26  lemma (in M_axioms) Inl_in_M_iff [iff]:
    1.27       "M(Inl(a)) <-> M(a)"
    1.28  by (simp add: Inl_def)