inv_onto -> inv_into
authornipkow
Thu Oct 22 09:27:48 2009 +0200 (2009-10-22)
changeset 33057764547b68538
parent 33056 791a4655cae3
child 33059 d1c9bf0f8ae8
inv_onto -> inv_into
NEWS
doc-src/Main/Docs/Main_Doc.thy
doc-src/Main/Docs/document/Main_Doc.tex
doc-src/TutorialI/Rules/rules.tex
src/HOL/Algebra/Bij.thy
src/HOL/Algebra/Group.thy
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Permutations.thy
src/HOL/SizeChange/Correctness.thy
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
src/HOL/UNITY/Extend.thy
src/HOL/ZF/HOLZF.thy
src/HOL/ZF/Zet.thy
src/HOL/ex/set.thy
     1.1 --- a/NEWS	Wed Oct 21 17:34:35 2009 +0200
     1.2 +++ b/NEWS	Thu Oct 22 09:27:48 2009 +0200
     1.3 @@ -153,8 +153,8 @@
     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 +* Function "Inv" is renamed to "inv_into" and function "inv" is now an
    1.10 +abbreviation for "inv_into UNIV". Lemmas are renamed accordingly.
    1.11  INCOMPATIBILITY.
    1.12  
    1.13  * ML antiquotation @{code_datatype} inserts definition of a datatype
     2.1 --- a/doc-src/Main/Docs/Main_Doc.thy	Wed Oct 21 17:34:35 2009 +0200
     2.2 +++ b/doc-src/Main/Docs/Main_Doc.thy	Thu Oct 22 09:27:48 2009 +0200
     2.3 @@ -170,13 +170,13 @@
     2.4  \smallskip
     2.5  
     2.6  \begin{tabular}{@ {} l @ {~::~} l @ {}}
     2.7 -@{const Hilbert_Choice.inv_onto} & @{term_type_only Hilbert_Choice.inv_onto "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"}
     2.8 +@{const Hilbert_Choice.inv_into} & @{term_type_only Hilbert_Choice.inv_into "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"}
     2.9  \end{tabular}
    2.10  
    2.11  \subsubsection*{Syntax}
    2.12  
    2.13  \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
    2.14 -@{term inv} & @{term[source]"inv_onto UNIV"}
    2.15 +@{term inv} & @{term[source]"inv_into UNIV"}
    2.16  \end{tabular}
    2.17  
    2.18  \section{Fixed Points}
     3.1 --- a/doc-src/Main/Docs/document/Main_Doc.tex	Wed Oct 21 17:34:35 2009 +0200
     3.2 +++ b/doc-src/Main/Docs/document/Main_Doc.tex	Thu Oct 22 09:27:48 2009 +0200
     3.3 @@ -181,13 +181,13 @@
     3.4  \smallskip
     3.5  
     3.6  \begin{tabular}{@ {} l @ {~::~} l @ {}}
     3.7 -\isa{inv{\isacharunderscore}onto} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a}
     3.8 +\isa{inv{\isacharunderscore}into} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a}
     3.9  \end{tabular}
    3.10  
    3.11  \subsubsection*{Syntax}
    3.12  
    3.13  \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
    3.14 -\isa{inv} & \isa{{\isachardoublequote}inv{\isacharunderscore}onto\ UNIV{\isachardoublequote}}
    3.15 +\isa{inv} & \isa{{\isachardoublequote}inv{\isacharunderscore}into\ UNIV{\isachardoublequote}}
    3.16  \end{tabular}
    3.17  
    3.18  \section{Fixed Points}
     4.1 --- a/doc-src/TutorialI/Rules/rules.tex	Wed Oct 21 17:34:35 2009 +0200
     4.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Thu Oct 22 09:27:48 2009 +0200
     4.3 @@ -1357,7 +1357,7 @@
     4.4  some $x$ such that $P(x)$ is true, provided one exists.
     4.5  Isabelle uses \sdx{SOME} for the Greek letter~$\varepsilon$.
     4.6  
     4.7 -Here is the definition of~\cdx{inv},\footnote{In fact, \isa{inv} is defined via a second constant \isa{inv_onto}, which we ignore here.} which expresses inverses of
     4.8 +Here is the definition of~\cdx{inv},\footnote{In fact, \isa{inv} is defined via a second constant \isa{inv_into}, which we ignore here.} which expresses inverses of
     4.9  functions:
    4.10  \begin{isabelle}
    4.11  inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y%
     5.1 --- a/src/HOL/Algebra/Bij.thy	Wed Oct 21 17:34:35 2009 +0200
     5.2 +++ b/src/HOL/Algebra/Bij.thy	Thu Oct 22 09:27:48 2009 +0200
     5.3 @@ -31,8 +31,8 @@
     5.4  
     5.5  subsection {*Bijections Form a Group *}
     5.6  
     5.7 -lemma restrict_inv_onto_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (inv_onto S f) x) \<in> Bij S"
     5.8 -  by (simp add: Bij_def bij_betw_inv_onto)
     5.9 +lemma restrict_inv_into_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (inv_into S f) x) \<in> Bij S"
    5.10 +  by (simp add: Bij_def bij_betw_inv_into)
    5.11  
    5.12  lemma id_Bij: "(\<lambda>x\<in>S. x) \<in> Bij S "
    5.13    by (auto simp add: Bij_def bij_betw_def inj_on_def)
    5.14 @@ -41,8 +41,8 @@
    5.15    by (auto simp add: Bij_def bij_betw_compose) 
    5.16  
    5.17  lemma Bij_compose_restrict_eq:
    5.18 -     "f \<in> Bij S \<Longrightarrow> compose S (restrict (inv_onto S f) S) f = (\<lambda>x\<in>S. x)"
    5.19 -  by (simp add: Bij_def compose_inv_onto_id)
    5.20 +     "f \<in> Bij S \<Longrightarrow> compose S (restrict (inv_into S f) S) f = (\<lambda>x\<in>S. x)"
    5.21 +  by (simp add: Bij_def compose_inv_into_id)
    5.22  
    5.23  theorem group_BijGroup: "group (BijGroup S)"
    5.24  apply (simp add: BijGroup_def)
    5.25 @@ -52,19 +52,19 @@
    5.26    apply (simp add: compose_Bij)
    5.27    apply (blast intro: compose_assoc [symmetric] dest: Bij_imp_funcset)
    5.28   apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp)
    5.29 -apply (blast intro: Bij_compose_restrict_eq restrict_inv_onto_Bij)
    5.30 +apply (blast intro: Bij_compose_restrict_eq restrict_inv_into_Bij)
    5.31  done
    5.32  
    5.33  
    5.34  subsection{*Automorphisms Form a Group*}
    5.35  
    5.36 -lemma Bij_inv_onto_mem: "\<lbrakk> f \<in> Bij S;  x \<in> S\<rbrakk> \<Longrightarrow> inv_onto S f x \<in> S"
    5.37 -by (simp add: Bij_def bij_betw_def inv_onto_into)
    5.38 +lemma Bij_inv_into_mem: "\<lbrakk> f \<in> Bij S;  x \<in> S\<rbrakk> \<Longrightarrow> inv_into S f x \<in> S"
    5.39 +by (simp add: Bij_def bij_betw_def inv_into_into)
    5.40  
    5.41 -lemma Bij_inv_onto_lemma:
    5.42 +lemma Bij_inv_into_lemma:
    5.43   assumes eq: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> h(g x y) = g (h x) (h y)"
    5.44   shows "\<lbrakk>h \<in> Bij S;  g \<in> S \<rightarrow> S \<rightarrow> S;  x \<in> S;  y \<in> S\<rbrakk>
    5.45 -        \<Longrightarrow> inv_onto S h (g x y) = g (inv_onto S h x) (inv_onto S h y)"
    5.46 +        \<Longrightarrow> inv_into S h (g x y) = g (inv_into S h x) (inv_into S h y)"
    5.47  apply (simp add: Bij_def bij_betw_def)
    5.48  apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' & y = h y'", clarify)
    5.49   apply (simp add: eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem], blast)
    5.50 @@ -84,17 +84,17 @@
    5.51  lemma (in group) mult_funcset: "mult G \<in> carrier G \<rightarrow> carrier G \<rightarrow> carrier G"
    5.52    by (simp add:  Pi_I group.axioms)
    5.53  
    5.54 -lemma (in group) restrict_inv_onto_hom:
    5.55 +lemma (in group) restrict_inv_into_hom:
    5.56        "\<lbrakk>h \<in> hom G G; h \<in> Bij (carrier G)\<rbrakk>
    5.57 -       \<Longrightarrow> restrict (inv_onto (carrier G) h) (carrier G) \<in> hom G G"
    5.58 -  by (simp add: hom_def Bij_inv_onto_mem restrictI mult_funcset
    5.59 -                group.axioms Bij_inv_onto_lemma)
    5.60 +       \<Longrightarrow> restrict (inv_into (carrier G) h) (carrier G) \<in> hom G G"
    5.61 +  by (simp add: hom_def Bij_inv_into_mem restrictI mult_funcset
    5.62 +                group.axioms Bij_inv_into_lemma)
    5.63  
    5.64  lemma inv_BijGroup:
    5.65 -     "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (inv_onto S f) x)"
    5.66 +     "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (inv_into S f) x)"
    5.67  apply (rule group.inv_equality)
    5.68  apply (rule group_BijGroup)
    5.69 -apply (simp_all add:BijGroup_def restrict_inv_onto_Bij Bij_compose_restrict_eq)
    5.70 +apply (simp_all add:BijGroup_def restrict_inv_into_Bij Bij_compose_restrict_eq)
    5.71  done
    5.72  
    5.73  lemma (in group) subgroup_auto:
    5.74 @@ -115,7 +115,7 @@
    5.75    assume "x \<in> auto G" 
    5.76    thus "inv\<^bsub>BijGroup (carrier G)\<^esub> x \<in> auto G"
    5.77      by (simp del: restrict_apply
    5.78 -        add: inv_BijGroup auto_def restrict_inv_onto_Bij restrict_inv_onto_hom)
    5.79 +        add: inv_BijGroup auto_def restrict_inv_into_Bij restrict_inv_into_hom)
    5.80  qed
    5.81  
    5.82  theorem (in group) AutoGroup: "group (AutoGroup G)"
     6.1 --- a/src/HOL/Algebra/Group.thy	Wed Oct 21 17:34:35 2009 +0200
     6.2 +++ b/src/HOL/Algebra/Group.thy	Thu Oct 22 09:27:48 2009 +0200
     6.3 @@ -553,11 +553,11 @@
     6.4  by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
     6.5  
     6.6  lemma (in group) iso_sym:
     6.7 -     "h \<in> G \<cong> H \<Longrightarrow> inv_onto (carrier G) h \<in> H \<cong> G"
     6.8 -apply (simp add: iso_def bij_betw_inv_onto) 
     6.9 -apply (subgoal_tac "inv_onto (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
    6.10 - prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_onto]) 
    6.11 -apply (simp add: hom_def bij_betw_def inv_onto_f_eq f_inv_onto_f Pi_def)
    6.12 +     "h \<in> G \<cong> H \<Longrightarrow> inv_into (carrier G) h \<in> H \<cong> G"
    6.13 +apply (simp add: iso_def bij_betw_inv_into) 
    6.14 +apply (subgoal_tac "inv_into (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
    6.15 + prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_into]) 
    6.16 +apply (simp add: hom_def bij_betw_def inv_into_f_eq f_inv_into_f Pi_def)
    6.17  done
    6.18  
    6.19  lemma (in group) iso_trans: 
     7.1 --- a/src/HOL/Finite_Set.thy	Wed Oct 21 17:34:35 2009 +0200
     7.2 +++ b/src/HOL/Finite_Set.thy	Thu Oct 22 09:27:48 2009 +0200
     7.3 @@ -162,9 +162,9 @@
     7.4    from finite_imp_nat_seg_image_inj_on[OF `finite A`]
     7.5    obtain f and n::nat where bij: "bij_betw f {i. i<n} A"
     7.6      by (auto simp:bij_betw_def)
     7.7 -  let ?f = "the_inv_onto {i. i<n} f"
     7.8 +  let ?f = "the_inv_into {i. i<n} f"
     7.9    have "inj_on ?f A & ?f ` A = {i. i<n}"
    7.10 -    by (fold bij_betw_def) (rule bij_betw_the_inv_onto[OF bij])
    7.11 +    by (fold bij_betw_def) (rule bij_betw_the_inv_into[OF bij])
    7.12    thus ?thesis by blast
    7.13  qed
    7.14  
     8.1 --- a/src/HOL/Fun.thy	Wed Oct 21 17:34:35 2009 +0200
     8.2 +++ b/src/HOL/Fun.thy	Thu Oct 22 09:27:48 2009 +0200
     8.3 @@ -508,65 +508,65 @@
     8.4  
     8.5  subsection {* Inversion of injective functions *}
     8.6  
     8.7 -definition the_inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where
     8.8 -"the_inv_onto A f == %x. THE y. y : A & f y = x"
     8.9 +definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
    8.10 +"the_inv_into A f == %x. THE y. y : A & f y = x"
    8.11  
    8.12 -lemma the_inv_onto_f_f:
    8.13 -  "[| inj_on f A;  x : A |] ==> the_inv_onto A f (f x) = x"
    8.14 -apply (simp add: the_inv_onto_def inj_on_def)
    8.15 +lemma the_inv_into_f_f:
    8.16 +  "[| inj_on f A;  x : A |] ==> the_inv_into A f (f x) = x"
    8.17 +apply (simp add: the_inv_into_def inj_on_def)
    8.18  apply (blast intro: the_equality)
    8.19  done
    8.20  
    8.21 -lemma f_the_inv_onto_f:
    8.22 -  "inj_on f A ==> y : f`A  ==> f (the_inv_onto A f y) = y"
    8.23 -apply (simp add: the_inv_onto_def)
    8.24 +lemma f_the_inv_into_f:
    8.25 +  "inj_on f A ==> y : f`A  ==> f (the_inv_into A f y) = y"
    8.26 +apply (simp add: the_inv_into_def)
    8.27  apply (rule the1I2)
    8.28   apply(blast dest: inj_onD)
    8.29  apply blast
    8.30  done
    8.31  
    8.32 -lemma the_inv_onto_into:
    8.33 -  "[| inj_on f A; x : f ` A; A <= B |] ==> the_inv_onto A f x : B"
    8.34 -apply (simp add: the_inv_onto_def)
    8.35 +lemma the_inv_into_into:
    8.36 +  "[| inj_on f A; x : f ` A; A <= B |] ==> the_inv_into A f x : B"
    8.37 +apply (simp add: the_inv_into_def)
    8.38  apply (rule the1I2)
    8.39   apply(blast dest: inj_onD)
    8.40  apply blast
    8.41  done
    8.42  
    8.43 -lemma the_inv_onto_onto[simp]:
    8.44 -  "inj_on f A ==> the_inv_onto A f ` (f ` A) = A"
    8.45 -by (fast intro:the_inv_onto_into the_inv_onto_f_f[symmetric])
    8.46 +lemma the_inv_into_onto[simp]:
    8.47 +  "inj_on f A ==> the_inv_into A f ` (f ` A) = A"
    8.48 +by (fast intro:the_inv_into_into the_inv_into_f_f[symmetric])
    8.49  
    8.50 -lemma the_inv_onto_f_eq:
    8.51 -  "[| inj_on f A; f x = y; x : A |] ==> the_inv_onto A f y = x"
    8.52 +lemma the_inv_into_f_eq:
    8.53 +  "[| inj_on f A; f x = y; x : A |] ==> the_inv_into A f y = x"
    8.54    apply (erule subst)
    8.55 -  apply (erule the_inv_onto_f_f, assumption)
    8.56 +  apply (erule the_inv_into_f_f, assumption)
    8.57    done
    8.58  
    8.59 -lemma the_inv_onto_comp:
    8.60 +lemma the_inv_into_comp:
    8.61    "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
    8.62 -  the_inv_onto A (f o g) x = (the_inv_onto A g o the_inv_onto (g ` A) f) x"
    8.63 -apply (rule the_inv_onto_f_eq)
    8.64 +  the_inv_into A (f o g) x = (the_inv_into A g o the_inv_into (g ` A) f) x"
    8.65 +apply (rule the_inv_into_f_eq)
    8.66    apply (fast intro: comp_inj_on)
    8.67 - apply (simp add: f_the_inv_onto_f the_inv_onto_into)
    8.68 -apply (simp add: the_inv_onto_into)
    8.69 + apply (simp add: f_the_inv_into_f the_inv_into_into)
    8.70 +apply (simp add: the_inv_into_into)
    8.71  done
    8.72  
    8.73 -lemma inj_on_the_inv_onto:
    8.74 -  "inj_on f A \<Longrightarrow> inj_on (the_inv_onto A f) (f ` A)"
    8.75 -by (auto intro: inj_onI simp: image_def the_inv_onto_f_f)
    8.76 +lemma inj_on_the_inv_into:
    8.77 +  "inj_on f A \<Longrightarrow> inj_on (the_inv_into A f) (f ` A)"
    8.78 +by (auto intro: inj_onI simp: image_def the_inv_into_f_f)
    8.79  
    8.80 -lemma bij_betw_the_inv_onto:
    8.81 -  "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_onto A f) B A"
    8.82 -by (auto simp add: bij_betw_def inj_on_the_inv_onto the_inv_onto_into)
    8.83 +lemma bij_betw_the_inv_into:
    8.84 +  "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_into A f) B A"
    8.85 +by (auto simp add: bij_betw_def inj_on_the_inv_into the_inv_into_into)
    8.86  
    8.87  abbreviation the_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
    8.88 -  "the_inv f \<equiv> the_inv_onto UNIV f"
    8.89 +  "the_inv f \<equiv> the_inv_into UNIV f"
    8.90  
    8.91  lemma the_inv_f_f:
    8.92    assumes "inj f"
    8.93    shows "the_inv f (f x) = x" using assms UNIV_I
    8.94 -  by (rule the_inv_onto_f_f)
    8.95 +  by (rule the_inv_into_f_f)
    8.96  
    8.97  
    8.98  subsection {* Proof tool setup *} 
     9.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Oct 21 17:34:35 2009 +0200
     9.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Oct 22 09:27:48 2009 +0200
     9.3 @@ -31,11 +31,11 @@
     9.4       in Syntax.const "_Eps" $ x $ t end)]
     9.5  *}
     9.6  
     9.7 -definition inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where
     9.8 -"inv_onto A f == %x. SOME y. y : A & f y = x"
     9.9 +definition inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
    9.10 +"inv_into A f == %x. SOME y. y : A & f y = x"
    9.11  
    9.12  abbreviation inv :: "('a => 'b) => ('b => 'a)" where
    9.13 -"inv == inv_onto UNIV"
    9.14 +"inv == inv_into UNIV"
    9.15  
    9.16  
    9.17  subsection {*Hilbert's Epsilon-operator*}
    9.18 @@ -92,40 +92,40 @@
    9.19  subsection {*Function Inverse*}
    9.20  
    9.21  lemma inv_def: "inv f = (%y. SOME x. f x = y)"
    9.22 -by(simp add: inv_onto_def)
    9.23 +by(simp add: inv_into_def)
    9.24  
    9.25 -lemma inv_onto_into: "x : f ` A ==> inv_onto A f x : A"
    9.26 -apply (simp add: inv_onto_def)
    9.27 +lemma inv_into_into: "x : f ` A ==> inv_into A f x : A"
    9.28 +apply (simp add: inv_into_def)
    9.29  apply (fast intro: someI2)
    9.30  done
    9.31  
    9.32  lemma inv_id [simp]: "inv id = id"
    9.33 -by (simp add: inv_onto_def id_def)
    9.34 +by (simp add: inv_into_def id_def)
    9.35  
    9.36 -lemma inv_onto_f_f [simp]:
    9.37 -  "[| inj_on f A;  x : A |] ==> inv_onto A f (f x) = x"
    9.38 -apply (simp add: inv_onto_def inj_on_def)
    9.39 +lemma inv_into_f_f [simp]:
    9.40 +  "[| inj_on f A;  x : A |] ==> inv_into A f (f x) = x"
    9.41 +apply (simp add: inv_into_def inj_on_def)
    9.42  apply (blast intro: someI2)
    9.43  done
    9.44  
    9.45  lemma inv_f_f: "inj f ==> inv f (f x) = x"
    9.46 -by (simp add: inv_onto_f_f)
    9.47 +by (simp add: inv_into_f_f)
    9.48  
    9.49 -lemma f_inv_onto_f: "y : f`A  ==> f (inv_onto A f y) = y"
    9.50 -apply (simp add: inv_onto_def)
    9.51 +lemma f_inv_into_f: "y : f`A  ==> f (inv_into A f y) = y"
    9.52 +apply (simp add: inv_into_def)
    9.53  apply (fast intro: someI2)
    9.54  done
    9.55  
    9.56 -lemma inv_onto_f_eq: "[| inj_on f A; x : A; f x = y |] ==> inv_onto A f y = x"
    9.57 +lemma inv_into_f_eq: "[| inj_on f A; x : A; f x = y |] ==> inv_into A f y = x"
    9.58  apply (erule subst)
    9.59 -apply (fast intro: inv_onto_f_f)
    9.60 +apply (fast intro: inv_into_f_f)
    9.61  done
    9.62  
    9.63  lemma inv_f_eq: "[| inj f; f x = y |] ==> inv f y = x"
    9.64 -by (simp add:inv_onto_f_eq)
    9.65 +by (simp add:inv_into_f_eq)
    9.66  
    9.67  lemma inj_imp_inv_eq: "[| inj f; ALL x. f(g x) = x |] ==> inv f = g"
    9.68 -by (blast intro: ext inv_onto_f_eq)
    9.69 +by (blast intro: ext inv_into_f_eq)
    9.70  
    9.71  text{*But is it useful?*}
    9.72  lemma inj_transfer:
    9.73 @@ -134,12 +134,12 @@
    9.74  proof -
    9.75    have "f x \<in> range f" by auto
    9.76    hence "P(inv f (f x))" by (rule minor)
    9.77 -  thus "P x" by (simp add: inv_onto_f_f [OF injf])
    9.78 +  thus "P x" by (simp add: inv_into_f_f [OF injf])
    9.79  qed
    9.80  
    9.81  lemma inj_iff: "(inj f) = (inv f o f = id)"
    9.82  apply (simp add: o_def expand_fun_eq)
    9.83 -apply (blast intro: inj_on_inverseI inv_onto_f_f)
    9.84 +apply (blast intro: inj_on_inverseI inv_into_f_f)
    9.85  done
    9.86  
    9.87  lemma inv_o_cancel[simp]: "inj f ==> inv f o f = id"
    9.88 @@ -148,34 +148,34 @@
    9.89  lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g"
    9.90  by (simp add: o_assoc[symmetric])
    9.91  
    9.92 -lemma inv_onto_image_cancel[simp]:
    9.93 -  "inj_on f A ==> S <= A ==> inv_onto A f ` f ` S = S"
    9.94 +lemma inv_into_image_cancel[simp]:
    9.95 +  "inj_on f A ==> S <= A ==> inv_into A f ` f ` S = S"
    9.96  by(fastsimp simp: image_def)
    9.97  
    9.98  lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
    9.99 -by (blast intro: surjI inv_onto_f_f)
   9.100 +by (blast intro: surjI inv_into_f_f)
   9.101  
   9.102  lemma surj_f_inv_f: "surj f ==> f(inv f y) = y"
   9.103 -by (simp add: f_inv_onto_f surj_range)
   9.104 +by (simp add: f_inv_into_f surj_range)
   9.105  
   9.106 -lemma inv_onto_injective:
   9.107 -  assumes eq: "inv_onto A f x = inv_onto A f y"
   9.108 +lemma inv_into_injective:
   9.109 +  assumes eq: "inv_into A f x = inv_into A f y"
   9.110        and x: "x: f`A"
   9.111        and y: "y: f`A"
   9.112    shows "x=y"
   9.113  proof -
   9.114 -  have "f (inv_onto A f x) = f (inv_onto A f y)" using eq by simp
   9.115 -  thus ?thesis by (simp add: f_inv_onto_f x y)
   9.116 +  have "f (inv_into A f x) = f (inv_into A f y)" using eq by simp
   9.117 +  thus ?thesis by (simp add: f_inv_into_f x y)
   9.118  qed
   9.119  
   9.120 -lemma inj_on_inv_onto: "B <= f`A ==> inj_on (inv_onto A f) B"
   9.121 -by (blast intro: inj_onI dest: inv_onto_injective injD)
   9.122 +lemma inj_on_inv_into: "B <= f`A ==> inj_on (inv_into A f) B"
   9.123 +by (blast intro: inj_onI dest: inv_into_injective injD)
   9.124  
   9.125 -lemma bij_betw_inv_onto: "bij_betw f A B ==> bij_betw (inv_onto A f) B A"
   9.126 -by (auto simp add: bij_betw_def inj_on_inv_onto)
   9.127 +lemma bij_betw_inv_into: "bij_betw f A B ==> bij_betw (inv_into A f) B A"
   9.128 +by (auto simp add: bij_betw_def inj_on_inv_into)
   9.129  
   9.130  lemma surj_imp_inj_inv: "surj f ==> inj (inv f)"
   9.131 -by (simp add: inj_on_inv_onto surj_range)
   9.132 +by (simp add: inj_on_inv_into surj_range)
   9.133  
   9.134  lemma surj_iff: "(surj f) = (f o inv f = id)"
   9.135  apply (simp add: o_def expand_fun_eq)
   9.136 @@ -193,7 +193,7 @@
   9.137  
   9.138  lemma inv_equality: "[| !!x. g (f x) = x;  !!y. f (g y) = y |] ==> inv f = g"
   9.139  apply (rule ext)
   9.140 -apply (auto simp add: inv_onto_def)
   9.141 +apply (auto simp add: inv_into_def)
   9.142  done
   9.143  
   9.144  lemma inv_inv_eq: "bij f ==> inv (inv f) = f"
   9.145 @@ -208,13 +208,13 @@
   9.146      inv(inv f)=f all fail.
   9.147  **)
   9.148  
   9.149 -lemma inv_onto_comp:
   9.150 +lemma inv_into_comp:
   9.151    "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
   9.152 -  inv_onto A (f o g) x = (inv_onto A g o inv_onto (g ` A) f) x"
   9.153 -apply (rule inv_onto_f_eq)
   9.154 +  inv_into A (f o g) x = (inv_into A g o inv_into (g ` A) f) x"
   9.155 +apply (rule inv_into_f_eq)
   9.156    apply (fast intro: comp_inj_on)
   9.157 - apply (simp add: inv_onto_into)
   9.158 -apply (simp add: f_inv_onto_f inv_onto_into)
   9.159 + apply (simp add: inv_into_into)
   9.160 +apply (simp add: f_inv_into_f inv_into_into)
   9.161  done
   9.162  
   9.163  lemma o_inv_distrib: "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f"
   9.164 @@ -239,7 +239,7 @@
   9.165  
   9.166  lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A" 
   9.167  apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
   9.168 -apply (blast intro: bij_is_inj [THEN inv_onto_f_f, symmetric])
   9.169 +apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
   9.170  done
   9.171  
   9.172  lemma finite_fun_UNIVD1:
   9.173 @@ -256,7 +256,7 @@
   9.174    moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
   9.175    proof (rule UNIV_eq_I)
   9.176      fix x :: 'a
   9.177 -    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_onto_def)
   9.178 +    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_into_def)
   9.179      thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast
   9.180    qed
   9.181    ultimately show "finite (UNIV :: 'a set)" by simp
    10.1 --- a/src/HOL/Library/FuncSet.thy	Wed Oct 21 17:34:35 2009 +0200
    10.2 +++ b/src/HOL/Library/FuncSet.thy	Thu Oct 22 09:27:48 2009 +0200
    10.3 @@ -190,20 +190,20 @@
    10.4        !!x. x\<in>A ==> f x = g x |] ==> f = g"
    10.5  by (force simp add: expand_fun_eq extensional_def)
    10.6  
    10.7 -lemma inv_onto_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_onto A f x) : B -> A"
    10.8 -by (unfold inv_onto_def) (fast intro: someI2)
    10.9 +lemma inv_into_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_into A f x) : B -> A"
   10.10 +by (unfold inv_into_def) (fast intro: someI2)
   10.11  
   10.12 -lemma compose_inv_onto_id:
   10.13 -  "bij_betw f A B ==> compose A (\<lambda>y\<in>B. inv_onto A f y) f = (\<lambda>x\<in>A. x)"
   10.14 +lemma compose_inv_into_id:
   10.15 +  "bij_betw f A B ==> compose A (\<lambda>y\<in>B. inv_into A f y) f = (\<lambda>x\<in>A. x)"
   10.16  apply (simp add: bij_betw_def compose_def)
   10.17  apply (rule restrict_ext, auto)
   10.18  done
   10.19  
   10.20 -lemma compose_id_inv_onto:
   10.21 -  "f ` A = B ==> compose B f (\<lambda>y\<in>B. inv_onto A f y) = (\<lambda>x\<in>B. x)"
   10.22 +lemma compose_id_inv_into:
   10.23 +  "f ` A = B ==> compose B f (\<lambda>y\<in>B. inv_into A f y) = (\<lambda>x\<in>B. x)"
   10.24  apply (simp add: compose_def)
   10.25  apply (rule restrict_ext)
   10.26 -apply (simp add: f_inv_onto_f)
   10.27 +apply (simp add: f_inv_into_f)
   10.28  done
   10.29  
   10.30  
    11.1 --- a/src/HOL/Library/Permutations.thy	Wed Oct 21 17:34:35 2009 +0200
    11.2 +++ b/src/HOL/Library/Permutations.thy	Thu Oct 22 09:27:48 2009 +0200
    11.3 @@ -83,7 +83,7 @@
    11.4    unfolding permutes_def by simp
    11.5  
    11.6  lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y"
    11.7 -  unfolding permutes_def inv_onto_def apply auto
    11.8 +  unfolding permutes_def inv_def apply auto
    11.9    apply (erule allE[where x=y])
   11.10    apply (erule allE[where x=y])
   11.11    apply (rule someI_ex) apply blast
    12.1 --- a/src/HOL/SizeChange/Correctness.thy	Wed Oct 21 17:34:35 2009 +0200
    12.2 +++ b/src/HOL/SizeChange/Correctness.thy	Thu Oct 22 09:27:48 2009 +0200
    12.3 @@ -1146,7 +1146,7 @@
    12.4    assumes "finite S" 
    12.5    shows "set (set2list S) = S"
    12.6    unfolding set2list_def 
    12.7 -proof (rule f_inv_onto_f)
    12.8 +proof (rule f_inv_into_f)
    12.9    from `finite S` have "\<exists>l. set l = S"
   12.10      by (rule finite_list)
   12.11    thus "S \<in> range set"
    13.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Wed Oct 21 17:34:35 2009 +0200
    13.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Thu Oct 22 09:27:48 2009 +0200
    13.3 @@ -481,7 +481,7 @@
    13.4  
    13.5      val Abs_inverse_thms' =
    13.6        map #1 newT_iso_axms @
    13.7 -      map2 (fn r_inj => fn r => @{thm f_the_inv_onto_f} OF [r_inj, r RS mp])
    13.8 +      map2 (fn r_inj => fn r => @{thm f_the_inv_into_f} OF [r_inj, r RS mp])
    13.9          iso_inj_thms_unfolded iso_thms;
   13.10  
   13.11      val Abs_inverse_thms = maps (mk_funs_inv thy5) Abs_inverse_thms';
   13.12 @@ -571,7 +571,7 @@
   13.13          val Abs_t = if i < length newTs then
   13.14              Const (Sign.intern_const thy6
   13.15                ("Abs_" ^ (nth new_type_names i)), Univ_elT --> T)
   13.16 -          else Const (@{const_name the_inv_onto},
   13.17 +          else Const (@{const_name the_inv_into},
   13.18                [HOLogic.mk_setT T, T --> Univ_elT, Univ_elT] ---> T) $
   13.19              HOLogic.mk_UNIV T $ Const (nth all_rep_names i, T --> Univ_elT)
   13.20  
    14.1 --- a/src/HOL/UNITY/Extend.thy	Wed Oct 21 17:34:35 2009 +0200
    14.2 +++ b/src/HOL/UNITY/Extend.thy	Thu Oct 22 09:27:48 2009 +0200
    14.3 @@ -121,7 +121,7 @@
    14.4       assumes surj_h: "surj h"
    14.5           and prem:   "!! x y. g (h(x,y)) = x"
    14.6       shows "fst (inv h z) = g z"
    14.7 -by (metis UNIV_I f_inv_onto_f pair_collapse prem surj_h surj_range)
    14.8 +by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h surj_range)
    14.9  
   14.10  
   14.11  subsection{*Trivial properties of f, g, h*}
    15.1 --- a/src/HOL/ZF/HOLZF.thy	Wed Oct 21 17:34:35 2009 +0200
    15.2 +++ b/src/HOL/ZF/HOLZF.thy	Thu Oct 22 09:27:48 2009 +0200
    15.3 @@ -626,7 +626,7 @@
    15.4  
    15.5  lemma nat2Nat_Nat2nat[simp]: "Elem n Nat \<Longrightarrow> nat2Nat (Nat2nat n) = n"
    15.6    apply (simp add: Nat2nat_def)
    15.7 -  apply (rule_tac f_inv_onto_f)
    15.8 +  apply (rule_tac f_inv_into_f)
    15.9    apply (auto simp add: image_def Nat_def Sep)
   15.10    done
   15.11  
    16.1 --- a/src/HOL/ZF/Zet.thy	Wed Oct 21 17:34:35 2009 +0200
    16.2 +++ b/src/HOL/ZF/Zet.thy	Thu Oct 22 09:27:48 2009 +0200
    16.3 @@ -35,7 +35,7 @@
    16.4  
    16.5  lemma image_zet_rep: "A \<in> zet \<Longrightarrow> ? z . g ` A = explode z"
    16.6    apply (auto simp add: zet_def')
    16.7 -  apply (rule_tac x="Repl z (g o (inv_onto A f))" in exI)
    16.8 +  apply (rule_tac x="Repl z (g o (inv_into A f))" in exI)
    16.9    apply (simp add: explode_Repl_eq)
   16.10    apply (subgoal_tac "explode z = f ` A")
   16.11    apply (simp_all add: comp_image_eq)
   16.12 @@ -49,10 +49,10 @@
   16.13      by (auto simp add: zet_def')
   16.14    then obtain f where injf: "inj_on (f :: _ \<Rightarrow> ZF) A"  
   16.15      by auto
   16.16 -  let ?w = "f o (inv_onto A g)"
   16.17 -  have subset: "(inv_onto A g) ` (g ` A) \<subseteq> A"
   16.18 -    by (auto simp add: inv_onto_into)
   16.19 -  have "inj_on (inv_onto A g) (g ` A)" by (simp add: inj_on_inv_onto)
   16.20 +  let ?w = "f o (inv_into A g)"
   16.21 +  have subset: "(inv_into A g) ` (g ` A) \<subseteq> A"
   16.22 +    by (auto simp add: inv_into_into)
   16.23 +  have "inj_on (inv_into A g) (g ` A)" by (simp add: inj_on_inv_into)
   16.24    then have injw: "inj_on ?w (g ` A)"
   16.25      apply (rule comp_inj_on)
   16.26      apply (rule subset_inj_on[where B=A])
   16.27 @@ -86,7 +86,7 @@
   16.28  lemma zexplode_zimplode: "zexplode (zimplode A) = A"
   16.29    apply (simp add: zimplode_def zexplode_def)
   16.30    apply (simp add: implode_def)
   16.31 -  apply (subst f_inv_onto_f[where y="Rep_zet A"])
   16.32 +  apply (subst f_inv_into_f[where y="Rep_zet A"])
   16.33    apply (auto simp add: Rep_zet_inverse Rep_zet_eq_explode image_def)
   16.34    done
   16.35  
    17.1 --- a/src/HOL/ex/set.thy	Wed Oct 21 17:34:35 2009 +0200
    17.2 +++ b/src/HOL/ex/set.thy	Thu Oct 22 09:27:48 2009 +0200
    17.3 @@ -104,7 +104,7 @@
    17.4      --{*The term above can be synthesized by a sufficiently detailed proof.*}
    17.5    apply (rule bij_if_then_else)
    17.6       apply (rule_tac [4] refl)
    17.7 -    apply (rule_tac [2] inj_on_inv_onto)
    17.8 +    apply (rule_tac [2] inj_on_inv_into)
    17.9      apply (erule subset_inj_on [OF _ subset_UNIV])
   17.10     apply blast
   17.11    apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])