src/HOLCF/Up.thy
changeset 17838 3032e90c4975
parent 17585 f12d7ac88eb4
child 18078 20e5a6440790
     1.1 --- a/src/HOLCF/Up.thy	Wed Oct 12 01:43:37 2005 +0200
     1.2 +++ b/src/HOLCF/Up.thy	Wed Oct 12 03:01:09 2005 +0200
     1.3 @@ -122,7 +122,7 @@
     1.4  apply (erule (1) up_lemma4)
     1.5  done
     1.6  
     1.7 -lemma up_chain_cases:
     1.8 +lemma up_chain_lemma:
     1.9    "chain Y \<Longrightarrow>
    1.10     (\<exists>A. chain A \<and> lub (range Y) = Iup (lub (range A)) \<and>
    1.11     (\<exists>j. \<forall>i. Y (i + j) = Iup (A i))) \<or> (Y = (\<lambda>i. Ibottom))"
    1.12 @@ -137,9 +137,9 @@
    1.13  done
    1.14  
    1.15  lemma cpo_up: "chain (Y::nat \<Rightarrow> 'a u) \<Longrightarrow> \<exists>x. range Y <<| x"
    1.16 -apply (frule up_chain_cases, safe)
    1.17 +apply (frule up_chain_lemma, safe)
    1.18  apply (rule_tac x="Iup (lub (range A))" in exI)
    1.19 -apply (erule_tac j1="j" in is_lub_range_shift [THEN iffD1])
    1.20 +apply (erule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
    1.21  apply (simp add: is_lub_Iup thelubE)
    1.22  apply (rule exI, rule lub_const)
    1.23  done
    1.24 @@ -185,8 +185,8 @@
    1.25  
    1.26  lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
    1.27  apply (rule contI)
    1.28 -apply (frule up_chain_cases, safe)
    1.29 -apply (rule_tac j1="j" in is_lub_range_shift [THEN iffD1])
    1.30 +apply (frule up_chain_lemma, safe)
    1.31 +apply (rule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
    1.32  apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
    1.33  apply (simp add: cont_cfun_arg)
    1.34  apply (simp add: thelub_const lub_const)
    1.35 @@ -202,7 +202,7 @@
    1.36    "fup \<equiv> \<Lambda> f p. Ifup f p"
    1.37  
    1.38  translations
    1.39 -"case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(LAM x. t)\<cdot>l"
    1.40 +  "case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(LAM x. t)\<cdot>l"
    1.41  
    1.42  text {* continuous versions of lemmas for @{typ "('a)u"} *}
    1.43  
    1.44 @@ -218,7 +218,7 @@
    1.45  lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
    1.46  by simp
    1.47  
    1.48 -lemma up_defined [simp]: " up\<cdot>x \<noteq> \<bottom>"
    1.49 +lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>"
    1.50  by (simp add: up_def cont_Iup inst_up_pcpo)
    1.51  
    1.52  lemma not_up_less_UU [simp]: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
    1.53 @@ -233,6 +233,26 @@
    1.54  apply (simp add: up_def cont_Iup)
    1.55  done
    1.56  
    1.57 +lemma up_chain_cases:
    1.58 +  "chain Y \<Longrightarrow>
    1.59 +  (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i) \<and>
    1.60 +  (\<exists>j. \<forall>i. Y (i + j) = up\<cdot>(A i))) \<or> Y = (\<lambda>i. \<bottom>)"
    1.61 +by (simp add: inst_up_pcpo up_def cont_Iup up_chain_lemma)
    1.62 +
    1.63 +lemma compact_up [simp]: "compact x \<Longrightarrow> compact (up\<cdot>x)"
    1.64 +apply (unfold compact_def)
    1.65 +apply (rule admI)
    1.66 +apply (drule up_chain_cases)
    1.67 +apply (elim disjE exE conjE)
    1.68 +apply simp
    1.69 +apply (erule (1) admD)
    1.70 +apply (rule allI, drule_tac x="i + j" in spec)
    1.71 +apply simp
    1.72 +apply (simp add: thelub_const)
    1.73 +done
    1.74 +
    1.75 +text {* properties of fup *}
    1.76 +
    1.77  lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
    1.78  by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo)
    1.79