src/ZF/Constructible/Relative.thy
changeset 13634 99a593b49b04
parent 13628 87482b5e3f2e
child 13687 22dce9134953
     1.1 --- a/src/ZF/Constructible/Relative.thy	Tue Oct 08 14:09:18 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Wed Oct 09 11:07:13 2002 +0200
     1.3 @@ -1,7 +1,6 @@
     1.4  (*  Title:      ZF/Constructible/Relative.thy
     1.5      ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   2002  University of Cambridge
     1.8  *)
     1.9  
    1.10  header {*Relativization and Absoluteness*}
    1.11 @@ -197,43 +196,43 @@
    1.12         (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
    1.13         (is_quasinat(M,k) | empty(M,z))"
    1.14  
    1.15 -  relativize1 :: "[i=>o, [i,i]=>o, i=>i] => o"
    1.16 -    "relativize1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) <-> y = f(x)"
    1.17 +  relation1 :: "[i=>o, [i,i]=>o, i=>i] => o"
    1.18 +    "relation1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) <-> y = f(x)"
    1.19  
    1.20 -  Relativize1 :: "[i=>o, i, [i,i]=>o, i=>i] => o"
    1.21 +  Relation1 :: "[i=>o, i, [i,i]=>o, i=>i] => o"
    1.22      --{*as above, but typed*}
    1.23 -    "Relativize1(M,A,is_f,f) ==
    1.24 +    "Relation1(M,A,is_f,f) ==
    1.25          \<forall>x[M]. \<forall>y[M]. x\<in>A --> is_f(x,y) <-> y = f(x)"
    1.26  
    1.27 -  relativize2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o"
    1.28 -    "relativize2(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) <-> z = f(x,y)"
    1.29 +  relation2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o"
    1.30 +    "relation2(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) <-> z = f(x,y)"
    1.31  
    1.32 -  Relativize2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o"
    1.33 -    "Relativize2(M,A,B,is_f,f) ==
    1.34 +  Relation2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o"
    1.35 +    "Relation2(M,A,B,is_f,f) ==
    1.36          \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. x\<in>A --> y\<in>B --> is_f(x,y,z) <-> z = f(x,y)"
    1.37  
    1.38 -  relativize3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o"
    1.39 -    "relativize3(M,is_f,f) ==
    1.40 +  relation3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o"
    1.41 +    "relation3(M,is_f,f) ==
    1.42         \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. is_f(x,y,z,u) <-> u = f(x,y,z)"
    1.43  
    1.44 -  Relativize3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o"
    1.45 -    "Relativize3(M,A,B,C,is_f,f) ==
    1.46 +  Relation3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o"
    1.47 +    "Relation3(M,A,B,C,is_f,f) ==
    1.48         \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M].
    1.49           x\<in>A --> y\<in>B --> z\<in>C --> is_f(x,y,z,u) <-> u = f(x,y,z)"
    1.50  
    1.51 -  relativize4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o"
    1.52 -    "relativize4(M,is_f,f) ==
    1.53 +  relation4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o"
    1.54 +    "relation4(M,is_f,f) ==
    1.55         \<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)"
    1.56  
    1.57  
    1.58  text{*Useful when absoluteness reasoning has replaced the predicates by terms*}
    1.59 -lemma triv_Relativize1:
    1.60 -     "Relativize1(M, A, \<lambda>x y. y = f(x), f)"
    1.61 -by (simp add: Relativize1_def)
    1.62 +lemma triv_Relation1:
    1.63 +     "Relation1(M, A, \<lambda>x y. y = f(x), f)"
    1.64 +by (simp add: Relation1_def)
    1.65  
    1.66 -lemma triv_Relativize2:
    1.67 -     "Relativize2(M, A, B, \<lambda>x y a. a = f(x,y), f)"
    1.68 -by (simp add: Relativize2_def)
    1.69 +lemma triv_Relation2:
    1.70 +     "Relation2(M, A, B, \<lambda>x y a. a = f(x,y), f)"
    1.71 +by (simp add: Relation2_def)
    1.72  
    1.73  
    1.74  subsection {*The relativized ZF axioms*}
    1.75 @@ -730,9 +729,9 @@
    1.76  
    1.77  lemma (in M_trivial) lambda_abs2 [simp]:
    1.78       "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
    1.79 -         Relativize1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |]
    1.80 +         Relation1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |]
    1.81        ==> is_lambda(M,A,is_b,z) <-> z = Lambda(A,b)"
    1.82 -apply (simp add: Relativize1_def is_lambda_def)
    1.83 +apply (simp add: Relation1_def is_lambda_def)
    1.84  apply (rule iffI)
    1.85   prefer 2 apply (simp add: lam_def)
    1.86  apply (rule M_equalityI)
    1.87 @@ -787,7 +786,7 @@
    1.88  by (auto simp add: is_quasinat_def quasinat_def)
    1.89  
    1.90  lemma (in M_trivial) nat_case_abs [simp]:
    1.91 -     "[| relativize1(M,is_b,b); M(k); M(z) |]
    1.92 +     "[| relation1(M,is_b,b); M(k); M(z) |]
    1.93        ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
    1.94  apply (case_tac "quasinat(k)")
    1.95   prefer 2
    1.96 @@ -795,7 +794,7 @@
    1.97   apply (force simp add: quasinat_def)
    1.98  apply (simp add: quasinat_def is_nat_case_def)
    1.99  apply (elim disjE exE)
   1.100 - apply (simp_all add: relativize1_def)
   1.101 + apply (simp_all add: relation1_def)
   1.102  done
   1.103  
   1.104  (*NOT for the simplifier.  The assumption M(z') is apparently necessary, but
   1.105 @@ -929,30 +928,8 @@
   1.106        strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. \<exists>cnbf[M].
   1.107                  pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &
   1.108                  upair(M,cnbf,cnbf,z))"
   1.109 -  and well_ord_iso_separation:
   1.110 -     "[| M(A); M(f); M(r) |]
   1.111 -      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y[M]. (\<exists>p[M].
   1.112 -		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
   1.113 -  and obase_separation:
   1.114 -     --{*part of the order type formalization*}
   1.115 -     "[| M(A); M(r) |]
   1.116 -      ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
   1.117 -	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
   1.118 -	     order_isomorphism(M,par,r,x,mx,g))"
   1.119 -  and obase_equals_separation:
   1.120 -     "[| M(A); M(r) |]
   1.121 -      ==> separation (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M].
   1.122 -			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M].
   1.123 -			      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
   1.124 -			      order_isomorphism(M,pxr,r,y,my,g))))"
   1.125 -  and omap_replacement:
   1.126 -     "[| M(A); M(r) |]
   1.127 -      ==> strong_replacement(M,
   1.128 -             \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
   1.129 -	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &
   1.130 -	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
   1.131    and is_recfun_separation:
   1.132 -     --{*for well-founded recursion*}
   1.133 +     --{*for well-founded recursion: used to prove @{text is_recfun_equal}*}
   1.134       "[| M(r); M(f); M(g); M(a); M(b) |]
   1.135       ==> separation(M,
   1.136              \<lambda>x. \<exists>xa[M]. \<exists>xb[M].
   1.137 @@ -1490,7 +1467,7 @@
   1.138  by (auto simp add: is_quasilist_def quasilist_def)
   1.139  
   1.140  lemma (in M_trivial) list_case_abs [simp]:
   1.141 -     "[| relativize2(M,is_b,b); M(k); M(z) |]
   1.142 +     "[| relation2(M,is_b,b); M(k); M(z) |]
   1.143        ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)"
   1.144  apply (case_tac "quasilist(k)")
   1.145   prefer 2
   1.146 @@ -1498,7 +1475,7 @@
   1.147   apply (force simp add: quasilist_def)
   1.148  apply (simp add: quasilist_def is_list_case_def)
   1.149  apply (elim disjE exE)
   1.150 - apply (simp_all add: relativize2_def)
   1.151 + apply (simp_all add: relation2_def)
   1.152  done
   1.153  
   1.154  
   1.155 @@ -1536,8 +1513,8 @@
   1.156  apply (elim disjE exE, auto)
   1.157  done
   1.158  
   1.159 -lemma (in M_trivial) relativize1_tl: "relativize1(M, is_tl(M), tl')"
   1.160 -by (simp add: relativize1_def)
   1.161 +lemma (in M_trivial) relation1_tl: "relation1(M, is_tl(M), tl')"
   1.162 +by (simp add: relation1_def)
   1.163  
   1.164  lemma hd'_Nil: "hd'([]) = 0"
   1.165  by (simp add: hd'_def)