merged
authorwenzelm
Thu, 22 Oct 2009 15:20:54 +0200
changeset 33069 d284306ea923
parent 33065 1cefea81ec4f (diff)
parent 33068 bee53a9f45c8 (current diff)
child 33070 c39f6bd5a46b
merged
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- a/NEWS	Wed Oct 21 22:01:44 2009 +0200
+++ b/NEWS	Thu Oct 22 15:20:54 2009 +0200
@@ -153,8 +153,8 @@
 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.
+* Function "Inv" is renamed to "inv_into" and function "inv" is now an
+abbreviation for "inv_into UNIV". Lemmas are renamed accordingly.
 INCOMPATIBILITY.
 
 * ML antiquotation @{code_datatype} inserts definition of a datatype
--- a/doc-src/Main/Docs/Main_Doc.thy	Wed Oct 21 22:01:44 2009 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy	Thu Oct 22 15:20:54 2009 +0200
@@ -170,13 +170,13 @@
 \smallskip
 
 \begin{tabular}{@ {} l @ {~::~} l @ {}}
-@{const Hilbert_Choice.inv_onto} & @{term_type_only Hilbert_Choice.inv_onto "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"}
+@{const Hilbert_Choice.inv_into} & @{term_type_only Hilbert_Choice.inv_into "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"}
 \end{tabular}
 
 \subsubsection*{Syntax}
 
 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{term inv} & @{term[source]"inv_onto UNIV"}
+@{term inv} & @{term[source]"inv_into UNIV"}
 \end{tabular}
 
 \section{Fixed Points}
--- a/doc-src/Main/Docs/document/Main_Doc.tex	Wed Oct 21 22:01:44 2009 +0200
+++ b/doc-src/Main/Docs/document/Main_Doc.tex	Thu Oct 22 15:20:54 2009 +0200
@@ -181,13 +181,13 @@
 \smallskip
 
 \begin{tabular}{@ {} l @ {~::~} l @ {}}
-\isa{inv{\isacharunderscore}onto} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a}
+\isa{inv{\isacharunderscore}into} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a}
 \end{tabular}
 
 \subsubsection*{Syntax}
 
 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-\isa{inv} & \isa{{\isachardoublequote}inv{\isacharunderscore}onto\ UNIV{\isachardoublequote}}
+\isa{inv} & \isa{{\isachardoublequote}inv{\isacharunderscore}into\ UNIV{\isachardoublequote}}
 \end{tabular}
 
 \section{Fixed Points}
--- a/doc-src/TutorialI/Rules/rules.tex	Wed Oct 21 22:01:44 2009 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Thu Oct 22 15:20:54 2009 +0200
@@ -1357,7 +1357,7 @@
 some $x$ such that $P(x)$ is true, provided one exists.
 Isabelle uses \sdx{SOME} for the Greek letter~$\varepsilon$.
 
-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
+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
 functions:
 \begin{isabelle}
 inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y%
--- a/src/FOLP/simp.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/FOLP/simp.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -534,7 +534,7 @@
 
 fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) =
 let fun xn_list(x,n) =
-        let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n);
+        let val ixs = map_range (fn i => (x^(radixstring(26,"a",i)),0)) (n - 1);
         in ListPair.map eta_Var (ixs, Library.take(n+1,Ts)) end
     val lhs = list_comb(f,xn_list("X",k-1))
     val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)
--- a/src/HOL/Algebra/Bij.thy	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Algebra/Bij.thy	Thu Oct 22 15:20:54 2009 +0200
@@ -31,8 +31,8 @@
 
 subsection {*Bijections Form a Group *}
 
-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 restrict_inv_into_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (inv_into S f) x) \<in> Bij S"
+  by (simp add: Bij_def bij_betw_inv_into)
 
 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_onto S f) S) f = (\<lambda>x\<in>S. x)"
-  by (simp add: Bij_def compose_inv_onto_id)
+     "f \<in> Bij S \<Longrightarrow> compose S (restrict (inv_into S f) S) f = (\<lambda>x\<in>S. x)"
+  by (simp add: Bij_def compose_inv_into_id)
 
 theorem group_BijGroup: "group (BijGroup S)"
 apply (simp add: BijGroup_def)
@@ -52,19 +52,19 @@
   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_onto_Bij)
+apply (blast intro: Bij_compose_restrict_eq restrict_inv_into_Bij)
 done
 
 
 subsection{*Automorphisms Form a Group*}
 
-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_into_mem: "\<lbrakk> f \<in> Bij S;  x \<in> S\<rbrakk> \<Longrightarrow> inv_into S f x \<in> S"
+by (simp add: Bij_def bij_betw_def inv_into_into)
 
-lemma Bij_inv_onto_lemma:
+lemma Bij_inv_into_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_onto S h (g x y) = g (inv_onto S h x) (inv_onto S h y)"
+        \<Longrightarrow> inv_into S h (g x y) = g (inv_into S h x) (inv_into 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)
@@ -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_onto_hom:
+lemma (in group) restrict_inv_into_hom:
       "\<lbrakk>h \<in> hom G G; h \<in> Bij (carrier G)\<rbrakk>
-       \<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)
+       \<Longrightarrow> restrict (inv_into (carrier G) h) (carrier G) \<in> hom G G"
+  by (simp add: hom_def Bij_inv_into_mem restrictI mult_funcset
+                group.axioms Bij_inv_into_lemma)
 
 lemma inv_BijGroup:
-     "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (inv_onto S f) x)"
+     "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (inv_into S f) x)"
 apply (rule group.inv_equality)
 apply (rule group_BijGroup)
-apply (simp_all add:BijGroup_def restrict_inv_onto_Bij Bij_compose_restrict_eq)
+apply (simp_all add:BijGroup_def restrict_inv_into_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_onto_Bij restrict_inv_onto_hom)
+        add: inv_BijGroup auto_def restrict_inv_into_Bij restrict_inv_into_hom)
 qed
 
 theorem (in group) AutoGroup: "group (AutoGroup G)"
