src/ZF/Constructible/Relative.thy
 author paulson Thu Jul 04 10:51:52 2002 +0200 (2002-07-04) changeset 13290 28ce81eff3de parent 13269 3ba9be497c33 child 13298 b4f370679c65 permissions -rw-r--r--
separation of M_axioms into M_triv_axioms and M_axioms
     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\<in>A. M(x) --> 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\<in>z. M(x) --> 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   union :: "[i=>o,i,i,i] => o"

    22     "union(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a | x \<in> b"

    23

    24   successor :: "[i=>o,i,i] => o"

    25     "successor(M,a,z) == \<exists>x[M]. upair(M,a,a,x) & union(M,x,a,z)"

    26

    27   powerset :: "[i=>o,i,i] => o"

    28     "powerset(M,A,z) == \<forall>x[M]. x \<in> z <-> subset(M,x,A)"

    29

    30   inter :: "[i=>o,i,i,i] => o"

    31     "inter(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<in> b"

    32

    33   setdiff :: "[i=>o,i,i,i] => o"

    34     "setdiff(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<notin> b"

    35

    36   big_union :: "[i=>o,i,i] => o"

    37     "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y\<in>A. M(y) & x \<in> y)"

    38

    39   big_inter :: "[i=>o,i,i] => o"

    40     "big_inter(M,A,z) ==

    41              (A=0 --> z=0) &

    42 	     (A\<noteq>0 --> (\<forall>x[M]. x \<in> z <-> (\<forall>y\<in>A. M(y) --> x \<in> y)))"

    43

    44   cartprod :: "[i=>o,i,i,i] => o"

    45     "cartprod(M,A,B,z) ==

    46 	\<forall>u[M]. u \<in> z <-> (\<exists>x\<in>A. M(x) & (\<exists>y\<in>B. M(y) & pair(M,x,y,u)))"

    47

    48   is_converse :: "[i=>o,i,i] => o"

    49     "is_converse(M,r,z) ==

    50 	\<forall>x. M(x) -->

    51             (x \<in> z <->

    52              (\<exists>w\<in>r. M(w) &

    53               (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x))))"

    54

    55   pre_image :: "[i=>o,i,i,i] => o"

    56     "pre_image(M,r,A,z) ==

    57 	\<forall>x. M(x) --> (x \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>y\<in>A. M(y) & pair(M,x,y,w))))"

    58

    59   is_domain :: "[i=>o,i,i] => o"

    60     "is_domain(M,r,z) ==

    61 	\<forall>x. M(x) --> (x \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>y. M(y) & pair(M,x,y,w))))"

    62

    63   image :: "[i=>o,i,i,i] => o"

    64     "image(M,r,A,z) ==

    65         \<forall>y. M(y) --> (y \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>x\<in>A. M(x) & pair(M,x,y,w))))"

    66

    67   is_range :: "[i=>o,i,i] => o"

    68     --{*the cleaner

    69       @{term "\<exists>r'. M(r') & is_converse(M,r,r') & is_domain(M,r',z)"}

    70       unfortunately needs an instance of separation in order to prove

    71         @{term "M(converse(r))"}.*}

    72     "is_range(M,r,z) ==

    73 	\<forall>y. M(y) --> (y \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>x. M(x) & pair(M,x,y,w))))"

    74

    75   is_field :: "[i=>o,i,i] => o"

    76     "is_field(M,r,z) ==

    77 	\<exists>dr. M(dr) & is_domain(M,r,dr) &

    78             (\<exists>rr. M(rr) & is_range(M,r,rr) & union(M,dr,rr,z))"

    79

    80   is_relation :: "[i=>o,i] => o"

    81     "is_relation(M,r) ==

    82         (\<forall>z\<in>r. M(z) --> (\<exists>x y. M(x) & M(y) & pair(M,x,y,z)))"

    83

    84   is_function :: "[i=>o,i] => o"

    85     "is_function(M,r) ==

    86 	(\<forall>x y y' p p'. M(x) --> M(y) --> M(y') --> M(p) --> M(p') -->

    87                       pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r -->

    88                       y=y')"

    89

    90   fun_apply :: "[i=>o,i,i,i] => o"

    91     "fun_apply(M,f,x,y) ==

    92 	(\<forall>y'. M(y') --> ((\<exists>u\<in>f. M(u) & pair(M,x,y',u)) <-> y=y'))"

    93

    94   typed_function :: "[i=>o,i,i,i] => o"

    95     "typed_function(M,A,B,r) ==

    96         is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &

    97         (\<forall>u\<in>r. M(u) --> (\<forall>x y. M(x) & M(y) & pair(M,x,y,u) --> y\<in>B))"

    98

    99   is_funspace :: "[i=>o,i,i,i] => o"

   100     "is_funspace(M,A,B,F) ==

   101         \<forall>f[M]. f \<in> F <-> typed_function(M,A,B,f)"

   102

   103   composition :: "[i=>o,i,i,i] => o"

   104     "composition(M,r,s,t) ==

   105         \<forall>p. M(p) --> (p \<in> t <->

   106                       (\<exists>x. M(x) & (\<exists>y. M(y) & (\<exists>z. M(z) &

   107                            p = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r))))"

   108

   109

   110   injection :: "[i=>o,i,i,i] => o"

   111     "injection(M,A,B,f) ==

   112 	typed_function(M,A,B,f) &

   113         (\<forall>x x' y p p'. M(x) --> M(x') --> M(y) --> M(p) --> M(p') -->

   114                       pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f -->

   115                       x=x')"

   116

   117   surjection :: "[i=>o,i,i,i] => o"

   118     "surjection(M,A,B,f) ==

   119         typed_function(M,A,B,f) &

   120         (\<forall>y\<in>B. M(y) --> (\<exists>x\<in>A. M(x) & fun_apply(M,f,x,y)))"

   121

   122   bijection :: "[i=>o,i,i,i] => o"

   123     "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)"

   124

   125   restriction :: "[i=>o,i,i,i] => o"

   126     "restriction(M,r,A,z) ==

   127 	\<forall>x. M(x) -->

   128             (x \<in> z <->

   129              (x \<in> r & (\<exists>u\<in>A. M(u) & (\<exists>v. M(v) & pair(M,u,v,x)))))"

   130

   131   transitive_set :: "[i=>o,i] => o"

   132     "transitive_set(M,a) == \<forall>x\<in>a. M(x) --> subset(M,x,a)"

   133

   134   ordinal :: "[i=>o,i] => o"

   135      --{*an ordinal is a transitive set of transitive sets*}

   136     "ordinal(M,a) == transitive_set(M,a) & (\<forall>x\<in>a. M(x) --> transitive_set(M,x))"

   137

   138   limit_ordinal :: "[i=>o,i] => o"

   139     --{*a limit ordinal is a non-empty, successor-closed ordinal*}

   140     "limit_ordinal(M,a) ==

   141 	ordinal(M,a) & ~ empty(M,a) &

   142         (\<forall>x\<in>a. M(x) --> (\<exists>y\<in>a. M(y) & successor(M,x,y)))"

   143

   144   successor_ordinal :: "[i=>o,i] => o"

   145     --{*a successor ordinal is any ordinal that is neither empty nor limit*}

   146     "successor_ordinal(M,a) ==

   147 	ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)"

   148

   149   finite_ordinal :: "[i=>o,i] => o"

   150     --{*an ordinal is finite if neither it nor any of its elements are limit*}

   151     "finite_ordinal(M,a) ==

   152 	ordinal(M,a) & ~ limit_ordinal(M,a) &

   153         (\<forall>x\<in>a. M(x) --> ~ limit_ordinal(M,x))"

   154

   155   omega :: "[i=>o,i] => o"

   156     --{*omega is a limit ordinal none of whose elements are limit*}

   157     "omega(M,a) == limit_ordinal(M,a) & (\<forall>x\<in>a. M(x) --> ~ limit_ordinal(M,x))"

   158

   159   number1 :: "[i=>o,i] => o"

   160     "number1(M,a) == (\<exists>x. M(x) & empty(M,x) & successor(M,x,a))"

   161

   162   number2 :: "[i=>o,i] => o"

   163     "number2(M,a) == (\<exists>x. M(x) & number1(M,x) & successor(M,x,a))"

   164

   165   number3 :: "[i=>o,i] => o"

   166     "number3(M,a) == (\<exists>x. M(x) & number2(M,x) & successor(M,x,a))"

   167

   168

   169 subsection {*The relativized ZF axioms*}

   170 constdefs

   171

   172   extensionality :: "(i=>o) => o"

   173     "extensionality(M) ==

   174 	\<forall>x[M]. \<forall>y[M]. (\<forall>z[M]. z \<in> x <-> z \<in> y) --> x=y"

   175

   176   separation :: "[i=>o, i=>o] => o"

   177     --{*Big problem: the formula @{text P} should only involve parameters

   178         belonging to @{text M}.  Don't see how to enforce that.*}

   179     "separation(M,P) ==

   180 	\<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"

   181

   182   upair_ax :: "(i=>o) => o"

   183     "upair_ax(M) == \<forall>x y. M(x) --> M(y) --> (\<exists>z. M(z) & upair(M,x,y,z))"

   184

   185   Union_ax :: "(i=>o) => o"

   186     "Union_ax(M) == \<forall>x. M(x) --> (\<exists>z. M(z) & big_union(M,x,z))"

   187

   188   power_ax :: "(i=>o) => o"

   189     "power_ax(M) == \<forall>x. M(x) --> (\<exists>z. M(z) & powerset(M,x,z))"

   190

   191   univalent :: "[i=>o, i, [i,i]=>o] => o"

   192     "univalent(M,A,P) ==

   193 	(\<forall>x\<in>A. M(x) --> (\<forall>y z. M(y) --> M(z) --> P(x,y) & P(x,z) --> y=z))"

   194

   195   replacement :: "[i=>o, [i,i]=>o] => o"

   196     "replacement(M,P) ==

   197       \<forall>A. M(A) --> univalent(M,A,P) -->

   198       (\<exists>Y. M(Y) & (\<forall>b. M(b) --> ((\<exists>x\<in>A. M(x) & P(x,b)) --> b \<in> Y)))"

   199

   200   strong_replacement :: "[i=>o, [i,i]=>o] => o"

   201     "strong_replacement(M,P) ==

   202       \<forall>A. M(A) --> univalent(M,A,P) -->

   203       (\<exists>Y. M(Y) & (\<forall>b. M(b) --> (b \<in> Y <-> (\<exists>x\<in>A. M(x) & P(x,b)))))"

   204

   205   foundation_ax :: "(i=>o) => o"

   206     "foundation_ax(M) ==

   207 	\<forall>x. M(x) --> (\<exists>y\<in>x. M(y))

   208                  --> (\<exists>y\<in>x. M(y) & ~(\<exists>z\<in>x. M(z) & z \<in> y))"

   209

   210

   211 subsection{*A trivial consistency proof for $V_\omega$ *}

   212

   213 text{*We prove that $V_\omega$

   214       (or @{text univ} in Isabelle) satisfies some ZF axioms.

   215      Kunen, Theorem IV 3.13, page 123.*}

   216

   217 lemma univ0_downwards_mem: "[| y \<in> x; x \<in> univ(0) |] ==> y \<in> univ(0)"

   218 apply (insert Transset_univ [OF Transset_0])

   219 apply (simp add: Transset_def, blast)

   220 done

   221

   222 lemma univ0_Ball_abs [simp]:

   223      "A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) --> P(x)) <-> (\<forall>x\<in>A. P(x))"

   224 by (blast intro: univ0_downwards_mem)

   225

   226 lemma univ0_Bex_abs [simp]:

   227      "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) <-> (\<exists>x\<in>A. P(x))"

   228 by (blast intro: univ0_downwards_mem)

   229

   230 text{*Congruence rule for separation: can assume the variable is in @{text M}*}

   231 lemma separation_cong [cong]:

   232      "(!!x. M(x) ==> P(x) <-> P'(x)) ==> separation(M,P) <-> separation(M,P')"

   233 by (simp add: separation_def)

   234

   235 text{*Congruence rules for replacement*}

   236 lemma univalent_cong [cong]:

   237      "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |]

   238       ==> univalent(M,A,P) <-> univalent(M,A',P')"

   239 by (simp add: univalent_def)

   240

   241 lemma strong_replacement_cong [cong]:

   242      "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |]

   243       ==> strong_replacement(M,P) <-> strong_replacement(M,P')"

   244 by (simp add: strong_replacement_def)

   245

   246 text{*The extensionality axiom*}

   247 lemma "extensionality(\<lambda>x. x \<in> univ(0))"

   248 apply (simp add: extensionality_def)

   249 apply (blast intro: univ0_downwards_mem)

   250 done

   251

   252 text{*The separation axiom requires some lemmas*}

   253 lemma Collect_in_Vfrom:

   254      "[| X \<in> Vfrom(A,j);  Transset(A) |] ==> Collect(X,P) \<in> Vfrom(A, succ(j))"

   255 apply (drule Transset_Vfrom)

   256 apply (rule subset_mem_Vfrom)

   257 apply (unfold Transset_def, blast)

   258 done

   259

   260 lemma Collect_in_VLimit:

   261      "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]

   262       ==> Collect(X,P) \<in> Vfrom(A,i)"

   263 apply (rule Limit_VfromE, assumption+)

   264 apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom)

   265 done

   266

   267 lemma Collect_in_univ:

   268      "[| X \<in> univ(A);  Transset(A) |] ==> Collect(X,P) \<in> univ(A)"

   269 by (simp add: univ_def Collect_in_VLimit Limit_nat)

   270

   271 lemma "separation(\<lambda>x. x \<in> univ(0), P)"

   272 apply (simp add: separation_def, clarify)

   273 apply (rule_tac x = "Collect(x,P)" in bexI)

   274 apply (blast intro: Collect_in_univ Transset_0)+

   275 done

   276

   277 text{*Unordered pairing axiom*}

   278 lemma "upair_ax(\<lambda>x. x \<in> univ(0))"

   279 apply (simp add: upair_ax_def upair_def)

   280 apply (blast intro: doubleton_in_univ)

   281 done

   282

   283 text{*Union axiom*}

   284 lemma "Union_ax(\<lambda>x. x \<in> univ(0))"

   285 apply (simp add: Union_ax_def big_union_def)

   286 apply (blast intro: Union_in_univ Transset_0 univ0_downwards_mem)

   287 done

   288

   289 text{*Powerset axiom*}

   290

   291 lemma Pow_in_univ:

   292      "[| X \<in> univ(A);  Transset(A) |] ==> Pow(X) \<in> univ(A)"

   293 apply (simp add: univ_def Pow_in_VLimit Limit_nat)

   294 done

   295

   296 lemma "power_ax(\<lambda>x. x \<in> univ(0))"

   297 apply (simp add: power_ax_def powerset_def subset_def)

   298 apply (blast intro: Pow_in_univ Transset_0 univ0_downwards_mem)

   299 done

   300

   301 text{*Foundation axiom*}

   302 lemma "foundation_ax(\<lambda>x. x \<in> univ(0))"

   303 apply (simp add: foundation_ax_def, clarify)

   304 apply (cut_tac A=x in foundation, blast)

   305 done

   306

   307 lemma "replacement(\<lambda>x. x \<in> univ(0), P)"

   308 apply (simp add: replacement_def, clarify)

   309 oops

   310 text{*no idea: maybe prove by induction on the rank of A?*}

   311

   312 text{*Still missing: Replacement, Choice*}

   313

   314 subsection{*lemmas needed to reduce some set constructions to instances

   315       of Separation*}

   316

   317 lemma image_iff_Collect: "r  A = {y \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=<x,y>}"

   318 apply (rule equalityI, auto)

   319 apply (simp add: Pair_def, blast)

   320 done

   321

   322 lemma vimage_iff_Collect:

   323      "r - A = {x \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=<x,y>}"

   324 apply (rule equalityI, auto)

   325 apply (simp add: Pair_def, blast)

   326 done

   327

   328 text{*These two lemmas lets us prove @{text domain_closed} and

   329       @{text range_closed} without new instances of separation*}

   330

   331 lemma domain_eq_vimage: "domain(r) = r - Union(Union(r))"

   332 apply (rule equalityI, auto)

   333 apply (rule vimageI, assumption)

   334 apply (simp add: Pair_def, blast)

   335 done

   336

   337 lemma range_eq_image: "range(r) = r  Union(Union(r))"

   338 apply (rule equalityI, auto)

   339 apply (rule imageI, assumption)

   340 apply (simp add: Pair_def, blast)

   341 done

   342

   343 lemma replacementD:

   344     "[| replacement(M,P); M(A);  univalent(M,A,P) |]

   345      ==> \<exists>Y. M(Y) & (\<forall>b. M(b) --> ((\<exists>x\<in>A. M(x) & P(x,b)) --> b \<in> Y))"

   346 by (simp add: replacement_def)

   347

   348 lemma strong_replacementD:

   349     "[| strong_replacement(M,P); M(A);  univalent(M,A,P) |]

   350      ==> \<exists>Y. M(Y) & (\<forall>b. M(b) --> (b \<in> Y <-> (\<exists>x\<in>A. M(x) & P(x,b))))"

   351 by (simp add: strong_replacement_def)

   352

   353 lemma separationD:

   354     "[| separation(M,P); M(z) |] ==> \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"

   355 by (simp add: separation_def)

   356

   357

   358 text{*More constants, for order types*}

   359 constdefs

   360

   361   order_isomorphism :: "[i=>o,i,i,i,i,i] => o"

   362     "order_isomorphism(M,A,r,B,s,f) ==

   363         bijection(M,A,B,f) &

   364         (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>p fx fy q.

   365             M(x) --> M(y) --> M(p) --> M(fx) --> M(fy) --> M(q) -->

   366             pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) -->

   367             pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))"

   368

   369

   370   pred_set :: "[i=>o,i,i,i,i] => o"

   371     "pred_set(M,A,x,r,B) ==

   372 	\<forall>y. M(y) --> (y \<in> B <-> (\<exists>p\<in>r. M(p) & y \<in> A & pair(M,y,x,p)))"

   373

   374   membership :: "[i=>o,i,i] => o" --{*membership relation*}

   375     "membership(M,A,r) ==

   376 	\<forall>p. M(p) -->

   377              (p \<in> r <-> (\<exists>x\<in>A. \<exists>y\<in>A. M(x) & M(y) & x\<in>y & pair(M,x,y,p)))"

   378

   379

   380 subsection{*Absoluteness for a transitive class model*}

   381

   382 text{*The class M is assumed to be transitive and to satisfy some

   383       relativized ZF axioms*}

   384 locale M_triv_axioms =

   385   fixes M

   386   assumes transM:           "[| y\<in>x; M(x) |] ==> M(y)"

   387       and nonempty [simp]:  "M(0)"

   388       and upair_ax:	    "upair_ax(M)"

   389       and Union_ax:	    "Union_ax(M)"

   390       and power_ax:         "power_ax(M)"

   391       and replacement:      "replacement(M,P)"

   392       and M_nat [iff]:      "M(nat)"           (*i.e. the axiom of infinity*)

   393

   394 lemma (in M_triv_axioms) ball_abs [simp]:

   395      "M(A) ==> (\<forall>x\<in>A. M(x) --> P(x)) <-> (\<forall>x\<in>A. P(x))"

   396 by (blast intro: transM)

   397

   398 lemma (in M_triv_axioms) rall_abs [simp]:

   399      "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))"

   400 by (blast intro: transM)

   401

   402 lemma (in M_triv_axioms) bex_abs [simp]:

   403      "M(A) ==> (\<exists>x\<in>A. M(x) & P(x)) <-> (\<exists>x\<in>A. P(x))"

   404 by (blast intro: transM)

   405

   406 lemma (in M_triv_axioms) rex_abs [simp]:

   407      "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))"

   408 by (blast intro: transM)

   409

   410 lemma (in M_triv_axioms) ball_iff_equiv:

   411      "M(A) ==> (\<forall>x. M(x) --> (x\<in>A <-> P(x))) <->

   412                (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)"

   413 by (blast intro: transM)

   414

   415 text{*Simplifies proofs of equalities when there's an iff-equality

   416       available for rewriting, universally quantified over M. *}

   417 lemma (in M_triv_axioms) M_equalityI:

   418      "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"

   419 by (blast intro!: equalityI dest: transM)

   420

   421 lemma (in M_triv_axioms) empty_abs [simp]:

   422      "M(z) ==> empty(M,z) <-> z=0"

   423 apply (simp add: empty_def)

   424 apply (blast intro: transM)

   425 done

   426

   427 lemma (in M_triv_axioms) subset_abs [simp]:

   428      "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"

   429 apply (simp add: subset_def)

   430 apply (blast intro: transM)

   431 done

   432

   433 lemma (in M_triv_axioms) upair_abs [simp]:

   434      "M(z) ==> upair(M,a,b,z) <-> z={a,b}"

   435 apply (simp add: upair_def)

   436 apply (blast intro: transM)

   437 done

   438

   439 lemma (in M_triv_axioms) upair_in_M_iff [iff]:

   440      "M({a,b}) <-> M(a) & M(b)"

   441 apply (insert upair_ax, simp add: upair_ax_def)

   442 apply (blast intro: transM)

   443 done

   444

   445 lemma (in M_triv_axioms) singleton_in_M_iff [iff]:

   446      "M({a}) <-> M(a)"

   447 by (insert upair_in_M_iff [of a a], simp)

   448

   449 lemma (in M_triv_axioms) pair_abs [simp]:

   450      "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"

   451 apply (simp add: pair_def ZF.Pair_def)

   452 apply (blast intro: transM)

   453 done

   454

   455 lemma (in M_triv_axioms) pair_in_M_iff [iff]:

   456      "M(<a,b>) <-> M(a) & M(b)"

   457 by (simp add: ZF.Pair_def)

   458

   459 lemma (in M_triv_axioms) pair_components_in_M:

   460      "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"

   461 apply (simp add: Pair_def)

   462 apply (blast dest: transM)

   463 done

   464

   465 lemma (in M_triv_axioms) cartprod_abs [simp]:

   466      "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"

   467 apply (simp add: cartprod_def)

   468 apply (rule iffI)

   469  apply (blast intro!: equalityI intro: transM dest!: rspec)

   470 apply (blast dest: transM)

   471 done

   472

   473 lemma (in M_triv_axioms) union_abs [simp]:

   474      "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"

   475 apply (simp add: union_def)

   476 apply (blast intro: transM)

   477 done

   478

   479 lemma (in M_triv_axioms) inter_abs [simp]:

   480      "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"

   481 apply (simp add: inter_def)

   482 apply (blast intro: transM)

   483 done

   484

   485 lemma (in M_triv_axioms) setdiff_abs [simp]:

   486      "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"

   487 apply (simp add: setdiff_def)

   488 apply (blast intro: transM)

   489 done

   490

   491 lemma (in M_triv_axioms) Union_abs [simp]:

   492      "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"

   493 apply (simp add: big_union_def)

   494 apply (blast intro!: equalityI dest: transM)

   495 done

   496

   497 lemma (in M_triv_axioms) Union_closed [intro,simp]:

   498      "M(A) ==> M(Union(A))"

   499 by (insert Union_ax, simp add: Union_ax_def)

   500

   501 lemma (in M_triv_axioms) Un_closed [intro,simp]:

   502      "[| M(A); M(B) |] ==> M(A Un B)"

   503 by (simp only: Un_eq_Union, blast)

   504

   505 lemma (in M_triv_axioms) cons_closed [intro,simp]:

   506      "[| M(a); M(A) |] ==> M(cons(a,A))"

   507 by (subst cons_eq [symmetric], blast)

   508

   509 lemma (in M_triv_axioms) successor_abs [simp]:

   510      "[| M(a); M(z) |] ==> successor(M,a,z) <-> z=succ(a)"

   511 by (simp add: successor_def, blast)

   512

   513 lemma (in M_triv_axioms) succ_in_M_iff [iff]:

   514      "M(succ(a)) <-> M(a)"

   515 apply (simp add: succ_def)

   516 apply (blast intro: transM)

   517 done

   518

   519 lemma (in M_triv_axioms) separation_closed [intro,simp]:

   520      "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"

   521 apply (insert separation, simp add: separation_def)

   522 apply (drule rspec, assumption, clarify)

   523 apply (subgoal_tac "y = Collect(A,P)", blast)

   524 apply (blast dest: transM)

   525 done

   526

   527 text{*Probably the premise and conclusion are equivalent*}

   528 lemma (in M_triv_axioms) strong_replacementI [rule_format]:

   529     "[| \<forall>A. M(A) --> separation(M, %u. \<exists>x\<in>A. P(x,u)) |]

   530      ==> strong_replacement(M,P)"

   531 apply (simp add: strong_replacement_def, clarify)

   532 apply (frule replacementD [OF replacement], assumption, clarify)

   533 apply (drule_tac x=A in spec, clarify)

   534 apply (drule_tac z=Y in separationD, assumption, clarify)

   535 apply (blast dest: transM)

   536 done

   537

   538

   539 (*The last premise expresses that P takes M to M*)

   540 lemma (in M_triv_axioms) strong_replacement_closed [intro,simp]:

   541      "[| strong_replacement(M,P); M(A); univalent(M,A,P);

   542        !!x y. [| x\<in>A; P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"

   543 apply (simp add: strong_replacement_def)

   544 apply (drule spec [THEN mp], auto)

   545 apply (subgoal_tac "Replace(A,P) = Y")

   546  apply simp

   547 apply (rule equality_iffI)

   548 apply (simp add: Replace_iff, safe)

   549  apply (blast dest: transM)

   550 apply (frule transM, assumption)

   551  apply (simp add: univalent_def)

   552  apply (drule spec [THEN mp, THEN iffD1], assumption, assumption)

   553  apply (blast dest: transM)

   554 done

   555

   556 (*The first premise can't simply be assumed as a schema.

   557   It is essential to take care when asserting instances of Replacement.

   558   Let K be a nonconstructible subset of nat and define

   559   f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a

   560   nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))

   561   even for f : M -> M.

   562 *)

   563 lemma (in M_triv_axioms) RepFun_closed [intro,simp]:

   564      "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]

   565       ==> M(RepFun(A,f))"

   566 apply (simp add: RepFun_def)

   567 apply (rule strong_replacement_closed)

   568 apply (auto dest: transM  simp add: univalent_def)

   569 done

   570

   571 lemma (in M_triv_axioms) lam_closed [intro,simp]:

   572      "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]

   573       ==> M(\<lambda>x\<in>A. b(x))"

   574 by (simp add: lam_def, blast dest: transM)

   575

   576 lemma (in M_triv_axioms) image_abs [simp]:

   577      "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = rA"

   578 apply (simp add: image_def)

   579 apply (rule iffI)

   580  apply (blast intro!: equalityI dest: transM, blast)

   581 done

   582

   583 text{*What about @{text Pow_abs}?  Powerset is NOT absolute!

   584       This result is one direction of absoluteness.*}

   585

   586 lemma (in M_triv_axioms) powerset_Pow:

   587      "powerset(M, x, Pow(x))"

   588 by (simp add: powerset_def)

   589

   590 text{*But we can't prove that the powerset in @{text M} includes the

   591       real powerset.*}

   592 lemma (in M_triv_axioms) powerset_imp_subset_Pow:

   593      "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"

   594 apply (simp add: powerset_def)

   595 apply (blast dest: transM)

   596 done

   597

   598 lemma (in M_triv_axioms) nat_into_M [intro]:

   599      "n \<in> nat ==> M(n)"

   600 by (induct n rule: nat_induct, simp_all)

   601

   602 lemma (in M_triv_axioms) nat_case_closed:

   603   "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"

   604 apply (case_tac "k=0", simp)

   605 apply (case_tac "\<exists>m. k = succ(m)", force)

   606 apply (simp add: nat_case_def)

   607 done

   608

   609 lemma (in M_triv_axioms) Inl_in_M_iff [iff]:

   610      "M(Inl(a)) <-> M(a)"

   611 by (simp add: Inl_def)

   612

   613 lemma (in M_triv_axioms) Inr_in_M_iff [iff]:

   614      "M(Inr(a)) <-> M(a)"

   615 by (simp add: Inr_def)

   616

   617

   618 subsection{*Absoluteness for ordinals*}

   619 text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}

   620

   621 lemma (in M_triv_axioms) lt_closed:

   622      "[| j<i; M(i) |] ==> M(j)"

   623 by (blast dest: ltD intro: transM)

   624

   625 lemma (in M_triv_axioms) transitive_set_abs [simp]:

   626      "M(a) ==> transitive_set(M,a) <-> Transset(a)"

   627 by (simp add: transitive_set_def Transset_def)

   628

   629 lemma (in M_triv_axioms) ordinal_abs [simp]:

   630      "M(a) ==> ordinal(M,a) <-> Ord(a)"

   631 by (simp add: ordinal_def Ord_def)

   632

   633 lemma (in M_triv_axioms) limit_ordinal_abs [simp]:

   634      "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"

   635 apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def)

   636 apply (simp add: lt_def, blast)

   637 done

   638

   639 lemma (in M_triv_axioms) successor_ordinal_abs [simp]:

   640      "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b. M(b) & a = succ(b))"

   641 apply (simp add: successor_ordinal_def, safe)

   642 apply (drule Ord_cases_disj, auto)

   643 done

   644

   645 lemma finite_Ord_is_nat:

   646       "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"

   647 by (induct a rule: trans_induct3, simp_all)

   648

   649 lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"

   650 by (induct a rule: nat_induct, auto)

   651

   652 lemma (in M_triv_axioms) finite_ordinal_abs [simp]:

   653      "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"

   654 apply (simp add: finite_ordinal_def)

   655 apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord

   656              dest: Ord_trans naturals_not_limit)

   657 done

   658

   659 lemma Limit_non_Limit_implies_nat:

   660      "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"

   661 apply (rule le_anti_sym)

   662 apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)

   663  apply (simp add: lt_def)

   664  apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat)

   665 apply (erule nat_le_Limit)

   666 done

   667

   668 lemma (in M_triv_axioms) omega_abs [simp]:

   669      "M(a) ==> omega(M,a) <-> a = nat"

   670 apply (simp add: omega_def)

   671 apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)

   672 done

   673

   674 lemma (in M_triv_axioms) number1_abs [simp]:

   675      "M(a) ==> number1(M,a) <-> a = 1"

   676 by (simp add: number1_def)

   677

   678 lemma (in M_triv_axioms) number1_abs [simp]:

   679      "M(a) ==> number2(M,a) <-> a = succ(1)"

   680 by (simp add: number2_def)

   681

   682 lemma (in M_triv_axioms) number3_abs [simp]:

   683      "M(a) ==> number3(M,a) <-> a = succ(succ(1))"

   684 by (simp add: number3_def)

   685

   686 text{*Kunen continued to 20...*}

   687

   688 (*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything

   689   but the recursion variable must stay unchanged.  But then the recursion

   690   equations only hold for x\<in>nat (or in some other set) and not for the

   691   whole of the class M.

   692   consts

   693     natnumber_aux :: "[i=>o,i] => i"

   694

   695   primrec

   696       "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"

   697       "natnumber_aux(M,succ(n)) =

   698 	   (\<lambda>x\<in>nat. if (\<exists>y. M(y) & natnumber_aux(M,n)y=1 & successor(M,y,x))

   699 		     then 1 else 0)"

   700

   701   constdefs

   702     natnumber :: "[i=>o,i,i] => o"

   703       "natnumber(M,n,x) == natnumber_aux(M,n)x = 1"

   704

   705   lemma (in M_triv_axioms) [simp]:

   706        "natnumber(M,0,x) == x=0"

   707 *)

   708

   709 subsection{*Some instances of separation and strong replacement*}

   710

   711 locale M_axioms = M_triv_axioms +

   712 assumes Inter_separation:

   713      "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"

   714   and cartprod_separation:

   715      "[| M(A); M(B) |]

   716       ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. M(x) & M(y) & pair(M,x,y,z))"

   717   and image_separation:

   718      "[| M(A); M(r) |]

   719       ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,p)))"

   720   and converse_separation:

   721      "M(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r.

   722                     M(p) & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"

   723   and restrict_separation:

   724      "M(A) ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. pair(M,x,y,z)))"

   725   and comp_separation:

   726      "[| M(r); M(s) |]

   727       ==> separation(M, \<lambda>xz. \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].

   728 		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) &

   729                   xy\<in>s & yz\<in>r)"

   730   and pred_separation:

   731      "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & pair(M,y,x,p))"

   732   and Memrel_separation:

   733      "separation(M, \<lambda>z. \<exists>x y. M(x) & M(y) & pair(M,x,y,z) & x \<in> y)"

   734   and obase_separation:

   735      --{*part of the order type formalization*}

   736      "[| M(A); M(r) |]

   737       ==> separation(M, \<lambda>a. \<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) &

   738 	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &

   739 	     order_isomorphism(M,par,r,x,mx,g))"

   740   and funspace_succ_replacement:

   741      "M(n) ==>

   742       strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M].

   743                 pair(M,f,b,p) & pair(M,n,b,nb) & z = {cons(nb,f)})"

   744   and well_ord_iso_separation:

   745      "[| M(A); M(f); M(r) |]

   746       ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. M(y) & (\<exists>p. M(p) &

   747 		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"

   748   and obase_equals_separation:

   749      "[| M(A); M(r) |]

   750       ==> separation

   751       (M, \<lambda>x. x\<in>A --> ~(\<exists>y. M(y) & (\<exists>g. M(g) &

   752 	      ordinal(M,y) & (\<exists>my pxr. M(my) & M(pxr) &

   753 	      membership(M,y,my) & pred_set(M,A,x,r,pxr) &

   754 	      order_isomorphism(M,pxr,r,y,my,g)))))"

   755   and is_recfun_separation:

   756      --{*for well-founded recursion.  NEEDS RELATIVIZATION*}

   757      "[| M(A); M(f); M(g); M(a); M(b) |]

   758      ==> separation(M, \<lambda>x. \<langle>x,a\<rangle> \<in> r & \<langle>x,b\<rangle> \<in> r & fx \<noteq> gx)"

   759   and omap_replacement:

   760      "[| M(A); M(r) |]

   761       ==> strong_replacement(M,

   762              \<lambda>a z. \<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) &

   763 	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &

   764 	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"

   765

   766 lemma (in M_axioms) cartprod_iff_lemma:

   767      "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}});

   768          powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]

   769        ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"

   770 apply (simp add: powerset_def)

   771 apply (rule equalityI, clarify, simp)

   772  apply (frule transM, assumption)

   773  apply (frule transM, assumption, simp)

   774  apply blast

   775 apply clarify

   776 apply (frule transM, assumption, force)

   777 done

   778

   779 lemma (in M_axioms) cartprod_iff:

   780      "[| M(A); M(B); M(C) |]

   781       ==> cartprod(M,A,B,C) <->

   782           (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &

   783                    C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"

   784 apply (simp add: Pair_def cartprod_def, safe)

   785 defer 1

   786   apply (simp add: powerset_def)

   787  apply blast

   788 txt{*Final, difficult case: the left-to-right direction of the theorem.*}

   789 apply (insert power_ax, simp add: power_ax_def)

   790 apply (frule_tac x="A Un B" and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec)

   791 apply (erule impE, blast, clarify)

   792 apply (drule_tac x=z and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec)

   793 apply (blast intro: cartprod_iff_lemma)

   794 done

   795

   796 lemma (in M_axioms) cartprod_closed_lemma:

   797      "[| M(A); M(B) |] ==> \<exists>C. M(C) & cartprod(M,A,B,C)"

   798 apply (simp del: cartprod_abs add: cartprod_iff)

   799 apply (insert power_ax, simp add: power_ax_def)

   800 apply (frule_tac x="A Un B" and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec)

   801 apply (erule impE, blast, clarify)

   802 apply (drule_tac x=z and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec)

   803 apply (erule impE, blast, clarify)

   804 apply (intro exI conjI)

   805 prefer 6 apply (rule refl)

   806 prefer 4 apply assumption

   807 prefer 4 apply assumption

   808 apply (insert cartprod_separation [of A B], auto)

   809 done

   810

   811 text{*All the lemmas above are necessary because Powerset is not absolute.

   812       I should have used Replacement instead!*}

   813 lemma (in M_axioms) cartprod_closed [intro,simp]:

   814      "[| M(A); M(B) |] ==> M(A*B)"

   815 by (frule cartprod_closed_lemma, assumption, force)

   816

   817 lemma (in M_axioms) sum_closed [intro,simp]:

   818      "[| M(A); M(B) |] ==> M(A+B)"

   819 by (simp add: sum_def)

   820

   821

   822 subsubsection {*converse of a relation*}

   823

   824 lemma (in M_axioms) M_converse_iff:

   825      "M(r) ==>

   826       converse(r) =

   827       {z \<in> Union(Union(r)) * Union(Union(r)).

   828        \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"

   829 apply (rule equalityI)

   830  prefer 2 apply (blast dest: transM, clarify, simp)

   831 apply (simp add: Pair_def)

   832 apply (blast dest: transM)

   833 done

   834

   835 lemma (in M_axioms) converse_closed [intro,simp]:

   836      "M(r) ==> M(converse(r))"

   837 apply (simp add: M_converse_iff)

   838 apply (insert converse_separation [of r], simp)

   839 done

   840

   841 lemma (in M_axioms) converse_abs [simp]:

   842      "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"

   843 apply (simp add: is_converse_def)

   844 apply (rule iffI)

   845  prefer 2 apply blast

   846 apply (rule M_equalityI)

   847   apply simp

   848   apply (blast dest: transM)+

   849 done

   850

   851

   852 subsubsection {*image, preimage, domain, range*}

   853

   854 lemma (in M_axioms) image_closed [intro,simp]:

   855      "[| M(A); M(r) |] ==> M(rA)"

   856 apply (simp add: image_iff_Collect)

   857 apply (insert image_separation [of A r], simp)

   858 done

   859

   860 lemma (in M_axioms) vimage_abs [simp]:

   861      "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-A"

   862 apply (simp add: pre_image_def)

   863 apply (rule iffI)

   864  apply (blast intro!: equalityI dest: transM, blast)

   865 done

   866

   867 lemma (in M_axioms) vimage_closed [intro,simp]:

   868      "[| M(A); M(r) |] ==> M(r-A)"

   869 by (simp add: vimage_def)

   870

   871

   872 subsubsection{*Domain, range and field*}

   873

   874 lemma (in M_axioms) domain_abs [simp]:

   875      "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"

   876 apply (simp add: is_domain_def)

   877 apply (blast intro!: equalityI dest: transM)

   878 done

   879

   880 lemma (in M_axioms) domain_closed [intro,simp]:

   881      "M(r) ==> M(domain(r))"

   882 apply (simp add: domain_eq_vimage)

   883 done

   884

   885 lemma (in M_axioms) range_abs [simp]:

   886      "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"

   887 apply (simp add: is_range_def)

   888 apply (blast intro!: equalityI dest: transM)

   889 done

   890

   891 lemma (in M_axioms) range_closed [intro,simp]:

   892      "M(r) ==> M(range(r))"

   893 apply (simp add: range_eq_image)

   894 done

   895

   896 lemma (in M_axioms) field_abs [simp]:

   897      "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"

   898 by (simp add: domain_closed range_closed is_field_def field_def)

   899

   900 lemma (in M_axioms) field_closed [intro,simp]:

   901      "M(r) ==> M(field(r))"

   902 by (simp add: domain_closed range_closed Un_closed field_def)

   903

   904

   905 subsubsection{*Relations, functions and application*}

   906

   907 lemma (in M_axioms) relation_abs [simp]:

   908      "M(r) ==> is_relation(M,r) <-> relation(r)"

   909 apply (simp add: is_relation_def relation_def)

   910 apply (blast dest!: bspec dest: pair_components_in_M)+

   911 done

   912

   913 lemma (in M_axioms) function_abs [simp]:

   914      "M(r) ==> is_function(M,r) <-> function(r)"

   915 apply (simp add: is_function_def function_def, safe)

   916    apply (frule transM, assumption)

   917   apply (blast dest: pair_components_in_M)+

   918 done

   919

   920 lemma (in M_axioms) apply_closed [intro,simp]:

   921      "[|M(f); M(a)|] ==> M(fa)"

   922 by (simp add: apply_def)

   923

   924 lemma (in M_axioms) apply_abs:

   925      "[| function(f); M(f); M(y) |]

   926       ==> fun_apply(M,f,x,y) <-> x \<in> domain(f) & fx = y"

   927 apply (simp add: fun_apply_def)

   928 apply (blast intro: function_apply_equality function_apply_Pair)

   929 done

   930

   931 lemma (in M_axioms) typed_apply_abs:

   932      "[| f \<in> A -> B; M(f); M(y) |]

   933       ==> fun_apply(M,f,x,y) <-> x \<in> A & fx = y"

   934 by (simp add: apply_abs fun_is_function domain_of_fun)

   935

   936 lemma (in M_axioms) typed_function_abs [simp]:

   937      "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"

   938 apply (auto simp add: typed_function_def relation_def Pi_iff)

   939 apply (blast dest: pair_components_in_M)+

   940 done

   941

   942 lemma (in M_axioms) injection_abs [simp]:

   943      "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"

   944 apply (simp add: injection_def apply_iff inj_def apply_closed)

   945 apply (blast dest: transM [of _ A])

   946 done

   947

   948 lemma (in M_axioms) surjection_abs [simp]:

   949      "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"

   950 by (simp add: typed_apply_abs surjection_def surj_def)

   951

   952 lemma (in M_axioms) bijection_abs [simp]:

   953      "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"

   954 by (simp add: bijection_def bij_def)

   955

   956

   957 subsubsection{*Composition of relations*}

   958

   959 lemma (in M_axioms) M_comp_iff:

   960      "[| M(r); M(s) |]

   961       ==> r O s =

   962           {xz \<in> domain(s) * range(r).

   963             \<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}"

   964 apply (simp add: comp_def)

   965 apply (rule equalityI)

   966  apply clarify

   967  apply simp

   968  apply  (blast dest:  transM)+

   969 done

   970

   971 lemma (in M_axioms) comp_closed [intro,simp]:

   972      "[| M(r); M(s) |] ==> M(r O s)"

   973 apply (simp add: M_comp_iff)

   974 apply (insert comp_separation [of r s], simp)

   975 done

   976

   977 lemma (in M_axioms) composition_abs [simp]:

   978      "[| M(r); M(s); M(t) |]

   979       ==> composition(M,r,s,t) <-> t = r O s"

   980 apply safe

   981  txt{*Proving @{term "composition(M, r, s, r O s)"}*}

   982  prefer 2

   983  apply (simp add: composition_def comp_def)

   984  apply (blast dest: transM)

   985 txt{*Opposite implication*}

   986 apply (rule M_equalityI)

   987   apply (simp add: composition_def comp_def)

   988   apply (blast del: allE dest: transM)+

   989 done

   990

   991 text{*no longer needed*}

   992 lemma (in M_axioms) restriction_is_function:

   993      "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |]

   994       ==> function(z)"

   995 apply (rotate_tac 1)

   996 apply (simp add: restriction_def ball_iff_equiv)

   997 apply (unfold function_def, blast)

   998 done

   999

  1000 lemma (in M_axioms) restriction_abs [simp]:

  1001      "[| M(f); M(A); M(z) |]

  1002       ==> restriction(M,f,A,z) <-> z = restrict(f,A)"

  1003 apply (simp add: ball_iff_equiv restriction_def restrict_def)

  1004 apply (blast intro!: equalityI dest: transM)

  1005 done

  1006

  1007

  1008 lemma (in M_axioms) M_restrict_iff:

  1009      "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"

  1010 by (simp add: restrict_def, blast dest: transM)

  1011

  1012 lemma (in M_axioms) restrict_closed [intro,simp]:

  1013      "[| M(A); M(r) |] ==> M(restrict(r,A))"

  1014 apply (simp add: M_restrict_iff)

  1015 apply (insert restrict_separation [of A], simp)

  1016 done

  1017

  1018 lemma (in M_axioms) Inter_abs [simp]:

  1019      "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"

  1020 apply (simp add: big_inter_def Inter_def)

  1021 apply (blast intro!: equalityI dest: transM)

  1022 done

  1023

  1024 lemma (in M_axioms) Inter_closed [intro,simp]:

  1025      "M(A) ==> M(Inter(A))"

  1026 by (insert Inter_separation, simp add: Inter_def)

  1027

  1028 lemma (in M_axioms) Int_closed [intro,simp]:

  1029      "[| M(A); M(B) |] ==> M(A Int B)"

  1030 apply (subgoal_tac "M({A,B})")

  1031 apply (frule Inter_closed, force+)

  1032 done

  1033

  1034 subsubsection{*Functions and function space*}

  1035

  1036 text{*M contains all finite functions*}

  1037 lemma (in M_axioms) finite_fun_closed_lemma [rule_format]:

  1038      "[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"

  1039 apply (induct_tac n, simp)

  1040 apply (rule ballI)

  1041 apply (simp add: succ_def)

  1042 apply (frule fun_cons_restrict_eq)

  1043 apply (erule ssubst)

  1044 apply (subgoal_tac "M(fx) & restrict(f,x) \<in> x -> A")

  1045  apply (simp add: cons_closed nat_into_M apply_closed)

  1046 apply (blast intro: apply_funtype transM restrict_type2)

  1047 done

  1048

  1049 lemma (in M_axioms) finite_fun_closed [rule_format]:

  1050      "[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"

  1051 by (blast intro: finite_fun_closed_lemma)

  1052

  1053 text{*The assumption @{term "M(A->B)"} is unusual, but essential: in

  1054 all but trivial cases, A->B cannot be expected to belong to @{term M}.*}

  1055 lemma (in M_axioms) is_funspace_abs [simp]:

  1056      "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B";

  1057 apply (simp add: is_funspace_def)

  1058 apply (rule iffI)

  1059  prefer 2 apply blast

  1060 apply (rule M_equalityI)

  1061   apply simp_all

  1062 done

  1063

  1064 lemma (in M_axioms) succ_fun_eq2:

  1065      "[|M(B); M(n->B)|] ==>

  1066       succ(n) -> B =

  1067       \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"

  1068 apply (simp add: succ_fun_eq)

  1069 apply (blast dest: transM)

  1070 done

  1071

  1072 lemma (in M_axioms) funspace_succ:

  1073      "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)"

  1074 apply (insert funspace_succ_replacement [of n])

  1075 apply (force simp add: succ_fun_eq2 univalent_def)

  1076 done

  1077

  1078 text{*@{term M} contains all finite function spaces.  Needed to prove the

  1079 absoluteness of transitive closure.*}

  1080 lemma (in M_axioms) finite_funspace_closed [intro,simp]:

  1081      "[|n\<in>nat; M(B)|] ==> M(n->B)"

  1082 apply (induct_tac n, simp)

  1083 apply (simp add: funspace_succ nat_into_M)

  1084 done

  1085

  1086 end