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