merged

--- a/NEWS	Sun Oct 18 00:10:20 2009 +0200
+++ b/NEWS	Sun Oct 18 12:07:56 2009 +0200
@@ -149,6 +149,10 @@
 this.  Fix using O_assoc[symmetric].  The same applies to the curried
 version "R OO S".
 
+* Function "Inv" is renamed to "inv_onto" and function "inv" is now an
+abbreviation for "inv_onto UNIV". Lemmas are renamed accordingly.
+INCOMPATIBILITY.
+
 * ML antiquotation @{code_datatype} inserts definition of a datatype
 generated by the code generator; see Predicate.thy for an example.
 

--- a/src/HOL/Algebra/Bij.thy	Sun Oct 18 00:10:20 2009 +0200
+++ b/src/HOL/Algebra/Bij.thy	Sun Oct 18 12:07:56 2009 +0200
@@ -31,8 +31,8 @@
 
 subsection {*Bijections Form a Group *}
 
-lemma restrict_Inv_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (Inv S f) x) \<in> Bij S"
-  by (simp add: Bij_def bij_betw_Inv)
+lemma restrict_inv_onto_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (inv_onto S f) x) \<in> Bij S"
+  by (simp add: Bij_def bij_betw_inv_onto)
 
 lemma id_Bij: "(\<lambda>x\<in>S. x) \<in> Bij S "
   by (auto simp add: Bij_def bij_betw_def inj_on_def)
@@ -41,8 +41,8 @@
   by (auto simp add: Bij_def bij_betw_compose) 
 
 lemma Bij_compose_restrict_eq:
-     "f \<in> Bij S \<Longrightarrow> compose S (restrict (Inv S f) S) f = (\<lambda>x\<in>S. x)"
-  by (simp add: Bij_def compose_Inv_id)
+     "f \<in> Bij S \<Longrightarrow> compose S (restrict (inv_onto S f) S) f = (\<lambda>x\<in>S. x)"
+  by (simp add: Bij_def compose_inv_onto_id)
 
 theorem group_BijGroup: "group (BijGroup S)"
 apply (simp add: BijGroup_def)
@@ -52,22 +52,22 @@
   apply (simp add: compose_Bij)
   apply (blast intro: compose_assoc [symmetric] dest: Bij_imp_funcset)
  apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp)
-apply (blast intro: Bij_compose_restrict_eq restrict_Inv_Bij)
+apply (blast intro: Bij_compose_restrict_eq restrict_inv_onto_Bij)
 done
 
 
 subsection{*Automorphisms Form a Group*}
 
-lemma Bij_Inv_mem: "\<lbrakk> f \<in> Bij S;  x \<in> S\<rbrakk> \<Longrightarrow> Inv S f x \<in> S"
-by (simp add: Bij_def bij_betw_def Inv_mem)
+lemma Bij_inv_onto_mem: "\<lbrakk> f \<in> Bij S;  x \<in> S\<rbrakk> \<Longrightarrow> inv_onto S f x \<in> S"
+by (simp add: Bij_def bij_betw_def inv_onto_into)
 
-lemma Bij_Inv_lemma:
+lemma Bij_inv_onto_lemma:
  assumes eq: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> h(g x y) = g (h x) (h y)"
  shows "\<lbrakk>h \<in> Bij S;  g \<in> S \<rightarrow> S \<rightarrow> S;  x \<in> S;  y \<in> S\<rbrakk>
-        \<Longrightarrow> Inv S h (g x y) = g (Inv S h x) (Inv S h y)"
+        \<Longrightarrow> inv_onto S h (g x y) = g (inv_onto S h x) (inv_onto S h y)"
 apply (simp add: Bij_def bij_betw_def)
 apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' & y = h y'", clarify)
- apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast)
+ apply (simp add: eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem], blast)
 done
 
 
@@ -84,17 +84,17 @@
 lemma (in group) mult_funcset: "mult G \<in> carrier G \<rightarrow> carrier G \<rightarrow> carrier G"
   by (simp add:  Pi_I group.axioms)
 
-lemma (in group) restrict_Inv_hom:
+lemma (in group) restrict_inv_onto_hom:
       "\<lbrakk>h \<in> hom G G; h \<in> Bij (carrier G)\<rbrakk>
-       \<Longrightarrow> restrict (Inv (carrier G) h) (carrier G) \<in> hom G G"
-  by (simp add: hom_def Bij_Inv_mem restrictI mult_funcset
-                group.axioms Bij_Inv_lemma)
+       \<Longrightarrow> restrict (inv_onto (carrier G) h) (carrier G) \<in> hom G G"
+  by (simp add: hom_def Bij_inv_onto_mem restrictI mult_funcset
+                group.axioms Bij_inv_onto_lemma)
 
 lemma inv_BijGroup:
-     "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (Inv S f) x)"
+     "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (inv_onto S f) x)"
 apply (rule group.inv_equality)
 apply (rule group_BijGroup)
-apply (simp_all add: BijGroup_def restrict_Inv_Bij Bij_compose_restrict_eq)
+apply (simp_all add:BijGroup_def restrict_inv_onto_Bij Bij_compose_restrict_eq)
 done
 
 lemma (in group) subgroup_auto:
@@ -115,7 +115,7 @@
   assume "x \<in> auto G" 
   thus "inv\<^bsub>BijGroup (carrier G)\<^esub> x \<in> auto G"
     by (simp del: restrict_apply
-             add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom)
+        add: inv_BijGroup auto_def restrict_inv_onto_Bij restrict_inv_onto_hom)
 qed
 
 theorem (in group) AutoGroup: "group (AutoGroup G)"

--- a/src/HOL/Algebra/Group.thy	Sun Oct 18 00:10:20 2009 +0200
+++ b/src/HOL/Algebra/Group.thy	Sun Oct 18 12:07:56 2009 +0200
@@ -553,11 +553,11 @@
 by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
 
 lemma (in group) iso_sym:
-     "h \<in> G \<cong> H \<Longrightarrow> Inv (carrier G) h \<in> H \<cong> G"
-apply (simp add: iso_def bij_betw_Inv) 
-apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
- prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv]) 
-apply (simp add: hom_def bij_betw_def Inv_f_eq f_Inv_f Pi_def)
+     "h \<in> G \<cong> H \<Longrightarrow> inv_onto (carrier G) h \<in> H \<cong> G"
+apply (simp add: iso_def bij_betw_inv_onto) 
+apply (subgoal_tac "inv_onto (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
+ prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_onto]) 
+apply (simp add: hom_def bij_betw_def inv_onto_f_eq f_inv_onto_f Pi_def)
 done
 
 lemma (in group) iso_trans: 

--- a/src/HOL/Finite_Set.thy	Sun Oct 18 00:10:20 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Sun Oct 18 12:07:56 2009 +0200
@@ -155,6 +155,19 @@
   "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
 by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
 
+lemma finite_imp_inj_to_nat_seg:
+assumes "finite A"
+shows "EX f n::nat. f`A = {i. i<n} & inj_on f A"
+proof -
+  from finite_imp_nat_seg_image_inj_on[OF `finite A`]
+  obtain f and n::nat where bij: "bij_betw f {i. i<n} A"
+    by (auto simp:bij_betw_def)
+  let ?f = "the_inv_onto {i. i<n} f"
+  have "inj_on ?f A & ?f ` A = {i. i<n}"
+    by (fold bij_betw_def) (rule bij_betw_the_inv_onto[OF bij])
+  thus ?thesis by blast
+qed
+
 lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}"
 by(fastsimp simp: finite_conv_nat_seg_image)
 

--- a/src/HOL/Fun.thy	Sun Oct 18 00:10:20 2009 +0200
+++ b/src/HOL/Fun.thy	Sun Oct 18 12:07:56 2009 +0200
@@ -145,10 +145,12 @@
 lemma injD: "[| inj(f); f(x) = f(y) |] ==> x=y"
 by (simp add: inj_on_def)
 
-(*Useful with the simplifier*)
-lemma inj_eq: "inj(f) ==> (f(x) = f(y)) = (x=y)"
+lemma inj_on_eq_iff: "inj_on f A ==> x:A ==> y:A ==> (f(x) = f(y)) = (x=y)"
 by (force simp add: inj_on_def)
 
+lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)"
+by (simp add: inj_on_eq_iff)
+
 lemma inj_on_id[simp]: "inj_on id A"
   by (simp add: inj_on_def) 
 
@@ -511,7 +513,7 @@
   shows "inv f (f x) = x"
 proof -
   from assms have "(THE x'. f x' = f x) = (THE x'. x' = x)"
-    by (simp only: inj_eq)
+    by (simp add: inj_on_eq_iff)
   also have "... = x" by (rule the_eq_trivial)
   finally show ?thesis by (unfold inv_def)
 qed

--- a/src/HOL/Hilbert_Choice.thy	Sun Oct 18 00:10:20 2009 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Sun Oct 18 12:07:56 2009 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Hilbert_Choice.thy
-    Author:     Lawrence C Paulson
+    Author:     Lawrence C Paulson, Tobias Nipkow
     Copyright   2001  University of Cambridge
 *)
 
@@ -31,12 +31,11 @@
      in Syntax.const "_Eps" $ x $ t end)]
 *}
 
-constdefs
-  inv :: "('a => 'b) => ('b => 'a)"
-  "inv(f :: 'a => 'b) == %y. SOME x. f x = y"
+definition inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where
+"inv_onto A f == %x. SOME y. y : A & f y = x"
 
-  Inv :: "'a set => ('a => 'b) => ('b => 'a)"
-  "Inv A f == %x. SOME y. y \<in> A & f y = x"
+abbreviation inv :: "('a => 'b) => ('b => 'a)" where
+"inv == inv_onto UNIV"
 
 
 subsection {*Hilbert's Epsilon-operator*}
@@ -92,20 +91,38 @@
 
 subsection {*Function Inverse*}
 
-lemma inv_id [simp]: "inv id = id"
-by (simp add: inv_def id_def)
+lemma inv_onto_into: "x : f ` A ==> inv_onto A f x : A"
+apply (simp add: inv_onto_def)
+apply (fast intro: someI2)
+done
 
-text{*A one-to-one function has an inverse.*}
-lemma inv_f_f [simp]: "inj f ==> inv f (f x) = x"
-by (simp add: inv_def inj_eq)
+lemma inv_id [simp]: "inv id = id"
+by (simp add: inv_onto_def id_def)
 
-lemma inv_f_eq: "[| inj f;  f x = y |] ==> inv f y = x"
-apply (erule subst)
-apply (erule inv_f_f)
+lemma inv_onto_f_f [simp]:
+  "[| inj_on f A;  x : A |] ==> inv_onto A f (f x) = x"
+apply (simp add: inv_onto_def inj_on_def)
+apply (blast intro: someI2)
 done
 
-lemma inj_imp_inv_eq: "[| inj f; \<forall>x. f(g x) = x |] ==> inv f = g"
-by (blast intro: ext inv_f_eq)
+lemma inv_f_f: "inj f ==> inv f (f x) = x"
+by (simp add: inv_onto_f_f)
+
+lemma f_inv_onto_f: "y : f`A  ==> f (inv_onto A f y) = y"
+apply (simp add: inv_onto_def)
+apply (fast intro: someI2)
+done
+
+lemma inv_onto_f_eq: "[| inj_on f A; x : A; f x = y |] ==> inv_onto A f y = x"
+apply (erule subst)
+apply (fast intro: inv_onto_f_f)
+done
+
+lemma inv_f_eq: "[| inj f; f x = y |] ==> inv f y = x"
+by (simp add:inv_onto_f_eq)
+
+lemma inj_imp_inv_eq: "[| inj f; ALL x. f(g x) = x |] ==> inv f = g"
+by (blast intro: ext inv_onto_f_eq)
 
 text{*But is it useful?*}
 lemma inj_transfer:
@@ -114,13 +131,12 @@
 proof -
   have "f x \<in> range f" by auto
   hence "P(inv f (f x))" by (rule minor)
-  thus "P x" by (simp add: inv_f_f [OF injf])
+  thus "P x" by (simp add: inv_onto_f_f [OF injf])
 qed
 
-
 lemma inj_iff: "(inj f) = (inv f o f = id)"
 apply (simp add: o_def expand_fun_eq)
-apply (blast intro: inj_on_inverseI inv_f_f)
+apply (blast intro: inj_on_inverseI inv_onto_f_f)
 done
 
 lemma inv_o_cancel[simp]: "inj f ==> inv f o f = id"
@@ -129,36 +145,34 @@
 lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g"
 by (simp add: o_assoc[symmetric])
 
-lemma inv_image_cancel[simp]:
-  "inj f ==> inv f ` f ` S = S"
-by (simp add: image_compose[symmetric])
- 
+lemma inv_onto_image_cancel[simp]:
+  "inj_on f A ==> S <= A ==> inv_onto A f ` f ` S = S"
+by(fastsimp simp: image_def)
+
 lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
-by (blast intro: surjI inv_f_f)
-
-lemma f_inv_f: "y \<in> range(f) ==> f(inv f y) = y"
-apply (simp add: inv_def)
-apply (fast intro: someI)
-done
+by (blast intro: surjI inv_onto_f_f)
 
 lemma surj_f_inv_f: "surj f ==> f(inv f y) = y"
-by (simp add: f_inv_f surj_range)
+by (simp add: f_inv_onto_f surj_range)
 
-lemma inv_injective:
-  assumes eq: "inv f x = inv f y"
-      and x: "x: range f"
-      and y: "y: range f"
+lemma inv_onto_injective:
+  assumes eq: "inv_onto A f x = inv_onto A f y"
+      and x: "x: f`A"
+      and y: "y: f`A"
   shows "x=y"
 proof -
-  have "f (inv f x) = f (inv f y)" using eq by simp
-  thus ?thesis by (simp add: f_inv_f x y) 
+  have "f (inv_onto A f x) = f (inv_onto A f y)" using eq by simp
+  thus ?thesis by (simp add: f_inv_onto_f x y)
 qed
 
-lemma inj_on_inv: "A <= range(f) ==> inj_on (inv f) A"
-by (fast intro: inj_onI elim: inv_injective injD)
+lemma inj_on_inv_onto: "B <= f`A ==> inj_on (inv_onto A f) B"
+by (blast intro: inj_onI dest: inv_onto_injective injD)
+
+lemma bij_betw_inv_onto: "bij_betw f A B ==> bij_betw (inv_onto A f) B A"
+by (auto simp add: bij_betw_def inj_on_inv_onto)
 
 lemma surj_imp_inj_inv: "surj f ==> inj (inv f)"
-by (simp add: inj_on_inv surj_range)
+by (simp add: inj_on_inv_onto surj_range)
 
 lemma surj_iff: "(surj f) = (f o inv f = id)"
 apply (simp add: o_def expand_fun_eq)
@@ -176,7 +190,7 @@
 
 lemma inv_equality: "[| !!x. g (f x) = x;  !!y. f (g y) = y |] ==> inv f = g"
 apply (rule ext)
-apply (auto simp add: inv_def)
+apply (auto simp add: inv_onto_def)
 done
 
 lemma inv_inv_eq: "bij f ==> inv (inv f) = f"
@@ -191,12 +205,20 @@
     inv(inv f)=f all fail.
 **)
 
+lemma inv_onto_comp:
+  "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
+  inv_onto A (f o g) x = (inv_onto A g o inv_onto (g ` A) f) x"
+apply (rule inv_onto_f_eq)
+  apply (fast intro: comp_inj_on)
+ apply (simp add: inv_onto_into)
+apply (simp add: f_inv_onto_f inv_onto_into)
+done
+
 lemma o_inv_distrib: "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f"
 apply (rule inv_equality)
 apply (auto simp add: bij_def surj_f_inv_f)
 done
 
-
 lemma image_surj_f_inv_f: "surj f ==> f ` (inv f ` A) = A"
 by (simp add: image_eq_UN surj_f_inv_f)
 
@@ -214,7 +236,7 @@
 
 lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A" 
 apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
-apply (blast intro: bij_is_inj [THEN inv_f_f, symmetric])
+apply (blast intro: bij_is_inj [THEN inv_onto_f_f, symmetric])
 done
 
 lemma finite_fun_UNIVD1:
@@ -231,64 +253,12 @@
   moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
   proof (rule UNIV_eq_I)
     fix x :: 'a
-    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_def)
+    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_onto_def)
     thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast
   qed
   ultimately show "finite (UNIV :: 'a set)" by simp
 qed
 
-subsection {*Inverse of a PI-function (restricted domain)*}
-
-lemma Inv_f_f: "[| inj_on f A;  x \<in> A |] ==> Inv A f (f x) = x"
-apply (simp add: Inv_def inj_on_def)
-apply (blast intro: someI2)
-done
-
-lemma f_Inv_f: "y \<in> f`A  ==> f (Inv A f y) = y"
-apply (simp add: Inv_def)
-apply (fast intro: someI2)
-done
-
-lemma Inv_injective:
-  assumes eq: "Inv A f x = Inv A f y"
-      and x: "x: f`A"
-      and y: "y: f`A"
-  shows "x=y"
-proof -
-  have "f (Inv A f x) = f (Inv A f y)" using eq by simp
-  thus ?thesis by (simp add: f_Inv_f x y) 
-qed
-
-lemma inj_on_Inv: "B <= f`A ==> inj_on (Inv A f) B"
-apply (rule inj_onI)
-apply (blast intro: inj_onI dest: Inv_injective injD)
-done
-
-lemma Inv_mem: "[| f ` A = B;  x \<in> B |] ==> Inv A f x \<in> A"
-apply (simp add: Inv_def)
-apply (fast intro: someI2)
-done
-
-lemma Inv_f_eq: "[| inj_on f A; f x = y; x \<in> A |] ==> Inv A f y = x"
-  apply (erule subst)
-  apply (erule Inv_f_f, assumption)
-  done
-
-lemma Inv_comp:
-  "[| inj_on f (g ` A); inj_on g A; x \<in> f ` g ` A |] ==>
-  Inv A (f o g) x = (Inv A g o Inv (g ` A) f) x"
-  apply simp
-  apply (rule Inv_f_eq)
-    apply (fast intro: comp_inj_on)
-   apply (simp add: f_Inv_f Inv_mem)
-  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*}
 

--- a/src/HOL/Library/FuncSet.thy	Sun Oct 18 00:10:20 2009 +0200
+++ b/src/HOL/Library/FuncSet.thy	Sun Oct 18 12:07:56 2009 +0200
@@ -157,7 +157,7 @@
 the theorems belong here, or need at least @{term Hilbert_Choice}.*}
 
 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)
+by (auto simp add: bij_betw_def)
 
 lemma inj_on_compose:
   "[| bij_betw f A B; inj_on g B |] ==> inj_on (compose A g f) A"
@@ -190,22 +190,20 @@
       !!x. x\<in>A ==> f x = g x |] ==> f = g"
 by (force simp add: expand_fun_eq extensional_def)
 
-lemma Inv_funcset: "f ` A = B ==> (\<lambda>x\<in>B. Inv A f x) : B -> A"
-by (unfold Inv_def) (fast intro: someI2)
+lemma inv_onto_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_onto A f x) : B -> A"
+by (unfold inv_onto_def) (fast intro: someI2)
 
-lemma compose_Inv_id:
-  "bij_betw f A B ==> compose A (\<lambda>y\<in>B. Inv A f y) f = (\<lambda>x\<in>A. x)"
+lemma compose_inv_onto_id:
+  "bij_betw f A B ==> compose A (\<lambda>y\<in>B. inv_onto A f y) f = (\<lambda>x\<in>A. x)"
 apply (simp add: bij_betw_def compose_def)
 apply (rule restrict_ext, auto)
-apply (erule subst)
-apply (simp add: Inv_f_f)
 done
 
-lemma compose_id_Inv:
-  "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)"
+lemma compose_id_inv_onto:
+  "f ` A = B ==> compose B f (\<lambda>y\<in>B. inv_onto A f y) = (\<lambda>x\<in>B. x)"
 apply (simp add: compose_def)
 apply (rule restrict_ext)
-apply (simp add: f_Inv_f)
+apply (simp add: f_inv_onto_f)
 done
 
 

--- a/src/HOL/Library/Permutations.thy	Sun Oct 18 00:10:20 2009 +0200
+++ b/src/HOL/Library/Permutations.thy	Sun Oct 18 12:07:56 2009 +0200
@@ -5,11 +5,9 @@
 header {* Permutations, both general and specifically on finite sets.*}
 
 theory Permutations
-imports Finite_Cartesian_Product Parity Fact Main
+imports Finite_Cartesian_Product Parity Fact
 begin
 
-  (* Why should I import Main just to solve the Typerep problem! *)
-
 definition permutes (infixr "permutes" 41) where
   "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)"
 
@@ -85,7 +83,7 @@
   unfolding permutes_def by simp
 
 lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y"
-  unfolding permutes_def inv_def apply auto
+  unfolding permutes_def inv_onto_def apply auto
   apply (erule allE[where x=y])
   apply (erule allE[where x=y])
   apply (rule someI_ex) apply blast
@@ -95,10 +93,11 @@
   done
 
 lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S ==> Fun.swap a b id permutes S"
-  unfolding permutes_def swap_def fun_upd_def  apply auto apply metis done
+  unfolding permutes_def swap_def fun_upd_def  by auto metis
 
-lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
-apply (simp add: Ball_def permutes_def Diff_iff) by metis
+lemma permutes_superset:
+  "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
+by (simp add: Ball_def permutes_def Diff_iff) metis
 
 (* ------------------------------------------------------------------------- *)
 (* Group properties.                                                         *)

--- a/src/HOL/SizeChange/Correctness.thy	Sun Oct 18 00:10:20 2009 +0200
+++ b/src/HOL/SizeChange/Correctness.thy	Sun Oct 18 12:07:56 2009 +0200
@@ -1146,7 +1146,7 @@
   assumes "finite S" 
   shows "set (set2list S) = S"
   unfolding set2list_def 
-proof (rule f_inv_f)
+proof (rule f_inv_onto_f)
   from `finite S` have "\<exists>l. set l = S"
     by (rule finite_list)
   thus "S \<in> range set"

--- a/src/HOL/UNITY/Extend.thy	Sun Oct 18 00:10:20 2009 +0200
+++ b/src/HOL/UNITY/Extend.thy	Sun Oct 18 12:07:56 2009 +0200
@@ -121,12 +121,7 @@
      assumes surj_h: "surj h"
          and prem:   "!! x y. g (h(x,y)) = x"
      shows "fst (inv h z) = g z"
-apply (unfold inv_def)
-apply (rule_tac y1 = z in surj_h [THEN surjD, THEN exE])
-apply (rule someI2)
-apply (drule_tac [2] f = g in arg_cong)
-apply (auto simp add: prem)
-done
+by (metis UNIV_I f_inv_onto_f pair_collapse prem surj_h surj_range)
 
 
 subsection{*Trivial properties of f, g, h*}

--- a/src/HOL/ZF/HOLZF.thy	Sun Oct 18 00:10:20 2009 +0200
+++ b/src/HOL/ZF/HOLZF.thy	Sun Oct 18 12:07:56 2009 +0200
@@ -626,7 +626,7 @@
 
 lemma nat2Nat_Nat2nat[simp]: "Elem n Nat \<Longrightarrow> nat2Nat (Nat2nat n) = n"
   apply (simp add: Nat2nat_def)
-  apply (rule_tac f_inv_f)
+  apply (rule_tac f_inv_onto_f)
   apply (auto simp add: image_def Nat_def Sep)
   done
 

--- a/src/HOL/ZF/Zet.thy	Sun Oct 18 00:10:20 2009 +0200
+++ b/src/HOL/ZF/Zet.thy	Sun Oct 18 12:07:56 2009 +0200
@@ -33,27 +33,12 @@
   apply (auto simp add: explode_def Sep)
   done
 
-lemma image_Inv_f_f: "inj_on f B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (Inv B f) ` f ` A = A"
-  apply (rule set_ext)
-  apply (auto simp add: Inv_f_f image_def)
-  apply (rule_tac x="f x" in exI)
-  apply (auto simp add: Inv_f_f)
-  done
-  
 lemma image_zet_rep: "A \<in> zet \<Longrightarrow> ? z . g ` A = explode z"
   apply (auto simp add: zet_def')
-  apply (rule_tac x="Repl z (g o (Inv A f))" in exI)
+  apply (rule_tac x="Repl z (g o (inv_onto A f))" in exI)
   apply (simp add: explode_Repl_eq)
   apply (subgoal_tac "explode z = f ` A")
-  apply (simp_all add: comp_image_eq image_Inv_f_f)  
-  done
-
-lemma Inv_f_f_mem:       
-  assumes "x \<in> A"
-  shows "Inv A g (g x) \<in> A"
-  apply (simp add: Inv_def)
-  apply (rule someI2)
-  using `x \<in> A` apply auto
+  apply (simp_all add: comp_image_eq)
   done
 
 lemma zet_image_mem:
@@ -64,10 +49,10 @@
     by (auto simp add: zet_def')
   then obtain f where injf: "inj_on (f :: _ \<Rightarrow> ZF) A"  
     by auto
-  let ?w = "f o (Inv A g)"
-  have subset: "(Inv A g) ` (g ` A) \<subseteq> A"
-    by (auto simp add: Inv_f_f_mem)
-  have "inj_on (Inv A g) (g ` A)" by (simp add: inj_on_Inv)
+  let ?w = "f o (inv_onto A g)"
+  have subset: "(inv_onto A g) ` (g ` A) \<subseteq> A"
+    by (auto simp add: inv_onto_into)
+  have "inj_on (inv_onto A g) (g ` A)" by (simp add: inj_on_inv_onto)
   then have injw: "inj_on ?w (g ` A)"
     apply (rule comp_inj_on)
     apply (rule subset_inj_on[where B=A])
@@ -101,7 +86,7 @@
 lemma zexplode_zimplode: "zexplode (zimplode A) = A"
   apply (simp add: zimplode_def zexplode_def)
   apply (simp add: implode_def)
-  apply (subst f_inv_f[where y="Rep_zet A"])
+  apply (subst f_inv_onto_f[where y="Rep_zet A"])
   apply (auto simp add: Rep_zet_inverse Rep_zet_eq_explode image_def)
   done
 

--- a/src/HOL/ex/set.thy	Sun Oct 18 00:10:20 2009 +0200
+++ b/src/HOL/ex/set.thy	Sun Oct 18 12:07:56 2009 +0200
@@ -104,7 +104,7 @@
     --{*The term above can be synthesized by a sufficiently detailed proof.*}
   apply (rule bij_if_then_else)
      apply (rule_tac [4] refl)
-    apply (rule_tac [2] inj_on_inv)
+    apply (rule_tac [2] inj_on_inv_onto)
     apply (erule subset_inj_on [OF _ subset_UNIV])
    apply blast
   apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])