--- a/src/HOL/Algebra/Group.thy	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Algebra/Group.thy	Thu Oct 22 15:20:54 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_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)
+     "h \<in> G \<cong> H \<Longrightarrow> inv_into (carrier G) h \<in> H \<cong> G"
+apply (simp add: iso_def bij_betw_inv_into) 
+apply (subgoal_tac "inv_into (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
+ prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_into]) 
+apply (simp add: hom_def bij_betw_def inv_into_f_eq f_inv_into_f Pi_def)
 done
 
 lemma (in group) iso_trans: 
--- a/src/HOL/Decision_Procs/Cooper.thy	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Oct 22 15:20:54 2009 +0200
@@ -2035,8 +2035,8 @@
     val t = Thm.term_of ct;
     val fs = OldTerm.term_frees t;
     val bs = term_bools [] t;
-    val vs = fs ~~ (0 upto (length fs - 1))
-    val ps = bs ~~ (0 upto (length bs - 1))
+    val vs = map_index swap fs;
+    val ps = map_index swap bs;
     val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t;
   in (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
 end;
--- a/src/HOL/Decision_Procs/Ferrack.thy	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Oct 22 15:20:54 2009 +0200
@@ -2073,7 +2073,7 @@
     val thy = Thm.theory_of_cterm ct;
     val t = Thm.term_of ct;
     val fs = OldTerm.term_frees t;
-    val vs = fs ~~ (0 upto (length fs - 1));
+    val vs = map_index swap fs;
     val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t))));
   in Thm.cterm_of thy res end
 end;
--- a/src/HOL/Decision_Procs/MIR.thy	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Thu Oct 22 15:20:54 2009 +0200
@@ -5898,7 +5898,7 @@
     val thy = Thm.theory_of_cterm ct;
     val t = Thm.term_of ct;
     val fs = OldTerm.term_frees t;
-    val vs = fs ~~ (0 upto (length fs - 1));
+    val vs = map_index swap fs;
     val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe};
     val t' = (term_of_fm vs o qe o fm_of_term vs) t;
   in (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
--- a/src/HOL/Finite_Set.thy	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Oct 22 15:20:54 2009 +0200
@@ -162,9 +162,9 @@
   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"
+  let ?f = "the_inv_into {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])
+    by (fold bij_betw_def) (rule bij_betw_the_inv_into[OF bij])
   thus ?thesis by blast
 qed
 
--- a/src/HOL/Fun.thy	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Fun.thy	Thu Oct 22 15:20:54 2009 +0200
@@ -508,65 +508,65 @@
 
 subsection {* Inversion of injective functions *}
 
-definition the_inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where
-"the_inv_onto A f == %x. THE y. y : A & f y = x"
+definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
+"the_inv_into A f == %x. THE y. y : A & f y = x"
 
-lemma the_inv_onto_f_f:
-  "[| inj_on f A;  x : A |] ==> the_inv_onto A f (f x) = x"
-apply (simp add: the_inv_onto_def inj_on_def)
+lemma the_inv_into_f_f:
+  "[| inj_on f A;  x : A |] ==> the_inv_into A f (f x) = x"
+apply (simp add: the_inv_into_def inj_on_def)
 apply (blast intro: the_equality)
 done
 
-lemma f_the_inv_onto_f:
-  "inj_on f A ==> y : f`A  ==> f (the_inv_onto A f y) = y"
-apply (simp add: the_inv_onto_def)
+lemma f_the_inv_into_f:
+  "inj_on f A ==> y : f`A  ==> f (the_inv_into A f y) = y"
+apply (simp add: the_inv_into_def)
 apply (rule the1I2)
  apply(blast dest: inj_onD)
 apply blast
 done
 
-lemma the_inv_onto_into:
-  "[| inj_on f A; x : f ` A; A <= B |] ==> the_inv_onto A f x : B"
-apply (simp add: the_inv_onto_def)
+lemma the_inv_into_into:
+  "[| inj_on f A; x : f ` A; A <= B |] ==> the_inv_into A f x : B"
+apply (simp add: the_inv_into_def)
 apply (rule the1I2)
  apply(blast dest: inj_onD)
 apply blast
 done
 
-lemma the_inv_onto_onto[simp]:
-  "inj_on f A ==> the_inv_onto A f ` (f ` A) = A"
-by (fast intro:the_inv_onto_into the_inv_onto_f_f[symmetric])
+lemma the_inv_into_onto[simp]:
+  "inj_on f A ==> the_inv_into A f ` (f ` A) = A"
+by (fast intro:the_inv_into_into the_inv_into_f_f[symmetric])
 
-lemma the_inv_onto_f_eq:
-  "[| inj_on f A; f x = y; x : A |] ==> the_inv_onto A f y = x"
+lemma the_inv_into_f_eq:
+  "[| inj_on f A; f x = y; x : A |] ==> the_inv_into A f y = x"
   apply (erule subst)
-  apply (erule the_inv_onto_f_f, assumption)
+  apply (erule the_inv_into_f_f, assumption)
   done
 
-lemma the_inv_onto_comp:
+lemma the_inv_into_comp:
   "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
-  the_inv_onto A (f o g) x = (the_inv_onto A g o the_inv_onto (g ` A) f) x"
-apply (rule the_inv_onto_f_eq)
+  the_inv_into A (f o g) x = (the_inv_into A g o the_inv_into (g ` A) f) x"
+apply (rule the_inv_into_f_eq)
   apply (fast intro: comp_inj_on)
- apply (simp add: f_the_inv_onto_f the_inv_onto_into)
-apply (simp add: the_inv_onto_into)
+ apply (simp add: f_the_inv_into_f the_inv_into_into)
+apply (simp add: the_inv_into_into)
 done
 
-lemma inj_on_the_inv_onto:
-  "inj_on f A \<Longrightarrow> inj_on (the_inv_onto A f) (f ` A)"
-by (auto intro: inj_onI simp: image_def the_inv_onto_f_f)
+lemma inj_on_the_inv_into:
+  "inj_on f A \<Longrightarrow> inj_on (the_inv_into A f) (f ` A)"
+by (auto intro: inj_onI simp: image_def the_inv_into_f_f)
 
-lemma bij_betw_the_inv_onto:
-  "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_onto A f) B A"
-by (auto simp add: bij_betw_def inj_on_the_inv_onto the_inv_onto_into)
+lemma bij_betw_the_inv_into:
+  "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_into A f) B A"
+by (auto simp add: bij_betw_def inj_on_the_inv_into the_inv_into_into)
 
 abbreviation the_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
-  "the_inv f \<equiv> the_inv_onto UNIV f"
+  "the_inv f \<equiv> the_inv_into UNIV f"
 
 lemma the_inv_f_f:
   assumes "inj f"
   shows "the_inv f (f x) = x" using assms UNIV_I
-  by (rule the_inv_onto_f_f)
+  by (rule the_inv_into_f_f)
 
 
 subsection {* Proof tool setup *} 
--- a/src/HOL/Hilbert_Choice.thy	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Thu Oct 22 15:20:54 2009 +0200
@@ -31,11 +31,11 @@
      in Syntax.const "_Eps" $ x $ t end)]
 *}
 
