# HG changeset patch
# User haftmann
# Date 1535044228 0
# Node ID e79c771c0619d1a74a64fbb81ad8208683ec656d
# Parent  9ca183045102454c1a239e2dbf9cf8978d5be6a0
tuned

diff -r 9ca183045102 -r e79c771c0619 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Thu Aug 23 17:09:39 2018 +0000
+++ b/src/HOL/Complete_Lattices.thy	Thu Aug 23 17:10:28 2018 +0000
@@ -21,22 +21,6 @@
 abbreviation (input) INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" \<comment> \<open>legacy\<close>
   where "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
 
-lemma INF_image [simp]: "INFIMUM (f ` A) g = INFIMUM A (g \<circ> f)"
-  by (simp add: image_comp)
-
-lemma INF_identity_eq [simp]: "INFIMUM A (\<lambda>x. x) = \<Sqinter>A"
-  by simp
-
-lemma INF_id_eq [simp]: "INFIMUM A id = \<Sqinter>A"
-  by simp
-
-lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
-  by (simp add: image_def)
-
-lemma strong_INF_cong [cong]:
-  "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
-  unfolding simp_implies_def by (fact INF_cong)
-
 end
 
 class Sup =
@@ -46,22 +30,6 @@
 abbreviation (input) SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" \<comment> \<open>legacy\<close>
   where "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
 
-lemma SUP_image [simp]: "SUPREMUM (f ` A) g = SUPREMUM A (g \<circ> f)"
-  by (simp add: image_comp)
-
-lemma SUP_identity_eq [simp]: "SUPREMUM A (\<lambda>x. x) = \<Squnion>A"
-  by simp
-
-lemma SUP_id_eq [simp]: "SUPREMUM A id = \<Squnion>A"
-  by (simp add: id_def)
-
-lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
-  by (simp add: image_def)
-
-lemma strong_SUP_cong [cong]:
-  "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
-  unfolding simp_implies_def by (fact SUP_cong)
-
 end
 
 syntax (ASCII)
@@ -90,6 +58,48 @@
   "\<Squnion>x. f"     \<rightleftharpoons> "\<Squnion>CONST range (\<lambda>x. f)"
   "\<Squnion>x\<in>A. f"   \<rightleftharpoons> "CONST Sup ((\<lambda>x. f) `  A)"
 
+context Inf
+begin
+
+lemma INF_image [simp]: " \<Sqinter>(g ` f ` A) = \<Sqinter>((g \<circ> f) ` A)"
+  by (simp add: image_comp)
+
+lemma INF_identity_eq [simp]: "(\<Sqinter>x\<in>A. x) = \<Sqinter>A"
+  by simp
+
+lemma INF_id_eq [simp]: "\<Sqinter>(id ` A) = \<Sqinter>A"
+  by simp
+
+lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)"
+  by (simp add: image_def)
+
+lemma strong_INF_cong [cong]:
+  "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)"
+  unfolding simp_implies_def by (fact INF_cong)
+
+end
+
+context Sup
+begin
+
+lemma SUP_image [simp]: "\<Squnion>(g ` f ` A) = \<Squnion>((g \<circ> f) ` A)"
+  by (simp add: image_comp)
+
+lemma SUP_identity_eq [simp]: "(\<Squnion>x\<in>A. x) = \<Squnion>A"
+  by simp
+
+lemma SUP_id_eq [simp]: "\<Squnion>(id ` A) = \<Squnion>A"
+  by (simp add: id_def)
+
+lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
+  by (simp add: image_def)
+
+lemma strong_SUP_cong [cong]:
+  "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
+  unfolding simp_implies_def by (fact SUP_cong)
+
+end
+
 
 subsection \<open>Abstract complete lattices\<close>
 
@@ -180,13 +190,13 @@
 lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
 
-lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFIMUM A f"
+lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> \<Sqinter>(f ` A)"
   by (simp cong del: strong_INF_cong)
 
 lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
   by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
 
-lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPREMUM A f"
+lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> \<Squnion>(f ` A)"
   by (simp cong del: strong_SUP_cong)
 
 lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
@@ -269,13 +279,13 @@
 lemma INF_eq:
   assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
     and "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
-  shows "INFIMUM A f = INFIMUM B g"
+  shows "\<Sqinter>(f ` A) = \<Sqinter>(g ` B)"
   by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
 
 lemma SUP_eq:
   assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<le> g j"
     and "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
-  shows "SUPREMUM A f = SUPREMUM B g"
+  shows "\<Squnion>(f ` A) = \<Squnion>(g ` B)"
   by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
 
 lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<le> \<Sqinter>(A \<inter> B)"
@@ -422,20 +432,20 @@
 lemma Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
   by (blast intro: Sup_upper2 Inf_lower ex_in_conv)
 
-lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFIMUM A f \<le> SUPREMUM A f"
+lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> \<Sqinter>(f ` A) \<le> \<Squnion>(f ` A)"
   using Inf_le_Sup [of "f ` A"] by simp
 
-lemma INF_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFIMUM I f = x"
+lemma INF_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> \<Sqinter>(f ` I) = x"
   by (auto intro: INF_eqI)
 
-lemma SUP_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x"
+lemma SUP_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> \<Squnion>(f ` I) = x"
   by (auto intro: SUP_eqI)
 
-lemma INF_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> INFIMUM I f = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
+lemma INF_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> \<Sqinter>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
   using INF_eq_const [of I f c] INF_lower [of _ I f]
   by (auto intro: antisym cong del: strong_INF_cong)
 
-lemma SUP_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> SUPREMUM I f = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
+lemma SUP_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> \<Squnion>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
   using SUP_eq_const [of I f c] SUP_upper [of _ I f]
   by (auto intro: antisym cong del: strong_SUP_cong)
 
@@ -467,7 +477,8 @@
       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"
+    have "\<Sqinter>(Sup ` {{a, b}, {a, c}}) =
+      \<Squnion>(Inf ` {f ` {{a, b}, {a, c}} | f. \<forall>Y\<in>{{a, b}, {a, c}}. f Y \<in> Y})"
       by (rule Inf_Sup)
     from this show "(a \<squnion> b) \<sqinter> (a \<squnion> c) \<le> a \<squnion> b \<sqinter> c"
       apply simp