--- a/src/HOL/Complete_Lattices.thy Wed Sep 07 11:59:07 2016 +0200
+++ b/src/HOL/Complete_Lattices.thy Wed Sep 07 11:59:09 2016 +0200
@@ -11,11 +11,6 @@
imports Fun
begin
-notation
- less_eq (infix "\<sqsubseteq>" 50) and
- less (infix "\<sqsubset>" 50)
-
-
subsection \<open>Syntactic infimum and supremum operations\<close>
class Inf =
@@ -116,10 +111,10 @@
in terms of infimum and supremum.\<close>
class complete_lattice = lattice + Inf + Sup + bot + top +
- assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
- and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
- and Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
- and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
+ assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<le> x"
+ and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A"
+ and Sup_upper: "x \<in> A \<Longrightarrow> x \<le> \<Squnion>A"
+ and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z"
and Inf_empty [simp]: "\<Sqinter>{} = \<top>"
and Sup_empty [simp]: "\<Squnion>{} = \<bottom>"
begin
@@ -158,40 +153,40 @@
"(\<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"
using Inf_eqI [of "f ` A" x] by auto
-lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
+lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<le> f i"
using Inf_lower [of _ "f ` A"] by simp
-lemma INF_greatest: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
+lemma INF_greatest: "(\<And>i. i \<in> A \<Longrightarrow> u \<le> f i) \<Longrightarrow> u \<le> (\<Sqinter>i\<in>A. f i)"
using Inf_greatest [of "f ` A"] by auto
-lemma SUP_upper: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
+lemma SUP_upper: "i \<in> A \<Longrightarrow> f i \<le> (\<Squnion>i\<in>A. f i)"
using Sup_upper [of _ "f ` A"] by simp
-lemma SUP_least: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
+lemma SUP_least: "(\<And>i. i \<in> A \<Longrightarrow> f i \<le> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<le> u"
using Sup_least [of "f ` A"] by auto
-lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
+lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<le> v \<Longrightarrow> \<Sqinter>A \<le> v"
using Inf_lower [of u A] by auto
-lemma INF_lower2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
+lemma INF_lower2: "i \<in> A \<Longrightarrow> f i \<le> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<le> u"
using INF_lower [of i A f] by auto
-lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
+lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<le> u \<Longrightarrow> v \<le> \<Squnion>A"
using Sup_upper [of u A] by auto
-lemma SUP_upper2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
+lemma SUP_upper2: "i \<in> A \<Longrightarrow> u \<le> f i \<Longrightarrow> u \<le> (\<Squnion>i\<in>A. f i)"
using SUP_upper [of i A f] by auto
-lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
+lemma le_Inf_iff: "b \<le> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<le> a)"
by (auto intro: Inf_greatest dest: Inf_lower)
-lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
+lemma le_INF_iff: "u \<le> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<le> f i)"
using le_Inf_iff [of _ "f ` A"] by simp
-lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
+lemma Sup_le_iff: "\<Squnion>A \<le> b \<longleftrightarrow> (\<forall>a\<in>A. a \<le> b)"
by (auto intro: Sup_least dest: Sup_upper)
-lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
+lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<le> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<le> u)"
using Sup_le_iff [of "f ` A"] by simp
lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
@@ -218,68 +213,68 @@
lemma Sup_UNIV [simp]: "\<Squnion>UNIV = \<top>"
by (auto intro!: antisym Sup_upper)
-lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
+lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
-lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
+lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
-lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
+lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<le> \<Sqinter>B"
by (auto intro: Inf_greatest Inf_lower)
-lemma Sup_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
+lemma Sup_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<le> \<Squnion>B"
by (auto intro: Sup_least Sup_upper)
lemma Inf_mono:
- assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b"
- shows "\<Sqinter>A \<sqsubseteq> \<Sqinter>B"
+ assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
+ shows "\<Sqinter>A \<le> \<Sqinter>B"
proof (rule Inf_greatest)
fix b assume "b \<in> B"
- with assms obtain a where "a \<in> A" and "a \<sqsubseteq> b" by blast
- from \<open>a \<in> A\<close> have "\<Sqinter>A \<sqsubseteq> a" by (rule Inf_lower)
- with \<open>a \<sqsubseteq> b\<close> show "\<Sqinter>A \<sqsubseteq> b" by auto
+ with assms obtain a where "a \<in> A" and "a \<le> b" by blast
+ from \<open>a \<in> A\<close> have "\<Sqinter>A \<le> a" by (rule Inf_lower)
+ with \<open>a \<le> b\<close> show "\<Sqinter>A \<le> b" by auto
qed
-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)"
+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)"
using Inf_mono [of "g ` B" "f ` A"] by auto
lemma Sup_mono:
- assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
- shows "\<Squnion>A \<sqsubseteq> \<Squnion>B"
+ assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
+ shows "\<Squnion>A \<le> \<Squnion>B"
proof (rule Sup_least)
fix a assume "a \<in> A"
- with assms obtain b where "b \<in> B" and "a \<sqsubseteq> b" by blast
- from \<open>b \<in> B\<close> have "b \<sqsubseteq> \<Squnion>B" by (rule Sup_upper)
- with \<open>a \<sqsubseteq> b\<close> show "a \<sqsubseteq> \<Squnion>B" by auto
+ with assms obtain b where "b \<in> B" and "a \<le> b" by blast
+ from \<open>b \<in> B\<close> have "b \<le> \<Squnion>B" by (rule Sup_upper)
+ with \<open>a \<le> b\<close> show "a \<le> \<Squnion>B" by auto
qed
-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)"
+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)"
using Sup_mono [of "f ` A" "g ` B"] by auto
-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)"
+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)"
\<comment> \<open>The last inclusion is POSITIVE!\<close>
by (blast intro: INF_mono dest: subsetD)
-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)"
+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)"
by (blast intro: SUP_mono dest: subsetD)
lemma Inf_less_eq:
- assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
+ assumes "\<And>v. v \<in> A \<Longrightarrow> v \<le> u"
and "A \<noteq> {}"
- shows "\<Sqinter>A \<sqsubseteq> u"
+ shows "\<Sqinter>A \<le> u"
proof -
from \<open>A \<noteq> {}\<close> obtain v where "v \<in> A" by blast
- moreover from \<open>v \<in> A\<close> assms(1) have "v \<sqsubseteq> u" by blast
+ moreover from \<open>v \<in> A\<close> assms(1) have "v \<le> u" by blast
ultimately show ?thesis by (rule Inf_lower2)
qed
lemma less_eq_Sup:
- assumes "\<And>v. v \<in> A \<Longrightarrow> u \<sqsubseteq> v"
+ assumes "\<And>v. v \<in> A \<Longrightarrow> u \<le> v"
and "A \<noteq> {}"
- shows "u \<sqsubseteq> \<Squnion>A"
+ shows "u \<le> \<Squnion>A"
proof -
from \<open>A \<noteq> {}\<close> obtain v where "v \<in> A" by blast
- moreover from \<open>v \<in> A\<close> assms(1) have "u \<sqsubseteq> v" by blast
+ moreover from \<open>v \<in> A\<close> assms(1) have "u \<le> v" by blast
ultimately show ?thesis by (rule Sup_upper2)
qed
@@ -295,10 +290,10 @@
shows "SUPREMUM A f = SUPREMUM B g"
by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
-lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
+lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<le> \<Sqinter>(A \<inter> B)"
by (auto intro: Inf_greatest Inf_lower)
-lemma Sup_inter_less_eq: "\<Squnion>(A \<inter> B) \<sqsubseteq> \<Squnion>A \<sqinter> \<Squnion>B "
+lemma Sup_inter_less_eq: "\<Squnion>(A \<inter> B) \<le> \<Squnion>A \<sqinter> \<Squnion>B "
by (auto intro: Sup_least Sup_upper)
lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
@@ -574,16 +569,16 @@
lemma complete_linorder_sup_max: "sup = max"
by (auto intro: antisym simp add: max_def fun_eq_iff)
-lemma Inf_less_iff: "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
+lemma Inf_less_iff: "\<Sqinter>S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
by (simp add: not_le [symmetric] le_Inf_iff)
-lemma INF_less_iff: "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
+lemma INF_less_iff: "(\<Sqinter>i\<in>A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
by (simp add: Inf_less_iff [of "f ` A"])
-lemma less_Sup_iff: "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
+lemma less_Sup_iff: "a < \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
by (simp add: not_le [symmetric] Sup_le_iff)
-lemma less_SUP_iff: "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
+lemma less_SUP_iff: "a < (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
by (simp add: less_Sup_iff [of _ "f ` A"])
lemma Sup_eq_top_iff [simp]: "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
@@ -1426,10 +1421,6 @@
text \<open>Finally\<close>
-no_notation
- less_eq (infix "\<sqsubseteq>" 50) and
- less (infix "\<sqsubset>" 50)
-
lemmas mem_simps =
insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
--- a/src/HOL/Lattices.thy Wed Sep 07 11:59:07 2016 +0200
+++ b/src/HOL/Lattices.thy Wed Sep 07 11:59:09 2016 +0200
@@ -161,19 +161,15 @@
subsection \<open>Concrete lattices\<close>
-notation
- less_eq (infix "\<sqsubseteq>" 50) and
- less (infix "\<sqsubset>" 50)
-
class semilattice_inf = order + inf +
- assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
- and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
- and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
+ assumes inf_le1 [simp]: "x \<sqinter> y \<le> x"
+ and inf_le2 [simp]: "x \<sqinter> y \<le> y"
+ and inf_greatest: "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
class semilattice_sup = order + sup +
- assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
- and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
- and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
+ assumes sup_ge1 [simp]: "x \<le> x \<squnion> y"
+ and sup_ge2 [simp]: "y \<le> x \<squnion> y"
+ and sup_least: "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x"
begin
text \<open>Dual lattice.\<close>
@@ -191,28 +187,28 @@
context semilattice_inf
begin
-lemma le_infI1: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+lemma le_infI1: "a \<le> x \<Longrightarrow> a \<sqinter> b \<le> x"
by (rule order_trans) auto
-lemma le_infI2: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+lemma le_infI2: "b \<le> x \<Longrightarrow> a \<sqinter> b \<le> x"
by (rule order_trans) auto
-lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
+lemma le_infI: "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> a \<sqinter> b"
by (fact inf_greatest) (* FIXME: duplicate lemma *)
-lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
+lemma le_infE: "x \<le> a \<sqinter> b \<Longrightarrow> (x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> P) \<Longrightarrow> P"
by (blast intro: order_trans inf_le1 inf_le2)
-lemma le_inf_iff: "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
+lemma le_inf_iff: "x \<le> y \<sqinter> z \<longleftrightarrow> x \<le> y \<and> x \<le> z"
by (blast intro: le_infI elim: le_infE)
-lemma le_iff_inf: "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
+lemma le_iff_inf: "x \<le> y \<longleftrightarrow> x \<sqinter> y = x"
by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1] simp add: le_inf_iff)
-lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
+lemma inf_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<le> c \<sqinter> d"
by (fast intro: inf_greatest le_infI1 le_infI2)
-lemma mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B" for f :: "'a \<Rightarrow> 'b::semilattice_inf"
+lemma mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B" for f :: "'a \<Rightarrow> 'b::semilattice_inf"
by (auto simp add: mono_def intro: Lattices.inf_greatest)
end
@@ -220,28 +216,28 @@
context semilattice_sup
begin
-lemma le_supI1: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+lemma le_supI1: "x \<le> a \<Longrightarrow> x \<le> a \<squnion> b"
by (rule order_trans) auto
-lemma le_supI2: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+lemma le_supI2: "x \<le> b \<Longrightarrow> x \<le> a \<squnion> b"
by (rule order_trans) auto
-lemma le_supI: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
+lemma le_supI: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> a \<squnion> b \<le> x"
by (fact sup_least) (* FIXME: duplicate lemma *)
-lemma le_supE: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
+lemma le_supE: "a \<squnion> b \<le> x \<Longrightarrow> (a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> P) \<Longrightarrow> P"
by (blast intro: order_trans sup_ge1 sup_ge2)
-lemma le_sup_iff: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
+lemma le_sup_iff: "x \<squnion> y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z"
by (blast intro: le_supI elim: le_supE)
-lemma le_iff_sup: "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
+lemma le_iff_sup: "x \<le> y \<longleftrightarrow> x \<squnion> y = y"
by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1] simp add: le_sup_iff)
-lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
+lemma sup_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<le> c \<squnion> d"
by (fast intro: sup_least le_supI1 le_supI2)
-lemma mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)" for f :: "'a \<Rightarrow> 'b::semilattice_sup"
+lemma mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)" for f :: "'a \<Rightarrow> 'b::semilattice_sup"
by (auto simp add: mono_def intro: Lattices.sup_least)
end
@@ -284,10 +280,10 @@
lemma inf_right_idem: "(x \<sqinter> y) \<sqinter> y = x \<sqinter> y"
by (fact inf.right_idem) (* already simp *)
-lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
+lemma inf_absorb1: "x \<le> y \<Longrightarrow> x \<sqinter> y = x"
by (rule antisym) auto
-lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
+lemma inf_absorb2: "y \<le> x \<Longrightarrow> x \<sqinter> y = y"
by (rule antisym) auto
lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
@@ -326,10 +322,10 @@
lemma sup_left_idem [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
by (fact sup.left_idem)
-lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
+lemma sup_absorb1: "y \<le> x \<Longrightarrow> x \<squnion> y = x"
by (rule antisym) auto
-lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
+lemma sup_absorb2: "x \<le> y \<Longrightarrow> x \<squnion> y = y"
by (rule antisym) auto
lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
@@ -358,10 +354,10 @@
text \<open>Towards distributivity.\<close>
-lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
+lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<le> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
-lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
+lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<le> x \<sqinter> (y \<squnion> z)"
by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
text \<open>If you have one of them, you have them all.\<close>
@@ -402,10 +398,10 @@
context semilattice_inf
begin
-lemma less_infI1: "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
+lemma less_infI1: "a < x \<Longrightarrow> a \<sqinter> b < x"
by (auto simp add: less_le inf_absorb1 intro: le_infI1)
-lemma less_infI2: "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
+lemma less_infI2: "b < x \<Longrightarrow> a \<sqinter> b < x"
by (auto simp add: less_le inf_absorb2 intro: le_infI2)
end
@@ -413,11 +409,11 @@
context semilattice_sup
begin
-lemma less_supI1: "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
+lemma less_supI1: "x < a \<Longrightarrow> x < a \<squnion> b"
using dual_semilattice
by (rule semilattice_inf.less_infI1)
-lemma less_supI2: "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
+lemma less_supI2: "x < b \<Longrightarrow> x < a \<squnion> b"
using dual_semilattice
by (rule semilattice_inf.less_infI2)
@@ -616,8 +612,8 @@
by (rule boolean_algebra.compl_inf)
lemma compl_mono:
- assumes "x \<sqsubseteq> y"
- shows "- y \<sqsubseteq> - x"
+ assumes "x \<le> y"
+ shows "- y \<le> - x"
proof -
from assms have "x \<squnion> y = y" by (simp only: le_iff_sup)
then have "- (x \<squnion> y) = - y" by simp
@@ -626,41 +622,41 @@
then show ?thesis by (simp only: le_iff_inf)
qed
-lemma compl_le_compl_iff [simp]: "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
+lemma compl_le_compl_iff [simp]: "- x \<le> - y \<longleftrightarrow> y \<le> x"
by (auto dest: compl_mono)
lemma compl_le_swap1:
- assumes "y \<sqsubseteq> - x"
- shows "x \<sqsubseteq> -y"
+ assumes "y \<le> - x"
+ shows "x \<le> -y"
proof -
- from assms have "- (- x) \<sqsubseteq> - y" by (simp only: compl_le_compl_iff)
+ from assms have "- (- x) \<le> - y" by (simp only: compl_le_compl_iff)
then show ?thesis by simp
qed
lemma compl_le_swap2:
- assumes "- y \<sqsubseteq> x"
- shows "- x \<sqsubseteq> y"
+ assumes "- y \<le> x"
+ shows "- x \<le> y"
proof -
- from assms have "- x \<sqsubseteq> - (- y)" by (simp only: compl_le_compl_iff)
+ from assms have "- x \<le> - (- y)" by (simp only: compl_le_compl_iff)
then show ?thesis by simp
qed
-lemma compl_less_compl_iff: "- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x" (* TODO: declare [simp] ? *)
+lemma compl_less_compl_iff: "- x < - y \<longleftrightarrow> y < x" (* TODO: declare [simp] ? *)
by (auto simp add: less_le)
lemma compl_less_swap1:
- assumes "y \<sqsubset> - x"
- shows "x \<sqsubset> - y"
+ assumes "y < - x"
+ shows "x < - y"
proof -
- from assms have "- (- x) \<sqsubset> - y" by (simp only: compl_less_compl_iff)
+ from assms have "- (- x) < - y" by (simp only: compl_less_compl_iff)
then show ?thesis by simp
qed
lemma compl_less_swap2:
- assumes "- y \<sqsubset> x"
- shows "- x \<sqsubset> y"
+ assumes "- y < x"
+ shows "- x < y"
proof -
- from assms have "- x \<sqsubset> - (- y)"
+ from assms have "- x < - (- y)"
by (simp only: compl_less_compl_iff)
then show ?thesis by simp
qed
@@ -772,31 +768,31 @@
lemma (in semilattice_inf) inf_unique:
fixes f (infixl "\<triangle>" 70)
- assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x"
- and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y"
- and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
+ assumes le1: "\<And>x y. x \<triangle> y \<le> x"
+ and le2: "\<And>x y. x \<triangle> y \<le> y"
+ and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
shows "x \<sqinter> y = x \<triangle> y"
proof (rule antisym)
- show "x \<triangle> y \<sqsubseteq> x \<sqinter> y"
+ show "x \<triangle> y \<le> x \<sqinter> y"
by (rule le_infI) (rule le1, rule le2)
- have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
+ have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
by (blast intro: greatest)
- show "x \<sqinter> y \<sqsubseteq> x \<triangle> y"
+ show "x \<sqinter> y \<le> x \<triangle> y"
by (rule leI) simp_all
qed
lemma (in semilattice_sup) sup_unique:
fixes f (infixl "\<nabla>" 70)
- assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y"
- and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y"
- and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x"
+ assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y"
+ and ge2: "\<And>x y. y \<le> x \<nabla> y"
+ and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
shows "x \<squnion> y = x \<nabla> y"
proof (rule antisym)
- show "x \<squnion> y \<sqsubseteq> x \<nabla> y"
+ show "x \<squnion> y \<le> x \<nabla> y"
by (rule le_supI) (rule ge1, rule ge2)
- have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z"
+ have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z"
by (blast intro: least)
- show "x \<nabla> y \<sqsubseteq> x \<squnion> y"
+ show "x \<nabla> y \<le> x \<squnion> y"
by (rule leI) simp_all
qed
@@ -942,9 +938,4 @@
lemma sup2CI: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
by (auto simp add: sup_fun_def)
-
-no_notation
- less_eq (infix "\<sqsubseteq>" 50) and
- less (infix "\<sqsubset>" 50)
-
end