tuned;
authorhaftmann
Sun Mar 09 22:45:07 2014 +0100 (2014-03-09)
changeset 56014aaa3f2365fc5
parent 56013 508836bbfed4
child 56015 57e2cfba9c6e
tuned;
elimination rule subset_imageE;
typical composition collapsing rewrite order in lemma image_image_eq_image_comp;
destruction rules ball_imageD, bex_imageD
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.thy	Sun Mar 09 22:27:04 2014 +0100
     1.2 +++ b/src/HOL/Set.thy	Sun Mar 09 22:45:07 2014 +0100
     1.3 @@ -891,75 +891,171 @@
     1.4    "({x} = A \<union> B) = (A = {} \<and> B = {x} \<or> A = {x} \<and> B = {} \<or> A = {x} \<and> B = {x})"
     1.5  by auto
     1.6  
     1.7 +
     1.8  subsubsection {* Image of a set under a function *}
     1.9  
    1.10  text {*
    1.11    Frequently @{term b} does not have the syntactic form of @{term "f x"}.
    1.12  *}
    1.13  
    1.14 -definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where
    1.15 -  image_def: "f ` A = {y. EX x:A. y = f(x)}"
    1.16 -
    1.17 -abbreviation
    1.18 -  range :: "('a => 'b) => 'b set" where -- "of function"
    1.19 -  "range f == f ` UNIV"
    1.20 -
    1.21 -lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A"
    1.22 +definition image :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixr "`" 90)
    1.23 +where
    1.24 +  "f ` A = {y. \<exists>x\<in>A. y = f x}"
    1.25 +
    1.26 +lemma image_eqI [simp, intro]:
    1.27 +  "b = f x \<Longrightarrow> x \<in> A \<Longrightarrow> b \<in> f ` A"
    1.28    by (unfold image_def) blast
    1.29  
    1.30 -lemma imageI: "x : A ==> f x : f ` A"
    1.31 +lemma imageI:
    1.32 +  "x \<in> A \<Longrightarrow> f x \<in> f ` A"
    1.33    by (rule image_eqI) (rule refl)
    1.34  
    1.35 -lemma rev_image_eqI: "x:A ==> b = f x ==> b : f`A"
    1.36 +lemma rev_image_eqI:
    1.37 +  "x \<in> A \<Longrightarrow> b = f x \<Longrightarrow> b \<in> f ` A"
    1.38    -- {* This version's more effective when we already have the
    1.39      required @{term x}. *}
    1.40 -  by (unfold image_def) blast
    1.41 +  by (rule image_eqI)
    1.42  
    1.43  lemma imageE [elim!]:
    1.44 -  "b : (%x. f x)`A ==> (!!x. b = f x ==> x:A ==> P) ==> P"
    1.45 -  -- {* The eta-expansion gives variable-name preservation. *}
    1.46 -  by (unfold image_def) blast
    1.47 +  assumes "b \<in> (\<lambda>x. f x) ` A" -- {* The eta-expansion gives variable-name preservation. *}
    1.48 +  obtains x where "b = f x" and "x \<in> A"
    1.49 +  using assms by (unfold image_def) blast
    1.50  
    1.51  lemma Compr_image_eq:
    1.52    "{x \<in> f ` A. P x} = f ` {x \<in> A. P (f x)}"
    1.53    by auto
    1.54  
    1.55 -lemma image_Un: "f`(A Un B) = f`A Un f`B"
    1.56 -  by blast
    1.57 -
    1.58 -lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
    1.59 -  by blast
    1.60 -
    1.61 -lemma image_subset_iff: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
    1.62 -  -- {* This rewrite rule would confuse users if made default. *}
    1.63 +lemma image_Un:
    1.64 +  "f ` (A \<union> B) = f ` A \<union> f ` B"
    1.65    by blast
    1.66  
    1.67 -lemma subset_image_iff: "(B \<subseteq> f`A) = (EX AA. AA \<subseteq> A & B = f`AA)"
    1.68 -  apply safe
    1.69 -   prefer 2 apply fast
    1.70 -  apply (rule_tac x = "{a. a : A & f a : B}" in exI, fast)
    1.71 -  done
    1.72 -
    1.73 -lemma image_subsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f`A \<subseteq> B"
    1.74 +lemma image_iff:
    1.75 +  "z \<in> f ` A \<longleftrightarrow> (\<exists>x\<in>A. z = f x)"
    1.76 +  by blast
    1.77 +
    1.78 +lemma image_subsetI:
    1.79 +  "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` A \<subseteq> B"
    1.80    -- {* Replaces the three steps @{text subsetI}, @{text imageE},
    1.81      @{text hypsubst}, but breaks too many existing proofs. *}
    1.82    by blast
    1.83  
    1.84 +lemma image_subset_iff:
    1.85 +  "f ` A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. f x \<in> B)"
    1.86 +  -- {* This rewrite rule would confuse users if made default. *}
    1.87 +  by blast
    1.88 +
    1.89 +lemma subset_imageE:
    1.90 +  assumes "B \<subseteq> f ` A"
    1.91 +  obtains C where "C \<subseteq> A" and "B = f ` C"
    1.92 +proof -
    1.93 +  from assms have "B = f ` {a \<in> A. f a \<in> B}" by fast
    1.94 +  moreover have "{a \<in> A. f a \<in> B} \<subseteq> A" by blast
    1.95 +  ultimately show thesis by (blast intro: that)
    1.96 +qed
    1.97 +
    1.98 +lemma subset_image_iff:
    1.99 +  "B \<subseteq> f ` A \<longleftrightarrow> (\<exists>AA\<subseteq>A. B = f ` AA)"
   1.100 +  by (blast elim: subset_imageE)
   1.101 +
   1.102 +lemma image_ident [simp]:
   1.103 +  "(\<lambda>x. x) ` Y = Y"
   1.104 +  by blast
   1.105 +
   1.106 +lemma image_empty [simp]:
   1.107 +  "f ` {} = {}"
   1.108 +  by blast
   1.109 +
   1.110 +lemma image_insert [simp]:
   1.111 +  "f ` insert a B = insert (f a) (f ` B)"
   1.112 +  by blast
   1.113 +
   1.114 +lemma image_constant:
   1.115 +  "x \<in> A \<Longrightarrow> (\<lambda>x. c) ` A = {c}"
   1.116 +  by auto
   1.117 +
   1.118 +lemma image_constant_conv:
   1.119 +  "(\<lambda>x. c) ` A = (if A = {} then {} else {c})"
   1.120 +  by auto
   1.121 +
   1.122 +lemma image_image:
   1.123 +  "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
   1.124 +  by blast
   1.125 +
   1.126 +lemma insert_image [simp]:
   1.127 +  "x \<in> A ==> insert (f x) (f ` A) = f ` A"
   1.128 +  by blast
   1.129 +
   1.130 +lemma image_is_empty [iff]:
   1.131 +  "f ` A = {} \<longleftrightarrow> A = {}"
   1.132 +  by blast
   1.133 +
   1.134 +lemma empty_is_image [iff]:
   1.135 +  "{} = f ` A \<longleftrightarrow> A = {}"
   1.136 +  by blast
   1.137 +
   1.138 +lemma image_Collect:
   1.139 +  "f ` {x. P x} = {f x | x. P x}"
   1.140 +  -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
   1.141 +      with its implicit quantifier and conjunction.  Also image enjoys better
   1.142 +      equational properties than does the RHS. *}
   1.143 +  by blast
   1.144 +
   1.145 +lemma if_image_distrib [simp]:
   1.146 +  "(\<lambda>x. if P x then f x else g x) ` S
   1.147 +    = (f ` (S \<inter> {x. P x})) \<union> (g ` (S \<inter> {x. \<not> P x}))"
   1.148 +  by (auto simp add: image_def)
   1.149 +
   1.150 +lemma image_cong:
   1.151 +  "M = N \<Longrightarrow> (\<And>x. x \<in> N \<Longrightarrow> f x = g x) \<Longrightarrow> f ` M = g ` N"
   1.152 +  by (simp add: image_def)
   1.153 +
   1.154 +lemma image_Int_subset:
   1.155 +  "f ` (A \<inter> B) \<subseteq> f ` A \<inter> f ` B"
   1.156 +  by blast
   1.157 +
   1.158 +lemma image_diff_subset:
   1.159 +  "f ` A - f ` B \<subseteq> f ` (A - B)"
   1.160 +  by blast
   1.161 +
   1.162 +lemma ball_imageD:
   1.163 +  assumes "\<forall>x\<in>f ` A. P x"
   1.164 +  shows "\<forall>x\<in>A. P (f x)"
   1.165 +  using assms by simp
   1.166 +
   1.167 +lemma bex_imageD:
   1.168 +  assumes "\<exists>x\<in>f ` A. P x"
   1.169 +  shows "\<exists>x\<in>A. P (f x)"
   1.170 +  using assms by auto
   1.171 +
   1.172 +
   1.173  text {*
   1.174    \medskip Range of a function -- just a translation for image!
   1.175  *}
   1.176  
   1.177 -lemma image_ident [simp]: "(%x. x) ` Y = Y"
   1.178 -  by blast
   1.179 -
   1.180 -lemma range_eqI: "b = f x ==> b \<in> range f"
   1.181 +abbreviation range :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set"
   1.182 +where -- "of function"
   1.183 +  "range f \<equiv> f ` UNIV"
   1.184 +
   1.185 +lemma range_eqI:
   1.186 +  "b = f x \<Longrightarrow> b \<in> range f"
   1.187 +  by simp
   1.188 +
   1.189 +lemma rangeI:
   1.190 +  "f x \<in> range f"
   1.191    by simp
   1.192  
   1.193 -lemma rangeI: "f x \<in> range f"
   1.194 -  by simp
   1.195 -
   1.196 -lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) ==> (!!x. b = f x ==> P) ==> P"
   1.197 -  by blast
   1.198 +lemma rangeE [elim?]:
   1.199 +  "b \<in> range (\<lambda>x. f x) \<Longrightarrow> (\<And>x. b = f x \<Longrightarrow> P) \<Longrightarrow> P"
   1.200 +  by (rule imageE)
   1.201 +
   1.202 +lemma full_SetCompr_eq:
   1.203 +  "{u. \<exists>x. u = f x} = range f"
   1.204 +  by auto
   1.205 +
   1.206 +lemma range_composition: 
   1.207 +  "range (\<lambda>x. f (g x)) = f ` range g"
   1.208 +  by (subst image_image) simp
   1.209 +
   1.210  
   1.211  subsubsection {* Some rules with @{text "if"} *}
   1.212  
   1.213 @@ -1053,19 +1149,15 @@
   1.214    and [symmetric, defn] = atomize_ball
   1.215  
   1.216  lemma image_Pow_mono:
   1.217 -  assumes "f ` A \<le> B"
   1.218 -  shows "(image f) ` (Pow A) \<le> Pow B"
   1.219 -using assms by blast
   1.220 +  assumes "f ` A \<subseteq> B"
   1.221 +  shows "image f ` Pow A \<subseteq> Pow B"
   1.222 +  using assms by blast
   1.223  
   1.224  lemma image_Pow_surj:
   1.225    assumes "f ` A = B"
   1.226 -  shows "(image f) ` (Pow A) = Pow B"
   1.227 -using assms unfolding Pow_def proof(auto)
   1.228 -  fix Y assume *: "Y \<le> f ` A"
   1.229 -  obtain X where X_def: "X = {x \<in> A. f x \<in> Y}" by blast
   1.230 -  have "f ` X = Y \<and> X \<le> A" unfolding X_def using * by auto
   1.231 -  thus "Y \<in> (image f) ` {X. X \<le> A}" by blast
   1.232 -qed
   1.233 +  shows "image f ` Pow A = Pow B"
   1.234 +  using assms by (blast elim: subset_imageE)
   1.235 +
   1.236  
   1.237  subsubsection {* Derived rules involving subsets. *}
   1.238  
   1.239 @@ -1194,62 +1286,6 @@
   1.240   "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
   1.241    by auto
   1.242  
   1.243 -text {* \medskip @{text image}. *}
   1.244 -
   1.245 -lemma image_empty [simp]: "f`{} = {}"
   1.246 -  by blast
   1.247 -
   1.248 -lemma image_insert [simp]: "f ` insert a B = insert (f a) (f`B)"
   1.249 -  by blast
   1.250 -
   1.251 -lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
   1.252 -  by auto
   1.253 -
   1.254 -lemma image_constant_conv: "(%x. c) ` A = (if A = {} then {} else {c})"
   1.255 -by auto
   1.256 -
   1.257 -lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
   1.258 -by blast
   1.259 -
   1.260 -lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A"
   1.261 -by blast
   1.262 -
   1.263 -lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
   1.264 -by blast
   1.265 -
   1.266 -lemma empty_is_image[iff]: "({} = f ` A) = (A = {})"
   1.267 -by blast
   1.268 -
   1.269 -
   1.270 -lemma image_Collect: "f ` {x. P x} = {f x | x. P x}"
   1.271 -  -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
   1.272 -      with its implicit quantifier and conjunction.  Also image enjoys better
   1.273 -      equational properties than does the RHS. *}
   1.274 -  by blast
   1.275 -
   1.276 -lemma if_image_distrib [simp]:
   1.277 -  "(\<lambda>x. if P x then f x else g x) ` S
   1.278 -    = (f ` (S \<inter> {x. P x})) \<union> (g ` (S \<inter> {x. \<not> P x}))"
   1.279 -  by (auto simp add: image_def)
   1.280 -
   1.281 -lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> f`M = g`N"
   1.282 -  by (simp add: image_def)
   1.283 -
   1.284 -lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
   1.285 -by blast
   1.286 -
   1.287 -lemma image_diff_subset: "f`A - f`B <= f`(A - B)"
   1.288 -by blast
   1.289 -
   1.290 -
   1.291 -text {* \medskip @{text range}. *}
   1.292 -
   1.293 -lemma full_SetCompr_eq: "{u. \<exists>x. u = f x} = range f"
   1.294 -  by auto
   1.295 -
   1.296 -lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
   1.297 -by (subst image_image, simp)
   1.298 -
   1.299  
   1.300  text {* \medskip @{text Int} *}
   1.301