882 apply (simp only: Relative.image_def setclass_simps) |
882 apply (simp only: Relative.image_def setclass_simps) |
883 apply (intro FOL_reflections pair_reflection) |
883 apply (intro FOL_reflections pair_reflection) |
884 done |
884 done |
885 |
885 |
886 |
886 |
|
887 subsubsection{*Pre-Image under a Relation, Internalized*} |
|
888 |
|
889 (* "pre_image(M,r,A,z) == |
|
890 \<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))" *) |
|
891 constdefs pre_image_fm :: "[i,i,i]=>i" |
|
892 "pre_image_fm(r,A,z) == |
|
893 Forall(Iff(Member(0,succ(z)), |
|
894 Exists(And(Member(0,succ(succ(r))), |
|
895 Exists(And(Member(0,succ(succ(succ(A)))), |
|
896 pair_fm(2,0,1)))))))" |
|
897 |
|
898 lemma pre_image_type [TC]: |
|
899 "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> pre_image_fm(x,y,z) \<in> formula" |
|
900 by (simp add: pre_image_fm_def) |
|
901 |
|
902 lemma arity_pre_image_fm [simp]: |
|
903 "[| x \<in> nat; y \<in> nat; z \<in> nat |] |
|
904 ==> arity(pre_image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" |
|
905 by (simp add: pre_image_fm_def succ_Un_distrib [symmetric] Un_ac) |
|
906 |
|
907 lemma sats_pre_image_fm [simp]: |
|
908 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
|
909 ==> sats(A, pre_image_fm(x,y,z), env) <-> |
|
910 pre_image(**A, nth(x,env), nth(y,env), nth(z,env))" |
|
911 by (simp add: pre_image_fm_def Relative.pre_image_def) |
|
912 |
|
913 lemma pre_image_iff_sats: |
|
914 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
|
915 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
|
916 ==> pre_image(**A, x, y, z) <-> sats(A, pre_image_fm(i,j,k), env)" |
|
917 by (simp add: sats_pre_image_fm) |
|
918 |
|
919 theorem pre_image_reflection: |
|
920 "REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)), |
|
921 \<lambda>i x. pre_image(**Lset(i),f(x),g(x),h(x))]" |
|
922 apply (simp only: Relative.pre_image_def setclass_simps) |
|
923 apply (intro FOL_reflections pair_reflection) |
|
924 done |
|
925 |
|
926 |
887 subsubsection{*The Concept of Relation, Internalized*} |
927 subsubsection{*The Concept of Relation, Internalized*} |
888 |
928 |
889 (* "is_relation(M,r) == |
929 (* "is_relation(M,r) == |
890 (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))" *) |
930 (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))" *) |
891 constdefs relation_fm :: "i=>i" |
931 constdefs relation_fm :: "i=>i" |
998 empty_reflection upair_reflection pair_reflection union_reflection |
1038 empty_reflection upair_reflection pair_reflection union_reflection |
999 cons_reflection successor_reflection |
1039 cons_reflection successor_reflection |
1000 fun_apply_reflection subset_reflection |
1040 fun_apply_reflection subset_reflection |
1001 transitive_set_reflection membership_reflection |
1041 transitive_set_reflection membership_reflection |
1002 pred_set_reflection domain_reflection range_reflection field_reflection |
1042 pred_set_reflection domain_reflection range_reflection field_reflection |
1003 image_reflection |
1043 image_reflection pre_image_reflection |
1004 is_relation_reflection is_function_reflection |
1044 is_relation_reflection is_function_reflection |
1005 |
1045 |
1006 lemmas function_iff_sats = |
1046 lemmas function_iff_sats = |
1007 empty_iff_sats upair_iff_sats pair_iff_sats union_iff_sats |
1047 empty_iff_sats upair_iff_sats pair_iff_sats union_iff_sats |
1008 cons_iff_sats successor_iff_sats |
1048 cons_iff_sats successor_iff_sats |
1009 fun_apply_iff_sats Memrel_iff_sats |
1049 fun_apply_iff_sats Memrel_iff_sats |
1010 pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats |
1050 pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats |
1011 image_iff_sats |
1051 image_iff_sats pre_image_iff_sats |
1012 relation_iff_sats function_iff_sats |
1052 relation_iff_sats function_iff_sats |
1013 |
1053 |
1014 |
1054 |
1015 theorem typed_function_reflection: |
1055 theorem typed_function_reflection: |
1016 "REFLECTS[\<lambda>x. typed_function(L,f(x),g(x),h(x)), |
1056 "REFLECTS[\<lambda>x. typed_function(L,f(x),g(x),h(x)), |
1187 apply (simp only: bijection_def setclass_simps) |
1227 apply (simp only: bijection_def setclass_simps) |
1188 apply (intro And_reflection injection_reflection surjection_reflection) |
1228 apply (intro And_reflection injection_reflection surjection_reflection) |
1189 done |
1229 done |
1190 |
1230 |
1191 |
1231 |
|
1232 subsubsection{*Restriction of a Relation, Internalized*} |
|
1233 |
|
1234 |
|
1235 (* "restriction(M,r,A,z) == |
|
1236 \<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))" *) |
|
1237 constdefs restriction_fm :: "[i,i,i]=>i" |
|
1238 "restriction_fm(r,A,z) == |
|
1239 Forall(Iff(Member(0,succ(z)), |
|
1240 And(Member(0,succ(r)), |
|
1241 Exists(And(Member(0,succ(succ(A))), |
|
1242 Exists(pair_fm(1,0,2)))))))" |
|
1243 |
|
1244 lemma restriction_type [TC]: |
|
1245 "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> restriction_fm(x,y,z) \<in> formula" |
|
1246 by (simp add: restriction_fm_def) |
|
1247 |
|
1248 lemma arity_restriction_fm [simp]: |
|
1249 "[| x \<in> nat; y \<in> nat; z \<in> nat |] |
|
1250 ==> arity(restriction_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" |
|
1251 by (simp add: restriction_fm_def succ_Un_distrib [symmetric] Un_ac) |
|
1252 |
|
1253 lemma sats_restriction_fm [simp]: |
|
1254 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
|
1255 ==> sats(A, restriction_fm(x,y,z), env) <-> |
|
1256 restriction(**A, nth(x,env), nth(y,env), nth(z,env))" |
|
1257 by (simp add: restriction_fm_def restriction_def) |
|
1258 |
|
1259 lemma restriction_iff_sats: |
|
1260 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
|
1261 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
|
1262 ==> restriction(**A, x, y, z) <-> sats(A, restriction_fm(i,j,k), env)" |
|
1263 by simp |
|
1264 |
|
1265 theorem restriction_reflection: |
|
1266 "REFLECTS[\<lambda>x. restriction(L,f(x),g(x),h(x)), |
|
1267 \<lambda>i x. restriction(**Lset(i),f(x),g(x),h(x))]" |
|
1268 apply (simp only: restriction_def setclass_simps) |
|
1269 apply (intro FOL_reflections pair_reflection) |
|
1270 done |
|
1271 |
1192 subsubsection{*Order-Isomorphisms, Internalized*} |
1272 subsubsection{*Order-Isomorphisms, Internalized*} |
1193 |
1273 |
1194 (* order_isomorphism :: "[i=>o,i,i,i,i,i] => o" |
1274 (* order_isomorphism :: "[i=>o,i,i,i,i,i] => o" |
1195 "order_isomorphism(M,A,r,B,s,f) == |
1275 "order_isomorphism(M,A,r,B,s,f) == |
1196 bijection(M,A,B,f) & |
1276 bijection(M,A,B,f) & |
1325 |
1405 |
1326 |
1406 |
1327 lemmas fun_plus_reflections = |
1407 lemmas fun_plus_reflections = |
1328 typed_function_reflection composition_reflection |
1408 typed_function_reflection composition_reflection |
1329 injection_reflection surjection_reflection |
1409 injection_reflection surjection_reflection |
1330 bijection_reflection order_isomorphism_reflection |
1410 bijection_reflection restriction_reflection |
|
1411 order_isomorphism_reflection |
1331 ordinal_reflection limit_ordinal_reflection omega_reflection |
1412 ordinal_reflection limit_ordinal_reflection omega_reflection |
1332 |
1413 |
1333 lemmas fun_plus_iff_sats = |
1414 lemmas fun_plus_iff_sats = |
1334 typed_function_iff_sats composition_iff_sats |
1415 typed_function_iff_sats composition_iff_sats |
1335 injection_iff_sats surjection_iff_sats bijection_iff_sats |
1416 injection_iff_sats surjection_iff_sats |
|
1417 bijection_iff_sats restriction_iff_sats |
1336 order_isomorphism_iff_sats |
1418 order_isomorphism_iff_sats |
1337 ordinal_iff_sats limit_ordinal_iff_sats omega_iff_sats |
1419 ordinal_iff_sats limit_ordinal_iff_sats omega_iff_sats |
1338 |
1420 |
1339 end |
1421 end |