src/ZF/Constructible/Relative.thy
 author paulson Fri Jul 05 18:33:50 2002 +0200 (2002-07-05) changeset 13306 6eebcddee32b parent 13299 3a932abf97e8 child 13316 d16629fd0f95 permissions -rw-r--r--
more internalized formulas and separation proofs
     1 header {*Relativization and Absoluteness*}

     2

     3 theory Relative = Main:

     4

     5 subsection{* Relativized versions of standard set-theoretic concepts *}

     6

     7 constdefs

     8   empty :: "[i=>o,i] => o"

     9     "empty(M,z) == \<forall>x[M]. x \<notin> z"

    10

    11   subset :: "[i=>o,i,i] => o"

    12     "subset(M,A,B) == \<forall>x[M]. x\<in>A --> x \<in> B"

    13

    14   upair :: "[i=>o,i,i,i] => o"

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

    16

    17   pair :: "[i=>o,i,i,i] => o"

    18     "pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) &

    19                           (\<exists>y[M]. upair(M,a,b,y) & upair(M,x,y,z))"

    20

    21

    22   union :: "[i=>o,i,i,i] => o"

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

    24

    25   is_cons :: "[i=>o,i,i,i] => o"

    26     "is_cons(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & union(M,x,b,z)"

    27

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

    29     "successor(M,a,z) == is_cons(M,a,a,z)"

    30

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

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

    33

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

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

    36

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

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

    39

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

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

    42

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

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

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

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

    47

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

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

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

    51

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

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

    54 	\<forall>x[M]. x \<in> z <->

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

    56

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

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

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

    60

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

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

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

    64

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

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

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

    68

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

    70     --{*the cleaner

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

    72       unfortunately needs an instance of separation in order to prove

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

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

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

    76

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

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

    79 	\<exists>dr[M]. is_domain(M,r,dr) &

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

    81

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

    83     "is_relation(M,r) ==

    84         (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))"

    85

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

    87     "is_function(M,r) ==

    88 	\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].

    89            pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'"

    90

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

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

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

    94

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

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

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

    98         (\<forall>u[M]. u\<in>r --> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) --> y\<in>B))"

    99

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

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

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

   103

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

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

   106         \<forall>p[M]. p \<in> t <->

   107                (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. pair(M,x,z,p) & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r)"

   108

   109

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

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

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

   113         (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M].

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

   115

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

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

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

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

   120

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

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

   123

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

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

   126 	\<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))"

   127

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

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

   130

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

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

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

   134

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

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

   137     "limit_ordinal(M,a) ==

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

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

   140

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

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

   143     "successor_ordinal(M,a) ==

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

   145

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

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

   148     "finite_ordinal(M,a) ==

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

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

   151

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

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

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

   155

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

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

   158

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

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

   161

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

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

   164

   165

   166 subsection {*The relativized ZF axioms*}

   167 constdefs

   168

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

   170     "extensionality(M) ==

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

   172

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

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

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

   176     "separation(M,P) ==

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

   178

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

   180     "upair_ax(M) == \<forall>x y. M(x) --> M(y) --> (\<exists>z[M]. upair(M,x,y,z))"

   181

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

   183     "Union_ax(M) == \<forall>x[M]. (\<exists>z[M]. big_union(M,x,z))"

   184

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

   186     "power_ax(M) == \<forall>x[M]. (\<exists>z[M]. powerset(M,x,z))"

   187

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

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

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

   191

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

   193     "replacement(M,P) ==

   194       \<forall>A[M]. univalent(M,A,P) -->

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

   196

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

   198     "strong_replacement(M,P) ==

   199       \<forall>A[M]. univalent(M,A,P) -->

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

   201

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

   203     "foundation_ax(M) ==

   204 	\<forall>x[M]. (\<exists>y\<in>x. M(y))

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

   206

   207

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

   209

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

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

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

   213

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

   215 apply (insert Transset_univ [OF Transset_0])

   216 apply (simp add: Transset_def, blast)

   217 done

   218

   219 lemma univ0_Ball_abs [simp]:

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

   221 by (blast intro: univ0_downwards_mem)

   222

   223 lemma univ0_Bex_abs [simp]:

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

   225 by (blast intro: univ0_downwards_mem)

   226

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

   228 lemma separation_cong [cong]:

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

   230 by (simp add: separation_def)

   231

   232 text{*Congruence rules for replacement*}

   233 lemma univalent_cong [cong]:

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

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

   236 by (simp add: univalent_def)

   237

   238 lemma strong_replacement_cong [cong]:

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

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

   241 by (simp add: strong_replacement_def)

   242

   243 text{*The extensionality axiom*}

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

   245 apply (simp add: extensionality_def)

   246 apply (blast intro: univ0_downwards_mem)

   247 done

   248

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

   250 lemma Collect_in_Vfrom:

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

   252 apply (drule Transset_Vfrom)

   253 apply (rule subset_mem_Vfrom)

   254 apply (unfold Transset_def, blast)

   255 done

   256

   257 lemma Collect_in_VLimit:

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

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

   260 apply (rule Limit_VfromE, assumption+)

   261 apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom)

   262 done

   263

   264 lemma Collect_in_univ:

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

   266 by (simp add: univ_def Collect_in_VLimit Limit_nat)

   267

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

   269 apply (simp add: separation_def, clarify)

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

   271 apply (blast intro: Collect_in_univ Transset_0)+

   272 done

   273

   274 text{*Unordered pairing axiom*}

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

   276 apply (simp add: upair_ax_def upair_def)

   277 apply (blast intro: doubleton_in_univ)

   278 done

   279

   280 text{*Union axiom*}

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

   282 apply (simp add: Union_ax_def big_union_def, clarify)

   283 apply (rule_tac x="\<Union>x" in bexI)

   284  apply (blast intro: univ0_downwards_mem)

   285 apply (blast intro: Union_in_univ Transset_0)

   286 done

   287

   288 text{*Powerset axiom*}

   289

   290 lemma Pow_in_univ:

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

   292 apply (simp add: univ_def Pow_in_VLimit Limit_nat)

   293 done

   294

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

   296 apply (simp add: power_ax_def powerset_def subset_def, clarify)

   297 apply (rule_tac x="Pow(x)" in bexI)

   298  apply (blast intro: univ0_downwards_mem)

   299 apply (blast intro: Pow_in_univ Transset_0)

   300 done

   301

   302 text{*Foundation axiom*}

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

   304 apply (simp add: foundation_ax_def, clarify)

   305 apply (cut_tac A=x in foundation)

   306 apply (blast intro: univ0_downwards_mem)

   307 done

   308

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

   310 apply (simp add: replacement_def, clarify)

   311 oops

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

   313

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

   315

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

   317       of Separation*}

   318

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

   320 apply (rule equalityI, auto)

   321 apply (simp add: Pair_def, blast)

   322 done

   323

   324 lemma vimage_iff_Collect:

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

   326 apply (rule equalityI, auto)

   327 apply (simp add: Pair_def, blast)

   328 done

   329

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

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

   332

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

   334 apply (rule equalityI, auto)

   335 apply (rule vimageI, assumption)

   336 apply (simp add: Pair_def, blast)

   337 done

   338

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

   340 apply (rule equalityI, auto)

   341 apply (rule imageI, assumption)

   342 apply (simp add: Pair_def, blast)

   343 done

   344

   345 lemma replacementD:

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

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

   348 by (simp add: replacement_def)

   349

   350 lemma strong_replacementD:

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

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

   353 by (simp add: strong_replacement_def)

   354

   355 lemma separationD:

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

   357 by (simp add: separation_def)

   358

   359

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

   361 constdefs

   362

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

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

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

   366         (\<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A -->

   367           (\<forall>p[M]. \<forall>fx[M]. \<forall>fy[M]. \<forall>q[M].

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

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

   370

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

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

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

   374

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

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

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

   378

   379

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

   381

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

   383       relativized ZF axioms*}

   384 locale M_triv_axioms =

   385   fixes M

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

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

   388       and upair_ax:	    "upair_ax(M)"

   389       and Union_ax:	    "Union_ax(M)"

   390       and power_ax:         "power_ax(M)"

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

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

   393

   394 lemma (in M_triv_axioms) ball_abs [simp]:

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

   396 by (blast intro: transM)

   397

   398 lemma (in M_triv_axioms) rall_abs [simp]:

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

   400 by (blast intro: transM)

   401

   402 lemma (in M_triv_axioms) bex_abs [simp]:

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

   404 by (blast intro: transM)

   405

   406 lemma (in M_triv_axioms) rex_abs [simp]:

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

   408 by (blast intro: transM)

   409

   410 lemma (in M_triv_axioms) ball_iff_equiv:

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

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

   413 by (blast intro: transM)

   414

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

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

   417 lemma (in M_triv_axioms) M_equalityI:

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

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

   420

   421 lemma (in M_triv_axioms) empty_abs [simp]:

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

   423 apply (simp add: empty_def)

   424 apply (blast intro: transM)

   425 done

   426

   427 lemma (in M_triv_axioms) subset_abs [simp]:

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

   429 apply (simp add: subset_def)

   430 apply (blast intro: transM)

   431 done

   432

   433 lemma (in M_triv_axioms) upair_abs [simp]:

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

   435 apply (simp add: upair_def)

   436 apply (blast intro: transM)

   437 done

   438

   439 lemma (in M_triv_axioms) upair_in_M_iff [iff]:

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

   441 apply (insert upair_ax, simp add: upair_ax_def)

   442 apply (blast intro: transM)

   443 done

   444

   445 lemma (in M_triv_axioms) singleton_in_M_iff [iff]:

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

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

   448

   449 lemma (in M_triv_axioms) pair_abs [simp]:

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

   451 apply (simp add: pair_def ZF.Pair_def)

   452 apply (blast intro: transM)

   453 done

   454

   455 lemma (in M_triv_axioms) pair_in_M_iff [iff]:

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

   457 by (simp add: ZF.Pair_def)

   458

   459 lemma (in M_triv_axioms) pair_components_in_M:

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

   461 apply (simp add: Pair_def)

   462 apply (blast dest: transM)

   463 done

   464

   465 lemma (in M_triv_axioms) cartprod_abs [simp]:

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

   467 apply (simp add: cartprod_def)

   468 apply (rule iffI)

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

   470 apply (blast dest: transM)

   471 done

   472

   473 lemma (in M_triv_axioms) union_abs [simp]:

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

   475 apply (simp add: union_def)

   476 apply (blast intro: transM)

   477 done

   478

   479 lemma (in M_triv_axioms) inter_abs [simp]:

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

   481 apply (simp add: inter_def)

   482 apply (blast intro: transM)

   483 done

   484

   485 lemma (in M_triv_axioms) setdiff_abs [simp]:

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

   487 apply (simp add: setdiff_def)

   488 apply (blast intro: transM)

   489 done

   490

   491 lemma (in M_triv_axioms) Union_abs [simp]:

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

   493 apply (simp add: big_union_def)

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

   495 done

   496

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

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

   499 by (insert Union_ax, simp add: Union_ax_def)

   500

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

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

   503 by (simp only: Un_eq_Union, blast)

   504

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

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

   507 by (subst cons_eq [symmetric], blast)

   508

   509 lemma (in M_triv_axioms) cons_abs [simp]:

   510      "[| M(b); M(z) |] ==> is_cons(M,a,b,z) <-> z = cons(a,b)"

   511 by (simp add: is_cons_def, blast intro: transM)

   512

   513 lemma (in M_triv_axioms) successor_abs [simp]:

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

   515 by (simp add: successor_def, blast)

   516

   517 lemma (in M_triv_axioms) succ_in_M_iff [iff]:

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

   519 apply (simp add: succ_def)

   520 apply (blast intro: transM)

   521 done

   522

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

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

   525 apply (insert separation, simp add: separation_def)

   526 apply (drule rspec, assumption, clarify)

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

   528 apply (blast dest: transM)

   529 done

   530

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

   532 lemma (in M_triv_axioms) strong_replacementI [OF rallI]:

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

   534      ==> strong_replacement(M,P)"

   535 apply (simp add: strong_replacement_def, clarify)

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

   537 apply (drule_tac x=A in rspec, clarify)

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

   539 apply (rule_tac x=y in rexI)

   540 apply (blast dest: transM)+

   541 done

   542

   543

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

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

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

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

   548 apply (simp add: strong_replacement_def)

   549 apply (drule rspec, auto)

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

   551  apply simp

   552 apply (rule equality_iffI)

   553 apply (simp add: Replace_iff, safe)

   554  apply (blast dest: transM)

   555 apply (frule transM, assumption)

   556  apply (simp add: univalent_def)

   557  apply (drule rspec [THEN iffD1], assumption, assumption)

   558  apply (blast dest: transM)

   559 done

   560

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

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

   563   Let K be a nonconstructible subset of nat and define

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

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

   566   even for f : M -> M.

   567 *)

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

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

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

   571 apply (simp add: RepFun_def)

   572 apply (rule strong_replacement_closed)

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

   574 done

   575

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

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

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

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

   580

   581 lemma (in M_triv_axioms) image_abs [simp]:

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

   583 apply (simp add: image_def)

   584 apply (rule iffI)

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

   586 done

   587

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

   589       This result is one direction of absoluteness.*}

   590

   591 lemma (in M_triv_axioms) powerset_Pow:

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

   593 by (simp add: powerset_def)

   594

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

   596       real powerset.*}

   597 lemma (in M_triv_axioms) powerset_imp_subset_Pow:

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

   599 apply (simp add: powerset_def)

   600 apply (blast dest: transM)

   601 done

   602

   603 lemma (in M_triv_axioms) nat_into_M [intro]:

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

   605 by (induct n rule: nat_induct, simp_all)

   606

   607 lemma (in M_triv_axioms) nat_case_closed:

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

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

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

   611 apply (simp add: nat_case_def)

   612 done

   613

   614 lemma (in M_triv_axioms) Inl_in_M_iff [iff]:

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

   616 by (simp add: Inl_def)

   617

   618 lemma (in M_triv_axioms) Inr_in_M_iff [iff]:

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

   620 by (simp add: Inr_def)

   621

   622

   623 subsection{*Absoluteness for ordinals*}

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

   625

   626 lemma (in M_triv_axioms) lt_closed:

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

   628 by (blast dest: ltD intro: transM)

   629

   630 lemma (in M_triv_axioms) transitive_set_abs [simp]:

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

   632 by (simp add: transitive_set_def Transset_def)

   633

   634 lemma (in M_triv_axioms) ordinal_abs [simp]:

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

   636 by (simp add: ordinal_def Ord_def)

   637

   638 lemma (in M_triv_axioms) limit_ordinal_abs [simp]:

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

   640 apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def)

   641 apply (simp add: lt_def, blast)

   642 done

   643

   644 lemma (in M_triv_axioms) successor_ordinal_abs [simp]:

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

   646 apply (simp add: successor_ordinal_def, safe)

   647 apply (drule Ord_cases_disj, auto)

   648 done

   649

   650 lemma finite_Ord_is_nat:

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

   652 by (induct a rule: trans_induct3, simp_all)

   653

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

   655 by (induct a rule: nat_induct, auto)

   656

   657 lemma (in M_triv_axioms) finite_ordinal_abs [simp]:

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

   659 apply (simp add: finite_ordinal_def)

   660 apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord

   661              dest: Ord_trans naturals_not_limit)

   662 done

   663

   664 lemma Limit_non_Limit_implies_nat:

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

   666 apply (rule le_anti_sym)

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

   668  apply (simp add: lt_def)

   669  apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat)

   670 apply (erule nat_le_Limit)

   671 done

   672

   673 lemma (in M_triv_axioms) omega_abs [simp]:

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

   675 apply (simp add: omega_def)

   676 apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)

   677 done

   678

   679 lemma (in M_triv_axioms) number1_abs [simp]:

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

   681 by (simp add: number1_def)

   682

   683 lemma (in M_triv_axioms) number1_abs [simp]:

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

   685 by (simp add: number2_def)

   686

   687 lemma (in M_triv_axioms) number3_abs [simp]:

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

   689 by (simp add: number3_def)

   690

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

   692

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

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

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

   696   whole of the class M.

   697   consts

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

   699

   700   primrec

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

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

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

   704 		     then 1 else 0)"

   705

   706   constdefs

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

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

   709

   710   lemma (in M_triv_axioms) [simp]:

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

   712 *)

   713

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

   715

   716 locale M_axioms = M_triv_axioms +

   717 assumes Inter_separation:

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

   719   and cartprod_separation:

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

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

   722   and image_separation:

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

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

   725   and converse_separation:

   726      "M(r) ==> separation(M,

   727          \<lambda>z. \<exists>p[M]. p\<in>r & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"

   728   and restrict_separation:

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

   730   and comp_separation:

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

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

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

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

   735   and pred_separation:

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

   737   and Memrel_separation:

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

   739   and funspace_succ_replacement:

   740      "M(n) ==>

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

   742                 pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &

   743                 upair(M,cnbf,cnbf,z))"

   744   and well_ord_iso_separation:

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

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

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

   748   and obase_separation:

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

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

   751       ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].

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

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

   754   and obase_equals_separation:

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

   756       ==> separation

   757       (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M].

   758 	      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M].

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

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

   761   and omap_replacement:

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

   763       ==> strong_replacement(M,

   764              \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].

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

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

   767   and is_recfun_separation:

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

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

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

   771

   772 lemma (in M_axioms) cartprod_iff_lemma:

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

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

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

   776 apply (simp add: powerset_def)

   777 apply (rule equalityI, clarify, simp)

   778  apply (frule transM, assumption)

   779  apply (frule transM, assumption, simp)

   780  apply blast

   781 apply clarify

   782 apply (frule transM, assumption, force)

   783 done

   784

   785 lemma (in M_axioms) cartprod_iff:

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

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

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

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

   790 apply (simp add: Pair_def cartprod_def, safe)

   791 defer 1

   792   apply (simp add: powerset_def)

   793  apply blast

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

   795 apply (insert power_ax, simp add: power_ax_def)

   796 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)

   797 apply (blast, clarify)

   798 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)

   799 apply assumption

   800 apply (blast intro: cartprod_iff_lemma)

   801 done

   802

   803 lemma (in M_axioms) cartprod_closed_lemma:

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

   805 apply (simp del: cartprod_abs add: cartprod_iff)

   806 apply (insert power_ax, simp add: power_ax_def)

   807 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)

   808 apply (blast, clarify)

   809 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)

   810 apply (blast, clarify)

   811 apply (intro rexI exI conjI)

   812 prefer 5 apply (rule refl)

   813 prefer 3 apply assumption

   814 prefer 3 apply assumption

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

   816 done

   817

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

   819       I should have used Replacement instead!*}

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

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

   822 by (frule cartprod_closed_lemma, assumption, force)

   823

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

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

   826 by (simp add: sum_def)

   827

   828

   829 subsubsection {*converse of a relation*}

   830

   831 lemma (in M_axioms) M_converse_iff:

   832      "M(r) ==>

   833       converse(r) =

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

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

   836 apply (rule equalityI)

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

   838 apply (simp add: Pair_def)

   839 apply (blast dest: transM)

   840 done

   841

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

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

   844 apply (simp add: M_converse_iff)

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

   846 done

   847

   848 lemma (in M_axioms) converse_abs [simp]:

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

   850 apply (simp add: is_converse_def)

   851 apply (rule iffI)

   852  prefer 2 apply blast

   853 apply (rule M_equalityI)

   854   apply simp

   855   apply (blast dest: transM)+

   856 done

   857

   858

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

   860

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

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

   863 apply (simp add: image_iff_Collect)

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

   865 done

   866

   867 lemma (in M_axioms) vimage_abs [simp]:

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

   869 apply (simp add: pre_image_def)

   870 apply (rule iffI)

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

   872 done

   873

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

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

   876 by (simp add: vimage_def)

   877

   878

   879 subsubsection{*Domain, range and field*}

   880

   881 lemma (in M_axioms) domain_abs [simp]:

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

   883 apply (simp add: is_domain_def)

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

   885 done

   886

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

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

   889 apply (simp add: domain_eq_vimage)

   890 done

   891

   892 lemma (in M_axioms) range_abs [simp]:

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

   894 apply (simp add: is_range_def)

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

   896 done

   897

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

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

   900 apply (simp add: range_eq_image)

   901 done

   902

   903 lemma (in M_axioms) field_abs [simp]:

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

   905 by (simp add: domain_closed range_closed is_field_def field_def)

   906

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

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

   909 by (simp add: domain_closed range_closed Un_closed field_def)

   910

   911

   912 subsubsection{*Relations, functions and application*}

   913

   914 lemma (in M_axioms) relation_abs [simp]:

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

   916 apply (simp add: is_relation_def relation_def)

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

   918 done

   919

   920 lemma (in M_axioms) function_abs [simp]:

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

   922 apply (simp add: is_function_def function_def, safe)

   923    apply (frule transM, assumption)

   924   apply (blast dest: pair_components_in_M)+

   925 done

   926

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

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

   929 by (simp add: apply_def)

   930

   931 lemma (in M_axioms) apply_abs:

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

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

   934 apply (simp add: fun_apply_def)

   935 apply (blast intro: function_apply_equality function_apply_Pair)

   936 done

   937

   938 lemma (in M_axioms) typed_apply_abs:

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

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

   941 by (simp add: apply_abs fun_is_function domain_of_fun)

   942

   943 lemma (in M_axioms) typed_function_abs [simp]:

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

   945 apply (auto simp add: typed_function_def relation_def Pi_iff)

   946 apply (blast dest: pair_components_in_M)+

   947 done

   948

   949 lemma (in M_axioms) injection_abs [simp]:

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

   951 apply (simp add: injection_def apply_iff inj_def apply_closed)

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

   953 done

   954

   955 lemma (in M_axioms) surjection_abs [simp]:

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

   957 by (simp add: typed_apply_abs surjection_def surj_def)

   958

   959 lemma (in M_axioms) bijection_abs [simp]:

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

   961 by (simp add: bijection_def bij_def)

   962

   963

   964 subsubsection{*Composition of relations*}

   965

   966 lemma (in M_axioms) M_comp_iff:

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

   968       ==> r O s =

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

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

   971 apply (simp add: comp_def)

   972 apply (rule equalityI)

   973  apply clarify

   974  apply simp

   975  apply  (blast dest:  transM)+

   976 done

   977

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

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

   980 apply (simp add: M_comp_iff)

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

   982 done

   983

   984 lemma (in M_axioms) composition_abs [simp]:

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

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

   987 apply safe

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

   989  prefer 2

   990  apply (simp add: composition_def comp_def)

   991  apply (blast dest: transM)

   992 txt{*Opposite implication*}

   993 apply (rule M_equalityI)

   994   apply (simp add: composition_def comp_def)

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

   996 done

   997

   998 text{*no longer needed*}

   999 lemma (in M_axioms) restriction_is_function:

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

  1001       ==> function(z)"

  1002 apply (rotate_tac 1)

  1003 apply (simp add: restriction_def ball_iff_equiv)

  1004 apply (unfold function_def, blast)

  1005 done

  1006

  1007 lemma (in M_axioms) restriction_abs [simp]:

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

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

  1010 apply (simp add: ball_iff_equiv restriction_def restrict_def)

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

  1012 done

  1013

  1014

  1015 lemma (in M_axioms) M_restrict_iff:

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

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

  1018

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

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

  1021 apply (simp add: M_restrict_iff)

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

  1023 done

  1024

  1025 lemma (in M_axioms) Inter_abs [simp]:

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

  1027 apply (simp add: big_inter_def Inter_def)

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

  1029 done

  1030

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

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

  1033 by (insert Inter_separation, simp add: Inter_def)

  1034

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

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

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

  1038 apply (frule Inter_closed, force+)

  1039 done

  1040

  1041 subsubsection{*Functions and function space*}

  1042

  1043 text{*M contains all finite functions*}

  1044 lemma (in M_axioms) finite_fun_closed_lemma [rule_format]:

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

  1046 apply (induct_tac n, simp)

  1047 apply (rule ballI)

  1048 apply (simp add: succ_def)

  1049 apply (frule fun_cons_restrict_eq)

  1050 apply (erule ssubst)

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

  1052  apply (simp add: cons_closed nat_into_M apply_closed)

  1053 apply (blast intro: apply_funtype transM restrict_type2)

  1054 done

  1055

  1056 lemma (in M_axioms) finite_fun_closed [rule_format]:

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

  1058 by (blast intro: finite_fun_closed_lemma)

  1059

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

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

  1062 lemma (in M_axioms) is_funspace_abs [simp]:

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

  1064 apply (simp add: is_funspace_def)

  1065 apply (rule iffI)

  1066  prefer 2 apply blast

  1067 apply (rule M_equalityI)

  1068   apply simp_all

  1069 done

  1070

  1071 lemma (in M_axioms) succ_fun_eq2:

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

  1073       succ(n) -> B =

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

  1075 apply (simp add: succ_fun_eq)

  1076 apply (blast dest: transM)

  1077 done

  1078

  1079 lemma (in M_axioms) funspace_succ:

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

  1081 apply (insert funspace_succ_replacement [of n], simp)

  1082 apply (force simp add: succ_fun_eq2 univalent_def)

  1083 done

  1084

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

  1086 absoluteness of transitive closure.*}

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

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

  1089 apply (induct_tac n, simp)

  1090 apply (simp add: funspace_succ nat_into_M)

  1091 done

  1092

  1093 end