--- a/src/HOL/Analysis/Polytope.thy Mon Mar 12 08:25:35 2018 +0000
+++ b/src/HOL/Analysis/Polytope.thy Mon Mar 12 20:52:53 2018 +0100
@@ -735,7 +735,11 @@
show ?thesis
proof (cases "Q = {}")
case True then show ?thesis
+ sledgehammer
+ by (metis IntQ Inter_UNIV_conv(2) assms(1) assms(2) ex_in_conv)
+(*
by (metis Inf_empty Inf_lower IntQ assms ex_in_conv subset_antisym top_greatest)
+*)
next
case False
have "Q \<subseteq> {T. T exposed_face_of S}"
--- a/src/HOL/Complete_Lattices.thy Mon Mar 12 08:25:35 2018 +0000
+++ b/src/HOL/Complete_Lattices.thy Mon Mar 12 20:52:53 2018 +0100
@@ -3,6 +3,7 @@
Author: Lawrence C Paulson
Author: Markus Wenzel
Author: Florian Haftmann
+ Author: Viorel Preoteasa (Complete Distributive Lattices)
*)
section \<open>Complete lattices\<close>
@@ -453,56 +454,43 @@
end
-class complete_distrib_lattice = complete_lattice +
- assumes sup_Inf: "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
- and inf_Sup: "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
+context complete_lattice
begin
-
-lemma sup_INF: "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
- by (simp add: sup_Inf)
+lemma Sup_Inf_le: "Sup (Inf ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)}) \<le> Inf (Sup ` A)"
+ by (rule SUP_least, clarify, rule INF_greatest, simp add: INF_lower2 Sup_upper)
+end
-lemma inf_SUP: "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
- by (simp add: inf_Sup)
-
-lemma dual_complete_distrib_lattice:
- "class.complete_distrib_lattice Sup Inf sup (\<ge>) (>) inf \<top> \<bottom>"
- apply (rule class.complete_distrib_lattice.intro)
- apply (fact dual_complete_lattice)
- apply (rule class.complete_distrib_lattice_axioms.intro)
- apply (simp_all add: inf_Sup sup_Inf)
- done
+class complete_distrib_lattice = complete_lattice +
+ assumes Inf_Sup_le: "Inf (Sup ` A) \<le> Sup (Inf ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)})"
+begin
+
+lemma Inf_Sup: "Inf (Sup ` A) = Sup (Inf ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)})"
+ by (rule antisym, rule Inf_Sup_le, rule Sup_Inf_le)
subclass distrib_lattice
proof
fix a b c
- have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" by (rule sup_Inf)
- then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by simp
+ show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)"
+ proof (rule antisym, simp_all, safe)
+ show "b \<sqinter> c \<le> a \<squnion> b"
+ by (rule le_infI1, simp)
+ show "b \<sqinter> c \<le> a \<squnion> c"
+ by (rule le_infI2, simp)
+ have [simp]: "a \<sqinter> c \<le> a \<squnion> b \<sqinter> c"
+ by (rule le_infI1, simp)
+ have [simp]: "b \<sqinter> a \<le> a \<squnion> b \<sqinter> c"
+ by (rule le_infI2, simp)
+ 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"
+ by (rule Inf_Sup)
+ from this show "(a \<squnion> b) \<sqinter> (a \<squnion> c) \<le> a \<squnion> b \<sqinter> c"
+ apply simp
+ by (rule SUP_least, safe, simp_all)
+ qed
qed
-
-lemma Inf_sup: "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
- by (simp add: sup_Inf sup_commute)
-
-lemma Sup_inf: "\<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)"
- by (simp add: inf_Sup inf_commute)
-
-lemma INF_sup: "(\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)"
- by (simp add: sup_INF sup_commute)
+end
-lemma SUP_inf: "(\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)"
- by (simp add: inf_SUP inf_commute)
-
-lemma Inf_sup_eq_top_iff: "(\<Sqinter>B \<squnion> a = \<top>) \<longleftrightarrow> (\<forall>b\<in>B. b \<squnion> a = \<top>)"
- by (simp only: Inf_sup INF_top_conv)
-
-lemma Sup_inf_eq_bot_iff: "(\<Squnion>B \<sqinter> a = \<bottom>) \<longleftrightarrow> (\<forall>b\<in>B. b \<sqinter> a = \<bottom>)"
- by (simp only: Sup_inf SUP_bot_conv)
-
-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)"
- by (subst INF_commute) (simp add: sup_INF INF_sup)
-
-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)"
- by (subst SUP_commute) (simp add: inf_SUP SUP_inf)
-
+context complete_lattice
+begin
context
fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
assumes "mono f"
@@ -527,12 +515,6 @@
class complete_boolean_algebra = boolean_algebra + complete_distrib_lattice
begin
-lemma dual_complete_boolean_algebra:
- "class.complete_boolean_algebra Sup Inf sup (\<ge>) (>) inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
- by (rule class.complete_boolean_algebra.intro,
- rule dual_complete_distrib_lattice,
- rule dual_boolean_algebra)
-
lemma uminus_Inf: "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
proof (rule antisym)
show "- \<Sqinter>A \<le> \<Squnion>(uminus ` A)"
@@ -639,18 +621,8 @@
lemma le_SUP_iff: "x \<le> SUPREMUM A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
using le_Sup_iff [of _ "f ` A"] by simp
-subclass complete_distrib_lattice
-proof
- fix a and B
- show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)" and "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
- by (safe intro!: INF_eqI [symmetric] sup_mono Inf_lower SUP_eqI [symmetric] inf_mono Sup_upper)
- (auto simp: not_less [symmetric] Inf_less_iff less_Sup_iff
- le_max_iff_disj complete_linorder_sup_max min_le_iff_disj complete_linorder_inf_min)
-qed
-
end
-
subsection \<open>Complete lattice on @{typ bool}\<close>
instantiation bool :: complete_lattice
@@ -678,8 +650,7 @@
by (simp add: fun_eq_iff)
instance bool :: complete_boolean_algebra
- by standard (auto intro: bool_induct)
-
+ by (standard, fastforce)
subsection \<open>Complete lattice on @{typ "_ \<Rightarrow> _"}\<close>
@@ -721,12 +692,6 @@
lemma SUP_apply [simp]: "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
using Sup_apply [of "f ` A"] by (simp add: comp_def)
-instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice
- by standard (auto simp add: inf_Sup sup_Inf fun_eq_iff image_image)
-
-instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
-
-
subsection \<open>Complete lattice on unary and binary predicates\<close>
lemma Inf1_I: "(\<And>P. P \<in> A \<Longrightarrow> P a) \<Longrightarrow> (\<Sqinter>A) a"
@@ -820,10 +785,6 @@
end
-instance "set" :: (type) complete_boolean_algebra
- by standard (auto simp add: Inf_set_def Sup_set_def image_def)
-
-
subsubsection \<open>Inter\<close>
abbreviation Inter :: "'a set set \<Rightarrow> 'a set" ("\<Inter>_" [900] 900)
@@ -1218,13 +1179,13 @@
subsubsection \<open>Distributive laws\<close>
lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
- by (fact inf_Sup)
+ by blast
lemma Un_Inter: "A \<union> \<Inter>B = (\<Inter>C\<in>B. A \<union> C)"
- by (fact sup_Inf)
+ by blast
lemma Int_Union2: "\<Union>B \<inter> A = (\<Union>C\<in>B. C \<inter> A)"
- by (fact Sup_inf)
+ by blast
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)"
by (rule sym) (rule INF_inf_distrib)
@@ -1241,20 +1202,20 @@
by (simp add: UN_Un_distrib)
lemma Un_INT_distrib: "B \<union> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. B \<union> A i)"
- by (fact sup_INF)
+ by blast
lemma Int_UN_distrib: "B \<inter> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. B \<inter> A i)"
\<comment> \<open>Halmos, Naive Set Theory, page 35.\<close>
- by (fact inf_SUP)
+ by blast
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)"
- by (fact SUP_inf_distrib2)
+ by blast
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)"
- by (fact INF_sup_distrib2)
+ by blast
lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})"
- by (fact Sup_inf_eq_bot_iff)
+ by blast
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)"
by (rule order_antisym) (blast intro: SUP_least SUP_upper2)+
@@ -1354,11 +1315,10 @@
subsubsection \<open>Complement\<close>
lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
- by (fact uminus_INF)
+ by blast
lemma Compl_UN [simp]: "- (\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
- by (fact uminus_SUP)
-
+ by blast
subsubsection \<open>Miniscoping and maxiscoping\<close>
--- a/src/HOL/Enum.thy Mon Mar 12 08:25:35 2018 +0000
+++ b/src/HOL/Enum.thy Mon Mar 12 20:52:53 2018 +0100
@@ -678,10 +678,9 @@
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)
end
-instance finite_2 :: complete_distrib_lattice
- by standard (auto simp add: sup_finite_2_def inf_finite_2_def Inf_finite_2_def Sup_finite_2_def)
+instance finite_2 :: complete_linorder ..
-instance finite_2 :: complete_linorder ..
+instance finite_2 :: complete_distrib_lattice ..
instantiation finite_2 :: "{field, idom_abs_sgn, idom_modulo}" begin
definition [simp]: "0 = a\<^sub>1"
@@ -783,7 +782,101 @@
from this[symmetric] show "wf \<dots>" by simp
qed intro_classes
-instantiation finite_3 :: complete_lattice
+class finite_lattice = finite + lattice + Inf + Sup + bot + top +
+ assumes Inf_finite_empty: "Inf {} = Sup UNIV"
+ assumes Inf_finite_insert: "Inf (insert a A) = a \<sqinter> Inf A"
+ assumes Sup_finite_empty: "Sup {} = Inf UNIV"
+ assumes Sup_finite_insert: "Sup (insert a A) = a \<squnion> Sup A"
+ assumes bot_finite_def: "bot = Inf UNIV"
+ assumes top_finite_def: "top = Sup UNIV"
+begin
+
+subclass complete_lattice
+proof
+ fix x A
+ show "x \<in> A \<Longrightarrow> \<Sqinter>A \<le> x"
+ by (cut_tac A = A and a = x in Inf_finite_insert, simp add: insert_absorb inf.absorb_iff2)
+ show "x \<in> A \<Longrightarrow> x \<le> \<Squnion>A"
+ by (cut_tac A = A and a = x in Sup_finite_insert, simp add: insert_absorb sup.absorb_iff2)
+next
+ fix A z
+ show "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A"
+ 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)
+ by(cut_tac A = UNIV and a = z in Sup_finite_insert, simp add: insert_UNIV local.sup.absorb_iff2)
+
+ show " (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z"
+ 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)
+ by(cut_tac A = UNIV and a = z in Inf_finite_insert, simp add: insert_UNIV local.inf.absorb_iff2)
+next
+ show "\<Sqinter>{} = \<top>"
+ by (simp add: Inf_finite_empty top_finite_def)
+ show " \<Squnion>{} = \<bottom>"
+ by (simp add: Sup_finite_empty bot_finite_def)
+qed
+end
+
+class finite_distrib_lattice = finite_lattice + distrib_lattice
+begin
+lemma finite_inf_Sup: "a \<sqinter> (Sup A) = Sup {a \<sqinter> b | b . b \<in> A}"
+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)
+ fix x::"'a"
+ fix F
+ assume "x \<notin> F"
+ assume A: "a \<sqinter> \<Squnion>F = \<Squnion>{a \<sqinter> b |b. b \<in> F}"
+
+ have [simp]: " insert (a \<sqinter> x) {a \<sqinter> b |b. b \<in> F} = {a \<sqinter> b |b. b = x \<or> b \<in> F}"
+ by auto
+
+ have "a \<sqinter> (x \<squnion> \<Squnion>F) = a \<sqinter> x \<squnion> a \<sqinter> \<Squnion>F"
+ by (simp add: inf_sup_distrib1)
+ also have "... = a \<sqinter> x \<squnion> \<Squnion>{a \<sqinter> b |b. b \<in> F}"
+ by (simp add: A)
+ also have "... = \<Squnion>{a \<sqinter> b |b. b = x \<or> b \<in> F}"
+ by (unfold Sup_insert[THEN sym], simp)
+
+ finally show "a \<sqinter> (x \<squnion> \<Squnion>F) = \<Squnion>{a \<sqinter> b |b. b = x \<or> b \<in> F}"
+ by simp
+qed
+
+lemma finite_Inf_Sup: "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+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)
+ fix x::"'a set"
+ fix F
+ assume "x \<notin> F"
+ 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)}"
+ by auto
+ 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)"
+ apply (rule_tac x = "(\<lambda> Y . (if Y = x then b else f Y))" in exI)
+ by auto
+ 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"
+ apply (rule_tac i = "(\<lambda> Y . (if Y = x then b else f Y)) ` ({x} \<union> F)" in SUP_upper2, simp)
+ apply (subst inf_commute)
+ by (simp add: INF_greatest Inf_lower inf.coboundedI2)
+
+ assume "INFIMUM F Sup \<le> SUPREMUM {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} Inf"
+
+ 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"
+ apply simp
+ using inf.coboundedI2 by blast
+ also have "... = Sup {\<Squnion>x \<sqinter> (Inf (f ` F)) |f . (\<forall>Y\<in>F. f Y \<in> Y)}"
+ by (simp add: finite_inf_Sup)
+
+ also have "... = Sup {Sup {Inf (f ` F) \<sqinter> b | b . b \<in> x} |f . (\<forall>Y\<in>F. f Y \<in> Y)}"
+ apply (subst inf_commute)
+ by (simp add: finite_inf_Sup)
+
+ also have "... \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
+ by (rule Sup_least, clarsimp, rule Sup_least, clarsimp)
+
+ 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"
+ by simp
+qed
+
+subclass complete_distrib_lattice
+ by (standard, rule finite_Inf_Sup)
+end
+
+instantiation finite_3 :: finite_lattice
begin
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)"
@@ -795,38 +888,16 @@
instance
proof
- fix x :: finite_3 and A
- assume "x \<in> A"
- then show "\<Sqinter>A \<le> x" "x \<le> \<Squnion>A"
- by(case_tac [!] x)(auto simp add: Inf_finite_3_def Sup_finite_3_def less_eq_finite_3_def less_finite_3_def)
-next
- fix A and z :: finite_3
- assume "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
- then show "z \<le> \<Sqinter>A"
- by(cases z)(auto simp add: Inf_finite_3_def less_eq_finite_3_def less_finite_3_def)
-next
- fix A and z :: finite_3
- assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
- show "\<Squnion>A \<le> z"
- by(auto simp add: Sup_finite_3_def less_eq_finite_3_def less_finite_3_def dest: *)
-qed(auto simp add: Inf_finite_3_def Sup_finite_3_def)
+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)
end
-instance finite_3 :: complete_distrib_lattice
-proof
- fix a :: finite_3 and B
- show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
- proof(cases a "\<Sqinter>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
- case a\<^sub>2_a\<^sub>3
- then have "\<And>x. x \<in> B \<Longrightarrow> x = a\<^sub>3"
- by(case_tac x)(auto simp add: Inf_finite_3_def split: if_split_asm)
- then show ?thesis using a\<^sub>2_a\<^sub>3
- by(auto simp add: Inf_finite_3_def max_def less_eq_finite_3_def less_finite_3_def split: if_split_asm)
- qed (auto simp add: Inf_finite_3_def max_def less_finite_3_def less_eq_finite_3_def split: if_split_asm)
- show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
- by (cases a "\<Squnion>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
- (auto simp add: Sup_finite_3_def min_def less_finite_3_def less_eq_finite_3_def split: if_split_asm)
-qed
+instance finite_3 :: complete_lattice ..
+
+instance finite_3 :: finite_distrib_lattice
+proof
+qed (auto simp add: min_def max_def)
+
+instance finite_3 :: complete_distrib_lattice ..
instance finite_3 :: complete_linorder ..
@@ -910,7 +981,7 @@
end
-instantiation finite_4 :: complete_lattice begin
+instantiation finite_4 :: finite_distrib_lattice begin
text \<open>@{term a\<^sub>1} $<$ @{term a\<^sub>2},@{term a\<^sub>3} $<$ @{term a\<^sub>4},
but @{term a\<^sub>2} and @{term a\<^sub>3} are incomparable.\<close>
@@ -947,38 +1018,22 @@
| (a\<^sub>3, _) \<Rightarrow> a\<^sub>3 | (_, a\<^sub>3) \<Rightarrow> a\<^sub>3
| _ \<Rightarrow> a\<^sub>1)"
-instance
-proof
- fix A and z :: finite_4
- assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
- show "\<Squnion>A \<le> z"
- by(auto simp add: Sup_finite_4_def less_eq_finite_4_def dest!: * split: finite_4.splits)
-next
- fix A and z :: finite_4
- assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
- show "z \<le> \<Sqinter>A"
- by(auto simp add: Inf_finite_4_def less_eq_finite_4_def dest!: * split: finite_4.splits)
-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)
-
+instance proof
+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)
end
-instance finite_4 :: complete_distrib_lattice
-proof
- fix a :: finite_4 and B
- show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
- by(cases a "\<Sqinter>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
- (auto simp add: sup_finite_4_def Inf_finite_4_def split: finite_4.splits if_split_asm)
- show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
- by(cases a "\<Squnion>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
- (auto simp add: inf_finite_4_def Sup_finite_4_def split: finite_4.splits if_split_asm)
-qed
+instance finite_4 :: complete_lattice ..
+
+instance finite_4 :: complete_distrib_lattice ..
instantiation finite_4 :: complete_boolean_algebra begin
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)"
definition "x - y = x \<sqinter> - (y :: finite_4)"
instance
by intro_classes
- (simp_all add: inf_finite_4_def sup_finite_4_def uminus_finite_4_def minus_finite_4_def split: finite_4.splits)
+ (simp_all add: inf_finite_4_def sup_finite_4_def uminus_finite_4_def minus_finite_4_def
+ split: finite_4.splits)
end
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
@@ -1013,7 +1068,7 @@
end
-instantiation finite_5 :: complete_lattice
+instantiation finite_5 :: finite_lattice
begin
text \<open>The non-distributive pentagon lattice $N_5$\<close>
@@ -1065,19 +1120,14 @@
| _ \<Rightarrow> a\<^sub>1)"
instance
-proof intro_classes
- fix A and z :: finite_5
- assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
- show "z \<le> \<Sqinter>A"
- by(auto simp add: less_eq_finite_5_def Inf_finite_5_def split: finite_5.splits if_split_asm dest!: *)
-next
- fix A and z :: finite_5
- assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
- show "\<Squnion>A \<le> z"
- by(auto simp add: less_eq_finite_5_def Sup_finite_5_def split: finite_5.splits if_split_asm dest!: *)
-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)
+proof
+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)
+end
-end
+
+instance finite_5 :: complete_lattice ..
+
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4 a\<^sub>5
--- a/src/HOL/Hilbert_Choice.thy Mon Mar 12 08:25:35 2018 +0000
+++ b/src/HOL/Hilbert_Choice.thy Mon Mar 12 20:52:53 2018 +0100
@@ -1,5 +1,6 @@
(* Title: HOL/Hilbert_Choice.thy
Author: Lawrence C Paulson, Tobias Nipkow
+ Author: Viorel Preoteasa (Results about complete distributive lattices)
Copyright 2001 University of Cambridge
*)
@@ -803,4 +804,319 @@
ML_file "Tools/choice_specification.ML"
+subsection \<open>Complete Distributive Lattices -- Properties depending on Hilbert Choice\<close>
+
+context complete_distrib_lattice
+begin
+lemma Sup_Inf: "Sup (Inf ` A) = Inf (Sup ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)})"
+proof (rule antisym)
+ show "SUPREMUM A Inf \<le> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Sup"
+ apply (rule Sup_least, rule INF_greatest)
+ using Inf_lower2 Sup_upper by auto
+next
+ show "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Sup \<le> SUPREMUM A Inf"
+ proof (simp add: Inf_Sup, rule_tac SUP_least, simp, safe)
+ fix f
+ assume "\<forall>Y. (\<exists>f. Y = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<longrightarrow> f Y \<in> Y"
+ from this have B: "\<And> F . (\<forall> Y \<in> A . F Y \<in> Y) \<Longrightarrow> \<exists> Z \<in> A . f (F ` A) = F Z"
+ by auto
+ show "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> SUPREMUM A Inf"
+ proof (cases "\<exists> Z \<in> A . INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> Inf Z")
+ case True
+ 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"
+ by blast
+ have B: "... \<le> SUPREMUM A Inf"
+ by (simp add: SUP_upper)
+ from A and B show ?thesis
+ by (drule_tac order_trans, simp_all)
+ next
+ case False
+ 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"
+ using Inf_greatest by blast
+ 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)"
+ have C: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
+ using X by (simp add: F_def, rule someI2_ex, auto)
+ 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"
+ using X by (simp add: F_def, rule someI2_ex, auto)
+ from C and B obtain Z where D: "Z \<in> A " and Y: "f (F ` A) = F Z"
+ by blast
+ from E and D have W: "\<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> F Z"
+ by simp
+ from C have "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> f (F ` A)"
+ by (rule_tac INF_lower, blast)
+ from this and W and Y show ?thesis
+ by simp
+ qed
+ qed
+qed
+
+lemma dual_complete_distrib_lattice:
+ "class.complete_distrib_lattice Sup Inf sup (\<ge>) (>) inf \<top> \<bottom>"
+ apply (rule class.complete_distrib_lattice.intro)
+ apply (fact dual_complete_lattice)
+ by (simp add: class.complete_distrib_lattice_axioms_def Sup_Inf)
+
+lemma sup_Inf: "a \<squnion> Inf B = (INF b:B. a \<squnion> b)"
+proof (rule antisym)
+ show "a \<squnion> Inf B \<le> (INF b:B. a \<squnion> b)"
+ using Inf_lower sup.mono by (rule_tac INF_greatest, fastforce)
+next
+ have "(INF b:B. a \<squnion> b) \<le> INFIMUM {{f {a}, f B} |f. f {a} = a \<and> f B \<in> B} Sup"
+ by (rule INF_greatest, auto simp add: INF_lower)
+ also have "... = a \<squnion> Inf B"
+ by (cut_tac A = "{{a}, B}" in Sup_Inf, simp)
+ finally show "(INF b:B. a \<squnion> b) \<le> a \<squnion> Inf B"
+ by simp
+qed
+
+lemma inf_Sup: "a \<sqinter> Sup B = (SUP b:B. a \<sqinter> b)"
+ using dual_complete_distrib_lattice
+ by (rule complete_distrib_lattice.sup_Inf)
+
+lemma INF_SUP: "(INF y. SUP x. ((P x y)::'a)) = (SUP x. INF y. P (x y) y)"
+proof (rule antisym)
+ show "(SUP x. INF y. P (x y) y) \<le> (INF y. SUP x. P x y)"
+ by (rule SUP_least, rule INF_greatest, rule SUP_upper2, simp_all, rule INF_lower2, simp, blast)
+next
+ have "(INF y. SUP x. ((P x y))) \<le> Inf (Sup ` {{P x y | x . True} | y . True })" (is "?A \<le> ?B")
+ proof (rule_tac INF_greatest, clarsimp)
+ fix y
+ have "?A \<le> (SUP x. P x y)"
+ by (rule INF_lower, simp)
+ also have "... \<le> Sup {uu. \<exists>x. uu = P x y}"
+ by (simp add: full_SetCompr_eq)
+ finally show "?A \<le> Sup {uu. \<exists>x. uu = P x y}"
+ by simp
+ qed
+ also have "... \<le> (SUP x. INF y. P (x y) y)"
+ proof (subst Inf_Sup, rule_tac SUP_least, clarsimp)
+ fix f
+ assume A: "\<forall>Y. (\<exists>y. Y = {uu. \<exists>x. uu = P x y}) \<longrightarrow> f Y \<in> Y"
+
+ 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)"
+ proof (rule INF_greatest, clarsimp)
+ fix y
+ 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}"
+ by (rule_tac INF_lower, blast)
+ also have "... \<le> P (SOME x. f {uu . \<exists>x. uu = P x y} = P x y) y"
+ using A by (rule_tac someI2_ex, auto)
+ 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"
+ by simp
+ qed
+ also have "... \<le> (SUP x. INF y. P (x y) y)"
+ by (rule SUP_upper, simp)
+ 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)"
+ by simp
+ qed
+ finally show "(INF y. SUP x. P x y) \<le> (SUP x. INF y. P (x y) y)"
+ by simp
+qed
+
+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)"
+proof (rule antisym)
+ 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"
+ by (rule_tac i = "(f xa)" in SUP_upper2, simp, rule_tac i = "xa" in INF_lower2, simp_all)
+ 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)"
+ apply (rule SUP_least, simp, safe, rule INF_greatest, simp)
+ by (rule A)
+next
+ 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)"
+ proof (cases "{} \<in> A")
+ case True
+ then show ?thesis
+ by (rule_tac i = "{}" in INF_lower2, simp_all)
+ next
+ case False
+ 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)"
+ by (rule_tac i = xb in INF_lower2, simp_all)
+ 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)"
+ by (rule_tac i = y in INF_lower2, simp_all)
+ 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)"
+ 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)
+ apply (rule_tac x = "(\<lambda> y . if x y \<in> y then x y else (SOME x . x \<in>y))" in exI, simp)
+ using False some_in_eq apply auto[1]
+ by (rule INF_greatest, auto)
+ 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>)"
+ apply (case_tac "x \<in> A")
+ apply (rule INF_lower2, simp)
+ by (rule SUP_least, rule SUP_upper2, auto)
+ 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>)"
+ by (rule INF_greatest)
+ also have "... = (\<Squnion>x. \<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>)"
+ by (simp add: INF_SUP)
+ also have "... \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a)"
+ by (rule SUP_least, simp)
+ finally show ?thesis by simp
+ qed
+qed
+
+lemma SUP_INF: "(SUP y. INF x. ((P x y)::'a)) = (INF x. SUP y. P (x y) y)"
+ using dual_complete_distrib_lattice
+ by (rule complete_distrib_lattice.INF_SUP)
+
+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)"
+ using dual_complete_distrib_lattice
+ by (rule complete_distrib_lattice.INF_SUP_set)
+
end
+
+(*properties of the former complete_distrib_lattice*)
+context complete_distrib_lattice
+begin
+
+lemma sup_INF: "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
+ by (simp add: sup_Inf)
+
+lemma inf_SUP: "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
+ by (simp add: inf_Sup)
+
+
+lemma Inf_sup: "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
+ by (simp add: sup_Inf sup_commute)
+
+lemma Sup_inf: "\<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)"
+ by (simp add: inf_Sup inf_commute)
+
+lemma INF_sup: "(\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)"
+ by (simp add: sup_INF sup_commute)
+
+lemma SUP_inf: "(\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)"
+ by (simp add: inf_SUP inf_commute)
+
+lemma Inf_sup_eq_top_iff: "(\<Sqinter>B \<squnion> a = \<top>) \<longleftrightarrow> (\<forall>b\<in>B. b \<squnion> a = \<top>)"
+ by (simp only: Inf_sup INF_top_conv)
+
+lemma Sup_inf_eq_bot_iff: "(\<Squnion>B \<sqinter> a = \<bottom>) \<longleftrightarrow> (\<forall>b\<in>B. b \<sqinter> a = \<bottom>)"
+ by (simp only: Sup_inf SUP_bot_conv)
+
+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)"
+ by (subst INF_commute) (simp add: sup_INF INF_sup)
+
+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)"
+ by (subst SUP_commute) (simp add: inf_SUP SUP_inf)
+
+end
+
+context complete_boolean_algebra
+begin
+
+lemma dual_complete_boolean_algebra:
+ "class.complete_boolean_algebra Sup Inf sup (\<ge>) (>) inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
+ by (rule class.complete_boolean_algebra.intro,
+ rule dual_complete_distrib_lattice,
+ rule dual_boolean_algebra)
+end
+
+
+
+instantiation "set" :: (type) complete_distrib_lattice
+begin
+instance proof (standard, clarsimp)
+ fix A :: "(('a set) set) set"
+ fix x::'a
+ define F where "F = (\<lambda> Y . (SOME X . (Y \<in> A \<and> X \<in> Y \<and> x \<in> X)))"
+ assume A: "\<forall>xa\<in>A. \<exists>X\<in>xa. x \<in> X"
+
+ from this have B: " (\<forall>xa \<in> F ` A. x \<in> xa)"
+ apply (safe, simp add: F_def)
+ by (rule someI2_ex, auto)
+
+ have "(\<exists>f. F ` A = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y))"
+ apply (rule_tac x = "F" in exI, simp add: F_def, safe)
+ using A by (rule_tac someI2_ex, auto)
+
+ 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)"
+ by auto
+qed
+end
+
+instance "set" :: (type) complete_boolean_algebra ..
+
+instantiation "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice
+begin
+instance by standard (simp add: le_fun_def INF_SUP_set)
+end
+
+instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
+
+context complete_linorder
+begin
+
+subclass complete_distrib_lattice
+proof (standard, rule ccontr)
+ fix A
+ assume "\<not> INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+ from this have C: "INFIMUM A Sup > SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+ using local.not_le by blast
+ show "False"
+ proof (cases "\<exists> z . INFIMUM A Sup > z \<and> z > SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf")
+ case True
+ 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"
+ by blast
+
+ from A have "\<And> Y . Y \<in> A \<Longrightarrow> z < Sup Y"
+ by (simp add: less_INF_D)
+
+ from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k \<in>Y . z < k"
+ using local.less_Sup_iff by blast
+
+ define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> z < k)"
+
+ have D: "\<And> Y . Y \<in> A \<Longrightarrow> z < F Y"
+ using B by (simp add: F_def, rule_tac someI2_ex, auto)
+
+ have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
+ using B by (simp add: F_def, rule_tac someI2_ex, auto)
+
+ have "z \<le> Inf (F ` A)"
+ by (simp add: D local.INF_greatest local.order.strict_implies_order)
+
+ also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+ apply (rule SUP_upper, safe)
+ using E by blast
+ finally have "z \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+ by simp
+
+ from X and this show ?thesis
+ using local.not_less by blast
+ next
+ case False
+ 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"
+ using local.le_less_linear by blast
+
+ from C have "\<And> Y . Y \<in> A \<Longrightarrow> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < Sup Y"
+ by (simp add: less_INF_D)
+
+ 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"
+ using local.less_Sup_iff by blast
+
+ 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)"
+
+ have D: "\<And> Y . Y \<in> A \<Longrightarrow> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < F Y"
+ using B by (simp add: F_def, rule_tac someI2_ex, auto)
+
+ have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
+ using B by (simp add: F_def, rule_tac someI2_ex, auto)
+
+ have "\<And> Y . Y \<in> A \<Longrightarrow> INFIMUM A Sup \<le> F Y"
+ using D False local.leI by blast
+
+ from this have "INFIMUM A Sup \<le> Inf (F ` A)"
+ by (simp add: local.INF_greatest)
+
+ also have "Inf (F ` A) \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+ apply (rule SUP_upper, safe)
+ using E by blast
+
+ finally have "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+ by simp
+
+ from C and this show ?thesis
+ using local.not_less by blast
+ qed
+ qed
+end
+
+
+
+end
--- a/src/HOL/Library/FSet.thy Mon Mar 12 08:25:35 2018 +0000
+++ b/src/HOL/Library/FSet.thy Mon Mar 12 20:52:53 2018 +0100
@@ -149,8 +149,7 @@
parametric right_total_Compl_transfer Compl_transfer by simp
instance
- by (standard; transfer) (simp_all add: Diff_eq)
-
+ by (standard; transfer) (simp_all add: Inf_Sup Diff_eq)
end
abbreviation fUNIV :: "'a::finite fset" where "fUNIV \<equiv> top"
--- a/src/HOL/Library/Finite_Lattice.thy Mon Mar 12 08:25:35 2018 +0000
+++ b/src/HOL/Library/Finite_Lattice.thy Mon Mar 12 20:52:53 2018 +0100
@@ -167,11 +167,21 @@
"inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
using finite [of A] by induct (simp_all add: inf_sup_distrib1)
-instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
-proof
-qed (auto simp:
- finite_distrib_lattice_complete_sup_Inf
- finite_distrib_lattice_complete_inf_Sup)
+context finite_distrib_lattice_complete
+begin
+subclass finite_distrib_lattice
+ apply standard
+ apply (simp_all add: Inf_def Sup_def bot_def top_def)
+ apply (metis (mono_tags) insert_UNIV local.Sup_fin.eq_fold local.bot_def local.finite_UNIV local.top_def)
+ apply (simp add: comp_fun_idem.fold_insert_idem local.comp_fun_idem_inf)
+ apply (metis (mono_tags) insert_UNIV local.Inf_fin.eq_fold local.finite_UNIV)
+ apply (simp add: comp_fun_idem.fold_insert_idem local.comp_fun_idem_sup)
+ apply (metis (mono_tags) insert_UNIV local.Inf_fin.eq_fold local.finite_UNIV)
+ apply (metis (mono_tags) insert_UNIV local.Sup_fin.eq_fold local.finite_UNIV)
+ done
+end
+
+instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice ..
text \<open>The product of two finite distributive lattices
is already a finite distributive lattice.\<close>
@@ -189,7 +199,6 @@
(finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete
..
-
subsection \<open>Linear Orders\<close>
text \<open>A linear order is a distributive lattice.
--- a/src/HOL/Library/Option_ord.thy Mon Mar 12 08:25:35 2018 +0000
+++ b/src/HOL/Library/Option_ord.thy Mon Mar 12 20:52:53 2018 +0100
@@ -283,60 +283,148 @@
"A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
using Some_Sup [of "f ` A"] by (simp add: comp_def)
-instance option :: (complete_distrib_lattice) complete_distrib_lattice
-proof
- fix a :: "'a option" and B
- show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
- proof (cases a)
- case None
- then show ?thesis by simp
+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"
+proof (cases "{} \<in> A")
+ case True
+ then show ?thesis
+ by (rule_tac i = "{}" in INF_lower2, simp_all)
+next
+ case False
+ from this have X: "{} \<notin> A"
+ by simp
+ then show ?thesis
+ proof (cases "{None} \<in> A")
+ case True
+ then show ?thesis
+ by (rule_tac i = "{None}" in INF_lower2, simp_all)
next
- case (Some c)
- show ?thesis
- proof (cases "None \<in> B")
- case True
- then have "Some c = (\<Sqinter>b\<in>B. Some c \<squnion> b)"
- by (auto intro!: antisym INF_lower2 INF_greatest)
- with True Some show ?thesis by simp
- next
- case False then have B: "{x \<in> B. \<exists>y. x = Some y} = B" by auto (metis not_Some_eq)
- from sup_Inf have "Some c \<squnion> Some (\<Sqinter>Option.these B) = Some (\<Sqinter>b\<in>Option.these B. c \<squnion> b)" by simp
- then have "Some c \<squnion> \<Sqinter>(Some ` Option.these B) = (\<Sqinter>x\<in>Some ` Option.these B. Some c \<squnion> x)"
- by (simp add: Some_INF Some_Inf comp_def)
- with Some B show ?thesis by (simp add: Some_image_these_eq cong del: strong_INF_cong)
- qed
- qed
- show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
- proof (cases a)
- case None
- then show ?thesis by (simp add: image_constant_conv bot_option_def cong del: strong_SUP_cong)
- next
- case (Some c)
- show ?thesis
- proof (cases "B = {} \<or> B = {None}")
- case True
- then show ?thesis by auto
- next
- have B: "B = {x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None}"
- by auto
- then have Sup_B: "\<Squnion>B = \<Squnion>({x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None})"
- 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)"
- by simp_all
- have Sup_None: "\<Squnion>{x. x = None \<and> x \<in> B} = None"
- by (simp add: bot_option_def [symmetric])
- have SUP_None: "(\<Squnion>x\<in>{x. x = None \<and> x \<in> B}. Some c \<sqinter> x) = None"
- by (simp add: bot_option_def [symmetric])
- case False then have "Option.these B \<noteq> {}" by (simp add: these_not_empty_eq)
- moreover from inf_Sup have "Some c \<sqinter> Some (\<Squnion>Option.these B) = Some (\<Squnion>b\<in>Option.these B. c \<sqinter> b)"
- by simp
- ultimately have "Some c \<sqinter> \<Squnion>(Some ` Option.these B) = (\<Squnion>x\<in>Some ` Option.these B. Some c \<sqinter> x)"
- by (simp add: Some_SUP Some_Sup comp_def)
- with Some show ?thesis
- 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)
- qed
+ case False
+ have "\<And> y . y\<in>A \<Longrightarrow> Sup (y - {None}) = Sup y"
+ by (metis (no_types, lifting) Sup_option_def insert_Diff_single these_insert_None these_not_empty_eq)
+
+ from this have A: "Sup ` A = (Sup ` {y - {None} | y. y\<in>A})"
+ apply (simp add: image_def, simp, safe)
+ apply (rule_tac x = "xa - {None}" in exI, simp, blast)
+ by blast
+
+ 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}
+ = {y. \<exists>x\<in>ya - {None}. y = the x} \<and> ya \<in> A"
+ by (rule_tac x = "y" in exI, auto)
+
+ have [simp]: "\<And>y. y \<in> A \<Longrightarrow>
+ (\<exists>ya. y - {None} = ya - {None} \<and> ya \<in> A) \<and> \<Squnion>{ya. \<exists>x\<in>y - {None}. ya = the x}
+ = \<Squnion>{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}"
+ apply safe
+ apply blast
+ apply (rule_tac f = Sup in arg_cong)
+ by auto
+
+ have C: "(\<lambda>x. (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A} = (Sup ` {the ` (y - {None}) |y. y \<in> A})"
+ apply (simp add: image_def Option.these_def, safe)
+ apply (rule_tac x = "{ya. \<exists>x. x \<in> y - {None} \<and> (\<exists>y. x = Some y) \<and> ya = the x}" in exI, simp)
+ by (rule_tac x = "y -{None}" in exI, simp)
+
+ have D: "\<forall> f . \<exists>Y\<in>A. f Y \<notin> Y \<Longrightarrow> False"
+ apply (drule_tac x = "\<lambda> Y . SOME x . x \<in> Y" in spec, safe)
+ by (simp add: X some_in_eq)
+
+ define F where "F = (\<lambda> Y . SOME x::'a option . x \<in> (Y - {None}))"
+
+ have G: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> x . x \<in> Y - {None}"
+ by (metis False X all_not_in_conv insert_Diff_single these_insert_None these_not_empty_eq)
+
+ have F: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> (Y - {None})"
+ by (metis F_def G empty_iff some_in_eq)
+
+ have "Some \<bottom> \<le> Inf (F ` A)"
+ by (metis (no_types, lifting) Diff_iff F Inf_option_def bot.extremum image_iff
+ less_eq_option_Some singletonI)
+
+ from this have "Inf (F ` A) \<noteq> None"
+ by (case_tac "\<Sqinter>x\<in>A. F x", simp_all)
+
+ from this have "\<exists> x . x \<noteq> None \<and> x \<in> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
+ apply (rule_tac x = "Inf (F ` A)" in exI, simp add: image_def, safe)
+ apply (rule_tac x = "F ` A" in exI, safe)
+ using F by auto
+
+ from this have E:" Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} = {None} \<Longrightarrow> False"
+ by blast
+
+ have [simp]: "((\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x) = None) = False"
+ 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>
+ ex_in_conv option.simps(3))
+
+ have B: "Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A})
+ = ((\<lambda>x. (\<Squnion> Option.these x)) ` {y - {None} |y. y \<in> A})"
+ by (metis image_image these_image_Some_eq)
+
+ 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>
+ \<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"
+ apply (rule_tac x = "{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) | x . x\<in> A}" in exI, safe)
+ apply (rule_tac x = "(\<lambda> Y . Some (f (the ` (Y - {None})))) " in exI, safe)
+ apply (rule_tac x = xa in bexI, simp add: image_def, simp)
+ apply (rule_tac x = xa in exI, simp add: image_def)
+ apply(drule_tac x = "(the ` (Y - {None}))" in spec)
+ apply (simp add: image_def,safe, simp)
+ using option.collapse apply fastforce
+ by (simp add: Setcompr_eq_image)
+
+ 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> \<exists>y. (\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x})) = Some y"
+ by (metis (no_types) Some_INF)
+
+ have [simp]: "\<And> f.
+ (\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> the (\<Sqinter>Y\<in>A. Some (f (the ` (Y - {None}))))"
+ apply (simp add: Inf_option_def, safe)
+ apply (rule Inf_greatest, simp add: image_def Option.these_def, safe)
+ apply (rule_tac i = " {y. \<exists>x\<in>xb - {None}. y = the x}" in INF_lower2)
+ apply simp_all
+ by blast
+
+ have X: "\<And> f . \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y
+ \<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})"
+ apply (rule_tac u = "the (Inf ((\<lambda> Y . Some (f (the ` (Y - {None})) )) ` A))" in Sup_upper2)
+ apply (simp add: Option.these_def image_def)
+ apply (rule_tac x = "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x}))" in exI, simp)
+ by simp
+
+ have "(Inf (Sup `A)) = (Inf (Sup ` {y - {None} | y. y\<in>A}))"
+ by (subst A, simp)
+
+ also have "... = (\<Sqinter>x\<in>{y - {None} |y. y \<in> A}. if x = {} \<or> x = {None} then None else Some (\<Squnion>Option.these x))"
+ by (simp add: Sup_option_def)
+
+ also have "... = (\<Sqinter>x\<in>{y - {None} |y. y \<in> A}. Some (\<Squnion>Option.these x))"
+ apply (subgoal_tac "\<And> x . x\<in>{y - {None} |y. y \<in> A} \<Longrightarrow> x \<noteq> {} \<and> x \<noteq> {None}", simp)
+ using G by fastforce
+
+ also have "... = Some (\<Sqinter>Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}))"
+ by (simp add: Inf_option_def, safe)
+
+ also have "... = Some (\<Sqinter> ((\<lambda>x. (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}))"
+ by (simp add: B)
+
+ also have "... = Some (Inf (Sup ` {the ` (y - {None}) |y. y \<in> A}))"
+ by (unfold C, simp)
+ thm Inf_Sup
+ 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) "
+ by (simp add: Inf_Sup)
+
+ also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+ apply (simp add: less_eq_option_def)
+ apply (case_tac "\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x", simp_all)
+ apply (rule Sup_least, safe)
+ apply (simp add: Sup_option_def)
+ 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)
+ by (drule X, simp)
+ finally show ?thesis by simp
qed
qed
+instance option :: (complete_distrib_lattice) complete_distrib_lattice
+ by (standard, simp add: option_Inf_Sup)
+
instance option :: (complete_linorder) complete_linorder ..
--- a/src/HOL/Library/Product_Order.thy Mon Mar 12 08:25:35 2018 +0000
+++ b/src/HOL/Library/Product_Order.thy Mon Mar 12 20:52:53 2018 +0100
@@ -233,14 +233,10 @@
(* Contribution: Alessandro Coglio *)
instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
-proof (standard, goal_cases)
- case 1
- then show ?case
- by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)
-next
- case 2
- then show ?case
- by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP comp_def)
+proof
+ fix A::"('a\<times>'b) set set"
+ show "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+ by (simp add: Sup_prod_def Inf_prod_def INF_SUP_set)
qed
subsection \<open>Bekic's Theorem\<close>
--- a/src/HOL/Predicate.thy Mon Mar 12 08:25:35 2018 +0000
+++ b/src/HOL/Predicate.thy Mon Mar 12 20:52:53 2018 +0100
@@ -102,6 +102,18 @@
by (simp add: minus_pred_def)
instance proof
+ fix A::"'a pred set set"
+ show "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+ proof (simp add: less_eq_pred_def Sup_fun_def Inf_fun_def, safe)
+ fix w
+ assume A: "\<forall>x\<in>A. \<exists>f\<in>x. eval f w"
+ define F where "F = (\<lambda> x . SOME f . f \<in> x \<and> eval f w)"
+ have [simp]: "(\<forall>f\<in> (F ` A). eval f w)"
+ by (metis (no_types, lifting) A F_def image_iff some_eq_ex)
+ 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)"
+ apply (rule_tac x = "F ` A" in exI, simp)
+ using A by (metis (no_types, lifting) F_def someI)+
+ qed
qed (auto intro!: pred_eqI)
end