--- 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, [])