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