# HG changeset patch
# User nipkow
# Date 1203611638 -3600
# Node ID ae06618225eccabb623a10fb9ef0504c97d1cb75
# Parent  200b4e401e650eeaf0057784e778f2470ac92743
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
added some

diff -r 200b4e401e65 -r ae06618225ec src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Feb 20 23:24:38 2008 +0100
+++ b/src/HOL/Fun.thy	Thu Feb 21 17:33:58 2008 +0100
@@ -59,9 +59,14 @@
 lemmas o_def = comp_def
 
 constdefs
-  inj_on :: "['a => 'b, 'a set] => bool"         (*injective*)
+  inj_on :: "['a => 'b, 'a set] => bool"  -- "injective"
   "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
 
+definition
+  bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
+  "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
+
+
 text{*A common special case: functions injective over the entire domain type.*}
 
 abbreviation
@@ -237,8 +242,7 @@
 done
 
 
-
-subsection{*The Predicate @{term bij}: Bijectivity*}
+subsection{*The Predicate @{const bij}: Bijectivity*}
 
 lemma bijI: "[| inj f; surj f |] ==> bij f"
 by (simp add: bij_def)
@@ -250,6 +254,43 @@
 by (simp add: bij_def)
 
 
+subsection{*The Predicate @{const bij_betw}: Bijectivity*}
+
+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_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A"
+proof -
+  have i: "inj_on f A" and s: "f ` A = B"
+    using assms by(auto simp:bij_betw_def)
+  let ?P = "%b a. a:A \<and> f a = b" let ?g = "%b. The (?P b)"
+  { fix a b assume P: "?P b a"
+    hence ex1: "\<exists>a. ?P b a" using s unfolding image_def by blast
+    hence uex1: "\<exists>!a. ?P b a" by(blast dest:inj_onD[OF i])
+    hence " ?g b = a" using the1_equality[OF uex1, OF P] P by simp
+  } note g = this
+  have "inj_on ?g B"
+  proof(rule inj_onI)
+    fix x y assume "x:B" "y:B" "?g x = ?g y"
+    from s `x:B` obtain a1 where a1: "?P x a1" unfolding image_def by blast
+    from s `y:B` obtain a2 where a2: "?P y a2" unfolding image_def by blast
+    from g[OF a1] a1 g[OF a2] a2 `?g x = ?g y` show "x=y" by simp
+  qed
+  moreover have "?g ` B = A"
+  proof(auto simp:image_def)
+    fix b assume "b:B"
+    with s obtain a where P: "?P b a" unfolding image_def by blast
+    thus "?g b \<in> A" using g[OF P] by auto
+  next
+    fix a assume "a:A"
+    then obtain b where P: "?P b a" using s unfolding image_def by blast
+    then have "b:B" using s unfolding image_def by blast
+    with g[OF P] show "\<exists>b\<in>B. a = ?g b" by blast
+  qed
+  ultimately show ?thesis by(auto simp:bij_betw_def)
+qed
+
+
 subsection{*Facts About the Identity Function*}
 
 text{*We seem to need both the @{term id} forms and the @{term "\<lambda>x. x"}
diff -r 200b4e401e65 -r ae06618225ec src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Wed Feb 20 23:24:38 2008 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Thu Feb 21 17:33:58 2008 +0100
@@ -268,6 +268,11 @@
   apply (simp add: Inv_mem)
   done
 
+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
 
 subsection {*Other Consequences of Hilbert's Epsilon*}
 
diff -r 200b4e401e65 -r ae06618225ec src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Wed Feb 20 23:24:38 2008 +0100
+++ b/src/HOL/SetInterval.thy	Thu Feb 21 17:33:58 2008 +0100
@@ -469,6 +469,18 @@
 lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
   by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
 
+
+lemma ex_bij_betw_nat_finite:
+  "finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M"
+apply(drule finite_imp_nat_seg_image_inj_on)
+apply(auto simp:atLeast0LessThan[symmetric] lessThan_def[symmetric] card_image bij_betw_def)
+done
+
+lemma ex_bij_betw_finite_nat:
+  "finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}"
+by (blast dest: ex_bij_betw_nat_finite bij_betw_inv)
+
+
 subsection {* Intervals of integers *}
 
 lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}"
diff -r 200b4e401e65 -r ae06618225ec src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Wed Feb 20 23:24:38 2008 +0100
+++ b/src/HOL/Wellfounded_Recursion.thy	Thu Feb 21 17:33:58 2008 +0100
@@ -633,6 +633,22 @@
    "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
 by (erule (1) Least_Suc [THEN ssubst], simp)
 
+lemma ex_least_nat_le: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not>P i) & P(k)"
+apply(cases n) apply blast
+apply(rule_tac x="LEAST k. P(k)" in exI)
+apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
+done
+
+lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)"
+apply(cases n) apply blast
+apply(frule (1) ex_least_nat_le)
+apply(erule exE)
+apply(case_tac k) apply simp
+apply(rename_tac k1)
+apply(rule_tac x=k1 in exI)
+apply fastsimp
+done
+
 
 subsection {* size of a datatype value *}