src/HOL/Fun.thy
changeset 40703 d1fc454d6735
parent 40702 cf26dd7395e4
child 40719 acb830207103
     1.1 --- a/src/HOL/Fun.thy	Mon Nov 22 10:34:33 2010 +0100
     1.2 +++ b/src/HOL/Fun.thy	Tue Nov 23 14:14:17 2010 +0100
     1.3 @@ -169,6 +169,14 @@
     1.4  lemma inj_on_eq_iff: "inj_on f A ==> x:A ==> y:A ==> (f(x) = f(y)) = (x=y)"
     1.5  by (force simp add: inj_on_def)
     1.6  
     1.7 +lemma inj_on_cong:
     1.8 +  "(\<And> a. a : A \<Longrightarrow> f a = g a) \<Longrightarrow> inj_on f A = inj_on g A"
     1.9 +unfolding inj_on_def by auto
    1.10 +
    1.11 +lemma inj_on_strict_subset:
    1.12 +  "\<lbrakk> inj_on f B; A < B \<rbrakk> \<Longrightarrow> f`A < f`B"
    1.13 +unfolding inj_on_def unfolding image_def by blast
    1.14 +
    1.15  lemma inj_comp:
    1.16    "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
    1.17    by (simp add: inj_on_def)
    1.18 @@ -185,6 +193,42 @@
    1.19  lemma inj_on_id2[simp]: "inj_on (%x. x) A"
    1.20  by (simp add: inj_on_def)
    1.21  
    1.22 +lemma inj_on_Int: "\<lbrakk>inj_on f A; inj_on f B\<rbrakk> \<Longrightarrow> inj_on f (A \<inter> B)"
    1.23 +unfolding inj_on_def by blast
    1.24 +
    1.25 +lemma inj_on_INTER:
    1.26 +  "\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)\<rbrakk> \<Longrightarrow> inj_on f (\<Inter> i \<in> I. A i)"
    1.27 +unfolding inj_on_def by blast
    1.28 +
    1.29 +lemma inj_on_Inter:
    1.30 +  "\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> inj_on f A\<rbrakk> \<Longrightarrow> inj_on f (Inter S)"
    1.31 +unfolding inj_on_def by blast
    1.32 +
    1.33 +lemma inj_on_UNION_chain:
    1.34 +  assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
    1.35 +         INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
    1.36 +  shows "inj_on f (\<Union> i \<in> I. A i)"
    1.37 +proof(unfold inj_on_def UNION_def, auto)
    1.38 +  fix i j x y
    1.39 +  assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
    1.40 +         and ***: "f x = f y"
    1.41 +  show "x = y"
    1.42 +  proof-
    1.43 +    {assume "A i \<le> A j"
    1.44 +     with ** have "x \<in> A j" by auto
    1.45 +     with INJ * ** *** have ?thesis
    1.46 +     by(auto simp add: inj_on_def)
    1.47 +    }
    1.48 +    moreover
    1.49 +    {assume "A j \<le> A i"
    1.50 +     with ** have "y \<in> A i" by auto
    1.51 +     with INJ * ** *** have ?thesis
    1.52 +     by(auto simp add: inj_on_def)
    1.53 +    }
    1.54 +    ultimately show ?thesis using  CH * by blast
    1.55 +  qed
    1.56 +qed
    1.57 +
    1.58  lemma surj_id: "surj id"
    1.59  by simp
    1.60  
    1.61 @@ -249,6 +293,14 @@
    1.62  apply (blast)
    1.63  done
    1.64  
    1.65 +lemma comp_inj_on_iff:
    1.66 +  "inj_on f A \<Longrightarrow> inj_on f' (f ` A) \<longleftrightarrow> inj_on (f' o f) A"
    1.67 +by(auto simp add: comp_inj_on inj_on_def)
    1.68 +
    1.69 +lemma inj_on_imageI2:
    1.70 +  "inj_on (f' o f) A \<Longrightarrow> inj_on f A"
    1.71 +by(auto simp add: comp_inj_on inj_on_def)
    1.72 +
    1.73  lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
    1.74    by auto
    1.75  
    1.76 @@ -270,6 +322,20 @@
    1.77  lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
    1.78    unfolding bij_betw_def by auto
    1.79  
    1.80 +lemma bij_betw_empty1:
    1.81 +  assumes "bij_betw f {} A"
    1.82 +  shows "A = {}"
    1.83 +using assms unfolding bij_betw_def by blast
    1.84 +
    1.85 +lemma bij_betw_empty2:
    1.86 +  assumes "bij_betw f A {}"
    1.87 +  shows "A = {}"
    1.88 +using assms unfolding bij_betw_def by blast
    1.89 +
    1.90 +lemma inj_on_imp_bij_betw:
    1.91 +  "inj_on f A \<Longrightarrow> bij_betw f A (f ` A)"
    1.92 +unfolding bij_betw_def by simp
    1.93 +
    1.94  lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
    1.95    unfolding bij_betw_def ..
    1.96  
    1.97 @@ -292,6 +358,32 @@
    1.98  lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
    1.99    by (rule bij_betw_trans)
   1.100  
   1.101 +lemma bij_betw_comp_iff:
   1.102 +  "bij_betw f A A' \<Longrightarrow> bij_betw f' A' A'' \<longleftrightarrow> bij_betw (f' o f) A A''"
   1.103 +by(auto simp add: bij_betw_def inj_on_def)
   1.104 +
   1.105 +lemma bij_betw_comp_iff2:
   1.106 +  assumes BIJ: "bij_betw f' A' A''" and IM: "f ` A \<le> A'"
   1.107 +  shows "bij_betw f A A' \<longleftrightarrow> bij_betw (f' o f) A A''"
   1.108 +using assms
   1.109 +proof(auto simp add: bij_betw_comp_iff)
   1.110 +  assume *: "bij_betw (f' \<circ> f) A A''"
   1.111 +  thus "bij_betw f A A'"
   1.112 +  using IM
   1.113 +  proof(auto simp add: bij_betw_def)
   1.114 +    assume "inj_on (f' \<circ> f) A"
   1.115 +    thus "inj_on f A" using inj_on_imageI2 by blast
   1.116 +  next
   1.117 +    fix a' assume **: "a' \<in> A'"
   1.118 +    hence "f' a' \<in> A''" using BIJ unfolding bij_betw_def by auto
   1.119 +    then obtain a where 1: "a \<in> A \<and> f'(f a) = f' a'" using *
   1.120 +    unfolding bij_betw_def by force
   1.121 +    hence "f a \<in> A'" using IM by auto
   1.122 +    hence "f a = a'" using BIJ ** 1 unfolding bij_betw_def inj_on_def by auto
   1.123 +    thus "a' \<in> f ` A" using 1 by auto
   1.124 +  qed
   1.125 +qed
   1.126 +
   1.127  lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A"
   1.128  proof -
   1.129    have i: "inj_on f A" and s: "f ` A = B"
   1.130 @@ -323,11 +415,73 @@
   1.131    ultimately show ?thesis by(auto simp:bij_betw_def)
   1.132  qed
   1.133  
   1.134 +lemma bij_betw_cong:
   1.135 +  "(\<And> a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> bij_betw f A A' = bij_betw g A A'"
   1.136 +unfolding bij_betw_def inj_on_def by force
   1.137 +
   1.138 +lemma bij_betw_id[intro, simp]:
   1.139 +  "bij_betw id A A"
   1.140 +unfolding bij_betw_def id_def by auto
   1.141 +
   1.142 +lemma bij_betw_id_iff:
   1.143 +  "bij_betw id A B \<longleftrightarrow> A = B"
   1.144 +by(auto simp add: bij_betw_def)
   1.145 +
   1.146  lemma bij_betw_combine:
   1.147    assumes "bij_betw f A B" "bij_betw f C D" "B \<inter> D = {}"
   1.148    shows "bij_betw f (A \<union> C) (B \<union> D)"
   1.149    using assms unfolding bij_betw_def inj_on_Un image_Un by auto
   1.150  
   1.151 +lemma bij_betw_UNION_chain:
   1.152 +  assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
   1.153 +         BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
   1.154 +  shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
   1.155 +proof(unfold bij_betw_def, auto simp add: image_def)
   1.156 +  have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
   1.157 +  using BIJ bij_betw_def[of f] by auto
   1.158 +  thus "inj_on f (\<Union> i \<in> I. A i)"
   1.159 +  using CH inj_on_UNION_chain[of I A f] by auto
   1.160 +next
   1.161 +  fix i x
   1.162 +  assume *: "i \<in> I" "x \<in> A i"
   1.163 +  hence "f x \<in> A' i" using BIJ bij_betw_def[of f] by auto
   1.164 +  thus "\<exists>j \<in> I. f x \<in> A' j" using * by blast
   1.165 +next
   1.166 +  fix i x'
   1.167 +  assume *: "i \<in> I" "x' \<in> A' i"
   1.168 +  hence "\<exists>x \<in> A i. x' = f x" using BIJ bij_betw_def[of f] by blast
   1.169 +  thus "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
   1.170 +  using * by blast
   1.171 +qed
   1.172 +
   1.173 +lemma bij_betw_Disj_Un:
   1.174 +  assumes DISJ: "A \<inter> B = {}" and DISJ': "A' \<inter> B' = {}" and
   1.175 +          B1: "bij_betw f A A'" and B2: "bij_betw f B B'"
   1.176 +  shows "bij_betw f (A \<union> B) (A' \<union> B')"
   1.177 +proof-
   1.178 +  have 1: "inj_on f A \<and> inj_on f B"
   1.179 +  using B1 B2 by (auto simp add: bij_betw_def)
   1.180 +  have 2: "f`A = A' \<and> f`B = B'"
   1.181 +  using B1 B2 by (auto simp add: bij_betw_def)
   1.182 +  hence "f`(A - B) \<inter> f`(B - A) = {}"
   1.183 +  using DISJ DISJ' by blast
   1.184 +  hence "inj_on f (A \<union> B)"
   1.185 +  using 1 by (auto simp add: inj_on_Un)
   1.186 +  (*  *)
   1.187 +  moreover
   1.188 +  have "f`(A \<union> B) = A' \<union> B'"
   1.189 +  using 2 by auto
   1.190 +  ultimately show ?thesis
   1.191 +  unfolding bij_betw_def by auto
   1.192 +qed
   1.193 +
   1.194 +lemma bij_betw_subset:
   1.195 +  assumes BIJ: "bij_betw f A A'" and
   1.196 +          SUB: "B \<le> A" and IM: "f ` B = B'"
   1.197 +  shows "bij_betw f B B'"
   1.198 +using assms
   1.199 +by(unfold bij_betw_def inj_on_def, auto simp add: inj_on_def)
   1.200 +
   1.201  lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
   1.202  by simp
   1.203  
   1.204 @@ -613,6 +767,17 @@
   1.205    shows "the_inv f (f x) = x" using assms UNIV_I
   1.206    by (rule the_inv_into_f_f)
   1.207  
   1.208 +subsection {* Cantor's Paradox *}
   1.209 +
   1.210 +lemma Cantors_paradox:
   1.211 +  "\<not>(\<exists>f. f ` A = Pow A)"
   1.212 +proof clarify
   1.213 +  fix f assume "f ` A = Pow A" hence *: "Pow A \<le> f ` A" by blast
   1.214 +  let ?X = "{a \<in> A. a \<notin> f a}"
   1.215 +  have "?X \<in> Pow A" unfolding Pow_def by auto
   1.216 +  with * obtain x where "x \<in> A \<and> f x = ?X" by blast
   1.217 +  thus False by best
   1.218 +qed
   1.219  
   1.220  subsection {* Proof tool setup *} 
   1.221