--- a/src/HOL/Hilbert_Choice.thy Sat Apr 26 13:25:44 2014 +0200
+++ b/src/HOL/Hilbert_Choice.thy Sat Apr 26 13:25:45 2014 +0200
@@ -235,11 +235,11 @@
lemma image_surj_f_inv_f: "surj f ==> f ` (inv f ` A) = A"
by (simp add: image_eq_UN surj_f_inv_f)
-lemma image_inv_f_f: "inj f ==> (inv f) ` (f ` A) = A"
-by (simp add: image_eq_UN)
+lemma image_inv_f_f: "inj f ==> inv f ` (f ` A) = A"
+ by (simp add: image_eq_UN)
-lemma inv_image_comp: "inj f ==> inv f ` (f`X) = X"
-by (auto simp add: image_def)
+lemma inv_image_comp: "inj f ==> inv f ` (f ` X) = X"
+ by (fact image_inv_f_f)
lemma bij_image_Collect_eq: "bij f ==> f ` Collect P = {y. P (inv f y)}"
apply auto
--- a/src/HOL/Library/Finite_Lattice.thy Sat Apr 26 13:25:44 2014 +0200
+++ b/src/HOL/Library/Finite_Lattice.thy Sat Apr 26 13:25:45 2014 +0200
@@ -161,11 +161,8 @@
lemma finite_distrib_lattice_complete_sup_Inf:
"sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)"
-apply (rule finite_induct)
-apply (metis finite_code)
-apply (metis INF_empty Inf_empty sup_top_right)
-apply (metis INF_insert Inf_insert sup_inf_distrib1)
-done
+ using finite by (induct A rule: finite_induct)
+ (simp_all add: sup_inf_distrib1)
lemma finite_distrib_lattice_complete_inf_Sup:
"inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
--- a/src/HOL/Set.thy Sat Apr 26 13:25:44 2014 +0200
+++ b/src/HOL/Set.thy Sat Apr 26 13:25:45 2014 +0200
@@ -1826,6 +1826,18 @@
lemma the_elem_eq [simp]: "the_elem {x} = x"
by (simp add: the_elem_def)
+lemma the_elem_image_unique:
+ assumes "A \<noteq> {}"
+ assumes *: "\<And>y. y \<in> A \<Longrightarrow> f y = f x"
+ shows "the_elem (f ` A) = f x"
+unfolding the_elem_def proof (rule the1_equality)
+ from `A \<noteq> {}` obtain y where "y \<in> A" by auto
+ with * have "f x = f y" by simp
+ with `y \<in> A` have "f x \<in> f ` A" by blast
+ with * show "f ` A = {f x}" by auto
+ then show "\<exists>!x. f ` A = {x}" by auto
+qed
+
subsubsection {* Least value operator *}