Changes to complete distributive lattices due to Viorel Preoteasa
authorManuel Eberl <eberlm@in.tum.de>
Mon Mar 12 20:52:53 2018 +0100 (16 months ago)
changeset 678292a6ef5ba4822
parent 67828 655d03493d0f
child 67830 4f992daf4707
Changes to complete distributive lattices due to Viorel Preoteasa
src/HOL/Analysis/Polytope.thy
src/HOL/Complete_Lattices.thy
src/HOL/Enum.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Finite_Lattice.thy
src/HOL/Library/Option_ord.thy
src/HOL/Library/Product_Order.thy
src/HOL/Predicate.thy
     1.1 --- a/src/HOL/Analysis/Polytope.thy	Mon Mar 12 08:25:35 2018 +0000
     1.2 +++ b/src/HOL/Analysis/Polytope.thy	Mon Mar 12 20:52:53 2018 +0100
     1.3 @@ -735,7 +735,11 @@
     1.4    show ?thesis
     1.5    proof (cases "Q = {}")
     1.6      case True then show ?thesis
     1.7 +      sledgehammer
     1.8 +      by (metis IntQ Inter_UNIV_conv(2) assms(1) assms(2) ex_in_conv)
     1.9 +(*
    1.10        by (metis Inf_empty Inf_lower IntQ assms ex_in_conv subset_antisym top_greatest)
    1.11 +*)
    1.12    next
    1.13      case False
    1.14      have "Q \<subseteq> {T. T exposed_face_of S}"
     2.1 --- a/src/HOL/Complete_Lattices.thy	Mon Mar 12 08:25:35 2018 +0000
     2.2 +++ b/src/HOL/Complete_Lattices.thy	Mon Mar 12 20:52:53 2018 +0100
     2.3 @@ -3,6 +3,7 @@
     2.4      Author:     Lawrence C Paulson
     2.5      Author:     Markus Wenzel
     2.6      Author:     Florian Haftmann
     2.7 +    Author:     Viorel Preoteasa (Complete Distributive Lattices)     
     2.8  *)
     2.9  
    2.10  section \<open>Complete lattices\<close>
    2.11 @@ -453,56 +454,43 @@
    2.12  
    2.13  end
    2.14  
    2.15 -class complete_distrib_lattice = complete_lattice +
    2.16 -  assumes sup_Inf: "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
    2.17 -    and inf_Sup: "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
    2.18 +context complete_lattice
    2.19  begin
    2.20 -
    2.21 -lemma sup_INF: "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
    2.22 -  by (simp add: sup_Inf)
    2.23 +lemma Sup_Inf_le: "Sup (Inf ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)}) \<le> Inf (Sup ` A)"
    2.24 +  by (rule SUP_least, clarify, rule INF_greatest, simp add: INF_lower2 Sup_upper)
    2.25 +end 
    2.26  
    2.27 -lemma inf_SUP: "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
    2.28 -  by (simp add: inf_Sup)
    2.29 -
    2.30 -lemma dual_complete_distrib_lattice:
    2.31 -  "class.complete_distrib_lattice Sup Inf sup (\<ge>) (>) inf \<top> \<bottom>"
    2.32 -  apply (rule class.complete_distrib_lattice.intro)
    2.33 -   apply (fact dual_complete_lattice)
    2.34 -  apply (rule class.complete_distrib_lattice_axioms.intro)
    2.35 -   apply (simp_all add: inf_Sup sup_Inf)
    2.36 -  done
    2.37 +class complete_distrib_lattice = complete_lattice +
    2.38 +  assumes Inf_Sup_le: "Inf (Sup ` A) \<le> Sup (Inf ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)})"
    2.39 +begin
    2.40 +  
    2.41 +lemma Inf_Sup: "Inf (Sup ` A) = Sup (Inf ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)})"
    2.42 +  by (rule antisym, rule Inf_Sup_le, rule Sup_Inf_le)
    2.43  
    2.44  subclass distrib_lattice
    2.45  proof
    2.46    fix a b c
    2.47 -  have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" by (rule sup_Inf)
    2.48 -  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by simp
    2.49 +  show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)"
    2.50 +  proof (rule antisym, simp_all, safe)
    2.51 +    show "b \<sqinter> c \<le> a \<squnion> b"
    2.52 +      by (rule le_infI1, simp)
    2.53 +    show "b \<sqinter> c \<le> a \<squnion> c"
    2.54 +      by (rule le_infI2, simp)
    2.55 +    have [simp]: "a \<sqinter> c \<le> a \<squnion> b \<sqinter> c"
    2.56 +      by (rule le_infI1, simp)
    2.57 +    have [simp]: "b \<sqinter> a \<le> a \<squnion> b \<sqinter> c"
    2.58 +      by (rule le_infI2, simp)
    2.59 +    have " INFIMUM {{a, b}, {a, c}} Sup = SUPREMUM {f ` {{a, b}, {a, c}} |f. \<forall>Y\<in>{{a, b}, {a, c}}. f Y \<in> Y} Inf"
    2.60 +      by (rule Inf_Sup)
    2.61 +    from this show "(a \<squnion> b) \<sqinter> (a \<squnion> c) \<le> a \<squnion> b \<sqinter> c"
    2.62 +      apply simp
    2.63 +      by (rule SUP_least, safe, simp_all)
    2.64 +  qed
    2.65  qed
    2.66 -
    2.67 -lemma Inf_sup: "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
    2.68 -  by (simp add: sup_Inf sup_commute)
    2.69 -
    2.70 -lemma Sup_inf: "\<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)"
    2.71 -  by (simp add: inf_Sup inf_commute)
    2.72 -
    2.73 -lemma INF_sup: "(\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)"
    2.74 -  by (simp add: sup_INF sup_commute)
    2.75 +end
    2.76  
    2.77 -lemma SUP_inf: "(\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)"
    2.78 -  by (simp add: inf_SUP inf_commute)
    2.79 -
    2.80 -lemma Inf_sup_eq_top_iff: "(\<Sqinter>B \<squnion> a = \<top>) \<longleftrightarrow> (\<forall>b\<in>B. b \<squnion> a = \<top>)"
    2.81 -  by (simp only: Inf_sup INF_top_conv)
    2.82 -
    2.83 -lemma Sup_inf_eq_bot_iff: "(\<Squnion>B \<sqinter> a = \<bottom>) \<longleftrightarrow> (\<forall>b\<in>B. b \<sqinter> a = \<bottom>)"
    2.84 -  by (simp only: Sup_inf SUP_bot_conv)
    2.85 -
    2.86 -lemma INF_sup_distrib2: "(\<Sqinter>a\<in>A. f a) \<squnion> (\<Sqinter>b\<in>B. g b) = (\<Sqinter>a\<in>A. \<Sqinter>b\<in>B. f a \<squnion> g b)"
    2.87 -  by (subst INF_commute) (simp add: sup_INF INF_sup)
    2.88 -
    2.89 -lemma SUP_inf_distrib2: "(\<Squnion>a\<in>A. f a) \<sqinter> (\<Squnion>b\<in>B. g b) = (\<Squnion>a\<in>A. \<Squnion>b\<in>B. f a \<sqinter> g b)"
    2.90 -  by (subst SUP_commute) (simp add: inf_SUP SUP_inf)
    2.91 -
    2.92 +context complete_lattice
    2.93 +begin
    2.94  context
    2.95    fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
    2.96    assumes "mono f"
    2.97 @@ -527,12 +515,6 @@
    2.98  class complete_boolean_algebra = boolean_algebra + complete_distrib_lattice
    2.99  begin
   2.100  
   2.101 -lemma dual_complete_boolean_algebra:
   2.102 -  "class.complete_boolean_algebra Sup Inf sup (\<ge>) (>) inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
   2.103 -  by (rule class.complete_boolean_algebra.intro,
   2.104 -      rule dual_complete_distrib_lattice,
   2.105 -      rule dual_boolean_algebra)
   2.106 -
   2.107  lemma uminus_Inf: "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
   2.108  proof (rule antisym)
   2.109    show "- \<Sqinter>A \<le> \<Squnion>(uminus ` A)"
   2.110 @@ -639,18 +621,8 @@
   2.111  lemma le_SUP_iff: "x \<le> SUPREMUM A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
   2.112    using le_Sup_iff [of _ "f ` A"] by simp
   2.113  
   2.114 -subclass complete_distrib_lattice
   2.115 -proof
   2.116 -  fix a and B
   2.117 -  show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)" and "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
   2.118 -    by (safe intro!: INF_eqI [symmetric] sup_mono Inf_lower SUP_eqI [symmetric] inf_mono Sup_upper)
   2.119 -      (auto simp: not_less [symmetric] Inf_less_iff less_Sup_iff
   2.120 -        le_max_iff_disj complete_linorder_sup_max min_le_iff_disj complete_linorder_inf_min)
   2.121 -qed
   2.122 -
   2.123  end
   2.124  
   2.125 -
   2.126  subsection \<open>Complete lattice on @{typ bool}\<close>
   2.127  
   2.128  instantiation bool :: complete_lattice
   2.129 @@ -678,8 +650,7 @@
   2.130    by (simp add: fun_eq_iff)
   2.131  
   2.132  instance bool :: complete_boolean_algebra
   2.133 -  by standard (auto intro: bool_induct)
   2.134 -
   2.135 +  by (standard, fastforce)
   2.136  
   2.137  subsection \<open>Complete lattice on @{typ "_ \<Rightarrow> _"}\<close>
   2.138  
   2.139 @@ -721,12 +692,6 @@
   2.140  lemma SUP_apply [simp]: "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
   2.141    using Sup_apply [of "f ` A"] by (simp add: comp_def)
   2.142  
   2.143 -instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice
   2.144 -  by standard (auto simp add: inf_Sup sup_Inf fun_eq_iff image_image)
   2.145 -
   2.146 -instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
   2.147 -
   2.148 -
   2.149  subsection \<open>Complete lattice on unary and binary predicates\<close>
   2.150  
   2.151  lemma Inf1_I: "(\<And>P. P \<in> A \<Longrightarrow> P a) \<Longrightarrow> (\<Sqinter>A) a"
   2.152 @@ -820,10 +785,6 @@
   2.153  
   2.154  end
   2.155  
   2.156 -instance "set" :: (type) complete_boolean_algebra
   2.157 -  by standard (auto simp add: Inf_set_def Sup_set_def image_def)
   2.158 -
   2.159 -
   2.160  subsubsection \<open>Inter\<close>
   2.161  
   2.162  abbreviation Inter :: "'a set set \<Rightarrow> 'a set"  ("\<Inter>_" [900] 900)
   2.163 @@ -1218,13 +1179,13 @@
   2.164  subsubsection \<open>Distributive laws\<close>
   2.165  
   2.166  lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
   2.167 -  by (fact inf_Sup)
   2.168 +  by blast
   2.169  
   2.170  lemma Un_Inter: "A \<union> \<Inter>B = (\<Inter>C\<in>B. A \<union> C)"
   2.171 -  by (fact sup_Inf)
   2.172 +  by blast
   2.173  
   2.174  lemma Int_Union2: "\<Union>B \<inter> A = (\<Union>C\<in>B. C \<inter> A)"
   2.175 -  by (fact Sup_inf)
   2.176 +  by blast
   2.177  
   2.178  lemma INT_Int_distrib: "(\<Inter>i\<in>I. A i \<inter> B i) = (\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i)"
   2.179    by (rule sym) (rule INF_inf_distrib)
   2.180 @@ -1241,20 +1202,20 @@
   2.181    by (simp add: UN_Un_distrib)
   2.182  
   2.183  lemma Un_INT_distrib: "B \<union> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. B \<union> A i)"
   2.184 -  by (fact sup_INF)
   2.185 +  by blast
   2.186  
   2.187  lemma Int_UN_distrib: "B \<inter> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. B \<inter> A i)"
   2.188    \<comment> \<open>Halmos, Naive Set Theory, page 35.\<close>
   2.189 -  by (fact inf_SUP)
   2.190 +  by blast
   2.191  
   2.192  lemma Int_UN_distrib2: "(\<Union>i\<in>I. A i) \<inter> (\<Union>j\<in>J. B j) = (\<Union>i\<in>I. \<Union>j\<in>J. A i \<inter> B j)"
   2.193 -  by (fact SUP_inf_distrib2)
   2.194 +  by blast
   2.195  
   2.196  lemma Un_INT_distrib2: "(\<Inter>i\<in>I. A i) \<union> (\<Inter>j\<in>J. B j) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A i \<union> B j)"
   2.197 -  by (fact INF_sup_distrib2)
   2.198 +  by blast
   2.199  
   2.200  lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})"
   2.201 -  by (fact Sup_inf_eq_bot_iff)
   2.202 +  by blast
   2.203  
   2.204  lemma SUP_UNION: "(\<Squnion>x\<in>(\<Union>y\<in>A. g y). f x) = (\<Squnion>y\<in>A. \<Squnion>x\<in>g y. f x :: _ :: complete_lattice)"
   2.205    by (rule order_antisym) (blast intro: SUP_least SUP_upper2)+
   2.206 @@ -1354,11 +1315,10 @@
   2.207  subsubsection \<open>Complement\<close>
   2.208  
   2.209  lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
   2.210 -  by (fact uminus_INF)
   2.211 +  by blast
   2.212  
   2.213  lemma Compl_UN [simp]: "- (\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
   2.214 -  by (fact uminus_SUP)
   2.215 -
   2.216 +  by blast
   2.217  
   2.218  subsubsection \<open>Miniscoping and maxiscoping\<close>
   2.219  
     3.1 --- a/src/HOL/Enum.thy	Mon Mar 12 08:25:35 2018 +0000
     3.2 +++ b/src/HOL/Enum.thy	Mon Mar 12 20:52:53 2018 +0100
     3.3 @@ -678,10 +678,9 @@
     3.4  qed(auto simp add: less_eq_finite_2_def less_finite_2_def inf_finite_2_def sup_finite_2_def Inf_finite_2_def Sup_finite_2_def)
     3.5  end
     3.6  
     3.7 -instance finite_2 :: complete_distrib_lattice
     3.8 -  by standard (auto simp add: sup_finite_2_def inf_finite_2_def Inf_finite_2_def Sup_finite_2_def)
     3.9 +instance finite_2 :: complete_linorder ..
    3.10  
    3.11 -instance finite_2 :: complete_linorder ..
    3.12 +instance finite_2 :: complete_distrib_lattice ..
    3.13  
    3.14  instantiation finite_2 :: "{field, idom_abs_sgn, idom_modulo}" begin
    3.15  definition [simp]: "0 = a\<^sub>1"
    3.16 @@ -783,7 +782,101 @@
    3.17    from this[symmetric] show "wf \<dots>" by simp
    3.18  qed intro_classes
    3.19  
    3.20 -instantiation finite_3 :: complete_lattice
    3.21 +class finite_lattice = finite +  lattice + Inf + Sup  + bot + top +
    3.22 +  assumes Inf_finite_empty: "Inf {} = Sup UNIV"
    3.23 +  assumes Inf_finite_insert: "Inf (insert a A) = a \<sqinter> Inf A"
    3.24 +  assumes Sup_finite_empty: "Sup {} = Inf UNIV"
    3.25 +  assumes Sup_finite_insert: "Sup (insert a A) = a \<squnion> Sup A"
    3.26 +  assumes bot_finite_def: "bot = Inf UNIV"
    3.27 +  assumes top_finite_def: "top = Sup UNIV"
    3.28 +begin
    3.29 +
    3.30 +subclass complete_lattice
    3.31 +proof
    3.32 +  fix x A
    3.33 +  show "x \<in> A \<Longrightarrow> \<Sqinter>A \<le> x"
    3.34 +    by (cut_tac A = A and a = x in Inf_finite_insert, simp add: insert_absorb inf.absorb_iff2)
    3.35 +  show "x \<in> A \<Longrightarrow> x \<le> \<Squnion>A"
    3.36 +    by (cut_tac A = A and a = x in Sup_finite_insert, simp add: insert_absorb sup.absorb_iff2)
    3.37 +next
    3.38 +  fix A z
    3.39 +  show "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A"
    3.40 +    apply (cut_tac F = A and P = "\<lambda> A . (\<forall> x. x \<in> A \<longrightarrow> z \<le> x) \<longrightarrow> z \<le> \<Sqinter>A" in finite_induct, simp_all add: Inf_finite_empty Inf_finite_insert)
    3.41 +    by(cut_tac A = UNIV and a = z in Sup_finite_insert, simp add: insert_UNIV local.sup.absorb_iff2)
    3.42 +
    3.43 +  show " (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z"
    3.44 +    apply (cut_tac F = A and  P = "\<lambda> A . (\<forall> x. x \<in> A \<longrightarrow> x \<le> z) \<longrightarrow> \<Squnion>A \<le> z" in finite_induct, simp_all add: Sup_finite_empty Sup_finite_insert)
    3.45 +    by(cut_tac A = UNIV and a = z in Inf_finite_insert, simp add: insert_UNIV local.inf.absorb_iff2)
    3.46 +next
    3.47 +  show "\<Sqinter>{} = \<top>"
    3.48 +    by (simp add: Inf_finite_empty top_finite_def)
    3.49 +  show " \<Squnion>{} = \<bottom>"
    3.50 +    by (simp add: Sup_finite_empty bot_finite_def)
    3.51 +qed
    3.52 +end
    3.53 +
    3.54 +class finite_distrib_lattice = finite_lattice + distrib_lattice 
    3.55 +begin
    3.56 +lemma finite_inf_Sup: "a \<sqinter> (Sup A) = Sup {a \<sqinter> b | b . b \<in> A}"
    3.57 +proof (cut_tac F = A and P = "\<lambda> A . a \<sqinter> (Sup A) = Sup {a \<sqinter> b | b . b \<in> A}" in finite_induct, simp_all)
    3.58 +  fix x::"'a"
    3.59 +  fix F
    3.60 +  assume "x \<notin> F"
    3.61 +  assume A: "a \<sqinter> \<Squnion>F = \<Squnion>{a \<sqinter> b |b. b \<in> F}"
    3.62 +
    3.63 +  have [simp]: " insert (a \<sqinter> x) {a \<sqinter> b |b. b \<in> F} = {a \<sqinter> b |b. b = x \<or> b \<in> F}"
    3.64 +    by auto
    3.65 +
    3.66 +  have "a \<sqinter> (x \<squnion> \<Squnion>F) = a \<sqinter> x \<squnion> a \<sqinter> \<Squnion>F"
    3.67 +    by (simp add: inf_sup_distrib1)
    3.68 +  also have "... = a \<sqinter> x \<squnion> \<Squnion>{a \<sqinter> b |b. b \<in> F}"
    3.69 +    by (simp add: A)
    3.70 +  also have "... = \<Squnion>{a \<sqinter> b |b. b = x \<or> b \<in> F}"
    3.71 +    by (unfold Sup_insert[THEN sym], simp)
    3.72 +
    3.73 +  finally show "a \<sqinter> (x \<squnion> \<Squnion>F) = \<Squnion>{a \<sqinter> b |b. b = x \<or> b \<in> F}"
    3.74 +    by simp
    3.75 +qed
    3.76 +
    3.77 +lemma finite_Inf_Sup: "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
    3.78 +proof (cut_tac F = A and P = "\<lambda> A .INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf" in finite_induct, simp_all add: finite_UnionD)
    3.79 +  fix x::"'a set"
    3.80 +  fix F
    3.81 +  assume "x \<notin> F"
    3.82 +  have [simp]: "{\<Squnion>x \<sqinter> b |b . b \<in> Inf ` {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} } = {\<Squnion>x \<sqinter> (Inf (f ` F)) |f  .  (\<forall>Y\<in>F. f Y \<in> Y)}"
    3.83 +    by auto
    3.84 +  have [simp]:" \<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> \<exists>fa. insert b (f ` (F \<inter> {Y. Y \<noteq> x})) = insert (fa x) (fa ` F) \<and> fa x \<in> x \<and> (\<forall>Y\<in>F. fa Y \<in> Y)"
    3.85 +     apply (rule_tac x = "(\<lambda> Y . (if Y = x then b else f Y))" in exI)
    3.86 +    by auto
    3.87 +  have [simp]: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> (\<Sqinter>x\<in>F. f x) \<sqinter> b \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
    3.88 +    apply (rule_tac i = "(\<lambda> Y . (if Y = x then b else f Y)) ` ({x} \<union> F)" in SUP_upper2, simp)
    3.89 +    apply (subst inf_commute)
    3.90 +    by (simp add: INF_greatest Inf_lower inf.coboundedI2)
    3.91 +
    3.92 +  assume "INFIMUM F Sup \<le> SUPREMUM {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} Inf"
    3.93 +
    3.94 +  from this have "\<Squnion>x \<sqinter> INFIMUM F Sup \<le> \<Squnion>x \<sqinter> SUPREMUM {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} Inf"
    3.95 +    apply simp
    3.96 +    using inf.coboundedI2 by blast
    3.97 +  also have "... = Sup {\<Squnion>x \<sqinter> (Inf (f ` F)) |f  .  (\<forall>Y\<in>F. f Y \<in> Y)}"
    3.98 +    by (simp add: finite_inf_Sup)
    3.99 +
   3.100 +  also have "... = Sup {Sup {Inf (f ` F) \<sqinter> b | b . b \<in> x} |f  .  (\<forall>Y\<in>F. f Y \<in> Y)}"
   3.101 +    apply (subst inf_commute)
   3.102 +    by (simp add: finite_inf_Sup)
   3.103 +
   3.104 +  also have "... \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
   3.105 +    by (rule Sup_least, clarsimp, rule Sup_least, clarsimp)
   3.106 +
   3.107 +  finally show "\<Squnion>x \<sqinter> INFIMUM F Sup \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
   3.108 +    by simp
   3.109 +qed
   3.110 +
   3.111 +subclass complete_distrib_lattice
   3.112 +  by (standard, rule finite_Inf_Sup)
   3.113 +end
   3.114 +
   3.115 +instantiation finite_3 :: finite_lattice
   3.116  begin
   3.117  
   3.118  definition "\<Sqinter>A = (if a\<^sub>1 \<in> A then a\<^sub>1 else if a\<^sub>2 \<in> A then a\<^sub>2 else a\<^sub>3)"
   3.119 @@ -795,38 +888,16 @@
   3.120  
   3.121  instance
   3.122  proof
   3.123 -  fix x :: finite_3 and A
   3.124 -  assume "x \<in> A"
   3.125 -  then show "\<Sqinter>A \<le> x" "x \<le> \<Squnion>A"
   3.126 -    by(case_tac [!] x)(auto simp add: Inf_finite_3_def Sup_finite_3_def less_eq_finite_3_def less_finite_3_def)
   3.127 -next
   3.128 -  fix A and z :: finite_3
   3.129 -  assume "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
   3.130 -  then show "z \<le> \<Sqinter>A"
   3.131 -    by(cases z)(auto simp add: Inf_finite_3_def less_eq_finite_3_def less_finite_3_def)
   3.132 -next
   3.133 -  fix A and z :: finite_3
   3.134 -  assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
   3.135 -  show "\<Squnion>A \<le> z"
   3.136 -    by(auto simp add: Sup_finite_3_def less_eq_finite_3_def less_finite_3_def dest: *)
   3.137 -qed(auto simp add: Inf_finite_3_def Sup_finite_3_def)
   3.138 +qed (auto simp add: Inf_finite_3_def Sup_finite_3_def max_def min_def less_eq_finite_3_def less_finite_3_def split: finite_3.split)
   3.139  end
   3.140  
   3.141 -instance finite_3 :: complete_distrib_lattice
   3.142 -proof
   3.143 -  fix a :: finite_3 and B
   3.144 -  show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
   3.145 -  proof(cases a "\<Sqinter>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
   3.146 -    case a\<^sub>2_a\<^sub>3
   3.147 -    then have "\<And>x. x \<in> B \<Longrightarrow> x = a\<^sub>3"
   3.148 -      by(case_tac x)(auto simp add: Inf_finite_3_def split: if_split_asm)
   3.149 -    then show ?thesis using a\<^sub>2_a\<^sub>3
   3.150 -      by(auto simp add: Inf_finite_3_def max_def less_eq_finite_3_def less_finite_3_def split: if_split_asm)
   3.151 -  qed (auto simp add: Inf_finite_3_def max_def less_finite_3_def less_eq_finite_3_def split: if_split_asm)
   3.152 -  show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
   3.153 -    by (cases a "\<Squnion>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
   3.154 -      (auto simp add: Sup_finite_3_def min_def less_finite_3_def less_eq_finite_3_def split: if_split_asm)
   3.155 -qed
   3.156 +instance finite_3 :: complete_lattice ..
   3.157 +
   3.158 +instance finite_3 :: finite_distrib_lattice
   3.159 +proof 
   3.160 +qed (auto simp add: min_def max_def)
   3.161 +
   3.162 +instance finite_3 :: complete_distrib_lattice ..
   3.163  
   3.164  instance finite_3 :: complete_linorder ..
   3.165  
   3.166 @@ -910,7 +981,7 @@
   3.167  
   3.168  end
   3.169  
   3.170 -instantiation finite_4 :: complete_lattice begin
   3.171 +instantiation finite_4 :: finite_distrib_lattice begin
   3.172  
   3.173  text \<open>@{term a\<^sub>1} $<$ @{term a\<^sub>2},@{term a\<^sub>3} $<$ @{term a\<^sub>4},
   3.174    but @{term a\<^sub>2} and @{term a\<^sub>3} are incomparable.\<close>
   3.175 @@ -947,38 +1018,22 @@
   3.176    | (a\<^sub>3, _) \<Rightarrow> a\<^sub>3 | (_, a\<^sub>3) \<Rightarrow> a\<^sub>3
   3.177    | _ \<Rightarrow> a\<^sub>1)"
   3.178  
   3.179 -instance
   3.180 -proof
   3.181 -  fix A and z :: finite_4
   3.182 -  assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
   3.183 -  show "\<Squnion>A \<le> z"
   3.184 -    by(auto simp add: Sup_finite_4_def less_eq_finite_4_def dest!: * split: finite_4.splits)
   3.185 -next
   3.186 -  fix A and z :: finite_4
   3.187 -  assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
   3.188 -  show "z \<le> \<Sqinter>A"
   3.189 -    by(auto simp add: Inf_finite_4_def less_eq_finite_4_def dest!: * split: finite_4.splits)
   3.190 -qed(auto simp add: less_finite_4_def less_eq_finite_4_def Inf_finite_4_def Sup_finite_4_def inf_finite_4_def sup_finite_4_def split: finite_4.splits)
   3.191 -
   3.192 +instance proof
   3.193 +qed(auto simp add: less_finite_4_def less_eq_finite_4_def Inf_finite_4_def Sup_finite_4_def 
   3.194 +    inf_finite_4_def sup_finite_4_def split: finite_4.splits)
   3.195  end
   3.196  
   3.197 -instance finite_4 :: complete_distrib_lattice
   3.198 -proof
   3.199 -  fix a :: finite_4 and B
   3.200 -  show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
   3.201 -    by(cases a "\<Sqinter>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
   3.202 -      (auto simp add: sup_finite_4_def Inf_finite_4_def split: finite_4.splits if_split_asm)
   3.203 -  show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
   3.204 -    by(cases a "\<Squnion>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
   3.205 -      (auto simp add: inf_finite_4_def Sup_finite_4_def split: finite_4.splits if_split_asm)
   3.206 -qed
   3.207 +instance finite_4 :: complete_lattice ..
   3.208 +
   3.209 +instance finite_4 :: complete_distrib_lattice ..
   3.210  
   3.211  instantiation finite_4 :: complete_boolean_algebra begin
   3.212  definition "- x = (case x of a\<^sub>1 \<Rightarrow> a\<^sub>4 | a\<^sub>2 \<Rightarrow> a\<^sub>3 | a\<^sub>3 \<Rightarrow> a\<^sub>2 | a\<^sub>4 \<Rightarrow> a\<^sub>1)"
   3.213  definition "x - y = x \<sqinter> - (y :: finite_4)"
   3.214  instance
   3.215  by intro_classes
   3.216 -  (simp_all add: inf_finite_4_def sup_finite_4_def uminus_finite_4_def minus_finite_4_def split: finite_4.splits)
   3.217 +  (simp_all add: inf_finite_4_def sup_finite_4_def uminus_finite_4_def minus_finite_4_def 
   3.218 +    split: finite_4.splits)
   3.219  end
   3.220  
   3.221  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
   3.222 @@ -1013,7 +1068,7 @@
   3.223  
   3.224  end
   3.225  
   3.226 -instantiation finite_5 :: complete_lattice
   3.227 +instantiation finite_5 :: finite_lattice
   3.228  begin
   3.229  
   3.230  text \<open>The non-distributive pentagon lattice $N_5$\<close>
   3.231 @@ -1065,19 +1120,14 @@
   3.232     | _ \<Rightarrow> a\<^sub>1)"
   3.233  
   3.234  instance 
   3.235 -proof intro_classes
   3.236 -  fix A and z :: finite_5
   3.237 -  assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
   3.238 -  show "z \<le> \<Sqinter>A"
   3.239 -    by(auto simp add: less_eq_finite_5_def Inf_finite_5_def split: finite_5.splits if_split_asm dest!: *)
   3.240 -next
   3.241 -  fix A and z :: finite_5
   3.242 -  assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
   3.243 -  show "\<Squnion>A \<le> z"
   3.244 -    by(auto simp add: less_eq_finite_5_def Sup_finite_5_def split: finite_5.splits if_split_asm dest!: *)
   3.245 -qed(auto simp add: less_eq_finite_5_def less_finite_5_def inf_finite_5_def sup_finite_5_def Inf_finite_5_def Sup_finite_5_def split: finite_5.splits if_split_asm)
   3.246 +proof
   3.247 +qed (auto simp add: less_eq_finite_5_def less_finite_5_def inf_finite_5_def sup_finite_5_def 
   3.248 +    Inf_finite_5_def Sup_finite_5_def split: finite_5.splits if_split_asm)
   3.249 +end
   3.250  
   3.251 -end
   3.252 +
   3.253 +instance  finite_5 :: complete_lattice ..
   3.254 +
   3.255  
   3.256  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4 a\<^sub>5
   3.257  
     4.1 --- a/src/HOL/Hilbert_Choice.thy	Mon Mar 12 08:25:35 2018 +0000
     4.2 +++ b/src/HOL/Hilbert_Choice.thy	Mon Mar 12 20:52:53 2018 +0100
     4.3 @@ -1,5 +1,6 @@
     4.4  (*  Title:      HOL/Hilbert_Choice.thy
     4.5      Author:     Lawrence C Paulson, Tobias Nipkow
     4.6 +    Author:     Viorel Preoteasa (Results about complete distributive lattices) 
     4.7      Copyright   2001  University of Cambridge
     4.8  *)
     4.9  
    4.10 @@ -803,4 +804,319 @@
    4.11  
    4.12  ML_file "Tools/choice_specification.ML"
    4.13  
    4.14 +subsection \<open>Complete Distributive Lattices -- Properties depending on Hilbert Choice\<close>
    4.15 +
    4.16 +context complete_distrib_lattice
    4.17 +begin
    4.18 +lemma Sup_Inf: "Sup (Inf ` A) = Inf (Sup ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)})"
    4.19 +proof (rule antisym)
    4.20 +  show "SUPREMUM A Inf \<le> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Sup"
    4.21 +    apply (rule Sup_least, rule INF_greatest)
    4.22 +    using Inf_lower2 Sup_upper by auto
    4.23 +next
    4.24 +  show "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Sup \<le> SUPREMUM A Inf"
    4.25 +  proof (simp add:  Inf_Sup, rule_tac SUP_least, simp, safe)
    4.26 +    fix f
    4.27 +    assume "\<forall>Y. (\<exists>f. Y = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<longrightarrow> f Y \<in> Y"
    4.28 +    from this have B: "\<And> F . (\<forall> Y \<in> A . F Y \<in> Y) \<Longrightarrow> \<exists> Z \<in> A . f (F ` A) = F Z"
    4.29 +      by auto
    4.30 +    show "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> SUPREMUM A Inf"
    4.31 +    proof (cases "\<exists> Z \<in> A . INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> Inf Z")
    4.32 +      case True
    4.33 +      from this obtain Z where [simp]: "Z \<in> A" and A: "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> Inf Z"
    4.34 +        by blast
    4.35 +      have B: "... \<le> SUPREMUM A Inf"
    4.36 +        by (simp add: SUP_upper)
    4.37 +      from A and B show ?thesis
    4.38 +        by (drule_tac order_trans, simp_all)
    4.39 +    next
    4.40 +      case False
    4.41 +      from this have X: "\<And> Z . Z \<in> A \<Longrightarrow> \<exists> x . x \<in> Z \<and> \<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> x"
    4.42 +        using Inf_greatest by blast
    4.43 +      define F where "F = (\<lambda> Z . SOME x . x \<in> Z \<and> \<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> x)"
    4.44 +      have C: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
    4.45 +        using X by (simp add: F_def, rule someI2_ex, auto)
    4.46 +      have E: "\<And> Y . Y \<in> A \<Longrightarrow> \<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> F Y"
    4.47 +        using X by (simp add: F_def, rule someI2_ex, auto)
    4.48 +      from C and B obtain  Z where D: "Z \<in> A " and Y: "f (F ` A) = F Z"
    4.49 +        by blast
    4.50 +      from E and D have W: "\<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> F Z"
    4.51 +        by simp
    4.52 +      from C have "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> f (F ` A)"
    4.53 +        by (rule_tac INF_lower, blast)
    4.54 +      from this and W and Y show ?thesis
    4.55 +        by simp
    4.56 +    qed
    4.57 +  qed
    4.58 +qed
    4.59 +  
    4.60 +lemma dual_complete_distrib_lattice:
    4.61 +  "class.complete_distrib_lattice Sup Inf sup (\<ge>) (>) inf \<top> \<bottom>"
    4.62 +  apply (rule class.complete_distrib_lattice.intro)
    4.63 +   apply (fact dual_complete_lattice)
    4.64 +  by (simp add: class.complete_distrib_lattice_axioms_def Sup_Inf)
    4.65 +
    4.66 +lemma sup_Inf: "a \<squnion> Inf B = (INF b:B. a \<squnion> b)"
    4.67 +proof (rule antisym)
    4.68 +  show "a \<squnion> Inf B \<le> (INF b:B. a \<squnion> b)"
    4.69 +    using Inf_lower sup.mono by (rule_tac INF_greatest, fastforce)
    4.70 +next
    4.71 +  have "(INF b:B. a \<squnion> b) \<le> INFIMUM {{f {a}, f B} |f. f {a} = a \<and> f B \<in> B} Sup"
    4.72 +    by (rule INF_greatest, auto simp add: INF_lower)
    4.73 +  also have "... = a \<squnion> Inf B"
    4.74 +    by (cut_tac A = "{{a}, B}" in Sup_Inf, simp)
    4.75 +  finally show "(INF b:B. a \<squnion> b) \<le> a \<squnion> Inf B"
    4.76 +    by simp
    4.77 +qed
    4.78 +
    4.79 +lemma inf_Sup: "a \<sqinter> Sup B = (SUP b:B. a \<sqinter> b)"
    4.80 +  using dual_complete_distrib_lattice
    4.81 +  by (rule complete_distrib_lattice.sup_Inf)
    4.82 +
    4.83 +lemma INF_SUP: "(INF y. SUP x. ((P x y)::'a)) = (SUP x. INF y. P (x y) y)"
    4.84 +proof (rule antisym)
    4.85 +  show "(SUP x. INF y. P (x y) y) \<le> (INF y. SUP x. P x y)"
    4.86 +    by (rule SUP_least, rule INF_greatest, rule SUP_upper2, simp_all, rule INF_lower2, simp, blast)
    4.87 +next
    4.88 +  have "(INF y. SUP x. ((P x y))) \<le> Inf (Sup ` {{P x y | x . True} | y . True })" (is "?A \<le> ?B")
    4.89 +  proof (rule_tac INF_greatest, clarsimp)
    4.90 +    fix y
    4.91 +    have "?A \<le> (SUP x. P x y)"
    4.92 +      by (rule INF_lower, simp)
    4.93 +    also have "... \<le> Sup {uu. \<exists>x. uu = P x y}"
    4.94 +      by (simp add: full_SetCompr_eq)
    4.95 +    finally show "?A \<le> Sup {uu. \<exists>x. uu = P x y}"
    4.96 +      by simp
    4.97 +  qed
    4.98 +  also have "... \<le>  (SUP x. INF y. P (x y) y)"
    4.99 +  proof (subst  Inf_Sup, rule_tac SUP_least, clarsimp)
   4.100 +    fix f
   4.101 +    assume A: "\<forall>Y. (\<exists>y. Y = {uu. \<exists>x. uu = P x y}) \<longrightarrow> f Y \<in> Y"
   4.102 +      
   4.103 +    have "(INF x:{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x) \<le>  (INF y. P ((\<lambda> y. SOME x . f ({P x y | x. True}) = P x y) y) y)"
   4.104 +    proof (rule INF_greatest, clarsimp)
   4.105 +      fix y
   4.106 +        have "(INF x:{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x) \<le> f {uu. \<exists>x. uu = P x y}"
   4.107 +          by (rule_tac INF_lower, blast)
   4.108 +        also have "... \<le> P (SOME x. f {uu . \<exists>x. uu = P x y} = P x y) y"
   4.109 +          using A by (rule_tac someI2_ex, auto)
   4.110 +        finally show "(INF x:{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x) \<le> P (SOME x. f {uu . \<exists>x. uu = P x y} = P x y) y"
   4.111 +          by simp
   4.112 +      qed
   4.113 +      also have "... \<le> (SUP x. INF y. P (x y) y)"
   4.114 +        by (rule SUP_upper, simp)
   4.115 +      finally show "(INF x:{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x) \<le> (SUP x. INF y. P (x y) y)"
   4.116 +        by simp
   4.117 +    qed
   4.118 +  finally show "(INF y. SUP x. P x y) \<le> (SUP x. INF y. P (x y) y)"
   4.119 +    by simp
   4.120 +qed
   4.121 +
   4.122 +lemma INF_SUP_set: "(INF x:A. SUP a:x. (g a)) = (SUP x:{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. INF a:x. g a)"
   4.123 +proof (rule antisym)
   4.124 +  have A: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> (\<Sqinter>x\<in>A. g (f x)) \<le> SUPREMUM xa g"
   4.125 +    by (rule_tac i = "(f xa)" in SUP_upper2, simp, rule_tac i = "xa" in INF_lower2, simp_all)
   4.126 +  show "(\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a) \<le> (\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a)"
   4.127 +    apply (rule SUP_least, simp, safe, rule INF_greatest, simp)
   4.128 +    by (rule A)
   4.129 +next
   4.130 +  show "(\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a)"
   4.131 +  proof (cases "{} \<in> A")
   4.132 +    case True
   4.133 +    then show ?thesis 
   4.134 +      by (rule_tac i = "{}" in INF_lower2, simp_all)
   4.135 +  next
   4.136 +    case False
   4.137 +    have [simp]: "\<And>x xa xb. xb \<in> A \<Longrightarrow> x xb \<in> xb \<Longrightarrow> (\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> g (x xb)"
   4.138 +      by (rule_tac i = xb in INF_lower2, simp_all)
   4.139 +    have [simp]: " \<And>x xa y. y \<in> A \<Longrightarrow> x y \<notin> y \<Longrightarrow> (\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> g (SOME x. x \<in> y)"
   4.140 +      by (rule_tac i = y in INF_lower2, simp_all)
   4.141 +    have [simp]: "\<And>x. (\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x\<in>x. g x)"
   4.142 +      apply (rule_tac i = "(\<lambda> y . if x y \<in> y then x y else (SOME x . x \<in>y)) ` A" in SUP_upper2, simp)
   4.143 +       apply (rule_tac x = "(\<lambda> y . if x y \<in> y then x y else (SOME x . x \<in>y))" in exI, simp)
   4.144 +      using False some_in_eq apply auto[1]
   4.145 +      by (rule INF_greatest, auto)
   4.146 +    have "\<And>x. (\<Sqinter>x\<in>A. \<Squnion>x\<in>x. g x) \<le> (\<Squnion>xa. if x \<in> A then if xa \<in> x then g xa else \<bottom> else \<top>)"
   4.147 +      apply (case_tac "x \<in> A")
   4.148 +       apply (rule INF_lower2, simp)
   4.149 +      by (rule SUP_least, rule SUP_upper2, auto)
   4.150 +    from this have "(\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a) \<le> (\<Sqinter>x. \<Squnion>xa. if x \<in> A then if xa \<in> x then g xa else \<bottom> else \<top>)"
   4.151 +      by (rule INF_greatest)
   4.152 +    also have "... = (\<Squnion>x. \<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>)"
   4.153 +      by (simp add: INF_SUP)
   4.154 +    also have "... \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a)"
   4.155 +      by (rule SUP_least, simp)
   4.156 +    finally show ?thesis by simp
   4.157 +  qed
   4.158 +qed
   4.159 +
   4.160 +lemma SUP_INF: "(SUP y. INF x. ((P x y)::'a)) = (INF x. SUP y. P (x y) y)"
   4.161 +  using dual_complete_distrib_lattice
   4.162 +  by (rule complete_distrib_lattice.INF_SUP)
   4.163 +
   4.164 +lemma SUP_INF_set: "(SUP x:A. INF a:x. (g a)) = (INF x:{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. SUP a:x. g a)"
   4.165 +  using dual_complete_distrib_lattice
   4.166 +  by (rule complete_distrib_lattice.INF_SUP_set)
   4.167 +
   4.168  end
   4.169 +
   4.170 +(*properties of the former complete_distrib_lattice*)
   4.171 +context complete_distrib_lattice
   4.172 +begin
   4.173 +
   4.174 +lemma sup_INF: "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
   4.175 +  by (simp add: sup_Inf)
   4.176 +
   4.177 +lemma inf_SUP: "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
   4.178 +  by (simp add: inf_Sup)
   4.179 +
   4.180 +
   4.181 +lemma Inf_sup: "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
   4.182 +  by (simp add: sup_Inf sup_commute)
   4.183 +
   4.184 +lemma Sup_inf: "\<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)"
   4.185 +  by (simp add: inf_Sup inf_commute)
   4.186 +
   4.187 +lemma INF_sup: "(\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)"
   4.188 +  by (simp add: sup_INF sup_commute)
   4.189 +
   4.190 +lemma SUP_inf: "(\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)"
   4.191 +  by (simp add: inf_SUP inf_commute)
   4.192 +
   4.193 +lemma Inf_sup_eq_top_iff: "(\<Sqinter>B \<squnion> a = \<top>) \<longleftrightarrow> (\<forall>b\<in>B. b \<squnion> a = \<top>)"
   4.194 +  by (simp only: Inf_sup INF_top_conv)
   4.195 +
   4.196 +lemma Sup_inf_eq_bot_iff: "(\<Squnion>B \<sqinter> a = \<bottom>) \<longleftrightarrow> (\<forall>b\<in>B. b \<sqinter> a = \<bottom>)"
   4.197 +  by (simp only: Sup_inf SUP_bot_conv)
   4.198 +
   4.199 +lemma INF_sup_distrib2: "(\<Sqinter>a\<in>A. f a) \<squnion> (\<Sqinter>b\<in>B. g b) = (\<Sqinter>a\<in>A. \<Sqinter>b\<in>B. f a \<squnion> g b)"
   4.200 +  by (subst INF_commute) (simp add: sup_INF INF_sup)
   4.201 +
   4.202 +lemma SUP_inf_distrib2: "(\<Squnion>a\<in>A. f a) \<sqinter> (\<Squnion>b\<in>B. g b) = (\<Squnion>a\<in>A. \<Squnion>b\<in>B. f a \<sqinter> g b)"
   4.203 +  by (subst SUP_commute) (simp add: inf_SUP SUP_inf)
   4.204 +
   4.205 +end
   4.206 +
   4.207 +context complete_boolean_algebra
   4.208 +begin
   4.209 +
   4.210 +lemma dual_complete_boolean_algebra:
   4.211 +  "class.complete_boolean_algebra Sup Inf sup (\<ge>) (>) inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
   4.212 +  by (rule class.complete_boolean_algebra.intro,
   4.213 +      rule dual_complete_distrib_lattice,
   4.214 +      rule dual_boolean_algebra)
   4.215 +end
   4.216 +
   4.217 +
   4.218 +
   4.219 +instantiation "set" :: (type) complete_distrib_lattice
   4.220 +begin
   4.221 +instance proof (standard, clarsimp)
   4.222 +  fix A :: "(('a set) set) set"
   4.223 +  fix x::'a
   4.224 +  define F where "F = (\<lambda> Y . (SOME X . (Y \<in> A \<and> X \<in> Y \<and> x \<in> X)))"
   4.225 +  assume A: "\<forall>xa\<in>A. \<exists>X\<in>xa. x \<in> X"
   4.226 +    
   4.227 +  from this have B: " (\<forall>xa \<in> F ` A. x \<in> xa)"
   4.228 +    apply (safe, simp add: F_def)
   4.229 +    by (rule someI2_ex, auto)
   4.230 +    
   4.231 +  have "(\<exists>f. F ` A  = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y))"
   4.232 +    apply (rule_tac x = "F" in exI, simp add: F_def, safe)
   4.233 +    using A by (rule_tac someI2_ex, auto)
   4.234 +    
   4.235 +  from B and this show "\<exists>X. (\<exists>f. X = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>xa\<in>X. x \<in> xa)"
   4.236 +    by auto
   4.237 +qed
   4.238 +end
   4.239 +
   4.240 +instance "set" :: (type) complete_boolean_algebra ..
   4.241 +
   4.242 +instantiation "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice
   4.243 +begin
   4.244 +instance by standard (simp add: le_fun_def INF_SUP_set)
   4.245 +end
   4.246 +
   4.247 +instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
   4.248 +
   4.249 +context complete_linorder
   4.250 +begin
   4.251 +  
   4.252 +subclass complete_distrib_lattice
   4.253 +proof (standard, rule ccontr)
   4.254 +  fix A
   4.255 +  assume "\<not> INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
   4.256 +  from this have C: "INFIMUM A Sup > SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
   4.257 +    using local.not_le by blast
   4.258 +  show "False"
   4.259 +    proof (cases "\<exists> z . INFIMUM A Sup > z \<and> z > SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf")
   4.260 +      case True
   4.261 +      from this obtain z where A: "z < INFIMUM A Sup" and X: "SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < z"
   4.262 +        by blast
   4.263 +          
   4.264 +      from A have "\<And> Y . Y \<in> A \<Longrightarrow> z < Sup Y"
   4.265 +        by (simp add: less_INF_D)
   4.266 +    
   4.267 +      from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k \<in>Y . z < k"
   4.268 +        using local.less_Sup_iff by blast
   4.269 +          
   4.270 +      define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> z < k)"
   4.271 +        
   4.272 +      have D: "\<And> Y . Y \<in> A \<Longrightarrow> z < F Y"
   4.273 +        using B by (simp add: F_def, rule_tac someI2_ex, auto)
   4.274 +    
   4.275 +      have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
   4.276 +        using B by (simp add: F_def, rule_tac someI2_ex, auto)
   4.277 +    
   4.278 +      have "z \<le> Inf (F ` A)"
   4.279 +        by (simp add: D local.INF_greatest local.order.strict_implies_order)
   4.280 +    
   4.281 +      also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
   4.282 +        apply (rule SUP_upper, safe)
   4.283 +        using E by blast
   4.284 +      finally have "z \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
   4.285 +        by simp
   4.286 +          
   4.287 +      from X and this show ?thesis
   4.288 +        using local.not_less by blast
   4.289 +    next
   4.290 +      case False
   4.291 +      from this have A: "\<And> z . INFIMUM A Sup \<le> z \<or> z \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
   4.292 +        using local.le_less_linear by blast
   4.293 +          
   4.294 +      from C have "\<And> Y . Y \<in> A \<Longrightarrow> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < Sup Y"
   4.295 +        by (simp add: less_INF_D)
   4.296 +    
   4.297 +      from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k \<in>Y . SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < k"
   4.298 +        using local.less_Sup_iff by blast
   4.299 +          
   4.300 +      define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < k)"
   4.301 +        
   4.302 +      have D: "\<And> Y . Y \<in> A \<Longrightarrow> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < F Y"
   4.303 +        using B by (simp add: F_def, rule_tac someI2_ex, auto)
   4.304 +    
   4.305 +      have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
   4.306 +        using B by (simp add: F_def, rule_tac someI2_ex, auto)
   4.307 +          
   4.308 +      have "\<And> Y . Y \<in> A \<Longrightarrow> INFIMUM A Sup \<le> F Y"
   4.309 +        using D False local.leI by blast
   4.310 +         
   4.311 +      from this have "INFIMUM A Sup \<le> Inf (F ` A)"
   4.312 +        by (simp add: local.INF_greatest)
   4.313 +          
   4.314 +      also have "Inf (F ` A) \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
   4.315 +        apply (rule SUP_upper, safe)
   4.316 +        using E by blast
   4.317 +          
   4.318 +      finally have "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
   4.319 +        by simp
   4.320 +        
   4.321 +      from C and this show ?thesis
   4.322 +        using local.not_less by blast
   4.323 +    qed
   4.324 +  qed
   4.325 +end
   4.326 +
   4.327 +
   4.328 +
   4.329 +end
     5.1 --- a/src/HOL/Library/FSet.thy	Mon Mar 12 08:25:35 2018 +0000
     5.2 +++ b/src/HOL/Library/FSet.thy	Mon Mar 12 20:52:53 2018 +0100
     5.3 @@ -149,8 +149,7 @@
     5.4    parametric right_total_Compl_transfer Compl_transfer by simp
     5.5  
     5.6  instance
     5.7 -  by (standard; transfer) (simp_all add: Diff_eq)
     5.8 -
     5.9 +  by (standard; transfer) (simp_all add: Inf_Sup Diff_eq)
    5.10  end
    5.11  
    5.12  abbreviation fUNIV :: "'a::finite fset" where "fUNIV \<equiv> top"
     6.1 --- a/src/HOL/Library/Finite_Lattice.thy	Mon Mar 12 08:25:35 2018 +0000
     6.2 +++ b/src/HOL/Library/Finite_Lattice.thy	Mon Mar 12 20:52:53 2018 +0100
     6.3 @@ -167,11 +167,21 @@
     6.4    "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
     6.5    using finite [of A] by induct (simp_all add: inf_sup_distrib1)
     6.6  
     6.7 -instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
     6.8 -proof
     6.9 -qed (auto simp:
    6.10 -  finite_distrib_lattice_complete_sup_Inf
    6.11 -  finite_distrib_lattice_complete_inf_Sup)
    6.12 +context finite_distrib_lattice_complete
    6.13 +begin
    6.14 +subclass finite_distrib_lattice
    6.15 +  apply standard
    6.16 +  apply (simp_all add: Inf_def Sup_def bot_def top_def)
    6.17 +       apply (metis (mono_tags) insert_UNIV local.Sup_fin.eq_fold local.bot_def local.finite_UNIV local.top_def) 
    6.18 +      apply (simp add: comp_fun_idem.fold_insert_idem local.comp_fun_idem_inf) 
    6.19 +     apply (metis (mono_tags) insert_UNIV local.Inf_fin.eq_fold local.finite_UNIV) 
    6.20 +    apply (simp add: comp_fun_idem.fold_insert_idem local.comp_fun_idem_sup)
    6.21 +  apply (metis (mono_tags) insert_UNIV local.Inf_fin.eq_fold local.finite_UNIV) 
    6.22 +  apply (metis (mono_tags) insert_UNIV local.Sup_fin.eq_fold local.finite_UNIV)
    6.23 +  done
    6.24 +end
    6.25 +
    6.26 +instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice ..
    6.27  
    6.28  text \<open>The product of two finite distributive lattices
    6.29  is already a finite distributive lattice.\<close>
    6.30 @@ -189,7 +199,6 @@
    6.31    (finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete
    6.32    ..
    6.33  
    6.34 -
    6.35  subsection \<open>Linear Orders\<close>
    6.36  
    6.37  text \<open>A linear order is a distributive lattice.
     7.1 --- a/src/HOL/Library/Option_ord.thy	Mon Mar 12 08:25:35 2018 +0000
     7.2 +++ b/src/HOL/Library/Option_ord.thy	Mon Mar 12 20:52:53 2018 +0100
     7.3 @@ -283,60 +283,148 @@
     7.4    "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
     7.5    using Some_Sup [of "f ` A"] by (simp add: comp_def)
     7.6  
     7.7 -instance option :: (complete_distrib_lattice) complete_distrib_lattice
     7.8 -proof
     7.9 -  fix a :: "'a option" and B
    7.10 -  show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
    7.11 -  proof (cases a)
    7.12 -    case None
    7.13 -    then show ?thesis by simp
    7.14 +lemma option_Inf_Sup: "INFIMUM (A::('a::complete_distrib_lattice option) set set) Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
    7.15 +proof (cases "{} \<in> A")
    7.16 +  case True
    7.17 +  then show ?thesis
    7.18 +    by (rule_tac i = "{}" in INF_lower2, simp_all)
    7.19 +next
    7.20 +  case False
    7.21 +  from this have X: "{} \<notin> A"
    7.22 +    by simp
    7.23 +  then show ?thesis
    7.24 +  proof (cases "{None} \<in> A")
    7.25 +    case True
    7.26 +    then show ?thesis
    7.27 +      by (rule_tac i = "{None}" in INF_lower2, simp_all)
    7.28    next
    7.29 -    case (Some c)
    7.30 -    show ?thesis
    7.31 -    proof (cases "None \<in> B")
    7.32 -      case True
    7.33 -      then have "Some c = (\<Sqinter>b\<in>B. Some c \<squnion> b)"
    7.34 -        by (auto intro!: antisym INF_lower2 INF_greatest)
    7.35 -      with True Some show ?thesis by simp
    7.36 -    next
    7.37 -      case False then have B: "{x \<in> B. \<exists>y. x = Some y} = B" by auto (metis not_Some_eq)
    7.38 -      from sup_Inf have "Some c \<squnion> Some (\<Sqinter>Option.these B) = Some (\<Sqinter>b\<in>Option.these B. c \<squnion> b)" by simp
    7.39 -      then have "Some c \<squnion> \<Sqinter>(Some ` Option.these B) = (\<Sqinter>x\<in>Some ` Option.these B. Some c \<squnion> x)"
    7.40 -        by (simp add: Some_INF Some_Inf comp_def)
    7.41 -      with Some B show ?thesis by (simp add: Some_image_these_eq cong del: strong_INF_cong)
    7.42 -    qed
    7.43 -  qed
    7.44 -  show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
    7.45 -  proof (cases a)
    7.46 -    case None
    7.47 -    then show ?thesis by (simp add: image_constant_conv bot_option_def cong del: strong_SUP_cong)
    7.48 -  next
    7.49 -    case (Some c)
    7.50 -    show ?thesis
    7.51 -    proof (cases "B = {} \<or> B = {None}")
    7.52 -      case True
    7.53 -      then show ?thesis by auto
    7.54 -    next
    7.55 -      have B: "B = {x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None}"
    7.56 -        by auto
    7.57 -      then have Sup_B: "\<Squnion>B = \<Squnion>({x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None})"
    7.58 -        and SUP_B: "\<And>f. (\<Squnion>x \<in> B. f x) = (\<Squnion>x \<in> {x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None}. f x)"
    7.59 -        by simp_all
    7.60 -      have Sup_None: "\<Squnion>{x. x = None \<and> x \<in> B} = None"
    7.61 -        by (simp add: bot_option_def [symmetric])
    7.62 -      have SUP_None: "(\<Squnion>x\<in>{x. x = None \<and> x \<in> B}. Some c \<sqinter> x) = None"
    7.63 -        by (simp add: bot_option_def [symmetric])
    7.64 -      case False then have "Option.these B \<noteq> {}" by (simp add: these_not_empty_eq)
    7.65 -      moreover from inf_Sup have "Some c \<sqinter> Some (\<Squnion>Option.these B) = Some (\<Squnion>b\<in>Option.these B. c \<sqinter> b)"
    7.66 -        by simp
    7.67 -      ultimately have "Some c \<sqinter> \<Squnion>(Some ` Option.these B) = (\<Squnion>x\<in>Some ` Option.these B. Some c \<sqinter> x)"
    7.68 -        by (simp add: Some_SUP Some_Sup comp_def)
    7.69 -      with Some show ?thesis
    7.70 -        by (simp add: Some_image_these_eq Sup_B SUP_B Sup_None SUP_None SUP_union Sup_union_distrib cong del: strong_SUP_cong)
    7.71 -    qed
    7.72 +    case False
    7.73 +    have "\<And> y . y\<in>A \<Longrightarrow> Sup (y - {None}) = Sup y"
    7.74 +      by (metis (no_types, lifting) Sup_option_def insert_Diff_single these_insert_None these_not_empty_eq)
    7.75 +   
    7.76 +    from this have A: "Sup ` A = (Sup ` {y - {None} | y. y\<in>A})"
    7.77 +      apply (simp add: image_def, simp, safe)
    7.78 +       apply (rule_tac x = "xa - {None}" in exI, simp, blast)
    7.79 +      by blast
    7.80 +
    7.81 +    have [simp]: "\<And>y. y \<in> A \<Longrightarrow> \<exists>ya. {ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x} 
    7.82 +          = {y. \<exists>x\<in>ya - {None}. y = the x} \<and> ya \<in> A"
    7.83 +      by (rule_tac x = "y" in exI, auto)
    7.84 +
    7.85 +    have [simp]: "\<And>y. y \<in> A \<Longrightarrow>
    7.86 +         (\<exists>ya. y - {None} = ya - {None} \<and> ya \<in> A) \<and> \<Squnion>{ya. \<exists>x\<in>y - {None}. ya = the x} 
    7.87 +          = \<Squnion>{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}"
    7.88 +      apply safe
    7.89 +       apply blast
    7.90 +      apply (rule_tac f = Sup in arg_cong)
    7.91 +      by auto
    7.92 +
    7.93 +    have C: "(\<lambda>x.  (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A} =  (Sup ` {the ` (y - {None}) |y. y \<in> A})"
    7.94 +      apply (simp add: image_def Option.these_def, safe)
    7.95 +       apply (rule_tac x = "{ya. \<exists>x. x \<in> y - {None} \<and> (\<exists>y. x = Some y) \<and> ya = the x}" in exI, simp)
    7.96 +      by (rule_tac x = "y -{None}" in exI, simp)
    7.97 +  
    7.98 +    have D: "\<forall> f . \<exists>Y\<in>A. f Y \<notin> Y \<Longrightarrow> False"
    7.99 +      apply (drule_tac x = "\<lambda> Y . SOME x . x \<in> Y" in spec, safe)
   7.100 +      by (simp add: X some_in_eq)
   7.101 +  
   7.102 +    define F where "F = (\<lambda> Y . SOME x::'a option . x \<in> (Y - {None}))"
   7.103 +  
   7.104 +    have G: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> x . x \<in> Y - {None}"
   7.105 +      by (metis False X all_not_in_conv insert_Diff_single these_insert_None these_not_empty_eq)
   7.106 +  
   7.107 +    have F: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> (Y - {None})"
   7.108 +      by (metis F_def G empty_iff some_in_eq)
   7.109 +  
   7.110 +    have "Some \<bottom> \<le> Inf (F ` A)"
   7.111 +      by (metis (no_types, lifting) Diff_iff F Inf_option_def bot.extremum image_iff 
   7.112 +          less_eq_option_Some singletonI)
   7.113 +      
   7.114 +    from this have "Inf (F ` A) \<noteq> None"
   7.115 +      by (case_tac "\<Sqinter>x\<in>A. F x", simp_all)
   7.116 +  
   7.117 +    from this have "\<exists> x . x \<noteq> None \<and> x \<in> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
   7.118 +      apply (rule_tac x = "Inf (F ` A)" in exI, simp add: image_def, safe)
   7.119 +      apply (rule_tac x = "F `  A" in exI, safe)
   7.120 +      using F by auto
   7.121 +  
   7.122 +    from this have E:" Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} = {None} \<Longrightarrow> False"
   7.123 +      by blast
   7.124 +
   7.125 +    have [simp]: "((\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x) = None) = False"
   7.126 +      by (metis (no_types, lifting) E Sup_option_def \<open>\<exists>x. x \<noteq> None \<and> x \<in> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}\<close> 
   7.127 +          ex_in_conv option.simps(3))
   7.128 +  
   7.129 +    have B: "Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}) 
   7.130 +        = ((\<lambda>x. (\<Squnion> Option.these x)) ` {y - {None} |y. y \<in> A})"
   7.131 +      by (metis image_image these_image_Some_eq)
   7.132 +
   7.133 +    have [simp]: "\<And>f. \<forall>Y. (\<exists>y. Y = {ya. \<exists>x\<in>y - {None}. ya = the x} \<and> y \<in> A) \<longrightarrow> f Y \<in> Y \<Longrightarrow>
   7.134 +         \<exists>x. (\<exists>f. x = {y. \<exists>x\<in>A. y = f x} \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x})) = \<Sqinter>x"
   7.135 +      apply (rule_tac x = "{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) | x . x\<in> A}" in exI, safe)
   7.136 +       apply (rule_tac x = "(\<lambda> Y . Some (f (the ` (Y - {None})))) " in exI, safe)
   7.137 +         apply (rule_tac x = xa in bexI, simp add: image_def, simp)
   7.138 +        apply (rule_tac x = xa in exI, simp add: image_def)
   7.139 +       apply(drule_tac x = "(the ` (Y - {None}))" in spec)
   7.140 +       apply (simp add: image_def,safe, simp)
   7.141 +      using option.collapse apply fastforce
   7.142 +      by (simp add: Setcompr_eq_image)
   7.143 +
   7.144 +    have [simp]: "\<And>f. \<forall>Y. (\<exists>y. Y = {ya. \<exists>x\<in>y - {None}. ya = the x} \<and> y \<in> A) \<longrightarrow> f Y \<in> Y 
   7.145 +        \<Longrightarrow> \<exists>y. (\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x})) = Some y"
   7.146 +      by (metis (no_types) Some_INF)
   7.147 +
   7.148 +    have [simp]: "\<And> f.
   7.149 +         (\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> the (\<Sqinter>Y\<in>A. Some (f (the ` (Y - {None}))))"
   7.150 +      apply (simp add: Inf_option_def, safe)
   7.151 +      apply (rule Inf_greatest, simp add: image_def Option.these_def, safe)
   7.152 +      apply (rule_tac i = " {y. \<exists>x\<in>xb - {None}. y = the x}" in INF_lower2)
   7.153 +       apply simp_all
   7.154 +      by blast
   7.155 +
   7.156 +    have X: "\<And> f . \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y
   7.157 +      \<Longrightarrow> (\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> \<Squnion>Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
   7.158 +      apply (rule_tac u = "the (Inf ((\<lambda> Y . Some (f (the ` (Y - {None})) )) ` A))" in Sup_upper2)
   7.159 +       apply (simp add:  Option.these_def image_def)
   7.160 +       apply (rule_tac x = "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x}))" in exI, simp)
   7.161 +      by simp
   7.162 +
   7.163 +    have "(Inf (Sup `A)) = (Inf (Sup ` {y - {None} | y. y\<in>A}))"
   7.164 +      by (subst A, simp)
   7.165 +
   7.166 +    also have "... = (\<Sqinter>x\<in>{y - {None} |y. y \<in> A}. if x = {} \<or> x = {None} then None else Some (\<Squnion>Option.these x))"
   7.167 +      by (simp add: Sup_option_def)
   7.168 +
   7.169 +    also have "... = (\<Sqinter>x\<in>{y - {None} |y. y \<in> A}. Some (\<Squnion>Option.these x))"
   7.170 +      apply (subgoal_tac "\<And> x . x\<in>{y - {None} |y. y \<in> A} \<Longrightarrow>  x \<noteq> {} \<and> x \<noteq> {None}", simp)
   7.171 +      using G by fastforce
   7.172 +  
   7.173 +    also have "... = Some (\<Sqinter>Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}))"
   7.174 +      by (simp add: Inf_option_def, safe)
   7.175 +  
   7.176 +    also have "... =  Some (\<Sqinter> ((\<lambda>x.  (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}))"
   7.177 +      by (simp add: B)
   7.178 +  
   7.179 +    also have "... = Some (Inf (Sup ` {the ` (y - {None}) |y. y \<in> A}))"
   7.180 +      by (unfold C, simp)
   7.181 +    thm Inf_Sup
   7.182 +    also have "... = Some (\<Squnion>x\<in>{f ` {the ` (y - {None}) |y. y \<in> A} |f. \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y}. \<Sqinter>x) "
   7.183 +      by (simp add: Inf_Sup)
   7.184 +  
   7.185 +    also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
   7.186 +      apply (simp add: less_eq_option_def)
   7.187 +      apply (case_tac "\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x", simp_all)
   7.188 +      apply (rule Sup_least, safe)
   7.189 +      apply (simp add: Sup_option_def)
   7.190 +      apply (case_tac "(\<forall>f. \<exists>Y\<in>A. f Y \<notin> Y) \<or> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} = {None}", simp_all)
   7.191 +      by (drule X, simp)
   7.192 +    finally show ?thesis by simp
   7.193    qed
   7.194  qed
   7.195  
   7.196 +instance option :: (complete_distrib_lattice) complete_distrib_lattice
   7.197 +  by (standard, simp add: option_Inf_Sup)
   7.198 +
   7.199  instance option :: (complete_linorder) complete_linorder ..
   7.200  
   7.201  
     8.1 --- a/src/HOL/Library/Product_Order.thy	Mon Mar 12 08:25:35 2018 +0000
     8.2 +++ b/src/HOL/Library/Product_Order.thy	Mon Mar 12 20:52:53 2018 +0100
     8.3 @@ -233,14 +233,10 @@
     8.4  (* Contribution: Alessandro Coglio *)
     8.5  
     8.6  instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
     8.7 -proof (standard, goal_cases)
     8.8 -  case 1
     8.9 -  then show ?case
    8.10 -    by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)
    8.11 -next
    8.12 -  case 2
    8.13 -  then show ?case
    8.14 -    by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP comp_def)
    8.15 +proof
    8.16 +  fix A::"('a\<times>'b) set set"
    8.17 +  show "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
    8.18 +    by (simp add: Sup_prod_def Inf_prod_def INF_SUP_set)
    8.19  qed
    8.20  
    8.21  subsection \<open>Bekic's Theorem\<close>
     9.1 --- a/src/HOL/Predicate.thy	Mon Mar 12 08:25:35 2018 +0000
     9.2 +++ b/src/HOL/Predicate.thy	Mon Mar 12 20:52:53 2018 +0100
     9.3 @@ -102,6 +102,18 @@
     9.4    by (simp add: minus_pred_def)
     9.5  
     9.6  instance proof
     9.7 +  fix A::"'a pred set set"
     9.8 +  show "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
     9.9 +  proof (simp add: less_eq_pred_def Sup_fun_def Inf_fun_def, safe)
    9.10 +    fix w
    9.11 +    assume A: "\<forall>x\<in>A. \<exists>f\<in>x. eval f w"
    9.12 +    define F where "F = (\<lambda> x . SOME f . f \<in> x \<and> eval f w)"
    9.13 +    have [simp]: "(\<forall>f\<in> (F ` A). eval f w)"
    9.14 +      by (metis (no_types, lifting) A F_def image_iff some_eq_ex)
    9.15 +    show "\<exists>x. (\<exists>f. x = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>f\<in>x. eval f w)"
    9.16 +      apply (rule_tac x = "F ` A" in exI, simp)
    9.17 +      using A by (metis (no_types, lifting) F_def someI)+
    9.18 +  qed
    9.19  qed (auto intro!: pred_eqI)
    9.20  
    9.21  end