src/ZF/Constructible/Relative.thy
author paulson
Fri Jul 12 16:41:39 2002 +0200 (2002-07-12)
changeset 13353 1800e7134d2e
parent 13352 3cd767f8d78b
child 13363 c26eeb000470
permissions -rw-r--r--
towards relativization of "iterates" and "wfrec"
     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_sum :: "[i=>o,i,i,i] => o"
    53     "is_sum(M,A,B,Z) == 
    54        \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M]. 
    55        number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
    56        cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"
    57 
    58   is_converse :: "[i=>o,i,i] => o"
    59     "is_converse(M,r,z) == 
    60 	\<forall>x[M]. x \<in> z <-> 
    61              (\<exists>w[M]. w\<in>r & (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x)))"
    62 
    63   pre_image :: "[i=>o,i,i,i] => o"
    64     "pre_image(M,r,A,z) == 
    65 	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))"
    66 
    67   is_domain :: "[i=>o,i,i] => o"
    68     "is_domain(M,r,z) == 
    69 	\<forall>x[M]. (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))"
    70 
    71   image :: "[i=>o,i,i,i] => o"
    72     "image(M,r,A,z) == 
    73         \<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))"
    74 
    75   is_range :: "[i=>o,i,i] => o"
    76     --{*the cleaner 
    77       @{term "\<exists>r'[M]. is_converse(M,r,r') & is_domain(M,r',z)"}
    78       unfortunately needs an instance of separation in order to prove 
    79         @{term "M(converse(r))"}.*}
    80     "is_range(M,r,z) == 
    81 	\<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))"
    82 
    83   is_field :: "[i=>o,i,i] => o"
    84     "is_field(M,r,z) == 
    85 	\<exists>dr[M]. is_domain(M,r,dr) & 
    86             (\<exists>rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))"
    87 
    88   is_relation :: "[i=>o,i] => o"
    89     "is_relation(M,r) == 
    90         (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))"
    91 
    92   is_function :: "[i=>o,i] => o"
    93     "is_function(M,r) == 
    94 	\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M]. 
    95            pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'"
    96 
    97   fun_apply :: "[i=>o,i,i,i] => o"
    98     "fun_apply(M,f,x,y) == 
    99         (\<exists>xs[M]. \<exists>fxs[M]. 
   100          upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))"
   101 
   102   typed_function :: "[i=>o,i,i,i] => o"
   103     "typed_function(M,A,B,r) == 
   104         is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
   105         (\<forall>u[M]. u\<in>r --> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) --> y\<in>B))"
   106 
   107   is_funspace :: "[i=>o,i,i,i] => o"
   108     "is_funspace(M,A,B,F) == 
   109         \<forall>f[M]. f \<in> F <-> typed_function(M,A,B,f)"
   110 
   111   composition :: "[i=>o,i,i,i] => o"
   112     "composition(M,r,s,t) == 
   113         \<forall>p[M]. p \<in> t <-> 
   114                (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
   115                 pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
   116                 xy \<in> s & yz \<in> r)"
   117 
   118   injection :: "[i=>o,i,i,i] => o"
   119     "injection(M,A,B,f) == 
   120 	typed_function(M,A,B,f) &
   121         (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M]. 
   122           pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> x=x')"
   123 
   124   surjection :: "[i=>o,i,i,i] => o"
   125     "surjection(M,A,B,f) == 
   126         typed_function(M,A,B,f) &
   127         (\<forall>y[M]. y\<in>B --> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))"
   128 
   129   bijection :: "[i=>o,i,i,i] => o"
   130     "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)"
   131 
   132   restriction :: "[i=>o,i,i,i] => o"
   133     "restriction(M,r,A,z) == 
   134 	\<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))"
   135 
   136   transitive_set :: "[i=>o,i] => o"
   137     "transitive_set(M,a) == \<forall>x[M]. x\<in>a --> subset(M,x,a)"
   138 
   139   ordinal :: "[i=>o,i] => o"
   140      --{*an ordinal is a transitive set of transitive sets*}
   141     "ordinal(M,a) == transitive_set(M,a) & (\<forall>x[M]. x\<in>a --> transitive_set(M,x))"
   142 
   143   limit_ordinal :: "[i=>o,i] => o"
   144     --{*a limit ordinal is a non-empty, successor-closed ordinal*}
   145     "limit_ordinal(M,a) == 
   146 	ordinal(M,a) & ~ empty(M,a) & 
   147         (\<forall>x[M]. x\<in>a --> (\<exists>y[M]. y\<in>a & successor(M,x,y)))"
   148 
   149   successor_ordinal :: "[i=>o,i] => o"
   150     --{*a successor ordinal is any ordinal that is neither empty nor limit*}
   151     "successor_ordinal(M,a) == 
   152 	ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)"
   153 
   154   finite_ordinal :: "[i=>o,i] => o"
   155     --{*an ordinal is finite if neither it nor any of its elements are limit*}
   156     "finite_ordinal(M,a) == 
   157 	ordinal(M,a) & ~ limit_ordinal(M,a) & 
   158         (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
   159 
   160   omega :: "[i=>o,i] => o"
   161     --{*omega is a limit ordinal none of whose elements are limit*}
   162     "omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
   163 
   164   number1 :: "[i=>o,i] => o"
   165     "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))"
   166 
   167   number2 :: "[i=>o,i] => o"
   168     "number2(M,a) == (\<exists>x[M]. number1(M,x) & successor(M,x,a))"
   169 
   170   number3 :: "[i=>o,i] => o"
   171     "number3(M,a) == (\<exists>x[M]. number2(M,x) & successor(M,x,a))"
   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) | z=0)"
   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 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 (*Needed?  surely better to replace is_nat_case by nat_case?*)
   673 lemma (in M_triv_axioms) is_nat_case_cong [cong]:
   674      "[| a = a'; k = k';  z = z';  M(z');
   675        !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
   676       ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"
   677 by (simp add: is_nat_case_def) 
   678 
   679 lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
   680      "M(Inl(a)) <-> M(a)"
   681 by (simp add: Inl_def) 
   682 
   683 lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
   684      "M(Inr(a)) <-> M(a)"
   685 by (simp add: Inr_def)
   686 
   687 
   688 subsection{*Absoluteness for ordinals*}
   689 text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
   690 
   691 lemma (in M_triv_axioms) lt_closed:
   692      "[| j<i; M(i) |] ==> M(j)" 
   693 by (blast dest: ltD intro: transM) 
   694 
   695 lemma (in M_triv_axioms) transitive_set_abs [simp]: 
   696      "M(a) ==> transitive_set(M,a) <-> Transset(a)"
   697 by (simp add: transitive_set_def Transset_def)
   698 
   699 lemma (in M_triv_axioms) ordinal_abs [simp]: 
   700      "M(a) ==> ordinal(M,a) <-> Ord(a)"
   701 by (simp add: ordinal_def Ord_def)
   702 
   703 lemma (in M_triv_axioms) limit_ordinal_abs [simp]: 
   704      "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
   705 apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def) 
   706 apply (simp add: lt_def, blast) 
   707 done
   708 
   709 lemma (in M_triv_axioms) successor_ordinal_abs [simp]: 
   710      "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b[M]. a = succ(b))"
   711 apply (simp add: successor_ordinal_def, safe)
   712 apply (drule Ord_cases_disj, auto) 
   713 done
   714 
   715 lemma finite_Ord_is_nat:
   716       "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"
   717 by (induct a rule: trans_induct3, simp_all)
   718 
   719 lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
   720 by (induct a rule: nat_induct, auto)
   721 
   722 lemma (in M_triv_axioms) finite_ordinal_abs [simp]: 
   723      "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
   724 apply (simp add: finite_ordinal_def)
   725 apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord 
   726              dest: Ord_trans naturals_not_limit)
   727 done
   728 
   729 lemma Limit_non_Limit_implies_nat:
   730      "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"
   731 apply (rule le_anti_sym) 
   732 apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)  
   733  apply (simp add: lt_def)  
   734  apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) 
   735 apply (erule nat_le_Limit)
   736 done
   737 
   738 lemma (in M_triv_axioms) omega_abs [simp]: 
   739      "M(a) ==> omega(M,a) <-> a = nat"
   740 apply (simp add: omega_def) 
   741 apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
   742 done
   743 
   744 lemma (in M_triv_axioms) number1_abs [simp]: 
   745      "M(a) ==> number1(M,a) <-> a = 1"
   746 by (simp add: number1_def) 
   747 
   748 lemma (in M_triv_axioms) number1_abs [simp]: 
   749      "M(a) ==> number2(M,a) <-> a = succ(1)"
   750 by (simp add: number2_def) 
   751 
   752 lemma (in M_triv_axioms) number3_abs [simp]: 
   753      "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
   754 by (simp add: number3_def) 
   755 
   756 text{*Kunen continued to 20...*}
   757 
   758 (*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything 
   759   but the recursion variable must stay unchanged.  But then the recursion
   760   equations only hold for x\<in>nat (or in some other set) and not for the 
   761   whole of the class M.
   762   consts
   763     natnumber_aux :: "[i=>o,i] => i"
   764 
   765   primrec
   766       "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
   767       "natnumber_aux(M,succ(n)) = 
   768 	   (\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x)) 
   769 		     then 1 else 0)"
   770 
   771   constdefs
   772     natnumber :: "[i=>o,i,i] => o"
   773       "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
   774 
   775   lemma (in M_triv_axioms) [simp]: 
   776        "natnumber(M,0,x) == x=0"
   777 *)
   778 
   779 subsection{*Some instances of separation and strong replacement*}
   780 
   781 locale M_axioms = M_triv_axioms +
   782 assumes Inter_separation:
   783      "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
   784   and cartprod_separation:
   785      "[| M(A); M(B) |] 
   786       ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,z)))"
   787   and image_separation:
   788      "[| M(A); M(r) |] 
   789       ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,p)))"
   790   and converse_separation:
   791      "M(r) ==> separation(M, 
   792          \<lambda>z. \<exists>p[M]. p\<in>r & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
   793   and restrict_separation:
   794      "M(A) ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. pair(M,x,y,z)))"
   795   and comp_separation:
   796      "[| M(r); M(s) |]
   797       ==> separation(M, \<lambda>xz. \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
   798 		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
   799                   xy\<in>s & yz\<in>r)"
   800   and pred_separation:
   801      "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & pair(M,y,x,p))"
   802   and Memrel_separation:
   803      "separation(M, \<lambda>z. \<exists>x[M]. \<exists>y[M]. pair(M,x,y,z) & x \<in> y)"
   804   and funspace_succ_replacement:
   805      "M(n) ==> 
   806       strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. \<exists>cnbf[M]. 
   807                 pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &
   808                 upair(M,cnbf,cnbf,z))"
   809   and well_ord_iso_separation:
   810      "[| M(A); M(f); M(r) |] 
   811       ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y[M]. (\<exists>p[M]. 
   812 		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
   813   and obase_separation:
   814      --{*part of the order type formalization*}
   815      "[| M(A); M(r) |] 
   816       ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
   817 	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
   818 	     order_isomorphism(M,par,r,x,mx,g))"
   819   and obase_equals_separation:
   820      "[| M(A); M(r) |] 
   821       ==> separation (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M]. 
   822 			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M]. 
   823 			      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
   824 			      order_isomorphism(M,pxr,r,y,my,g))))"
   825   and omap_replacement:
   826      "[| M(A); M(r) |] 
   827       ==> strong_replacement(M,
   828              \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
   829 	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
   830 	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
   831   and is_recfun_separation:
   832      --{*for well-founded recursion*}
   833      "[| M(r); M(f); M(g); M(a); M(b) |] 
   834      ==> separation(M, 
   835             \<lambda>x. \<exists>xa[M]. \<exists>xb[M]. 
   836                 pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r & 
   837                 (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) & 
   838                                    fx \<noteq> gx))"
   839 
   840 lemma (in M_axioms) cartprod_iff_lemma:
   841      "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
   842          powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
   843        ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
   844 apply (simp add: powerset_def) 
   845 apply (rule equalityI, clarify, simp)
   846  apply (frule transM, assumption) 
   847  apply (frule transM, assumption, simp) 
   848  apply blast 
   849 apply clarify
   850 apply (frule transM, assumption, force) 
   851 done
   852 
   853 lemma (in M_axioms) cartprod_iff:
   854      "[| M(A); M(B); M(C) |] 
   855       ==> cartprod(M,A,B,C) <-> 
   856           (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &
   857                    C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
   858 apply (simp add: Pair_def cartprod_def, safe)
   859 defer 1 
   860   apply (simp add: powerset_def) 
   861  apply blast 
   862 txt{*Final, difficult case: the left-to-right direction of the theorem.*}
   863 apply (insert power_ax, simp add: power_ax_def) 
   864 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   865 apply (blast, clarify) 
   866 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)
   867 apply assumption
   868 apply (blast intro: cartprod_iff_lemma) 
   869 done
   870 
   871 lemma (in M_axioms) cartprod_closed_lemma:
   872      "[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
   873 apply (simp del: cartprod_abs add: cartprod_iff)
   874 apply (insert power_ax, simp add: power_ax_def) 
   875 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   876 apply (blast, clarify) 
   877 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   878 apply (blast, clarify)
   879 apply (intro rexI exI conjI) 
   880 prefer 5 apply (rule refl) 
   881 prefer 3 apply assumption
   882 prefer 3 apply assumption
   883 apply (insert cartprod_separation [of A B], auto)
   884 done
   885 
   886 text{*All the lemmas above are necessary because Powerset is not absolute.
   887       I should have used Replacement instead!*}
   888 lemma (in M_axioms) cartprod_closed [intro,simp]: 
   889      "[| M(A); M(B) |] ==> M(A*B)"
   890 by (frule cartprod_closed_lemma, assumption, force)
   891 
   892 lemma (in M_axioms) sum_closed [intro,simp]: 
   893      "[| M(A); M(B) |] ==> M(A+B)"
   894 by (simp add: sum_def)
   895 
   896 lemma (in M_axioms) sum_abs [simp]:
   897      "[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) <-> (Z = A+B)"
   898 by (simp add: is_sum_def sum_def singleton_0 nat_into_M)
   899 
   900 
   901 subsubsection {*converse of a relation*}
   902 
   903 lemma (in M_axioms) M_converse_iff:
   904      "M(r) ==> 
   905       converse(r) = 
   906       {z \<in> Union(Union(r)) * Union(Union(r)). 
   907        \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"
   908 apply (rule equalityI)
   909  prefer 2 apply (blast dest: transM, clarify, simp) 
   910 apply (simp add: Pair_def) 
   911 apply (blast dest: transM) 
   912 done
   913 
   914 lemma (in M_axioms) converse_closed [intro,simp]: 
   915      "M(r) ==> M(converse(r))"
   916 apply (simp add: M_converse_iff)
   917 apply (insert converse_separation [of r], simp)
   918 done
   919 
   920 lemma (in M_axioms) converse_abs [simp]: 
   921      "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
   922 apply (simp add: is_converse_def)
   923 apply (rule iffI)
   924  prefer 2 apply blast 
   925 apply (rule M_equalityI)
   926   apply simp
   927   apply (blast dest: transM)+
   928 done
   929 
   930 
   931 subsubsection {*image, preimage, domain, range*}
   932 
   933 lemma (in M_axioms) image_closed [intro,simp]: 
   934      "[| M(A); M(r) |] ==> M(r``A)"
   935 apply (simp add: image_iff_Collect)
   936 apply (insert image_separation [of A r], simp) 
   937 done
   938 
   939 lemma (in M_axioms) vimage_abs [simp]: 
   940      "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A"
   941 apply (simp add: pre_image_def)
   942 apply (rule iffI) 
   943  apply (blast intro!: equalityI dest: transM, blast) 
   944 done
   945 
   946 lemma (in M_axioms) vimage_closed [intro,simp]: 
   947      "[| M(A); M(r) |] ==> M(r-``A)"
   948 by (simp add: vimage_def)
   949 
   950 
   951 subsubsection{*Domain, range and field*}
   952 
   953 lemma (in M_axioms) domain_abs [simp]: 
   954      "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
   955 apply (simp add: is_domain_def) 
   956 apply (blast intro!: equalityI dest: transM) 
   957 done
   958 
   959 lemma (in M_axioms) domain_closed [intro,simp]: 
   960      "M(r) ==> M(domain(r))"
   961 apply (simp add: domain_eq_vimage)
   962 done
   963 
   964 lemma (in M_axioms) range_abs [simp]: 
   965      "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
   966 apply (simp add: is_range_def)
   967 apply (blast intro!: equalityI dest: transM)
   968 done
   969 
   970 lemma (in M_axioms) range_closed [intro,simp]: 
   971      "M(r) ==> M(range(r))"
   972 apply (simp add: range_eq_image)
   973 done
   974 
   975 lemma (in M_axioms) field_abs [simp]: 
   976      "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"
   977 by (simp add: domain_closed range_closed is_field_def field_def)
   978 
   979 lemma (in M_axioms) field_closed [intro,simp]: 
   980      "M(r) ==> M(field(r))"
   981 by (simp add: domain_closed range_closed Un_closed field_def) 
   982 
   983 
   984 subsubsection{*Relations, functions and application*}
   985 
   986 lemma (in M_axioms) relation_abs [simp]: 
   987      "M(r) ==> is_relation(M,r) <-> relation(r)"
   988 apply (simp add: is_relation_def relation_def) 
   989 apply (blast dest!: bspec dest: pair_components_in_M)+
   990 done
   991 
   992 lemma (in M_axioms) function_abs [simp]: 
   993      "M(r) ==> is_function(M,r) <-> function(r)"
   994 apply (simp add: is_function_def function_def, safe) 
   995    apply (frule transM, assumption) 
   996   apply (blast dest: pair_components_in_M)+
   997 done
   998 
   999 lemma (in M_axioms) apply_closed [intro,simp]: 
  1000      "[|M(f); M(a)|] ==> M(f`a)"
  1001 by (simp add: apply_def)
  1002 
  1003 lemma (in M_axioms) apply_abs [simp]: 
  1004      "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> f`x = y"
  1005 apply (simp add: fun_apply_def apply_def, blast) 
  1006 done
  1007 
  1008 lemma (in M_axioms) typed_function_abs [simp]: 
  1009      "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
  1010 apply (auto simp add: typed_function_def relation_def Pi_iff) 
  1011 apply (blast dest: pair_components_in_M)+
  1012 done
  1013 
  1014 lemma (in M_axioms) injection_abs [simp]: 
  1015      "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
  1016 apply (simp add: injection_def apply_iff inj_def apply_closed)
  1017 apply (blast dest: transM [of _ A]) 
  1018 done
  1019 
  1020 lemma (in M_axioms) surjection_abs [simp]: 
  1021      "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
  1022 by (simp add: surjection_def surj_def)
  1023 
  1024 lemma (in M_axioms) bijection_abs [simp]: 
  1025      "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
  1026 by (simp add: bijection_def bij_def)
  1027 
  1028 
  1029 subsubsection{*Composition of relations*}
  1030 
  1031 lemma (in M_axioms) M_comp_iff:
  1032      "[| M(r); M(s) |] 
  1033       ==> r O s = 
  1034           {xz \<in> domain(s) * range(r).  
  1035             \<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}"
  1036 apply (simp add: comp_def)
  1037 apply (rule equalityI) 
  1038  apply clarify 
  1039  apply simp 
  1040  apply  (blast dest:  transM)+
  1041 done
  1042 
  1043 lemma (in M_axioms) comp_closed [intro,simp]: 
  1044      "[| M(r); M(s) |] ==> M(r O s)"
  1045 apply (simp add: M_comp_iff)
  1046 apply (insert comp_separation [of r s], simp) 
  1047 done
  1048 
  1049 lemma (in M_axioms) composition_abs [simp]: 
  1050      "[| M(r); M(s); M(t) |] 
  1051       ==> composition(M,r,s,t) <-> t = r O s"
  1052 apply safe
  1053  txt{*Proving @{term "composition(M, r, s, r O s)"}*}
  1054  prefer 2 
  1055  apply (simp add: composition_def comp_def)
  1056  apply (blast dest: transM) 
  1057 txt{*Opposite implication*}
  1058 apply (rule M_equalityI)
  1059   apply (simp add: composition_def comp_def)
  1060   apply (blast del: allE dest: transM)+
  1061 done
  1062 
  1063 text{*no longer needed*}
  1064 lemma (in M_axioms) restriction_is_function: 
  1065      "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
  1066       ==> function(z)"
  1067 apply (rotate_tac 1)
  1068 apply (simp add: restriction_def ball_iff_equiv) 
  1069 apply (unfold function_def, blast) 
  1070 done
  1071 
  1072 lemma (in M_axioms) restriction_abs [simp]: 
  1073      "[| M(f); M(A); M(z) |] 
  1074       ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
  1075 apply (simp add: ball_iff_equiv restriction_def restrict_def)
  1076 apply (blast intro!: equalityI dest: transM) 
  1077 done
  1078 
  1079 
  1080 lemma (in M_axioms) M_restrict_iff:
  1081      "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
  1082 by (simp add: restrict_def, blast dest: transM)
  1083 
  1084 lemma (in M_axioms) restrict_closed [intro,simp]: 
  1085      "[| M(A); M(r) |] ==> M(restrict(r,A))"
  1086 apply (simp add: M_restrict_iff)
  1087 apply (insert restrict_separation [of A], simp) 
  1088 done
  1089 
  1090 lemma (in M_axioms) Inter_abs [simp]: 
  1091      "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
  1092 apply (simp add: big_inter_def Inter_def) 
  1093 apply (blast intro!: equalityI dest: transM) 
  1094 done
  1095 
  1096 lemma (in M_axioms) Inter_closed [intro,simp]:
  1097      "M(A) ==> M(Inter(A))"
  1098 by (insert Inter_separation, simp add: Inter_def)
  1099 
  1100 lemma (in M_axioms) Int_closed [intro,simp]:
  1101      "[| M(A); M(B) |] ==> M(A Int B)"
  1102 apply (subgoal_tac "M({A,B})")
  1103 apply (frule Inter_closed, force+) 
  1104 done
  1105 
  1106 subsubsection{*Functions and function space*}
  1107 
  1108 text{*M contains all finite functions*}
  1109 lemma (in M_axioms) finite_fun_closed_lemma [rule_format]: 
  1110      "[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"
  1111 apply (induct_tac n, simp)
  1112 apply (rule ballI)  
  1113 apply (simp add: succ_def) 
  1114 apply (frule fun_cons_restrict_eq)
  1115 apply (erule ssubst) 
  1116 apply (subgoal_tac "M(f`x) & restrict(f,x) \<in> x -> A") 
  1117  apply (simp add: cons_closed nat_into_M apply_closed) 
  1118 apply (blast intro: apply_funtype transM restrict_type2) 
  1119 done
  1120 
  1121 lemma (in M_axioms) finite_fun_closed [rule_format]: 
  1122      "[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"
  1123 by (blast intro: finite_fun_closed_lemma) 
  1124 
  1125 text{*The assumption @{term "M(A->B)"} is unusual, but essential: in 
  1126 all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
  1127 lemma (in M_axioms) is_funspace_abs [simp]:
  1128      "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B";
  1129 apply (simp add: is_funspace_def)
  1130 apply (rule iffI)
  1131  prefer 2 apply blast 
  1132 apply (rule M_equalityI)
  1133   apply simp_all
  1134 done
  1135 
  1136 lemma (in M_axioms) succ_fun_eq2:
  1137      "[|M(B); M(n->B)|] ==>
  1138       succ(n) -> B = 
  1139       \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"
  1140 apply (simp add: succ_fun_eq)
  1141 apply (blast dest: transM)  
  1142 done
  1143 
  1144 lemma (in M_axioms) funspace_succ:
  1145      "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)"
  1146 apply (insert funspace_succ_replacement [of n], simp) 
  1147 apply (force simp add: succ_fun_eq2 univalent_def) 
  1148 done
  1149 
  1150 text{*@{term M} contains all finite function spaces.  Needed to prove the
  1151 absoluteness of transitive closure.*}
  1152 lemma (in M_axioms) finite_funspace_closed [intro,simp]:
  1153      "[|n\<in>nat; M(B)|] ==> M(n->B)"
  1154 apply (induct_tac n, simp)
  1155 apply (simp add: funspace_succ nat_into_M) 
  1156 done
  1157 
  1158 
  1159 end