# HG changeset patch
# User hoelzl
# Date 1283445923 -7200
# Node ID bddc3d3f6e537222900e7a66fb44c57b9e517fc7
# Parent  928c5a5bdc93848464195efd6e0fe417da503f4b# Parent  39f8f6d1eb743692662836f42502e23e92eaadfa
merged

diff -r 928c5a5bdc93 -r bddc3d3f6e53 NEWS
--- a/NEWS	Thu Sep 02 17:02:00 2010 +0200
+++ b/NEWS	Thu Sep 02 18:45:23 2010 +0200
@@ -200,6 +200,9 @@
 derive instantiated and simplified equations for inductive predicates,
 similar to inductive_cases.
 
+* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". surj_on is a
+generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
+The theorems bij_def and surj_def are unchanged.
 
 *** FOL ***
 
diff -r 928c5a5bdc93 -r bddc3d3f6e53 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Sep 02 17:02:00 2010 +0200
+++ b/src/HOL/Fun.thy	Thu Sep 02 18:45:23 2010 +0200
@@ -117,31 +117,27 @@
 no_notation fcomp (infixl "\<circ>>" 60)
 
 
-subsection {* Injectivity and Surjectivity *}
+subsection {* Injectivity, Surjectivity and Bijectivity *}
+
+definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where -- "injective"
+  "inj_on f A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y)"
 
-definition
-  inj_on :: "['a => 'b, 'a set] => bool" where
-  -- "injective"
-  "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
+definition surj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> bool" where -- "surjective"
+  "surj_on f B \<longleftrightarrow> B \<subseteq> range f"
+
+definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where -- "bijective"
+  "bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
 
 text{*A common special case: functions injective over the entire domain type.*}
 
 abbreviation
-  "inj f == inj_on f UNIV"
-
-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"
+  "inj f \<equiv> inj_on f UNIV"
 
-definition
-  surj :: "('a => 'b) => bool" where
-  -- "surjective"
-  "surj f == ! y. ? x. y=f(x)"
+abbreviation
+  "surj f \<equiv> surj_on f UNIV"
 
-definition
-  bij :: "('a => 'b) => bool" where
-  -- "bijective"
-  "bij f == inj f & surj f"
+abbreviation
+  "bij f \<equiv> bij_betw f UNIV UNIV"
 
 lemma injI:
   assumes "\<And>x y. f x = f y \<Longrightarrow> x = y"
@@ -173,16 +169,16 @@
 by (simp add: inj_on_eq_iff)
 
 lemma inj_on_id[simp]: "inj_on id A"
-  by (simp add: inj_on_def) 
+  by (simp add: inj_on_def)
 
 lemma inj_on_id2[simp]: "inj_on (%x. x) A"
-by (simp add: inj_on_def) 
+by (simp add: inj_on_def)
 
-lemma surj_id[simp]: "surj id"
-by (simp add: surj_def) 
+lemma surj_id[simp]: "surj_on id A"
+by (simp add: surj_on_def)
 
-lemma bij_id[simp]: "bij id"
-by (simp add: bij_def)
+lemma bij_id[simp]: "bij_betw id A A"
+by (simp add: bij_betw_def)
 
 lemma inj_onI:
     "(!! x y. [|  x:A;  y:A;  f(x) = f(y) |] ==> x=y) ==> inj_on f A"
@@ -242,19 +238,26 @@
 apply (blast)
 done
 
-lemma surjI: "(!! x. g(f x) = x) ==> surj g"
-apply (simp add: surj_def)
-apply (blast intro: sym)
-done
+lemma surj_onI: "(\<And>x. x \<in> B \<Longrightarrow> g (f x) = x) \<Longrightarrow> surj_on g B"
+  by (simp add: surj_on_def) (blast intro: sym)
+
+lemma surj_onD: "surj_on f B \<Longrightarrow> y \<in> B \<Longrightarrow> \<exists>x. y = f x"
+  by (auto simp: surj_on_def)
+
+lemma surj_on_range_iff: "surj_on f B \<longleftrightarrow> (\<exists>A. f ` A = B)"
+  unfolding surj_on_def by (auto intro!: exI[of _ "f -` B"])
 