-definition inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where
-"inv_onto A f == %x. SOME y. y : A & f y = x"
+definition inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
+"inv_into A f == %x. SOME y. y : A & f y = x"
 
 abbreviation inv :: "('a => 'b) => ('b => 'a)" where
-"inv == inv_onto UNIV"
+"inv == inv_into UNIV"
 
 
 subsection {*Hilbert's Epsilon-operator*}
@@ -92,40 +92,40 @@
 subsection {*Function Inverse*}
 
 lemma inv_def: "inv f = (%y. SOME x. f x = y)"
-by(simp add: inv_onto_def)
+by(simp add: inv_into_def)
 
-lemma inv_onto_into: "x : f ` A ==> inv_onto A f x : A"
-apply (simp add: inv_onto_def)
+lemma inv_into_into: "x : f ` A ==> inv_into A f x : A"
+apply (simp add: inv_into_def)
 apply (fast intro: someI2)
 done
 
 lemma inv_id [simp]: "inv id = id"
-by (simp add: inv_onto_def id_def)
+by (simp add: inv_into_def id_def)
 
-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)
+lemma inv_into_f_f [simp]:
+  "[| inj_on f A;  x : A |] ==> inv_into A f (f x) = x"
+apply (simp add: inv_into_def inj_on_def)
 apply (blast intro: someI2)
 done
 
 lemma inv_f_f: "inj f ==> inv f (f x) = x"
-by (simp add: inv_onto_f_f)
+by (simp add: inv_into_f_f)
 
-lemma f_inv_onto_f: "y : f`A  ==> f (inv_onto A f y) = y"
-apply (simp add: inv_onto_def)
+lemma f_inv_into_f: "y : f`A  ==> f (inv_into A f y) = y"
+apply (simp add: inv_into_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"
+lemma inv_into_f_eq: "[| inj_on f A; x : A; f x = y |] ==> inv_into A f y = x"
 apply (erule subst)
-apply (fast intro: inv_onto_f_f)
+apply (fast intro: inv_into_f_f)
 done
 
 lemma inv_f_eq: "[| inj f; f x = y |] ==> inv f y = x"
-by (simp add:inv_onto_f_eq)
+by (simp add:inv_into_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)
+by (blast intro: ext inv_into_f_eq)
 
 text{*But is it useful?*}
 lemma inj_transfer:
@@ -134,12 +134,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_onto_f_f [OF injf])
+  thus "P x" by (simp add: inv_into_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_onto_f_f)
+apply (blast intro: inj_on_inverseI inv_into_f_f)
 done
 
 lemma inv_o_cancel[simp]: "inj f ==> inv f o f = id"
@@ -148,34 +148,34 @@
 lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g"
 by (simp add: o_assoc[symmetric])
 
-lemma inv_onto_image_cancel[simp]:
-  "inj_on f A ==> S <= A ==> inv_onto A f ` f ` S = S"
+lemma inv_into_image_cancel[simp]:
+  "inj_on f A ==> S <= A ==> inv_into 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_onto_f_f)
+by (blast intro: surjI inv_into_f_f)
 
 lemma surj_f_inv_f: "surj f ==> f(inv f y) = y"
-by (simp add: f_inv_onto_f surj_range)
+by (simp add: f_inv_into_f surj_range)
 
-lemma inv_onto_injective:
-  assumes eq: "inv_onto A f x = inv_onto A f y"
+lemma inv_into_injective:
+  assumes eq: "inv_into A f x = inv_into A f y"
       and x: "x: f`A"
       and y: "y: f`A"
   shows "x=y"
 proof -
-  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)
+  have "f (inv_into A f x) = f (inv_into A f y)" using eq by simp
+  thus ?thesis by (simp add: f_inv_into_f x y)
 qed
 
-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 inj_on_inv_into: "B <= f`A ==> inj_on (inv_into A f) B"
+by (blast intro: inj_onI dest: inv_into_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 bij_betw_inv_into: "bij_betw f A B ==> bij_betw (inv_into A f) B A"
+by (auto simp add: bij_betw_def inj_on_inv_into)
 
 lemma surj_imp_inj_inv: "surj f ==> inj (inv f)"
-by (simp add: inj_on_inv_onto surj_range)
+by (simp add: inj_on_inv_into surj_range)
 
 lemma surj_iff: "(surj f) = (f o inv f = id)"
 apply (simp add: o_def expand_fun_eq)
@@ -193,7 +193,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_onto_def)
+apply (auto simp add: inv_into_def)
 done
 
 lemma inv_inv_eq: "bij f ==> inv (inv f) = f"
@@ -208,13 +208,13 @@
     inv(inv f)=f all fail.
 **)
 
