src/HOL/Library/FuncSet.thy
changeset 26106 be52145f482d
parent 21404 eb85850d3eb7
child 27183 0fc4c0f97a1b
     1.1 --- a/src/HOL/Library/FuncSet.thy	Thu Feb 21 17:33:58 2008 +0100
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Thu Feb 21 17:34:09 2008 +0100
     1.3 @@ -141,25 +141,12 @@
     1.4  
     1.5  subsection{*Bijections Between Sets*}
     1.6  
     1.7 -text{*The basic definition could be moved to @{text "Fun.thy"}, but most of
     1.8 +text{*The definition of @{const bij_betw} is in @{text "Fun.thy"}, but most of
     1.9  the theorems belong here, or need at least @{term Hilbert_Choice}.*}
    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 = (inj_on f A & f ` A = B)"
    1.14 -
    1.15 -lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
    1.16 -  by (simp add: bij_betw_def)
    1.17 -
    1.18  lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B"
    1.19    by (auto simp add: bij_betw_def inj_on_Inv Pi_def)
    1.20  
    1.21 -lemma bij_betw_Inv: "bij_betw f A B \<Longrightarrow> bij_betw (Inv A f) B A"
    1.22 -  apply (auto simp add: bij_betw_def inj_on_Inv Inv_mem)
    1.23 -  apply (simp add: image_compose [symmetric] o_def)
    1.24 -  apply (simp add: image_def Inv_f_f)
    1.25 -  done
    1.26 -
    1.27  lemma inj_on_compose:
    1.28      "[| bij_betw f A B; inj_on g B |] ==> inj_on (compose A g f) A"
    1.29    by (auto simp add: bij_betw_def inj_on_def compose_eq)