src/ZF/Constructible/Relative.thy
author paulson
Thu Jul 11 13:43:24 2002 +0200 (2002-07-11)
changeset 13348 374d05460db4
parent 13339 0f89104dd377
child 13350 626b79677dfa
permissions -rw-r--r--
Separation/Replacement up to M_wfrank!
     1 header {*Relativization and Absoluteness*}
     2 
     3 theory Relative = Main:
     4 
     5 subsection{* Relativized versions of standard set-theoretic concepts *}
     6 
     7 constdefs
     8   empty :: "[i=>o,i] => o"
     9     "empty(M,z) == \<forall>x[M]. x \<notin> z"
    10 
    11   subset :: "[i=>o,i,i] => o"
    12     "subset(M,A,B) == \<forall>x[M]. x\<in>A --> x \<in> B"
    13 
    14   upair :: "[i=>o,i,i,i] => o"
    15     "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x[M]. x\<in>z --> x = a | x = b)"
    16 
    17   pair :: "[i=>o,i,i,i] => o"
    18     "pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & 
    19                           (\<exists>y[M]. upair(M,a,b,y) & upair(M,x,y,z))"
    20 
    21 
    22   union :: "[i=>o,i,i,i] => o"
    23     "union(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a | x \<in> b"
    24 
    25   is_cons :: "[i=>o,i,i,i] => o"
    26     "is_cons(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & union(M,x,b,z)"
    27 
    28   successor :: "[i=>o,i,i] => o"
    29     "successor(M,a,z) == is_cons(M,a,a,z)"
    30 
    31   powerset :: "[i=>o,i,i] => o"
    32     "powerset(M,A,z) == \<forall>x[M]. x \<in> z <-> subset(M,x,A)"
    33 
    34   inter :: "[i=>o,i,i,i] => o"
    35     "inter(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<in> b"
    36 
    37   setdiff :: "[i=>o,i,i,i] => o"
    38     "setdiff(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<notin> b"
    39 
    40   big_union :: "[i=>o,i,i] => o"
    41     "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)"
    42 
    43   big_inter :: "[i=>o,i,i] => o"
    44     "big_inter(M,A,z) == 
    45              (A=0 --> z=0) &
    46 	     (A\<noteq>0 --> (\<forall>x[M]. x \<in> z <-> (\<forall>y[M]. y\<in>A --> x \<in> y)))"
    47 
    48   cartprod :: "[i=>o,i,i,i] => o"
    49     "cartprod(M,A,B,z) == 
    50 	\<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))"
    51 
    52   is_converse :: "[i=>o,i,i] => o"
    53     "is_converse(M,r,z) == 
    54 	\<forall>x[M]. x \<in> z <-> 
    55              (\<exists>w[M]. w\<in>r & (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x)))"
    56 
    57   pre_image :: "[i=>o,i,i,i] => o"
    58     "pre_image(M,r,A,z) == 
    59 	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))"
    60 
    61   is_domain :: "[i=>o,i,i] => o"
    62     "is_domain(M,r,z) == 
    63 	\<forall>x[M]. (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))"
    64 
    65   image :: "[i=>o,i,i,i] => o"
    66     "image(M,r,A,z) == 
    67         \<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))"
    68 
    69   is_range :: "[i=>o,i,i] => o"
    70     --{*the cleaner 
    71       @{term "\<exists>r'[M]. is_converse(M,r,r') & is_domain(M,r',z)"}
    72       unfortunately needs an instance of separation in order to prove 
    73         @{term "M(converse(r))"}.*}
    74     "is_range(M,r,z) == 
    75 	\<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))"
    76 
    77   is_field :: "[i=>o,i,i] => o"
    78     "is_field(M,r,z) == 
    79 	\<exists>dr[M]. is_domain(M,r,dr) & 
    80             (\<exists>rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))"
    81 
    82   is_relation :: "[i=>o,i] => o"
    83     "is_relation(M,r) == 
    84         (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))"
    85 
    86   is_function :: "[i=>o,i] => o"
    87     "is_function(M,r) == 
    88 	\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M]. 
    89            pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'"
    90 
    91   fun_apply :: "[i=>o,i,i,i] => o"
    92     "fun_apply(M,f,x,y) == 
    93 	(\<forall>y'[M]. (\<exists>u[M]. u\<in>f & pair(M,x,y',u)) <-> y=y')"
    94 
    95   typed_function :: "[i=>o,i,i,i] => o"
    96     "typed_function(M,A,B,r) == 
    97         is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
    98         (\<forall>u[M]. u\<in>r --> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) --> y\<in>B))"
    99 
   100   is_funspace :: "[i=>o,i,i,i] => o"
   101     "is_funspace(M,A,B,F) == 
   102         \<forall>f[M]. f \<in> F <-> typed_function(M,A,B,f)"
   103 
   104   composition :: "[i=>o,i,i,i] => o"
   105     "composition(M,r,s,t) == 
   106         \<forall>p[M]. p \<in> t <-> 
   107                (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
   108                 pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
   109                 xy \<in> s & yz \<in> r)"
   110 
   111   injection :: "[i=>o,i,i,i] => o"
   112     "injection(M,A,B,f) == 
   113 	typed_function(M,A,B,f) &
   114         (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M]. 
   115           pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> x=x')"
   116 
   117   surjection :: "[i=>o,i,i,i] => o"
   118     "surjection(M,A,B,f) == 
   119         typed_function(M,A,B,f) &
   120         (\<forall>y[M]. y\<in>B --> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))"
   121 
   122   bijection :: "[i=>o,i,i,i] => o"
   123     "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)"
   124 
   125   restriction :: "[i=>o,i,i,i] => o"
   126     "restriction(M,r,A,z) == 
   127 	\<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))"
   128 
   129   transitive_set :: "[i=>o,i] => o"
   130     "transitive_set(M,a) == \<forall>x[M]. x\<in>a --> subset(M,x,a)"
   131 
   132   ordinal :: "[i=>o,i] => o"
   133      --{*an ordinal is a transitive set of transitive sets*}
   134     "ordinal(M,a) == transitive_set(M,a) & (\<forall>x[M]. x\<in>a --> transitive_set(M,x))"
   135 
   136   limit_ordinal :: "[i=>o,i] => o"
   137     --{*a limit ordinal is a non-empty, successor-closed ordinal*}
   138     "limit_ordinal(M,a) == 
   139 	ordinal(M,a) & ~ empty(M,a) & 
   140         (\<forall>x[M]. x\<in>a --> (\<exists>y[M]. y\<in>a & successor(M,x,y)))"
   141 
   142   successor_ordinal :: "[i=>o,i] => o"
   143     --{*a successor ordinal is any ordinal that is neither empty nor limit*}
   144     "successor_ordinal(M,a) == 
   145 	ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)"
   146 
   147   finite_ordinal :: "[i=>o,i] => o"
   148     --{*an ordinal is finite if neither it nor any of its elements are limit*}
   149     "finite_ordinal(M,a) == 
   150 	ordinal(M,a) & ~ limit_ordinal(M,a) & 
   151         (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
   152 
   153   omega :: "[i=>o,i] => o"
   154     --{*omega is a limit ordinal none of whose elements are limit*}
   155     "omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
   156 
   157   number1 :: "[i=>o,i] => o"
   158     "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))"
   159 
   160   number2 :: "[i=>o,i] => o"
   161     "number2(M,a) == (\<exists>x[M]. number1(M,x) & successor(M,x,a))"
   162 
   163   number3 :: "[i=>o,i] => o"
   164     "number3(M,a) == (\<exists>x[M]. number2(M,x) & successor(M,x,a))"
   165 
   166 
   167 subsection {*The relativized ZF axioms*}
   168 constdefs
   169 
   170   extensionality :: "(i=>o) => o"
   171     "extensionality(M) == 
   172 	\<forall>x[M]. \<forall>y[M]. (\<forall>z[M]. z \<in> x <-> z \<in> y) --> x=y"
   173 
   174   separation :: "[i=>o, i=>o] => o"
   175     --{*Big problem: the formula @{text P} should only involve parameters
   176         belonging to @{text M}.  Don't see how to enforce that.*}
   177     "separation(M,P) == 
   178 	\<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
   179 
   180   upair_ax :: "(i=>o) => o"
   181     "upair_ax(M) == \<forall>x y. M(x) --> M(y) --> (\<exists>z[M]. upair(M,x,y,z))"
   182 
   183   Union_ax :: "(i=>o) => o"
   184     "Union_ax(M) == \<forall>x[M]. (\<exists>z[M]. big_union(M,x,z))"
   185 
   186   power_ax :: "(i=>o) => o"
   187     "power_ax(M) == \<forall>x[M]. (\<exists>z[M]. powerset(M,x,z))"
   188 
   189   univalent :: "[i=>o, i, [i,i]=>o] => o"
   190     "univalent(M,A,P) == 
   191 	(\<forall>x[M]. x\<in>A --> (\<forall>y z. M(y) --> M(z) --> P(x,y) & P(x,z) --> y=z))"
   192 
   193   replacement :: "[i=>o, [i,i]=>o] => o"
   194     "replacement(M,P) == 
   195       \<forall>A[M]. univalent(M,A,P) -->
   196       (\<exists>Y[M]. (\<forall>b[M]. ((\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y)))"
   197 
   198   strong_replacement :: "[i=>o, [i,i]=>o] => o"
   199     "strong_replacement(M,P) == 
   200       \<forall>A[M]. univalent(M,A,P) -->
   201       (\<exists>Y[M]. (\<forall>b[M]. (b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b)))))"
   202 
   203   foundation_ax :: "(i=>o) => o"
   204     "foundation_ax(M) == 
   205 	\<forall>x[M]. (\<exists>y\<in>x. M(y))
   206                  --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & z \<in> y))"
   207 
   208 
   209 subsection{*A trivial consistency proof for $V_\omega$ *}
   210 
   211 text{*We prove that $V_\omega$ 
   212       (or @{text univ} in Isabelle) satisfies some ZF axioms.
   213      Kunen, Theorem IV 3.13, page 123.*}
   214 
   215 lemma univ0_downwards_mem: "[| y \<in> x; x \<in> univ(0) |] ==> y \<in> univ(0)"
   216 apply (insert Transset_univ [OF Transset_0])  
   217 apply (simp add: Transset_def, blast) 
   218 done
   219 
   220 lemma univ0_Ball_abs [simp]: 
   221      "A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   222 by (blast intro: univ0_downwards_mem) 
   223 
   224 lemma univ0_Bex_abs [simp]: 
   225      "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   226 by (blast intro: univ0_downwards_mem) 
   227 
   228 text{*Congruence rule for separation: can assume the variable is in @{text M}*}
   229 lemma separation_cong [cong]:
   230      "(!!x. M(x) ==> P(x) <-> P'(x)) 
   231       ==> separation(M, %x. P(x)) <-> separation(M, %x. P'(x))"
   232 by (simp add: separation_def) 
   233 
   234 text{*Congruence rules for replacement*}
   235 lemma univalent_cong [cong]:
   236      "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
   237       ==> univalent(M, A, %x y. P(x,y)) <-> univalent(M, A', %x y. P'(x,y))"
   238 by (simp add: univalent_def) 
   239 
   240 lemma strong_replacement_cong [cong]:
   241      "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
   242       ==> strong_replacement(M, %x y. P(x,y)) <-> 
   243           strong_replacement(M, %x y. P'(x,y))" 
   244 by (simp add: strong_replacement_def) 
   245 
   246 text{*The extensionality axiom*}
   247 lemma "extensionality(\<lambda>x. x \<in> univ(0))"
   248 apply (simp add: extensionality_def)
   249 apply (blast intro: univ0_downwards_mem) 
   250 done
   251 
   252 text{*The separation axiom requires some lemmas*}
   253 lemma Collect_in_Vfrom:
   254      "[| X \<in> Vfrom(A,j);  Transset(A) |] ==> Collect(X,P) \<in> Vfrom(A, succ(j))"
   255 apply (drule Transset_Vfrom)
   256 apply (rule subset_mem_Vfrom)
   257 apply (unfold Transset_def, blast)
   258 done
   259 
   260 lemma Collect_in_VLimit:
   261      "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] 
   262       ==> Collect(X,P) \<in> Vfrom(A,i)"
   263 apply (rule Limit_VfromE, assumption+)
   264 apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom)
   265 done
   266 
   267 lemma Collect_in_univ:
   268      "[| X \<in> univ(A);  Transset(A) |] ==> Collect(X,P) \<in> univ(A)"
   269 by (simp add: univ_def Collect_in_VLimit Limit_nat)
   270 
   271 lemma "separation(\<lambda>x. x \<in> univ(0), P)"
   272 apply (simp add: separation_def, clarify) 
   273 apply (rule_tac x = "Collect(z,P)" in bexI) 
   274 apply (blast intro: Collect_in_univ Transset_0)+
   275 done
   276 
   277 text{*Unordered pairing axiom*}
   278 lemma "upair_ax(\<lambda>x. x \<in> univ(0))"
   279 apply (simp add: upair_ax_def upair_def)  
   280 apply (blast intro: doubleton_in_univ) 
   281 done
   282 
   283 text{*Union axiom*}
   284 lemma "Union_ax(\<lambda>x. x \<in> univ(0))"  
   285 apply (simp add: Union_ax_def big_union_def, clarify) 
   286 apply (rule_tac x="\<Union>x" in bexI)  
   287  apply (blast intro: univ0_downwards_mem)
   288 apply (blast intro: Union_in_univ Transset_0) 
   289 done
   290 
   291 text{*Powerset axiom*}
   292 
   293 lemma Pow_in_univ:
   294      "[| X \<in> univ(A);  Transset(A) |] ==> Pow(X) \<in> univ(A)"
   295 apply (simp add: univ_def Pow_in_VLimit Limit_nat)
   296 done
   297 
   298 lemma "power_ax(\<lambda>x. x \<in> univ(0))"  
   299 apply (simp add: power_ax_def powerset_def subset_def, clarify) 
   300 apply (rule_tac x="Pow(x)" in bexI)
   301  apply (blast intro: univ0_downwards_mem)
   302 apply (blast intro: Pow_in_univ Transset_0) 
   303 done
   304 
   305 text{*Foundation axiom*}
   306 lemma "foundation_ax(\<lambda>x. x \<in> univ(0))"  
   307 apply (simp add: foundation_ax_def, clarify)
   308 apply (cut_tac A=x in foundation) 
   309 apply (blast intro: univ0_downwards_mem)
   310 done
   311 
   312 lemma "replacement(\<lambda>x. x \<in> univ(0), P)"  
   313 apply (simp add: replacement_def, clarify) 
   314 oops
   315 text{*no idea: maybe prove by induction on the rank of A?*}
   316 
   317 text{*Still missing: Replacement, Choice*}
   318 
   319 subsection{*lemmas needed to reduce some set constructions to instances
   320       of Separation*}
   321 
   322 lemma image_iff_Collect: "r `` A = {y \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=<x,y>}"
   323 apply (rule equalityI, auto) 
   324 apply (simp add: Pair_def, blast) 
   325 done
   326 
   327 lemma vimage_iff_Collect:
   328      "r -`` A = {x \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=<x,y>}"
   329 apply (rule equalityI, auto) 
   330 apply (simp add: Pair_def, blast) 
   331 done
   332 
   333 text{*These two lemmas lets us prove @{text domain_closed} and 
   334       @{text range_closed} without new instances of separation*}
   335 
   336 lemma domain_eq_vimage: "domain(r) = r -`` Union(Union(r))"
   337 apply (rule equalityI, auto)
   338 apply (rule vimageI, assumption)
   339 apply (simp add: Pair_def, blast) 
   340 done
   341 
   342 lemma range_eq_image: "range(r) = r `` Union(Union(r))"
   343 apply (rule equalityI, auto)
   344 apply (rule imageI, assumption)
   345 apply (simp add: Pair_def, blast) 
   346 done
   347 
   348 lemma replacementD:
   349     "[| replacement(M,P); M(A);  univalent(M,A,P) |]
   350      ==> \<exists>Y[M]. (\<forall>b[M]. ((\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y))"
   351 by (simp add: replacement_def) 
   352 
   353 lemma strong_replacementD:
   354     "[| strong_replacement(M,P); M(A);  univalent(M,A,P) |]
   355      ==> \<exists>Y[M]. (\<forall>b[M]. (b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b))))"
   356 by (simp add: strong_replacement_def) 
   357 
   358 lemma separationD:
   359     "[| separation(M,P); M(z) |] ==> \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
   360 by (simp add: separation_def) 
   361 
   362 
   363 text{*More constants, for order types*}
   364 constdefs
   365 
   366   order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
   367     "order_isomorphism(M,A,r,B,s,f) == 
   368         bijection(M,A,B,f) & 
   369         (\<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A -->
   370           (\<forall>p[M]. \<forall>fx[M]. \<forall>fy[M]. \<forall>q[M].
   371             pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) --> 
   372             pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))))"
   373 
   374   pred_set :: "[i=>o,i,i,i,i] => o"
   375     "pred_set(M,A,x,r,B) == 
   376 	\<forall>y[M]. y \<in> B <-> (\<exists>p[M]. p\<in>r & y \<in> A & pair(M,y,x,p))"
   377 
   378   membership :: "[i=>o,i,i] => o" --{*membership relation*}
   379     "membership(M,A,r) == 
   380 	\<forall>p[M]. p \<in> r <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>A & x\<in>y & pair(M,x,y,p)))"
   381 
   382 
   383 subsection{*Absoluteness for a transitive class model*}
   384 
   385 text{*The class M is assumed to be transitive and to satisfy some
   386       relativized ZF axioms*}
   387 locale M_triv_axioms =
   388   fixes M
   389   assumes transM:           "[| y\<in>x; M(x) |] ==> M(y)"
   390       and nonempty [simp]:  "M(0)"
   391       and upair_ax:	    "upair_ax(M)"
   392       and Union_ax:	    "Union_ax(M)"
   393       and power_ax:         "power_ax(M)"
   394       and replacement:      "replacement(M,P)"
   395       and M_nat [iff]:      "M(nat)"           (*i.e. the axiom of infinity*)
   396 
   397 lemma (in M_triv_axioms) ball_abs [simp]: 
   398      "M(A) ==> (\<forall>x\<in>A. M(x) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   399 by (blast intro: transM) 
   400 
   401 lemma (in M_triv_axioms) rall_abs [simp]: 
   402      "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   403 by (blast intro: transM) 
   404 
   405 lemma (in M_triv_axioms) bex_abs [simp]: 
   406      "M(A) ==> (\<exists>x\<in>A. M(x) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   407 by (blast intro: transM) 
   408 
   409 lemma (in M_triv_axioms) rex_abs [simp]: 
   410      "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   411 by (blast intro: transM) 
   412 
   413 lemma (in M_triv_axioms) ball_iff_equiv: 
   414      "M(A) ==> (\<forall>x[M]. (x\<in>A <-> P(x))) <-> 
   415                (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)" 
   416 by (blast intro: transM)
   417 
   418 text{*Simplifies proofs of equalities when there's an iff-equality
   419       available for rewriting, universally quantified over M. *}
   420 lemma (in M_triv_axioms) M_equalityI: 
   421      "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"
   422 by (blast intro!: equalityI dest: transM) 
   423 
   424 lemma (in M_triv_axioms) empty_abs [simp]: 
   425      "M(z) ==> empty(M,z) <-> z=0"
   426 apply (simp add: empty_def)
   427 apply (blast intro: transM) 
   428 done
   429 
   430 lemma (in M_triv_axioms) subset_abs [simp]: 
   431      "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"
   432 apply (simp add: subset_def) 
   433 apply (blast intro: transM) 
   434 done
   435 
   436 lemma (in M_triv_axioms) upair_abs [simp]: 
   437      "M(z) ==> upair(M,a,b,z) <-> z={a,b}"
   438 apply (simp add: upair_def) 
   439 apply (blast intro: transM) 
   440 done
   441 
   442 lemma (in M_triv_axioms) upair_in_M_iff [iff]:
   443      "M({a,b}) <-> M(a) & M(b)"
   444 apply (insert upair_ax, simp add: upair_ax_def) 
   445 apply (blast intro: transM) 
   446 done
   447 
   448 lemma (in M_triv_axioms) singleton_in_M_iff [iff]:
   449      "M({a}) <-> M(a)"
   450 by (insert upair_in_M_iff [of a a], simp) 
   451 
   452 lemma (in M_triv_axioms) pair_abs [simp]: 
   453      "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"
   454 apply (simp add: pair_def ZF.Pair_def)
   455 apply (blast intro: transM) 
   456 done
   457 
   458 lemma (in M_triv_axioms) pair_in_M_iff [iff]:
   459      "M(<a,b>) <-> M(a) & M(b)"
   460 by (simp add: ZF.Pair_def)
   461 
   462 lemma (in M_triv_axioms) pair_components_in_M:
   463      "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
   464 apply (simp add: Pair_def)
   465 apply (blast dest: transM) 
   466 done
   467 
   468 lemma (in M_triv_axioms) cartprod_abs [simp]: 
   469      "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
   470 apply (simp add: cartprod_def)
   471 apply (rule iffI) 
   472  apply (blast intro!: equalityI intro: transM dest!: rspec) 
   473 apply (blast dest: transM) 
   474 done
   475 
   476 lemma (in M_triv_axioms) union_abs [simp]: 
   477      "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
   478 apply (simp add: union_def) 
   479 apply (blast intro: transM) 
   480 done
   481 
   482 lemma (in M_triv_axioms) inter_abs [simp]: 
   483      "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"
   484 apply (simp add: inter_def) 
   485 apply (blast intro: transM) 
   486 done
   487 
   488 lemma (in M_triv_axioms) setdiff_abs [simp]: 
   489      "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"
   490 apply (simp add: setdiff_def) 
   491 apply (blast intro: transM) 
   492 done
   493 
   494 lemma (in M_triv_axioms) Union_abs [simp]: 
   495      "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"
   496 apply (simp add: big_union_def) 
   497 apply (blast intro!: equalityI dest: transM) 
   498 done
   499 
   500 lemma (in M_triv_axioms) Union_closed [intro,simp]:
   501      "M(A) ==> M(Union(A))"
   502 by (insert Union_ax, simp add: Union_ax_def) 
   503 
   504 lemma (in M_triv_axioms) Un_closed [intro,simp]:
   505      "[| M(A); M(B) |] ==> M(A Un B)"
   506 by (simp only: Un_eq_Union, blast) 
   507 
   508 lemma (in M_triv_axioms) cons_closed [intro,simp]:
   509      "[| M(a); M(A) |] ==> M(cons(a,A))"
   510 by (subst cons_eq [symmetric], blast) 
   511 
   512 lemma (in M_triv_axioms) cons_abs [simp]: 
   513      "[| M(b); M(z) |] ==> is_cons(M,a,b,z) <-> z = cons(a,b)"
   514 by (simp add: is_cons_def, blast intro: transM)  
   515 
   516 lemma (in M_triv_axioms) successor_abs [simp]: 
   517      "[| M(a); M(z) |] ==> successor(M,a,z) <-> z = succ(a)"
   518 by (simp add: successor_def, blast)  
   519 
   520 lemma (in M_triv_axioms) succ_in_M_iff [iff]:
   521      "M(succ(a)) <-> M(a)"
   522 apply (simp add: succ_def) 
   523 apply (blast intro: transM) 
   524 done
   525 
   526 lemma (in M_triv_axioms) separation_closed [intro,simp]:
   527      "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
   528 apply (insert separation, simp add: separation_def) 
   529 apply (drule rspec, assumption, clarify) 
   530 apply (subgoal_tac "y = Collect(A,P)", blast)
   531 apply (blast dest: transM) 
   532 done
   533 
   534 text{*Probably the premise and conclusion are equivalent*}
   535 lemma (in M_triv_axioms) strong_replacementI [rule_format]:
   536     "[| \<forall>A[M]. separation(M, %u. \<exists>x[M]. x\<in>A & P(x,u)) |]
   537      ==> strong_replacement(M,P)"
   538 apply (simp add: strong_replacement_def, clarify) 
   539 apply (frule replacementD [OF replacement], assumption, clarify) 
   540 apply (drule_tac x=A in rspec, clarify)  
   541 apply (drule_tac z=Y in separationD, assumption, clarify) 
   542 apply (rule_tac x=y in rexI) 
   543 apply (blast dest: transM)+
   544 done
   545 
   546 
   547 (*The last premise expresses that P takes M to M*)
   548 lemma (in M_triv_axioms) strong_replacement_closed [intro,simp]:
   549      "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
   550        !!x y. [| x\<in>A; P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
   551 apply (simp add: strong_replacement_def) 
   552 apply (drule rspec, auto) 
   553 apply (subgoal_tac "Replace(A,P) = Y")
   554  apply simp 
   555 apply (rule equality_iffI) 
   556 apply (simp add: Replace_iff, safe)
   557  apply (blast dest: transM) 
   558 apply (frule transM, assumption) 
   559  apply (simp add: univalent_def)
   560  apply (drule rspec [THEN iffD1], assumption, assumption)
   561  apply (blast dest: transM) 
   562 done
   563 
   564 (*The first premise can't simply be assumed as a schema.
   565   It is essential to take care when asserting instances of Replacement.
   566   Let K be a nonconstructible subset of nat and define
   567   f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a 
   568   nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
   569   even for f : M -> M.
   570 *)
   571 lemma (in M_triv_axioms) RepFun_closed [intro,simp]:
   572      "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
   573       ==> M(RepFun(A,f))"
   574 apply (simp add: RepFun_def) 
   575 apply (rule strong_replacement_closed) 
   576 apply (auto dest: transM  simp add: univalent_def) 
   577 done
   578 
   579 lemma (in M_triv_axioms) lam_closed [intro,simp]:
   580      "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
   581       ==> M(\<lambda>x\<in>A. b(x))"
   582 by (simp add: lam_def, blast dest: transM) 
   583 
   584 lemma (in M_triv_axioms) image_abs [simp]: 
   585      "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
   586 apply (simp add: image_def)
   587 apply (rule iffI) 
   588  apply (blast intro!: equalityI dest: transM, blast) 
   589 done
   590 
   591 text{*What about @{text Pow_abs}?  Powerset is NOT absolute!
   592       This result is one direction of absoluteness.*}
   593 
   594 lemma (in M_triv_axioms) powerset_Pow: 
   595      "powerset(M, x, Pow(x))"
   596 by (simp add: powerset_def)
   597 
   598 text{*But we can't prove that the powerset in @{text M} includes the
   599       real powerset.*}
   600 lemma (in M_triv_axioms) powerset_imp_subset_Pow: 
   601      "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
   602 apply (simp add: powerset_def) 
   603 apply (blast dest: transM) 
   604 done
   605 
   606 lemma (in M_triv_axioms) nat_into_M [intro]:
   607      "n \<in> nat ==> M(n)"
   608 by (induct n rule: nat_induct, simp_all)
   609 
   610 lemma (in M_triv_axioms) nat_case_closed:
   611   "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
   612 apply (case_tac "k=0", simp) 
   613 apply (case_tac "\<exists>m. k = succ(m)", force)
   614 apply (simp add: nat_case_def) 
   615 done
   616 
   617 lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
   618      "M(Inl(a)) <-> M(a)"
   619 by (simp add: Inl_def) 
   620 
   621 lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
   622      "M(Inr(a)) <-> M(a)"
   623 by (simp add: Inr_def)
   624 
   625 
   626 subsection{*Absoluteness for ordinals*}
   627 text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
   628 
   629 lemma (in M_triv_axioms) lt_closed:
   630      "[| j<i; M(i) |] ==> M(j)" 
   631 by (blast dest: ltD intro: transM) 
   632 
   633 lemma (in M_triv_axioms) transitive_set_abs [simp]: 
   634      "M(a) ==> transitive_set(M,a) <-> Transset(a)"
   635 by (simp add: transitive_set_def Transset_def)
   636 
   637 lemma (in M_triv_axioms) ordinal_abs [simp]: 
   638      "M(a) ==> ordinal(M,a) <-> Ord(a)"
   639 by (simp add: ordinal_def Ord_def)
   640 
   641 lemma (in M_triv_axioms) limit_ordinal_abs [simp]: 
   642      "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
   643 apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def) 
   644 apply (simp add: lt_def, blast) 
   645 done
   646 
   647 lemma (in M_triv_axioms) successor_ordinal_abs [simp]: 
   648      "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b[M]. a = succ(b))"
   649 apply (simp add: successor_ordinal_def, safe)
   650 apply (drule Ord_cases_disj, auto) 
   651 done
   652 
   653 lemma finite_Ord_is_nat:
   654       "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"
   655 by (induct a rule: trans_induct3, simp_all)
   656 
   657 lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
   658 by (induct a rule: nat_induct, auto)
   659 
   660 lemma (in M_triv_axioms) finite_ordinal_abs [simp]: 
   661      "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
   662 apply (simp add: finite_ordinal_def)
   663 apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord 
   664              dest: Ord_trans naturals_not_limit)
   665 done
   666 
   667 lemma Limit_non_Limit_implies_nat:
   668      "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"
   669 apply (rule le_anti_sym) 
   670 apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)  
   671  apply (simp add: lt_def)  
   672  apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) 
   673 apply (erule nat_le_Limit)
   674 done
   675 
   676 lemma (in M_triv_axioms) omega_abs [simp]: 
   677      "M(a) ==> omega(M,a) <-> a = nat"
   678 apply (simp add: omega_def) 
   679 apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
   680 done
   681 
   682 lemma (in M_triv_axioms) number1_abs [simp]: 
   683      "M(a) ==> number1(M,a) <-> a = 1"
   684 by (simp add: number1_def) 
   685 
   686 lemma (in M_triv_axioms) number1_abs [simp]: 
   687      "M(a) ==> number2(M,a) <-> a = succ(1)"
   688 by (simp add: number2_def) 
   689 
   690 lemma (in M_triv_axioms) number3_abs [simp]: 
   691      "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
   692 by (simp add: number3_def) 
   693 
   694 text{*Kunen continued to 20...*}
   695 
   696 (*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything 
   697   but the recursion variable must stay unchanged.  But then the recursion
   698   equations only hold for x\<in>nat (or in some other set) and not for the 
   699   whole of the class M.
   700   consts
   701     natnumber_aux :: "[i=>o,i] => i"
   702 
   703   primrec
   704       "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
   705       "natnumber_aux(M,succ(n)) = 
   706 	   (\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x)) 
   707 		     then 1 else 0)"
   708 
   709   constdefs
   710     natnumber :: "[i=>o,i,i] => o"
   711       "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
   712 
   713   lemma (in M_triv_axioms) [simp]: 
   714        "natnumber(M,0,x) == x=0"
   715 *)
   716 
   717 subsection{*Some instances of separation and strong replacement*}
   718 
   719 locale M_axioms = M_triv_axioms +
   720 assumes Inter_separation:
   721      "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
   722   and cartprod_separation:
   723      "[| M(A); M(B) |] 
   724       ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,z)))"
   725   and image_separation:
   726      "[| M(A); M(r) |] 
   727       ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,p)))"
   728   and converse_separation:
   729      "M(r) ==> separation(M, 
   730          \<lambda>z. \<exists>p[M]. p\<in>r & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
   731   and restrict_separation:
   732      "M(A) ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. pair(M,x,y,z)))"
   733   and comp_separation:
   734      "[| M(r); M(s) |]
   735       ==> separation(M, \<lambda>xz. \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
   736 		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
   737                   xy\<in>s & yz\<in>r)"
   738   and pred_separation:
   739      "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & pair(M,y,x,p))"
   740   and Memrel_separation:
   741      "separation(M, \<lambda>z. \<exists>x[M]. \<exists>y[M]. pair(M,x,y,z) & x \<in> y)"
   742   and funspace_succ_replacement:
   743      "M(n) ==> 
   744       strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. \<exists>cnbf[M]. 
   745                 pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &
   746                 upair(M,cnbf,cnbf,z))"
   747   and well_ord_iso_separation:
   748      "[| M(A); M(f); M(r) |] 
   749       ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y[M]. (\<exists>p[M]. 
   750 		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
   751   and obase_separation:
   752      --{*part of the order type formalization*}
   753      "[| M(A); M(r) |] 
   754       ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
   755 	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
   756 	     order_isomorphism(M,par,r,x,mx,g))"
   757   and obase_equals_separation:
   758      "[| M(A); M(r) |] 
   759       ==> separation (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M]. 
   760 			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M]. 
   761 			      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
   762 			      order_isomorphism(M,pxr,r,y,my,g))))"
   763   and omap_replacement:
   764      "[| M(A); M(r) |] 
   765       ==> strong_replacement(M,
   766              \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
   767 	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
   768 	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
   769   and is_recfun_separation:
   770      --{*for well-founded recursion*}
   771      "[| M(r); M(f); M(g); M(a); M(b) |] 
   772      ==> separation(M, 
   773             \<lambda>x. \<exists>xa[M]. \<exists>xb[M]. 
   774                 pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r & 
   775                 (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) & 
   776                                    fx \<noteq> gx))"
   777 
   778 lemma (in M_axioms) cartprod_iff_lemma:
   779      "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
   780          powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
   781        ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
   782 apply (simp add: powerset_def) 
   783 apply (rule equalityI, clarify, simp)
   784  apply (frule transM, assumption) 
   785  apply (frule transM, assumption, simp) 
   786  apply blast 
   787 apply clarify
   788 apply (frule transM, assumption, force) 
   789 done
   790 
   791 lemma (in M_axioms) cartprod_iff:
   792      "[| M(A); M(B); M(C) |] 
   793       ==> cartprod(M,A,B,C) <-> 
   794           (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &
   795                    C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
   796 apply (simp add: Pair_def cartprod_def, safe)
   797 defer 1 
   798   apply (simp add: powerset_def) 
   799  apply blast 
   800 txt{*Final, difficult case: the left-to-right direction of the theorem.*}
   801 apply (insert power_ax, simp add: power_ax_def) 
   802 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   803 apply (blast, clarify) 
   804 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)
   805 apply assumption
   806 apply (blast intro: cartprod_iff_lemma) 
   807 done
   808 
   809 lemma (in M_axioms) cartprod_closed_lemma:
   810      "[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
   811 apply (simp del: cartprod_abs add: cartprod_iff)
   812 apply (insert power_ax, simp add: power_ax_def) 
   813 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   814 apply (blast, clarify) 
   815 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   816 apply (blast, clarify)
   817 apply (intro rexI exI conjI) 
   818 prefer 5 apply (rule refl) 
   819 prefer 3 apply assumption
   820 prefer 3 apply assumption
   821 apply (insert cartprod_separation [of A B], auto)
   822 done
   823 
   824 text{*All the lemmas above are necessary because Powerset is not absolute.
   825       I should have used Replacement instead!*}
   826 lemma (in M_axioms) cartprod_closed [intro,simp]: 
   827      "[| M(A); M(B) |] ==> M(A*B)"
   828 by (frule cartprod_closed_lemma, assumption, force)
   829 
   830 lemma (in M_axioms) sum_closed [intro,simp]: 
   831      "[| M(A); M(B) |] ==> M(A+B)"
   832 by (simp add: sum_def)
   833 
   834 
   835 subsubsection {*converse of a relation*}
   836 
   837 lemma (in M_axioms) M_converse_iff:
   838      "M(r) ==> 
   839       converse(r) = 
   840       {z \<in> Union(Union(r)) * Union(Union(r)). 
   841        \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"
   842 apply (rule equalityI)
   843  prefer 2 apply (blast dest: transM, clarify, simp) 
   844 apply (simp add: Pair_def) 
   845 apply (blast dest: transM) 
   846 done
   847 
   848 lemma (in M_axioms) converse_closed [intro,simp]: 
   849      "M(r) ==> M(converse(r))"
   850 apply (simp add: M_converse_iff)
   851 apply (insert converse_separation [of r], simp)
   852 done
   853 
   854 lemma (in M_axioms) converse_abs [simp]: 
   855      "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
   856 apply (simp add: is_converse_def)
   857 apply (rule iffI)
   858  prefer 2 apply blast 
   859 apply (rule M_equalityI)
   860   apply simp
   861   apply (blast dest: transM)+
   862 done
   863 
   864 
   865 subsubsection {*image, preimage, domain, range*}
   866 
   867 lemma (in M_axioms) image_closed [intro,simp]: 
   868      "[| M(A); M(r) |] ==> M(r``A)"
   869 apply (simp add: image_iff_Collect)
   870 apply (insert image_separation [of A r], simp) 
   871 done
   872 
   873 lemma (in M_axioms) vimage_abs [simp]: 
   874      "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A"
   875 apply (simp add: pre_image_def)
   876 apply (rule iffI) 
   877  apply (blast intro!: equalityI dest: transM, blast) 
   878 done
   879 
   880 lemma (in M_axioms) vimage_closed [intro,simp]: 
   881      "[| M(A); M(r) |] ==> M(r-``A)"
   882 by (simp add: vimage_def)
   883 
   884 
   885 subsubsection{*Domain, range and field*}
   886 
   887 lemma (in M_axioms) domain_abs [simp]: 
   888      "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
   889 apply (simp add: is_domain_def) 
   890 apply (blast intro!: equalityI dest: transM) 
   891 done
   892 
   893 lemma (in M_axioms) domain_closed [intro,simp]: 
   894      "M(r) ==> M(domain(r))"
   895 apply (simp add: domain_eq_vimage)
   896 done
   897 
   898 lemma (in M_axioms) range_abs [simp]: 
   899      "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
   900 apply (simp add: is_range_def)
   901 apply (blast intro!: equalityI dest: transM)
   902 done
   903 
   904 lemma (in M_axioms) range_closed [intro,simp]: 
   905      "M(r) ==> M(range(r))"
   906 apply (simp add: range_eq_image)
   907 done
   908 
   909 lemma (in M_axioms) field_abs [simp]: 
   910      "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"
   911 by (simp add: domain_closed range_closed is_field_def field_def)
   912 
   913 lemma (in M_axioms) field_closed [intro,simp]: 
   914      "M(r) ==> M(field(r))"
   915 by (simp add: domain_closed range_closed Un_closed field_def) 
   916 
   917 
   918 subsubsection{*Relations, functions and application*}
   919 
   920 lemma (in M_axioms) relation_abs [simp]: 
   921      "M(r) ==> is_relation(M,r) <-> relation(r)"
   922 apply (simp add: is_relation_def relation_def) 
   923 apply (blast dest!: bspec dest: pair_components_in_M)+
   924 done
   925 
   926 lemma (in M_axioms) function_abs [simp]: 
   927      "M(r) ==> is_function(M,r) <-> function(r)"
   928 apply (simp add: is_function_def function_def, safe) 
   929    apply (frule transM, assumption) 
   930   apply (blast dest: pair_components_in_M)+
   931 done
   932 
   933 lemma (in M_axioms) apply_closed [intro,simp]: 
   934      "[|M(f); M(a)|] ==> M(f`a)"
   935 by (simp add: apply_def)
   936 
   937 lemma (in M_axioms) apply_abs: 
   938      "[| function(f); M(f); M(y) |] 
   939       ==> fun_apply(M,f,x,y) <-> x \<in> domain(f) & f`x = y"
   940 apply (simp add: fun_apply_def)
   941 apply (blast intro: function_apply_equality function_apply_Pair) 
   942 done
   943 
   944 lemma (in M_axioms) typed_apply_abs: 
   945      "[| f \<in> A -> B; M(f); M(y) |] 
   946       ==> fun_apply(M,f,x,y) <-> x \<in> A & f`x = y"
   947 by (simp add: apply_abs fun_is_function domain_of_fun) 
   948 
   949 lemma (in M_axioms) typed_function_abs [simp]: 
   950      "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
   951 apply (auto simp add: typed_function_def relation_def Pi_iff) 
   952 apply (blast dest: pair_components_in_M)+
   953 done
   954 
   955 lemma (in M_axioms) injection_abs [simp]: 
   956      "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
   957 apply (simp add: injection_def apply_iff inj_def apply_closed)
   958 apply (blast dest: transM [of _ A]) 
   959 done
   960 
   961 lemma (in M_axioms) surjection_abs [simp]: 
   962      "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
   963 by (simp add: typed_apply_abs surjection_def surj_def)
   964 
   965 lemma (in M_axioms) bijection_abs [simp]: 
   966      "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
   967 by (simp add: bijection_def bij_def)
   968 
   969 
   970 subsubsection{*Composition of relations*}
   971 
   972 lemma (in M_axioms) M_comp_iff:
   973      "[| M(r); M(s) |] 
   974       ==> r O s = 
   975           {xz \<in> domain(s) * range(r).  
   976             \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. xz = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r}"
   977 apply (simp add: comp_def)
   978 apply (rule equalityI) 
   979  apply clarify 
   980  apply simp 
   981  apply  (blast dest:  transM)+
   982 done
   983 
   984 lemma (in M_axioms) comp_closed [intro,simp]: 
   985      "[| M(r); M(s) |] ==> M(r O s)"
   986 apply (simp add: M_comp_iff)
   987 apply (insert comp_separation [of r s], simp) 
   988 done
   989 
   990 lemma (in M_axioms) composition_abs [simp]: 
   991      "[| M(r); M(s); M(t) |] 
   992       ==> composition(M,r,s,t) <-> t = r O s"
   993 apply safe
   994  txt{*Proving @{term "composition(M, r, s, r O s)"}*}
   995  prefer 2 
   996  apply (simp add: composition_def comp_def)
   997  apply (blast dest: transM) 
   998 txt{*Opposite implication*}
   999 apply (rule M_equalityI)
  1000   apply (simp add: composition_def comp_def)
  1001   apply (blast del: allE dest: transM)+
  1002 done
  1003 
  1004 text{*no longer needed*}
  1005 lemma (in M_axioms) restriction_is_function: 
  1006      "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
  1007       ==> function(z)"
  1008 apply (rotate_tac 1)
  1009 apply (simp add: restriction_def ball_iff_equiv) 
  1010 apply (unfold function_def, blast) 
  1011 done
  1012 
  1013 lemma (in M_axioms) restriction_abs [simp]: 
  1014      "[| M(f); M(A); M(z) |] 
  1015       ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
  1016 apply (simp add: ball_iff_equiv restriction_def restrict_def)
  1017 apply (blast intro!: equalityI dest: transM) 
  1018 done
  1019 
  1020 
  1021 lemma (in M_axioms) M_restrict_iff:
  1022      "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
  1023 by (simp add: restrict_def, blast dest: transM)
  1024 
  1025 lemma (in M_axioms) restrict_closed [intro,simp]: 
  1026      "[| M(A); M(r) |] ==> M(restrict(r,A))"
  1027 apply (simp add: M_restrict_iff)
  1028 apply (insert restrict_separation [of A], simp) 
  1029 done
  1030 
  1031 lemma (in M_axioms) Inter_abs [simp]: 
  1032      "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
  1033 apply (simp add: big_inter_def Inter_def) 
  1034 apply (blast intro!: equalityI dest: transM) 
  1035 done
  1036 
  1037 lemma (in M_axioms) Inter_closed [intro,simp]:
  1038      "M(A) ==> M(Inter(A))"
  1039 by (insert Inter_separation, simp add: Inter_def)
  1040 
  1041 lemma (in M_axioms) Int_closed [intro,simp]:
  1042      "[| M(A); M(B) |] ==> M(A Int B)"
  1043 apply (subgoal_tac "M({A,B})")
  1044 apply (frule Inter_closed, force+) 
  1045 done
  1046 
  1047 subsubsection{*Functions and function space*}
  1048 
  1049 text{*M contains all finite functions*}
  1050 lemma (in M_axioms) finite_fun_closed_lemma [rule_format]: 
  1051      "[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"
  1052 apply (induct_tac n, simp)
  1053 apply (rule ballI)  
  1054 apply (simp add: succ_def) 
  1055 apply (frule fun_cons_restrict_eq)
  1056 apply (erule ssubst) 
  1057 apply (subgoal_tac "M(f`x) & restrict(f,x) \<in> x -> A") 
  1058  apply (simp add: cons_closed nat_into_M apply_closed) 
  1059 apply (blast intro: apply_funtype transM restrict_type2) 
  1060 done
  1061 
  1062 lemma (in M_axioms) finite_fun_closed [rule_format]: 
  1063      "[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"
  1064 by (blast intro: finite_fun_closed_lemma) 
  1065 
  1066 text{*The assumption @{term "M(A->B)"} is unusual, but essential: in 
  1067 all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
  1068 lemma (in M_axioms) is_funspace_abs [simp]:
  1069      "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B";
  1070 apply (simp add: is_funspace_def)
  1071 apply (rule iffI)
  1072  prefer 2 apply blast 
  1073 apply (rule M_equalityI)
  1074   apply simp_all
  1075 done
  1076 
  1077 lemma (in M_axioms) succ_fun_eq2:
  1078      "[|M(B); M(n->B)|] ==>
  1079       succ(n) -> B = 
  1080       \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"
  1081 apply (simp add: succ_fun_eq)
  1082 apply (blast dest: transM)  
  1083 done
  1084 
  1085 lemma (in M_axioms) funspace_succ:
  1086      "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)"
  1087 apply (insert funspace_succ_replacement [of n], simp) 
  1088 apply (force simp add: succ_fun_eq2 univalent_def) 
  1089 done
  1090 
  1091 text{*@{term M} contains all finite function spaces.  Needed to prove the
  1092 absoluteness of transitive closure.*}
  1093 lemma (in M_axioms) finite_funspace_closed [intro,simp]:
  1094      "[|n\<in>nat; M(B)|] ==> M(n->B)"
  1095 apply (induct_tac n, simp)
  1096 apply (simp add: funspace_succ nat_into_M) 
  1097 done
  1098 
  1099 end