# HG changeset patch # User haftmann # Date 1295599452 -3600 # Node ID 89451110ba8e0dccd9d85f4bc01e8dd135d6688c # Parent 011fcb70e32f433097371abeff78daa75c2a3297 moved theorem diff -r 011fcb70e32f -r 89451110ba8e src/HOL/Finite_Set.thy --- 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 \ f -` {a} \ {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 \ bool" diff -r 011fcb70e32f -r 89451110ba8e src/HOL/Fun.thy --- 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 \ f -` {a} \ {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 \ inj_on f A" by (auto intro!: inj_onI dest: strict_mono_eq) + subsection{*Function Updating*} definition