# HG changeset patch
# User paulson
# Date 1084959056 -7200
# Node ID bd349ff7907aa5a5c28acb4ea7b6fecba7126f8a
# Parent  28b5eb4a867f086b7923a9a83577431d9308db15
new bij_betw operator

diff -r 28b5eb4a867f -r bd349ff7907a src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Wed May 19 11:30:18 2004 +0200
+++ b/src/HOL/Library/FuncSet.thy	Wed May 19 11:30:56 2004 +0200
@@ -57,6 +57,9 @@
 lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
   by (simp add: Pi_def)
 
+lemma funcset_image: "f \<in> A\<rightarrow>B ==> f ` A \<subseteq> B"
+by (auto simp add: Pi_def)
+
 lemma Pi_eq_empty: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
 apply (simp add: Pi_def, auto)
 txt{*Converse direction requires Axiom of Choice to exhibit a function
@@ -166,6 +169,34 @@
   done
 
 
+subsection{*Bijections Between Sets*}
+
+text{*The basic definition could be moved to @{text "Fun.thy"}, but most of
+the theorems belong here, or need at least @{term Hilbert_Choice}.*}
+
+constdefs
+  bij_betw :: "['a => 'b, 'a set, 'b set] => bool"         (*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 bij_betw_compose:
+    "[| bij_betw f A B; bij_betw g B C |] ==> bij_betw (compose A g f) A C"
+apply (simp add: bij_betw_def compose_eq inj_on_compose)
+apply (auto simp add: compose_def image_def)
+done
+
+
 subsection{*Cardinality*}
 
 lemma card_inj: "[|f \<in> A\<rightarrow>B; inj_on f A; finite B|] ==> card(A) \<le> card(B)"