new compactness lemmas
authorhuffman
Thu Jan 10 05:15:43 2008 +0100 (2008-01-10)
changeset 2587998b93782c3b1
parent 25878 bfd53f791c10
child 25880 2c6cabe7a47c
new compactness lemmas
src/HOLCF/Cprod.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Cprod.thy	Thu Jan 10 05:11:09 2008 +0100
     1.2 +++ b/src/HOLCF/Cprod.thy	Thu Jan 10 05:15:43 2008 +0100
     1.3 @@ -342,9 +342,27 @@
     1.4  lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
     1.5  by (auto simp add: po_eq_conv less_cprod)
     1.6  
     1.7 -lemma compact_cpair [simp]: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
     1.8 +lemma cfst_less_iff: "cfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <y, csnd\<cdot>x>"
     1.9 +by (simp add: less_cprod)
    1.10 +
    1.11 +lemma csnd_less_iff: "csnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <cfst\<cdot>x, y>"
    1.12 +by (simp add: less_cprod)
    1.13 +
    1.14 +lemma compact_cfst: "compact x \<Longrightarrow> compact (cfst\<cdot>x)"
    1.15 +by (rule compactI, simp add: cfst_less_iff)
    1.16 +
    1.17 +lemma compact_csnd: "compact x \<Longrightarrow> compact (csnd\<cdot>x)"
    1.18 +by (rule compactI, simp add: csnd_less_iff)
    1.19 +
    1.20 +lemma compact_cpair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
    1.21  by (rule compactI, simp add: less_cprod)
    1.22  
    1.23 +lemma compact_cpair_iff [simp]: "compact <x, y> = (compact x \<and> compact y)"
    1.24 +apply (safe intro!: compact_cpair)
    1.25 +apply (drule compact_cfst, simp)
    1.26 +apply (drule compact_csnd, simp)
    1.27 +done
    1.28 +
    1.29  lemma lub_cprod2: 
    1.30    "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
    1.31  apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)
     2.1 --- a/src/HOLCF/Up.thy	Thu Jan 10 05:11:09 2008 +0100
     2.2 +++ b/src/HOLCF/Up.thy	Thu Jan 10 05:15:43 2008 +0100
     2.3 @@ -325,29 +325,27 @@
     2.4    (\<exists>j. \<forall>i. Y (i + j) = up\<cdot>(A i))) \<or> Y = (\<lambda>i. \<bottom>)"
     2.5  by (simp add: inst_up_pcpo up_def cont_Iup up_chain_lemma)
     2.6  
     2.7 +lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
     2.8 +apply (rule compactI2)
     2.9 +apply (drule up_chain_cases, safe)
    2.10 +apply (drule (1) compactD2, simp)
    2.11 +apply (erule exE, rule_tac x="i + j" in exI)
    2.12 +apply simp
    2.13 +apply simp
    2.14 +done
    2.15 +
    2.16 +lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x"
    2.17 +unfolding compact_def
    2.18 +by (drule adm_subst [OF cont_Rep_CFun2 [where f=up]], simp)
    2.19 +
    2.20 +lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x"
    2.21 +by (safe elim!: compact_up compact_upD)
    2.22 +
    2.23  instance u :: (chfin) chfin
    2.24  apply (intro_classes, clarify)
    2.25 -apply (drule up_chain_cases, safe)
    2.26 -apply (drule chfin [rule_format])
    2.27 -apply (erule exE, rename_tac n)
    2.28 -apply (rule_tac x="n + j" in exI)
    2.29 -apply (simp only: max_in_chain_def)
    2.30 -apply (clarify, rename_tac k)
    2.31 -apply (subgoal_tac "\<exists>m. k = m + j", clarsimp)
    2.32 -apply (rule_tac x="k - j" in exI, simp)
    2.33 -apply (simp add: max_in_chain_def)
    2.34 -done
    2.35 -
    2.36 -lemma compact_up [simp]: "compact x \<Longrightarrow> compact (up\<cdot>x)"
    2.37 -apply (unfold compact_def)
    2.38 -apply (rule admI)
    2.39 -apply (drule up_chain_cases)
    2.40 -apply (elim disjE exE conjE)
    2.41 -apply simp
    2.42 -apply (erule (1) admD)
    2.43 -apply (rule allI, drule_tac x="i + j" in spec)
    2.44 -apply simp
    2.45 -apply simp
    2.46 +apply (erule compact_imp_max_in_chain)
    2.47 +apply (rule_tac p="\<Squnion>i. Y i" in upE)
    2.48 +apply (simp, simp add: compact_chfin)
    2.49  done
    2.50  
    2.51  text {* properties of fup *}