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 = rA"

   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(rA)"

  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(fa)"

  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) <-> fx = 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