1.1 --- a/src/HOL/HOLCF/Library/List_Cpo.thy	Mon Nov 29 16:10:44 2010 +0100
     1.2 +++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Mon Nov 29 14:37:40 2010 -0800
     1.3 @@ -237,6 +237,54 @@
     1.4  deserve to have continuity lemmas.  I'll add more as they are
     1.5  needed. *}
     1.6  
     1.7 +subsection {* Lists are a discrete cpo *}
     1.8 +
     1.9 +instance list :: (discrete_cpo) discrete_cpo
    1.10 +proof
    1.11 +  fix xs ys :: "'a list"
    1.12 +  show "xs \<sqsubseteq> ys \<longleftrightarrow> xs = ys"
    1.13 +    by (induct xs arbitrary: ys, case_tac [!] ys, simp_all)
    1.14 +qed
    1.15 +
    1.16 +subsection {* Compactness and chain-finiteness *}
    1.17 +
    1.18 +lemma compact_Nil [simp]: "compact []"
    1.19 +apply (rule compactI2)
    1.20 +apply (erule list_chain_cases)
    1.21 +apply simp
    1.22 +apply (simp add: lub_Cons)
    1.23 +done
    1.24 +
    1.25 +lemma compact_Cons: "\<lbrakk>compact x; compact xs\<rbrakk> \<Longrightarrow> compact (x # xs)"
    1.26 +apply (rule compactI2)
    1.27 +apply (erule list_chain_cases)
    1.28 +apply (auto simp add: lub_Cons dest!: compactD2)
    1.29 +apply (rename_tac i j, rule_tac x="max i j" in exI)
    1.30 +apply (drule (1) below_trans [OF _ chain_mono [OF _ le_maxI1]])
    1.31 +apply (drule (1) below_trans [OF _ chain_mono [OF _ le_maxI2]])
    1.32 +apply (erule (1) conjI)
    1.33 +done
    1.34 +
    1.35 +lemma compact_Cons_iff [simp]:
    1.36 +  "compact (x # xs) \<longleftrightarrow> compact x \<and> compact xs"
    1.37 +apply (safe intro!: compact_Cons)
    1.38 +apply (simp only: compact_def)
    1.39 +apply (subgoal_tac "cont (\<lambda>x. x # xs)")
    1.40 +apply (drule (1) adm_subst, simp, simp)
    1.41 +apply (simp only: compact_def)
    1.42 +apply (subgoal_tac "cont (\<lambda>xs. x # xs)")
    1.43 +apply (drule (1) adm_subst, simp, simp)
    1.44 +done
    1.45 +
    1.46 +instance list :: (chfin) chfin
    1.47 +proof
    1.48 +  fix Y :: "nat \<Rightarrow> 'a list" assume "chain Y"
    1.49 +  moreover have "\<And>(xs::'a list). compact xs"
    1.50 +    by (induct_tac xs, simp_all)
    1.51 +  ultimately show "\<exists>i. max_in_chain i Y"
    1.52 +    by (rule compact_imp_max_in_chain)
    1.53 +qed
    1.54 +
    1.55  subsection {* Using lists with fixrec *}
    1.56  
    1.57  definition