src/ZF/Constructible/L_axioms.thy
 changeset 13306 6eebcddee32b parent 13304 43ef6c6dd906 child 13309 a6adee8ea75a
```     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Fri Jul 05 17:48:05 2002 +0200
1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Fri Jul 05 18:33:50 2002 +0200
1.3 @@ -1,4 +1,4 @@
1.4 -header {* The class L satisfies the axioms of ZF*}
1.5 +header {*The Class L Satisfies the ZF Axioms*}
1.6
1.7  theory L_axioms = Formula + Relative + Reflection:
1.8
1.9 @@ -166,7 +166,7 @@
1.10  declare successor_abs [simp]
1.11  declare succ_in_M_iff [iff]
1.12  declare separation_closed [intro,simp]
1.13 -declare strong_replacementI [rule_format]
1.14 +declare strong_replacementI
1.15  declare strong_replacement_closed [intro,simp]
1.16  declare RepFun_closed [intro,simp]
1.17  declare lam_closed [intro,simp]
1.18 @@ -290,6 +290,28 @@
1.19
1.20  subsection{*Internalized formulas for some relativized ones*}
1.21
1.22 +lemmas setclass_simps = rall_setclass_is_ball rex_setclass_is_bex
1.23 +
1.24 +subsubsection{*Some numbers to help write de Bruijn indices*}
1.25 +
1.26 +syntax
1.27 +    "3" :: i   ("3")
1.28 +    "4" :: i   ("4")
1.29 +    "5" :: i   ("5")
1.30 +    "6" :: i   ("6")
1.31 +    "7" :: i   ("7")
1.32 +    "8" :: i   ("8")
1.33 +    "9" :: i   ("9")
1.34 +
1.35 +translations
1.36 +   "3"  == "succ(2)"
1.37 +   "4"  == "succ(3)"
1.38 +   "5"  == "succ(4)"
1.39 +   "6"  == "succ(5)"
1.40 +   "7"  == "succ(6)"
1.41 +   "8"  == "succ(7)"
1.42 +   "9"  == "succ(8)"
1.43 +
1.44  subsubsection{*Unordered pairs*}
1.45
1.46  constdefs upair_fm :: "[i,i,i]=>i"
1.47 @@ -330,6 +352,12 @@
1.48  apply (blast intro: nth_type)
1.49  done
1.50
1.51 +text{*The @{text simplified} attribute tidies up the reflecting class.*}
1.52 +theorem upair_reflection [simplified,intro]:
1.53 +     "L_Reflects(?Cl, \<lambda>x. upair(L,f(x),g(x),h(x)),
1.54 +                    \<lambda>i x. upair(**Lset(i),f(x),g(x),h(x)))"
1.55 +by (simp add: upair_def, fast)
1.56 +
1.57  subsubsection{*Ordered pairs*}
1.58
1.59  constdefs pair_fm :: "[i,i,i]=>i"
1.60 @@ -359,327 +387,417 @@
1.61         ==> pair(**A, x, y, z) <-> sats(A, pair_fm(i,j,k), env)"
1.62  by (simp add: sats_pair_fm)
1.63
1.64 -
1.65 -
1.66 -subsection{*Proving instances of Separation using Reflection!*}
1.67 -
1.68 -text{*Helps us solve for de Bruijn indices!*}
1.69 -lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x"
1.70 -by simp
1.71 -
1.72 -
1.73 -lemma Collect_conj_in_DPow:
1.74 -     "[| {x\<in>A. P(x)} \<in> DPow(A);  {x\<in>A. Q(x)} \<in> DPow(A) |]
1.75 -      ==> {x\<in>A. P(x) & Q(x)} \<in> DPow(A)"
1.76 -by (simp add: Int_in_DPow Collect_Int_Collect_eq [symmetric])
1.77 -
1.78 -lemma Collect_conj_in_DPow_Lset:
1.79 -     "[|z \<in> Lset(j); {x \<in> Lset(j). P(x)} \<in> DPow(Lset(j))|]
1.80 -      ==> {x \<in> Lset(j). x \<in> z & P(x)} \<in> DPow(Lset(j))"
1.81 -apply (frule mem_Lset_imp_subset_Lset)
1.82 -apply (simp add: Collect_conj_in_DPow Collect_mem_eq
1.83 -                 subset_Int_iff2 elem_subset_in_DPow)
1.84 -done
1.85 -
1.86 -lemma separation_CollectI:
1.87 -     "(\<And>z. L(z) ==> L({x \<in> z . P(x)})) ==> separation(L, \<lambda>x. P(x))"
1.88 -apply (unfold separation_def, clarify)
1.89 -apply (rule_tac x="{x\<in>z. P(x)}" in rexI)
1.90 -apply simp_all
1.91 -done
1.92 -
1.93 -text{*Reduces the original comprehension to the reflected one*}
1.94 -lemma reflection_imp_L_separation:
1.95 -      "[| \<forall>x\<in>Lset(j). P(x) <-> Q(x);
1.96 -          {x \<in> Lset(j) . Q(x)} \<in> DPow(Lset(j));
1.97 -          Ord(j);  z \<in> Lset(j)|] ==> L({x \<in> z . P(x)})"
1.98 -apply (rule_tac i = "succ(j)" in L_I)
1.99 - prefer 2 apply simp
1.100 -apply (subgoal_tac "{x \<in> z. P(x)} = {x \<in> Lset(j). x \<in> z & (Q(x))}")
1.101 - prefer 2
1.102 - apply (blast dest: mem_Lset_imp_subset_Lset)
1.103 -apply (simp add: Lset_succ Collect_conj_in_DPow_Lset)
1.104 -done
1.105 -
1.106 -
1.107 -subsubsection{*Separation for Intersection*}
1.108 -
1.109 -lemma Inter_Reflects:
1.110 -     "L_Reflects(?Cl, \<lambda>x. \<forall>y[L]. y\<in>A --> x \<in> y,
1.111 -               \<lambda>i x. \<forall>y\<in>Lset(i). y\<in>A --> x \<in> y)"
1.112 -by fast
1.113 -
1.114 -lemma Inter_separation:
1.115 -     "L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)"
1.116 -apply (rule separation_CollectI)
1.117 -apply (rule_tac A="{A,z}" in subset_LsetE, blast )
1.118 -apply (rule ReflectsE [OF Inter_Reflects], assumption)
1.119 -apply (drule subset_Lset_ltD, assumption)
1.120 -apply (erule reflection_imp_L_separation)
1.121 -  apply (simp_all add: lt_Ord2, clarify)
1.122 -apply (rule DPowI2)
1.123 -apply (rule ball_iff_sats)
1.124 -apply (rule imp_iff_sats)
1.125 -apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats)
1.126 -apply (rule_tac i=0 and j=2 in mem_iff_sats)
1.127 -apply (simp_all add: succ_Un_distrib [symmetric])
1.128 -done
1.129 -
1.130 -subsubsection{*Separation for Cartesian Product*}
1.131 -
1.132 -text{*The @{text simplified} attribute tidies up the reflecting class.*}
1.133 -theorem upair_reflection [simplified,intro]:
1.134 -     "L_Reflects(?Cl, \<lambda>x. upair(L,f(x),g(x),h(x)),
1.135 -                    \<lambda>i x. upair(**Lset(i),f(x),g(x),h(x)))"
1.136 -by (simp add: upair_def, fast)
1.137 -
1.138  theorem pair_reflection [simplified,intro]:
1.139       "L_Reflects(?Cl, \<lambda>x. pair(L,f(x),g(x),h(x)),
1.140                      \<lambda>i x. pair(**Lset(i),f(x),g(x),h(x)))"
1.141 -by (simp only: pair_def rex_setclass_is_bex, fast)
1.142 +by (simp only: pair_def setclass_simps, fast)
1.143 +
1.144 +
1.145 +subsubsection{*Binary Unions*}
1.146
1.147 -lemma cartprod_Reflects [simplified]:
1.148 -     "L_Reflects(?Cl, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),
1.149 -                \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B &
1.150 -                               pair(**Lset(i),x,y,z)))"
1.151 -by fast
1.152 +constdefs union_fm :: "[i,i,i]=>i"
1.153 +    "union_fm(x,y,z) ==
1.154 +       Forall(Iff(Member(0,succ(z)),
1.155 +                  Or(Member(0,succ(x)),Member(0,succ(y)))))"
1.156 +
1.157 +lemma union_type [TC]:
1.158 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> union_fm(x,y,z) \<in> formula"
1.159 +by (simp add: union_fm_def)
1.160 +
1.161 +lemma arity_union_fm [simp]:
1.162 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.163 +      ==> arity(union_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.164 +by (simp add: union_fm_def succ_Un_distrib [symmetric] Un_ac)
1.165
1.166 -lemma cartprod_separation:
1.167 -     "[| L(A); L(B) |]
1.168 -      ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)))"
1.169 -apply (rule separation_CollectI)
1.170 -apply (rule_tac A="{A,B,z}" in subset_LsetE, blast )
1.171 -apply (rule ReflectsE [OF cartprod_Reflects], assumption)
1.172 -apply (drule subset_Lset_ltD, assumption)
1.173 -apply (erule reflection_imp_L_separation)
1.174 -  apply (simp_all add: lt_Ord2, clarify)
1.175 -apply (rule DPowI2)
1.176 -apply (rename_tac u)
1.177 -apply (rule bex_iff_sats)
1.178 -apply (rule conj_iff_sats)
1.179 -apply (rule_tac i=0 and j=2 and env="[x,u,A,B]" in mem_iff_sats, simp_all)
1.180 -apply (rule bex_iff_sats)
1.181 -apply (rule conj_iff_sats)
1.182 -apply (rule mem_iff_sats)
1.183 -apply (blast intro: nth_0 nth_ConsI)
1.184 -apply (blast intro: nth_0 nth_ConsI, simp_all)
1.185 -apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats)
1.186 -apply (simp_all add: succ_Un_distrib [symmetric])
1.187 -done
1.188 +lemma sats_union_fm [simp]:
1.189 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.190 +    ==> sats(A, union_fm(x,y,z), env) <->
1.191 +        union(**A, nth(x,env), nth(y,env), nth(z,env))"
1.192 +by (simp add: union_fm_def union_def)
1.193 +
1.194 +lemma union_iff_sats:
1.195 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.196 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.197 +       ==> union(**A, x, y, z) <-> sats(A, union_fm(i,j,k), env)"
1.198 +by (simp add: sats_union_fm)
1.199
1.200 -subsubsection{*Separation for Image*}
1.201 +theorem union_reflection [simplified,intro]:
1.202 +     "L_Reflects(?Cl, \<lambda>x. union(L,f(x),g(x),h(x)),
1.203 +                    \<lambda>i x. union(**Lset(i),f(x),g(x),h(x)))"
1.204 +by (simp add: union_def, fast)
1.205 +
1.206
1.207 -text{*No @{text simplified} here: it simplifies the occurrence of
1.208 -      the predicate @{term pair}!*}
1.209 -lemma image_Reflects:
1.210 -     "L_Reflects(?Cl, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)),
1.211 -           \<lambda>i y. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). x\<in>A & pair(**Lset(i),x,y,p)))"
1.212 -by fast
1.213 +subsubsection{*`Cons' for sets*}
1.214 +
1.215 +constdefs cons_fm :: "[i,i,i]=>i"
1.216 +    "cons_fm(x,y,z) ==
1.217 +       Exists(And(upair_fm(succ(x),succ(x),0),
1.218 +                  union_fm(0,succ(y),succ(z))))"
1.219
1.220
1.221 -lemma image_separation:
1.222 -     "[| L(A); L(r) |]
1.223 -      ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)))"
1.224 -apply (rule separation_CollectI)
1.225 -apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
1.226 -apply (rule ReflectsE [OF image_Reflects], assumption)
1.227 -apply (drule subset_Lset_ltD, assumption)
1.228 -apply (erule reflection_imp_L_separation)
1.229 -  apply (simp_all add: lt_Ord2, clarify)
1.230 -apply (rule DPowI2)
1.231 -apply (rule bex_iff_sats)
1.232 -apply (rule conj_iff_sats)
1.233 -apply (rule_tac env="[p,y,A,r]" in mem_iff_sats)
1.234 -apply (blast intro: nth_0 nth_ConsI)
1.235 -apply (blast intro: nth_0 nth_ConsI, simp_all)
1.236 -apply (rule bex_iff_sats)
1.237 -apply (rule conj_iff_sats)
1.238 -apply (rule mem_iff_sats)
1.239 -apply (blast intro: nth_0 nth_ConsI)
1.240 -apply (blast intro: nth_0 nth_ConsI, simp_all)
1.241 -apply (rule pair_iff_sats)
1.242 -apply (blast intro: nth_0 nth_ConsI)
1.243 -apply (blast intro: nth_0 nth_ConsI)
1.244 -apply (blast intro: nth_0 nth_ConsI)
1.245 -apply (simp_all add: succ_Un_distrib [symmetric])
1.246 -done
1.247 +lemma cons_type [TC]:
1.248 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> cons_fm(x,y,z) \<in> formula"
1.249 +by (simp add: cons_fm_def)
1.250 +
1.251 +lemma arity_cons_fm [simp]:
1.252 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.253 +      ==> arity(cons_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.254 +by (simp add: cons_fm_def succ_Un_distrib [symmetric] Un_ac)
1.255 +
1.256 +lemma sats_cons_fm [simp]:
1.257 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.258 +    ==> sats(A, cons_fm(x,y,z), env) <->
1.259 +        is_cons(**A, nth(x,env), nth(y,env), nth(z,env))"
1.260 +by (simp add: cons_fm_def is_cons_def)
1.261 +
1.262 +lemma cons_iff_sats:
1.263 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.264 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.265 +       ==> is_cons(**A, x, y, z) <-> sats(A, cons_fm(i,j,k), env)"
1.266 +by simp
1.267 +
1.268 +theorem cons_reflection [simplified,intro]:
1.269 +     "L_Reflects(?Cl, \<lambda>x. is_cons(L,f(x),g(x),h(x)),
1.270 +                    \<lambda>i x. is_cons(**Lset(i),f(x),g(x),h(x)))"
1.271 +by (simp only: is_cons_def setclass_simps, fast)
1.272
1.273
1.274 -subsubsection{*Separation for Converse*}
1.275 +subsubsection{*Function Applications*}
1.276 +
1.277 +constdefs fun_apply_fm :: "[i,i,i]=>i"
1.278 +    "fun_apply_fm(f,x,y) ==
1.279 +       Forall(Iff(Exists(And(Member(0,succ(succ(f))),
1.280 +                             pair_fm(succ(succ(x)), 1, 0))),
1.281 +                  Equal(succ(y),0)))"
1.282
1.283 -lemma converse_Reflects:
1.284 -     "L_Reflects(?Cl,
1.285 -        \<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)),
1.286 -     \<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i).
1.287 -                     pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z)))"
1.288 -by fast
1.289 +lemma fun_apply_type [TC]:
1.290 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> fun_apply_fm(x,y,z) \<in> formula"
1.291 +by (simp add: fun_apply_fm_def)
1.292 +
1.293 +lemma arity_fun_apply_fm [simp]:
1.294 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.295 +      ==> arity(fun_apply_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.296 +by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac)
1.297
1.298 -lemma converse_separation:
1.299 -     "L(r) ==> separation(L,
1.300 -         \<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)))"
1.301 -apply (rule separation_CollectI)
1.302 -apply (rule_tac A="{r,z}" in subset_LsetE, blast )
1.303 -apply (rule ReflectsE [OF converse_Reflects], assumption)
1.304 -apply (drule subset_Lset_ltD, assumption)
1.305 -apply (erule reflection_imp_L_separation)
1.306 -  apply (simp_all add: lt_Ord2, clarify)
1.307 -apply (rule DPowI2)
1.308 -apply (rename_tac u)
1.309 -apply (rule bex_iff_sats)
1.310 -apply (rule conj_iff_sats)
1.311 -apply (rule_tac i=0 and j="2" and env="[p,u,r]" in mem_iff_sats, simp_all)
1.312 -apply (rule bex_iff_sats)
1.313 -apply (rule bex_iff_sats)
1.314 -apply (rule conj_iff_sats)
1.315 -apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats, simp_all)
1.316 -apply (rule pair_iff_sats)
1.317 -apply (blast intro: nth_0 nth_ConsI)
1.318 -apply (blast intro: nth_0 nth_ConsI)
1.319 -apply (blast intro: nth_0 nth_ConsI)
1.320 -apply (simp_all add: succ_Un_distrib [symmetric])
1.321 -done
1.322 +lemma sats_fun_apply_fm [simp]:
1.323 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.324 +    ==> sats(A, fun_apply_fm(x,y,z), env) <->
1.325 +        fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))"
1.326 +by (simp add: fun_apply_fm_def fun_apply_def)
1.327 +
1.328 +lemma fun_apply_iff_sats:
1.329 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.330 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.331 +       ==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)"
1.332 +by simp
1.333 +
1.334 +theorem fun_apply_reflection [simplified,intro]:
1.335 +     "L_Reflects(?Cl, \<lambda>x. fun_apply(L,f(x),g(x),h(x)),
1.336 +                    \<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x)))"
1.337 +by (simp only: fun_apply_def setclass_simps, fast)
1.338
1.339
1.340 -subsubsection{*Separation for Restriction*}
1.341 +subsubsection{*Variants of Satisfaction Definitions for Ordinals, etc.*}
1.342 +
1.343 +text{*Differs from the one in Formula by using "ordinal" rather than "Ord"*}
1.344 +
1.345 +
1.346 +lemma sats_subset_fm':
1.347 +   "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.348 +    ==> sats(A, subset_fm(x,y), env) <-> subset(**A, nth(x,env), nth(y,env))"
1.349 +by (simp add: subset_fm_def subset_def)
1.350
1.351 -lemma restrict_Reflects:
1.352 -     "L_Reflects(?Cl, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)),
1.353 -        \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(**Lset(i),x,y,z)))"
1.354 -by fast
1.355 +theorem subset_reflection [simplified,intro]:
1.356 +     "L_Reflects(?Cl, \<lambda>x. subset(L,f(x),g(x)),
1.357 +                    \<lambda>i x. subset(**Lset(i),f(x),g(x)))"
1.358 +by (simp add: subset_def, fast)
1.359 +
1.360 +lemma sats_transset_fm':
1.361 +   "[|x \<in> nat; env \<in> list(A)|]
1.362 +    ==> sats(A, transset_fm(x), env) <-> transitive_set(**A, nth(x,env))"
1.363 +by (simp add: sats_subset_fm' transset_fm_def transitive_set_def)
1.364
1.365 -lemma restrict_separation:
1.366 -   "L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))"
1.367 -apply (rule separation_CollectI)
1.368 -apply (rule_tac A="{A,z}" in subset_LsetE, blast )
1.369 -apply (rule ReflectsE [OF restrict_Reflects], assumption)
1.370 -apply (drule subset_Lset_ltD, assumption)
1.371 -apply (erule reflection_imp_L_separation)
1.372 -  apply (simp_all add: lt_Ord2, clarify)
1.373 -apply (rule DPowI2)
1.374 -apply (rename_tac u)
1.375 -apply (rule bex_iff_sats)
1.376 -apply (rule conj_iff_sats)
1.377 -apply (rule_tac i=0 and j="2" and env="[x,u,A]" in mem_iff_sats, simp_all)
1.378 -apply (rule bex_iff_sats)
1.379 -apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats)
1.380 -apply (simp_all add: succ_Un_distrib [symmetric])
1.381 -done
1.382 +theorem transitive_set_reflection [simplified,intro]:
1.383 +     "L_Reflects(?Cl, \<lambda>x. transitive_set(L,f(x)),
1.384 +                    \<lambda>i x. transitive_set(**Lset(i),f(x)))"
1.385 +by (simp only: transitive_set_def setclass_simps, fast)
1.386 +
1.387 +lemma sats_ordinal_fm':
1.388 +   "[|x \<in> nat; env \<in> list(A)|]
1.389 +    ==> sats(A, ordinal_fm(x), env) <-> ordinal(**A,nth(x,env))"
1.390 +by (simp add: sats_transset_fm' ordinal_fm_def ordinal_def)
1.391 +
1.392 +lemma ordinal_iff_sats:
1.393 +      "[| nth(i,env) = x;  i \<in> nat; env \<in> list(A)|]
1.394 +       ==> ordinal(**A, x) <-> sats(A, ordinal_fm(i), env)"
1.395 +by (simp add: sats_ordinal_fm')
1.396 +
1.397 +theorem ordinal_reflection [simplified,intro]:
1.398 +     "L_Reflects(?Cl, \<lambda>x. ordinal(L,f(x)),
1.399 +                    \<lambda>i x. ordinal(**Lset(i),f(x)))"
1.400 +by (simp only: ordinal_def setclass_simps, fast)
1.401
1.402
1.403 -subsubsection{*Separation for Composition*}
1.404 +subsubsection{*Membership Relation*}
1.405
1.406 -lemma comp_Reflects:
1.407 -     "L_Reflects(?Cl, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
1.408 -		  pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
1.409 -                  xy\<in>s & yz\<in>r,
1.410 -        \<lambda>i xz. \<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). \<exists>z\<in>Lset(i). \<exists>xy\<in>Lset(i). \<exists>yz\<in>Lset(i).
1.411 -		  pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) &
1.412 -                  pair(**Lset(i),y,z,yz) & xy\<in>s & yz\<in>r)"
1.413 -by fast
1.414 +constdefs Memrel_fm :: "[i,i]=>i"
1.415 +    "Memrel_fm(A,r) ==
1.416 +       Forall(Iff(Member(0,succ(r)),
1.417 +                  Exists(And(Member(0,succ(succ(A))),
1.418 +                             Exists(And(Member(0,succ(succ(succ(A)))),
1.419 +                                        And(Member(1,0),
1.420 +                                            pair_fm(1,0,2))))))))"
1.421 +
1.422 +lemma Memrel_type [TC]:
1.423 +     "[| x \<in> nat; y \<in> nat |] ==> Memrel_fm(x,y) \<in> formula"
1.424 +by (simp add: Memrel_fm_def)
1.425
1.426 -lemma comp_separation:
1.427 -     "[| L(r); L(s) |]
1.428 -      ==> separation(L, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
1.429 -		  pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
1.430 -                  xy\<in>s & yz\<in>r)"
1.431 -apply (rule separation_CollectI)
1.432 -apply (rule_tac A="{r,s,z}" in subset_LsetE, blast )
1.433 -apply (rule ReflectsE [OF comp_Reflects], assumption)
1.434 -apply (drule subset_Lset_ltD, assumption)
1.435 -apply (erule reflection_imp_L_separation)
1.436 -  apply (simp_all add: lt_Ord2, clarify)
1.437 -apply (rule DPowI2)
1.438 -apply (rename_tac u)
1.439 -apply (rule bex_iff_sats)+
1.440 -apply (rename_tac x y z)
1.441 -apply (rule conj_iff_sats)
1.442 -apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats)
1.443 -apply (blast intro: nth_0 nth_ConsI)
1.444 -apply (blast intro: nth_0 nth_ConsI)
1.445 -apply (blast intro: nth_0 nth_ConsI, simp_all)
1.446 -apply (rule bex_iff_sats)
1.447 -apply (rule conj_iff_sats)
1.448 -apply (rule pair_iff_sats)
1.449 -apply (blast intro: nth_0 nth_ConsI)
1.450 -apply (blast intro: nth_0 nth_ConsI)
1.451 -apply (blast intro: nth_0 nth_ConsI, simp_all)
1.452 -apply (rule bex_iff_sats)
1.453 -apply (rule conj_iff_sats)
1.454 -apply (rule pair_iff_sats)
1.455 -apply (blast intro: nth_0 nth_ConsI)
1.456 -apply (blast intro: nth_0 nth_ConsI)
1.457 -apply (blast intro: nth_0 nth_ConsI, simp_all)
1.458 -apply (rule conj_iff_sats)
1.459 -apply (rule mem_iff_sats)
1.460 -apply (blast intro: nth_0 nth_ConsI)
1.461 -apply (blast intro: nth_0 nth_ConsI, simp)
1.462 -apply (rule mem_iff_sats)
1.463 -apply (blast intro: nth_0 nth_ConsI)
1.464 -apply (blast intro: nth_0 nth_ConsI)
1.465 -apply (simp_all add: succ_Un_distrib [symmetric])
1.466 -done
1.467 +lemma arity_Memrel_fm [simp]:
1.468 +     "[| x \<in> nat; y \<in> nat |]
1.469 +      ==> arity(Memrel_fm(x,y)) = succ(x) \<union> succ(y)"
1.470 +by (simp add: Memrel_fm_def succ_Un_distrib [symmetric] Un_ac)
1.471 +
1.472 +lemma sats_Memrel_fm [simp]:
1.473 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.474 +    ==> sats(A, Memrel_fm(x,y), env) <->
1.475 +        membership(**A, nth(x,env), nth(y,env))"
1.476 +by (simp add: Memrel_fm_def membership_def)
1.477
1.478 -subsubsection{*Separation for Predecessors in an Order*}
1.479 -
1.480 -lemma pred_Reflects:
1.481 -     "L_Reflects(?Cl, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),
1.482 -                    \<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(**Lset(i),y,x,p))"
1.483 -by fast
1.484 +lemma Memrel_iff_sats:
1.485 +      "[| nth(i,env) = x; nth(j,env) = y;
1.486 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
1.487 +       ==> membership(**A, x, y) <-> sats(A, Memrel_fm(i,j), env)"
1.488 +by simp
1.489
1.490 -lemma pred_separation:
1.491 -     "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
1.492 -apply (rule separation_CollectI)
1.493 -apply (rule_tac A="{r,x,z}" in subset_LsetE, blast )
1.494 -apply (rule ReflectsE [OF pred_Reflects], assumption)
1.495 -apply (drule subset_Lset_ltD, assumption)
1.496 -apply (erule reflection_imp_L_separation)
1.497 -  apply (simp_all add: lt_Ord2, clarify)
1.498 -apply (rule DPowI2)
1.499 -apply (rename_tac u)
1.500 -apply (rule bex_iff_sats)
1.501 -apply (rule conj_iff_sats)
1.502 -apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats)
1.503 -apply (blast intro: nth_0 nth_ConsI)
1.504 -apply (blast intro: nth_0 nth_ConsI, simp)
1.505 -apply (rule pair_iff_sats)
1.506 -apply (blast intro: nth_0 nth_ConsI)
1.507 -apply (blast intro: nth_0 nth_ConsI)
1.508 -apply (blast intro: nth_0 nth_ConsI, simp_all)
1.509 -apply (simp_all add: succ_Un_distrib [symmetric])
1.510 -done
1.511 +theorem membership_reflection [simplified,intro]:
1.512 +     "L_Reflects(?Cl, \<lambda>x. membership(L,f(x),g(x)),
1.513 +                    \<lambda>i x. membership(**Lset(i),f(x),g(x)))"
1.514 +by (simp only: membership_def setclass_simps, fast)
1.515
1.516
1.517 -subsubsection{*Separation for the Membership Relation*}
1.518 +subsubsection{*Predecessor Set*}
1.519
1.520 -lemma Memrel_Reflects:
1.521 -     "L_Reflects(?Cl, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y,
1.522 -            \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(**Lset(i),x,y,z) & x \<in> y)"
1.523 -by fast
1.524 +constdefs pred_set_fm :: "[i,i,i,i]=>i"
1.525 +    "pred_set_fm(A,x,r,B) ==
1.526 +       Forall(Iff(Member(0,succ(B)),
1.527 +                  Exists(And(Member(0,succ(succ(r))),
1.528 +                             And(Member(1,succ(succ(A))),
1.529 +                                 pair_fm(1,succ(succ(x)),0))))))"
1.530 +
1.531 +
1.532 +lemma pred_set_type [TC]:
1.533 +     "[| A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat |]
1.534 +      ==> pred_set_fm(A,x,r,B) \<in> formula"
1.535 +by (simp add: pred_set_fm_def)
1.536
1.537 -lemma Memrel_separation:
1.538 -     "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
1.539 -apply (rule separation_CollectI)
1.540 -apply (rule_tac A="{z}" in subset_LsetE, blast )
1.541 -apply (rule ReflectsE [OF Memrel_Reflects], assumption)
1.542 -apply (drule subset_Lset_ltD, assumption)
1.543 -apply (erule reflection_imp_L_separation)
1.544 -  apply (simp_all add: lt_Ord2)
1.545 -apply (rule DPowI2)
1.546 -apply (rename_tac u)
1.547 -apply (rule bex_iff_sats)+
1.548 -apply (rule conj_iff_sats)
1.549 -apply (rule_tac env = "[y,x,u]" in pair_iff_sats)
1.550 -apply (blast intro: nth_0 nth_ConsI)
1.551 -apply (blast intro: nth_0 nth_ConsI)
1.552 -apply (blast intro: nth_0 nth_ConsI, simp_all)
1.553 -apply (rule mem_iff_sats)
1.554 -apply (blast intro: nth_0 nth_ConsI)
1.555 -apply (blast intro: nth_0 nth_ConsI)
1.556 -apply (simp_all add: succ_Un_distrib [symmetric])
1.557 -done
1.558 +lemma arity_pred_set_fm [simp]:
1.559 +   "[| A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat |]
1.560 +    ==> arity(pred_set_fm(A,x,r,B)) = succ(A) \<union> succ(x) \<union> succ(r) \<union> succ(B)"
1.561 +by (simp add: pred_set_fm_def succ_Un_distrib [symmetric] Un_ac)
1.562 +
1.563 +lemma sats_pred_set_fm [simp]:
1.564 +   "[| U \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat; env \<in> list(A)|]
1.565 +    ==> sats(A, pred_set_fm(U,x,r,B), env) <->
1.566 +        pred_set(**A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))"
1.567 +by (simp add: pred_set_fm_def pred_set_def)
1.568 +
1.569 +lemma pred_set_iff_sats:
1.570 +      "[| nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B;
1.571 +          i \<in> nat; j \<in> nat; k \<in> nat; l \<in> nat; env \<in> list(A)|]
1.572 +       ==> pred_set(**A,U,x,r,B) <-> sats(A, pred_set_fm(i,j,k,l), env)"
1.573 +by (simp add: sats_pred_set_fm)
1.574 +
1.575 +theorem pred_set_reflection [simplified,intro]:
1.576 +     "L_Reflects(?Cl, \<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)),
1.577 +                    \<lambda>i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x)))"
1.578 +by (simp only: pred_set_def setclass_simps, fast)
1.579
1.580
1.581
1.582 +subsubsection{*Domain*}
1.583 +
1.584 +(* "is_domain(M,r,z) ==
1.585 +	\<forall>x[M]. (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))" *)
1.586 +constdefs domain_fm :: "[i,i]=>i"
1.587 +    "domain_fm(r,z) ==
1.588 +       Forall(Iff(Member(0,succ(z)),
1.589 +                  Exists(And(Member(0,succ(succ(r))),
1.590 +                             Exists(pair_fm(2,0,1))))))"
1.591 +
1.592 +lemma domain_type [TC]:
1.593 +     "[| x \<in> nat; y \<in> nat |] ==> domain_fm(x,y) \<in> formula"
1.594 +by (simp add: domain_fm_def)
1.595 +
1.596 +lemma arity_domain_fm [simp]:
1.597 +     "[| x \<in> nat; y \<in> nat |]
1.598 +      ==> arity(domain_fm(x,y)) = succ(x) \<union> succ(y)"
1.599 +by (simp add: domain_fm_def succ_Un_distrib [symmetric] Un_ac)
1.600 +
1.601 +lemma sats_domain_fm [simp]:
1.602 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.603 +    ==> sats(A, domain_fm(x,y), env) <->
1.604 +        is_domain(**A, nth(x,env), nth(y,env))"
1.605 +by (simp add: domain_fm_def is_domain_def)
1.606 +
1.607 +lemma domain_iff_sats:
1.608 +      "[| nth(i,env) = x; nth(j,env) = y;
1.609 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
1.610 +       ==> is_domain(**A, x, y) <-> sats(A, domain_fm(i,j), env)"
1.611 +by simp
1.612 +
1.613 +theorem domain_reflection [simplified,intro]:
1.614 +     "L_Reflects(?Cl, \<lambda>x. is_domain(L,f(x),g(x)),
1.615 +                    \<lambda>i x. is_domain(**Lset(i),f(x),g(x)))"
1.616 +by (simp only: is_domain_def setclass_simps, fast)
1.617 +
1.618 +
1.619 +subsubsection{*Range*}
1.620 +
1.621 +(* "is_range(M,r,z) ==
1.622 +	\<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))" *)
1.623 +constdefs range_fm :: "[i,i]=>i"
1.624 +    "range_fm(r,z) ==
1.625 +       Forall(Iff(Member(0,succ(z)),
1.626 +                  Exists(And(Member(0,succ(succ(r))),
1.627 +                             Exists(pair_fm(0,2,1))))))"
1.628 +
1.629 +lemma range_type [TC]:
1.630 +     "[| x \<in> nat; y \<in> nat |] ==> range_fm(x,y) \<in> formula"
1.631 +by (simp add: range_fm_def)
1.632 +
1.633 +lemma arity_range_fm [simp]:
1.634 +     "[| x \<in> nat; y \<in> nat |]
1.635 +      ==> arity(range_fm(x,y)) = succ(x) \<union> succ(y)"
1.636 +by (simp add: range_fm_def succ_Un_distrib [symmetric] Un_ac)
1.637 +
1.638 +lemma sats_range_fm [simp]:
1.639 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.640 +    ==> sats(A, range_fm(x,y), env) <->
1.641 +        is_range(**A, nth(x,env), nth(y,env))"
1.642 +by (simp add: range_fm_def is_range_def)
1.643 +
1.644 +lemma range_iff_sats:
1.645 +      "[| nth(i,env) = x; nth(j,env) = y;
1.646 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
1.647 +       ==> is_range(**A, x, y) <-> sats(A, range_fm(i,j), env)"
1.648 +by simp
1.649 +
1.650 +theorem range_reflection [simplified,intro]:
1.651 +     "L_Reflects(?Cl, \<lambda>x. is_range(L,f(x),g(x)),
1.652 +                    \<lambda>i x. is_range(**Lset(i),f(x),g(x)))"
1.653 +by (simp only: is_range_def setclass_simps, fast)
1.654 +
1.655 +
1.656 +
1.657 +
1.658 +
1.659 +subsubsection{*Image*}
1.660 +
1.661 +(* "image(M,r,A,z) ==
1.662 +        \<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))" *)
1.663 +constdefs image_fm :: "[i,i,i]=>i"
1.664 +    "image_fm(r,A,z) ==
1.665 +       Forall(Iff(Member(0,succ(z)),
1.666 +                  Exists(And(Member(0,succ(succ(r))),
1.667 +                             Exists(And(Member(0,succ(succ(succ(A)))),
1.668 +	 			        pair_fm(0,2,1)))))))"
1.669 +
1.670 +lemma image_type [TC]:
1.671 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> image_fm(x,y,z) \<in> formula"
1.672 +by (simp add: image_fm_def)
1.673 +
1.674 +lemma arity_image_fm [simp]:
1.675 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.676 +      ==> arity(image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.677 +by (simp add: image_fm_def succ_Un_distrib [symmetric] Un_ac)
1.678 +
1.679 +lemma sats_image_fm [simp]:
1.680 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.681 +    ==> sats(A, image_fm(x,y,z), env) <->
1.682 +        image(**A, nth(x,env), nth(y,env), nth(z,env))"
1.683 +by (simp add: image_fm_def image_def)
1.684 +
1.685 +lemma image_iff_sats:
1.686 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.687 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.688 +       ==> image(**A, x, y, z) <-> sats(A, image_fm(i,j,k), env)"
1.689 +by (simp add: sats_image_fm)
1.690 +
1.691 +theorem image_reflection [simplified,intro]:
1.692 +     "L_Reflects(?Cl, \<lambda>x. image(L,f(x),g(x),h(x)),
1.693 +                    \<lambda>i x. image(**Lset(i),f(x),g(x),h(x)))"
1.694 +by (simp only: image_def setclass_simps, fast)
1.695 +
1.696 +
1.697 +subsubsection{*The Concept of Relation*}
1.698 +
1.699 +(* "is_relation(M,r) ==
1.700 +        (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))" *)
1.701 +constdefs relation_fm :: "i=>i"
1.702 +    "relation_fm(r) ==
1.703 +       Forall(Implies(Member(0,succ(r)), Exists(Exists(pair_fm(1,0,2)))))"
1.704 +
1.705 +lemma relation_type [TC]:
1.706 +     "[| x \<in> nat |] ==> relation_fm(x) \<in> formula"
1.707 +by (simp add: relation_fm_def)
1.708 +
1.709 +lemma arity_relation_fm [simp]:
1.710 +     "x \<in> nat ==> arity(relation_fm(x)) = succ(x)"
1.711 +by (simp add: relation_fm_def succ_Un_distrib [symmetric] Un_ac)
1.712 +
1.713 +lemma sats_relation_fm [simp]:
1.714 +   "[| x \<in> nat; env \<in> list(A)|]
1.715 +    ==> sats(A, relation_fm(x), env) <-> is_relation(**A, nth(x,env))"
1.716 +by (simp add: relation_fm_def is_relation_def)
1.717 +
1.718 +lemma relation_iff_sats:
1.719 +      "[| nth(i,env) = x; nth(j,env) = y;
1.720 +          i \<in> nat; env \<in> list(A)|]
1.721 +       ==> is_relation(**A, x) <-> sats(A, relation_fm(i), env)"
1.722 +by simp
1.723 +
1.724 +theorem is_relation_reflection [simplified,intro]:
1.725 +     "L_Reflects(?Cl, \<lambda>x. is_relation(L,f(x)),
1.726 +                    \<lambda>i x. is_relation(**Lset(i),f(x)))"
1.727 +by (simp only: is_relation_def setclass_simps, fast)
1.728 +
1.729 +
1.730 +subsubsection{*The Concept of Function*}
1.731 +
1.732 +(* "is_function(M,r) ==
1.733 +	\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].
1.734 +           pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'" *)
1.735 +constdefs function_fm :: "i=>i"
1.736 +    "function_fm(r) ==
1.737 +       Forall(Forall(Forall(Forall(Forall(
1.738 +         Implies(pair_fm(4,3,1),
1.739 +                 Implies(pair_fm(4,2,0),
1.740 +                         Implies(Member(1,r#+5),
1.741 +                                 Implies(Member(0,r#+5), Equal(3,2))))))))))"
1.742 +
1.743 +lemma function_type [TC]:
1.744 +     "[| x \<in> nat |] ==> function_fm(x) \<in> formula"
1.745 +by (simp add: function_fm_def)
1.746 +
1.747 +lemma arity_function_fm [simp]:
1.748 +     "x \<in> nat ==> arity(function_fm(x)) = succ(x)"
1.749 +by (simp add: function_fm_def succ_Un_distrib [symmetric] Un_ac)
1.750 +
1.751 +lemma sats_function_fm [simp]:
1.752 +   "[| x \<in> nat; env \<in> list(A)|]
1.753 +    ==> sats(A, function_fm(x), env) <-> is_function(**A, nth(x,env))"
1.754 +by (simp add: function_fm_def is_function_def)
1.755 +
1.756 +lemma function_iff_sats:
1.757 +      "[| nth(i,env) = x; nth(j,env) = y;
1.758 +          i \<in> nat; env \<in> list(A)|]
1.759 +       ==> is_function(**A, x) <-> sats(A, function_fm(i), env)"
1.760 +by simp
1.761 +
1.762 +theorem is_function_reflection [simplified,intro]:
1.763 +     "L_Reflects(?Cl, \<lambda>x. is_function(L,f(x)),
1.764 +                    \<lambda>i x. is_function(**Lset(i),f(x)))"
1.765 +by (simp only: is_function_def setclass_simps, fast)
1.766
1.767
1.768  end
```