src/ZF/Constructible/L_axioms.thy
changeset 13348 374d05460db4
parent 13339 0f89104dd377
child 13352 3cd767f8d78b
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Thu Jul 11 10:48:30 2002 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Thu Jul 11 13:43:24 2002 +0200
     1.3 @@ -884,6 +884,46 @@
     1.4  done
     1.5  
     1.6  
     1.7 +subsubsection{*Pre-Image under a Relation, Internalized*}
     1.8 +
     1.9 +(* "pre_image(M,r,A,z) == 
    1.10 +	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))" *)
    1.11 +constdefs pre_image_fm :: "[i,i,i]=>i"
    1.12 +    "pre_image_fm(r,A,z) == 
    1.13 +       Forall(Iff(Member(0,succ(z)),
    1.14 +                  Exists(And(Member(0,succ(succ(r))),
    1.15 +                             Exists(And(Member(0,succ(succ(succ(A)))),
    1.16 +	 			        pair_fm(2,0,1)))))))"
    1.17 +
    1.18 +lemma pre_image_type [TC]:
    1.19 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> pre_image_fm(x,y,z) \<in> formula"
    1.20 +by (simp add: pre_image_fm_def) 
    1.21 +
    1.22 +lemma arity_pre_image_fm [simp]:
    1.23 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
    1.24 +      ==> arity(pre_image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    1.25 +by (simp add: pre_image_fm_def succ_Un_distrib [symmetric] Un_ac) 
    1.26 +
    1.27 +lemma sats_pre_image_fm [simp]:
    1.28 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    1.29 +    ==> sats(A, pre_image_fm(x,y,z), env) <-> 
    1.30 +        pre_image(**A, nth(x,env), nth(y,env), nth(z,env))"
    1.31 +by (simp add: pre_image_fm_def Relative.pre_image_def)
    1.32 +
    1.33 +lemma pre_image_iff_sats:
    1.34 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
    1.35 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
    1.36 +       ==> pre_image(**A, x, y, z) <-> sats(A, pre_image_fm(i,j,k), env)"
    1.37 +by (simp add: sats_pre_image_fm)
    1.38 +
    1.39 +theorem pre_image_reflection:
    1.40 +     "REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)), 
    1.41 +               \<lambda>i x. pre_image(**Lset(i),f(x),g(x),h(x))]"
    1.42 +apply (simp only: Relative.pre_image_def setclass_simps)
    1.43 +apply (intro FOL_reflections pair_reflection)  
    1.44 +done
    1.45 +
    1.46 +
    1.47  subsubsection{*The Concept of Relation, Internalized*}
    1.48  
    1.49  (* "is_relation(M,r) == 
    1.50 @@ -1000,7 +1040,7 @@
    1.51          fun_apply_reflection subset_reflection
    1.52  	transitive_set_reflection membership_reflection
    1.53  	pred_set_reflection domain_reflection range_reflection field_reflection
    1.54 -        image_reflection
    1.55 +        image_reflection pre_image_reflection
    1.56  	is_relation_reflection is_function_reflection
    1.57  
    1.58  lemmas function_iff_sats = 
    1.59 @@ -1008,7 +1048,7 @@
    1.60  	cons_iff_sats successor_iff_sats
    1.61          fun_apply_iff_sats  Memrel_iff_sats
    1.62  	pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats
    1.63 -        image_iff_sats
    1.64 +        image_iff_sats pre_image_iff_sats 
    1.65  	relation_iff_sats function_iff_sats
    1.66  
    1.67  
    1.68 @@ -1189,6 +1229,46 @@
    1.69  done
    1.70  
    1.71  
    1.72 +subsubsection{*Restriction of a Relation, Internalized*}
    1.73 +
    1.74 +
    1.75 +(* "restriction(M,r,A,z) == 
    1.76 +	\<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))" *)
    1.77 +constdefs restriction_fm :: "[i,i,i]=>i"
    1.78 +    "restriction_fm(r,A,z) == 
    1.79 +       Forall(Iff(Member(0,succ(z)),
    1.80 +                  And(Member(0,succ(r)),
    1.81 +                      Exists(And(Member(0,succ(succ(A))),
    1.82 +                                 Exists(pair_fm(1,0,2)))))))"
    1.83 +
    1.84 +lemma restriction_type [TC]:
    1.85 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> restriction_fm(x,y,z) \<in> formula"
    1.86 +by (simp add: restriction_fm_def) 
    1.87 +
    1.88 +lemma arity_restriction_fm [simp]:
    1.89 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
    1.90 +      ==> arity(restriction_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    1.91 +by (simp add: restriction_fm_def succ_Un_distrib [symmetric] Un_ac) 
    1.92 +
    1.93 +lemma sats_restriction_fm [simp]:
    1.94 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    1.95 +    ==> sats(A, restriction_fm(x,y,z), env) <-> 
    1.96 +        restriction(**A, nth(x,env), nth(y,env), nth(z,env))"
    1.97 +by (simp add: restriction_fm_def restriction_def)
    1.98 +
    1.99 +lemma restriction_iff_sats:
   1.100 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.101 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   1.102 +       ==> restriction(**A, x, y, z) <-> sats(A, restriction_fm(i,j,k), env)"
   1.103 +by simp
   1.104 +
   1.105 +theorem restriction_reflection:
   1.106 +     "REFLECTS[\<lambda>x. restriction(L,f(x),g(x),h(x)), 
   1.107 +               \<lambda>i x. restriction(**Lset(i),f(x),g(x),h(x))]"
   1.108 +apply (simp only: restriction_def setclass_simps)
   1.109 +apply (intro FOL_reflections pair_reflection)  
   1.110 +done
   1.111 +
   1.112  subsubsection{*Order-Isomorphisms, Internalized*}
   1.113  
   1.114  (*  order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
   1.115 @@ -1327,12 +1407,14 @@
   1.116  lemmas fun_plus_reflections =
   1.117          typed_function_reflection composition_reflection
   1.118          injection_reflection surjection_reflection
   1.119 -        bijection_reflection order_isomorphism_reflection
   1.120 +        bijection_reflection restriction_reflection
   1.121 +        order_isomorphism_reflection
   1.122          ordinal_reflection limit_ordinal_reflection omega_reflection
   1.123  
   1.124  lemmas fun_plus_iff_sats = 
   1.125  	typed_function_iff_sats composition_iff_sats
   1.126 -        injection_iff_sats surjection_iff_sats bijection_iff_sats 
   1.127 +        injection_iff_sats surjection_iff_sats 
   1.128 +        bijection_iff_sats restriction_iff_sats 
   1.129          order_isomorphism_iff_sats
   1.130          ordinal_iff_sats limit_ordinal_iff_sats omega_iff_sats
   1.131