--- a/src/HOL/Finite_Set.thy Fri Jan 21 09:41:59 2011 +0100
+++ b/src/HOL/Finite_Set.thy Fri Jan 21 09:44:12 2011 +0100
@@ -9,15 +9,6 @@
imports Option Power
begin
--- {* FIXME move *}
-
-lemma inj_vimage_singleton: "inj f \<Longrightarrow> f -` {a} \<subseteq> {THE x. f x = a}"
- -- {* The inverse image of a singleton under an injective function
- is included in a singleton. *}
- apply (auto simp add: inj_on_def)
- apply (blast intro: the_equality [symmetric])
- done
-
subsection {* Predicate for finite sets *}
inductive finite :: "'a set \<Rightarrow> bool"
--- a/src/HOL/Fun.thy Fri Jan 21 09:41:59 2011 +0100
+++ b/src/HOL/Fun.thy Fri Jan 21 09:44:12 2011 +0100
@@ -546,12 +546,20 @@
apply (simp_all (no_asm_simp) add: inj_image_Compl_subset surj_Compl_image_subset)
done
+lemma inj_vimage_singleton: "inj f \<Longrightarrow> f -` {a} \<subseteq> {THE x. f x = a}"
+ -- {* The inverse image of a singleton under an injective function
+ is included in a singleton. *}
+ apply (auto simp add: inj_on_def)
+ apply (blast intro: the_equality [symmetric])
+ done
+
lemma (in ordered_ab_group_add) inj_uminus[simp, intro]: "inj_on uminus A"
by (auto intro!: inj_onI)
lemma (in linorder) strict_mono_imp_inj_on: "strict_mono f \<Longrightarrow> inj_on f A"
by (auto intro!: inj_onI dest: strict_mono_eq)
+
subsection{*Function Updating*}
definition