src/HOL/Fun.thy
changeset 59504 8c6747dba731
parent 58889 5b7a9633cfa8
child 59507 b468e0f8da2a
     1.1 --- a/src/HOL/Fun.thy	Tue Feb 10 12:27:30 2015 +0100
     1.2 +++ b/src/HOL/Fun.thy	Tue Feb 10 16:08:11 2015 +0000
     1.3 @@ -15,6 +15,12 @@
     1.4    "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
     1.5    by auto
     1.6  
     1.7 +text{*Uniqueness, so NOT the axiom of choice.*}
     1.8 +lemma uniq_choice: "\<forall>x. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x. Q x (f x)"
     1.9 +  by (force intro: theI')
    1.10 +
    1.11 +lemma b_uniq_choice: "\<forall>x\<in>S. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x\<in>S. Q x (f x)"
    1.12 +  by (force intro: theI')
    1.13  
    1.14  subsection {* The Identity Function @{text id} *}
    1.15  
    1.16 @@ -79,6 +85,9 @@
    1.17    "f -` (g -` x) = (g \<circ> f) -` x"
    1.18    by auto
    1.19  
    1.20 +lemma image_eq_imp_comp: "f ` A = g ` B \<Longrightarrow> (h o f) ` A = (h o g) ` B"
    1.21 +  by (auto simp: comp_def elim!: equalityE)
    1.22 +
    1.23  code_printing
    1.24    constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."
    1.25  
    1.26 @@ -477,14 +486,17 @@
    1.27  lemma image_set_diff: "inj f ==> f`(A-B) = f`A - f`B"
    1.28  by (simp add: inj_on_def, blast)
    1.29  
    1.30 -lemma inj_image_mem_iff: "inj f ==> (f a : f`A) = (a : A)"
    1.31 -by (blast dest: injD)
    1.32 +lemma inj_on_image_mem_iff: "\<lbrakk>inj_on f B; a \<in> B; A \<subseteq> B\<rbrakk> \<Longrightarrow> f a \<in> f`A \<longleftrightarrow> a \<in> A"
    1.33 +  by (auto simp: inj_on_def)
    1.34 +
    1.35 +lemma inj_image_mem_iff: "inj f \<Longrightarrow> f a \<in> f`A \<longleftrightarrow> a \<in> A"
    1.36 +  by (blast dest: injD)
    1.37  
    1.38  lemma inj_image_subset_iff: "inj f ==> (f`A <= f`B) = (A<=B)"
    1.39 -by (simp add: inj_on_def, blast)
    1.40 +  by (blast dest: injD)
    1.41  
    1.42  lemma inj_image_eq_iff: "inj f ==> (f`A = f`B) = (A = B)"
    1.43 -by (blast dest: injD)
    1.44 +  by (blast dest: injD)
    1.45  
    1.46  lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)"
    1.47  by auto