--- 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
--- 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 *}
--- 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"