-lemma surj_range: "surj f ==> range f = UNIV"
-by (auto simp add: surj_def)
+lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
+  by (simp add: surj_on_def subset_eq image_iff)
+
+lemma surjI: "(\<And> x. g (f x) = x) \<Longrightarrow> surj g"
+  by (blast intro: surj_onI)
 
-lemma surjD: "surj f ==> EX x. y = f x"
-by (simp add: surj_def)
+lemma surjD: "surj f \<Longrightarrow> \<exists>x. y = f x"
+  by (simp add: surj_def)
 
-lemma surjE: "surj f ==> (!!x. y = f x ==> C) ==> C"
-by (simp add: surj_def, blast)
+lemma surjE: "surj f \<Longrightarrow> (\<And>x. y = f x \<Longrightarrow> C) \<Longrightarrow> C"
+  by (simp add: surj_def, blast)
 
 lemma comp_surj: "[| surj f;  surj g |] ==> surj (g o f)"
 apply (simp add: comp_def surj_def, clarify)
@@ -262,6 +265,18 @@
 apply (drule_tac x = x in spec, blast)
 done
 
+lemma surj_range: "surj f \<Longrightarrow> range f = UNIV"
+  by (auto simp add: surj_on_def)
+
+lemma surj_range_iff: "surj f \<longleftrightarrow> range f = UNIV"
+  unfolding surj_on_def by auto
+
+lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
+  unfolding bij_betw_def surj_range_iff by auto
+
+lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
+  unfolding surj_range_iff bij_betw_def ..
+
 lemma bijI: "[| inj f; surj f |] ==> bij f"
 by (simp add: bij_def)
 
@@ -274,6 +289,9 @@
 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_surj_on: "bij_betw f A B \<Longrightarrow> surj_on f B"
+by (auto simp: bij_betw_def surj_on_range_iff)
+
 lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
 by(fastsimp intro: comp_inj_on comp_surj simp: bij_def surj_range)
 
@@ -312,6 +330,11 @@
   ultimately show ?thesis by(auto simp:bij_betw_def)
 qed
 
+lemma bij_betw_combine:
+  assumes "bij_betw f A B" "bij_betw f C D" "B \<inter> D = {}"
+  shows "bij_betw f (A \<union> C) (B \<union> D)"
+  using assms unfolding bij_betw_def inj_on_Un image_Un by auto
+
 lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
 by (simp add: surj_range)
 
@@ -497,44 +520,46 @@
 lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)"
 by (rule ext, simp add: fun_upd_def swap_def)
 
+lemma swap_image_eq [simp]:
+  assumes "a \<in> A" "b \<in> A" shows "swap a b f ` A = f ` A"
+proof -
+  have subset: "\<And>f. swap a b f ` A \<subseteq> f ` A"
+    using assms by (auto simp: image_iff swap_def)
+  then have "swap a b (swap a b f) ` A \<subseteq> (swap a b f) ` A" .
+  with subset[of f] show ?thesis by auto
+qed
+
 lemma inj_on_imp_inj_on_swap:
-  "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
-by (simp add: inj_on_def swap_def, blast)
+  "\<lbrakk>inj_on f A; a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> inj_on (swap a b f) A"
+  by (simp add: inj_on_def swap_def, blast)
 
 lemma inj_on_swap_iff [simp]:
-  assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A = inj_on f A"
-proof 
+  assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A \<longleftrightarrow> inj_on f A"
+proof
   assume "inj_on (swap a b f) A"
-  with A have "inj_on (swap a b (swap a b f)) A" 
-    by (iprover intro: inj_on_imp_inj_on_swap) 
-  thus "inj_on f A" by simp 
+  with A have "inj_on (swap a b (swap a b f)) A"
+    by (iprover intro: inj_on_imp_inj_on_swap)
+  thus "inj_on f A" by simp
 next
   assume "inj_on f A"
   with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
 qed
 
-lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
-apply (simp add: surj_def swap_def, clarify)
-apply (case_tac "y = f b", blast)
-apply (case_tac "y = f a", auto)
-done
+lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (swap a b f)"
+  unfolding surj_range_iff by simp
+
+lemma surj_swap_iff [simp]: "surj (swap a b f) \<longleftrightarrow> surj f"
+  unfolding surj_range_iff by simp
 
