tuned
authorhaftmann
Sat Apr 26 13:25:45 2014 +0200 (2014-04-26)
changeset 567405ebaa364d8ab
parent 56739 0d56854096ba
child 56741 2b3710a4fa94
tuned
src/HOL/Hilbert_Choice.thy
src/HOL/Library/Finite_Lattice.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Apr 26 13:25:44 2014 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Sat Apr 26 13:25:45 2014 +0200
     1.3 @@ -235,11 +235,11 @@
     1.4  lemma image_surj_f_inv_f: "surj f ==> f ` (inv f ` A) = A"
     1.5  by (simp add: image_eq_UN surj_f_inv_f)
     1.6  
     1.7 -lemma image_inv_f_f: "inj f ==> (inv f) ` (f ` A) = A"
     1.8 -by (simp add: image_eq_UN)
     1.9 +lemma image_inv_f_f: "inj f ==> inv f ` (f ` A) = A"
    1.10 +  by (simp add: image_eq_UN)
    1.11  
    1.12 -lemma inv_image_comp: "inj f ==> inv f ` (f`X) = X"
    1.13 -by (auto simp add: image_def)
    1.14 +lemma inv_image_comp: "inj f ==> inv f ` (f ` X) = X"
    1.15 +  by (fact image_inv_f_f)
    1.16  
    1.17  lemma bij_image_Collect_eq: "bij f ==> f ` Collect P = {y. P (inv f y)}"
    1.18  apply auto
     2.1 --- a/src/HOL/Library/Finite_Lattice.thy	Sat Apr 26 13:25:44 2014 +0200
     2.2 +++ b/src/HOL/Library/Finite_Lattice.thy	Sat Apr 26 13:25:45 2014 +0200
     2.3 @@ -161,11 +161,8 @@
     2.4  
     2.5  lemma finite_distrib_lattice_complete_sup_Inf:
     2.6    "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)"
     2.7 -apply (rule finite_induct)
     2.8 -apply (metis finite_code)
     2.9 -apply (metis INF_empty Inf_empty sup_top_right)
    2.10 -apply (metis INF_insert Inf_insert sup_inf_distrib1)
    2.11 -done
    2.12 +  using finite by (induct A rule: finite_induct)
    2.13 +    (simp_all add: sup_inf_distrib1)
    2.14  
    2.15  lemma finite_distrib_lattice_complete_inf_Sup:
    2.16    "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
     3.1 --- a/src/HOL/Set.thy	Sat Apr 26 13:25:44 2014 +0200
     3.2 +++ b/src/HOL/Set.thy	Sat Apr 26 13:25:45 2014 +0200
     3.3 @@ -1826,6 +1826,18 @@
     3.4  lemma the_elem_eq [simp]: "the_elem {x} = x"
     3.5    by (simp add: the_elem_def)
     3.6  
     3.7 +lemma the_elem_image_unique:
     3.8 +  assumes "A \<noteq> {}"
     3.9 +  assumes *: "\<And>y. y \<in> A \<Longrightarrow> f y = f x"
    3.10 +  shows "the_elem (f ` A) = f x"
    3.11 +unfolding the_elem_def proof (rule the1_equality)
    3.12 +  from `A \<noteq> {}` obtain y where "y \<in> A" by auto
    3.13 +  with * have "f x = f y" by simp
    3.14 +  with `y \<in> A` have "f x \<in> f ` A" by blast
    3.15 +  with * show "f ` A = {f x}" by auto
    3.16 +  then show "\<exists>!x. f ` A = {x}" by auto
    3.17 +qed
    3.18 +
    3.19  
    3.20  subsubsection {* Least value operator *}
    3.21