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