-lemma surj_swap_iff [simp]: "surj (swap a b f) = surj f"
-proof 
-  assume "surj (swap a b f)"
-  hence "surj (swap a b (swap a b f))" by (rule surj_imp_surj_swap) 
-  thus "surj f" by simp 
-next
-  assume "surj f"
-  thus "surj (swap a b f)" by (rule surj_imp_surj_swap) 
-qed
+lemma bij_betw_swap_iff [simp]:
+  "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> bij_betw (swap x y f) A B \<longleftrightarrow> bij_betw f A B"
+  by (auto simp: bij_betw_def)
 
-lemma bij_swap_iff: "bij (swap a b f) = bij f"
-by (simp add: bij_def)
+lemma bij_swap_iff [simp]: "bij (swap a b f) \<longleftrightarrow> bij f"
+  by simp
 
 hide_const (open) swap
 
-
 subsection {* Inversion of injective functions *}
 
 definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
diff -r 928c5a5bdc93 -r bddc3d3f6e53 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Thu Sep 02 17:02:00 2010 +0200
+++ b/src/HOL/Library/Permutation.thy	Thu Sep 02 18:45:23 2010 +0200
@@ -183,4 +183,55 @@
 lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
   by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
 
+lemma permutation_Ex_bij:
+  assumes "xs <~~> ys"
+  shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
+using assms proof induct
+  case Nil then show ?case unfolding bij_betw_def by simp
+next
+  case (swap y x l)
+  show ?case
+  proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI)
+    show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
+      by (auto simp: bij_betw_def bij_betw_swap_iff)
+    fix i assume "i < length(y#x#l)"
+    show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
+      by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
+  qed
+next
+  case (Cons xs ys z)
+  then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" and
+    perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" by blast
+  let "?f i" = "case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0"
+  show ?case
+  proof (intro exI[of _ ?f] allI conjI impI)
+    have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}"
+            "{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}"
+      by (simp_all add: lessThan_Suc_eq_insert_0)
+    show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}" unfolding *
+    proof (rule bij_betw_combine)
+      show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})"
+        using bij unfolding bij_betw_def
+        by (auto intro!: inj_onI imageI dest: inj_onD simp: image_compose[symmetric] comp_def)
+    qed (auto simp: bij_betw_def)
+    fix i assume "i < length (z#xs)"
+    then show "(z # xs) ! i = (z # ys) ! (?f i)"
+      using perm by (cases i) auto
+  qed
+next
+  case (trans xs ys zs)
+  then obtain f g where
+    bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}" and
+    perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)" by blast
+  show ?case
+  proof (intro exI[of _ "g\<circ>f"] conjI allI impI)
+    show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}"
+      using bij by (rule bij_betw_trans)
+    fix i assume "i < length xs"
+    with bij have "f i < length ys" unfolding bij_betw_def by force
+    with `i < length xs` show "xs ! i = zs ! (g \<circ> f) i"
+      using trans(1,3)[THEN perm_length] perm by force
+  qed
+qed
+
 end
diff -r 928c5a5bdc93 -r bddc3d3f6e53 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Sep 02 17:02:00 2010 +0200
+++ b/src/HOL/List.thy	Thu Sep 02 18:45:23 2010 +0200
@@ -3076,6 +3076,10 @@
   "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
 by(induct xs) auto
 
+lemma filter_remove1:
+  "filter Q (remove1 x xs) = remove1 x (filter Q xs)"
+by (induct xs) auto
+
 lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
 apply(insert set_remove1_subset)
 apply fast
diff -r 928c5a5bdc93 -r bddc3d3f6e53 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Thu Sep 02 17:02:00 2010 +0200
+++ b/src/HOL/SetInterval.thy	Thu Sep 02 18:45:23 2010 +0200
@@ -304,6 +304,17 @@
 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
 by (simp add: lessThan_def less_Suc_eq, blast)
 
+text {* The following proof is convinient in induction proofs where
+new elements get indices at the beginning. So it is used to transform
+@{term "{..<Suc n}"} to @{term "0::nat"} and @{term "{..< n}"}. *}
+
+lemma lessThan_Suc_eq_insert_0: "{..<Suc n} = insert 0 (Suc ` {..<n})"
+proof safe
+  fix x assume "x < Suc n" "x \<notin> Suc ` {..<n}"
+  then have "x \<noteq> Suc (x - 1)" by auto
+  with `x < Suc n` show "x = 0" by auto
+qed
+
 lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
 by (simp add: lessThan_def atMost_def less_Suc_eq_le)