src/HOLCF/Up.thy
changeset 25879 98b93782c3b1
parent 25827 c2adeb1bae5c
child 25898 d8f17d8cf9d4
     1.1 --- a/src/HOLCF/Up.thy	Thu Jan 10 05:11:09 2008 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Thu Jan 10 05:15:43 2008 +0100
     1.3 @@ -325,29 +325,27 @@
     1.4    (\<exists>j. \<forall>i. Y (i + j) = up\<cdot>(A i))) \<or> Y = (\<lambda>i. \<bottom>)"
     1.5  by (simp add: inst_up_pcpo up_def cont_Iup up_chain_lemma)
     1.6  
     1.7 +lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
     1.8 +apply (rule compactI2)
     1.9 +apply (drule up_chain_cases, safe)
    1.10 +apply (drule (1) compactD2, simp)
    1.11 +apply (erule exE, rule_tac x="i + j" in exI)
    1.12 +apply simp
    1.13 +apply simp
    1.14 +done
    1.15 +
    1.16 +lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x"
    1.17 +unfolding compact_def
    1.18 +by (drule adm_subst [OF cont_Rep_CFun2 [where f=up]], simp)
    1.19 +
    1.20 +lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x"
    1.21 +by (safe elim!: compact_up compact_upD)
    1.22 +
    1.23  instance u :: (chfin) chfin
    1.24  apply (intro_classes, clarify)
    1.25 -apply (drule up_chain_cases, safe)
    1.26 -apply (drule chfin [rule_format])
    1.27 -apply (erule exE, rename_tac n)
    1.28 -apply (rule_tac x="n + j" in exI)
    1.29 -apply (simp only: max_in_chain_def)
    1.30 -apply (clarify, rename_tac k)
    1.31 -apply (subgoal_tac "\<exists>m. k = m + j", clarsimp)
    1.32 -apply (rule_tac x="k - j" in exI, simp)
    1.33 -apply (simp add: max_in_chain_def)
    1.34 -done
    1.35 -
    1.36 -lemma compact_up [simp]: "compact x \<Longrightarrow> compact (up\<cdot>x)"
    1.37 -apply (unfold compact_def)
    1.38 -apply (rule admI)
    1.39 -apply (drule up_chain_cases)
    1.40 -apply (elim disjE exE conjE)
    1.41 -apply simp
    1.42 -apply (erule (1) admD)
    1.43 -apply (rule allI, drule_tac x="i + j" in spec)
    1.44 -apply simp
    1.45 -apply simp
    1.46 +apply (erule compact_imp_max_in_chain)
    1.47 +apply (rule_tac p="\<Squnion>i. Y i" in upE)
    1.48 +apply (simp, simp add: compact_chfin)
    1.49  done
    1.50  
    1.51  text {* properties of fup *}