src/HOL/Complete_Lattices.thy

--- a/src/HOL/Complete_Lattices.thy	Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Complete_Lattices.thy	Sun Oct 21 09:39:09 2018 +0200
@@ -73,7 +73,7 @@
 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]:
+lemma INF_cong_strong [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)
 
@@ -83,20 +83,20 @@
 begin
 
 lemma SUP_image [simp]: "\<Squnion>(g ` f ` A) = \<Squnion>((g \<circ> f) ` A)"
-  by (simp add: image_comp)
+by(fact Inf.INF_image)
 
 lemma SUP_identity_eq [simp]: "(\<Squnion>x\<in>A. x) = \<Squnion>A"
-  by simp
+by(fact Inf.INF_identity_eq)
 
 lemma SUP_id_eq [simp]: "\<Squnion>(id ` A) = \<Squnion>A"
-  by (simp add: id_def)
+by(fact Inf.INF_id_eq)
 
 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)
+by (fact Inf.INF_cong)
 
-lemma strong_SUP_cong [cong]:
+lemma SUP_cong_strong [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)
+by (fact Inf.INF_cong_strong)
 
 end
 
@@ -191,19 +191,19 @@
   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> \<Sqinter>(f ` A)"
-  by (simp cong del: strong_INF_cong)
+  by (simp cong del: INF_cong_strong)
 
 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> \<Squnion>(f ` A)"
-  by (simp cong del: strong_SUP_cong)
+  by (simp cong del: SUP_cong_strong)
 
 lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
-  by (simp cong del: strong_INF_cong)
+  by (simp cong del: INF_cong_strong)
 
 lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
-  by (simp cong del: strong_SUP_cong)
+  by (simp cong del: SUP_cong_strong)
 
 lemma Inf_UNIV [simp]: "\<Sqinter>UNIV = \<bottom>"
   by (auto intro!: antisym Inf_lower)
@@ -449,11 +449,11 @@
 
 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)
+  by (auto intro: antisym cong del: INF_cong_strong)
 
 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)
+  by (auto intro: antisym cong del: SUP_cong_strong)
 
 end