src/ZF/Constructible/L_axioms.thy

--- a/src/ZF/Constructible/L_axioms.thy	Thu Jul 11 10:48:30 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Thu Jul 11 13:43:24 2002 +0200
@@ -884,6 +884,46 @@
 done
 
 
+subsubsection{*Pre-Image under a Relation, Internalized*}
+
+(* "pre_image(M,r,A,z) == 
+	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))" *)
+constdefs pre_image_fm :: "[i,i,i]=>i"
+    "pre_image_fm(r,A,z) == 
+       Forall(Iff(Member(0,succ(z)),
+                  Exists(And(Member(0,succ(succ(r))),
+                             Exists(And(Member(0,succ(succ(succ(A)))),
+	 			        pair_fm(2,0,1)))))))"
+
+lemma pre_image_type [TC]:
+     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> pre_image_fm(x,y,z) \<in> formula"
+by (simp add: pre_image_fm_def) 
+
+lemma arity_pre_image_fm [simp]:
+     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
+      ==> arity(pre_image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
+by (simp add: pre_image_fm_def succ_Un_distrib [symmetric] Un_ac) 
+
+lemma sats_pre_image_fm [simp]:
+   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
+    ==> sats(A, pre_image_fm(x,y,z), env) <-> 
+        pre_image(**A, nth(x,env), nth(y,env), nth(z,env))"
+by (simp add: pre_image_fm_def Relative.pre_image_def)
+
+lemma pre_image_iff_sats:
+      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
+          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
+       ==> pre_image(**A, x, y, z) <-> sats(A, pre_image_fm(i,j,k), env)"
+by (simp add: sats_pre_image_fm)
+
+theorem pre_image_reflection:
+     "REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)), 
+               \<lambda>i x. pre_image(**Lset(i),f(x),g(x),h(x))]"
+apply (simp only: Relative.pre_image_def setclass_simps)
+apply (intro FOL_reflections pair_reflection)  
+done
+
+
 subsubsection{*The Concept of Relation, Internalized*}
 
 (* "is_relation(M,r) == 
@@ -1000,7 +1040,7 @@
         fun_apply_reflection subset_reflection
 	transitive_set_reflection membership_reflection
 	pred_set_reflection domain_reflection range_reflection field_reflection
-        image_reflection
+        image_reflection pre_image_reflection
 	is_relation_reflection is_function_reflection
 
 lemmas function_iff_sats = 
@@ -1008,7 +1048,7 @@
 	cons_iff_sats successor_iff_sats
         fun_apply_iff_sats  Memrel_iff_sats
 	pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats
-        image_iff_sats
+        image_iff_sats pre_image_iff_sats 
 	relation_iff_sats function_iff_sats
 
 
@@ -1189,6 +1229,46 @@
 done
 
 
+subsubsection{*Restriction of a Relation, Internalized*}
+
+
+(* "restriction(M,r,A,z) == 
+	\<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))" *)
+constdefs restriction_fm :: "[i,i,i]=>i"
+    "restriction_fm(r,A,z) == 
+       Forall(Iff(Member(0,succ(z)),
+                  And(Member(0,succ(r)),
+                      Exists(And(Member(0,succ(succ(A))),
+                                 Exists(pair_fm(1,0,2)))))))"
+
+lemma restriction_type [TC]:
+     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> restriction_fm(x,y,z) \<in> formula"
+by (simp add: restriction_fm_def) 
+
+lemma arity_restriction_fm [simp]:
+     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
+      ==> arity(restriction_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
+by (simp add: restriction_fm_def succ_Un_distrib [symmetric] Un_ac) 
+
+lemma sats_restriction_fm [simp]:
+   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
+    ==> sats(A, restriction_fm(x,y,z), env) <-> 
+        restriction(**A, nth(x,env), nth(y,env), nth(z,env))"
+by (simp add: restriction_fm_def restriction_def)
+
+lemma restriction_iff_sats:
+      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
+          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
+       ==> restriction(**A, x, y, z) <-> sats(A, restriction_fm(i,j,k), env)"
+by simp
+
+theorem restriction_reflection:
+     "REFLECTS[\<lambda>x. restriction(L,f(x),g(x),h(x)), 
+               \<lambda>i x. restriction(**Lset(i),f(x),g(x),h(x))]"
+apply (simp only: restriction_def setclass_simps)
+apply (intro FOL_reflections pair_reflection)  
+done
+
 subsubsection{*Order-Isomorphisms, Internalized*}
 
 (*  order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
@@ -1327,12 +1407,14 @@
 lemmas fun_plus_reflections =
         typed_function_reflection composition_reflection
         injection_reflection surjection_reflection
-        bijection_reflection order_isomorphism_reflection
+        bijection_reflection restriction_reflection
+        order_isomorphism_reflection
         ordinal_reflection limit_ordinal_reflection omega_reflection
 
 lemmas fun_plus_iff_sats = 
 	typed_function_iff_sats composition_iff_sats
-        injection_iff_sats surjection_iff_sats bijection_iff_sats 
+        injection_iff_sats surjection_iff_sats 
+        bijection_iff_sats restriction_iff_sats 
         order_isomorphism_iff_sats
         ordinal_iff_sats limit_ordinal_iff_sats omega_iff_sats