-lemma inv_onto_comp:
+lemma inv_into_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)
+  inv_into A (f o g) x = (inv_into A g o inv_into (g ` A) f) x"
+apply (rule inv_into_f_eq)
   apply (fast intro: comp_inj_on)
- apply (simp add: inv_onto_into)
-apply (simp add: f_inv_onto_f inv_onto_into)
+ apply (simp add: inv_into_into)
+apply (simp add: f_inv_into_f inv_into_into)
 done
 
 lemma o_inv_distrib: "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f"
@@ -239,7 +239,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_onto_f_f, symmetric])
+apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
 done
 
 lemma finite_fun_UNIVD1:
@@ -256,7 +256,7 @@
   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_onto_def)
+    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_into_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
--- a/src/HOL/Library/FuncSet.thy	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Library/FuncSet.thy	Thu Oct 22 15:20:54 2009 +0200
@@ -190,20 +190,20 @@
       !!x. x\<in>A ==> f x = g x |] ==> f = g"
 by (force simp add: expand_fun_eq extensional_def)
 
-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 inv_into_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_into A f x) : B -> A"
+by (unfold inv_into_def) (fast intro: someI2)
 
-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)"
+lemma compose_inv_into_id:
+  "bij_betw f A B ==> compose A (\<lambda>y\<in>B. inv_into A f y) f = (\<lambda>x\<in>A. x)"
 apply (simp add: bij_betw_def compose_def)
 apply (rule restrict_ext, auto)
 done
 
-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)"
+lemma compose_id_inv_into:
+  "f ` A = B ==> compose B f (\<lambda>y\<in>B. inv_into A f y) = (\<lambda>x\<in>B. x)"
 apply (simp add: compose_def)
 apply (rule restrict_ext)
-apply (simp add: f_inv_onto_f)
+apply (simp add: f_inv_into_f)
 done
 
 
--- a/src/HOL/Library/Permutations.thy	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Library/Permutations.thy	Thu Oct 22 15:20:54 2009 +0200
@@ -83,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_onto_def apply auto
+  unfolding permutes_def inv_def apply auto
   apply (erule allE[where x=y])
   apply (erule allE[where x=y])
   apply (rule someI_ex) apply blast
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -967,8 +967,8 @@
  else if d = 0 then [FuncUtil.Ctermfunc.empty]
  else if null vars then [monomial_1] else
  let val alts =
-  map (fn k => let val oths = enumerate_monomials (d - k) (tl vars)
-               in map (fn ks => if k = 0 then ks else FuncUtil.Ctermfunc.update (hd vars, k) ks) oths end) (0 upto d)
+  map_range (fn k => let val oths = enumerate_monomials (d - k) (tl vars)
+               in map (fn ks => if k = 0 then ks else FuncUtil.Ctermfunc.update (hd vars, k) ks) oths end) (d + 1)
  in flat alts
  end;
 
@@ -1204,9 +1204,9 @@
    val eq0 = map (poly_of_term o Thm.dest_arg1 o concl) eqs
    val le0 = map (poly_of_term o Thm.dest_arg o concl) les
    val lt0 = map (poly_of_term o Thm.dest_arg o concl) lts
-   val eqp0 = map (fn (t,i) => (t,RealArith.Axiom_eq i)) (eq0 ~~ (0 upto (length eq0 - 1)))
-   val lep0 = map (fn (t,i) => (t,RealArith.Axiom_le i)) (le0 ~~ (0 upto (length le0 - 1)))
-   val ltp0 = map (fn (t,i) => (t,RealArith.Axiom_lt i)) (lt0 ~~ (0 upto (length lt0 - 1)))
+   val eqp0 = map_index (fn (i, t) => (t,RealArith.Axiom_eq i)) eq0
+   val lep0 = map_index (fn (i, t) => (t,RealArith.Axiom_le i)) le0
+   val ltp0 = map_index (fn (i, t) => (t,RealArith.Axiom_lt i)) lt0
    val (keq,eq) = List.partition (fn (p,_) => multidegree p = 0) eqp0
    val (klep,lep) = List.partition (fn (p,_) => multidegree p = 0) lep0
    val (kltp,ltp) = List.partition (fn (p,_) => multidegree p = 0) ltp0
--- a/src/HOL/Library/positivstellensatz.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -643,9 +643,9 @@
 
   fun linear_prover (eq,le,lt) = 
    let 
-    val eqs = map2 (fn p => fn n => (p,Axiom_eq n)) eq (0 upto (length eq - 1))
-    val les = map2 (fn p => fn n => (p,Axiom_le n)) le (0 upto (length le - 1))
-    val lts = map2 (fn p => fn n => (p,Axiom_lt n)) lt (0 upto (length lt - 1))
+    val eqs = map_index (fn (n, p) => (p,Axiom_eq n)) eq
+    val les = map_index (fn (n, p) => (p,Axiom_le n)) le
+    val lts = map_index (fn (n, p) => (p,Axiom_lt n)) lt
    in linear_eqs(eqs,les,lts)
    end 
   
--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -102,7 +102,7 @@
 (**** make datatype info ****)
 
 fun make_dt_info descr sorts induct reccomb_names rec_thms
-    (((i, (_, (tname, _, _))), distinct), inject) =
+    (i, (((_, (tname, _, _)), distinct), inject)) =
   (tname,
    {index = i,
     descr = descr,
@@ -2045,8 +2045,8 @@
       end) (rec_eq_prems ~~
         DatatypeProp.make_primrecs new_type_names descr' sorts thy12);
 
-    val dt_infos = map (make_dt_info pdescr sorts induct reccomb_names rec_thms)
-      ((0 upto length descr1 - 1) ~~ descr1 ~~ distinct_thms ~~ inject_thms);
+    val dt_infos = map_index (make_dt_info pdescr sorts induct reccomb_names rec_thms)
+      (descr1 ~~ distinct_thms ~~ inject_thms);
 
     (* FIXME: theorems are stored in database for testing only *)
     val (_, thy13) = thy12 |>
--- a/src/HOL/SizeChange/Correctness.thy	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/SizeChange/Correctness.thy	Thu Oct 22 15:20:54 2009 +0200
@@ -1146,7 +1146,7 @@
   assumes "finite S" 
   shows "set (set2list S) = S"
   unfolding set2list_def 
-proof (rule f_inv_onto_f)
+proof (rule f_inv_into_f)
   from `finite S` have "\<exists>l. set l = S"
     by (rule finite_list)
   thus "S \<in> range set"
--- a/src/HOL/SizeChange/sct.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/SizeChange/sct.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -156,9 +156,9 @@
 val mk_number = HOLogic.mk_nat
 val dest_number = HOLogic.dest_nat
 
-fun nums_to i = map mk_number (0 upto (i - 1))
+fun nums_to i = map_range mk_number i
 
-val nth_simps = [thm "List.nth_Cons_0", thm "List.nth_Cons_Suc"]
+val nth_simps = [@{thm List.nth_Cons_0}, @{thm List.nth_Cons_Suc}]
 val nth_ss = (HOL_basic_ss addsimps nth_simps)
 val simp_nth_tac = simp_tac nth_ss
 
@@ -166,7 +166,7 @@
 fun tabulate_tlist thy l =
     let
       val n = length (HOLogic.dest_list l)
-      val table = Inttab.make (map (fn i => (i, Simplifier.rewrite nth_ss (cterm_of thy (mk_nth l $ mk_number i)))) (0 upto n - 1))
+      val table = Inttab.make (map_range (fn i => (i, Simplifier.rewrite nth_ss (cterm_of thy (mk_nth l $ mk_number i)))) n)
     in
       the o Inttab.lookup table
     end
@@ -250,7 +250,7 @@
 
           val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2)
 
-          val tac = (EVERY (map (fn n => EVERY (map (set_m1 n) (0 upto M - 1))) (0 upto N - 1)))
+          val tac = (EVERY (map_range (fn n => EVERY (map_range (set_m1 n) M)) N))
                       THEN (rtac approx_empty 1)
 
           val approx_thm = goal
--- a/src/HOL/String.thy	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/String.thy	Thu Oct 22 15:20:54 2009 +0200
@@ -48,7 +48,7 @@
 
 setup {*
 let
-  val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
+  val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
   val thms = map_product
    (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
       nibbles nibbles;
--- a/src/HOL/Tools/Datatype/datatype.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -26,7 +26,6 @@
   val info_of_constr : theory -> string * typ -> info option
   val info_of_case : theory -> string -> info option
   val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
-  val distinct_simproc : simproc
   val make_case :  Proof.context -> DatatypeCase.config -> string list -> term ->
     (term * term) list -> term * (term * (int * bool)) list
   val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
@@ -159,49 +158,6 @@
 
 (** various auxiliary **)
 
-(* simplification procedure for showing distinctness of constructors *)
-
-fun stripT (i, Type ("fun", [_, T])) = stripT (i + 1, T)
-  | stripT p = p;
-
-fun stripC (i, f $ x) = stripC (i + 1, f)
-  | stripC p = p;
-
-val distinctN = "constr_distinct";
-
-fun distinct_rule thy ss tname eq_t = Goal.prove (Simplifier.the_context ss) [] [] eq_t
-  (K (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
-    atac 2, resolve_tac (#distinct (the_info thy tname)) 1, etac FalseE 1]));
-
-fun get_constr thy dtco =
-  get_info thy dtco
-  |> Option.map (fn { descr, index, ... } => (#3 o the o AList.lookup (op =) descr) index);
-
-fun distinct_proc thy ss (t as Const ("op =", _) $ t1 $ t2) =
-  (case (stripC (0, t1), stripC (0, t2)) of
-     ((i, Const (cname1, T1)), (j, Const (cname2, T2))) =>
-         (case (stripT (0, T1), stripT (0, T2)) of
-            ((i', Type (tname1, _)), (j', Type (tname2, _))) =>
-                if tname1 = tname2 andalso not (cname1 = cname2) andalso i = i' andalso j = j' then
-                   (case get_constr thy tname1 of
-                      SOME constrs => let val cnames = map fst constrs
-                        in if cname1 mem cnames andalso cname2 mem cnames then
-                             SOME (distinct_rule thy ss tname1
-                               (Logic.mk_equals (t, HOLogic.false_const)))
-                           else NONE
-                        end
-                    | NONE => NONE)
-                else NONE
-          | _ => NONE)
-   | _ => NONE)
-  | distinct_proc _ _ _ = NONE;
-
-val distinct_simproc =
-  Simplifier.simproc @{theory HOL} distinctN ["s = t"] distinct_proc;
-
-val simproc_setup =
-  Simplifier.map_simpset (fn ss => ss addsimprocs [distinct_simproc]);
-
 (* prepare datatype specifications *)
 
 fun read_typ thy ((Ts, sorts), str) =
@@ -271,7 +227,8 @@
     [("_case_syntax", DatatypeCase.case_tr true info_of_constr)],
     [], []);
 
-(* document antiquotation *)
+
+(** document antiquotation **)
 
 val _ = ThyOutput.antiquotation "datatype" Args.tyname
   (fn {source = src, context = ctxt, ...} => fn dtco =>
@@ -593,4 +550,3 @@
 end;
 
 end;
-
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -56,7 +56,7 @@
     val {maxidx, ...} = rep_thm induct;
     val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
 
-    fun prove_casedist_thm ((i, t), T) =
+    fun prove_casedist_thm (i, (T, t)) =
       let
         val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) =>
           Abs ("z", T', Const ("True", T''))) induct_Ps;
@@ -77,8 +77,8 @@
              REPEAT (rtac TrueI 1)])
       end;
 
-    val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~
-      (DatatypeProp.make_casedists descr sorts) ~~ newTs)
+    val casedist_thms = map_index prove_casedist_thm
+      (newTs ~~ DatatypeProp.make_casedists descr sorts)
   in
     thy
     |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -481,7 +481,7 @@
 
     val Abs_inverse_thms' =
       map #1 newT_iso_axms @
-      map2 (fn r_inj => fn r => @{thm f_the_inv_onto_f} OF [r_inj, r RS mp])
+      map2 (fn r_inj => fn r => @{thm f_the_inv_into_f} OF [r_inj, r RS mp])
         iso_inj_thms_unfolded iso_thms;
 
     val Abs_inverse_thms = maps (mk_funs_inv thy5) Abs_inverse_thms';
@@ -571,7 +571,7 @@
         val Abs_t = if i < length newTs then
             Const (Sign.intern_const thy6
               ("Abs_" ^ (nth new_type_names i)), Univ_elT --> T)
-          else Const (@{const_name the_inv_onto},
+          else Const (@{const_name the_inv_into},
               [HOLogic.mk_setT T, T --> Univ_elT, Univ_elT] ---> T) $
             HOLogic.mk_UNIV T $ Const (nth all_rep_names i, T --> Univ_elT)
 
--- a/src/HOL/Tools/Function/induction_scheme.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Tools/Function/induction_scheme.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -363,7 +363,7 @@
 
     val ineqss = mk_ineqs R scheme
                    |> map (map (pairself (assume o cert)))
-    val complete = map (mk_completeness ctxt scheme #> cert #> assume) (0 upto (length branches - 1))
+    val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
     val wf_thm = mk_wf ctxt R scheme |> cert |> assume
 
     val (descent, pres) = split_list (flat ineqss)
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -119,7 +119,7 @@
         G (p, q, edges)
       end
   in
-    GP (map arity (0 upto n - 1), map mk_graph cs)
+    GP (map_range arity n, map mk_graph cs)
   end
 
 (* General reduction pair application *)
@@ -312,8 +312,8 @@
 fun print_error ctxt D = CALLS (fn (cs, i) =>
   let
     val np = get_num_points D
-    val ms = map (get_measures D) (0 upto np - 1)
-    val tys = map (get_types D) (0 upto np - 1)
+    val ms = map_range (get_measures D) np
+    val tys = map_range (get_types D) np
     fun index xs = (1 upto length xs) ~~ xs
     fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
     val ims = index (map index ms)
--- a/src/HOL/Tools/Function/scnp_solve.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_solve.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -63,8 +63,8 @@
                        /  \  f i
                       0<=i<n
  *)
-fun iforall n f = all (map f (0 upto n - 1))
-fun iexists n f = PropLogic.exists (map f (0 upto n - 1))
+fun iforall n f = all (map_range f n)
+fun iexists n f = PropLogic.exists (map_range f n)
 fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
 
 fun the_one var n x = all (var x :: map (Not o var) (remove (op =) x (0 upto n - 1)))
@@ -221,7 +221,7 @@
       let fun prog_pt_mapping p =
             map_filter (fn x => if assign (P(p, x)) then SOME (x, assignTag p x) else NONE)
               (0 upto (arity gp p) - 1)
-      in map prog_pt_mapping (0 upto num_prog_pts gp - 1) end
+      in map_range prog_pt_mapping (num_prog_pts gp) end
 
     val strict_list = filter (assign o STRICT) (0 upto num_graphs gp - 1)
 
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -312,7 +312,7 @@
 (* Overall function.                                                         *)
 
 fun grobner pols =
-    let val npols = map2 (fn p => fn n => (p,Start n)) pols (0 upto (length pols - 1))
+    let val npols = map_index (fn (n, p) => (p, Start n)) pols
         val phists = filter (fn (p,_) => not (null p)) npols
         val bas = grobner_interreduce [] (map monic phists)
         val prs0 = map_product pair bas bas
@@ -802,8 +802,8 @@
   val pols = map (grobify_term vars) tms
   val pol = grobify_term vars tm
   val cert = grobner_ideal vars pols pol
- in map (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars)
-        (0 upto (length pols - 1))
+ in map_range (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars)
+   (length pols)
  end
 
 fun poly_eq_conv t = 
--- a/src/HOL/Tools/TFL/tfl.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -54,8 +54,6 @@
 
 val list_mk_type = U.end_itlist (curry (op -->));
 
-fun enumerate xs = ListPair.zip(xs, 0 upto (length xs - 1));
-
 fun front_last [] = raise TFL_ERR "front_last" "empty list"
   | front_last [x] = ([],x)
   | front_last (h::t) =
@@ -328,7 +326,7 @@
      val (fname,ftype) = dest_atom atom
      val dummy = map (no_repeat_vars thy) pats
      val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
-                              map (fn (t,i) => (t,(i,true))) (enumerate R))
+                              map_index (fn (i, t) => (t,(i,true))) R)
      val names = List.foldr OldTerm.add_term_names [] R
      val atype = type_of(hd pats)
      and aname = Name.variant names "a"
--- a/src/HOL/Tools/inductive_codegen.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -625,7 +625,7 @@
 fun conv_ntuple fs ts p =
   let
     val k = length fs;
-    val xs = map (fn i => str ("x" ^ string_of_int i)) (0 upto k);
+    val xs = map_range (fn i => str ("x" ^ string_of_int i)) (k + 1);
     val xs' = map (fn Bound i => nth xs (k - i)) ts;
     fun conv xs js =
       if js mem fs then
--- a/src/HOL/Tools/record.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Tools/record.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -1894,8 +1894,8 @@
             more;
       in
         if more = HOLogic.unit
-        then build (map recT (0 upto parent_len))
-        else build (map rec_schemeT (0 upto parent_len))
+        then build (map_range recT (parent_len + 1))
+        else build (map_range rec_schemeT (parent_len + 1))
       end;
 
     val r_rec0 = mk_rec all_vars_more 0;
--- a/src/HOL/Tools/refute.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/Tools/refute.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -2618,8 +2618,7 @@
                           "unexpected size of IDT (wrong type associated?)")
                       else ()
                   (* interpretation *)
-                  val rec_op = Node (map (compute_array_entry idt_index)
-                    (0 upto (idt_size - 1)))
+                  val rec_op = Node (map_range (compute_array_entry idt_index) idt_size)
                 in
                   SOME (rec_op, model', args')
                 end
@@ -2784,8 +2783,8 @@
                 (replicate (size_of_nat - element - 1) False))
           end
       in
-        SOME (Node (map (fn m => Node (map (plus m) (0 upto size_of_nat-1)))
-          (0 upto size_of_nat-1)), model, args)
+        SOME (Node (map_range (fn m => Node (map_range (plus m) size_of_nat)) size_of_nat),
+          model, args)
       end
     | _ =>
       NONE;
@@ -2812,8 +2811,8 @@
               (replicate (size_of_nat - element - 1) False))
           end
       in
-        SOME (Node (map (fn m => Node (map (minus m) (0 upto size_of_nat-1)))
-          (0 upto size_of_nat-1)), model, args)
+        SOME (Node (map_range (fn m => Node (map_range (minus m) size_of_nat)) size_of_nat),
+          model, args)
       end
     | _ =>
       NONE;
@@ -2843,8 +2842,8 @@
                 (replicate (size_of_nat - element - 1) False))
           end
       in
-        SOME (Node (map (fn m => Node (map (mult m) (0 upto size_of_nat-1)))
-          (0 upto size_of_nat-1)), model, args)
+        SOME (Node (map_range (fn m => Node (map_range (mult m) size_of_nat)) size_of_nat),
+          model, args)
       end
     | _ =>
       NONE;
--- a/src/HOL/UNITY/Extend.thy	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/UNITY/Extend.thy	Thu Oct 22 15:20:54 2009 +0200
@@ -121,7 +121,7 @@
      assumes surj_h: "surj h"
          and prem:   "!! x y. g (h(x,y)) = x"
      shows "fst (inv h z) = g z"
-by (metis UNIV_I f_inv_onto_f pair_collapse prem surj_h surj_range)
+by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h surj_range)
 
 
 subsection{*Trivial properties of f, g, h*}
--- a/src/HOL/ZF/HOLZF.thy	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/ZF/HOLZF.thy	Thu Oct 22 15:20:54 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_onto_f)
+  apply (rule_tac f_inv_into_f)
   apply (auto simp add: image_def Nat_def Sep)
   done
 
--- a/src/HOL/ZF/Zet.thy	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/ZF/Zet.thy	Thu Oct 22 15:20:54 2009 +0200
@@ -35,7 +35,7 @@
 
 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_onto A f))" in exI)
