# HG changeset patch
# User nipkow
# Date 1203611649 -3600
# Node ID be52145f482d9c95139ee51168d0b829b078d5a2
# Parent  ae06618225eccabb623a10fb9ef0504c97d1cb75
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas

diff -r ae06618225ec -r be52145f482d src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Thu Feb 21 17:33:58 2008 +0100
+++ b/src/HOL/Library/FuncSet.thy	Thu Feb 21 17:34:09 2008 +0100
@@ -141,25 +141,12 @@
 
 subsection{*Bijections Between Sets*}
 
-text{*The basic definition could be moved to @{text "Fun.thy"}, but most of
+text{*The definition of @{const bij_betw} is in @{text "Fun.thy"}, but most of
 the theorems belong here, or need at least @{term Hilbert_Choice}.*}
 
-definition
-  bij_betw :: "['a => 'b, 'a set, 'b set] => bool" where -- {* bijective *}
-  "bij_betw f A B = (inj_on f A & f ` A = B)"
-
-lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
-  by (simp add: bij_betw_def)
-
 lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B"
   by (auto simp add: bij_betw_def inj_on_Inv Pi_def)
 
-lemma bij_betw_Inv: "bij_betw f A B \<Longrightarrow> bij_betw (Inv A f) B A"
-  apply (auto simp add: bij_betw_def inj_on_Inv Inv_mem)
-  apply (simp add: image_compose [symmetric] o_def)
-  apply (simp add: image_def Inv_f_f)
-  done
-
 lemma inj_on_compose:
     "[| bij_betw f A B; inj_on g B |] ==> inj_on (compose A g f) A"
   by (auto simp add: bij_betw_def inj_on_def compose_eq)