# HG changeset patch
# User haftmann
# Date 1291138823 -3600
# Node ID a3af470a55d29db2952d136352af50a9add50c05
# Parent  ab0a8cc7976a848373f44cfa83fed5b2a11da01f# Parent  c55ee3793712eb9bd5e82f7b64d1d814f2565a5d
merged

diff -r c55ee3793712 -r a3af470a55d2 src/HOL/HOLCF/Library/List_Cpo.thy
--- a/src/HOL/HOLCF/Library/List_Cpo.thy	Tue Nov 30 17:22:59 2010 +0100
+++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Tue Nov 30 18:40:23 2010 +0100
@@ -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
diff -r c55ee3793712 -r a3af470a55d2 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Tue Nov 30 17:22:59 2010 +0100
+++ b/src/HOL/RealDef.thy	Tue Nov 30 18:40:23 2010 +0100
@@ -14,8 +14,8 @@
 text {*
   This theory contains a formalization of the real numbers as
   equivalence classes of Cauchy sequences of rationals.  See
-  \url{HOL/ex/Dedekind_Real.thy} for an alternative construction
-  using Dedekind cuts.
+  @{file "~~/src/HOL/ex/Dedekind_Real.thy"} for an alternative
+  construction using Dedekind cuts.
 *}
 
 subsection {* Preliminary lemmas *}
diff -r c55ee3793712 -r a3af470a55d2 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Tue Nov 30 17:22:59 2010 +0100
+++ b/src/HOL/SEQ.thy	Tue Nov 30 18:40:23 2010 +0100
@@ -221,15 +221,7 @@
 lemma LIMSEQ_unique:
   fixes a b :: "'a::metric_space"
   shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
-apply (rule ccontr)
-apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
-apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
-apply (clarify, rename_tac M N)
-apply (subgoal_tac "dist a b < dist a b / 2 + dist a b / 2", simp)
-apply (subgoal_tac "dist a b \<le> dist (X (max M N)) a + dist (X (max M N)) b")
-apply (erule le_less_trans, rule add_strict_mono, simp, simp)
-apply (subst dist_commute, rule dist_triangle)
-done
+by (drule (1) tendsto_dist, simp add: LIMSEQ_const_iff)
 
 lemma (in bounded_linear) LIMSEQ:
   "X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a"