src/ZF/Constructible/Relative.thy
author paulson
Tue Jul 09 10:44:53 2002 +0200 (2002-07-09)
changeset 13319 23de7b3af453
parent 13316 d16629fd0f95
child 13323 2c287f50c9f3
permissions -rw-r--r--
More 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 (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M]. 
   757 			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M]. 
   758 			      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
   759 			      order_isomorphism(M,pxr,r,y,my,g))))"
   760   and omap_replacement:
   761      "[| M(A); M(r) |] 
   762       ==> strong_replacement(M,
   763              \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
   764 	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
   765 	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
   766   and is_recfun_separation:
   767      --{*for well-founded recursion*}
   768      "[| M(r); M(f); M(g); M(a); M(b) |] 
   769      ==> separation(M, 
   770             \<lambda>x. \<exists>xa[M]. \<exists>xb[M]. 
   771                 pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r & 
   772                 (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) & 
   773                                    fx \<noteq> gx))"
   774 
   775 lemma (in M_axioms) cartprod_iff_lemma:
   776      "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
   777          powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
   778        ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
   779 apply (simp add: powerset_def) 
   780 apply (rule equalityI, clarify, simp)
   781  apply (frule transM, assumption) 
   782  apply (frule transM, assumption, simp) 
   783  apply blast 
   784 apply clarify
   785 apply (frule transM, assumption, force) 
   786 done
   787 
   788 lemma (in M_axioms) cartprod_iff:
   789      "[| M(A); M(B); M(C) |] 
   790       ==> cartprod(M,A,B,C) <-> 
   791           (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &
   792                    C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
   793 apply (simp add: Pair_def cartprod_def, safe)
   794 defer 1 
   795   apply (simp add: powerset_def) 
   796  apply blast 
   797 txt{*Final, difficult case: the left-to-right direction of the theorem.*}
   798 apply (insert power_ax, simp add: power_ax_def) 
   799 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   800 apply (blast, clarify) 
   801 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)
   802 apply assumption
   803 apply (blast intro: cartprod_iff_lemma) 
   804 done
   805 
   806 lemma (in M_axioms) cartprod_closed_lemma:
   807      "[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
   808 apply (simp del: cartprod_abs add: cartprod_iff)
   809 apply (insert power_ax, simp add: power_ax_def) 
   810 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   811 apply (blast, clarify) 
   812 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   813 apply (blast, clarify)
   814 apply (intro rexI exI conjI) 
   815 prefer 5 apply (rule refl) 
   816 prefer 3 apply assumption
   817 prefer 3 apply assumption
   818 apply (insert cartprod_separation [of A B], auto)
   819 done
   820 
   821 text{*All the lemmas above are necessary because Powerset is not absolute.
   822       I should have used Replacement instead!*}
   823 lemma (in M_axioms) cartprod_closed [intro,simp]: 
   824      "[| M(A); M(B) |] ==> M(A*B)"
   825 by (frule cartprod_closed_lemma, assumption, force)
   826 
   827 lemma (in M_axioms) sum_closed [intro,simp]: 
   828      "[| M(A); M(B) |] ==> M(A+B)"
   829 by (simp add: sum_def)
   830 
   831 
   832 subsubsection {*converse of a relation*}
   833 
   834 lemma (in M_axioms) M_converse_iff:
   835      "M(r) ==> 
   836       converse(r) = 
   837       {z \<in> Union(Union(r)) * Union(Union(r)). 
   838        \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"
   839 apply (rule equalityI)
   840  prefer 2 apply (blast dest: transM, clarify, simp) 
   841 apply (simp add: Pair_def) 
   842 apply (blast dest: transM) 
   843 done
   844 
   845 lemma (in M_axioms) converse_closed [intro,simp]: 
   846      "M(r) ==> M(converse(r))"
   847 apply (simp add: M_converse_iff)
   848 apply (insert converse_separation [of r], simp)
   849 done
   850 
   851 lemma (in M_axioms) converse_abs [simp]: 
   852      "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
   853 apply (simp add: is_converse_def)
   854 apply (rule iffI)
   855  prefer 2 apply blast 
   856 apply (rule M_equalityI)
   857   apply simp
   858   apply (blast dest: transM)+
   859 done
   860 
   861 
   862 subsubsection {*image, preimage, domain, range*}
   863 
   864 lemma (in M_axioms) image_closed [intro,simp]: 
   865      "[| M(A); M(r) |] ==> M(r``A)"
   866 apply (simp add: image_iff_Collect)
   867 apply (insert image_separation [of A r], simp) 
   868 done
   869 
   870 lemma (in M_axioms) vimage_abs [simp]: 
   871      "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A"
   872 apply (simp add: pre_image_def)
   873 apply (rule iffI) 
   874  apply (blast intro!: equalityI dest: transM, blast) 
   875 done
   876 
   877 lemma (in M_axioms) vimage_closed [intro,simp]: 
   878      "[| M(A); M(r) |] ==> M(r-``A)"
   879 by (simp add: vimage_def)
   880 
   881 
   882 subsubsection{*Domain, range and field*}
   883 
   884 lemma (in M_axioms) domain_abs [simp]: 
   885      "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
   886 apply (simp add: is_domain_def) 
   887 apply (blast intro!: equalityI dest: transM) 
   888 done
   889 
   890 lemma (in M_axioms) domain_closed [intro,simp]: 
   891      "M(r) ==> M(domain(r))"
   892 apply (simp add: domain_eq_vimage)
   893 done
   894 
   895 lemma (in M_axioms) range_abs [simp]: 
   896      "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
   897 apply (simp add: is_range_def)
   898 apply (blast intro!: equalityI dest: transM)
   899 done
   900 
   901 lemma (in M_axioms) range_closed [intro,simp]: 
   902      "M(r) ==> M(range(r))"
   903 apply (simp add: range_eq_image)
   904 done
   905 
   906 lemma (in M_axioms) field_abs [simp]: 
   907      "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"
   908 by (simp add: domain_closed range_closed is_field_def field_def)
   909 
   910 lemma (in M_axioms) field_closed [intro,simp]: 
   911      "M(r) ==> M(field(r))"
   912 by (simp add: domain_closed range_closed Un_closed field_def) 
   913 
   914 
   915 subsubsection{*Relations, functions and application*}
   916 
   917 lemma (in M_axioms) relation_abs [simp]: 
   918      "M(r) ==> is_relation(M,r) <-> relation(r)"
   919 apply (simp add: is_relation_def relation_def) 
   920 apply (blast dest!: bspec dest: pair_components_in_M)+
   921 done
   922 
   923 lemma (in M_axioms) function_abs [simp]: 
   924      "M(r) ==> is_function(M,r) <-> function(r)"
   925 apply (simp add: is_function_def function_def, safe) 
   926    apply (frule transM, assumption) 
   927   apply (blast dest: pair_components_in_M)+
   928 done
   929 
   930 lemma (in M_axioms) apply_closed [intro,simp]: 
   931      "[|M(f); M(a)|] ==> M(f`a)"
   932 by (simp add: apply_def)
   933 
   934 lemma (in M_axioms) apply_abs: 
   935      "[| function(f); M(f); M(y) |] 
   936       ==> fun_apply(M,f,x,y) <-> x \<in> domain(f) & f`x = y"
   937 apply (simp add: fun_apply_def)
   938 apply (blast intro: function_apply_equality function_apply_Pair) 
   939 done
   940 
   941 lemma (in M_axioms) typed_apply_abs: 
   942      "[| f \<in> A -> B; M(f); M(y) |] 
   943       ==> fun_apply(M,f,x,y) <-> x \<in> A & f`x = y"
   944 by (simp add: apply_abs fun_is_function domain_of_fun) 
   945 
   946 lemma (in M_axioms) typed_function_abs [simp]: 
   947      "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
   948 apply (auto simp add: typed_function_def relation_def Pi_iff) 
   949 apply (blast dest: pair_components_in_M)+
   950 done
   951 
   952 lemma (in M_axioms) injection_abs [simp]: 
   953      "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
   954 apply (simp add: injection_def apply_iff inj_def apply_closed)
   955 apply (blast dest: transM [of _ A]) 
   956 done
   957 
   958 lemma (in M_axioms) surjection_abs [simp]: 
   959      "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
   960 by (simp add: typed_apply_abs surjection_def surj_def)
   961 
   962 lemma (in M_axioms) bijection_abs [simp]: 
   963      "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
   964 by (simp add: bijection_def bij_def)
   965 
   966 
   967 subsubsection{*Composition of relations*}
   968 
   969 lemma (in M_axioms) M_comp_iff:
   970      "[| M(r); M(s) |] 
   971       ==> r O s = 
   972           {xz \<in> domain(s) * range(r).  
   973             \<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}"
   974 apply (simp add: comp_def)
   975 apply (rule equalityI) 
   976  apply clarify 
   977  apply simp 
   978  apply  (blast dest:  transM)+
   979 done
   980 
   981 lemma (in M_axioms) comp_closed [intro,simp]: 
   982      "[| M(r); M(s) |] ==> M(r O s)"
   983 apply (simp add: M_comp_iff)
   984 apply (insert comp_separation [of r s], simp) 
   985 done
   986 
   987 lemma (in M_axioms) composition_abs [simp]: 
   988      "[| M(r); M(s); M(t) |] 
   989       ==> composition(M,r,s,t) <-> t = r O s"
   990 apply safe
   991  txt{*Proving @{term "composition(M, r, s, r O s)"}*}
   992  prefer 2 
   993  apply (simp add: composition_def comp_def)
   994  apply (blast dest: transM) 
   995 txt{*Opposite implication*}
   996 apply (rule M_equalityI)
   997   apply (simp add: composition_def comp_def)
   998   apply (blast del: allE dest: transM)+
   999 done
  1000 
  1001 text{*no longer needed*}
  1002 lemma (in M_axioms) restriction_is_function: 
  1003      "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
  1004       ==> function(z)"
  1005 apply (rotate_tac 1)
  1006 apply (simp add: restriction_def ball_iff_equiv) 
  1007 apply (unfold function_def, blast) 
  1008 done
  1009 
  1010 lemma (in M_axioms) restriction_abs [simp]: 
  1011      "[| M(f); M(A); M(z) |] 
  1012       ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
  1013 apply (simp add: ball_iff_equiv restriction_def restrict_def)
  1014 apply (blast intro!: equalityI dest: transM) 
  1015 done
  1016 
  1017 
  1018 lemma (in M_axioms) M_restrict_iff:
  1019      "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
  1020 by (simp add: restrict_def, blast dest: transM)
  1021 
  1022 lemma (in M_axioms) restrict_closed [intro,simp]: 
  1023      "[| M(A); M(r) |] ==> M(restrict(r,A))"
  1024 apply (simp add: M_restrict_iff)
  1025 apply (insert restrict_separation [of A], simp) 
  1026 done
  1027 
  1028 lemma (in M_axioms) Inter_abs [simp]: 
  1029      "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
  1030 apply (simp add: big_inter_def Inter_def) 
  1031 apply (blast intro!: equalityI dest: transM) 
  1032 done
  1033 
  1034 lemma (in M_axioms) Inter_closed [intro,simp]:
  1035      "M(A) ==> M(Inter(A))"
  1036 by (insert Inter_separation, simp add: Inter_def)
  1037 
  1038 lemma (in M_axioms) Int_closed [intro,simp]:
  1039      "[| M(A); M(B) |] ==> M(A Int B)"
  1040 apply (subgoal_tac "M({A,B})")
  1041 apply (frule Inter_closed, force+) 
  1042 done
  1043 
  1044 subsubsection{*Functions and function space*}
  1045 
  1046 text{*M contains all finite functions*}
  1047 lemma (in M_axioms) finite_fun_closed_lemma [rule_format]: 
  1048      "[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"
  1049 apply (induct_tac n, simp)
  1050 apply (rule ballI)  
  1051 apply (simp add: succ_def) 
  1052 apply (frule fun_cons_restrict_eq)
  1053 apply (erule ssubst) 
  1054 apply (subgoal_tac "M(f`x) & restrict(f,x) \<in> x -> A") 
  1055  apply (simp add: cons_closed nat_into_M apply_closed) 
  1056 apply (blast intro: apply_funtype transM restrict_type2) 
  1057 done
  1058 
  1059 lemma (in M_axioms) finite_fun_closed [rule_format]: 
  1060      "[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"
  1061 by (blast intro: finite_fun_closed_lemma) 
  1062 
  1063 text{*The assumption @{term "M(A->B)"} is unusual, but essential: in 
  1064 all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
  1065 lemma (in M_axioms) is_funspace_abs [simp]:
  1066      "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B";
  1067 apply (simp add: is_funspace_def)
  1068 apply (rule iffI)
  1069  prefer 2 apply blast 
  1070 apply (rule M_equalityI)
  1071   apply simp_all
  1072 done
  1073 
  1074 lemma (in M_axioms) succ_fun_eq2:
  1075      "[|M(B); M(n->B)|] ==>
  1076       succ(n) -> B = 
  1077       \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"
  1078 apply (simp add: succ_fun_eq)
  1079 apply (blast dest: transM)  
  1080 done
  1081 
  1082 lemma (in M_axioms) funspace_succ:
  1083      "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)"
  1084 apply (insert funspace_succ_replacement [of n], simp) 
  1085 apply (force simp add: succ_fun_eq2 univalent_def) 
  1086 done
  1087 
  1088 text{*@{term M} contains all finite function spaces.  Needed to prove the
  1089 absoluteness of transitive closure.*}
  1090 lemma (in M_axioms) finite_funspace_closed [intro,simp]:
  1091      "[|n\<in>nat; M(B)|] ==> M(n->B)"
  1092 apply (induct_tac n, simp)
  1093 apply (simp add: funspace_succ nat_into_M) 
  1094 done
  1095 
  1096 end