summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Thu, 16 Jan 2014 16:50:41 +0100 | |

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 | comparison | revisions | |

src/HOL/Fun.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Cardinals/Fun_More_FP.thy Thu Jan 16 16:33:19 2014 +0100 +++ b/src/HOL/Cardinals/Fun_More_FP.thy Thu Jan 16 16:50:41 2014 +0100 @@ -18,89 +18,16 @@ finite sets. *} -subsection {* Purely functional properties *} - - -(*2*)lemma bij_betw_id_iff: -"(A = B) = (bij_betw id A B)" -by(simp add: bij_betw_def) - - -(*2*)lemma bij_betw_byWitness: -assumes LEFT: "\<forall>a \<in> A. f'(f a) = a" and - RIGHT: "\<forall>a' \<in> A'. f(f' a') = a'" and - IM1: "f ` A \<le> A'" and IM2: "f' ` A' \<le> A" -shows "bij_betw f A A'" -using assms -proof(unfold bij_betw_def inj_on_def, safe) - fix a b assume *: "a \<in> A" "b \<in> A" and **: "f a = f b" - have "a = f'(f a) \<and> b = f'(f b)" using * LEFT by simp - with ** show "a = b" by simp -next - fix a' assume *: "a' \<in> A'" - hence "f' a' \<in> A" using IM2 by blast - moreover - have "a' = f(f' a')" using * RIGHT by simp - ultimately show "a' \<in> f ` A" by blast -qed - - -(*3*)corollary notIn_Un_bij_betw: -assumes NIN: "b \<notin> A" and NIN': "f b \<notin> A'" and - BIJ: "bij_betw f A A'" -shows "bij_betw f (A \<union> {b}) (A' \<union> {f b})" -proof- - have "bij_betw f {b} {f b}" - unfolding bij_betw_def inj_on_def by simp - with assms show ?thesis - using bij_betw_combine[of f A A' "{b}" "{f b}"] by blast -qed - - -(*1*)lemma notIn_Un_bij_betw3: -assumes NIN: "b \<notin> A" and NIN': "f b \<notin> A'" -shows "bij_betw f A A' = bij_betw f (A \<union> {b}) (A' \<union> {f b})" -proof - assume "bij_betw f A A'" - thus "bij_betw f (A \<union> {b}) (A' \<union> {f b})" - using assms notIn_Un_bij_betw[of b A f A'] by blast -next - assume *: "bij_betw f (A \<union> {b}) (A' \<union> {f b})" - have "f ` A = A'" - proof(auto) - fix a assume **: "a \<in> A" - hence "f a \<in> A' \<union> {f b}" using * unfolding bij_betw_def by blast - moreover - {assume "f a = f b" - hence "a = b" using * ** unfolding bij_betw_def inj_on_def by blast - with NIN ** have False by blast - } - ultimately show "f a \<in> A'" by blast - next - fix a' assume **: "a' \<in> A'" - hence "a' \<in> f`(A \<union> {b})" - using * by (auto simp add: bij_betw_def) - then obtain a where 1: "a \<in> A \<union> {b} \<and> f a = a'" by blast - moreover - {assume "a = b" with 1 ** NIN' have False by blast - } - ultimately have "a \<in> A" by blast - with 1 show "a' \<in> f ` A" by blast - qed - thus "bij_betw f A A'" using * bij_betw_subset[of f "A \<union> {b}" _ A] by blast -qed - - subsection {* Properties involving finite and infinite sets *} -(*3*)lemma inj_on_finite: +lemma inj_on_finite: assumes "inj_on f A" "f ` A \<le> B" "finite B" shows "finite A" using assms by (metis finite_imageD finite_subset) -(*3*)lemma infinite_imp_bij_betw: +lemma infinite_imp_bij_betw: assumes INF: "\<not> finite A" shows "\<exists>h. bij_betw h A (A - {a})" proof(cases "a \<in> A") @@ -179,7 +106,7 @@ qed -(*3*)lemma infinite_imp_bij_betw2: +lemma infinite_imp_bij_betw2: assumes INF: "\<not> finite A" shows "\<exists>h. bij_betw h A (A \<union> {a})" proof(cases "a \<in> A") @@ -199,19 +126,19 @@ subsection {* Properties involving Hilbert choice *} -(*2*)lemma bij_betw_inv_into_left: +lemma bij_betw_inv_into_left: assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A" shows "(inv_into A f) (f a) = a" using assms unfolding bij_betw_def by clarify (rule inv_into_f_f) -(*2*)lemma bij_betw_inv_into_right: +lemma bij_betw_inv_into_right: assumes "bij_betw f A A'" "a' \<in> A'" shows "f(inv_into A f a') = a'" using assms unfolding bij_betw_def using f_inv_into_f by force -(*1*)lemma bij_betw_inv_into_subset: +lemma bij_betw_inv_into_subset: assumes BIJ: "bij_betw f A A'" and SUB: "B \<le> A" and IM: "f ` B = B'" shows "bij_betw (inv_into A f) B' B"

--- a/src/HOL/Fun.thy Thu Jan 16 16:33:19 2014 +0100 +++ b/src/HOL/Fun.thy Thu Jan 16 16:50:41 2014 +0100 @@ -1,6 +1,7 @@ (* Title: HOL/Fun.thy Author: Tobias Nipkow, Cambridge University Computer Laboratory - Copyright 1994 University of Cambridge + Author: Andrei Popescu, TU Muenchen + Copyright 1994, 2012 *) header {* Notions about functions *} @@ -296,7 +297,7 @@ assumes "inj_on f A" assumes "x \<notin> B" and "insert x B = f ` A" obtains x' A' where "x' \<notin> A'" and "A = insert x' A'" - and "x = f x'" and "B = f ` A'" + and "x = f x'" and "B = f ` A'" proof - from assms have "x \<in> f ` A" by auto then obtain x' where *: "x' \<in> A" "x = f x'" by auto @@ -575,6 +576,68 @@ lemma (in linorder) strict_mono_imp_inj_on: "strict_mono f \<Longrightarrow> inj_on f A" by (auto intro!: inj_onI dest: strict_mono_eq) +lemma bij_betw_byWitness: +assumes LEFT: "\<forall>a \<in> A. f'(f a) = a" and + RIGHT: "\<forall>a' \<in> A'. f(f' a') = a'" and + IM1: "f ` A \<le> A'" and IM2: "f' ` A' \<le> A" +shows "bij_betw f A A'" +using assms +proof(unfold bij_betw_def inj_on_def, safe) + fix a b assume *: "a \<in> A" "b \<in> A" and **: "f a = f b" + have "a = f'(f a) \<and> b = f'(f b)" using * LEFT by simp + with ** show "a = b" by simp +next + fix a' assume *: "a' \<in> A'" + hence "f' a' \<in> A" using IM2 by blast + moreover + have "a' = f(f' a')" using * RIGHT by simp + ultimately show "a' \<in> f ` A" by blast +qed + +corollary notIn_Un_bij_betw: +assumes NIN: "b \<notin> A" and NIN': "f b \<notin> A'" and + BIJ: "bij_betw f A A'" +shows "bij_betw f (A \<union> {b}) (A' \<union> {f b})" +proof- + have "bij_betw f {b} {f b}" + unfolding bij_betw_def inj_on_def by simp + with assms show ?thesis + using bij_betw_combine[of f A A' "{b}" "{f b}"] by blast +qed + +lemma notIn_Un_bij_betw3: +assumes NIN: "b \<notin> A" and NIN': "f b \<notin> A'" +shows "bij_betw f A A' = bij_betw f (A \<union> {b}) (A' \<union> {f b})" +proof + assume "bij_betw f A A'" + thus "bij_betw f (A \<union> {b}) (A' \<union> {f b})" + using assms notIn_Un_bij_betw[of b A f A'] by blast +next + assume *: "bij_betw f (A \<union> {b}) (A' \<union> {f b})" + have "f ` A = A'" + proof(auto) + fix a assume **: "a \<in> A" + hence "f a \<in> A' \<union> {f b}" using * unfolding bij_betw_def by blast + moreover + {assume "f a = f b" + hence "a = b" using * ** unfolding bij_betw_def inj_on_def by blast + with NIN ** have False by blast + } + ultimately show "f a \<in> A'" by blast + next + fix a' assume **: "a' \<in> A'" + hence "a' \<in> f`(A \<union> {b})" + using * by (auto simp add: bij_betw_def) + then obtain a where 1: "a \<in> A \<union> {b} \<and> f a = a'" by blast + moreover + {assume "a = b" with 1 ** NIN' have False by blast + } + ultimately have "a \<in> A" by blast + with 1 show "a' \<in> f ` A" by blast + qed + thus "bij_betw f A A'" using * bij_betw_subset[of f "A \<union> {b}" _ A] by blast +qed + subsection{*Function Updating*} @@ -856,4 +919,3 @@ lemmas vimage_compose = vimage_comp end -