# HG changeset patch
# User huffman
# Date 1129078869 -7200
# Node ID 3032e90c49753ffa4de2c19bf059c8ac75b9d6b1
# Parent  2922be3544f8587c052df054506dcb70cec8b905
added compactness theorems

diff -r 2922be3544f8 -r 3032e90c4975 src/HOLCF/Cprod.ML
--- a/src/HOLCF/Cprod.ML	Wed Oct 12 01:43:37 2005 +0200
+++ b/src/HOLCF/Cprod.ML	Wed Oct 12 03:01:09 2005 +0200
@@ -6,6 +6,7 @@
 val cfst_def = thm "cfst_def";
 val cfst_strict = thm "cfst_strict";
 val CLet_def = thm "CLet_def";
+val compact_cpair = thm "compact_cpair";
 val cont_fst = thm "cont_fst";
 val contlub_fst = thm "contlub_fst";
 val contlub_pair1 = thm "contlub_pair1";
diff -r 2922be3544f8 -r 3032e90c4975 src/HOLCF/One.ML
--- a/src/HOLCF/One.ML	Wed Oct 12 01:43:37 2005 +0200
+++ b/src/HOLCF/One.ML	Wed Oct 12 03:01:09 2005 +0200
@@ -1,6 +1,7 @@
 
 (* legacy ML bindings *)
 
+val compact_ONE = thm "compact_ONE";
 val dist_eq_one = thms "dist_eq_one";
 val dist_less_one = thm "dist_less_one";
 val Exh_one = thm "Exh_one";
diff -r 2922be3544f8 -r 3032e90c4975 src/HOLCF/One.thy
--- a/src/HOLCF/One.thy	Wed Oct 12 01:43:37 2005 +0200
+++ b/src/HOLCF/One.thy	Wed Oct 12 03:01:09 2005 +0200
@@ -45,4 +45,7 @@
 apply simp_all
 done
 
+lemma compact_ONE [simp]: "compact ONE"
+by (rule compact_chfin)
+
 end
diff -r 2922be3544f8 -r 3032e90c4975 src/HOLCF/Sprod.ML
--- a/src/HOLCF/Sprod.ML	Wed Oct 12 01:43:37 2005 +0200
+++ b/src/HOLCF/Sprod.ML	Wed Oct 12 03:01:09 2005 +0200
@@ -1,6 +1,7 @@
 
 (* legacy ML bindings *)
 
+val compact_spair = thm "compact_spair";
 val eq_sprod = thm "eq_sprod";
 val Exh_Sprod2 = thm "Exh_Sprod2"; (* *)
 val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2"; (* *)
diff -r 2922be3544f8 -r 3032e90c4975 src/HOLCF/Ssum.ML
--- a/src/HOLCF/Ssum.ML	Wed Oct 12 01:43:37 2005 +0200
+++ b/src/HOLCF/Ssum.ML	Wed Oct 12 03:01:09 2005 +0200
@@ -2,6 +2,8 @@
 (* legacy ML bindings *)
 
 val beta_sscase = thm "beta_sscase";
+val compact_sinl = thm "compact_sinl";
+val compact_sinr = thm "compact_sinr";
 val cont_Iwhen1 = thm "cont_Iwhen1";
 val cont_Iwhen2 = thm "cont_Iwhen2";
 val cont_Iwhen3 = thm "cont_Iwhen3";
diff -r 2922be3544f8 -r 3032e90c4975 src/HOLCF/Up.ML
--- a/src/HOLCF/Up.ML	Wed Oct 12 01:43:37 2005 +0200
+++ b/src/HOLCF/Up.ML	Wed Oct 12 03:01:09 2005 +0200
@@ -2,6 +2,7 @@
 (* legacy ML bindings *)
 
 val antisym_less_up = thm "antisym_less_up";
+val compact_up = thm "compact_up";
 val cont_Ifup1 = thm "cont_Ifup1";
 val cont_Ifup2 = thm "cont_Ifup2";
 val cont_Iup = thm "cont_Iup";
diff -r 2922be3544f8 -r 3032e90c4975 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Wed Oct 12 01:43:37 2005 +0200
+++ b/src/HOLCF/Up.thy	Wed Oct 12 03:01:09 2005 +0200
@@ -122,7 +122,7 @@
 apply (erule (1) up_lemma4)
 done
 
-lemma up_chain_cases:
+lemma up_chain_lemma:
   "chain Y \<Longrightarrow>
    (\<exists>A. chain A \<and> lub (range Y) = Iup (lub (range A)) \<and>
    (\<exists>j. \<forall>i. Y (i + j) = Iup (A i))) \<or> (Y = (\<lambda>i. Ibottom))"
@@ -137,9 +137,9 @@
 done
 
 lemma cpo_up: "chain (Y::nat \<Rightarrow> 'a u) \<Longrightarrow> \<exists>x. range Y <<| x"
-apply (frule up_chain_cases, safe)
+apply (frule up_chain_lemma, safe)
 apply (rule_tac x="Iup (lub (range A))" in exI)
-apply (erule_tac j1="j" in is_lub_range_shift [THEN iffD1])
+apply (erule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
 apply (simp add: is_lub_Iup thelubE)
 apply (rule exI, rule lub_const)
 done
@@ -185,8 +185,8 @@
 
 lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
 apply (rule contI)
-apply (frule up_chain_cases, safe)
-apply (rule_tac j1="j" in is_lub_range_shift [THEN iffD1])
+apply (frule up_chain_lemma, safe)
+apply (rule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
 apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
 apply (simp add: cont_cfun_arg)
 apply (simp add: thelub_const lub_const)
@@ -202,7 +202,7 @@
   "fup \<equiv> \<Lambda> f p. Ifup f p"
 
 translations
-"case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(LAM x. t)\<cdot>l"
+  "case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(LAM x. t)\<cdot>l"
 
 text {* continuous versions of lemmas for @{typ "('a)u"} *}
 
@@ -218,7 +218,7 @@
 lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
 by simp
 
-lemma up_defined [simp]: " up\<cdot>x \<noteq> \<bottom>"
+lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>"
 by (simp add: up_def cont_Iup inst_up_pcpo)
 
 lemma not_up_less_UU [simp]: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
@@ -233,6 +233,26 @@
 apply (simp add: up_def cont_Iup)
 done
 
+lemma up_chain_cases:
+  "chain Y \<Longrightarrow>
+  (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i) \<and>
+  (\<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 [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 add: thelub_const)
+done
+
+text {* properties of fup *}
+
 lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
 by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo)