src/HOL/Fun.thy
changeset 26105 ae06618225ec
parent 25886 7753e0d81b7a
child 26147 ae2bf929e33c
     1.1 --- a/src/HOL/Fun.thy	Wed Feb 20 23:24:38 2008 +0100
     1.2 +++ b/src/HOL/Fun.thy	Thu Feb 21 17:33:58 2008 +0100
     1.3 @@ -59,9 +59,14 @@
     1.4  lemmas o_def = comp_def
     1.5  
     1.6  constdefs
     1.7 -  inj_on :: "['a => 'b, 'a set] => bool"         (*injective*)
     1.8 +  inj_on :: "['a => 'b, 'a set] => bool"  -- "injective"
     1.9    "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    1.10  
    1.11 +definition
    1.12 +  bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
    1.13 +  "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
    1.14 +
    1.15 +
    1.16  text{*A common special case: functions injective over the entire domain type.*}
    1.17  
    1.18  abbreviation
    1.19 @@ -237,8 +242,7 @@
    1.20  done
    1.21  
    1.22  
    1.23 -
    1.24 -subsection{*The Predicate @{term bij}: Bijectivity*}
    1.25 +subsection{*The Predicate @{const bij}: Bijectivity*}
    1.26  
    1.27  lemma bijI: "[| inj f; surj f |] ==> bij f"
    1.28  by (simp add: bij_def)
    1.29 @@ -250,6 +254,43 @@
    1.30  by (simp add: bij_def)
    1.31  
    1.32  
    1.33 +subsection{*The Predicate @{const bij_betw}: Bijectivity*}
    1.34 +
    1.35 +lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
    1.36 +by (simp add: bij_betw_def)
    1.37 +
    1.38 +lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A"
    1.39 +proof -
    1.40 +  have i: "inj_on f A" and s: "f ` A = B"
    1.41 +    using assms by(auto simp:bij_betw_def)
    1.42 +  let ?P = "%b a. a:A \<and> f a = b" let ?g = "%b. The (?P b)"
    1.43 +  { fix a b assume P: "?P b a"
    1.44 +    hence ex1: "\<exists>a. ?P b a" using s unfolding image_def by blast
    1.45 +    hence uex1: "\<exists>!a. ?P b a" by(blast dest:inj_onD[OF i])
    1.46 +    hence " ?g b = a" using the1_equality[OF uex1, OF P] P by simp
    1.47 +  } note g = this
    1.48 +  have "inj_on ?g B"
    1.49 +  proof(rule inj_onI)
    1.50 +    fix x y assume "x:B" "y:B" "?g x = ?g y"
    1.51 +    from s `x:B` obtain a1 where a1: "?P x a1" unfolding image_def by blast
    1.52 +    from s `y:B` obtain a2 where a2: "?P y a2" unfolding image_def by blast
    1.53 +    from g[OF a1] a1 g[OF a2] a2 `?g x = ?g y` show "x=y" by simp
    1.54 +  qed
    1.55 +  moreover have "?g ` B = A"
    1.56 +  proof(auto simp:image_def)
    1.57 +    fix b assume "b:B"
    1.58 +    with s obtain a where P: "?P b a" unfolding image_def by blast
    1.59 +    thus "?g b \<in> A" using g[OF P] by auto
    1.60 +  next
    1.61 +    fix a assume "a:A"
    1.62 +    then obtain b where P: "?P b a" using s unfolding image_def by blast
    1.63 +    then have "b:B" using s unfolding image_def by blast
    1.64 +    with g[OF P] show "\<exists>b\<in>B. a = ?g b" by blast
    1.65 +  qed
    1.66 +  ultimately show ?thesis by(auto simp:bij_betw_def)
    1.67 +qed
    1.68 +
    1.69 +
    1.70  subsection{*Facts About the Identity Function*}
    1.71  
    1.72  text{*We seem to need both the @{term id} forms and the @{term "\<lambda>x. x"}