--- a/src/HOLCF/Cont.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Cont.thy Sun Oct 21 14:21:48 2007 +0200
@@ -20,15 +20,17 @@
subsection {* Definitions *}
-constdefs
- monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" -- "monotonicity"
- "monofun f \<equiv> \<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y"
+definition
+ monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" -- "monotonicity" where
+ "monofun f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
- contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" -- "first cont. def"
- "contlub f \<equiv> \<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))"
+definition
+ contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" -- "first cont. def" where
+ "contlub f = (\<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i)))"
- cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" -- "secnd cont. def"
- "cont f \<equiv> \<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)"
+definition
+ cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" -- "secnd cont. def" where
+ "cont f = (\<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i))"
lemma contlubI:
"\<lbrakk>\<And>Y. chain Y \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))\<rbrakk> \<Longrightarrow> contlub f"