# HG changeset patch
# User huffman
# Date 1201810882 -3600
# Node ID 29c1e3e98276a446822724c7f63b049b96d03492
# Parent  b30a342a6e29ed60888fc1ad41f6f5b4c4d075ed
new discrete_cpo axclass

diff -r b30a342a6e29 -r 29c1e3e98276 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Thu Jan 31 11:47:12 2008 +0100
+++ b/src/HOLCF/Pcpo.thy	Thu Jan 31 21:21:22 2008 +0100
@@ -314,6 +314,36 @@
 lemma chfin2finch: "chain (Y::nat \<Rightarrow> 'a::chfin) \<Longrightarrow> finite_chain Y"
 by (simp add: chfin finite_chain_def)
 
+text {* Discrete cpos *}
+
+axclass discrete_cpo < sq_ord
+  discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
+
+instance discrete_cpo < po
+by (intro_classes, simp_all)
+
+text {* In a discrete cpo, every chain is constant *}
+
+lemma discrete_chain_const:
+  assumes S: "chain (S::nat \<Rightarrow> 'a::discrete_cpo)"
+  shows "\<exists>x. S = (\<lambda>i. x)"
+proof (intro exI ext)
+  fix i :: nat
+  have "S 0 \<sqsubseteq> S i" using S le0 by (rule chain_mono)
+  hence "S 0 = S i" by simp
+  thus "S i = S 0" by (rule sym)
+qed
+
+instance discrete_cpo < cpo
+proof
+  fix S :: "nat \<Rightarrow> 'a"
+  assume S: "chain S"
+  hence "\<exists>x. S = (\<lambda>i. x)"
+    by (rule discrete_chain_const)
+  thus "\<exists>x. range S <<| x"
+    by (fast intro: lub_const)
+qed
+
 text {* lemmata for improved admissibility introdution rule *}
 
 lemma infinite_chain_adm_lemma: