merged

--- a/src/HOL/Fun.thy	Tue Oct 20 08:10:31 2009 +0200
+++ b/src/HOL/Fun.thy	Tue Oct 20 08:10:47 2009 +0200
@@ -505,36 +505,6 @@
 
 subsection {* Inversion of injective functions *}
 
-definition inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
-  "inv f y = (THE x. f x = y)"
-
-lemma inv_f_f:
-  assumes "inj f"
-  shows "inv f (f x) = x"
-proof -
-  from assms have "(THE x'. f x' = f x) = (THE x'. x' = x)"
-    by (simp add: inj_on_eq_iff)
-  also have "... = x" by (rule the_eq_trivial)
-  finally show ?thesis by (unfold inv_def)
-qed
-
-lemma f_inv_f:
-  assumes "inj f"
-  and "y \<in> range f"
-  shows "f (inv f y) = y"
-proof (unfold inv_def)
-  from `y \<in> range f` obtain x where "y = f x" ..
-  then have "f x = y" ..
-  then show "f (THE x. f x = y) = y"
-  proof (rule theI)
-    fix x' assume "f x' = y"
-    with `f x = y` have "f x' = f x" by simp
-    with `inj f` show "x' = x" by (rule injD)
-  qed
-qed
-
-hide (open) const inv
-
 definition the_inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where
 "the_inv_onto A f == %x. THE y. y : A & f y = x"
 
@@ -587,6 +557,14 @@
   "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)
 
+abbreviation the_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
+  "the_inv f \<equiv> the_inv_onto 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)
+
 
 subsection {* Proof tool setup *} 
 

--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Oct 20 08:10:31 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Oct 20 08:10:47 2009 +0200
@@ -481,7 +481,7 @@
 
     val Abs_inverse_thms' =
       map #1 newT_iso_axms @
-      map2 (fn r_inj => fn r => @{thm f_inv_f} OF [r_inj, r RS mp])
+      map2 (fn r_inj => fn r => @{thm f_the_inv_onto_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';
@@ -560,8 +560,8 @@
     val _ = message config "Proving induction rule for datatypes ...";
 
     val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
-      (map (fn r => r RS @{thm inv_f_f} RS subst) iso_inj_thms_unfolded);
-    val Rep_inverse_thms' = map (fn r => r RS @{thm inv_f_f}) iso_inj_thms_unfolded;
+      (map (fn r => r RS @{thm the_inv_f_f} RS subst) iso_inj_thms_unfolded);
+    val Rep_inverse_thms' = map (fn r => r RS @{thm the_inv_f_f}) iso_inj_thms_unfolded;
 
     fun mk_indrule_lemma ((prems, concls), ((i, _), T)) =
       let
@@ -571,8 +571,9 @@
         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 Fun.inv}, [T --> Univ_elT, Univ_elT] ---> T) $
-            Const (nth all_rep_names i, T --> Univ_elT)
+          else Const (@{const_name the_inv_onto},
+              [HOLogic.mk_setT T, T --> Univ_elT, Univ_elT] ---> T) $
+            HOLogic.mk_UNIV T $ Const (nth all_rep_names i, T --> Univ_elT)
 
       in (prems @ [HOLogic.imp $
             (Const (nth rep_set_names i, UnivT') $ Rep_t) $

--- a/src/HOL/ex/LocaleTest2.thy	Tue Oct 20 08:10:31 2009 +0200
+++ b/src/HOL/ex/LocaleTest2.thy	Tue Oct 20 08:10:47 2009 +0200
@@ -897,7 +897,7 @@
 apply simp
 done
   show "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
-apply (unfold Dmonoid.inv_def [OF Dmonoid] inv_def)
+apply (unfold Dmonoid.inv_def [OF Dmonoid])
 apply (insert unit_id)
 apply simp
 apply (rule the_equality)

--- a/src/Pure/codegen.ML	Tue Oct 20 08:10:31 2009 +0200
+++ b/src/Pure/codegen.ML	Tue Oct 20 08:10:47 2009 +0200
@@ -500,8 +500,6 @@
   let
     val axmss = map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy'))
       (thy :: Theory.ancestors_of thy);
-    fun prep_def def = (case preprocess thy [def] of
-      [def'] => prop_of def' | _ => error "mk_deftab: bad preprocessor");
     fun add_def thyname (name, t) = (case dest_prim_def t of
         NONE => I
       | SOME (s, (T, _)) => Symtab.map_default (s, [])