--- a/src/HOL/Lattice/Bounds.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Lattice/Bounds.thy Fri Nov 17 02:20:03 2006 +0100
@@ -16,16 +16,19 @@
*}
definition
- is_inf :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ is_inf :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
"is_inf x y inf = (inf \<sqsubseteq> x \<and> inf \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> inf))"
- is_sup :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+definition
+ is_sup :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
"is_sup x y sup = (x \<sqsubseteq> sup \<and> y \<sqsubseteq> sup \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> sup \<sqsubseteq> z))"
- is_Inf :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool"
+definition
+ is_Inf :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool" where
"is_Inf A inf = ((\<forall>x \<in> A. inf \<sqsubseteq> x) \<and> (\<forall>z. (\<forall>x \<in> A. z \<sqsubseteq> x) \<longrightarrow> z \<sqsubseteq> inf))"
- is_Sup :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool"
+definition
+ is_Sup :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool" where
"is_Sup A sup = ((\<forall>x \<in> A. x \<sqsubseteq> sup) \<and> (\<forall>z. (\<forall>x \<in> A. x \<sqsubseteq> z) \<longrightarrow> sup \<sqsubseteq> z))"
text {*