author haftmann Fri, 21 Jan 2011 09:44:12 +0100 changeset 41657 89451110ba8e parent 41656 011fcb70e32f child 41658 1eef159301df
moved theorem
 src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions src/HOL/Fun.thy file | annotate | diff | comparison | revisions
```--- 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```