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