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 -