# HG changeset patch
# User haftmann
# Date 1535142134 0
# Node ID 3974935e0252d0bf411d5f9d7bc960218025706a
# Parent  c898c2b1fd5893251f20709f6fc6a9718b976714
some modernization of notation

diff -r c898c2b1fd58 -r 3974935e0252 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Fri Aug 24 20:22:10 2018 +0000
+++ b/src/HOL/Complete_Lattices.thy	Fri Aug 24 20:22:14 2018 +0000
@@ -604,7 +604,7 @@
     unfolding Inf_less_iff .
 qed (auto elim!: allE[of _ "\<Sqinter>A"] simp add: not_le[symmetric] Inf_lower)
 
-lemma INF_le_iff: "INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
+lemma INF_le_iff: "\<Sqinter>(f ` A) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
   using Inf_le_iff [of "f ` A"] by simp
 
 lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
@@ -616,7 +616,7 @@
     unfolding less_Sup_iff .
 qed (auto elim!: allE[of _ "\<Squnion>A"] simp add: not_le[symmetric] Sup_upper)
 
-lemma le_SUP_iff: "x \<le> SUPREMUM A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
+lemma le_SUP_iff: "x \<le> \<Squnion>(f ` A) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
   using le_Sup_iff [of _ "f ` A"] by simp
 
 end
@@ -641,10 +641,10 @@
 lemma True_in_image_Bex [simp]: "True \<in> P ` A \<longleftrightarrow> Bex A P"
   by auto
 
-lemma INF_bool_eq [simp]: "INFIMUM = Ball"
+lemma INF_bool_eq [simp]: "(\<lambda>A f. \<Sqinter>(f ` A)) = Ball"
   by (simp add: fun_eq_iff)
 
-lemma SUP_bool_eq [simp]: "SUPREMUM = Bex"
+lemma SUP_bool_eq [simp]: "(\<lambda>A f. \<Squnion>(f ` A)) = Bex"
   by (simp add: fun_eq_iff)
 
 instance bool :: complete_boolean_algebra
diff -r c898c2b1fd58 -r 3974935e0252 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Fri Aug 24 20:22:10 2018 +0000
+++ b/src/HOL/Hilbert_Choice.thy	Fri Aug 24 20:22:14 2018 +0000
@@ -943,21 +943,21 @@
    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)"
+lemma sup_Inf: "a \<squnion> \<Sqinter>B = \<Sqinter>((\<squnion>) a ` B)"
 proof (rule antisym)
-  show "a \<squnion> Inf B \<le> (INF b:B. a \<squnion> b)"
+  show "a \<squnion> \<Sqinter>B \<le> \<Sqinter>((\<squnion>) a ` B)"
     apply (rule INF_greatest)
     using Inf_lower sup.mono by 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"
+  have "\<Sqinter>((\<squnion>) a ` B) \<le> \<Sqinter>(Sup ` {{f {a}, f B} |f. f {a} = a \<and> f B \<in> B})"
     by (rule INF_greatest, auto simp add: INF_lower)
   also have "... = SUPREMUM {{a}, B} Inf"
     by (unfold Sup_Inf, simp)
-  finally show "(INF b:B. a \<squnion> b) \<le> a \<squnion> Inf B"
+  finally show "\<Sqinter>((\<squnion>) a ` B) \<le> a \<squnion> \<Sqinter>B"
     by simp
 qed
 
-lemma inf_Sup: "a \<sqinter> Sup B = (SUP b:B. a \<sqinter> b)"
+lemma inf_Sup: "a \<sqinter> \<Squnion>B = \<Squnion>((\<sqinter>) a ` B)"
   using dual_complete_distrib_lattice
   by (rule complete_distrib_lattice.sup_Inf)
 
@@ -981,27 +981,29 @@
     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)"
+    have " \<Sqinter>(f ` {uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}) \<le>
+      (\<Sqinter>y. P (SOME x. f {P x y |x. True} = P x 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}"
+        have "(INF x\<in>{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x) \<le> f {uu. \<exists>x. uu = P x y}"
           by (rule INF_lower, blast)
         also have "... \<le> P (SOME x. f {uu . \<exists>x. uu = P x y} = P x y) y"
           apply (rule someI2_ex)
           using A by 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"
+        finally show "\<Sqinter>(f ` {uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}) \<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)"
+      finally show "\<Sqinter>(f ` {uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}) \<le> (\<Squnion>x. \<Sqinter>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)"
+lemma INF_SUP_set: "(\<Sqinter>x\<in>A. \<Squnion>(g ` x)) = (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>(g ` x))"
 proof (rule antisym)
   have [simp]: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> (\<Sqinter>x\<in>A. g (f x)) \<le> g (f xa)"
     by (rule INF_lower2, blast+)
@@ -1063,7 +1065,7 @@
   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)"
+lemma SUP_INF_set: "(\<Squnion>x\<in>A. \<Sqinter>(g ` x)) = (\<Sqinter>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Squnion>(g ` x))"
   using dual_complete_distrib_lattice
   by (rule complete_distrib_lattice.INF_SUP_set)
 
@@ -1118,7 +1120,7 @@
 
 
 
-instantiation "set" :: (type) complete_distrib_lattice
+instantiation set :: (type) complete_distrib_lattice
 begin
 instance proof (standard, clarsimp)
   fix A :: "(('a set) set) set"
@@ -1143,7 +1145,7 @@
 qed
 end
 
-instance "set" :: (type) complete_boolean_algebra ..
+instance set :: (type) complete_boolean_algebra ..
 
 instantiation "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice
 begin
diff -r c898c2b1fd58 -r 3974935e0252 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Fri Aug 24 20:22:10 2018 +0000
+++ b/src/HOL/Topological_Spaces.thy	Fri Aug 24 20:22:14 2018 +0000
@@ -456,7 +456,7 @@
 subsubsection \<open>Topological filters\<close>
 
 definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
-  where "nhds a = (INF S:{S. open S \<and> a \<in> S}. principal S)"
+  where "nhds a = (INF S\<in>{S. open S \<and> a \<in> S}. principal S)"
 
 definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter"
     ("at (_)/ within (_)" [1000, 60] 60)
@@ -472,12 +472,12 @@
   where "at_left x \<equiv> at x within {..< x}"
 
 lemma (in topological_space) nhds_generated_topology:
-  "open = generate_topology T \<Longrightarrow> nhds x = (INF S:{S\<in>T. x \<in> S}. principal S)"
+  "open = generate_topology T \<Longrightarrow> nhds x = (INF S\<in>{S\<in>T. x \<in> S}. principal S)"
   unfolding nhds_def
 proof (safe intro!: antisym INF_greatest)
   fix S
   assume "generate_topology T S" "x \<in> S"
-  then show "(INF S:{S \<in> T. x \<in> S}. principal S) \<le> principal S"
+  then show "(INF S\<in>{S \<in> T. x \<in> S}. principal S) \<le> principal S"
     by induct
       (auto intro: INF_lower order_trans simp: inf_principal[symmetric] simp del: inf_principal)
 qed (auto intro!: INF_lower intro: generate_topology.intros)