author blanchet Thu Jan 16 16:50:41 2014 +0100 (2014-01-16) changeset 55019 0d5e831175de parent 55018 2a526bd279ed child 55020 96b05fd2aee4
moved lemmas from 'Fun_More_FP' to where they belong
 src/HOL/Cardinals/Fun_More_FP.thy file | annotate | diff | revisions src/HOL/Fun.thy file | annotate | diff | revisions
```     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.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.9  *)
2.10
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 -
```