889 |
889 |
890 lemma singleton_Un_iff: |
890 lemma singleton_Un_iff: |
891 "({x} = A \<union> B) = (A = {} \<and> B = {x} \<or> A = {x} \<and> B = {} \<or> A = {x} \<and> B = {x})" |
891 "({x} = A \<union> B) = (A = {} \<and> B = {x} \<or> A = {x} \<and> B = {} \<or> A = {x} \<and> B = {x})" |
892 by auto |
892 by auto |
893 |
893 |
|
894 |
894 subsubsection {* Image of a set under a function *} |
895 subsubsection {* Image of a set under a function *} |
895 |
896 |
896 text {* |
897 text {* |
897 Frequently @{term b} does not have the syntactic form of @{term "f x"}. |
898 Frequently @{term b} does not have the syntactic form of @{term "f x"}. |
898 *} |
899 *} |
899 |
900 |
900 definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where |
901 definition image :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixr "`" 90) |
901 image_def: "f ` A = {y. EX x:A. y = f(x)}" |
902 where |
902 |
903 "f ` A = {y. \<exists>x\<in>A. y = f x}" |
903 abbreviation |
904 |
904 range :: "('a => 'b) => 'b set" where -- "of function" |
905 lemma image_eqI [simp, intro]: |
905 "range f == f ` UNIV" |
906 "b = f x \<Longrightarrow> x \<in> A \<Longrightarrow> b \<in> f ` A" |
906 |
|
907 lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A" |
|
908 by (unfold image_def) blast |
907 by (unfold image_def) blast |
909 |
908 |
910 lemma imageI: "x : A ==> f x : f ` A" |
909 lemma imageI: |
|
910 "x \<in> A \<Longrightarrow> f x \<in> f ` A" |
911 by (rule image_eqI) (rule refl) |
911 by (rule image_eqI) (rule refl) |
912 |
912 |
913 lemma rev_image_eqI: "x:A ==> b = f x ==> b : f`A" |
913 lemma rev_image_eqI: |
|
914 "x \<in> A \<Longrightarrow> b = f x \<Longrightarrow> b \<in> f ` A" |
914 -- {* This version's more effective when we already have the |
915 -- {* This version's more effective when we already have the |
915 required @{term x}. *} |
916 required @{term x}. *} |
916 by (unfold image_def) blast |
917 by (rule image_eqI) |
917 |
918 |
918 lemma imageE [elim!]: |
919 lemma imageE [elim!]: |
919 "b : (%x. f x)`A ==> (!!x. b = f x ==> x:A ==> P) ==> P" |
920 assumes "b \<in> (\<lambda>x. f x) ` A" -- {* The eta-expansion gives variable-name preservation. *} |
920 -- {* The eta-expansion gives variable-name preservation. *} |
921 obtains x where "b = f x" and "x \<in> A" |
921 by (unfold image_def) blast |
922 using assms by (unfold image_def) blast |
922 |
923 |
923 lemma Compr_image_eq: |
924 lemma Compr_image_eq: |
924 "{x \<in> f ` A. P x} = f ` {x \<in> A. P (f x)}" |
925 "{x \<in> f ` A. P x} = f ` {x \<in> A. P (f x)}" |
925 by auto |
926 by auto |
926 |
927 |
927 lemma image_Un: "f`(A Un B) = f`A Un f`B" |
928 lemma image_Un: |
928 by blast |
929 "f ` (A \<union> B) = f ` A \<union> f ` B" |
929 |
930 by blast |
930 lemma image_iff: "(z : f`A) = (EX x:A. z = f x)" |
931 |
931 by blast |
932 lemma image_iff: |
932 |
933 "z \<in> f ` A \<longleftrightarrow> (\<exists>x\<in>A. z = f x)" |
933 lemma image_subset_iff: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)" |
934 by blast |
934 -- {* This rewrite rule would confuse users if made default. *} |
935 |
935 by blast |
936 lemma image_subsetI: |
936 |
937 "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` A \<subseteq> B" |
937 lemma subset_image_iff: "(B \<subseteq> f`A) = (EX AA. AA \<subseteq> A & B = f`AA)" |
|
938 apply safe |
|
939 prefer 2 apply fast |
|
940 apply (rule_tac x = "{a. a : A & f a : B}" in exI, fast) |
|
941 done |
|
942 |
|
943 lemma image_subsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f`A \<subseteq> B" |
|
944 -- {* Replaces the three steps @{text subsetI}, @{text imageE}, |
938 -- {* Replaces the three steps @{text subsetI}, @{text imageE}, |
945 @{text hypsubst}, but breaks too many existing proofs. *} |
939 @{text hypsubst}, but breaks too many existing proofs. *} |
946 by blast |
940 by blast |
947 |
941 |
|
942 lemma image_subset_iff: |
|
943 "f ` A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. f x \<in> B)" |
|
944 -- {* This rewrite rule would confuse users if made default. *} |
|
945 by blast |
|
946 |
|
947 lemma subset_imageE: |
|
948 assumes "B \<subseteq> f ` A" |
|
949 obtains C where "C \<subseteq> A" and "B = f ` C" |
|
950 proof - |
|
951 from assms have "B = f ` {a \<in> A. f a \<in> B}" by fast |
|
952 moreover have "{a \<in> A. f a \<in> B} \<subseteq> A" by blast |
|
953 ultimately show thesis by (blast intro: that) |
|
954 qed |
|
955 |
|
956 lemma subset_image_iff: |
|
957 "B \<subseteq> f ` A \<longleftrightarrow> (\<exists>AA\<subseteq>A. B = f ` AA)" |
|
958 by (blast elim: subset_imageE) |
|
959 |
|
960 lemma image_ident [simp]: |
|
961 "(\<lambda>x. x) ` Y = Y" |
|
962 by blast |
|
963 |
|
964 lemma image_empty [simp]: |
|
965 "f ` {} = {}" |
|
966 by blast |
|
967 |
|
968 lemma image_insert [simp]: |
|
969 "f ` insert a B = insert (f a) (f ` B)" |
|
970 by blast |
|
971 |
|
972 lemma image_constant: |
|
973 "x \<in> A \<Longrightarrow> (\<lambda>x. c) ` A = {c}" |
|
974 by auto |
|
975 |
|
976 lemma image_constant_conv: |
|
977 "(\<lambda>x. c) ` A = (if A = {} then {} else {c})" |
|
978 by auto |
|
979 |
|
980 lemma image_image: |
|
981 "f ` (g ` A) = (\<lambda>x. f (g x)) ` A" |
|
982 by blast |
|
983 |
|
984 lemma insert_image [simp]: |
|
985 "x \<in> A ==> insert (f x) (f ` A) = f ` A" |
|
986 by blast |
|
987 |
|
988 lemma image_is_empty [iff]: |
|
989 "f ` A = {} \<longleftrightarrow> A = {}" |
|
990 by blast |
|
991 |
|
992 lemma empty_is_image [iff]: |
|
993 "{} = f ` A \<longleftrightarrow> A = {}" |
|
994 by blast |
|
995 |
|
996 lemma image_Collect: |
|
997 "f ` {x. P x} = {f x | x. P x}" |
|
998 -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS, |
|
999 with its implicit quantifier and conjunction. Also image enjoys better |
|
1000 equational properties than does the RHS. *} |
|
1001 by blast |
|
1002 |
|
1003 lemma if_image_distrib [simp]: |
|
1004 "(\<lambda>x. if P x then f x else g x) ` S |
|
1005 = (f ` (S \<inter> {x. P x})) \<union> (g ` (S \<inter> {x. \<not> P x}))" |
|
1006 by (auto simp add: image_def) |
|
1007 |
|
1008 lemma image_cong: |
|
1009 "M = N \<Longrightarrow> (\<And>x. x \<in> N \<Longrightarrow> f x = g x) \<Longrightarrow> f ` M = g ` N" |
|
1010 by (simp add: image_def) |
|
1011 |
|
1012 lemma image_Int_subset: |
|
1013 "f ` (A \<inter> B) \<subseteq> f ` A \<inter> f ` B" |
|
1014 by blast |
|
1015 |
|
1016 lemma image_diff_subset: |
|
1017 "f ` A - f ` B \<subseteq> f ` (A - B)" |
|
1018 by blast |
|
1019 |
|
1020 lemma ball_imageD: |
|
1021 assumes "\<forall>x\<in>f ` A. P x" |
|
1022 shows "\<forall>x\<in>A. P (f x)" |
|
1023 using assms by simp |
|
1024 |
|
1025 lemma bex_imageD: |
|
1026 assumes "\<exists>x\<in>f ` A. P x" |
|
1027 shows "\<exists>x\<in>A. P (f x)" |
|
1028 using assms by auto |
|
1029 |
|
1030 |
948 text {* |
1031 text {* |
949 \medskip Range of a function -- just a translation for image! |
1032 \medskip Range of a function -- just a translation for image! |
950 *} |
1033 *} |
951 |
1034 |
952 lemma image_ident [simp]: "(%x. x) ` Y = Y" |
1035 abbreviation range :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set" |
953 by blast |
1036 where -- "of function" |
954 |
1037 "range f \<equiv> f ` UNIV" |
955 lemma range_eqI: "b = f x ==> b \<in> range f" |
1038 |
956 by simp |
1039 lemma range_eqI: |
957 |
1040 "b = f x \<Longrightarrow> b \<in> range f" |
958 lemma rangeI: "f x \<in> range f" |
1041 by simp |
959 by simp |
1042 |
960 |
1043 lemma rangeI: |
961 lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) ==> (!!x. b = f x ==> P) ==> P" |
1044 "f x \<in> range f" |
962 by blast |
1045 by simp |
|
1046 |
|
1047 lemma rangeE [elim?]: |
|
1048 "b \<in> range (\<lambda>x. f x) \<Longrightarrow> (\<And>x. b = f x \<Longrightarrow> P) \<Longrightarrow> P" |
|
1049 by (rule imageE) |
|
1050 |
|
1051 lemma full_SetCompr_eq: |
|
1052 "{u. \<exists>x. u = f x} = range f" |
|
1053 by auto |
|
1054 |
|
1055 lemma range_composition: |
|
1056 "range (\<lambda>x. f (g x)) = f ` range g" |
|
1057 by (subst image_image) simp |
|
1058 |
963 |
1059 |
964 subsubsection {* Some rules with @{text "if"} *} |
1060 subsubsection {* Some rules with @{text "if"} *} |
965 |
1061 |
966 text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *} |
1062 text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *} |
967 |
1063 |
1051 |
1147 |
1052 lemmas [symmetric, rulify] = atomize_ball |
1148 lemmas [symmetric, rulify] = atomize_ball |
1053 and [symmetric, defn] = atomize_ball |
1149 and [symmetric, defn] = atomize_ball |
1054 |
1150 |
1055 lemma image_Pow_mono: |
1151 lemma image_Pow_mono: |
1056 assumes "f ` A \<le> B" |
1152 assumes "f ` A \<subseteq> B" |
1057 shows "(image f) ` (Pow A) \<le> Pow B" |
1153 shows "image f ` Pow A \<subseteq> Pow B" |
1058 using assms by blast |
1154 using assms by blast |
1059 |
1155 |
1060 lemma image_Pow_surj: |
1156 lemma image_Pow_surj: |
1061 assumes "f ` A = B" |
1157 assumes "f ` A = B" |
1062 shows "(image f) ` (Pow A) = Pow B" |
1158 shows "image f ` Pow A = Pow B" |
1063 using assms unfolding Pow_def proof(auto) |
1159 using assms by (blast elim: subset_imageE) |
1064 fix Y assume *: "Y \<le> f ` A" |
1160 |
1065 obtain X where X_def: "X = {x \<in> A. f x \<in> Y}" by blast |
|
1066 have "f ` X = Y \<and> X \<le> A" unfolding X_def using * by auto |
|
1067 thus "Y \<in> (image f) ` {X. X \<le> A}" by blast |
|
1068 qed |
|
1069 |
1161 |
1070 subsubsection {* Derived rules involving subsets. *} |
1162 subsubsection {* Derived rules involving subsets. *} |
1071 |
1163 |
1072 text {* @{text insert}. *} |
1164 text {* @{text insert}. *} |
1073 |
1165 |
1191 |
1283 |
1192 lemma disjoint_insert [simp]: |
1284 lemma disjoint_insert [simp]: |
1193 "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})" |
1285 "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})" |
1194 "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)" |
1286 "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)" |
1195 by auto |
1287 by auto |
1196 |
|
1197 text {* \medskip @{text image}. *} |
|
1198 |
|
1199 lemma image_empty [simp]: "f`{} = {}" |
|
1200 by blast |
|
1201 |
|
1202 lemma image_insert [simp]: "f ` insert a B = insert (f a) (f`B)" |
|
1203 by blast |
|
1204 |
|
1205 lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}" |
|
1206 by auto |
|
1207 |
|
1208 lemma image_constant_conv: "(%x. c) ` A = (if A = {} then {} else {c})" |
|
1209 by auto |
|
1210 |
|
1211 lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A" |
|
1212 by blast |
|
1213 |
|
1214 lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A" |
|
1215 by blast |
|
1216 |
|
1217 lemma image_is_empty [iff]: "(f`A = {}) = (A = {})" |
|
1218 by blast |
|
1219 |
|
1220 lemma empty_is_image[iff]: "({} = f ` A) = (A = {})" |
|
1221 by blast |
|
1222 |
|
1223 |
|
1224 lemma image_Collect: "f ` {x. P x} = {f x | x. P x}" |
|
1225 -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS, |
|
1226 with its implicit quantifier and conjunction. Also image enjoys better |
|
1227 equational properties than does the RHS. *} |
|
1228 by blast |
|
1229 |
|
1230 lemma if_image_distrib [simp]: |
|
1231 "(\<lambda>x. if P x then f x else g x) ` S |
|
1232 = (f ` (S \<inter> {x. P x})) \<union> (g ` (S \<inter> {x. \<not> P x}))" |
|
1233 by (auto simp add: image_def) |
|
1234 |
|
1235 lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> f`M = g`N" |
|
1236 by (simp add: image_def) |
|
1237 |
|
1238 lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B" |
|
1239 by blast |
|
1240 |
|
1241 lemma image_diff_subset: "f`A - f`B <= f`(A - B)" |
|
1242 by blast |
|
1243 |
|
1244 |
|
1245 text {* \medskip @{text range}. *} |
|
1246 |
|
1247 lemma full_SetCompr_eq: "{u. \<exists>x. u = f x} = range f" |
|
1248 by auto |
|
1249 |
|
1250 lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g" |
|
1251 by (subst image_image, simp) |
|
1252 |
1288 |
1253 |
1289 |
1254 text {* \medskip @{text Int} *} |
1290 text {* \medskip @{text Int} *} |
1255 |
1291 |
1256 lemma Int_absorb: "A \<inter> A = A" |
1292 lemma Int_absorb: "A \<inter> A = A" |