# HG changeset patch
# User huffman
# Date 1291070260 28800
# Node ID 63276d22ea6028649c7975dfb2ced64f3c2cef89
# Parent  5a195f11ef46b17c4d9b3ad8993c66e2b82898ca
instance list :: (discrete_cpo) discrete_cpo;
compactness lemmas for Nil, Cons;
instance list :: (chfin) chfin;

diff -r 5a195f11ef46 -r 63276d22ea60 src/HOL/HOLCF/Library/List_Cpo.thy
--- a/src/HOL/HOLCF/Library/List_Cpo.thy	Mon Nov 29 16:10:44 2010 +0100
+++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Mon Nov 29 14:37:40 2010 -0800
@@ -237,6 +237,54 @@
 deserve to have continuity lemmas.  I'll add more as they are
 needed. *}
 
+subsection {* Lists are a discrete cpo *}
+
+instance list :: (discrete_cpo) discrete_cpo
+proof
+  fix xs ys :: "'a list"
+  show "xs \<sqsubseteq> ys \<longleftrightarrow> xs = ys"
+    by (induct xs arbitrary: ys, case_tac [!] ys, simp_all)
+qed
+
+subsection {* Compactness and chain-finiteness *}
+
+lemma compact_Nil [simp]: "compact []"
+apply (rule compactI2)
+apply (erule list_chain_cases)
+apply simp
+apply (simp add: lub_Cons)
+done
+
+lemma compact_Cons: "\<lbrakk>compact x; compact xs\<rbrakk> \<Longrightarrow> compact (x # xs)"
+apply (rule compactI2)
+apply (erule list_chain_cases)
+apply (auto simp add: lub_Cons dest!: compactD2)
+apply (rename_tac i j, rule_tac x="max i j" in exI)
+apply (drule (1) below_trans [OF _ chain_mono [OF _ le_maxI1]])
+apply (drule (1) below_trans [OF _ chain_mono [OF _ le_maxI2]])
+apply (erule (1) conjI)
+done
+
+lemma compact_Cons_iff [simp]:
+  "compact (x # xs) \<longleftrightarrow> compact x \<and> compact xs"
+apply (safe intro!: compact_Cons)
+apply (simp only: compact_def)
+apply (subgoal_tac "cont (\<lambda>x. x # xs)")
+apply (drule (1) adm_subst, simp, simp)
+apply (simp only: compact_def)
+apply (subgoal_tac "cont (\<lambda>xs. x # xs)")
+apply (drule (1) adm_subst, simp, simp)
+done
+
+instance list :: (chfin) chfin
+proof
+  fix Y :: "nat \<Rightarrow> 'a list" assume "chain Y"
+  moreover have "\<And>(xs::'a list). compact xs"
+    by (induct_tac xs, simp_all)
+  ultimately show "\<exists>i. max_in_chain i Y"
+    by (rule compact_imp_max_in_chain)
+qed
+
 subsection {* Using lists with fixrec *}
 
 definition