src/ZF/Constructible/Relative.thy
author paulson
Fri Jul 05 18:33:50 2002 +0200 (2002-07-05)
changeset 13306 6eebcddee32b
parent 13299 3a932abf97e8
child 13316 d16629fd0f95
permissions -rw-r--r--
more internalized formulas and separation proofs
     1 header {*Relativization and Absoluteness*}
     2 
     3 theory Relative = Main:
     4 
     5 subsection{* Relativized versions of standard set-theoretic concepts *}
     6 
     7 constdefs
     8   empty :: "[i=>o,i] => o"
     9     "empty(M,z) == \<forall>x[M]. x \<notin> z"
    10 
    11   subset :: "[i=>o,i,i] => o"
    12     "subset(M,A,B) == \<forall>x[M]. x\<in>A --> x \<in> B"
    13 
    14   upair :: "[i=>o,i,i,i] => o"
    15     "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x[M]. x\<in>z --> x = a | x = b)"
    16 
    17   pair :: "[i=>o,i,i,i] => o"
    18     "pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & 
    19                           (\<exists>y[M]. upair(M,a,b,y) & upair(M,x,y,z))"
    20 
    21 
    22   union :: "[i=>o,i,i,i] => o"
    23     "union(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a | x \<in> b"
    24 
    25   is_cons :: "[i=>o,i,i,i] => o"
    26     "is_cons(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & union(M,x,b,z)"
    27 
    28   successor :: "[i=>o,i,i] => o"
    29     "successor(M,a,z) == is_cons(M,a,a,z)"
    30 
    31   powerset :: "[i=>o,i,i] => o"
    32     "powerset(M,A,z) == \<forall>x[M]. x \<in> z <-> subset(M,x,A)"
    33 
    34   inter :: "[i=>o,i,i,i] => o"
    35     "inter(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<in> b"
    36 
    37   setdiff :: "[i=>o,i,i,i] => o"
    38     "setdiff(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<notin> b"
    39 
    40   big_union :: "[i=>o,i,i] => o"
    41     "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)"
    42 
    43   big_inter :: "[i=>o,i,i] => o"
    44     "big_inter(M,A,z) == 
    45              (A=0 --> z=0) &
    46 	     (A\<noteq>0 --> (\<forall>x[M]. x \<in> z <-> (\<forall>y[M]. y\<in>A --> x \<in> y)))"
    47 
    48   cartprod :: "[i=>o,i,i,i] => o"
    49     "cartprod(M,A,B,z) == 
    50 	\<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))"
    51 
    52   is_converse :: "[i=>o,i,i] => o"
    53     "is_converse(M,r,z) == 
    54 	\<forall>x[M]. x \<in> z <-> 
    55              (\<exists>w[M]. w\<in>r & (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x)))"
    56 
    57   pre_image :: "[i=>o,i,i,i] => o"
    58     "pre_image(M,r,A,z) == 
    59 	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))"
    60 
    61   is_domain :: "[i=>o,i,i] => o"
    62     "is_domain(M,r,z) == 
    63 	\<forall>x[M]. (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))"
    64 
    65   image :: "[i=>o,i,i,i] => o"
    66     "image(M,r,A,z) == 
    67         \<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))"
    68 
    69   is_range :: "[i=>o,i,i] => o"
    70     --{*the cleaner 
    71       @{term "\<exists>r'[M]. is_converse(M,r,r') & is_domain(M,r',z)"}
    72       unfortunately needs an instance of separation in order to prove 
    73         @{term "M(converse(r))"}.*}
    74     "is_range(M,r,z) == 
    75 	\<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))"
    76 
    77   is_field :: "[i=>o,i,i] => o"
    78     "is_field(M,r,z) == 
    79 	\<exists>dr[M]. is_domain(M,r,dr) & 
    80             (\<exists>rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))"
    81 
    82   is_relation :: "[i=>o,i] => o"
    83     "is_relation(M,r) == 
    84         (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))"
    85 
    86   is_function :: "[i=>o,i] => o"
    87     "is_function(M,r) == 
    88 	\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M]. 
    89            pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'"
    90 
    91   fun_apply :: "[i=>o,i,i,i] => o"
    92     "fun_apply(M,f,x,y) == 
    93 	(\<forall>y'[M]. (\<exists>u[M]. u\<in>f & pair(M,x,y',u)) <-> y=y')"
    94 
    95   typed_function :: "[i=>o,i,i,i] => o"
    96     "typed_function(M,A,B,r) == 
    97         is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
    98         (\<forall>u[M]. u\<in>r --> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) --> y\<in>B))"
    99 
   100   is_funspace :: "[i=>o,i,i,i] => o"
   101     "is_funspace(M,A,B,F) == 
   102         \<forall>f[M]. f \<in> F <-> typed_function(M,A,B,f)"
   103 
   104   composition :: "[i=>o,i,i,i] => o"
   105     "composition(M,r,s,t) == 
   106         \<forall>p[M]. p \<in> t <-> 
   107                (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. pair(M,x,z,p) & \<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[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M]. 
   114           pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> 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[M]. y\<in>B --> (\<exists>x[M]. x\<in>A & 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 \<in> z <-> (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[M]. x\<in>A --> (\<forall>y[M]. y\<in>A -->
   367           (\<forall>p[M]. \<forall>fx[M]. \<forall>fy[M]. \<forall>q[M].
   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   pred_set :: "[i=>o,i,i,i,i] => o"
   372     "pred_set(M,A,x,r,B) == 
   373 	\<forall>y[M]. y \<in> B <-> (\<exists>p[M]. p\<in>r & y \<in> A & pair(M,y,x,p))"
   374 
   375   membership :: "[i=>o,i,i] => o" --{*membership relation*}
   376     "membership(M,A,r) == 
   377 	\<forall>p[M]. p \<in> r <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>A & x\<in>y & pair(M,x,y,p)))"
   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\<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) cons_abs [simp]: 
   510      "[| M(b); M(z) |] ==> is_cons(M,a,b,z) <-> z = cons(a,b)"
   511 by (simp add: is_cons_def, blast intro: transM)  
   512 
   513 lemma (in M_triv_axioms) successor_abs [simp]: 
   514      "[| M(a); M(z) |] ==> successor(M,a,z) <-> z = succ(a)"
   515 by (simp add: successor_def, blast)  
   516 
   517 lemma (in M_triv_axioms) succ_in_M_iff [iff]:
   518      "M(succ(a)) <-> M(a)"
   519 apply (simp add: succ_def) 
   520 apply (blast intro: transM) 
   521 done
   522 
   523 lemma (in M_triv_axioms) separation_closed [intro,simp]:
   524      "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
   525 apply (insert separation, simp add: separation_def) 
   526 apply (drule rspec, assumption, clarify) 
   527 apply (subgoal_tac "y = Collect(A,P)", blast)
   528 apply (blast dest: transM) 
   529 done
   530 
   531 text{*Probably the premise and conclusion are equivalent*}
   532 lemma (in M_triv_axioms) strong_replacementI [OF rallI]:
   533     "[| \<forall>A[M]. separation(M, %u. \<exists>x[M]. x\<in>A & P(x,u)) |]
   534      ==> strong_replacement(M,P)"
   535 apply (simp add: strong_replacement_def, clarify) 
   536 apply (frule replacementD [OF replacement], assumption, clarify) 
   537 apply (drule_tac x=A in rspec, clarify)  
   538 apply (drule_tac z=Y in separationD, assumption, clarify) 
   539 apply (rule_tac x=y in rexI) 
   540 apply (blast dest: transM)+
   541 done
   542 
   543 
   544 (*The last premise expresses that P takes M to M*)
   545 lemma (in M_triv_axioms) strong_replacement_closed [intro,simp]:
   546      "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
   547        !!x y. [| x\<in>A; P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
   548 apply (simp add: strong_replacement_def) 
   549 apply (drule rspec, auto) 
   550 apply (subgoal_tac "Replace(A,P) = Y")
   551  apply simp 
   552 apply (rule equality_iffI) 
   553 apply (simp add: Replace_iff, safe)
   554  apply (blast dest: transM) 
   555 apply (frule transM, assumption) 
   556  apply (simp add: univalent_def)
   557  apply (drule rspec [THEN iffD1], assumption, assumption)
   558  apply (blast dest: transM) 
   559 done
   560 
   561 (*The first premise can't simply be assumed as a schema.
   562   It is essential to take care when asserting instances of Replacement.
   563   Let K be a nonconstructible subset of nat and define
   564   f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a 
   565   nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
   566   even for f : M -> M.
   567 *)
   568 lemma (in M_triv_axioms) RepFun_closed [intro,simp]:
   569      "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
   570       ==> M(RepFun(A,f))"
   571 apply (simp add: RepFun_def) 
   572 apply (rule strong_replacement_closed) 
   573 apply (auto dest: transM  simp add: univalent_def) 
   574 done
   575 
   576 lemma (in M_triv_axioms) lam_closed [intro,simp]:
   577      "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
   578       ==> M(\<lambda>x\<in>A. b(x))"
   579 by (simp add: lam_def, blast dest: transM) 
   580 
   581 lemma (in M_triv_axioms) image_abs [simp]: 
   582      "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
   583 apply (simp add: image_def)
   584 apply (rule iffI) 
   585  apply (blast intro!: equalityI dest: transM, blast) 
   586 done
   587 
   588 text{*What about @{text Pow_abs}?  Powerset is NOT absolute!
   589       This result is one direction of absoluteness.*}
   590 
   591 lemma (in M_triv_axioms) powerset_Pow: 
   592      "powerset(M, x, Pow(x))"
   593 by (simp add: powerset_def)
   594 
   595 text{*But we can't prove that the powerset in @{text M} includes the
   596       real powerset.*}
   597 lemma (in M_triv_axioms) powerset_imp_subset_Pow: 
   598      "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
   599 apply (simp add: powerset_def) 
   600 apply (blast dest: transM) 
   601 done
   602 
   603 lemma (in M_triv_axioms) nat_into_M [intro]:
   604      "n \<in> nat ==> M(n)"
   605 by (induct n rule: nat_induct, simp_all)
   606 
   607 lemma (in M_triv_axioms) nat_case_closed:
   608   "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
   609 apply (case_tac "k=0", simp) 
   610 apply (case_tac "\<exists>m. k = succ(m)", force)
   611 apply (simp add: nat_case_def) 
   612 done
   613 
   614 lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
   615      "M(Inl(a)) <-> M(a)"
   616 by (simp add: Inl_def) 
   617 
   618 lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
   619      "M(Inr(a)) <-> M(a)"
   620 by (simp add: Inr_def)
   621 
   622 
   623 subsection{*Absoluteness for ordinals*}
   624 text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
   625 
   626 lemma (in M_triv_axioms) lt_closed:
   627      "[| j<i; M(i) |] ==> M(j)" 
   628 by (blast dest: ltD intro: transM) 
   629 
   630 lemma (in M_triv_axioms) transitive_set_abs [simp]: 
   631      "M(a) ==> transitive_set(M,a) <-> Transset(a)"
   632 by (simp add: transitive_set_def Transset_def)
   633 
   634 lemma (in M_triv_axioms) ordinal_abs [simp]: 
   635      "M(a) ==> ordinal(M,a) <-> Ord(a)"
   636 by (simp add: ordinal_def Ord_def)
   637 
   638 lemma (in M_triv_axioms) limit_ordinal_abs [simp]: 
   639      "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
   640 apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def) 
   641 apply (simp add: lt_def, blast) 
   642 done
   643 
   644 lemma (in M_triv_axioms) successor_ordinal_abs [simp]: 
   645      "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b[M]. a = succ(b))"
   646 apply (simp add: successor_ordinal_def, safe)
   647 apply (drule Ord_cases_disj, auto) 
   648 done
   649 
   650 lemma finite_Ord_is_nat:
   651       "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"
   652 by (induct a rule: trans_induct3, simp_all)
   653 
   654 lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
   655 by (induct a rule: nat_induct, auto)
   656 
   657 lemma (in M_triv_axioms) finite_ordinal_abs [simp]: 
   658      "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
   659 apply (simp add: finite_ordinal_def)
   660 apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord 
   661              dest: Ord_trans naturals_not_limit)
   662 done
   663 
   664 lemma Limit_non_Limit_implies_nat:
   665      "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"
   666 apply (rule le_anti_sym) 
   667 apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)  
   668  apply (simp add: lt_def)  
   669  apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) 
   670 apply (erule nat_le_Limit)
   671 done
   672 
   673 lemma (in M_triv_axioms) omega_abs [simp]: 
   674      "M(a) ==> omega(M,a) <-> a = nat"
   675 apply (simp add: omega_def) 
   676 apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
   677 done
   678 
   679 lemma (in M_triv_axioms) number1_abs [simp]: 
   680      "M(a) ==> number1(M,a) <-> a = 1"
   681 by (simp add: number1_def) 
   682 
   683 lemma (in M_triv_axioms) number1_abs [simp]: 
   684      "M(a) ==> number2(M,a) <-> a = succ(1)"
   685 by (simp add: number2_def) 
   686 
   687 lemma (in M_triv_axioms) number3_abs [simp]: 
   688      "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
   689 by (simp add: number3_def) 
   690 
   691 text{*Kunen continued to 20...*}
   692 
   693 (*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything 
   694   but the recursion variable must stay unchanged.  But then the recursion
   695   equations only hold for x\<in>nat (or in some other set) and not for the 
   696   whole of the class M.
   697   consts
   698     natnumber_aux :: "[i=>o,i] => i"
   699 
   700   primrec
   701       "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
   702       "natnumber_aux(M,succ(n)) = 
   703 	   (\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x)) 
   704 		     then 1 else 0)"
   705 
   706   constdefs
   707     natnumber :: "[i=>o,i,i] => o"
   708       "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
   709 
   710   lemma (in M_triv_axioms) [simp]: 
   711        "natnumber(M,0,x) == x=0"
   712 *)
   713 
   714 subsection{*Some instances of separation and strong replacement*}
   715 
   716 locale M_axioms = M_triv_axioms +
   717 assumes Inter_separation:
   718      "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
   719   and cartprod_separation:
   720      "[| M(A); M(B) |] 
   721       ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,z)))"
   722   and image_separation:
   723      "[| M(A); M(r) |] 
   724       ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,p)))"
   725   and converse_separation:
   726      "M(r) ==> separation(M, 
   727          \<lambda>z. \<exists>p[M]. p\<in>r & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
   728   and restrict_separation:
   729      "M(A) ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. pair(M,x,y,z)))"
   730   and comp_separation:
   731      "[| M(r); M(s) |]
   732       ==> separation(M, \<lambda>xz. \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
   733 		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
   734                   xy\<in>s & yz\<in>r)"
   735   and pred_separation:
   736      "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & pair(M,y,x,p))"
   737   and Memrel_separation:
   738      "separation(M, \<lambda>z. \<exists>x[M]. \<exists>y[M]. pair(M,x,y,z) & x \<in> y)"
   739   and funspace_succ_replacement:
   740      "M(n) ==> 
   741       strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. \<exists>cnbf[M]. 
   742                 pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &
   743                 upair(M,cnbf,cnbf,z))"
   744   and well_ord_iso_separation:
   745      "[| M(A); M(f); M(r) |] 
   746       ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y[M]. (\<exists>p[M]. 
   747 		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
   748   and obase_separation:
   749      --{*part of the order type formalization*}
   750      "[| M(A); M(r) |] 
   751       ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
   752 	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
   753 	     order_isomorphism(M,par,r,x,mx,g))"
   754   and obase_equals_separation:
   755      "[| M(A); M(r) |] 
   756       ==> separation
   757       (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M]. 
   758 	      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M]. 
   759 	      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
   760 	      order_isomorphism(M,pxr,r,y,my,g))))"
   761   and omap_replacement:
   762      "[| M(A); M(r) |] 
   763       ==> strong_replacement(M,
   764              \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
   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   and is_recfun_separation:
   768      --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
   769      "[| M(A); M(f); M(g); M(a); M(b) |] 
   770      ==> separation(M, \<lambda>x. \<langle>x,a\<rangle> \<in> r & \<langle>x,b\<rangle> \<in> r & f`x \<noteq> g`x)"
   771 
   772 lemma (in M_axioms) cartprod_iff_lemma:
   773      "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
   774          powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
   775        ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
   776 apply (simp add: powerset_def) 
   777 apply (rule equalityI, clarify, simp)
   778  apply (frule transM, assumption) 
   779  apply (frule transM, assumption, simp) 
   780  apply blast 
   781 apply clarify
   782 apply (frule transM, assumption, force) 
   783 done
   784 
   785 lemma (in M_axioms) cartprod_iff:
   786      "[| M(A); M(B); M(C) |] 
   787       ==> cartprod(M,A,B,C) <-> 
   788           (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &
   789                    C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
   790 apply (simp add: Pair_def cartprod_def, safe)
   791 defer 1 
   792   apply (simp add: powerset_def) 
   793  apply blast 
   794 txt{*Final, difficult case: the left-to-right direction of the theorem.*}
   795 apply (insert power_ax, simp add: power_ax_def) 
   796 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   797 apply (blast, clarify) 
   798 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)
   799 apply assumption
   800 apply (blast intro: cartprod_iff_lemma) 
   801 done
   802 
   803 lemma (in M_axioms) cartprod_closed_lemma:
   804      "[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
   805 apply (simp del: cartprod_abs add: cartprod_iff)
   806 apply (insert power_ax, simp add: power_ax_def) 
   807 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   808 apply (blast, clarify) 
   809 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   810 apply (blast, clarify)
   811 apply (intro rexI exI conjI) 
   812 prefer 5 apply (rule refl) 
   813 prefer 3 apply assumption
   814 prefer 3 apply assumption
   815 apply (insert cartprod_separation [of A B], auto)
   816 done
   817 
   818 text{*All the lemmas above are necessary because Powerset is not absolute.
   819       I should have used Replacement instead!*}
   820 lemma (in M_axioms) cartprod_closed [intro,simp]: 
   821      "[| M(A); M(B) |] ==> M(A*B)"
   822 by (frule cartprod_closed_lemma, assumption, force)
   823 
   824 lemma (in M_axioms) sum_closed [intro,simp]: 
   825      "[| M(A); M(B) |] ==> M(A+B)"
   826 by (simp add: sum_def)
   827 
   828 
   829 subsubsection {*converse of a relation*}
   830 
   831 lemma (in M_axioms) M_converse_iff:
   832      "M(r) ==> 
   833       converse(r) = 
   834       {z \<in> Union(Union(r)) * Union(Union(r)). 
   835        \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"
   836 apply (rule equalityI)
   837  prefer 2 apply (blast dest: transM, clarify, simp) 
   838 apply (simp add: Pair_def) 
   839 apply (blast dest: transM) 
   840 done
   841 
   842 lemma (in M_axioms) converse_closed [intro,simp]: 
   843      "M(r) ==> M(converse(r))"
   844 apply (simp add: M_converse_iff)
   845 apply (insert converse_separation [of r], simp)
   846 done
   847 
   848 lemma (in M_axioms) converse_abs [simp]: 
   849      "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
   850 apply (simp add: is_converse_def)
   851 apply (rule iffI)
   852  prefer 2 apply blast 
   853 apply (rule M_equalityI)
   854   apply simp
   855   apply (blast dest: transM)+
   856 done
   857 
   858 
   859 subsubsection {*image, preimage, domain, range*}
   860 
   861 lemma (in M_axioms) image_closed [intro,simp]: 
   862      "[| M(A); M(r) |] ==> M(r``A)"
   863 apply (simp add: image_iff_Collect)
   864 apply (insert image_separation [of A r], simp) 
   865 done
   866 
   867 lemma (in M_axioms) vimage_abs [simp]: 
   868      "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A"
   869 apply (simp add: pre_image_def)
   870 apply (rule iffI) 
   871  apply (blast intro!: equalityI dest: transM, blast) 
   872 done
   873 
   874 lemma (in M_axioms) vimage_closed [intro,simp]: 
   875      "[| M(A); M(r) |] ==> M(r-``A)"
   876 by (simp add: vimage_def)
   877 
   878 
   879 subsubsection{*Domain, range and field*}
   880 
   881 lemma (in M_axioms) domain_abs [simp]: 
   882      "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
   883 apply (simp add: is_domain_def) 
   884 apply (blast intro!: equalityI dest: transM) 
   885 done
   886 
   887 lemma (in M_axioms) domain_closed [intro,simp]: 
   888      "M(r) ==> M(domain(r))"
   889 apply (simp add: domain_eq_vimage)
   890 done
   891 
   892 lemma (in M_axioms) range_abs [simp]: 
   893      "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
   894 apply (simp add: is_range_def)
   895 apply (blast intro!: equalityI dest: transM)
   896 done
   897 
   898 lemma (in M_axioms) range_closed [intro,simp]: 
   899      "M(r) ==> M(range(r))"
   900 apply (simp add: range_eq_image)
   901 done
   902 
   903 lemma (in M_axioms) field_abs [simp]: 
   904      "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"
   905 by (simp add: domain_closed range_closed is_field_def field_def)
   906 
   907 lemma (in M_axioms) field_closed [intro,simp]: 
   908      "M(r) ==> M(field(r))"
   909 by (simp add: domain_closed range_closed Un_closed field_def) 
   910 
   911 
   912 subsubsection{*Relations, functions and application*}
   913 
   914 lemma (in M_axioms) relation_abs [simp]: 
   915      "M(r) ==> is_relation(M,r) <-> relation(r)"
   916 apply (simp add: is_relation_def relation_def) 
   917 apply (blast dest!: bspec dest: pair_components_in_M)+
   918 done
   919 
   920 lemma (in M_axioms) function_abs [simp]: 
   921      "M(r) ==> is_function(M,r) <-> function(r)"
   922 apply (simp add: is_function_def function_def, safe) 
   923    apply (frule transM, assumption) 
   924   apply (blast dest: pair_components_in_M)+
   925 done
   926 
   927 lemma (in M_axioms) apply_closed [intro,simp]: 
   928      "[|M(f); M(a)|] ==> M(f`a)"
   929 by (simp add: apply_def)
   930 
   931 lemma (in M_axioms) apply_abs: 
   932      "[| function(f); M(f); M(y) |] 
   933       ==> fun_apply(M,f,x,y) <-> x \<in> domain(f) & f`x = y"
   934 apply (simp add: fun_apply_def)
   935 apply (blast intro: function_apply_equality function_apply_Pair) 
   936 done
   937 
   938 lemma (in M_axioms) typed_apply_abs: 
   939      "[| f \<in> A -> B; M(f); M(y) |] 
   940       ==> fun_apply(M,f,x,y) <-> x \<in> A & f`x = y"
   941 by (simp add: apply_abs fun_is_function domain_of_fun) 
   942 
   943 lemma (in M_axioms) typed_function_abs [simp]: 
   944      "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
   945 apply (auto simp add: typed_function_def relation_def Pi_iff) 
   946 apply (blast dest: pair_components_in_M)+
   947 done
   948 
   949 lemma (in M_axioms) injection_abs [simp]: 
   950      "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
   951 apply (simp add: injection_def apply_iff inj_def apply_closed)
   952 apply (blast dest: transM [of _ A]) 
   953 done
   954 
   955 lemma (in M_axioms) surjection_abs [simp]: 
   956      "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
   957 by (simp add: typed_apply_abs surjection_def surj_def)
   958 
   959 lemma (in M_axioms) bijection_abs [simp]: 
   960      "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
   961 by (simp add: bijection_def bij_def)
   962 
   963 
   964 subsubsection{*Composition of relations*}
   965 
   966 lemma (in M_axioms) M_comp_iff:
   967      "[| M(r); M(s) |] 
   968       ==> r O s = 
   969           {xz \<in> domain(s) * range(r).  
   970             \<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}"
   971 apply (simp add: comp_def)
   972 apply (rule equalityI) 
   973  apply clarify 
   974  apply simp 
   975  apply  (blast dest:  transM)+
   976 done
   977 
   978 lemma (in M_axioms) comp_closed [intro,simp]: 
   979      "[| M(r); M(s) |] ==> M(r O s)"
   980 apply (simp add: M_comp_iff)
   981 apply (insert comp_separation [of r s], simp) 
   982 done
   983 
   984 lemma (in M_axioms) composition_abs [simp]: 
   985      "[| M(r); M(s); M(t) |] 
   986       ==> composition(M,r,s,t) <-> t = r O s"
   987 apply safe
   988  txt{*Proving @{term "composition(M, r, s, r O s)"}*}
   989  prefer 2 
   990  apply (simp add: composition_def comp_def)
   991  apply (blast dest: transM) 
   992 txt{*Opposite implication*}
   993 apply (rule M_equalityI)
   994   apply (simp add: composition_def comp_def)
   995   apply (blast del: allE dest: transM)+
   996 done
   997 
   998 text{*no longer needed*}
   999 lemma (in M_axioms) restriction_is_function: 
  1000      "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
  1001       ==> function(z)"
  1002 apply (rotate_tac 1)
  1003 apply (simp add: restriction_def ball_iff_equiv) 
  1004 apply (unfold function_def, blast) 
  1005 done
  1006 
  1007 lemma (in M_axioms) restriction_abs [simp]: 
  1008      "[| M(f); M(A); M(z) |] 
  1009       ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
  1010 apply (simp add: ball_iff_equiv restriction_def restrict_def)
  1011 apply (blast intro!: equalityI dest: transM) 
  1012 done
  1013 
  1014 
  1015 lemma (in M_axioms) M_restrict_iff:
  1016      "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
  1017 by (simp add: restrict_def, blast dest: transM)
  1018 
  1019 lemma (in M_axioms) restrict_closed [intro,simp]: 
  1020      "[| M(A); M(r) |] ==> M(restrict(r,A))"
  1021 apply (simp add: M_restrict_iff)
  1022 apply (insert restrict_separation [of A], simp) 
  1023 done
  1024 
  1025 lemma (in M_axioms) Inter_abs [simp]: 
  1026      "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
  1027 apply (simp add: big_inter_def Inter_def) 
  1028 apply (blast intro!: equalityI dest: transM) 
  1029 done
  1030 
  1031 lemma (in M_axioms) Inter_closed [intro,simp]:
  1032      "M(A) ==> M(Inter(A))"
  1033 by (insert Inter_separation, simp add: Inter_def)
  1034 
  1035 lemma (in M_axioms) Int_closed [intro,simp]:
  1036      "[| M(A); M(B) |] ==> M(A Int B)"
  1037 apply (subgoal_tac "M({A,B})")
  1038 apply (frule Inter_closed, force+) 
  1039 done
  1040 
  1041 subsubsection{*Functions and function space*}
  1042 
  1043 text{*M contains all finite functions*}
  1044 lemma (in M_axioms) finite_fun_closed_lemma [rule_format]: 
  1045      "[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"
  1046 apply (induct_tac n, simp)
  1047 apply (rule ballI)  
  1048 apply (simp add: succ_def) 
  1049 apply (frule fun_cons_restrict_eq)
  1050 apply (erule ssubst) 
  1051 apply (subgoal_tac "M(f`x) & restrict(f,x) \<in> x -> A") 
  1052  apply (simp add: cons_closed nat_into_M apply_closed) 
  1053 apply (blast intro: apply_funtype transM restrict_type2) 
  1054 done
  1055 
  1056 lemma (in M_axioms) finite_fun_closed [rule_format]: 
  1057      "[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"
  1058 by (blast intro: finite_fun_closed_lemma) 
  1059 
  1060 text{*The assumption @{term "M(A->B)"} is unusual, but essential: in 
  1061 all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
  1062 lemma (in M_axioms) is_funspace_abs [simp]:
  1063      "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B";
  1064 apply (simp add: is_funspace_def)
  1065 apply (rule iffI)
  1066  prefer 2 apply blast 
  1067 apply (rule M_equalityI)
  1068   apply simp_all
  1069 done
  1070 
  1071 lemma (in M_axioms) succ_fun_eq2:
  1072      "[|M(B); M(n->B)|] ==>
  1073       succ(n) -> B = 
  1074       \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"
  1075 apply (simp add: succ_fun_eq)
  1076 apply (blast dest: transM)  
  1077 done
  1078 
  1079 lemma (in M_axioms) funspace_succ:
  1080      "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)"
  1081 apply (insert funspace_succ_replacement [of n], simp) 
  1082 apply (force simp add: succ_fun_eq2 univalent_def) 
  1083 done
  1084 
  1085 text{*@{term M} contains all finite function spaces.  Needed to prove the
  1086 absoluteness of transitive closure.*}
  1087 lemma (in M_axioms) finite_funspace_closed [intro,simp]:
  1088      "[|n\<in>nat; M(B)|] ==> M(n->B)"
  1089 apply (induct_tac n, simp)
  1090 apply (simp add: funspace_succ nat_into_M) 
  1091 done
  1092 
  1093 end