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