+  apply (rule_tac x="Repl z (g o (inv_into A f))" in exI)
   apply (simp add: explode_Repl_eq)
   apply (subgoal_tac "explode z = f ` A")
   apply (simp_all add: comp_image_eq)
@@ -49,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_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)
+  let ?w = "f o (inv_into A g)"
+  have subset: "(inv_into A g) ` (g ` A) \<subseteq> A"
+    by (auto simp add: inv_into_into)
+  have "inj_on (inv_into A g) (g ` A)" by (simp add: inj_on_inv_into)
   then have injw: "inj_on ?w (g ` A)"
     apply (rule comp_inj_on)
     apply (rule subset_inj_on[where B=A])
@@ -86,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_onto_f[where y="Rep_zet A"])
+  apply (subst f_inv_into_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	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/HOL/ex/set.thy	Thu Oct 22 15:20:54 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_onto)
+    apply (rule_tac [2] inj_on_inv_into)
     apply (erule subset_inj_on [OF _ subset_UNIV])
    apply blast
   apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
--- a/src/Provers/order.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/Provers/order.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -731,9 +731,6 @@
  in u :: dfs_visit g u end;
 
 
-fun indexComps components =
-    ListPair.map (fn (a,b) => (a,b)) (0 upto (length components -1), components);
-
 fun indexNodes IndexComp =
     maps (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp;
 
@@ -1109,7 +1106,7 @@
 |   mk_sccGraphs components leqG neqG ntc =
     let
     (* Liste (Index der Komponente, Komponente *)
-    val IndexComp = indexComps components;
+    val IndexComp = map_index I components;
 
 
     fun handleContr edge g =
@@ -1211,7 +1208,7 @@
  let
   val (leqG, neqG, neqE) = mkGraphs asms
   val components = scc_term leqG
-  val ntc = indexNodes (indexComps components)
+  val ntc = indexNodes (map_index I components)
   val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc
  in
    let
--- a/src/Provers/quasi.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/Provers/quasi.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -118,8 +118,8 @@
 (*                                                                          *)
 (* ************************************************************************ *)
 
-fun mkasm_trans sign (t, n) =
-  case Less.decomp_trans sign t of
+fun mkasm_trans thy (t, n) =
+  case Less.decomp_trans thy t of
     SOME (x, rel, y) =>
     (case rel of
      "<="  =>  [Le (x, y, Asm n)]
@@ -137,8 +137,8 @@
 (*                                                                          *)
 (* ************************************************************************ *)
 
-fun mkasm_quasi sign (t, n) =
-  case Less.decomp_quasi sign t of
+fun mkasm_quasi thy (t, n) =
+  case Less.decomp_quasi thy t of
     SOME (x, rel, y) => (case rel of
       "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE))
                else [Less (x, y, Asm n)]
@@ -164,8 +164,8 @@
 (* ************************************************************************ *)
 
 
-fun mkconcl_trans sign t =
-  case Less.decomp_trans sign t of
+fun mkconcl_trans thy t =
+  case Less.decomp_trans thy t of
     SOME (x, rel, y) => (case rel of
      "<="  => (Le (x, y, Asm ~1), Asm 0)
     | _  => raise Cannot)
@@ -181,8 +181,8 @@
 (*                                                                          *)
 (* ************************************************************************ *)
 
-fun mkconcl_quasi sign t =
-  case Less.decomp_quasi sign t of
+fun mkconcl_quasi thy t =
+  case Less.decomp_quasi thy t of
     SOME (x, rel, y) => (case rel of
       "<"   => ([Less (x, y, Asm ~1)], Asm 0)
     | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
@@ -503,12 +503,12 @@
 (*                                                                         *)
 (* *********************************************************************** *)
 
-fun solveLeTrans sign (asms, concl) =
+fun solveLeTrans thy (asms, concl) =
  let
   val g = mkGraph asms
  in
    let
-    val (subgoal, prf) = mkconcl_trans sign concl
+    val (subgoal, prf) = mkconcl_trans thy concl
     val (found, path) = findPath (lower subgoal) (upper subgoal) g
    in
     if found then [getprf (transPath (tl path, hd path))]
@@ -526,12 +526,12 @@
 (*                                                                         *)
 (* *********************************************************************** *)
 
-fun solveQuasiOrder sign (asms, concl) =
+fun solveQuasiOrder thy (asms, concl) =
  let
   val (leG, neqE) = mkQuasiGraph asms
  in
    let
-   val (subgoals, prf) = mkconcl_quasi sign concl
+   val (subgoals, prf) = mkconcl_quasi thy concl
    fun solve facts less =
        (case triv_solv less of NONE => findQuasiProof (leG, neqE) less
        | SOME prf => prf )
@@ -555,7 +555,7 @@
   val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
   val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
-  val lesss = flat (ListPair.map (mkasm_trans thy) (Hs, 0 upto (length Hs - 1)));
+  val lesss = flat (map_index (mkasm_trans thy o swap) Hs);
   val prfs = solveLeTrans thy (lesss, C);
 
   val (subgoal, prf) = mkconcl_trans thy C;
@@ -576,7 +576,7 @@
   val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
   val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
-  val lesss = flat (ListPair.map (mkasm_quasi thy) (Hs, 0 upto (length Hs - 1)));
+  val lesss = flat (map_index (mkasm_quasi thy o swap) Hs);
   val prfs = solveQuasiOrder thy (lesss, C);
   val (subgoals, prf) = mkconcl_quasi thy C;
  in
--- a/src/Provers/trancl.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/Provers/trancl.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -538,7 +538,7 @@
   val C = Logic.strip_assums_concl A;
   val (rel, subgoals, prf) = mkconcl_trancl C;
 
-  val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)));
+  val prems = flat (map_index (mkasm_trancl rel o swap) Hs);
   val prfs = solveTrancl (prems, C);
  in
   Subgoal.FOCUS (fn {prems, ...} =>
@@ -555,7 +555,7 @@
   val C = Logic.strip_assums_concl A;
   val (rel, subgoals, prf) = mkconcl_rtrancl C;
 
-  val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)));
+  val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs);
   val prfs = solveRtrancl (prems, C);
  in
   Subgoal.FOCUS (fn {prems, ...} =>
--- a/src/Pure/Syntax/parser.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/Pure/Syntax/parser.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -840,7 +840,7 @@
 
 fun guess_infix_lr (Gram gram) c = (*based on educated guess*)
   let
-    fun freeze a = map (curry Array.sub a) (0 upto Array.length a - 1);
+    fun freeze a = map_range (curry Array.sub a) (Array.length a);
     val prods = maps snd (maps snd (freeze (#prods gram)));
     fun guess (SOME ([Nonterminal (_, k), Terminal (Token (Literal, s, _)), Nonterminal (_, l)], _, j)) =
           if k = j andalso l = j + 1 then SOME (s, true, false, j)
--- a/src/Pure/axclass.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/Pure/axclass.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -364,12 +364,11 @@
       |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
       |> (map o apsnd o map_atyps) (K T);
     val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
-    val th' = Drule.unconstrainTs th;
   in
     thy
     |> fold (snd oo declare_overloaded) missing_params
     |> Sign.primitive_arity (t, Ss, [c])
-    |> put_arity ((t, Ss, c), th')
+    |> put_arity ((t, Ss, c), Thm.close_derivation (Drule.unconstrainTs th))
   end;
 
 
--- a/src/Pure/library.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/Pure/library.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -89,6 +89,7 @@
   val nth_list: 'a list list -> int -> 'a list
   val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
   val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
+  val map_range: (int -> 'a) -> int -> 'a list
   val split_last: 'a list -> 'a list * 'a
   val find_index: ('a -> bool) -> 'a list -> int
   val find_first: ('a -> bool) -> 'a list -> 'a option
@@ -463,6 +464,12 @@
       | fold_aux i (x :: xs) y = fold_aux (i + 1) xs (f (i, x) y);
   in fold_aux 0 end;
 
+fun map_range f i =
+  let
+    fun mapp k =
+      if k < i then f k :: mapp (k + 1) else [];
+  in mapp 0 end;
+
 val last_elem = List.last;
 
 (*rear decomposition*)
--- a/src/Pure/term.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/Pure/term.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -939,7 +939,7 @@
   | free_dummy_patterns a used = (a, used);
 
 fun replace_dummy Ts (Const ("dummy_pattern", T)) i =
-      (list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)), i + 1)
+      (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1)
   | replace_dummy Ts (Abs (x, T, t)) i =
       let val (t', i') = replace_dummy (T :: Ts) t i
       in (Abs (x, T, t'), i') end
--- a/src/Pure/unify.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/Pure/unify.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -531,12 +531,12 @@
   Bound vars in the binder are "banned" unless used in both t AND u *)
 fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) =
   let val loot = loose_bnos t  and  loou = loose_bnos u
-      fun add_index (((a,T), j), (bnos, newbinder)) =
+      fun add_index (j, (a,T)) (bnos, newbinder) =
             if  member (op =) loot j  andalso  member (op =) loou j
             then  (bnos, (a,T)::newbinder)  (*needed by both: keep*)
             else  (j::bnos, newbinder);   (*remove*)
-      val indices = 0 upto (length rbinder - 1);
-      val (banned,rbin') = List.foldr add_index ([],[]) (rbinder~~indices);
+      val (banned,rbin') = fold_rev add_index
+        ((0 upto (length rbinder - 1)) ~~ rbinder) ([],[]);
       val (env', t') = clean_term banned (env, t);
       val (env'',u') = clean_term banned (env',u)
   in  (ff_assign thy (env'', rbin', t', u'), tpairs)
--- a/src/Tools/Code/code_preproc.ML	Wed Oct 21 22:01:44 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML	Thu Oct 22 15:20:54 2009 +0200
@@ -408,9 +408,8 @@
   in Thm.instantiate (insts, []) thm end;
 
 fun add_arity thy vardeps (class, tyco) =
-  AList.default (op =)
-    ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
-      (0 upto Sign.arity_number thy tyco - 1));
+  AList.default (op =) ((class, tyco),
+    map_range (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k)) (Sign.arity_number thy tyco));
 
 fun add_eqs thy vardeps (c, (proto_lhs, proto_eqns)) (rhss, eqngr) =
   if can (Graph.get_node eqngr) c then (rhss, eqngr)