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