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