# HG changeset patch
# User nipkow
# Date 1285009765 -7200
# Node ID 9f86e46779e4a4777d31afa9dfbc786296fb97cd
# Parent  e7d4923b9b1c9f47558eb3e25d34d4bde6c5a363
new lemmas

diff -r e7d4923b9b1c -r 9f86e46779e4 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Mon Sep 20 14:50:45 2010 +0200
+++ b/src/HOL/Library/FuncSet.thy	Mon Sep 20 21:09:25 2010 +0200
@@ -173,6 +173,20 @@
 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}.*}
 
+lemma bij_betwI:
+assumes "f \<in> A \<rightarrow> B" and "g \<in> B \<rightarrow> A"
+    and g_f: "\<And>x. x\<in>A \<Longrightarrow> g (f x) = x" and f_g: "\<And>y. y\<in>B \<Longrightarrow> f (g y) = y"
+shows "bij_betw f A B"
+unfolding bij_betw_def
+proof
+  show "inj_on f A" by (metis g_f inj_on_def)
+next
+  have "f ` A \<subseteq> B" using `f \<in> A \<rightarrow> B` by auto
+  moreover
+  have "B \<subseteq> f ` A" by auto (metis Pi_mem `g \<in> B \<rightarrow> A` f_g image_iff)
+  ultimately show "f ` A = B" by blast
+qed
+
 lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B"
 by (auto simp add: bij_betw_def)
 
@@ -207,6 +221,9 @@
       !!x. x\<in>A ==> f x = g x |] ==> f = g"
 by (force simp add: fun_eq_iff extensional_def)
 
+lemma extensional_restrict:  "f \<in> extensional A \<Longrightarrow> restrict f A = f"
+by(rule extensionalityI[OF restrict_extensional]) auto
+
 lemma inv_into_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_into A f x) : B -> A"
 by (unfold inv_into_def) (fast intro: someI2)