src/ZF/Constructible/Datatype_absolute.thy
changeset 13269 3ba9be497c33
parent 13268 240509babf00
child 13293 09276ee04361
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Mon Jul 01 18:16:18 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Jul 02 13:28:08 2002 +0200
     1.3 @@ -1,28 +1,4 @@
     1.4 -theory Datatype_absolute = WF_absolute:
     1.5 -
     1.6 -(*Epsilon.thy*)
     1.7 -lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})"
     1.8 -apply (insert arg_subset_eclose [of "{i}"], simp) 
     1.9 -apply (frule eclose_subset, blast) 
    1.10 -done
    1.11 -
    1.12 -lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)"
    1.13 -apply (rule equalityI)
    1.14 -apply (erule eclose_sing_Ord)  
    1.15 -apply (rule succ_subset_eclose_sing) 
    1.16 -done
    1.17 -
    1.18 -(*Ordinal.thy*)
    1.19 -lemma relation_Memrel: "relation(Memrel(A))"
    1.20 -by (simp add: relation_def Memrel_def, blast)
    1.21 -
    1.22 -lemma (in M_axioms) nat_case_closed:
    1.23 -  "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
    1.24 -apply (case_tac "k=0", simp) 
    1.25 -apply (case_tac "\<exists>m. k = succ(m)")
    1.26 -apply force 
    1.27 -apply (simp add: nat_case_def) 
    1.28 -done
    1.29 +theory Datatype_absolute = Formula + WF_absolute:
    1.30  
    1.31  
    1.32  subsection{*The lfp of a continuous function can be expressed as a union*}
    1.33 @@ -143,13 +119,16 @@
    1.34                wf_Memrel trans_Memrel relation_Memrel nat_case_closed)
    1.35  
    1.36  
    1.37 +
    1.38  locale M_datatypes = M_wfrank +
    1.39  (*THEY NEED RELATIVIZATION*)
    1.40    assumes list_replacement1: 
    1.41  	   "[|M(A); n \<in> nat|] ==> 
    1.42  	    strong_replacement(M, 
    1.43 -	      \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) &
    1.44 -		     is_recfun (Memrel(succ(n)), x,
    1.45 +	      \<lambda>x z. \<exists>y[M]. \<exists>g[M]. \<exists>sucn[M]. \<exists>memr[M]. 
    1.46 +                     pair(M,x,y,z) & successor(M,n,sucn) & 
    1.47 +                     membership(M,sucn,memr) &
    1.48 +		     is_recfun (memr, x,
    1.49  				\<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
    1.50  		     y = nat_case(0, \<lambda>m. {0} + A \<times> g`m, x))"
    1.51        and list_replacement2': 
    1.52 @@ -159,11 +138,11 @@
    1.53  lemma (in M_datatypes) list_replacement1':
    1.54    "[|M(A); n \<in> nat|]
    1.55     ==> strong_replacement
    1.56 -	  (M, \<lambda>x y. \<exists>z[M]. \<exists>g[M]. y = \<langle>x, z\<rangle> &
    1.57 +	  (M, \<lambda>x y. \<exists>z[M]. \<exists>g[M]. y = \<langle>x,z\<rangle> &
    1.58                 is_recfun (Memrel(succ(n)), x,
    1.59 -		          \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f ` m, n), g) &
    1.60 +		          \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
    1.61   	       z = nat_case(0, \<lambda>m. {0} + A \<times> g ` m, x))"
    1.62 -by (insert list_replacement1, simp) 
    1.63 +by (insert list_replacement1, simp add: nat_into_M) 
    1.64  
    1.65  
    1.66  lemma (in M_datatypes) list_closed [intro,simp]: