merged
authornipkow
Sun Oct 18 12:07:56 2009 +0200 (2009-10-18)
changeset 32989c28279b29ff1
parent 32987 eac0ff83005e
parent 32988 d1d4d7a08a66
child 32991 b6ba8adc14c2
child 32992 2318ff5fca1a
merged
NEWS
src/HOL/Algebra/Group.thy
src/HOL/Finite_Set.thy
src/HOL/Library/Permutations.thy
src/HOL/SizeChange/Correctness.thy
src/HOL/UNITY/Extend.thy
src/HOL/ZF/HOLZF.thy
     1.1 --- a/NEWS	Sun Oct 18 00:10:20 2009 +0200
     1.2 +++ b/NEWS	Sun Oct 18 12:07:56 2009 +0200
     1.3 @@ -149,6 +149,10 @@
     1.4  this.  Fix using O_assoc[symmetric].  The same applies to the curried
     1.5  version "R OO S".
     1.6  
     1.7 +* Function "Inv" is renamed to "inv_onto" and function "inv" is now an
     1.8 +abbreviation for "inv_onto UNIV". Lemmas are renamed accordingly.
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  * ML antiquotation @{code_datatype} inserts definition of a datatype
    1.12  generated by the code generator; see Predicate.thy for an example.
    1.13  
     2.1 --- a/src/HOL/Algebra/Bij.thy	Sun Oct 18 00:10:20 2009 +0200
     2.2 +++ b/src/HOL/Algebra/Bij.thy	Sun Oct 18 12:07:56 2009 +0200
     2.3 @@ -31,8 +31,8 @@
     2.4  
     2.5  subsection {*Bijections Form a Group *}
     2.6  
     2.7 -lemma restrict_Inv_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (Inv S f) x) \<in> Bij S"
     2.8 -  by (simp add: Bij_def bij_betw_Inv)
     2.9 +lemma restrict_inv_onto_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (inv_onto S f) x) \<in> Bij S"
    2.10 +  by (simp add: Bij_def bij_betw_inv_onto)
    2.11  
    2.12  lemma id_Bij: "(\<lambda>x\<in>S. x) \<in> Bij S "
    2.13    by (auto simp add: Bij_def bij_betw_def inj_on_def)
    2.14 @@ -41,8 +41,8 @@
    2.15    by (auto simp add: Bij_def bij_betw_compose) 
    2.16  
    2.17  lemma Bij_compose_restrict_eq:
    2.18 -     "f \<in> Bij S \<Longrightarrow> compose S (restrict (Inv S f) S) f = (\<lambda>x\<in>S. x)"
    2.19 -  by (simp add: Bij_def compose_Inv_id)
    2.20 +     "f \<in> Bij S \<Longrightarrow> compose S (restrict (inv_onto S f) S) f = (\<lambda>x\<in>S. x)"
    2.21 +  by (simp add: Bij_def compose_inv_onto_id)
    2.22  
    2.23  theorem group_BijGroup: "group (BijGroup S)"
    2.24  apply (simp add: BijGroup_def)
    2.25 @@ -52,22 +52,22 @@
    2.26    apply (simp add: compose_Bij)
    2.27    apply (blast intro: compose_assoc [symmetric] dest: Bij_imp_funcset)
    2.28   apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp)
    2.29 -apply (blast intro: Bij_compose_restrict_eq restrict_Inv_Bij)
    2.30 +apply (blast intro: Bij_compose_restrict_eq restrict_inv_onto_Bij)
    2.31  done
    2.32  
    2.33  
    2.34  subsection{*Automorphisms Form a Group*}
    2.35  
    2.36 -lemma Bij_Inv_mem: "\<lbrakk> f \<in> Bij S;  x \<in> S\<rbrakk> \<Longrightarrow> Inv S f x \<in> S"
    2.37 -by (simp add: Bij_def bij_betw_def Inv_mem)
    2.38 +lemma Bij_inv_onto_mem: "\<lbrakk> f \<in> Bij S;  x \<in> S\<rbrakk> \<Longrightarrow> inv_onto S f x \<in> S"
    2.39 +by (simp add: Bij_def bij_betw_def inv_onto_into)
    2.40  
    2.41 -lemma Bij_Inv_lemma:
    2.42 +lemma Bij_inv_onto_lemma:
    2.43   assumes eq: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> h(g x y) = g (h x) (h y)"
    2.44   shows "\<lbrakk>h \<in> Bij S;  g \<in> S \<rightarrow> S \<rightarrow> S;  x \<in> S;  y \<in> S\<rbrakk>
    2.45 -        \<Longrightarrow> Inv S h (g x y) = g (Inv S h x) (Inv S h y)"
    2.46 +        \<Longrightarrow> inv_onto S h (g x y) = g (inv_onto S h x) (inv_onto S h y)"
    2.47  apply (simp add: Bij_def bij_betw_def)
    2.48  apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' & y = h y'", clarify)
    2.49 - apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast)
    2.50 + apply (simp add: eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem], blast)
    2.51  done
    2.52  
    2.53  
    2.54 @@ -84,17 +84,17 @@
    2.55  lemma (in group) mult_funcset: "mult G \<in> carrier G \<rightarrow> carrier G \<rightarrow> carrier G"
    2.56    by (simp add:  Pi_I group.axioms)
    2.57  
    2.58 -lemma (in group) restrict_Inv_hom:
    2.59 +lemma (in group) restrict_inv_onto_hom:
    2.60        "\<lbrakk>h \<in> hom G G; h \<in> Bij (carrier G)\<rbrakk>
    2.61 -       \<Longrightarrow> restrict (Inv (carrier G) h) (carrier G) \<in> hom G G"
    2.62 -  by (simp add: hom_def Bij_Inv_mem restrictI mult_funcset
    2.63 -                group.axioms Bij_Inv_lemma)
    2.64 +       \<Longrightarrow> restrict (inv_onto (carrier G) h) (carrier G) \<in> hom G G"
    2.65 +  by (simp add: hom_def Bij_inv_onto_mem restrictI mult_funcset
    2.66 +                group.axioms Bij_inv_onto_lemma)
    2.67  
    2.68  lemma inv_BijGroup:
    2.69 -     "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (Inv S f) x)"
    2.70 +     "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (inv_onto S f) x)"
    2.71  apply (rule group.inv_equality)
    2.72  apply (rule group_BijGroup)
    2.73 -apply (simp_all add: BijGroup_def restrict_Inv_Bij Bij_compose_restrict_eq)
    2.74 +apply (simp_all add:BijGroup_def restrict_inv_onto_Bij Bij_compose_restrict_eq)
    2.75  done
    2.76  
    2.77  lemma (in group) subgroup_auto:
    2.78 @@ -115,7 +115,7 @@
    2.79    assume "x \<in> auto G" 
    2.80    thus "inv\<^bsub>BijGroup (carrier G)\<^esub> x \<in> auto G"
    2.81      by (simp del: restrict_apply
    2.82 -             add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom)
    2.83 +        add: inv_BijGroup auto_def restrict_inv_onto_Bij restrict_inv_onto_hom)
    2.84  qed
    2.85  
    2.86  theorem (in group) AutoGroup: "group (AutoGroup G)"
     3.1 --- a/src/HOL/Algebra/Group.thy	Sun Oct 18 00:10:20 2009 +0200
     3.2 +++ b/src/HOL/Algebra/Group.thy	Sun Oct 18 12:07:56 2009 +0200
     3.3 @@ -553,11 +553,11 @@
     3.4  by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
     3.5  
     3.6  lemma (in group) iso_sym:
     3.7 -     "h \<in> G \<cong> H \<Longrightarrow> Inv (carrier G) h \<in> H \<cong> G"
     3.8 -apply (simp add: iso_def bij_betw_Inv) 
     3.9 -apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
    3.10 - prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv]) 
    3.11 -apply (simp add: hom_def bij_betw_def Inv_f_eq f_Inv_f Pi_def)
    3.12 +     "h \<in> G \<cong> H \<Longrightarrow> inv_onto (carrier G) h \<in> H \<cong> G"
    3.13 +apply (simp add: iso_def bij_betw_inv_onto) 
    3.14 +apply (subgoal_tac "inv_onto (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
    3.15 + prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_onto]) 
    3.16 +apply (simp add: hom_def bij_betw_def inv_onto_f_eq f_inv_onto_f Pi_def)
    3.17  done
    3.18  
    3.19  lemma (in group) iso_trans: 
     4.1 --- a/src/HOL/Finite_Set.thy	Sun Oct 18 00:10:20 2009 +0200
     4.2 +++ b/src/HOL/Finite_Set.thy	Sun Oct 18 12:07:56 2009 +0200
     4.3 @@ -155,6 +155,19 @@
     4.4    "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
     4.5  by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
     4.6  
     4.7 +lemma finite_imp_inj_to_nat_seg:
     4.8 +assumes "finite A"
     4.9 +shows "EX f n::nat. f`A = {i. i<n} & inj_on f A"
    4.10 +proof -
    4.11 +  from finite_imp_nat_seg_image_inj_on[OF `finite A`]
    4.12 +  obtain f and n::nat where bij: "bij_betw f {i. i<n} A"
    4.13 +    by (auto simp:bij_betw_def)
    4.14 +  let ?f = "the_inv_onto {i. i<n} f"
    4.15 +  have "inj_on ?f A & ?f ` A = {i. i<n}"
    4.16 +    by (fold bij_betw_def) (rule bij_betw_the_inv_onto[OF bij])
    4.17 +  thus ?thesis by blast
    4.18 +qed
    4.19 +
    4.20  lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}"
    4.21  by(fastsimp simp: finite_conv_nat_seg_image)
    4.22  
     5.1 --- a/src/HOL/Fun.thy	Sun Oct 18 00:10:20 2009 +0200
     5.2 +++ b/src/HOL/Fun.thy	Sun Oct 18 12:07:56 2009 +0200
     5.3 @@ -145,10 +145,12 @@
     5.4  lemma injD: "[| inj(f); f(x) = f(y) |] ==> x=y"
     5.5  by (simp add: inj_on_def)
     5.6  
     5.7 -(*Useful with the simplifier*)
     5.8 -lemma inj_eq: "inj(f) ==> (f(x) = f(y)) = (x=y)"
     5.9 +lemma inj_on_eq_iff: "inj_on f A ==> x:A ==> y:A ==> (f(x) = f(y)) = (x=y)"
    5.10  by (force simp add: inj_on_def)
    5.11  
    5.12 +lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)"
    5.13 +by (simp add: inj_on_eq_iff)
    5.14 +
    5.15  lemma inj_on_id[simp]: "inj_on id A"
    5.16    by (simp add: inj_on_def) 
    5.17  
    5.18 @@ -511,7 +513,7 @@
    5.19    shows "inv f (f x) = x"
    5.20  proof -
    5.21    from assms have "(THE x'. f x' = f x) = (THE x'. x' = x)"
    5.22 -    by (simp only: inj_eq)
    5.23 +    by (simp add: inj_on_eq_iff)
    5.24    also have "... = x" by (rule the_eq_trivial)
    5.25    finally show ?thesis by (unfold inv_def)
    5.26  qed
     6.1 --- a/src/HOL/Hilbert_Choice.thy	Sun Oct 18 00:10:20 2009 +0200
     6.2 +++ b/src/HOL/Hilbert_Choice.thy	Sun Oct 18 12:07:56 2009 +0200
     6.3 @@ -1,5 +1,5 @@
     6.4  (*  Title:      HOL/Hilbert_Choice.thy
     6.5 -    Author:     Lawrence C Paulson
     6.6 +    Author:     Lawrence C Paulson, Tobias Nipkow
     6.7      Copyright   2001  University of Cambridge
     6.8  *)
     6.9  
    6.10 @@ -31,12 +31,11 @@
    6.11       in Syntax.const "_Eps" $ x $ t end)]
    6.12  *}
    6.13  
    6.14 -constdefs
    6.15 -  inv :: "('a => 'b) => ('b => 'a)"
    6.16 -  "inv(f :: 'a => 'b) == %y. SOME x. f x = y"
    6.17 +definition inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where
    6.18 +"inv_onto A f == %x. SOME y. y : A & f y = x"
    6.19  
    6.20 -  Inv :: "'a set => ('a => 'b) => ('b => 'a)"
    6.21 -  "Inv A f == %x. SOME y. y \<in> A & f y = x"
    6.22 +abbreviation inv :: "('a => 'b) => ('b => 'a)" where
    6.23 +"inv == inv_onto UNIV"
    6.24  
    6.25  
    6.26  subsection {*Hilbert's Epsilon-operator*}
    6.27 @@ -92,20 +91,38 @@
    6.28  
    6.29  subsection {*Function Inverse*}
    6.30  
    6.31 -lemma inv_id [simp]: "inv id = id"
    6.32 -by (simp add: inv_def id_def)
    6.33 +lemma inv_onto_into: "x : f ` A ==> inv_onto A f x : A"
    6.34 +apply (simp add: inv_onto_def)
    6.35 +apply (fast intro: someI2)
    6.36 +done
    6.37  
    6.38 -text{*A one-to-one function has an inverse.*}
    6.39 -lemma inv_f_f [simp]: "inj f ==> inv f (f x) = x"
    6.40 -by (simp add: inv_def inj_eq)
    6.41 +lemma inv_id [simp]: "inv id = id"
    6.42 +by (simp add: inv_onto_def id_def)
    6.43  
    6.44 -lemma inv_f_eq: "[| inj f;  f x = y |] ==> inv f y = x"
    6.45 -apply (erule subst)
    6.46 -apply (erule inv_f_f)
    6.47 +lemma inv_onto_f_f [simp]:
    6.48 +  "[| inj_on f A;  x : A |] ==> inv_onto A f (f x) = x"
    6.49 +apply (simp add: inv_onto_def inj_on_def)
    6.50 +apply (blast intro: someI2)
    6.51  done
    6.52  
    6.53 -lemma inj_imp_inv_eq: "[| inj f; \<forall>x. f(g x) = x |] ==> inv f = g"
    6.54 -by (blast intro: ext inv_f_eq)
    6.55 +lemma inv_f_f: "inj f ==> inv f (f x) = x"
    6.56 +by (simp add: inv_onto_f_f)
    6.57 +
    6.58 +lemma f_inv_onto_f: "y : f`A  ==> f (inv_onto A f y) = y"
    6.59 +apply (simp add: inv_onto_def)
    6.60 +apply (fast intro: someI2)
    6.61 +done
    6.62 +
    6.63 +lemma inv_onto_f_eq: "[| inj_on f A; x : A; f x = y |] ==> inv_onto A f y = x"
    6.64 +apply (erule subst)
    6.65 +apply (fast intro: inv_onto_f_f)
    6.66 +done
    6.67 +
    6.68 +lemma inv_f_eq: "[| inj f; f x = y |] ==> inv f y = x"
    6.69 +by (simp add:inv_onto_f_eq)
    6.70 +
    6.71 +lemma inj_imp_inv_eq: "[| inj f; ALL x. f(g x) = x |] ==> inv f = g"
    6.72 +by (blast intro: ext inv_onto_f_eq)
    6.73  
    6.74  text{*But is it useful?*}
    6.75  lemma inj_transfer:
    6.76 @@ -114,13 +131,12 @@
    6.77  proof -
    6.78    have "f x \<in> range f" by auto
    6.79    hence "P(inv f (f x))" by (rule minor)
    6.80 -  thus "P x" by (simp add: inv_f_f [OF injf])
    6.81 +  thus "P x" by (simp add: inv_onto_f_f [OF injf])
    6.82  qed
    6.83  
    6.84 -
    6.85  lemma inj_iff: "(inj f) = (inv f o f = id)"
    6.86  apply (simp add: o_def expand_fun_eq)
    6.87 -apply (blast intro: inj_on_inverseI inv_f_f)
    6.88 +apply (blast intro: inj_on_inverseI inv_onto_f_f)
    6.89  done
    6.90  
    6.91  lemma inv_o_cancel[simp]: "inj f ==> inv f o f = id"
    6.92 @@ -129,36 +145,34 @@
    6.93  lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g"
    6.94  by (simp add: o_assoc[symmetric])
    6.95  
    6.96 -lemma inv_image_cancel[simp]:
    6.97 -  "inj f ==> inv f ` f ` S = S"
    6.98 -by (simp add: image_compose[symmetric])
    6.99 - 
   6.100 +lemma inv_onto_image_cancel[simp]:
   6.101 +  "inj_on f A ==> S <= A ==> inv_onto A f ` f ` S = S"
   6.102 +by(fastsimp simp: image_def)
   6.103 +
   6.104  lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
   6.105 -by (blast intro: surjI inv_f_f)
   6.106 -
   6.107 -lemma f_inv_f: "y \<in> range(f) ==> f(inv f y) = y"
   6.108 -apply (simp add: inv_def)
   6.109 -apply (fast intro: someI)
   6.110 -done
   6.111 +by (blast intro: surjI inv_onto_f_f)
   6.112  
   6.113  lemma surj_f_inv_f: "surj f ==> f(inv f y) = y"
   6.114 -by (simp add: f_inv_f surj_range)
   6.115 +by (simp add: f_inv_onto_f surj_range)
   6.116  
   6.117 -lemma inv_injective:
   6.118 -  assumes eq: "inv f x = inv f y"
   6.119 -      and x: "x: range f"
   6.120 -      and y: "y: range f"
   6.121 +lemma inv_onto_injective:
   6.122 +  assumes eq: "inv_onto A f x = inv_onto A f y"
   6.123 +      and x: "x: f`A"
   6.124 +      and y: "y: f`A"
   6.125    shows "x=y"
   6.126  proof -
   6.127 -  have "f (inv f x) = f (inv f y)" using eq by simp
   6.128 -  thus ?thesis by (simp add: f_inv_f x y) 
   6.129 +  have "f (inv_onto A f x) = f (inv_onto A f y)" using eq by simp
   6.130 +  thus ?thesis by (simp add: f_inv_onto_f x y)
   6.131  qed
   6.132  
   6.133 -lemma inj_on_inv: "A <= range(f) ==> inj_on (inv f) A"
   6.134 -by (fast intro: inj_onI elim: inv_injective injD)
   6.135 +lemma inj_on_inv_onto: "B <= f`A ==> inj_on (inv_onto A f) B"
   6.136 +by (blast intro: inj_onI dest: inv_onto_injective injD)
   6.137 +
   6.138 +lemma bij_betw_inv_onto: "bij_betw f A B ==> bij_betw (inv_onto A f) B A"
   6.139 +by (auto simp add: bij_betw_def inj_on_inv_onto)
   6.140  
   6.141  lemma surj_imp_inj_inv: "surj f ==> inj (inv f)"
   6.142 -by (simp add: inj_on_inv surj_range)
   6.143 +by (simp add: inj_on_inv_onto surj_range)
   6.144  
   6.145  lemma surj_iff: "(surj f) = (f o inv f = id)"
   6.146  apply (simp add: o_def expand_fun_eq)
   6.147 @@ -176,7 +190,7 @@
   6.148  
   6.149  lemma inv_equality: "[| !!x. g (f x) = x;  !!y. f (g y) = y |] ==> inv f = g"
   6.150  apply (rule ext)
   6.151 -apply (auto simp add: inv_def)
   6.152 +apply (auto simp add: inv_onto_def)
   6.153  done
   6.154  
   6.155  lemma inv_inv_eq: "bij f ==> inv (inv f) = f"
   6.156 @@ -191,12 +205,20 @@
   6.157      inv(inv f)=f all fail.
   6.158  **)
   6.159  
   6.160 +lemma inv_onto_comp:
   6.161 +  "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
   6.162 +  inv_onto A (f o g) x = (inv_onto A g o inv_onto (g ` A) f) x"
   6.163 +apply (rule inv_onto_f_eq)
   6.164 +  apply (fast intro: comp_inj_on)
   6.165 + apply (simp add: inv_onto_into)
   6.166 +apply (simp add: f_inv_onto_f inv_onto_into)
   6.167 +done
   6.168 +
   6.169  lemma o_inv_distrib: "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f"
   6.170  apply (rule inv_equality)
   6.171  apply (auto simp add: bij_def surj_f_inv_f)
   6.172  done
   6.173  
   6.174 -
   6.175  lemma image_surj_f_inv_f: "surj f ==> f ` (inv f ` A) = A"
   6.176  by (simp add: image_eq_UN surj_f_inv_f)
   6.177  
   6.178 @@ -214,7 +236,7 @@
   6.179  
   6.180  lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A" 
   6.181  apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
   6.182 -apply (blast intro: bij_is_inj [THEN inv_f_f, symmetric])
   6.183 +apply (blast intro: bij_is_inj [THEN inv_onto_f_f, symmetric])
   6.184  done
   6.185  
   6.186  lemma finite_fun_UNIVD1:
   6.187 @@ -231,64 +253,12 @@
   6.188    moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
   6.189    proof (rule UNIV_eq_I)
   6.190      fix x :: 'a
   6.191 -    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_def)
   6.192 +    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_onto_def)
   6.193      thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast
   6.194    qed
   6.195    ultimately show "finite (UNIV :: 'a set)" by simp
   6.196  qed
   6.197  
   6.198 -subsection {*Inverse of a PI-function (restricted domain)*}
   6.199 -
   6.200 -lemma Inv_f_f: "[| inj_on f A;  x \<in> A |] ==> Inv A f (f x) = x"
   6.201 -apply (simp add: Inv_def inj_on_def)
   6.202 -apply (blast intro: someI2)
   6.203 -done
   6.204 -
   6.205 -lemma f_Inv_f: "y \<in> f`A  ==> f (Inv A f y) = y"
   6.206 -apply (simp add: Inv_def)
   6.207 -apply (fast intro: someI2)
   6.208 -done
   6.209 -
   6.210 -lemma Inv_injective:
   6.211 -  assumes eq: "Inv A f x = Inv A f y"
   6.212 -      and x: "x: f`A"
   6.213 -      and y: "y: f`A"
   6.214 -  shows "x=y"
   6.215 -proof -
   6.216 -  have "f (Inv A f x) = f (Inv A f y)" using eq by simp
   6.217 -  thus ?thesis by (simp add: f_Inv_f x y) 
   6.218 -qed
   6.219 -
   6.220 -lemma inj_on_Inv: "B <= f`A ==> inj_on (Inv A f) B"
   6.221 -apply (rule inj_onI)
   6.222 -apply (blast intro: inj_onI dest: Inv_injective injD)
   6.223 -done
   6.224 -
   6.225 -lemma Inv_mem: "[| f ` A = B;  x \<in> B |] ==> Inv A f x \<in> A"
   6.226 -apply (simp add: Inv_def)
   6.227 -apply (fast intro: someI2)
   6.228 -done
   6.229 -
   6.230 -lemma Inv_f_eq: "[| inj_on f A; f x = y; x \<in> A |] ==> Inv A f y = x"
   6.231 -  apply (erule subst)
   6.232 -  apply (erule Inv_f_f, assumption)
   6.233 -  done
   6.234 -
   6.235 -lemma Inv_comp:
   6.236 -  "[| inj_on f (g ` A); inj_on g A; x \<in> f ` g ` A |] ==>
   6.237 -  Inv A (f o g) x = (Inv A g o Inv (g ` A) f) x"
   6.238 -  apply simp
   6.239 -  apply (rule Inv_f_eq)
   6.240 -    apply (fast intro: comp_inj_on)
   6.241 -   apply (simp add: f_Inv_f Inv_mem)
   6.242 -  apply (simp add: Inv_mem)
   6.243 -  done
   6.244 -
   6.245 -lemma bij_betw_Inv: "bij_betw f A B \<Longrightarrow> bij_betw (Inv A f) B A"
   6.246 -  apply (auto simp add: bij_betw_def inj_on_Inv Inv_mem)
   6.247 -  apply (simp add: image_compose [symmetric] o_def)
   6.248 -  apply (simp add: image_def Inv_f_f)
   6.249 -  done
   6.250  
   6.251  subsection {*Other Consequences of Hilbert's Epsilon*}
   6.252  
     7.1 --- a/src/HOL/Library/FuncSet.thy	Sun Oct 18 00:10:20 2009 +0200
     7.2 +++ b/src/HOL/Library/FuncSet.thy	Sun Oct 18 12:07:56 2009 +0200
     7.3 @@ -157,7 +157,7 @@
     7.4  the theorems belong here, or need at least @{term Hilbert_Choice}.*}
     7.5  
     7.6  lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B"
     7.7 -by (auto simp add: bij_betw_def inj_on_Inv)
     7.8 +by (auto simp add: bij_betw_def)
     7.9  
    7.10  lemma inj_on_compose:
    7.11    "[| bij_betw f A B; inj_on g B |] ==> inj_on (compose A g f) A"
    7.12 @@ -190,22 +190,20 @@
    7.13        !!x. x\<in>A ==> f x = g x |] ==> f = g"
    7.14  by (force simp add: expand_fun_eq extensional_def)
    7.15  
    7.16 -lemma Inv_funcset: "f ` A = B ==> (\<lambda>x\<in>B. Inv A f x) : B -> A"
    7.17 -by (unfold Inv_def) (fast intro: someI2)
    7.18 +lemma inv_onto_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_onto A f x) : B -> A"
    7.19 +by (unfold inv_onto_def) (fast intro: someI2)
    7.20  
    7.21 -lemma compose_Inv_id:
    7.22 -  "bij_betw f A B ==> compose A (\<lambda>y\<in>B. Inv A f y) f = (\<lambda>x\<in>A. x)"
    7.23 +lemma compose_inv_onto_id:
    7.24 +  "bij_betw f A B ==> compose A (\<lambda>y\<in>B. inv_onto A f y) f = (\<lambda>x\<in>A. x)"
    7.25  apply (simp add: bij_betw_def compose_def)
    7.26  apply (rule restrict_ext, auto)
    7.27 -apply (erule subst)
    7.28 -apply (simp add: Inv_f_f)
    7.29  done
    7.30  
    7.31 -lemma compose_id_Inv:
    7.32 -  "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)"
    7.33 +lemma compose_id_inv_onto:
    7.34 +  "f ` A = B ==> compose B f (\<lambda>y\<in>B. inv_onto A f y) = (\<lambda>x\<in>B. x)"
    7.35  apply (simp add: compose_def)
    7.36  apply (rule restrict_ext)
    7.37 -apply (simp add: f_Inv_f)
    7.38 +apply (simp add: f_inv_onto_f)
    7.39  done
    7.40  
    7.41  
     8.1 --- a/src/HOL/Library/Permutations.thy	Sun Oct 18 00:10:20 2009 +0200
     8.2 +++ b/src/HOL/Library/Permutations.thy	Sun Oct 18 12:07:56 2009 +0200
     8.3 @@ -5,11 +5,9 @@
     8.4  header {* Permutations, both general and specifically on finite sets.*}
     8.5  
     8.6  theory Permutations
     8.7 -imports Finite_Cartesian_Product Parity Fact Main
     8.8 +imports Finite_Cartesian_Product Parity Fact
     8.9  begin
    8.10  
    8.11 -  (* Why should I import Main just to solve the Typerep problem! *)
    8.12 -
    8.13  definition permutes (infixr "permutes" 41) where
    8.14    "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)"
    8.15  
    8.16 @@ -85,7 +83,7 @@
    8.17    unfolding permutes_def by simp
    8.18  
    8.19  lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y"
    8.20 -  unfolding permutes_def inv_def apply auto
    8.21 +  unfolding permutes_def inv_onto_def apply auto
    8.22    apply (erule allE[where x=y])
    8.23    apply (erule allE[where x=y])
    8.24    apply (rule someI_ex) apply blast
    8.25 @@ -95,10 +93,11 @@
    8.26    done
    8.27  
    8.28  lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S ==> Fun.swap a b id permutes S"
    8.29 -  unfolding permutes_def swap_def fun_upd_def  apply auto apply metis done
    8.30 +  unfolding permutes_def swap_def fun_upd_def  by auto metis
    8.31  
    8.32 -lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
    8.33 -apply (simp add: Ball_def permutes_def Diff_iff) by metis
    8.34 +lemma permutes_superset:
    8.35 +  "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
    8.36 +by (simp add: Ball_def permutes_def Diff_iff) metis
    8.37  
    8.38  (* ------------------------------------------------------------------------- *)
    8.39  (* Group properties.                                                         *)
     9.1 --- a/src/HOL/SizeChange/Correctness.thy	Sun Oct 18 00:10:20 2009 +0200
     9.2 +++ b/src/HOL/SizeChange/Correctness.thy	Sun Oct 18 12:07:56 2009 +0200
     9.3 @@ -1146,7 +1146,7 @@
     9.4    assumes "finite S" 
     9.5    shows "set (set2list S) = S"
     9.6    unfolding set2list_def 
     9.7 -proof (rule f_inv_f)
     9.8 +proof (rule f_inv_onto_f)
     9.9    from `finite S` have "\<exists>l. set l = S"
    9.10      by (rule finite_list)
    9.11    thus "S \<in> range set"
    10.1 --- a/src/HOL/UNITY/Extend.thy	Sun Oct 18 00:10:20 2009 +0200
    10.2 +++ b/src/HOL/UNITY/Extend.thy	Sun Oct 18 12:07:56 2009 +0200
    10.3 @@ -121,12 +121,7 @@
    10.4       assumes surj_h: "surj h"
    10.5           and prem:   "!! x y. g (h(x,y)) = x"
    10.6       shows "fst (inv h z) = g z"
    10.7 -apply (unfold inv_def)
    10.8 -apply (rule_tac y1 = z in surj_h [THEN surjD, THEN exE])
    10.9 -apply (rule someI2)
   10.10 -apply (drule_tac [2] f = g in arg_cong)
   10.11 -apply (auto simp add: prem)
   10.12 -done
   10.13 +by (metis UNIV_I f_inv_onto_f pair_collapse prem surj_h surj_range)
   10.14  
   10.15  
   10.16  subsection{*Trivial properties of f, g, h*}
    11.1 --- a/src/HOL/ZF/HOLZF.thy	Sun Oct 18 00:10:20 2009 +0200
    11.2 +++ b/src/HOL/ZF/HOLZF.thy	Sun Oct 18 12:07:56 2009 +0200
    11.3 @@ -626,7 +626,7 @@
    11.4  
    11.5  lemma nat2Nat_Nat2nat[simp]: "Elem n Nat \<Longrightarrow> nat2Nat (Nat2nat n) = n"
    11.6    apply (simp add: Nat2nat_def)
    11.7 -  apply (rule_tac f_inv_f)
    11.8 +  apply (rule_tac f_inv_onto_f)
    11.9    apply (auto simp add: image_def Nat_def Sep)
   11.10    done
   11.11  
    12.1 --- a/src/HOL/ZF/Zet.thy	Sun Oct 18 00:10:20 2009 +0200
    12.2 +++ b/src/HOL/ZF/Zet.thy	Sun Oct 18 12:07:56 2009 +0200
    12.3 @@ -33,27 +33,12 @@
    12.4    apply (auto simp add: explode_def Sep)
    12.5    done
    12.6  
    12.7 -lemma image_Inv_f_f: "inj_on f B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (Inv B f) ` f ` A = A"
    12.8 -  apply (rule set_ext)
    12.9 -  apply (auto simp add: Inv_f_f image_def)
   12.10 -  apply (rule_tac x="f x" in exI)
   12.11 -  apply (auto simp add: Inv_f_f)
   12.12 -  done
   12.13 -  
   12.14  lemma image_zet_rep: "A \<in> zet \<Longrightarrow> ? z . g ` A = explode z"
   12.15    apply (auto simp add: zet_def')
   12.16 -  apply (rule_tac x="Repl z (g o (Inv A f))" in exI)
   12.17 +  apply (rule_tac x="Repl z (g o (inv_onto A f))" in exI)
   12.18    apply (simp add: explode_Repl_eq)
   12.19    apply (subgoal_tac "explode z = f ` A")
   12.20 -  apply (simp_all add: comp_image_eq image_Inv_f_f)  
   12.21 -  done
   12.22 -
   12.23 -lemma Inv_f_f_mem:       
   12.24 -  assumes "x \<in> A"
   12.25 -  shows "Inv A g (g x) \<in> A"
   12.26 -  apply (simp add: Inv_def)
   12.27 -  apply (rule someI2)
   12.28 -  using `x \<in> A` apply auto
   12.29 +  apply (simp_all add: comp_image_eq)
   12.30    done
   12.31  
   12.32  lemma zet_image_mem:
   12.33 @@ -64,10 +49,10 @@
   12.34      by (auto simp add: zet_def')
   12.35    then obtain f where injf: "inj_on (f :: _ \<Rightarrow> ZF) A"  
   12.36      by auto
   12.37 -  let ?w = "f o (Inv A g)"
   12.38 -  have subset: "(Inv A g) ` (g ` A) \<subseteq> A"
   12.39 -    by (auto simp add: Inv_f_f_mem)
   12.40 -  have "inj_on (Inv A g) (g ` A)" by (simp add: inj_on_Inv)
   12.41 +  let ?w = "f o (inv_onto A g)"
   12.42 +  have subset: "(inv_onto A g) ` (g ` A) \<subseteq> A"
   12.43 +    by (auto simp add: inv_onto_into)
   12.44 +  have "inj_on (inv_onto A g) (g ` A)" by (simp add: inj_on_inv_onto)
   12.45    then have injw: "inj_on ?w (g ` A)"
   12.46      apply (rule comp_inj_on)
   12.47      apply (rule subset_inj_on[where B=A])
   12.48 @@ -101,7 +86,7 @@
   12.49  lemma zexplode_zimplode: "zexplode (zimplode A) = A"
   12.50    apply (simp add: zimplode_def zexplode_def)
   12.51    apply (simp add: implode_def)
   12.52 -  apply (subst f_inv_f[where y="Rep_zet A"])
   12.53 +  apply (subst f_inv_onto_f[where y="Rep_zet A"])
   12.54    apply (auto simp add: Rep_zet_inverse Rep_zet_eq_explode image_def)
   12.55    done
   12.56  
    13.1 --- a/src/HOL/ex/set.thy	Sun Oct 18 00:10:20 2009 +0200
    13.2 +++ b/src/HOL/ex/set.thy	Sun Oct 18 12:07:56 2009 +0200
    13.3 @@ -104,7 +104,7 @@
    13.4      --{*The term above can be synthesized by a sufficiently detailed proof.*}
    13.5    apply (rule bij_if_then_else)
    13.6       apply (rule_tac [4] refl)
    13.7 -    apply (rule_tac [2] inj_on_inv)
    13.8 +    apply (rule_tac [2] inj_on_inv_onto)
    13.9      apply (erule subset_inj_on [OF _ subset_UNIV])
   13.10     apply blast
   13.11    apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])