moved lemmas from 'Fun_More_FP' to where they belong
authorblanchet
Thu Jan 16 16:50:41 2014 +0100 (2014-01-16)
changeset 550190d5e831175de
parent 55018 2a526bd279ed
child 55020 96b05fd2aee4
moved lemmas from 'Fun_More_FP' to where they belong
src/HOL/Cardinals/Fun_More_FP.thy
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Cardinals/Fun_More_FP.thy	Thu Jan 16 16:33:19 2014 +0100
     1.2 +++ b/src/HOL/Cardinals/Fun_More_FP.thy	Thu Jan 16 16:50:41 2014 +0100
     1.3 @@ -18,89 +18,16 @@
     1.4  finite sets. *}
     1.5  
     1.6  
     1.7 -subsection {* Purely functional properties  *}
     1.8 -
     1.9 -
    1.10 -(*2*)lemma bij_betw_id_iff:
    1.11 -"(A = B) = (bij_betw id A B)"
    1.12 -by(simp add: bij_betw_def)
    1.13 -
    1.14 -
    1.15 -(*2*)lemma bij_betw_byWitness:
    1.16 -assumes LEFT: "\<forall>a \<in> A. f'(f a) = a" and
    1.17 -        RIGHT: "\<forall>a' \<in> A'. f(f' a') = a'" and
    1.18 -        IM1: "f ` A \<le> A'" and IM2: "f' ` A' \<le> A"
    1.19 -shows "bij_betw f A A'"
    1.20 -using assms
    1.21 -proof(unfold bij_betw_def inj_on_def, safe)
    1.22 -  fix a b assume *: "a \<in> A" "b \<in> A" and **: "f a = f b"
    1.23 -  have "a = f'(f a) \<and> b = f'(f b)" using * LEFT by simp
    1.24 -  with ** show "a = b" by simp
    1.25 -next
    1.26 -  fix a' assume *: "a' \<in> A'"
    1.27 -  hence "f' a' \<in> A" using IM2 by blast
    1.28 -  moreover
    1.29 -  have "a' = f(f' a')" using * RIGHT by simp
    1.30 -  ultimately show "a' \<in> f ` A" by blast
    1.31 -qed
    1.32 -
    1.33 -
    1.34 -(*3*)corollary notIn_Un_bij_betw:
    1.35 -assumes NIN: "b \<notin> A" and NIN': "f b \<notin> A'" and
    1.36 -       BIJ: "bij_betw f A A'"
    1.37 -shows "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
    1.38 -proof-
    1.39 -  have "bij_betw f {b} {f b}"
    1.40 -  unfolding bij_betw_def inj_on_def by simp
    1.41 -  with assms show ?thesis
    1.42 -  using bij_betw_combine[of f A A' "{b}" "{f b}"] by blast
    1.43 -qed
    1.44 -
    1.45 -
    1.46 -(*1*)lemma notIn_Un_bij_betw3:
    1.47 -assumes NIN: "b \<notin> A" and NIN': "f b \<notin> A'"
    1.48 -shows "bij_betw f A A' = bij_betw f (A \<union> {b}) (A' \<union> {f b})"
    1.49 -proof
    1.50 -  assume "bij_betw f A A'"
    1.51 -  thus "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
    1.52 -  using assms notIn_Un_bij_betw[of b A f A'] by blast
    1.53 -next
    1.54 -  assume *: "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
    1.55 -  have "f ` A = A'"
    1.56 -  proof(auto)
    1.57 -    fix a assume **: "a \<in> A"
    1.58 -    hence "f a \<in> A' \<union> {f b}" using * unfolding bij_betw_def by blast
    1.59 -    moreover
    1.60 -    {assume "f a = f b"
    1.61 -     hence "a = b" using * ** unfolding bij_betw_def inj_on_def by blast
    1.62 -     with NIN ** have False by blast
    1.63 -    }
    1.64 -    ultimately show "f a \<in> A'" by blast
    1.65 -  next
    1.66 -    fix a' assume **: "a' \<in> A'"
    1.67 -    hence "a' \<in> f`(A \<union> {b})"
    1.68 -    using * by (auto simp add: bij_betw_def)
    1.69 -    then obtain a where 1: "a \<in> A \<union> {b} \<and> f a = a'" by blast
    1.70 -    moreover
    1.71 -    {assume "a = b" with 1 ** NIN' have False by blast
    1.72 -    }
    1.73 -    ultimately have "a \<in> A" by blast
    1.74 -    with 1 show "a' \<in> f ` A" by blast
    1.75 -  qed
    1.76 -  thus "bij_betw f A A'" using * bij_betw_subset[of f "A \<union> {b}" _ A] by blast
    1.77 -qed
    1.78 -
    1.79 -
    1.80  subsection {* Properties involving finite and infinite sets *}
    1.81  
    1.82  
    1.83 -(*3*)lemma inj_on_finite:
    1.84 +lemma inj_on_finite:
    1.85  assumes "inj_on f A" "f ` A \<le> B" "finite B"
    1.86  shows "finite A"
    1.87  using assms by (metis finite_imageD finite_subset)
    1.88  
    1.89  
    1.90 -(*3*)lemma infinite_imp_bij_betw:
    1.91 +lemma infinite_imp_bij_betw:
    1.92  assumes INF: "\<not> finite A"
    1.93  shows "\<exists>h. bij_betw h A (A - {a})"
    1.94  proof(cases "a \<in> A")
    1.95 @@ -179,7 +106,7 @@
    1.96  qed
    1.97  
    1.98  
    1.99 -(*3*)lemma infinite_imp_bij_betw2:
   1.100 +lemma infinite_imp_bij_betw2:
   1.101  assumes INF: "\<not> finite A"
   1.102  shows "\<exists>h. bij_betw h A (A \<union> {a})"
   1.103  proof(cases "a \<in> A")
   1.104 @@ -199,19 +126,19 @@
   1.105  subsection {* Properties involving Hilbert choice *}
   1.106  
   1.107  
   1.108 -(*2*)lemma bij_betw_inv_into_left:
   1.109 +lemma bij_betw_inv_into_left:
   1.110  assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A"
   1.111  shows "(inv_into A f) (f a) = a"
   1.112  using assms unfolding bij_betw_def
   1.113  by clarify (rule inv_into_f_f)
   1.114  
   1.115 -(*2*)lemma bij_betw_inv_into_right:
   1.116 +lemma bij_betw_inv_into_right:
   1.117  assumes "bij_betw f A A'" "a' \<in> A'"
   1.118  shows "f(inv_into A f a') = a'"
   1.119  using assms unfolding bij_betw_def using f_inv_into_f by force
   1.120  
   1.121  
   1.122 -(*1*)lemma bij_betw_inv_into_subset:
   1.123 +lemma bij_betw_inv_into_subset:
   1.124  assumes BIJ: "bij_betw f A A'" and
   1.125          SUB: "B \<le> A" and IM: "f ` B = B'"
   1.126  shows "bij_betw (inv_into A f) B' B"
     2.1 --- a/src/HOL/Fun.thy	Thu Jan 16 16:33:19 2014 +0100
     2.2 +++ b/src/HOL/Fun.thy	Thu Jan 16 16:50:41 2014 +0100
     2.3 @@ -1,6 +1,7 @@
     2.4  (*  Title:      HOL/Fun.thy
     2.5      Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     2.6 -    Copyright   1994  University of Cambridge
     2.7 +    Author:     Andrei Popescu, TU Muenchen
     2.8 +    Copyright   1994, 2012
     2.9  *)
    2.10  
    2.11  header {* Notions about functions *}
    2.12 @@ -296,7 +297,7 @@
    2.13    assumes "inj_on f A"
    2.14    assumes "x \<notin> B" and "insert x B = f ` A"
    2.15    obtains x' A' where "x' \<notin> A'" and "A = insert x' A'"
    2.16 -    and "x = f x'" and "B = f ` A'" 
    2.17 +    and "x = f x'" and "B = f ` A'"
    2.18  proof -
    2.19    from assms have "x \<in> f ` A" by auto
    2.20    then obtain x' where *: "x' \<in> A" "x = f x'" by auto
    2.21 @@ -575,6 +576,68 @@
    2.22  lemma (in linorder) strict_mono_imp_inj_on: "strict_mono f \<Longrightarrow> inj_on f A"
    2.23    by (auto intro!: inj_onI dest: strict_mono_eq)
    2.24  
    2.25 +lemma bij_betw_byWitness:
    2.26 +assumes LEFT: "\<forall>a \<in> A. f'(f a) = a" and
    2.27 +        RIGHT: "\<forall>a' \<in> A'. f(f' a') = a'" and
    2.28 +        IM1: "f ` A \<le> A'" and IM2: "f' ` A' \<le> A"
    2.29 +shows "bij_betw f A A'"
    2.30 +using assms
    2.31 +proof(unfold bij_betw_def inj_on_def, safe)
    2.32 +  fix a b assume *: "a \<in> A" "b \<in> A" and **: "f a = f b"
    2.33 +  have "a = f'(f a) \<and> b = f'(f b)" using * LEFT by simp
    2.34 +  with ** show "a = b" by simp
    2.35 +next
    2.36 +  fix a' assume *: "a' \<in> A'"
    2.37 +  hence "f' a' \<in> A" using IM2 by blast
    2.38 +  moreover
    2.39 +  have "a' = f(f' a')" using * RIGHT by simp
    2.40 +  ultimately show "a' \<in> f ` A" by blast
    2.41 +qed
    2.42 +
    2.43 +corollary notIn_Un_bij_betw:
    2.44 +assumes NIN: "b \<notin> A" and NIN': "f b \<notin> A'" and
    2.45 +       BIJ: "bij_betw f A A'"
    2.46 +shows "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
    2.47 +proof-
    2.48 +  have "bij_betw f {b} {f b}"
    2.49 +  unfolding bij_betw_def inj_on_def by simp
    2.50 +  with assms show ?thesis
    2.51 +  using bij_betw_combine[of f A A' "{b}" "{f b}"] by blast
    2.52 +qed
    2.53 +
    2.54 +lemma notIn_Un_bij_betw3:
    2.55 +assumes NIN: "b \<notin> A" and NIN': "f b \<notin> A'"
    2.56 +shows "bij_betw f A A' = bij_betw f (A \<union> {b}) (A' \<union> {f b})"
    2.57 +proof
    2.58 +  assume "bij_betw f A A'"
    2.59 +  thus "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
    2.60 +  using assms notIn_Un_bij_betw[of b A f A'] by blast
    2.61 +next
    2.62 +  assume *: "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
    2.63 +  have "f ` A = A'"
    2.64 +  proof(auto)
    2.65 +    fix a assume **: "a \<in> A"
    2.66 +    hence "f a \<in> A' \<union> {f b}" using * unfolding bij_betw_def by blast
    2.67 +    moreover
    2.68 +    {assume "f a = f b"
    2.69 +     hence "a = b" using * ** unfolding bij_betw_def inj_on_def by blast
    2.70 +     with NIN ** have False by blast
    2.71 +    }
    2.72 +    ultimately show "f a \<in> A'" by blast
    2.73 +  next
    2.74 +    fix a' assume **: "a' \<in> A'"
    2.75 +    hence "a' \<in> f`(A \<union> {b})"
    2.76 +    using * by (auto simp add: bij_betw_def)
    2.77 +    then obtain a where 1: "a \<in> A \<union> {b} \<and> f a = a'" by blast
    2.78 +    moreover
    2.79 +    {assume "a = b" with 1 ** NIN' have False by blast
    2.80 +    }
    2.81 +    ultimately have "a \<in> A" by blast
    2.82 +    with 1 show "a' \<in> f ` A" by blast
    2.83 +  qed
    2.84 +  thus "bij_betw f A A'" using * bij_betw_subset[of f "A \<union> {b}" _ A] by blast
    2.85 +qed
    2.86 +
    2.87  
    2.88  subsection{*Function Updating*}
    2.89  
    2.90 @@ -856,4 +919,3 @@
    2.91  lemmas vimage_compose = vimage_comp
    2.92  
    2.93  end
    2.94 -