src/HOL/Fun.thy
 changeset 55019 0d5e831175de parent 54578 9387251b6a46 child 55066 4e5ddf3162ac
```     1.1 --- a/src/HOL/Fun.thy	Thu Jan 16 16:33:19 2014 +0100
1.2 +++ b/src/HOL/Fun.thy	Thu Jan 16 16:50:41 2014 +0100
1.3 @@ -1,6 +1,7 @@
1.4  (*  Title:      HOL/Fun.thy
1.5      Author:     Tobias Nipkow, Cambridge University Computer Laboratory
1.6 -    Copyright   1994  University of Cambridge
1.7 +    Author:     Andrei Popescu, TU Muenchen
1.8 +    Copyright   1994, 2012
1.9  *)
1.10
1.11  header {* Notions about functions *}
1.12 @@ -296,7 +297,7 @@
1.13    assumes "inj_on f A"
1.14    assumes "x \<notin> B" and "insert x B = f ` A"
1.15    obtains x' A' where "x' \<notin> A'" and "A = insert x' A'"
1.16 -    and "x = f x'" and "B = f ` A'"
1.17 +    and "x = f x'" and "B = f ` A'"
1.18  proof -
1.19    from assms have "x \<in> f ` A" by auto
1.20    then obtain x' where *: "x' \<in> A" "x = f x'" by auto
1.21 @@ -575,6 +576,68 @@
1.22  lemma (in linorder) strict_mono_imp_inj_on: "strict_mono f \<Longrightarrow> inj_on f A"
1.23    by (auto intro!: inj_onI dest: strict_mono_eq)
1.24
1.25 +lemma bij_betw_byWitness:
1.26 +assumes LEFT: "\<forall>a \<in> A. f'(f a) = a" and
1.27 +        RIGHT: "\<forall>a' \<in> A'. f(f' a') = a'" and
1.28 +        IM1: "f ` A \<le> A'" and IM2: "f' ` A' \<le> A"
1.29 +shows "bij_betw f A A'"
1.30 +using assms
1.31 +proof(unfold bij_betw_def inj_on_def, safe)
1.32 +  fix a b assume *: "a \<in> A" "b \<in> A" and **: "f a = f b"
1.33 +  have "a = f'(f a) \<and> b = f'(f b)" using * LEFT by simp
1.34 +  with ** show "a = b" by simp
1.35 +next
1.36 +  fix a' assume *: "a' \<in> A'"
1.37 +  hence "f' a' \<in> A" using IM2 by blast
1.38 +  moreover
1.39 +  have "a' = f(f' a')" using * RIGHT by simp
1.40 +  ultimately show "a' \<in> f ` A" by blast
1.41 +qed
1.42 +
1.43 +corollary notIn_Un_bij_betw:
1.44 +assumes NIN: "b \<notin> A" and NIN': "f b \<notin> A'" and
1.45 +       BIJ: "bij_betw f A A'"
1.46 +shows "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
1.47 +proof-
1.48 +  have "bij_betw f {b} {f b}"
1.49 +  unfolding bij_betw_def inj_on_def by simp
1.50 +  with assms show ?thesis
1.51 +  using bij_betw_combine[of f A A' "{b}" "{f b}"] by blast
1.52 +qed
1.53 +
1.54 +lemma notIn_Un_bij_betw3:
1.55 +assumes NIN: "b \<notin> A" and NIN': "f b \<notin> A'"
1.56 +shows "bij_betw f A A' = bij_betw f (A \<union> {b}) (A' \<union> {f b})"
1.57 +proof
1.58 +  assume "bij_betw f A A'"
1.59 +  thus "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
1.60 +  using assms notIn_Un_bij_betw[of b A f A'] by blast
1.61 +next
1.62 +  assume *: "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
1.63 +  have "f ` A = A'"
1.64 +  proof(auto)
1.65 +    fix a assume **: "a \<in> A"
1.66 +    hence "f a \<in> A' \<union> {f b}" using * unfolding bij_betw_def by blast
1.67 +    moreover
1.68 +    {assume "f a = f b"
1.69 +     hence "a = b" using * ** unfolding bij_betw_def inj_on_def by blast
1.70 +     with NIN ** have False by blast
1.71 +    }
1.72 +    ultimately show "f a \<in> A'" by blast
1.73 +  next
1.74 +    fix a' assume **: "a' \<in> A'"
1.75 +    hence "a' \<in> f`(A \<union> {b})"
1.76 +    using * by (auto simp add: bij_betw_def)
1.77 +    then obtain a where 1: "a \<in> A \<union> {b} \<and> f a = a'" by blast
1.78 +    moreover
1.79 +    {assume "a = b" with 1 ** NIN' have False by blast
1.80 +    }
1.81 +    ultimately have "a \<in> A" by blast
1.82 +    with 1 show "a' \<in> f ` A" by blast
1.83 +  qed
1.84 +  thus "bij_betw f A A'" using * bij_betw_subset[of f "A \<union> {b}" _ A] by blast
1.85 +qed
1.86 +
1.87
1.88  subsection{*Function Updating*}
1.89
1.90 @@ -856,4 +919,3 @@
1.91  lemmas vimage_compose = vimage_comp
1.92
1.93  end
1.94 -
```