src/ZF/Constructible/Datatype_absolute.thy
changeset 13395 4eb948d1eb4e
parent 13386 f3e9e8b21aba
child 13397 6e5f4d911435
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 18 12:10:24 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 18 15:21:42 2002 +0200
     1.3 @@ -268,6 +268,39 @@
     1.4  
     1.5  
     1.6  subsection{*@{term M} Contains the List and Formula Datatypes*}
     1.7 +
     1.8 +constdefs
     1.9 +  is_list_n :: "[i=>o,i,i,i] => o"
    1.10 +    "is_list_n(M,A,n,Z) == 
    1.11 +      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M]. 
    1.12 +       empty(M,zero) & 
    1.13 +       successor(M,n,sn) & membership(M,sn,msn) &
    1.14 +       is_wfrec(M, iterates_MH(M, is_list_functor(M,A),zero), msn, n, Z)"
    1.15 +  
    1.16 +  mem_list :: "[i=>o,i,i] => o"
    1.17 +    "mem_list(M,A,l) == 
    1.18 +      \<exists>n[M]. \<exists>listn[M]. 
    1.19 +       finite_ordinal(M,n) & is_list_n(M,A,n,listn) & l \<in> listn"
    1.20 +
    1.21 +  is_list :: "[i=>o,i,i] => o"
    1.22 +    "is_list(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_list(M,A,l)"
    1.23 +
    1.24 +constdefs
    1.25 +  is_formula_n :: "[i=>o,i,i] => o"
    1.26 +    "is_formula_n(M,n,Z) == 
    1.27 +      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M]. 
    1.28 +       empty(M,zero) & 
    1.29 +       successor(M,n,sn) & membership(M,sn,msn) &
    1.30 +       is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)"
    1.31 +  
    1.32 +  mem_formula :: "[i=>o,i] => o"
    1.33 +    "mem_formula(M,p) == 
    1.34 +      \<exists>n[M]. \<exists>formn[M]. 
    1.35 +       finite_ordinal(M,n) & is_formula_n(M,n,formn) & p \<in> formn"
    1.36 +
    1.37 +  is_formula :: "[i=>o,i] => o"
    1.38 +    "is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p)"
    1.39 +
    1.40  locale (open) M_datatypes = M_wfrank +
    1.41   assumes list_replacement1: 
    1.42     "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
    1.43 @@ -286,6 +319,9 @@
    1.44                 is_wfrec(M, iterates_MH(M,is_formula_functor(M), 0), 
    1.45                          msn, n, y)))"
    1.46  
    1.47 +
    1.48 +subsubsection{*Absoluteness of the List Construction*}
    1.49 +
    1.50  lemma (in M_datatypes) list_replacement2': 
    1.51    "M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. {0} + A * X)^n (0))"
    1.52  apply (insert list_replacement2 [of A]) 
    1.53 @@ -300,7 +336,28 @@
    1.54  by  (simp add: RepFun_closed2 list_eq_Union 
    1.55                 list_replacement2' relativize1_def
    1.56                 iterates_closed [of "is_list_functor(M,A)"])
    1.57 +lemma (in M_datatypes) is_list_n_abs [simp]:
    1.58 +     "[|M(A); n\<in>nat; M(Z)|] 
    1.59 +      ==> is_list_n(M,A,n,Z) <-> Z = (\<lambda>X. {0} + A * X)^n (0)"
    1.60 +apply (insert list_replacement1)
    1.61 +apply (simp add: is_list_n_def relativize1_def nat_into_M
    1.62 +                 iterates_abs [of "is_list_functor(M,A)" _ "\<lambda>X. {0} + A*X"])
    1.63 +done
    1.64  
    1.65 +lemma (in M_datatypes) mem_list_abs [simp]:
    1.66 +     "M(A) ==> mem_list(M,A,l) <-> l \<in> list(A)"
    1.67 +apply (insert list_replacement1)
    1.68 +apply (simp add: mem_list_def relativize1_def list_eq_Union
    1.69 +                 iterates_closed [of "is_list_functor(M,A)"]) 
    1.70 +done
    1.71 +
    1.72 +lemma (in M_datatypes) list_abs [simp]:
    1.73 +     "[|M(A); M(Z)|] ==> is_list(M,A,Z) <-> Z = list(A)"
    1.74 +apply (simp add: is_list_def, safe)
    1.75 +apply (rule M_equalityI, simp_all)
    1.76 +done
    1.77 +
    1.78 +subsubsection{*Absoluteness of Formulas*}
    1.79  
    1.80  lemma (in M_datatypes) formula_replacement2': 
    1.81    "strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))^n (0))"
    1.82 @@ -318,4 +375,151 @@
    1.83                    iterates_closed [of "is_formula_functor(M)"])
    1.84  done
    1.85  
    1.86 +lemma (in M_datatypes) is_formula_n_abs [simp]:
    1.87 +     "[|n\<in>nat; M(Z)|] 
    1.88 +      ==> is_formula_n(M,n,Z) <-> 
    1.89 +          Z = (\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))^n (0)"
    1.90 +apply (insert formula_replacement1)
    1.91 +apply (simp add: is_formula_n_def relativize1_def nat_into_M
    1.92 +                 iterates_abs [of "is_formula_functor(M)" _ 
    1.93 +                        "\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X))"])
    1.94 +done
    1.95 +
    1.96 +lemma (in M_datatypes) mem_formula_abs [simp]:
    1.97 +     "mem_formula(M,l) <-> l \<in> formula"
    1.98 +apply (insert formula_replacement1)
    1.99 +apply (simp add: mem_formula_def relativize1_def formula_eq_Union
   1.100 +                 iterates_closed [of "is_formula_functor(M)"]) 
   1.101 +done
   1.102 +
   1.103 +lemma (in M_datatypes) formula_abs [simp]:
   1.104 +     "[|M(Z)|] ==> is_formula(M,Z) <-> Z = formula"
   1.105 +apply (simp add: is_formula_def, safe)
   1.106 +apply (rule M_equalityI, simp_all)
   1.107 +done
   1.108 +
   1.109 +
   1.110 +subsection{*Absoluteness for @{text \<epsilon>}-Closure: the @{term eclose} Operator*}
   1.111 +
   1.112 +text{*Re-expresses eclose using "iterates"*}
   1.113 +lemma eclose_eq_Union:
   1.114 +     "eclose(A) = (\<Union>n\<in>nat. Union^n (A))"
   1.115 +apply (simp add: eclose_def) 
   1.116 +apply (rule UN_cong) 
   1.117 +apply (rule refl)
   1.118 +apply (induct_tac n)
   1.119 +apply (simp add: nat_rec_0)  
   1.120 +apply (simp add: nat_rec_succ) 
   1.121 +done
   1.122 +
   1.123 +constdefs
   1.124 +  is_eclose_n :: "[i=>o,i,i,i] => o"
   1.125 +    "is_eclose_n(M,A,n,Z) == 
   1.126 +      \<exists>sn[M]. \<exists>msn[M]. 
   1.127 +       successor(M,n,sn) & membership(M,sn,msn) &
   1.128 +       is_wfrec(M, iterates_MH(M, big_union(M), A), msn, n, Z)"
   1.129 +  
   1.130 +  mem_eclose :: "[i=>o,i,i] => o"
   1.131 +    "mem_eclose(M,A,l) == 
   1.132 +      \<exists>n[M]. \<exists>eclosen[M]. 
   1.133 +       finite_ordinal(M,n) & is_eclose_n(M,A,n,eclosen) & l \<in> eclosen"
   1.134 +
   1.135 +  is_eclose :: "[i=>o,i,i] => o"
   1.136 +    "is_eclose(M,A,Z) == \<forall>u[M]. u \<in> Z <-> mem_eclose(M,A,u)"
   1.137 +
   1.138 +
   1.139 +locale (open) M_eclose = M_wfrank +
   1.140 + assumes eclose_replacement1: 
   1.141 +   "M(A) ==> iterates_replacement(M, big_union(M), A)"
   1.142 +  and eclose_replacement2: 
   1.143 +   "M(A) ==> strong_replacement(M, 
   1.144 +         \<lambda>n y. n\<in>nat & 
   1.145 +               (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
   1.146 +               is_wfrec(M, iterates_MH(M,big_union(M), A), 
   1.147 +                        msn, n, y)))"
   1.148 +
   1.149 +lemma (in M_eclose) eclose_replacement2': 
   1.150 +  "M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = Union^n (A))"
   1.151 +apply (insert eclose_replacement2 [of A]) 
   1.152 +apply (rule strong_replacement_cong [THEN iffD1])  
   1.153 +apply (rule conj_cong [OF iff_refl iterates_abs [of "big_union(M)"]]) 
   1.154 +apply (simp_all add: eclose_replacement1 relativize1_def) 
   1.155 +done
   1.156 +
   1.157 +lemma (in M_eclose) eclose_closed [intro,simp]:
   1.158 +     "M(A) ==> M(eclose(A))"
   1.159 +apply (insert eclose_replacement1)
   1.160 +by  (simp add: RepFun_closed2 eclose_eq_Union 
   1.161 +               eclose_replacement2' relativize1_def
   1.162 +               iterates_closed [of "big_union(M)"])
   1.163 +
   1.164 +lemma (in M_eclose) is_eclose_n_abs [simp]:
   1.165 +     "[|M(A); n\<in>nat; M(Z)|] ==> is_eclose_n(M,A,n,Z) <-> Z = Union^n (A)"
   1.166 +apply (insert eclose_replacement1)
   1.167 +apply (simp add: is_eclose_n_def relativize1_def nat_into_M
   1.168 +                 iterates_abs [of "big_union(M)" _ "Union"])
   1.169 +done
   1.170 +
   1.171 +lemma (in M_eclose) mem_eclose_abs [simp]:
   1.172 +     "M(A) ==> mem_eclose(M,A,l) <-> l \<in> eclose(A)"
   1.173 +apply (insert eclose_replacement1)
   1.174 +apply (simp add: mem_eclose_def relativize1_def eclose_eq_Union
   1.175 +                 iterates_closed [of "big_union(M)"]) 
   1.176 +done
   1.177 +
   1.178 +lemma (in M_eclose) eclose_abs [simp]:
   1.179 +     "[|M(A); M(Z)|] ==> is_eclose(M,A,Z) <-> Z = eclose(A)"
   1.180 +apply (simp add: is_eclose_def, safe)
   1.181 +apply (rule M_equalityI, simp_all)
   1.182 +done
   1.183 +
   1.184 +
   1.185 +
   1.186 +
   1.187 +subsection {*Absoluteness for @{term transrec}*}
   1.188 +
   1.189 +
   1.190 +text{* @{term "transrec(a,H) \<equiv> wfrec(Memrel(eclose({a})), a, H)"} *}
   1.191 +constdefs
   1.192 +
   1.193 +  is_transrec :: "[i=>o, [i,i,i]=>o, i, i] => o"
   1.194 +   "is_transrec(M,MH,a,z) == 
   1.195 +      \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M]. 
   1.196 +       upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
   1.197 +       is_wfrec(M,MH,mesa,a,z)"
   1.198 +
   1.199 +  transrec_replacement :: "[i=>o, [i,i,i]=>o, i] => o"
   1.200 +   "transrec_replacement(M,MH,a) ==
   1.201 +      \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M]. 
   1.202 +       upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
   1.203 +       wfrec_replacement(M,MH,mesa)"
   1.204 +
   1.205 +(*????????????????Ordinal.thy*)
   1.206 +lemma Transset_trans_Memrel: 
   1.207 +    "\<forall>j\<in>i. Transset(j) ==> trans(Memrel(i))"
   1.208 +by (unfold Transset_def trans_def, blast)
   1.209 +
   1.210 +text{*The condition @{term "Ord(i)"} lets us use the simpler 
   1.211 +  @{text "trans_wfrec_abs"} rather than @{text "trans_wfrec_abs"},
   1.212 +  which I haven't even proved yet. *}
   1.213 +theorem (in M_eclose) transrec_abs:
   1.214 +  "[|Ord(i);  M(i);  M(z);
   1.215 +     transrec_replacement(M,MH,i);  relativize2(M,MH,H);
   1.216 +     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.217 +   ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)" 
   1.218 +by (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
   1.219 +       transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
   1.220 +
   1.221 +
   1.222 +theorem (in M_eclose) transrec_closed:
   1.223 +     "[|Ord(i);  M(i);  M(z);
   1.224 +	transrec_replacement(M,MH,i);  relativize2(M,MH,H);
   1.225 +	\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.226 +      ==> M(transrec(i,H))"
   1.227 +by (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
   1.228 +       transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
   1.229 +
   1.230 +
   1.231 +
   1.232 +
   1.233  end