discontinued theory-local special syntax for lattice orderings
authorhaftmann
Wed Sep 07 11:59:09 2016 +0200 (2016-09-07)
changeset 638209f004fbf9d5c
parent 63819 58f74e90b96d
child 63822 c575a3814a76
discontinued theory-local special syntax for lattice orderings
src/HOL/Complete_Lattices.thy
src/HOL/Lattices.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Wed Sep 07 11:59:07 2016 +0200
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Wed Sep 07 11:59:09 2016 +0200
     1.3 @@ -11,11 +11,6 @@
     1.4    imports Fun
     1.5  begin
     1.6  
     1.7 -notation
     1.8 -  less_eq (infix "\<sqsubseteq>" 50) and
     1.9 -  less (infix "\<sqsubset>" 50)
    1.10 -
    1.11 -
    1.12  subsection \<open>Syntactic infimum and supremum operations\<close>
    1.13  
    1.14  class Inf =
    1.15 @@ -116,10 +111,10 @@
    1.16  in terms of infimum and supremum.\<close>
    1.17  
    1.18  class complete_lattice = lattice + Inf + Sup + bot + top +
    1.19 -  assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
    1.20 -    and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
    1.21 -    and Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
    1.22 -    and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
    1.23 +  assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<le> x"
    1.24 +    and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A"
    1.25 +    and Sup_upper: "x \<in> A \<Longrightarrow> x \<le> \<Squnion>A"
    1.26 +    and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z"
    1.27      and Inf_empty [simp]: "\<Sqinter>{} = \<top>"
    1.28      and Sup_empty [simp]: "\<Squnion>{} = \<bottom>"
    1.29  begin
    1.30 @@ -158,40 +153,40 @@
    1.31    "(\<And>i. i \<in> A \<Longrightarrow> x \<le> f i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<ge> y) \<Longrightarrow> x \<ge> y) \<Longrightarrow> (\<Sqinter>i\<in>A. f i) = x"
    1.32    using Inf_eqI [of "f ` A" x] by auto
    1.33  
    1.34 -lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
    1.35 +lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<le> f i"
    1.36    using Inf_lower [of _ "f ` A"] by simp
    1.37  
    1.38 -lemma INF_greatest: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
    1.39 +lemma INF_greatest: "(\<And>i. i \<in> A \<Longrightarrow> u \<le> f i) \<Longrightarrow> u \<le> (\<Sqinter>i\<in>A. f i)"
    1.40    using Inf_greatest [of "f ` A"] by auto
    1.41  
    1.42 -lemma SUP_upper: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
    1.43 +lemma SUP_upper: "i \<in> A \<Longrightarrow> f i \<le> (\<Squnion>i\<in>A. f i)"
    1.44    using Sup_upper [of _ "f ` A"] by simp
    1.45  
    1.46 -lemma SUP_least: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
    1.47 +lemma SUP_least: "(\<And>i. i \<in> A \<Longrightarrow> f i \<le> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<le> u"
    1.48    using Sup_least [of "f ` A"] by auto
    1.49  
    1.50 -lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
    1.51 +lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<le> v \<Longrightarrow> \<Sqinter>A \<le> v"
    1.52    using Inf_lower [of u A] by auto
    1.53  
    1.54 -lemma INF_lower2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
    1.55 +lemma INF_lower2: "i \<in> A \<Longrightarrow> f i \<le> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<le> u"
    1.56    using INF_lower [of i A f] by auto
    1.57  
    1.58 -lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
    1.59 +lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<le> u \<Longrightarrow> v \<le> \<Squnion>A"
    1.60    using Sup_upper [of u A] by auto
    1.61  
    1.62 -lemma SUP_upper2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
    1.63 +lemma SUP_upper2: "i \<in> A \<Longrightarrow> u \<le> f i \<Longrightarrow> u \<le> (\<Squnion>i\<in>A. f i)"
    1.64    using SUP_upper [of i A f] by auto
    1.65  
    1.66 -lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
    1.67 +lemma le_Inf_iff: "b \<le> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<le> a)"
    1.68    by (auto intro: Inf_greatest dest: Inf_lower)
    1.69  
    1.70 -lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
    1.71 +lemma le_INF_iff: "u \<le> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<le> f i)"
    1.72    using le_Inf_iff [of _ "f ` A"] by simp
    1.73  
    1.74 -lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
    1.75 +lemma Sup_le_iff: "\<Squnion>A \<le> b \<longleftrightarrow> (\<forall>a\<in>A. a \<le> b)"
    1.76    by (auto intro: Sup_least dest: Sup_upper)
    1.77  
    1.78 -lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
    1.79 +lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<le> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<le> u)"
    1.80    using Sup_le_iff [of "f ` A"] by simp
    1.81  
    1.82  lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
    1.83 @@ -218,68 +213,68 @@
    1.84  lemma Sup_UNIV [simp]: "\<Squnion>UNIV = \<top>"
    1.85    by (auto intro!: antisym Sup_upper)
    1.86  
    1.87 -lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
    1.88 +lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
    1.89    by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
    1.90  
    1.91 -lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
    1.92 +lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
    1.93    by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
    1.94  
    1.95 -lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
    1.96 +lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<le> \<Sqinter>B"
    1.97    by (auto intro: Inf_greatest Inf_lower)
    1.98  
    1.99 -lemma Sup_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
   1.100 +lemma Sup_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<le> \<Squnion>B"
   1.101    by (auto intro: Sup_least Sup_upper)
   1.102  
   1.103  lemma Inf_mono:
   1.104 -  assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b"
   1.105 -  shows "\<Sqinter>A \<sqsubseteq> \<Sqinter>B"
   1.106 +  assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
   1.107 +  shows "\<Sqinter>A \<le> \<Sqinter>B"
   1.108  proof (rule Inf_greatest)
   1.109    fix b assume "b \<in> B"
   1.110 -  with assms obtain a where "a \<in> A" and "a \<sqsubseteq> b" by blast
   1.111 -  from \<open>a \<in> A\<close> have "\<Sqinter>A \<sqsubseteq> a" by (rule Inf_lower)
   1.112 -  with \<open>a \<sqsubseteq> b\<close> show "\<Sqinter>A \<sqsubseteq> b" by auto
   1.113 +  with assms obtain a where "a \<in> A" and "a \<le> b" by blast
   1.114 +  from \<open>a \<in> A\<close> have "\<Sqinter>A \<le> a" by (rule Inf_lower)
   1.115 +  with \<open>a \<le> b\<close> show "\<Sqinter>A \<le> b" by auto
   1.116  qed
   1.117  
   1.118 -lemma INF_mono: "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<sqsubseteq> (\<Sqinter>n\<in>B. g n)"
   1.119 +lemma INF_mono: "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<le> (\<Sqinter>n\<in>B. g n)"
   1.120    using Inf_mono [of "g ` B" "f ` A"] by auto
   1.121  
   1.122  lemma Sup_mono:
   1.123 -  assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
   1.124 -  shows "\<Squnion>A \<sqsubseteq> \<Squnion>B"
   1.125 +  assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
   1.126 +  shows "\<Squnion>A \<le> \<Squnion>B"
   1.127  proof (rule Sup_least)
   1.128    fix a assume "a \<in> A"
   1.129 -  with assms obtain b where "b \<in> B" and "a \<sqsubseteq> b" by blast
   1.130 -  from \<open>b \<in> B\<close> have "b \<sqsubseteq> \<Squnion>B" by (rule Sup_upper)
   1.131 -  with \<open>a \<sqsubseteq> b\<close> show "a \<sqsubseteq> \<Squnion>B" by auto
   1.132 +  with assms obtain b where "b \<in> B" and "a \<le> b" by blast
   1.133 +  from \<open>b \<in> B\<close> have "b \<le> \<Squnion>B" by (rule Sup_upper)
   1.134 +  with \<open>a \<le> b\<close> show "a \<le> \<Squnion>B" by auto
   1.135  qed
   1.136  
   1.137 -lemma SUP_mono: "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<sqsubseteq> (\<Squnion>n\<in>B. g n)"
   1.138 +lemma SUP_mono: "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<le> (\<Squnion>n\<in>B. g n)"
   1.139    using Sup_mono [of "f ` A" "g ` B"] by auto
   1.140  
   1.141 -lemma INF_superset_mono: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
   1.142 +lemma INF_superset_mono: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<le> (\<Sqinter>x\<in>B. g x)"
   1.143    \<comment> \<open>The last inclusion is POSITIVE!\<close>
   1.144    by (blast intro: INF_mono dest: subsetD)
   1.145  
   1.146 -lemma SUP_subset_mono: "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)"
   1.147 +lemma SUP_subset_mono: "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<le> (\<Squnion>x\<in>B. g x)"
   1.148    by (blast intro: SUP_mono dest: subsetD)
   1.149  
   1.150  lemma Inf_less_eq:
   1.151 -  assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
   1.152 +  assumes "\<And>v. v \<in> A \<Longrightarrow> v \<le> u"
   1.153      and "A \<noteq> {}"
   1.154 -  shows "\<Sqinter>A \<sqsubseteq> u"
   1.155 +  shows "\<Sqinter>A \<le> u"
   1.156  proof -
   1.157    from \<open>A \<noteq> {}\<close> obtain v where "v \<in> A" by blast
   1.158 -  moreover from \<open>v \<in> A\<close> assms(1) have "v \<sqsubseteq> u" by blast
   1.159 +  moreover from \<open>v \<in> A\<close> assms(1) have "v \<le> u" by blast
   1.160    ultimately show ?thesis by (rule Inf_lower2)
   1.161  qed
   1.162  
   1.163  lemma less_eq_Sup:
   1.164 -  assumes "\<And>v. v \<in> A \<Longrightarrow> u \<sqsubseteq> v"
   1.165 +  assumes "\<And>v. v \<in> A \<Longrightarrow> u \<le> v"
   1.166      and "A \<noteq> {}"
   1.167 -  shows "u \<sqsubseteq> \<Squnion>A"
   1.168 +  shows "u \<le> \<Squnion>A"
   1.169  proof -
   1.170    from \<open>A \<noteq> {}\<close> obtain v where "v \<in> A" by blast
   1.171 -  moreover from \<open>v \<in> A\<close> assms(1) have "u \<sqsubseteq> v" by blast
   1.172 +  moreover from \<open>v \<in> A\<close> assms(1) have "u \<le> v" by blast
   1.173    ultimately show ?thesis by (rule Sup_upper2)
   1.174  qed
   1.175  
   1.176 @@ -295,10 +290,10 @@
   1.177    shows "SUPREMUM A f = SUPREMUM B g"
   1.178    by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
   1.179  
   1.180 -lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
   1.181 +lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<le> \<Sqinter>(A \<inter> B)"
   1.182    by (auto intro: Inf_greatest Inf_lower)
   1.183  
   1.184 -lemma Sup_inter_less_eq: "\<Squnion>(A \<inter> B) \<sqsubseteq> \<Squnion>A \<sqinter> \<Squnion>B "
   1.185 +lemma Sup_inter_less_eq: "\<Squnion>(A \<inter> B) \<le> \<Squnion>A \<sqinter> \<Squnion>B "
   1.186    by (auto intro: Sup_least Sup_upper)
   1.187  
   1.188  lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
   1.189 @@ -574,16 +569,16 @@
   1.190  lemma complete_linorder_sup_max: "sup = max"
   1.191    by (auto intro: antisym simp add: max_def fun_eq_iff)
   1.192  
   1.193 -lemma Inf_less_iff: "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
   1.194 +lemma Inf_less_iff: "\<Sqinter>S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
   1.195    by (simp add: not_le [symmetric] le_Inf_iff)
   1.196  
   1.197 -lemma INF_less_iff: "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
   1.198 +lemma INF_less_iff: "(\<Sqinter>i\<in>A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
   1.199    by (simp add: Inf_less_iff [of "f ` A"])
   1.200  
   1.201 -lemma less_Sup_iff: "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
   1.202 +lemma less_Sup_iff: "a < \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
   1.203    by (simp add: not_le [symmetric] Sup_le_iff)
   1.204  
   1.205 -lemma less_SUP_iff: "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   1.206 +lemma less_SUP_iff: "a < (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
   1.207    by (simp add: less_Sup_iff [of _ "f ` A"])
   1.208  
   1.209  lemma Sup_eq_top_iff [simp]: "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
   1.210 @@ -1426,10 +1421,6 @@
   1.211  
   1.212  text \<open>Finally\<close>
   1.213  
   1.214 -no_notation
   1.215 -  less_eq (infix "\<sqsubseteq>" 50) and
   1.216 -  less (infix "\<sqsubset>" 50)
   1.217 -
   1.218  lemmas mem_simps =
   1.219    insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
   1.220    mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
     2.1 --- a/src/HOL/Lattices.thy	Wed Sep 07 11:59:07 2016 +0200
     2.2 +++ b/src/HOL/Lattices.thy	Wed Sep 07 11:59:09 2016 +0200
     2.3 @@ -161,19 +161,15 @@
     2.4  
     2.5  subsection \<open>Concrete lattices\<close>
     2.6  
     2.7 -notation
     2.8 -  less_eq  (infix "\<sqsubseteq>" 50) and
     2.9 -  less  (infix "\<sqsubset>" 50)
    2.10 -
    2.11  class semilattice_inf =  order + inf +
    2.12 -  assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
    2.13 -  and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
    2.14 -  and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    2.15 +  assumes inf_le1 [simp]: "x \<sqinter> y \<le> x"
    2.16 +  and inf_le2 [simp]: "x \<sqinter> y \<le> y"
    2.17 +  and inf_greatest: "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
    2.18  
    2.19  class semilattice_sup = order + sup +
    2.20 -  assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
    2.21 -  and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
    2.22 -  and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
    2.23 +  assumes sup_ge1 [simp]: "x \<le> x \<squnion> y"
    2.24 +  and sup_ge2 [simp]: "y \<le> x \<squnion> y"
    2.25 +  and sup_least: "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x"
    2.26  begin
    2.27  
    2.28  text \<open>Dual lattice.\<close>
    2.29 @@ -191,28 +187,28 @@
    2.30  context semilattice_inf
    2.31  begin
    2.32  
    2.33 -lemma le_infI1: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    2.34 +lemma le_infI1: "a \<le> x \<Longrightarrow> a \<sqinter> b \<le> x"
    2.35    by (rule order_trans) auto
    2.36  
    2.37 -lemma le_infI2: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    2.38 +lemma le_infI2: "b \<le> x \<Longrightarrow> a \<sqinter> b \<le> x"
    2.39    by (rule order_trans) auto
    2.40  
    2.41 -lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    2.42 +lemma le_infI: "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> a \<sqinter> b"
    2.43    by (fact inf_greatest) (* FIXME: duplicate lemma *)
    2.44  
    2.45 -lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    2.46 +lemma le_infE: "x \<le> a \<sqinter> b \<Longrightarrow> (x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> P) \<Longrightarrow> P"
    2.47    by (blast intro: order_trans inf_le1 inf_le2)
    2.48  
    2.49 -lemma le_inf_iff: "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
    2.50 +lemma le_inf_iff: "x \<le> y \<sqinter> z \<longleftrightarrow> x \<le> y \<and> x \<le> z"
    2.51    by (blast intro: le_infI elim: le_infE)
    2.52  
    2.53 -lemma le_iff_inf: "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
    2.54 +lemma le_iff_inf: "x \<le> y \<longleftrightarrow> x \<sqinter> y = x"
    2.55    by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1] simp add: le_inf_iff)
    2.56  
    2.57 -lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
    2.58 +lemma inf_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<le> c \<sqinter> d"
    2.59    by (fast intro: inf_greatest le_infI1 le_infI2)
    2.60  
    2.61 -lemma mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B" for f :: "'a \<Rightarrow> 'b::semilattice_inf"
    2.62 +lemma mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B" for f :: "'a \<Rightarrow> 'b::semilattice_inf"
    2.63    by (auto simp add: mono_def intro: Lattices.inf_greatest)
    2.64  
    2.65  end
    2.66 @@ -220,28 +216,28 @@
    2.67  context semilattice_sup
    2.68  begin
    2.69  
    2.70 -lemma le_supI1: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    2.71 +lemma le_supI1: "x \<le> a \<Longrightarrow> x \<le> a \<squnion> b"
    2.72    by (rule order_trans) auto
    2.73  
    2.74 -lemma le_supI2: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    2.75 +lemma le_supI2: "x \<le> b \<Longrightarrow> x \<le> a \<squnion> b"
    2.76    by (rule order_trans) auto
    2.77  
    2.78 -lemma le_supI: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
    2.79 +lemma le_supI: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> a \<squnion> b \<le> x"
    2.80    by (fact sup_least) (* FIXME: duplicate lemma *)
    2.81  
    2.82 -lemma le_supE: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    2.83 +lemma le_supE: "a \<squnion> b \<le> x \<Longrightarrow> (a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> P) \<Longrightarrow> P"
    2.84    by (blast intro: order_trans sup_ge1 sup_ge2)
    2.85  
    2.86 -lemma le_sup_iff: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
    2.87 +lemma le_sup_iff: "x \<squnion> y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z"
    2.88    by (blast intro: le_supI elim: le_supE)
    2.89  
    2.90 -lemma le_iff_sup: "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
    2.91 +lemma le_iff_sup: "x \<le> y \<longleftrightarrow> x \<squnion> y = y"
    2.92    by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1] simp add: le_sup_iff)
    2.93  
    2.94 -lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
    2.95 +lemma sup_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<le> c \<squnion> d"
    2.96    by (fast intro: sup_least le_supI1 le_supI2)
    2.97  
    2.98 -lemma mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)" for f :: "'a \<Rightarrow> 'b::semilattice_sup"
    2.99 +lemma mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)" for f :: "'a \<Rightarrow> 'b::semilattice_sup"
   2.100    by (auto simp add: mono_def intro: Lattices.sup_least)
   2.101  
   2.102  end
   2.103 @@ -284,10 +280,10 @@
   2.104  lemma inf_right_idem: "(x \<sqinter> y) \<sqinter> y = x \<sqinter> y"
   2.105    by (fact inf.right_idem) (* already simp *)
   2.106  
   2.107 -lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
   2.108 +lemma inf_absorb1: "x \<le> y \<Longrightarrow> x \<sqinter> y = x"
   2.109    by (rule antisym) auto
   2.110  
   2.111 -lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
   2.112 +lemma inf_absorb2: "y \<le> x \<Longrightarrow> x \<sqinter> y = y"
   2.113    by (rule antisym) auto
   2.114  
   2.115  lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
   2.116 @@ -326,10 +322,10 @@
   2.117  lemma sup_left_idem [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   2.118    by (fact sup.left_idem)
   2.119  
   2.120 -lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
   2.121 +lemma sup_absorb1: "y \<le> x \<Longrightarrow> x \<squnion> y = x"
   2.122    by (rule antisym) auto
   2.123  
   2.124 -lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   2.125 +lemma sup_absorb2: "x \<le> y \<Longrightarrow> x \<squnion> y = y"
   2.126    by (rule antisym) auto
   2.127  
   2.128  lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
   2.129 @@ -358,10 +354,10 @@
   2.130  
   2.131  text \<open>Towards distributivity.\<close>
   2.132  
   2.133 -lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   2.134 +lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<le> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   2.135    by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
   2.136  
   2.137 -lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
   2.138 +lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<le> x \<sqinter> (y \<squnion> z)"
   2.139    by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
   2.140  
   2.141  text \<open>If you have one of them, you have them all.\<close>
   2.142 @@ -402,10 +398,10 @@
   2.143  context semilattice_inf
   2.144  begin
   2.145  
   2.146 -lemma less_infI1: "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   2.147 +lemma less_infI1: "a < x \<Longrightarrow> a \<sqinter> b < x"
   2.148    by (auto simp add: less_le inf_absorb1 intro: le_infI1)
   2.149  
   2.150 -lemma less_infI2: "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   2.151 +lemma less_infI2: "b < x \<Longrightarrow> a \<sqinter> b < x"
   2.152    by (auto simp add: less_le inf_absorb2 intro: le_infI2)
   2.153  
   2.154  end
   2.155 @@ -413,11 +409,11 @@
   2.156  context semilattice_sup
   2.157  begin
   2.158  
   2.159 -lemma less_supI1: "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
   2.160 +lemma less_supI1: "x < a \<Longrightarrow> x < a \<squnion> b"
   2.161    using dual_semilattice
   2.162    by (rule semilattice_inf.less_infI1)
   2.163  
   2.164 -lemma less_supI2: "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
   2.165 +lemma less_supI2: "x < b \<Longrightarrow> x < a \<squnion> b"
   2.166    using dual_semilattice
   2.167    by (rule semilattice_inf.less_infI2)
   2.168  
   2.169 @@ -616,8 +612,8 @@
   2.170    by (rule boolean_algebra.compl_inf)
   2.171  
   2.172  lemma compl_mono:
   2.173 -  assumes "x \<sqsubseteq> y"
   2.174 -  shows "- y \<sqsubseteq> - x"
   2.175 +  assumes "x \<le> y"
   2.176 +  shows "- y \<le> - x"
   2.177  proof -
   2.178    from assms have "x \<squnion> y = y" by (simp only: le_iff_sup)
   2.179    then have "- (x \<squnion> y) = - y" by simp
   2.180 @@ -626,41 +622,41 @@
   2.181    then show ?thesis by (simp only: le_iff_inf)
   2.182  qed
   2.183  
   2.184 -lemma compl_le_compl_iff [simp]: "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
   2.185 +lemma compl_le_compl_iff [simp]: "- x \<le> - y \<longleftrightarrow> y \<le> x"
   2.186    by (auto dest: compl_mono)
   2.187  
   2.188  lemma compl_le_swap1:
   2.189 -  assumes "y \<sqsubseteq> - x"
   2.190 -  shows "x \<sqsubseteq> -y"
   2.191 +  assumes "y \<le> - x"
   2.192 +  shows "x \<le> -y"
   2.193  proof -
   2.194 -  from assms have "- (- x) \<sqsubseteq> - y" by (simp only: compl_le_compl_iff)
   2.195 +  from assms have "- (- x) \<le> - y" by (simp only: compl_le_compl_iff)
   2.196    then show ?thesis by simp
   2.197  qed
   2.198  
   2.199  lemma compl_le_swap2:
   2.200 -  assumes "- y \<sqsubseteq> x"
   2.201 -  shows "- x \<sqsubseteq> y"
   2.202 +  assumes "- y \<le> x"
   2.203 +  shows "- x \<le> y"
   2.204  proof -
   2.205 -  from assms have "- x \<sqsubseteq> - (- y)" by (simp only: compl_le_compl_iff)
   2.206 +  from assms have "- x \<le> - (- y)" by (simp only: compl_le_compl_iff)
   2.207    then show ?thesis by simp
   2.208  qed
   2.209  
   2.210 -lemma compl_less_compl_iff: "- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x"  (* TODO: declare [simp] ? *)
   2.211 +lemma compl_less_compl_iff: "- x < - y \<longleftrightarrow> y < x"  (* TODO: declare [simp] ? *)
   2.212    by (auto simp add: less_le)
   2.213  
   2.214  lemma compl_less_swap1:
   2.215 -  assumes "y \<sqsubset> - x"
   2.216 -  shows "x \<sqsubset> - y"
   2.217 +  assumes "y < - x"
   2.218 +  shows "x < - y"
   2.219  proof -
   2.220 -  from assms have "- (- x) \<sqsubset> - y" by (simp only: compl_less_compl_iff)
   2.221 +  from assms have "- (- x) < - y" by (simp only: compl_less_compl_iff)
   2.222    then show ?thesis by simp
   2.223  qed
   2.224  
   2.225  lemma compl_less_swap2:
   2.226 -  assumes "- y \<sqsubset> x"
   2.227 -  shows "- x \<sqsubset> y"
   2.228 +  assumes "- y < x"
   2.229 +  shows "- x < y"
   2.230  proof -
   2.231 -  from assms have "- x \<sqsubset> - (- y)"
   2.232 +  from assms have "- x < - (- y)"
   2.233      by (simp only: compl_less_compl_iff)
   2.234    then show ?thesis by simp
   2.235  qed
   2.236 @@ -772,31 +768,31 @@
   2.237  
   2.238  lemma (in semilattice_inf) inf_unique:
   2.239    fixes f  (infixl "\<triangle>" 70)
   2.240 -  assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x"
   2.241 -    and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y"
   2.242 -    and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
   2.243 +  assumes le1: "\<And>x y. x \<triangle> y \<le> x"
   2.244 +    and le2: "\<And>x y. x \<triangle> y \<le> y"
   2.245 +    and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
   2.246    shows "x \<sqinter> y = x \<triangle> y"
   2.247  proof (rule antisym)
   2.248 -  show "x \<triangle> y \<sqsubseteq> x \<sqinter> y"
   2.249 +  show "x \<triangle> y \<le> x \<sqinter> y"
   2.250      by (rule le_infI) (rule le1, rule le2)
   2.251 -  have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
   2.252 +  have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
   2.253      by (blast intro: greatest)
   2.254 -  show "x \<sqinter> y \<sqsubseteq> x \<triangle> y"
   2.255 +  show "x \<sqinter> y \<le> x \<triangle> y"
   2.256      by (rule leI) simp_all
   2.257  qed
   2.258  
   2.259  lemma (in semilattice_sup) sup_unique:
   2.260    fixes f  (infixl "\<nabla>" 70)
   2.261 -  assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y"
   2.262 -    and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y"
   2.263 -    and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x"
   2.264 +  assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y"
   2.265 +    and ge2: "\<And>x y. y \<le> x \<nabla> y"
   2.266 +    and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
   2.267    shows "x \<squnion> y = x \<nabla> y"
   2.268  proof (rule antisym)
   2.269 -  show "x \<squnion> y \<sqsubseteq> x \<nabla> y"
   2.270 +  show "x \<squnion> y \<le> x \<nabla> y"
   2.271      by (rule le_supI) (rule ge1, rule ge2)
   2.272 -  have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z"
   2.273 +  have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z"
   2.274      by (blast intro: least)
   2.275 -  show "x \<nabla> y \<sqsubseteq> x \<squnion> y"
   2.276 +  show "x \<nabla> y \<le> x \<squnion> y"
   2.277      by (rule leI) simp_all
   2.278  qed
   2.279  
   2.280 @@ -942,9 +938,4 @@
   2.281  lemma sup2CI: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
   2.282    by (auto simp add: sup_fun_def)
   2.283  
   2.284 -
   2.285 -no_notation
   2.286 -  less_eq (infix "\<sqsubseteq>" 50) and
   2.287 -  less (infix "\<sqsubset>" 50)
   2.288 -
   2.289  end