--- a/src/HOL/Complete_Lattice.thy Sun Jul 10 21:39:03 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy Sun Jul 10 21:56:39 2011 +0200
@@ -190,58 +190,58 @@
lemma le_INFI: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. M i)"
by (auto simp add: INFI_def intro: Inf_greatest)
-lemma SUP_le_iff: "(SUP i:A. M i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. M i \<sqsubseteq> u)"
+lemma SUP_le_iff: "(\<Squnion>i\<in>A. M i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. M i \<sqsubseteq> u)"
unfolding SUPR_def by (auto simp add: Sup_le_iff)
-lemma le_INF_iff: "u \<sqsubseteq> (INF i:A. M i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> M i)"
+lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. M i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> M i)"
unfolding INFI_def by (auto simp add: le_Inf_iff)
-lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
+lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. M) = M"
by (auto intro: antisym INF_leI le_INFI)
-lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
+lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. M) = M"
by (auto intro: antisym SUP_leI le_SUPI)
lemma INF_mono:
- "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INF n:A. f n) \<le> (INF n:B. g n)"
+ "(\<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)"
by (force intro!: Inf_mono simp: INFI_def)
lemma SUP_mono:
- "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n:A. f n) \<le> (SUP n:B. g n)"
+ "(\<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)"
by (force intro!: Sup_mono simp: SUPR_def)
-lemma INF_subset: "A \<subseteq> B \<Longrightarrow> INFI B f \<le> INFI A f"
+lemma INF_subset: "A \<subseteq> B \<Longrightarrow> INFI B f \<sqsubseteq> INFI A f"
by (intro INF_mono) auto
-lemma SUP_subset: "A \<subseteq> B \<Longrightarrow> SUPR A f \<le> SUPR B f"
+lemma SUP_subset: "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f"
by (intro SUP_mono) auto
-lemma INF_commute: "(INF i:A. INF j:B. f i j) = (INF j:B. INF i:A. f i j)"
+lemma INF_commute: "(\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>A. f i j)"
by (iprover intro: INF_leI le_INFI order_trans antisym)
-lemma SUP_commute: "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)"
+lemma SUP_commute: "(\<Squnion>i\<in>A. \<Squnion>j\<in>B. f i j) = (\<Squnion>j\<in>B. \<Squnion>i\<in>A. f i j)"
by (iprover intro: SUP_leI le_SUPI order_trans antisym)
end
lemma Inf_less_iff:
fixes a :: "'a\<Colon>{complete_lattice,linorder}"
- shows "Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
+ shows "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
unfolding not_le[symmetric] le_Inf_iff by auto
lemma less_Sup_iff:
fixes a :: "'a\<Colon>{complete_lattice,linorder}"
- shows "a < Sup S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
+ shows "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
unfolding not_le[symmetric] Sup_le_iff by auto
lemma INF_less_iff:
fixes a :: "'a::{complete_lattice,linorder}"
- shows "(INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
+ shows "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
unfolding INFI_def Inf_less_iff by auto
lemma less_SUP_iff:
fixes a :: "'a::{complete_lattice,linorder}"
- shows "a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
+ shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
unfolding SUPR_def less_Sup_iff by auto
subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
@@ -265,7 +265,7 @@
proof (rule ext)+
fix A :: "'a set"
fix P :: "'a \<Rightarrow> bool"
- show "(INF x:A. P x) \<longleftrightarrow> (\<forall>x \<in> A. P x)"
+ show "(\<Sqinter>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)"
by (auto simp add: Ball_def INFI_def Inf_bool_def)
qed
@@ -274,7 +274,7 @@
proof (rule ext)+
fix A :: "'a set"
fix P :: "'a \<Rightarrow> bool"
- show "(SUP x:A. P x) \<longleftrightarrow> (\<exists>x \<in> A. P x)"
+ show "(\<Squnion>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P x)"
by (auto simp add: Bex_def SUPR_def Sup_bool_def)
qed
@@ -354,7 +354,7 @@
lemma (in complete_lattice) Inf_less_eq:
assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
and "A \<noteq> {}"
- shows "\<Sqinter>A \<le> u"
+ shows "\<Sqinter>A \<sqsubseteq> u"
proof -
from `A \<noteq> {}` obtain v where "v \<in> A" by blast
moreover with assms have "v \<sqsubseteq> u" by blast
--- a/src/HOL/Lattices.thy Sun Jul 10 21:39:03 2011 +0200
+++ b/src/HOL/Lattices.thy Sun Jul 10 21:56:39 2011 +0200
@@ -68,7 +68,7 @@
text {* Dual lattice *}
lemma dual_semilattice:
- "class.semilattice_inf (op \<ge>) (op >) sup"
+ "class.semilattice_inf greater_eq greater sup"
by (rule class.semilattice_inf.intro, rule dual_order)
(unfold_locales, simp_all add: sup_least)
@@ -104,7 +104,7 @@
"x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
-lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
+lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
by (fast intro: inf_greatest le_infI1 le_infI2)
lemma mono_inf:
@@ -141,7 +141,7 @@
"x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
-lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
+lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
by (fast intro: sup_least le_supI1 le_supI2)
lemma mono_sup:
@@ -420,7 +420,7 @@
begin
lemma dual_bounded_lattice:
- "class.bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+ "class.bounded_lattice greater_eq greater sup inf \<top> \<bottom>"
by unfold_locales (auto simp add: less_le_not_le)
end
@@ -432,7 +432,7 @@
begin
lemma dual_boolean_algebra:
- "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+ "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus greater_eq greater sup inf \<top> \<bottom>"
by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
(unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
@@ -506,7 +506,7 @@
lemma compl_sup [simp]:
"- (x \<squnion> y) = - x \<sqinter> - y"
proof -
- interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
+ interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus greater_eq greater sup inf \<top> \<bottom>
by (rule dual_boolean_algebra)
then show ?thesis by simp
qed
@@ -523,7 +523,7 @@
qed
lemma compl_le_compl_iff: (* TODO: declare [simp] ? *)
- "- x \<le> - y \<longleftrightarrow> y \<le> x"
+ "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
by (auto dest: compl_mono)
end