src/HOLCF/Up.thy
changeset 25827 c2adeb1bae5c
parent 25789 c0506ac5b6b4
child 25879 98b93782c3b1
     1.1 --- a/src/HOLCF/Up.thy	Thu Jan 03 23:59:51 2008 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Fri Jan 04 00:01:02 2008 +0100
     1.3 @@ -68,6 +68,13 @@
     1.4      by (auto split: u.split_asm intro: trans_less)
     1.5  qed
     1.6  
     1.7 +lemma u_UNIV: "UNIV = insert Ibottom (range Iup)"
     1.8 +by (auto, case_tac x, auto)
     1.9 +
    1.10 +instance u :: (finite_po) finite_po
    1.11 +by (intro_classes, simp add: u_UNIV)
    1.12 +
    1.13 +
    1.14  subsection {* Lifted cpo is a cpo *}
    1.15  
    1.16  lemma is_lub_Iup:
    1.17 @@ -310,12 +317,27 @@
    1.18  lemma up_induct [induct type: u]: "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
    1.19  by (cases x, simp_all)
    1.20  
    1.21 +text {* lifting preserves chain-finiteness *}
    1.22 +
    1.23  lemma up_chain_cases:
    1.24    "chain Y \<Longrightarrow>
    1.25    (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i) \<and>
    1.26    (\<exists>j. \<forall>i. Y (i + j) = up\<cdot>(A i))) \<or> Y = (\<lambda>i. \<bottom>)"
    1.27  by (simp add: inst_up_pcpo up_def cont_Iup up_chain_lemma)
    1.28  
    1.29 +instance u :: (chfin) chfin
    1.30 +apply (intro_classes, clarify)
    1.31 +apply (drule up_chain_cases, safe)
    1.32 +apply (drule chfin [rule_format])
    1.33 +apply (erule exE, rename_tac n)
    1.34 +apply (rule_tac x="n + j" in exI)
    1.35 +apply (simp only: max_in_chain_def)
    1.36 +apply (clarify, rename_tac k)
    1.37 +apply (subgoal_tac "\<exists>m. k = m + j", clarsimp)
    1.38 +apply (rule_tac x="k - j" in exI, simp)
    1.39 +apply (simp add: max_in_chain_def)
    1.40 +done
    1.41 +
    1.42  lemma compact_up [simp]: "compact x \<Longrightarrow> compact (up\<cdot>x)"
    1.43  apply (unfold compact_def)
    1.44  apply (rule admI)