# 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\x = cfst\y \ csnd\x = csnd\y)" by (auto simp add: po_eq_conv less_cprod) -lemma compact_cpair [simp]: "\compact x; compact y\ \ compact " +lemma cfst_less_iff: "cfst\x \ y = x \ x>" +by (simp add: less_cprod) + +lemma csnd_less_iff: "csnd\x \ y = x \ x, y>" +by (simp add: less_cprod) + +lemma compact_cfst: "compact x \ compact (cfst\x)" +by (rule compactI, simp add: cfst_less_iff) + +lemma compact_csnd: "compact x \ compact (csnd\x)" +by (rule compactI, simp add: csnd_less_iff) + +lemma compact_cpair: "\compact x; compact y\ \ compact " by (rule compactI, simp add: less_cprod) +lemma compact_cpair_iff [simp]: "compact = (compact x \ compact y)" +apply (safe intro!: compact_cpair) +apply (drule compact_cfst, simp) +apply (drule compact_csnd, simp) +done + lemma lub_cprod2: "chain S \ range S <<| <\i. cfst\(S i), \i. csnd\(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 @@ (\j. \i. Y (i + j) = up\(A i))) \ Y = (\i. \)" by (simp add: inst_up_pcpo up_def cont_Iup up_chain_lemma) +lemma compact_up: "compact x \ compact (up\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\x) \ compact x" +unfolding compact_def +by (drule adm_subst [OF cont_Rep_CFun2 [where f=up]], simp) + +lemma compact_up_iff [simp]: "compact (up\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 "\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 \ compact (up\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="\i. Y i" in upE) +apply (simp, simp add: compact_chfin) done text {* properties of fup *}