src/ZF/Constructible/Relative.thy
author ballarin
Thu Dec 11 18:30:26 2008 +0100 (2008-12-11)
changeset 29223 e09c53289830
parent 22710 f44439cdce77
child 32960 69916a850301
permissions -rw-r--r--
Conversion of HOL-Main and ZF to new locales.
     1 (*  Title:      ZF/Constructible/Relative.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4 *)
     5 
     6 header {*Relativization and Absoluteness*}
     7 
     8 theory Relative imports Main begin
     9 
    10 subsection{* Relativized versions of standard set-theoretic concepts *}
    11 
    12 definition
    13   empty :: "[i=>o,i] => o" where
    14     "empty(M,z) == \<forall>x[M]. x \<notin> z"
    15 
    16 definition
    17   subset :: "[i=>o,i,i] => o" where
    18     "subset(M,A,B) == \<forall>x[M]. x\<in>A --> x \<in> B"
    19 
    20 definition
    21   upair :: "[i=>o,i,i,i] => o" where
    22     "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x[M]. x\<in>z --> x = a | x = b)"
    23 
    24 definition
    25   pair :: "[i=>o,i,i,i] => o" where
    26     "pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) &
    27                      (\<exists>y[M]. upair(M,a,b,y) & upair(M,x,y,z))"
    28 
    29 
    30 definition
    31   union :: "[i=>o,i,i,i] => o" where
    32     "union(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a | x \<in> b"
    33 
    34 definition
    35   is_cons :: "[i=>o,i,i,i] => o" where
    36     "is_cons(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & union(M,x,b,z)"
    37 
    38 definition
    39   successor :: "[i=>o,i,i] => o" where
    40     "successor(M,a,z) == is_cons(M,a,a,z)"
    41 
    42 definition
    43   number1 :: "[i=>o,i] => o" where
    44     "number1(M,a) == \<exists>x[M]. empty(M,x) & successor(M,x,a)"
    45 
    46 definition
    47   number2 :: "[i=>o,i] => o" where
    48     "number2(M,a) == \<exists>x[M]. number1(M,x) & successor(M,x,a)"
    49 
    50 definition
    51   number3 :: "[i=>o,i] => o" where
    52     "number3(M,a) == \<exists>x[M]. number2(M,x) & successor(M,x,a)"
    53 
    54 definition
    55   powerset :: "[i=>o,i,i] => o" where
    56     "powerset(M,A,z) == \<forall>x[M]. x \<in> z <-> subset(M,x,A)"
    57 
    58 definition
    59   is_Collect :: "[i=>o,i,i=>o,i] => o" where
    60     "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z <-> x \<in> A & P(x)"
    61 
    62 definition
    63   is_Replace :: "[i=>o,i,[i,i]=>o,i] => o" where
    64     "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & P(x,u))"
    65 
    66 definition
    67   inter :: "[i=>o,i,i,i] => o" where
    68     "inter(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<in> b"
    69 
    70 definition
    71   setdiff :: "[i=>o,i,i,i] => o" where
    72     "setdiff(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<notin> b"
    73 
    74 definition
    75   big_union :: "[i=>o,i,i] => o" where
    76     "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)"
    77 
    78 definition
    79   big_inter :: "[i=>o,i,i] => o" where
    80     "big_inter(M,A,z) ==
    81              (A=0 --> z=0) &
    82 	     (A\<noteq>0 --> (\<forall>x[M]. x \<in> z <-> (\<forall>y[M]. y\<in>A --> x \<in> y)))"
    83 
    84 definition
    85   cartprod :: "[i=>o,i,i,i] => o" where
    86     "cartprod(M,A,B,z) ==
    87 	\<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))"
    88 
    89 definition
    90   is_sum :: "[i=>o,i,i,i] => o" where
    91     "is_sum(M,A,B,Z) ==
    92        \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M].
    93        number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
    94        cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"
    95 
    96 definition
    97   is_Inl :: "[i=>o,i,i] => o" where
    98     "is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z)"
    99 
   100 definition
   101   is_Inr :: "[i=>o,i,i] => o" where
   102     "is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z)"
   103 
   104 definition
   105   is_converse :: "[i=>o,i,i] => o" where
   106     "is_converse(M,r,z) ==
   107 	\<forall>x[M]. x \<in> z <->
   108              (\<exists>w[M]. w\<in>r & (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x)))"
   109 
   110 definition
   111   pre_image :: "[i=>o,i,i,i] => o" where
   112     "pre_image(M,r,A,z) ==
   113 	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))"
   114 
   115 definition
   116   is_domain :: "[i=>o,i,i] => o" where
   117     "is_domain(M,r,z) ==
   118 	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w)))"
   119 
   120 definition
   121   image :: "[i=>o,i,i,i] => o" where
   122     "image(M,r,A,z) ==
   123         \<forall>y[M]. y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w)))"
   124 
   125 definition
   126   is_range :: "[i=>o,i,i] => o" where
   127     --{*the cleaner
   128       @{term "\<exists>r'[M]. is_converse(M,r,r') & is_domain(M,r',z)"}
   129       unfortunately needs an instance of separation in order to prove
   130         @{term "M(converse(r))"}.*}
   131     "is_range(M,r,z) ==
   132 	\<forall>y[M]. y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w)))"
   133 
   134 definition
   135   is_field :: "[i=>o,i,i] => o" where
   136     "is_field(M,r,z) ==
   137 	\<exists>dr[M]. \<exists>rr[M]. is_domain(M,r,dr) & is_range(M,r,rr) &
   138                         union(M,dr,rr,z)"
   139 
   140 definition
   141   is_relation :: "[i=>o,i] => o" where
   142     "is_relation(M,r) ==
   143         (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))"
   144 
   145 definition
   146   is_function :: "[i=>o,i] => o" where
   147     "is_function(M,r) ==
   148 	\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].
   149            pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'"
   150 
   151 definition
   152   fun_apply :: "[i=>o,i,i,i] => o" where
   153     "fun_apply(M,f,x,y) ==
   154         (\<exists>xs[M]. \<exists>fxs[M].
   155          upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))"
   156 
   157 definition
   158   typed_function :: "[i=>o,i,i,i] => o" where
   159     "typed_function(M,A,B,r) ==
   160         is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
   161         (\<forall>u[M]. u\<in>r --> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) --> y\<in>B))"
   162 
   163 definition
   164   is_funspace :: "[i=>o,i,i,i] => o" where
   165     "is_funspace(M,A,B,F) ==
   166         \<forall>f[M]. f \<in> F <-> typed_function(M,A,B,f)"
   167 
   168 definition
   169   composition :: "[i=>o,i,i,i] => o" where
   170     "composition(M,r,s,t) ==
   171         \<forall>p[M]. p \<in> t <->
   172                (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
   173                 pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) &
   174                 xy \<in> s & yz \<in> r)"
   175 
   176 definition
   177   injection :: "[i=>o,i,i,i] => o" where
   178     "injection(M,A,B,f) ==
   179 	typed_function(M,A,B,f) &
   180         (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M].
   181           pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> x=x')"
   182 
   183 definition
   184   surjection :: "[i=>o,i,i,i] => o" where
   185     "surjection(M,A,B,f) ==
   186         typed_function(M,A,B,f) &
   187         (\<forall>y[M]. y\<in>B --> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))"
   188 
   189 definition
   190   bijection :: "[i=>o,i,i,i] => o" where
   191     "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)"
   192 
   193 definition
   194   restriction :: "[i=>o,i,i,i] => o" where
   195     "restriction(M,r,A,z) ==
   196 	\<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))"
   197 
   198 definition
   199   transitive_set :: "[i=>o,i] => o" where
   200     "transitive_set(M,a) == \<forall>x[M]. x\<in>a --> subset(M,x,a)"
   201 
   202 definition
   203   ordinal :: "[i=>o,i] => o" where
   204      --{*an ordinal is a transitive set of transitive sets*}
   205     "ordinal(M,a) == transitive_set(M,a) & (\<forall>x[M]. x\<in>a --> transitive_set(M,x))"
   206 
   207 definition
   208   limit_ordinal :: "[i=>o,i] => o" where
   209     --{*a limit ordinal is a non-empty, successor-closed ordinal*}
   210     "limit_ordinal(M,a) ==
   211 	ordinal(M,a) & ~ empty(M,a) &
   212         (\<forall>x[M]. x\<in>a --> (\<exists>y[M]. y\<in>a & successor(M,x,y)))"
   213 
   214 definition
   215   successor_ordinal :: "[i=>o,i] => o" where
   216     --{*a successor ordinal is any ordinal that is neither empty nor limit*}
   217     "successor_ordinal(M,a) ==
   218 	ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)"
   219 
   220 definition
   221   finite_ordinal :: "[i=>o,i] => o" where
   222     --{*an ordinal is finite if neither it nor any of its elements are limit*}
   223     "finite_ordinal(M,a) ==
   224 	ordinal(M,a) & ~ limit_ordinal(M,a) &
   225         (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
   226 
   227 definition
   228   omega :: "[i=>o,i] => o" where
   229     --{*omega is a limit ordinal none of whose elements are limit*}
   230     "omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
   231 
   232 definition
   233   is_quasinat :: "[i=>o,i] => o" where
   234     "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))"
   235 
   236 definition
   237   is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o" where
   238     "is_nat_case(M, a, is_b, k, z) ==
   239        (empty(M,k) --> z=a) &
   240        (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
   241        (is_quasinat(M,k) | empty(M,z))"
   242 
   243 definition
   244   relation1 :: "[i=>o, [i,i]=>o, i=>i] => o" where
   245     "relation1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) <-> y = f(x)"
   246 
   247 definition
   248   Relation1 :: "[i=>o, i, [i,i]=>o, i=>i] => o" where
   249     --{*as above, but typed*}
   250     "Relation1(M,A,is_f,f) ==
   251         \<forall>x[M]. \<forall>y[M]. x\<in>A --> is_f(x,y) <-> y = f(x)"
   252 
   253 definition
   254   relation2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o" where
   255     "relation2(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) <-> z = f(x,y)"
   256 
   257 definition
   258   Relation2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o" where
   259     "Relation2(M,A,B,is_f,f) ==
   260         \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. x\<in>A --> y\<in>B --> is_f(x,y,z) <-> z = f(x,y)"
   261 
   262 definition
   263   relation3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o" where
   264     "relation3(M,is_f,f) ==
   265        \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. is_f(x,y,z,u) <-> u = f(x,y,z)"
   266 
   267 definition
   268   Relation3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o" where
   269     "Relation3(M,A,B,C,is_f,f) ==
   270        \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M].
   271          x\<in>A --> y\<in>B --> z\<in>C --> is_f(x,y,z,u) <-> u = f(x,y,z)"
   272 
   273 definition
   274   relation4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o" where
   275     "relation4(M,is_f,f) ==
   276        \<forall>u[M]. \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>a[M]. is_f(u,x,y,z,a) <-> a = f(u,x,y,z)"
   277 
   278 
   279 text{*Useful when absoluteness reasoning has replaced the predicates by terms*}
   280 lemma triv_Relation1:
   281      "Relation1(M, A, \<lambda>x y. y = f(x), f)"
   282 by (simp add: Relation1_def)
   283 
   284 lemma triv_Relation2:
   285      "Relation2(M, A, B, \<lambda>x y a. a = f(x,y), f)"
   286 by (simp add: Relation2_def)
   287 
   288 
   289 subsection {*The relativized ZF axioms*}
   290 
   291 definition
   292   extensionality :: "(i=>o) => o" where
   293     "extensionality(M) ==
   294 	\<forall>x[M]. \<forall>y[M]. (\<forall>z[M]. z \<in> x <-> z \<in> y) --> x=y"
   295 
   296 definition
   297   separation :: "[i=>o, i=>o] => o" where
   298     --{*The formula @{text P} should only involve parameters
   299         belonging to @{text M} and all its quantifiers must be relativized
   300         to @{text M}.  We do not have separation as a scheme; every instance
   301         that we need must be assumed (and later proved) separately.*}
   302     "separation(M,P) ==
   303 	\<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
   304 
   305 definition
   306   upair_ax :: "(i=>o) => o" where
   307     "upair_ax(M) == \<forall>x[M]. \<forall>y[M]. \<exists>z[M]. upair(M,x,y,z)"
   308 
   309 definition
   310   Union_ax :: "(i=>o) => o" where
   311     "Union_ax(M) == \<forall>x[M]. \<exists>z[M]. big_union(M,x,z)"
   312 
   313 definition
   314   power_ax :: "(i=>o) => o" where
   315     "power_ax(M) == \<forall>x[M]. \<exists>z[M]. powerset(M,x,z)"
   316 
   317 definition
   318   univalent :: "[i=>o, i, [i,i]=>o] => o" where
   319     "univalent(M,A,P) ==
   320 	\<forall>x[M]. x\<in>A --> (\<forall>y[M]. \<forall>z[M]. P(x,y) & P(x,z) --> y=z)"
   321 
   322 definition
   323   replacement :: "[i=>o, [i,i]=>o] => o" where
   324     "replacement(M,P) ==
   325       \<forall>A[M]. univalent(M,A,P) -->
   326       (\<exists>Y[M]. \<forall>b[M]. (\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y)"
   327 
   328 definition
   329   strong_replacement :: "[i=>o, [i,i]=>o] => o" where
   330     "strong_replacement(M,P) ==
   331       \<forall>A[M]. univalent(M,A,P) -->
   332       (\<exists>Y[M]. \<forall>b[M]. b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b)))"
   333 
   334 definition
   335   foundation_ax :: "(i=>o) => o" where
   336     "foundation_ax(M) ==
   337 	\<forall>x[M]. (\<exists>y[M]. y\<in>x) --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & z \<in> y))"
   338 
   339 
   340 subsection{*A trivial consistency proof for $V_\omega$ *}
   341 
   342 text{*We prove that $V_\omega$
   343       (or @{text univ} in Isabelle) satisfies some ZF axioms.
   344      Kunen, Theorem IV 3.13, page 123.*}
   345 
   346 lemma univ0_downwards_mem: "[| y \<in> x; x \<in> univ(0) |] ==> y \<in> univ(0)"
   347 apply (insert Transset_univ [OF Transset_0])
   348 apply (simp add: Transset_def, blast)
   349 done
   350 
   351 lemma univ0_Ball_abs [simp]:
   352      "A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) --> P(x)) <-> (\<forall>x\<in>A. P(x))"
   353 by (blast intro: univ0_downwards_mem)
   354 
   355 lemma univ0_Bex_abs [simp]:
   356      "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) <-> (\<exists>x\<in>A. P(x))"
   357 by (blast intro: univ0_downwards_mem)
   358 
   359 text{*Congruence rule for separation: can assume the variable is in @{text M}*}
   360 lemma separation_cong [cong]:
   361      "(!!x. M(x) ==> P(x) <-> P'(x))
   362       ==> separation(M, %x. P(x)) <-> separation(M, %x. P'(x))"
   363 by (simp add: separation_def)
   364 
   365 lemma univalent_cong [cong]:
   366      "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |]
   367       ==> univalent(M, A, %x y. P(x,y)) <-> univalent(M, A', %x y. P'(x,y))"
   368 by (simp add: univalent_def)
   369 
   370 lemma univalent_triv [intro,simp]:
   371      "univalent(M, A, \<lambda>x y. y = f(x))"
   372 by (simp add: univalent_def)
   373 
   374 lemma univalent_conjI2 [intro,simp]:
   375      "univalent(M,A,Q) ==> univalent(M, A, \<lambda>x y. P(x,y) & Q(x,y))"
   376 by (simp add: univalent_def, blast)
   377 
   378 text{*Congruence rule for replacement*}
   379 lemma strong_replacement_cong [cong]:
   380      "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |]
   381       ==> strong_replacement(M, %x y. P(x,y)) <->
   382           strong_replacement(M, %x y. P'(x,y))"
   383 by (simp add: strong_replacement_def)
   384 
   385 text{*The extensionality axiom*}
   386 lemma "extensionality(\<lambda>x. x \<in> univ(0))"
   387 apply (simp add: extensionality_def)
   388 apply (blast intro: univ0_downwards_mem)
   389 done
   390 
   391 text{*The separation axiom requires some lemmas*}
   392 lemma Collect_in_Vfrom:
   393      "[| X \<in> Vfrom(A,j);  Transset(A) |] ==> Collect(X,P) \<in> Vfrom(A, succ(j))"
   394 apply (drule Transset_Vfrom)
   395 apply (rule subset_mem_Vfrom)
   396 apply (unfold Transset_def, blast)
   397 done
   398 
   399 lemma Collect_in_VLimit:
   400      "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]
   401       ==> Collect(X,P) \<in> Vfrom(A,i)"
   402 apply (rule Limit_VfromE, assumption+)
   403 apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom)
   404 done
   405 
   406 lemma Collect_in_univ:
   407      "[| X \<in> univ(A);  Transset(A) |] ==> Collect(X,P) \<in> univ(A)"
   408 by (simp add: univ_def Collect_in_VLimit Limit_nat)
   409 
   410 lemma "separation(\<lambda>x. x \<in> univ(0), P)"
   411 apply (simp add: separation_def, clarify)
   412 apply (rule_tac x = "Collect(z,P)" in bexI)
   413 apply (blast intro: Collect_in_univ Transset_0)+
   414 done
   415 
   416 text{*Unordered pairing axiom*}
   417 lemma "upair_ax(\<lambda>x. x \<in> univ(0))"
   418 apply (simp add: upair_ax_def upair_def)
   419 apply (blast intro: doubleton_in_univ)
   420 done
   421 
   422 text{*Union axiom*}
   423 lemma "Union_ax(\<lambda>x. x \<in> univ(0))"
   424 apply (simp add: Union_ax_def big_union_def, clarify)
   425 apply (rule_tac x="\<Union>x" in bexI)
   426  apply (blast intro: univ0_downwards_mem)
   427 apply (blast intro: Union_in_univ Transset_0)
   428 done
   429 
   430 text{*Powerset axiom*}
   431 
   432 lemma Pow_in_univ:
   433      "[| X \<in> univ(A);  Transset(A) |] ==> Pow(X) \<in> univ(A)"
   434 apply (simp add: univ_def Pow_in_VLimit Limit_nat)
   435 done
   436 
   437 lemma "power_ax(\<lambda>x. x \<in> univ(0))"
   438 apply (simp add: power_ax_def powerset_def subset_def, clarify)
   439 apply (rule_tac x="Pow(x)" in bexI)
   440  apply (blast intro: univ0_downwards_mem)
   441 apply (blast intro: Pow_in_univ Transset_0)
   442 done
   443 
   444 text{*Foundation axiom*}
   445 lemma "foundation_ax(\<lambda>x. x \<in> univ(0))"
   446 apply (simp add: foundation_ax_def, clarify)
   447 apply (cut_tac A=x in foundation)
   448 apply (blast intro: univ0_downwards_mem)
   449 done
   450 
   451 lemma "replacement(\<lambda>x. x \<in> univ(0), P)"
   452 apply (simp add: replacement_def, clarify)
   453 oops
   454 text{*no idea: maybe prove by induction on the rank of A?*}
   455 
   456 text{*Still missing: Replacement, Choice*}
   457 
   458 subsection{*Lemmas Needed to Reduce Some Set Constructions to Instances
   459       of Separation*}
   460 
   461 lemma image_iff_Collect: "r `` A = {y \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=<x,y>}"
   462 apply (rule equalityI, auto)
   463 apply (simp add: Pair_def, blast)
   464 done
   465 
   466 lemma vimage_iff_Collect:
   467      "r -`` A = {x \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=<x,y>}"
   468 apply (rule equalityI, auto)
   469 apply (simp add: Pair_def, blast)
   470 done
   471 
   472 text{*These two lemmas lets us prove @{text domain_closed} and
   473       @{text range_closed} without new instances of separation*}
   474 
   475 lemma domain_eq_vimage: "domain(r) = r -`` Union(Union(r))"
   476 apply (rule equalityI, auto)
   477 apply (rule vimageI, assumption)
   478 apply (simp add: Pair_def, blast)
   479 done
   480 
   481 lemma range_eq_image: "range(r) = r `` Union(Union(r))"
   482 apply (rule equalityI, auto)
   483 apply (rule imageI, assumption)
   484 apply (simp add: Pair_def, blast)
   485 done
   486 
   487 lemma replacementD:
   488     "[| replacement(M,P); M(A);  univalent(M,A,P) |]
   489      ==> \<exists>Y[M]. (\<forall>b[M]. ((\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y))"
   490 by (simp add: replacement_def)
   491 
   492 lemma strong_replacementD:
   493     "[| strong_replacement(M,P); M(A);  univalent(M,A,P) |]
   494      ==> \<exists>Y[M]. (\<forall>b[M]. (b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b))))"
   495 by (simp add: strong_replacement_def)
   496 
   497 lemma separationD:
   498     "[| separation(M,P); M(z) |] ==> \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
   499 by (simp add: separation_def)
   500 
   501 
   502 text{*More constants, for order types*}
   503 
   504 definition
   505   order_isomorphism :: "[i=>o,i,i,i,i,i] => o" where
   506     "order_isomorphism(M,A,r,B,s,f) ==
   507         bijection(M,A,B,f) &
   508         (\<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A -->
   509           (\<forall>p[M]. \<forall>fx[M]. \<forall>fy[M]. \<forall>q[M].
   510             pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) -->
   511             pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))))"
   512 
   513 definition
   514   pred_set :: "[i=>o,i,i,i,i] => o" where
   515     "pred_set(M,A,x,r,B) ==
   516 	\<forall>y[M]. y \<in> B <-> (\<exists>p[M]. p\<in>r & y \<in> A & pair(M,y,x,p))"
   517 
   518 definition
   519   membership :: "[i=>o,i,i] => o" where --{*membership relation*}
   520     "membership(M,A,r) ==
   521 	\<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)))"
   522 
   523 
   524 subsection{*Introducing a Transitive Class Model*}
   525 
   526 text{*The class M is assumed to be transitive and to satisfy some
   527       relativized ZF axioms*}
   528 locale M_trivial =
   529   fixes M
   530   assumes transM:           "[| y\<in>x; M(x) |] ==> M(y)"
   531       and upair_ax:	    "upair_ax(M)"
   532       and Union_ax:	    "Union_ax(M)"
   533       and power_ax:         "power_ax(M)"
   534       and replacement:      "replacement(M,P)"
   535       and M_nat [iff]:      "M(nat)"           (*i.e. the axiom of infinity*)
   536 
   537 
   538 text{*Automatically discovers the proof using @{text transM}, @{text nat_0I}
   539 and @{text M_nat}.*}
   540 lemma (in M_trivial) nonempty [simp]: "M(0)"
   541 by (blast intro: transM)
   542 
   543 lemma (in M_trivial) rall_abs [simp]:
   544      "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))"
   545 by (blast intro: transM)
   546 
   547 lemma (in M_trivial) rex_abs [simp]:
   548      "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))"
   549 by (blast intro: transM)
   550 
   551 lemma (in M_trivial) ball_iff_equiv:
   552      "M(A) ==> (\<forall>x[M]. (x\<in>A <-> P(x))) <->
   553                (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)"
   554 by (blast intro: transM)
   555 
   556 text{*Simplifies proofs of equalities when there's an iff-equality
   557       available for rewriting, universally quantified over M.  
   558       But it's not the only way to prove such equalities: its
   559       premises @{term "M(A)"} and  @{term "M(B)"} can be too strong.*}
   560 lemma (in M_trivial) M_equalityI:
   561      "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"
   562 by (blast intro!: equalityI dest: transM)
   563 
   564 
   565 subsubsection{*Trivial Absoluteness Proofs: Empty Set, Pairs, etc.*}
   566 
   567 lemma (in M_trivial) empty_abs [simp]:
   568      "M(z) ==> empty(M,z) <-> z=0"
   569 apply (simp add: empty_def)
   570 apply (blast intro: transM)
   571 done
   572 
   573 lemma (in M_trivial) subset_abs [simp]:
   574      "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"
   575 apply (simp add: subset_def)
   576 apply (blast intro: transM)
   577 done
   578 
   579 lemma (in M_trivial) upair_abs [simp]:
   580      "M(z) ==> upair(M,a,b,z) <-> z={a,b}"
   581 apply (simp add: upair_def)
   582 apply (blast intro: transM)
   583 done
   584 
   585 lemma (in M_trivial) upair_in_M_iff [iff]:
   586      "M({a,b}) <-> M(a) & M(b)"
   587 apply (insert upair_ax, simp add: upair_ax_def)
   588 apply (blast intro: transM)
   589 done
   590 
   591 lemma (in M_trivial) singleton_in_M_iff [iff]:
   592      "M({a}) <-> M(a)"
   593 by (insert upair_in_M_iff [of a a], simp)
   594 
   595 lemma (in M_trivial) pair_abs [simp]:
   596      "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"
   597 apply (simp add: pair_def ZF.Pair_def)
   598 apply (blast intro: transM)
   599 done
   600 
   601 lemma (in M_trivial) pair_in_M_iff [iff]:
   602      "M(<a,b>) <-> M(a) & M(b)"
   603 by (simp add: ZF.Pair_def)
   604 
   605 lemma (in M_trivial) pair_components_in_M:
   606      "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
   607 apply (simp add: Pair_def)
   608 apply (blast dest: transM)
   609 done
   610 
   611 lemma (in M_trivial) cartprod_abs [simp]:
   612      "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
   613 apply (simp add: cartprod_def)
   614 apply (rule iffI)
   615  apply (blast intro!: equalityI intro: transM dest!: rspec)
   616 apply (blast dest: transM)
   617 done
   618 
   619 subsubsection{*Absoluteness for Unions and Intersections*}
   620 
   621 lemma (in M_trivial) union_abs [simp]:
   622      "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
   623 apply (simp add: union_def)
   624 apply (blast intro: transM)
   625 done
   626 
   627 lemma (in M_trivial) inter_abs [simp]:
   628      "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"
   629 apply (simp add: inter_def)
   630 apply (blast intro: transM)
   631 done
   632 
   633 lemma (in M_trivial) setdiff_abs [simp]:
   634      "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"
   635 apply (simp add: setdiff_def)
   636 apply (blast intro: transM)
   637 done
   638 
   639 lemma (in M_trivial) Union_abs [simp]:
   640      "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"
   641 apply (simp add: big_union_def)
   642 apply (blast intro!: equalityI dest: transM)
   643 done
   644 
   645 lemma (in M_trivial) Union_closed [intro,simp]:
   646      "M(A) ==> M(Union(A))"
   647 by (insert Union_ax, simp add: Union_ax_def)
   648 
   649 lemma (in M_trivial) Un_closed [intro,simp]:
   650      "[| M(A); M(B) |] ==> M(A Un B)"
   651 by (simp only: Un_eq_Union, blast)
   652 
   653 lemma (in M_trivial) cons_closed [intro,simp]:
   654      "[| M(a); M(A) |] ==> M(cons(a,A))"
   655 by (subst cons_eq [symmetric], blast)
   656 
   657 lemma (in M_trivial) cons_abs [simp]:
   658      "[| M(b); M(z) |] ==> is_cons(M,a,b,z) <-> z = cons(a,b)"
   659 by (simp add: is_cons_def, blast intro: transM)
   660 
   661 lemma (in M_trivial) successor_abs [simp]:
   662      "[| M(a); M(z) |] ==> successor(M,a,z) <-> z = succ(a)"
   663 by (simp add: successor_def, blast)
   664 
   665 lemma (in M_trivial) succ_in_M_iff [iff]:
   666      "M(succ(a)) <-> M(a)"
   667 apply (simp add: succ_def)
   668 apply (blast intro: transM)
   669 done
   670 
   671 subsubsection{*Absoluteness for Separation and Replacement*}
   672 
   673 lemma (in M_trivial) separation_closed [intro,simp]:
   674      "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
   675 apply (insert separation, simp add: separation_def)
   676 apply (drule rspec, assumption, clarify)
   677 apply (subgoal_tac "y = Collect(A,P)", blast)
   678 apply (blast dest: transM)
   679 done
   680 
   681 lemma separation_iff:
   682      "separation(M,P) <-> (\<forall>z[M]. \<exists>y[M]. is_Collect(M,z,P,y))"
   683 by (simp add: separation_def is_Collect_def)
   684 
   685 lemma (in M_trivial) Collect_abs [simp]:
   686      "[| M(A); M(z) |] ==> is_Collect(M,A,P,z) <-> z = Collect(A,P)"
   687 apply (simp add: is_Collect_def)
   688 apply (blast intro!: equalityI dest: transM)
   689 done
   690 
   691 text{*Probably the premise and conclusion are equivalent*}
   692 lemma (in M_trivial) strong_replacementI [rule_format]:
   693     "[| \<forall>B[M]. separation(M, %u. \<exists>x[M]. x\<in>B & P(x,u)) |]
   694      ==> strong_replacement(M,P)"
   695 apply (simp add: strong_replacement_def, clarify)
   696 apply (frule replacementD [OF replacement], assumption, clarify)
   697 apply (drule_tac x=A in rspec, clarify)
   698 apply (drule_tac z=Y in separationD, assumption, clarify)
   699 apply (rule_tac x=y in rexI, force, assumption)
   700 done
   701 
   702 subsubsection{*The Operator @{term is_Replace}*}
   703 
   704 
   705 lemma is_Replace_cong [cong]:
   706      "[| A=A';
   707          !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y);
   708          z=z' |]
   709       ==> is_Replace(M, A, %x y. P(x,y), z) <->
   710           is_Replace(M, A', %x y. P'(x,y), z')"
   711 by (simp add: is_Replace_def)
   712 
   713 lemma (in M_trivial) univalent_Replace_iff:
   714      "[| M(A); univalent(M,A,P);
   715          !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |]
   716       ==> u \<in> Replace(A,P) <-> (\<exists>x. x\<in>A & P(x,u))"
   717 apply (simp add: Replace_iff univalent_def)
   718 apply (blast dest: transM)
   719 done
   720 
   721 (*The last premise expresses that P takes M to M*)
   722 lemma (in M_trivial) strong_replacement_closed [intro,simp]:
   723      "[| strong_replacement(M,P); M(A); univalent(M,A,P);
   724          !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] ==> M(Replace(A,P))"
   725 apply (simp add: strong_replacement_def)
   726 apply (drule_tac x=A in rspec, safe)
   727 apply (subgoal_tac "Replace(A,P) = Y")
   728  apply simp
   729 apply (rule equality_iffI)
   730 apply (simp add: univalent_Replace_iff)
   731 apply (blast dest: transM)
   732 done
   733 
   734 lemma (in M_trivial) Replace_abs:
   735      "[| M(A); M(z); univalent(M,A,P); 
   736          !!x y. [| x\<in>A; P(x,y) |] ==> M(y)  |]
   737       ==> is_Replace(M,A,P,z) <-> z = Replace(A,P)"
   738 apply (simp add: is_Replace_def)
   739 apply (rule iffI)
   740  apply (rule equality_iffI)
   741  apply (simp_all add: univalent_Replace_iff) 
   742  apply (blast dest: transM)+
   743 done
   744 
   745 
   746 (*The first premise can't simply be assumed as a schema.
   747   It is essential to take care when asserting instances of Replacement.
   748   Let K be a nonconstructible subset of nat and define
   749   f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a
   750   nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
   751   even for f : M -> M.
   752 *)
   753 lemma (in M_trivial) RepFun_closed:
   754      "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
   755       ==> M(RepFun(A,f))"
   756 apply (simp add: RepFun_def)
   757 apply (rule strong_replacement_closed)
   758 apply (auto dest: transM  simp add: univalent_def)
   759 done
   760 
   761 lemma Replace_conj_eq: "{y . x \<in> A, x\<in>A & y=f(x)} = {y . x\<in>A, y=f(x)}"
   762 by simp
   763 
   764 text{*Better than @{text RepFun_closed} when having the formula @{term "x\<in>A"}
   765       makes relativization easier.*}
   766 lemma (in M_trivial) RepFun_closed2:
   767      "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
   768       ==> M(RepFun(A, %x. f(x)))"
   769 apply (simp add: RepFun_def)
   770 apply (frule strong_replacement_closed, assumption)
   771 apply (auto dest: transM  simp add: Replace_conj_eq univalent_def)
   772 done
   773 
   774 subsubsection {*Absoluteness for @{term Lambda}*}
   775 
   776 definition
   777  is_lambda :: "[i=>o, i, [i,i]=>o, i] => o" where
   778     "is_lambda(M, A, is_b, z) ==
   779        \<forall>p[M]. p \<in> z <->
   780         (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))"
   781 
   782 lemma (in M_trivial) lam_closed:
   783      "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
   784       ==> M(\<lambda>x\<in>A. b(x))"
   785 by (simp add: lam_def, blast intro: RepFun_closed dest: transM)
   786 
   787 text{*Better than @{text lam_closed}: has the formula @{term "x\<in>A"}*}
   788 lemma (in M_trivial) lam_closed2:
   789   "[|strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
   790      M(A); \<forall>m[M]. m\<in>A --> M(b(m))|] ==> M(Lambda(A,b))"
   791 apply (simp add: lam_def)
   792 apply (blast intro: RepFun_closed2 dest: transM)
   793 done
   794 
   795 lemma (in M_trivial) lambda_abs2:
   796      "[| Relation1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |]
   797       ==> is_lambda(M,A,is_b,z) <-> z = Lambda(A,b)"
   798 apply (simp add: Relation1_def is_lambda_def)
   799 apply (rule iffI)
   800  prefer 2 apply (simp add: lam_def)
   801 apply (rule equality_iffI)
   802 apply (simp add: lam_def) 
   803 apply (rule iffI) 
   804  apply (blast dest: transM) 
   805 apply (auto simp add: transM [of _ A]) 
   806 done
   807 
   808 lemma is_lambda_cong [cong]:
   809      "[| A=A';  z=z';
   810          !!x y. [| x\<in>A; M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
   811       ==> is_lambda(M, A, %x y. is_b(x,y), z) <->
   812           is_lambda(M, A', %x y. is_b'(x,y), z')"
   813 by (simp add: is_lambda_def)
   814 
   815 lemma (in M_trivial) image_abs [simp]:
   816      "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
   817 apply (simp add: image_def)
   818 apply (rule iffI)
   819  apply (blast intro!: equalityI dest: transM, blast)
   820 done
   821 
   822 text{*What about @{text Pow_abs}?  Powerset is NOT absolute!
   823       This result is one direction of absoluteness.*}
   824 
   825 lemma (in M_trivial) powerset_Pow:
   826      "powerset(M, x, Pow(x))"
   827 by (simp add: powerset_def)
   828 
   829 text{*But we can't prove that the powerset in @{text M} includes the
   830       real powerset.*}
   831 lemma (in M_trivial) powerset_imp_subset_Pow:
   832      "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
   833 apply (simp add: powerset_def)
   834 apply (blast dest: transM)
   835 done
   836 
   837 subsubsection{*Absoluteness for the Natural Numbers*}
   838 
   839 lemma (in M_trivial) nat_into_M [intro]:
   840      "n \<in> nat ==> M(n)"
   841 by (induct n rule: nat_induct, simp_all)
   842 
   843 lemma (in M_trivial) nat_case_closed [intro,simp]:
   844   "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
   845 apply (case_tac "k=0", simp)
   846 apply (case_tac "\<exists>m. k = succ(m)", force)
   847 apply (simp add: nat_case_def)
   848 done
   849 
   850 lemma (in M_trivial) quasinat_abs [simp]:
   851      "M(z) ==> is_quasinat(M,z) <-> quasinat(z)"
   852 by (auto simp add: is_quasinat_def quasinat_def)
   853 
   854 lemma (in M_trivial) nat_case_abs [simp]:
   855      "[| relation1(M,is_b,b); M(k); M(z) |]
   856       ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
   857 apply (case_tac "quasinat(k)")
   858  prefer 2
   859  apply (simp add: is_nat_case_def non_nat_case)
   860  apply (force simp add: quasinat_def)
   861 apply (simp add: quasinat_def is_nat_case_def)
   862 apply (elim disjE exE)
   863  apply (simp_all add: relation1_def)
   864 done
   865 
   866 (*NOT for the simplifier.  The assumption M(z') is apparently necessary, but
   867   causes the error "Failed congruence proof!"  It may be better to replace
   868   is_nat_case by nat_case before attempting congruence reasoning.*)
   869 lemma is_nat_case_cong:
   870      "[| a = a'; k = k';  z = z';  M(z');
   871        !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
   872       ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"
   873 by (simp add: is_nat_case_def)
   874 
   875 
   876 subsection{*Absoluteness for Ordinals*}
   877 text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
   878 
   879 lemma (in M_trivial) lt_closed:
   880      "[| j<i; M(i) |] ==> M(j)"
   881 by (blast dest: ltD intro: transM)
   882 
   883 lemma (in M_trivial) transitive_set_abs [simp]:
   884      "M(a) ==> transitive_set(M,a) <-> Transset(a)"
   885 by (simp add: transitive_set_def Transset_def)
   886 
   887 lemma (in M_trivial) ordinal_abs [simp]:
   888      "M(a) ==> ordinal(M,a) <-> Ord(a)"
   889 by (simp add: ordinal_def Ord_def)
   890 
   891 lemma (in M_trivial) limit_ordinal_abs [simp]:
   892      "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
   893 apply (unfold Limit_def limit_ordinal_def)
   894 apply (simp add: Ord_0_lt_iff)
   895 apply (simp add: lt_def, blast)
   896 done
   897 
   898 lemma (in M_trivial) successor_ordinal_abs [simp]:
   899      "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b[M]. a = succ(b))"
   900 apply (simp add: successor_ordinal_def, safe)
   901 apply (drule Ord_cases_disj, auto)
   902 done
   903 
   904 lemma finite_Ord_is_nat:
   905       "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"
   906 by (induct a rule: trans_induct3, simp_all)
   907 
   908 lemma (in M_trivial) finite_ordinal_abs [simp]:
   909      "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
   910 apply (simp add: finite_ordinal_def)
   911 apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord
   912              dest: Ord_trans naturals_not_limit)
   913 done
   914 
   915 lemma Limit_non_Limit_implies_nat:
   916      "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"
   917 apply (rule le_anti_sym)
   918 apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)
   919  apply (simp add: lt_def)
   920  apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat)
   921 apply (erule nat_le_Limit)
   922 done
   923 
   924 lemma (in M_trivial) omega_abs [simp]:
   925      "M(a) ==> omega(M,a) <-> a = nat"
   926 apply (simp add: omega_def)
   927 apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
   928 done
   929 
   930 lemma (in M_trivial) number1_abs [simp]:
   931      "M(a) ==> number1(M,a) <-> a = 1"
   932 by (simp add: number1_def)
   933 
   934 lemma (in M_trivial) number2_abs [simp]:
   935      "M(a) ==> number2(M,a) <-> a = succ(1)"
   936 by (simp add: number2_def)
   937 
   938 lemma (in M_trivial) number3_abs [simp]:
   939      "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
   940 by (simp add: number3_def)
   941 
   942 text{*Kunen continued to 20...*}
   943 
   944 (*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything
   945   but the recursion variable must stay unchanged.  But then the recursion
   946   equations only hold for x\<in>nat (or in some other set) and not for the
   947   whole of the class M.
   948   consts
   949     natnumber_aux :: "[i=>o,i] => i"
   950 
   951   primrec
   952       "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
   953       "natnumber_aux(M,succ(n)) =
   954 	   (\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x))
   955 		     then 1 else 0)"
   956 
   957   definition
   958     natnumber :: "[i=>o,i,i] => o"
   959       "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
   960 
   961   lemma (in M_trivial) [simp]:
   962        "natnumber(M,0,x) == x=0"
   963 *)
   964 
   965 subsection{*Some instances of separation and strong replacement*}
   966 
   967 locale M_basic = M_trivial +
   968 assumes Inter_separation:
   969      "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
   970   and Diff_separation:
   971      "M(B) ==> separation(M, \<lambda>x. x \<notin> B)"
   972   and cartprod_separation:
   973      "[| M(A); M(B) |]
   974       ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,z)))"
   975   and image_separation:
   976      "[| M(A); M(r) |]
   977       ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,p)))"
   978   and converse_separation:
   979      "M(r) ==> separation(M,
   980          \<lambda>z. \<exists>p[M]. p\<in>r & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
   981   and restrict_separation:
   982      "M(A) ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. pair(M,x,y,z)))"
   983   and comp_separation:
   984      "[| M(r); M(s) |]
   985       ==> separation(M, \<lambda>xz. \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
   986 		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) &
   987                   xy\<in>s & yz\<in>r)"
   988   and pred_separation:
   989      "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & pair(M,y,x,p))"
   990   and Memrel_separation:
   991      "separation(M, \<lambda>z. \<exists>x[M]. \<exists>y[M]. pair(M,x,y,z) & x \<in> y)"
   992   and funspace_succ_replacement:
   993      "M(n) ==>
   994       strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. \<exists>cnbf[M].
   995                 pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &
   996                 upair(M,cnbf,cnbf,z))"
   997   and is_recfun_separation:
   998      --{*for well-founded recursion: used to prove @{text is_recfun_equal}*}
   999      "[| M(r); M(f); M(g); M(a); M(b) |]
  1000      ==> separation(M,
  1001             \<lambda>x. \<exists>xa[M]. \<exists>xb[M].
  1002                 pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r &
  1003                 (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) &
  1004                                    fx \<noteq> gx))"
  1005 
  1006 lemma (in M_basic) cartprod_iff_lemma:
  1007      "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}});
  1008          powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
  1009        ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
  1010 apply (simp add: powerset_def)
  1011 apply (rule equalityI, clarify, simp)
  1012  apply (frule transM, assumption)
  1013  apply (frule transM, assumption, simp (no_asm_simp))
  1014  apply blast
  1015 apply clarify
  1016 apply (frule transM, assumption, force)
  1017 done
  1018 
  1019 lemma (in M_basic) cartprod_iff:
  1020      "[| M(A); M(B); M(C) |]
  1021       ==> cartprod(M,A,B,C) <->
  1022           (\<exists>p1[M]. \<exists>p2[M]. powerset(M,A Un B,p1) & powerset(M,p1,p2) &
  1023                    C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
  1024 apply (simp add: Pair_def cartprod_def, safe)
  1025 defer 1
  1026   apply (simp add: powerset_def)
  1027  apply blast
  1028 txt{*Final, difficult case: the left-to-right direction of the theorem.*}
  1029 apply (insert power_ax, simp add: power_ax_def)
  1030 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)
  1031 apply (blast, clarify)
  1032 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)
  1033 apply assumption
  1034 apply (blast intro: cartprod_iff_lemma)
  1035 done
  1036 
  1037 lemma (in M_basic) cartprod_closed_lemma:
  1038      "[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
  1039 apply (simp del: cartprod_abs add: cartprod_iff)
  1040 apply (insert power_ax, simp add: power_ax_def)
  1041 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)
  1042 apply (blast, clarify)
  1043 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec, auto)
  1044 apply (intro rexI conjI, simp+)
  1045 apply (insert cartprod_separation [of A B], simp)
  1046 done
  1047 
  1048 text{*All the lemmas above are necessary because Powerset is not absolute.
  1049       I should have used Replacement instead!*}
  1050 lemma (in M_basic) cartprod_closed [intro,simp]:
  1051      "[| M(A); M(B) |] ==> M(A*B)"
  1052 by (frule cartprod_closed_lemma, assumption, force)
  1053 
  1054 lemma (in M_basic) sum_closed [intro,simp]:
  1055      "[| M(A); M(B) |] ==> M(A+B)"
  1056 by (simp add: sum_def)
  1057 
  1058 lemma (in M_basic) sum_abs [simp]:
  1059      "[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) <-> (Z = A+B)"
  1060 by (simp add: is_sum_def sum_def singleton_0 nat_into_M)
  1061 
  1062 lemma (in M_trivial) Inl_in_M_iff [iff]:
  1063      "M(Inl(a)) <-> M(a)"
  1064 by (simp add: Inl_def)
  1065 
  1066 lemma (in M_trivial) Inl_abs [simp]:
  1067      "M(Z) ==> is_Inl(M,a,Z) <-> (Z = Inl(a))"
  1068 by (simp add: is_Inl_def Inl_def)
  1069 
  1070 lemma (in M_trivial) Inr_in_M_iff [iff]:
  1071      "M(Inr(a)) <-> M(a)"
  1072 by (simp add: Inr_def)
  1073 
  1074 lemma (in M_trivial) Inr_abs [simp]:
  1075      "M(Z) ==> is_Inr(M,a,Z) <-> (Z = Inr(a))"
  1076 by (simp add: is_Inr_def Inr_def)
  1077 
  1078 
  1079 subsubsection {*converse of a relation*}
  1080 
  1081 lemma (in M_basic) M_converse_iff:
  1082      "M(r) ==>
  1083       converse(r) =
  1084       {z \<in> Union(Union(r)) * Union(Union(r)).
  1085        \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"
  1086 apply (rule equalityI)
  1087  prefer 2 apply (blast dest: transM, clarify, simp)
  1088 apply (simp add: Pair_def)
  1089 apply (blast dest: transM)
  1090 done
  1091 
  1092 lemma (in M_basic) converse_closed [intro,simp]:
  1093      "M(r) ==> M(converse(r))"
  1094 apply (simp add: M_converse_iff)
  1095 apply (insert converse_separation [of r], simp)
  1096 done
  1097 
  1098 lemma (in M_basic) converse_abs [simp]:
  1099      "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
  1100 apply (simp add: is_converse_def)
  1101 apply (rule iffI)
  1102  prefer 2 apply blast
  1103 apply (rule M_equalityI)
  1104   apply simp
  1105   apply (blast dest: transM)+
  1106 done
  1107 
  1108 
  1109 subsubsection {*image, preimage, domain, range*}
  1110 
  1111 lemma (in M_basic) image_closed [intro,simp]:
  1112      "[| M(A); M(r) |] ==> M(r``A)"
  1113 apply (simp add: image_iff_Collect)
  1114 apply (insert image_separation [of A r], simp)
  1115 done
  1116 
  1117 lemma (in M_basic) vimage_abs [simp]:
  1118      "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A"
  1119 apply (simp add: pre_image_def)
  1120 apply (rule iffI)
  1121  apply (blast intro!: equalityI dest: transM, blast)
  1122 done
  1123 
  1124 lemma (in M_basic) vimage_closed [intro,simp]:
  1125      "[| M(A); M(r) |] ==> M(r-``A)"
  1126 by (simp add: vimage_def)
  1127 
  1128 
  1129 subsubsection{*Domain, range and field*}
  1130 
  1131 lemma (in M_basic) domain_abs [simp]:
  1132      "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
  1133 apply (simp add: is_domain_def)
  1134 apply (blast intro!: equalityI dest: transM)
  1135 done
  1136 
  1137 lemma (in M_basic) domain_closed [intro,simp]:
  1138      "M(r) ==> M(domain(r))"
  1139 apply (simp add: domain_eq_vimage)
  1140 done
  1141 
  1142 lemma (in M_basic) range_abs [simp]:
  1143      "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
  1144 apply (simp add: is_range_def)
  1145 apply (blast intro!: equalityI dest: transM)
  1146 done
  1147 
  1148 lemma (in M_basic) range_closed [intro,simp]:
  1149      "M(r) ==> M(range(r))"
  1150 apply (simp add: range_eq_image)
  1151 done
  1152 
  1153 lemma (in M_basic) field_abs [simp]:
  1154      "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"
  1155 by (simp add: domain_closed range_closed is_field_def field_def)
  1156 
  1157 lemma (in M_basic) field_closed [intro,simp]:
  1158      "M(r) ==> M(field(r))"
  1159 by (simp add: domain_closed range_closed Un_closed field_def)
  1160 
  1161 
  1162 subsubsection{*Relations, functions and application*}
  1163 
  1164 lemma (in M_basic) relation_abs [simp]:
  1165      "M(r) ==> is_relation(M,r) <-> relation(r)"
  1166 apply (simp add: is_relation_def relation_def)
  1167 apply (blast dest!: bspec dest: pair_components_in_M)+
  1168 done
  1169 
  1170 lemma (in M_basic) function_abs [simp]:
  1171      "M(r) ==> is_function(M,r) <-> function(r)"
  1172 apply (simp add: is_function_def function_def, safe)
  1173    apply (frule transM, assumption)
  1174   apply (blast dest: pair_components_in_M)+
  1175 done
  1176 
  1177 lemma (in M_basic) apply_closed [intro,simp]:
  1178      "[|M(f); M(a)|] ==> M(f`a)"
  1179 by (simp add: apply_def)
  1180 
  1181 lemma (in M_basic) apply_abs [simp]:
  1182      "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> f`x = y"
  1183 apply (simp add: fun_apply_def apply_def, blast)
  1184 done
  1185 
  1186 lemma (in M_basic) typed_function_abs [simp]:
  1187      "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
  1188 apply (auto simp add: typed_function_def relation_def Pi_iff)
  1189 apply (blast dest: pair_components_in_M)+
  1190 done
  1191 
  1192 lemma (in M_basic) injection_abs [simp]:
  1193      "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
  1194 apply (simp add: injection_def apply_iff inj_def apply_closed)
  1195 apply (blast dest: transM [of _ A])
  1196 done
  1197 
  1198 lemma (in M_basic) surjection_abs [simp]:
  1199      "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
  1200 by (simp add: surjection_def surj_def)
  1201 
  1202 lemma (in M_basic) bijection_abs [simp]:
  1203      "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
  1204 by (simp add: bijection_def bij_def)
  1205 
  1206 
  1207 subsubsection{*Composition of relations*}
  1208 
  1209 lemma (in M_basic) M_comp_iff:
  1210      "[| M(r); M(s) |]
  1211       ==> r O s =
  1212           {xz \<in> domain(s) * range(r).
  1213             \<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}"
  1214 apply (simp add: comp_def)
  1215 apply (rule equalityI)
  1216  apply clarify
  1217  apply simp
  1218  apply  (blast dest:  transM)+
  1219 done
  1220 
  1221 lemma (in M_basic) comp_closed [intro,simp]:
  1222      "[| M(r); M(s) |] ==> M(r O s)"
  1223 apply (simp add: M_comp_iff)
  1224 apply (insert comp_separation [of r s], simp)
  1225 done
  1226 
  1227 lemma (in M_basic) composition_abs [simp]:
  1228      "[| M(r); M(s); M(t) |] ==> composition(M,r,s,t) <-> t = r O s"
  1229 apply safe
  1230  txt{*Proving @{term "composition(M, r, s, r O s)"}*}
  1231  prefer 2
  1232  apply (simp add: composition_def comp_def)
  1233  apply (blast dest: transM)
  1234 txt{*Opposite implication*}
  1235 apply (rule M_equalityI)
  1236   apply (simp add: composition_def comp_def)
  1237   apply (blast del: allE dest: transM)+
  1238 done
  1239 
  1240 text{*no longer needed*}
  1241 lemma (in M_basic) restriction_is_function:
  1242      "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |]
  1243       ==> function(z)"
  1244 apply (simp add: restriction_def ball_iff_equiv)
  1245 apply (unfold function_def, blast)
  1246 done
  1247 
  1248 lemma (in M_basic) restriction_abs [simp]:
  1249      "[| M(f); M(A); M(z) |]
  1250       ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
  1251 apply (simp add: ball_iff_equiv restriction_def restrict_def)
  1252 apply (blast intro!: equalityI dest: transM)
  1253 done
  1254 
  1255 
  1256 lemma (in M_basic) M_restrict_iff:
  1257      "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
  1258 by (simp add: restrict_def, blast dest: transM)
  1259 
  1260 lemma (in M_basic) restrict_closed [intro,simp]:
  1261      "[| M(A); M(r) |] ==> M(restrict(r,A))"
  1262 apply (simp add: M_restrict_iff)
  1263 apply (insert restrict_separation [of A], simp)
  1264 done
  1265 
  1266 lemma (in M_basic) Inter_abs [simp]:
  1267      "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
  1268 apply (simp add: big_inter_def Inter_def)
  1269 apply (blast intro!: equalityI dest: transM)
  1270 done
  1271 
  1272 lemma (in M_basic) Inter_closed [intro,simp]:
  1273      "M(A) ==> M(Inter(A))"
  1274 by (insert Inter_separation, simp add: Inter_def)
  1275 
  1276 lemma (in M_basic) Int_closed [intro,simp]:
  1277      "[| M(A); M(B) |] ==> M(A Int B)"
  1278 apply (subgoal_tac "M({A,B})")
  1279 apply (frule Inter_closed, force+)
  1280 done
  1281 
  1282 lemma (in M_basic) Diff_closed [intro,simp]:
  1283      "[|M(A); M(B)|] ==> M(A-B)"
  1284 by (insert Diff_separation, simp add: Diff_def)
  1285 
  1286 subsubsection{*Some Facts About Separation Axioms*}
  1287 
  1288 lemma (in M_basic) separation_conj:
  1289      "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) & Q(z))"
  1290 by (simp del: separation_closed
  1291          add: separation_iff Collect_Int_Collect_eq [symmetric])
  1292 
  1293 (*???equalities*)
  1294 lemma Collect_Un_Collect_eq:
  1295      "Collect(A,P) Un Collect(A,Q) = Collect(A, %x. P(x) | Q(x))"
  1296 by blast
  1297 
  1298 lemma Diff_Collect_eq:
  1299      "A - Collect(A,P) = Collect(A, %x. ~ P(x))"
  1300 by blast
  1301 
  1302 lemma (in M_trivial) Collect_rall_eq:
  1303      "M(Y) ==> Collect(A, %x. \<forall>y[M]. y\<in>Y --> P(x,y)) =
  1304                (if Y=0 then A else (\<Inter>y \<in> Y. {x \<in> A. P(x,y)}))"
  1305 apply simp
  1306 apply (blast intro!: equalityI dest: transM)
  1307 done
  1308 
  1309 lemma (in M_basic) separation_disj:
  1310      "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) | Q(z))"
  1311 by (simp del: separation_closed
  1312          add: separation_iff Collect_Un_Collect_eq [symmetric])
  1313 
  1314 lemma (in M_basic) separation_neg:
  1315      "separation(M,P) ==> separation(M, \<lambda>z. ~P(z))"
  1316 by (simp del: separation_closed
  1317          add: separation_iff Diff_Collect_eq [symmetric])
  1318 
  1319 lemma (in M_basic) separation_imp:
  1320      "[|separation(M,P); separation(M,Q)|]
  1321       ==> separation(M, \<lambda>z. P(z) --> Q(z))"
  1322 by (simp add: separation_neg separation_disj not_disj_iff_imp [symmetric])
  1323 
  1324 text{*This result is a hint of how little can be done without the Reflection
  1325   Theorem.  The quantifier has to be bounded by a set.  We also need another
  1326   instance of Separation!*}
  1327 lemma (in M_basic) separation_rall:
  1328      "[|M(Y); \<forall>y[M]. separation(M, \<lambda>x. P(x,y));
  1329         \<forall>z[M]. strong_replacement(M, \<lambda>x y. y = {u \<in> z . P(u,x)})|]
  1330       ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y --> P(x,y))"
  1331 apply (simp del: separation_closed rall_abs
  1332          add: separation_iff Collect_rall_eq)
  1333 apply (blast intro!: Inter_closed RepFun_closed dest: transM)
  1334 done
  1335 
  1336 
  1337 subsubsection{*Functions and function space*}
  1338 
  1339 text{*The assumption @{term "M(A->B)"} is unusual, but essential: in
  1340 all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
  1341 lemma (in M_basic) is_funspace_abs [simp]:
  1342      "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B";
  1343 apply (simp add: is_funspace_def)
  1344 apply (rule iffI)
  1345  prefer 2 apply blast
  1346 apply (rule M_equalityI)
  1347   apply simp_all
  1348 done
  1349 
  1350 lemma (in M_basic) succ_fun_eq2:
  1351      "[|M(B); M(n->B)|] ==>
  1352       succ(n) -> B =
  1353       \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"
  1354 apply (simp add: succ_fun_eq)
  1355 apply (blast dest: transM)
  1356 done
  1357 
  1358 lemma (in M_basic) funspace_succ:
  1359      "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)"
  1360 apply (insert funspace_succ_replacement [of n], simp)
  1361 apply (force simp add: succ_fun_eq2 univalent_def)
  1362 done
  1363 
  1364 text{*@{term M} contains all finite function spaces.  Needed to prove the
  1365 absoluteness of transitive closure.  See the definition of
  1366 @{text rtrancl_alt} in in @{text WF_absolute.thy}.*}
  1367 lemma (in M_basic) finite_funspace_closed [intro,simp]:
  1368      "[|n\<in>nat; M(B)|] ==> M(n->B)"
  1369 apply (induct_tac n, simp)
  1370 apply (simp add: funspace_succ nat_into_M)
  1371 done
  1372 
  1373 
  1374 subsection{*Relativization and Absoluteness for Boolean Operators*}
  1375 
  1376 definition
  1377   is_bool_of_o :: "[i=>o, o, i] => o" where
  1378    "is_bool_of_o(M,P,z) == (P & number1(M,z)) | (~P & empty(M,z))"
  1379 
  1380 definition
  1381   is_not :: "[i=>o, i, i] => o" where
  1382    "is_not(M,a,z) == (number1(M,a)  & empty(M,z)) |
  1383                      (~number1(M,a) & number1(M,z))"
  1384 
  1385 definition
  1386   is_and :: "[i=>o, i, i, i] => o" where
  1387    "is_and(M,a,b,z) == (number1(M,a)  & z=b) |
  1388                        (~number1(M,a) & empty(M,z))"
  1389 
  1390 definition
  1391   is_or :: "[i=>o, i, i, i] => o" where
  1392    "is_or(M,a,b,z) == (number1(M,a)  & number1(M,z)) |
  1393                       (~number1(M,a) & z=b)"
  1394 
  1395 lemma (in M_trivial) bool_of_o_abs [simp]:
  1396      "M(z) ==> is_bool_of_o(M,P,z) <-> z = bool_of_o(P)"
  1397 by (simp add: is_bool_of_o_def bool_of_o_def)
  1398 
  1399 
  1400 lemma (in M_trivial) not_abs [simp]:
  1401      "[| M(a); M(z)|] ==> is_not(M,a,z) <-> z = not(a)"
  1402 by (simp add: Bool.not_def cond_def is_not_def)
  1403 
  1404 lemma (in M_trivial) and_abs [simp]:
  1405      "[| M(a); M(b); M(z)|] ==> is_and(M,a,b,z) <-> z = a and b"
  1406 by (simp add: Bool.and_def cond_def is_and_def)
  1407 
  1408 lemma (in M_trivial) or_abs [simp]:
  1409      "[| M(a); M(b); M(z)|] ==> is_or(M,a,b,z) <-> z = a or b"
  1410 by (simp add: Bool.or_def cond_def is_or_def)
  1411 
  1412 
  1413 lemma (in M_trivial) bool_of_o_closed [intro,simp]:
  1414      "M(bool_of_o(P))"
  1415 by (simp add: bool_of_o_def)
  1416 
  1417 lemma (in M_trivial) and_closed [intro,simp]:
  1418      "[| M(p); M(q) |] ==> M(p and q)"
  1419 by (simp add: and_def cond_def)
  1420 
  1421 lemma (in M_trivial) or_closed [intro,simp]:
  1422      "[| M(p); M(q) |] ==> M(p or q)"
  1423 by (simp add: or_def cond_def)
  1424 
  1425 lemma (in M_trivial) not_closed [intro,simp]:
  1426      "M(p) ==> M(not(p))"
  1427 by (simp add: Bool.not_def cond_def)
  1428 
  1429 
  1430 subsection{*Relativization and Absoluteness for List Operators*}
  1431 
  1432 definition
  1433   is_Nil :: "[i=>o, i] => o" where
  1434      --{* because @{prop "[] \<equiv> Inl(0)"}*}
  1435     "is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs)"
  1436 
  1437 definition
  1438   is_Cons :: "[i=>o,i,i,i] => o" where
  1439      --{* because @{prop "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}*}
  1440     "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)"
  1441 
  1442 
  1443 lemma (in M_trivial) Nil_in_M [intro,simp]: "M(Nil)"
  1444 by (simp add: Nil_def)
  1445 
  1446 lemma (in M_trivial) Nil_abs [simp]: "M(Z) ==> is_Nil(M,Z) <-> (Z = Nil)"
  1447 by (simp add: is_Nil_def Nil_def)
  1448 
  1449 lemma (in M_trivial) Cons_in_M_iff [iff]: "M(Cons(a,l)) <-> M(a) & M(l)"
  1450 by (simp add: Cons_def)
  1451 
  1452 lemma (in M_trivial) Cons_abs [simp]:
  1453      "[|M(a); M(l); M(Z)|] ==> is_Cons(M,a,l,Z) <-> (Z = Cons(a,l))"
  1454 by (simp add: is_Cons_def Cons_def)
  1455 
  1456 
  1457 definition
  1458   quasilist :: "i => o" where
  1459     "quasilist(xs) == xs=Nil | (\<exists>x l. xs = Cons(x,l))"
  1460 
  1461 definition
  1462   is_quasilist :: "[i=>o,i] => o" where
  1463     "is_quasilist(M,z) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))"
  1464 
  1465 definition
  1466   list_case' :: "[i, [i,i]=>i, i] => i" where
  1467     --{*A version of @{term list_case} that's always defined.*}
  1468     "list_case'(a,b,xs) ==
  1469        if quasilist(xs) then list_case(a,b,xs) else 0"
  1470 
  1471 definition
  1472   is_list_case :: "[i=>o, i, [i,i,i]=>o, i, i] => o" where
  1473     --{*Returns 0 for non-lists*}
  1474     "is_list_case(M, a, is_b, xs, z) ==
  1475        (is_Nil(M,xs) --> z=a) &
  1476        (\<forall>x[M]. \<forall>l[M]. is_Cons(M,x,l,xs) --> is_b(x,l,z)) &
  1477        (is_quasilist(M,xs) | empty(M,z))"
  1478 
  1479 definition
  1480   hd' :: "i => i" where
  1481     --{*A version of @{term hd} that's always defined.*}
  1482     "hd'(xs) == if quasilist(xs) then hd(xs) else 0"
  1483 
  1484 definition
  1485   tl' :: "i => i" where
  1486     --{*A version of @{term tl} that's always defined.*}
  1487     "tl'(xs) == if quasilist(xs) then tl(xs) else 0"
  1488 
  1489 definition
  1490   is_hd :: "[i=>o,i,i] => o" where
  1491      --{* @{term "hd([]) = 0"} no constraints if not a list.
  1492           Avoiding implication prevents the simplifier's looping.*}
  1493     "is_hd(M,xs,H) ==
  1494        (is_Nil(M,xs) --> empty(M,H)) &
  1495        (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
  1496        (is_quasilist(M,xs) | empty(M,H))"
  1497 
  1498 definition
  1499   is_tl :: "[i=>o,i,i] => o" where
  1500      --{* @{term "tl([]) = []"}; see comments about @{term is_hd}*}
  1501     "is_tl(M,xs,T) ==
  1502        (is_Nil(M,xs) --> T=xs) &
  1503        (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
  1504        (is_quasilist(M,xs) | empty(M,T))"
  1505 
  1506 subsubsection{*@{term quasilist}: For Case-Splitting with @{term list_case'}*}
  1507 
  1508 lemma [iff]: "quasilist(Nil)"
  1509 by (simp add: quasilist_def)
  1510 
  1511 lemma [iff]: "quasilist(Cons(x,l))"
  1512 by (simp add: quasilist_def)
  1513 
  1514 lemma list_imp_quasilist: "l \<in> list(A) ==> quasilist(l)"
  1515 by (erule list.cases, simp_all)
  1516 
  1517 subsubsection{*@{term list_case'}, the Modified Version of @{term list_case}*}
  1518 
  1519 lemma list_case'_Nil [simp]: "list_case'(a,b,Nil) = a"
  1520 by (simp add: list_case'_def quasilist_def)
  1521 
  1522 lemma list_case'_Cons [simp]: "list_case'(a,b,Cons(x,l)) = b(x,l)"
  1523 by (simp add: list_case'_def quasilist_def)
  1524 
  1525 lemma non_list_case: "~ quasilist(x) ==> list_case'(a,b,x) = 0"
  1526 by (simp add: quasilist_def list_case'_def)
  1527 
  1528 lemma list_case'_eq_list_case [simp]:
  1529      "xs \<in> list(A) ==>list_case'(a,b,xs) = list_case(a,b,xs)"
  1530 by (erule list.cases, simp_all)
  1531 
  1532 lemma (in M_basic) list_case'_closed [intro,simp]:
  1533   "[|M(k); M(a); \<forall>x[M]. \<forall>y[M]. M(b(x,y))|] ==> M(list_case'(a,b,k))"
  1534 apply (case_tac "quasilist(k)")
  1535  apply (simp add: quasilist_def, force)
  1536 apply (simp add: non_list_case)
  1537 done
  1538 
  1539 lemma (in M_trivial) quasilist_abs [simp]:
  1540      "M(z) ==> is_quasilist(M,z) <-> quasilist(z)"
  1541 by (auto simp add: is_quasilist_def quasilist_def)
  1542 
  1543 lemma (in M_trivial) list_case_abs [simp]:
  1544      "[| relation2(M,is_b,b); M(k); M(z) |]
  1545       ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)"
  1546 apply (case_tac "quasilist(k)")
  1547  prefer 2
  1548  apply (simp add: is_list_case_def non_list_case)
  1549  apply (force simp add: quasilist_def)
  1550 apply (simp add: quasilist_def is_list_case_def)
  1551 apply (elim disjE exE)
  1552  apply (simp_all add: relation2_def)
  1553 done
  1554 
  1555 
  1556 subsubsection{*The Modified Operators @{term hd'} and @{term tl'}*}
  1557 
  1558 lemma (in M_trivial) is_hd_Nil: "is_hd(M,[],Z) <-> empty(M,Z)"
  1559 by (simp add: is_hd_def)
  1560 
  1561 lemma (in M_trivial) is_hd_Cons:
  1562      "[|M(a); M(l)|] ==> is_hd(M,Cons(a,l),Z) <-> Z = a"
  1563 by (force simp add: is_hd_def)
  1564 
  1565 lemma (in M_trivial) hd_abs [simp]:
  1566      "[|M(x); M(y)|] ==> is_hd(M,x,y) <-> y = hd'(x)"
  1567 apply (simp add: hd'_def)
  1568 apply (intro impI conjI)
  1569  prefer 2 apply (force simp add: is_hd_def)
  1570 apply (simp add: quasilist_def is_hd_def)
  1571 apply (elim disjE exE, auto)
  1572 done
  1573 
  1574 lemma (in M_trivial) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []"
  1575 by (simp add: is_tl_def)
  1576 
  1577 lemma (in M_trivial) is_tl_Cons:
  1578      "[|M(a); M(l)|] ==> is_tl(M,Cons(a,l),Z) <-> Z = l"
  1579 by (force simp add: is_tl_def)
  1580 
  1581 lemma (in M_trivial) tl_abs [simp]:
  1582      "[|M(x); M(y)|] ==> is_tl(M,x,y) <-> y = tl'(x)"
  1583 apply (simp add: tl'_def)
  1584 apply (intro impI conjI)
  1585  prefer 2 apply (force simp add: is_tl_def)
  1586 apply (simp add: quasilist_def is_tl_def)
  1587 apply (elim disjE exE, auto)
  1588 done
  1589 
  1590 lemma (in M_trivial) relation1_tl: "relation1(M, is_tl(M), tl')"
  1591 by (simp add: relation1_def)
  1592 
  1593 lemma hd'_Nil: "hd'([]) = 0"
  1594 by (simp add: hd'_def)
  1595 
  1596 lemma hd'_Cons: "hd'(Cons(a,l)) = a"
  1597 by (simp add: hd'_def)
  1598 
  1599 lemma tl'_Nil: "tl'([]) = []"
  1600 by (simp add: tl'_def)
  1601 
  1602 lemma tl'_Cons: "tl'(Cons(a,l)) = l"
  1603 by (simp add: tl'_def)
  1604 
  1605 lemma iterates_tl_Nil: "n \<in> nat ==> tl'^n ([]) = []"
  1606 apply (induct_tac n)
  1607 apply (simp_all add: tl'_Nil)
  1608 done
  1609 
  1610 lemma (in M_basic) tl'_closed: "M(x) ==> M(tl'(x))"
  1611 apply (simp add: tl'_def)
  1612 apply (force simp add: quasilist_def)
  1613 done
  1614 
  1615 
  1616 end