# HG changeset patch
# User huffman
# Date 1199938543 -3600
# Node ID 98b93782c3b130bcdaee286c0aa8369ab43bdabf
# Parent  bfd53f791c10ff7c813fb0abe20137f44135b0bb
new compactness lemmas

diff -r bfd53f791c10 -r 98b93782c3b1 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Thu Jan 10 05:11:09 2008 +0100
+++ b/src/HOLCF/Cprod.thy	Thu Jan 10 05:15:43 2008 +0100
@@ -342,9 +342,27 @@
 lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
 by (auto simp add: po_eq_conv less_cprod)
 
-lemma compact_cpair [simp]: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
+lemma cfst_less_iff: "cfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <y, csnd\<cdot>x>"
+by (simp add: less_cprod)
+
+lemma csnd_less_iff: "csnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <cfst\<cdot>x, y>"
+by (simp add: less_cprod)
+
+lemma compact_cfst: "compact x \<Longrightarrow> compact (cfst\<cdot>x)"
+by (rule compactI, simp add: cfst_less_iff)
+
+lemma compact_csnd: "compact x \<Longrightarrow> compact (csnd\<cdot>x)"
+by (rule compactI, simp add: csnd_less_iff)
+
+lemma compact_cpair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
 by (rule compactI, simp add: less_cprod)
 
+lemma compact_cpair_iff [simp]: "compact <x, y> = (compact x \<and> compact y)"
+apply (safe intro!: compact_cpair)
+apply (drule compact_cfst, simp)
+apply (drule compact_csnd, simp)
+done
+
 lemma lub_cprod2: 
   "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
 apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)
diff -r bfd53f791c10 -r 98b93782c3b1 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Thu Jan 10 05:11:09 2008 +0100
+++ b/src/HOLCF/Up.thy	Thu Jan 10 05:15:43 2008 +0100
@@ -325,29 +325,27 @@
   (\<exists>j. \<forall>i. Y (i + j) = up\<cdot>(A i))) \<or> Y = (\<lambda>i. \<bottom>)"
 by (simp add: inst_up_pcpo up_def cont_Iup up_chain_lemma)
 
+lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
+apply (rule compactI2)
+apply (drule up_chain_cases, safe)
+apply (drule (1) compactD2, simp)
+apply (erule exE, rule_tac x="i + j" in exI)
+apply simp
+apply simp
+done
+
+lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x"
+unfolding compact_def
+by (drule adm_subst [OF cont_Rep_CFun2 [where f=up]], simp)
+
+lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x"
+by (safe elim!: compact_up compact_upD)
+
 instance u :: (chfin) chfin
 apply (intro_classes, clarify)
-apply (drule up_chain_cases, safe)
-apply (drule chfin [rule_format])
-apply (erule exE, rename_tac n)
-apply (rule_tac x="n + j" in exI)
-apply (simp only: max_in_chain_def)
-apply (clarify, rename_tac k)
-apply (subgoal_tac "\<exists>m. k = m + j", clarsimp)
-apply (rule_tac x="k - j" in exI, simp)
-apply (simp add: max_in_chain_def)
-done
-
-lemma compact_up [simp]: "compact x \<Longrightarrow> compact (up\<cdot>x)"
-apply (unfold compact_def)
-apply (rule admI)
-apply (drule up_chain_cases)
-apply (elim disjE exE conjE)
-apply simp
-apply (erule (1) admD)
-apply (rule allI, drule_tac x="i + j" in spec)
-apply simp
-apply simp
+apply (erule compact_imp_max_in_chain)
+apply (rule_tac p="\<Squnion>i. Y i" in upE)
+apply (simp, simp add: compact_chfin)
 done
 
 text {* properties of fup *}