1(* Title: HOL/HOLCF/Up.thy 2 Author: Franz Regensburger 3 Author: Brian Huffman 4*) 5 6section \<open>The type of lifted values\<close> 7 8theory Up 9 imports Cfun 10begin 11 12default_sort cpo 13 14 15subsection \<open>Definition of new type for lifting\<close> 16 17datatype 'a u ("(_\<^sub>\<bottom>)" [1000] 999) = Ibottom | Iup 'a 18 19primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" 20 where 21 "Ifup f Ibottom = \<bottom>" 22 | "Ifup f (Iup x) = f\<cdot>x" 23 24 25subsection \<open>Ordering on lifted cpo\<close> 26 27instantiation u :: (cpo) below 28begin 29 30definition below_up_def: 31 "(\<sqsubseteq>) \<equiv> 32 (\<lambda>x y. 33 (case x of 34 Ibottom \<Rightarrow> True 35 | Iup a \<Rightarrow> (case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b)))" 36 37instance .. 38 39end 40 41lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z" 42 by (simp add: below_up_def) 43 44lemma not_Iup_below [iff]: "Iup x \<notsqsubseteq> Ibottom" 45 by (simp add: below_up_def) 46 47lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)" 48 by (simp add: below_up_def) 49 50 51subsection \<open>Lifted cpo is a partial order\<close> 52 53instance u :: (cpo) po 54proof 55 fix x :: "'a u" 56 show "x \<sqsubseteq> x" 57 by (simp add: below_up_def split: u.split) 58next 59 fix x y :: "'a u" 60 assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" 61 then show "x = y" 62 by (auto simp: below_up_def split: u.split_asm intro: below_antisym) 63next 64 fix x y z :: "'a u" 65 assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" 66 then show "x \<sqsubseteq> z" 67 by (auto simp: below_up_def split: u.split_asm intro: below_trans) 68qed 69 70 71subsection \<open>Lifted cpo is a cpo\<close> 72 73lemma is_lub_Iup: "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x" 74 by (auto simp: is_lub_def is_ub_def ball_simps below_up_def split: u.split) 75 76lemma up_chain_lemma: 77 assumes Y: "chain Y" 78 obtains "\<forall>i. Y i = Ibottom" 79 | A k where "\<forall>i. Iup (A i) = Y (i + k)" and "chain A" and "range Y <<| Iup (\<Squnion>i. A i)" 80proof (cases "\<exists>k. Y k \<noteq> Ibottom") 81 case True 82 then obtain k where k: "Y k \<noteq> Ibottom" .. 83 define A where "A i = (THE a. Iup a = Y (i + k))" for i 84 have Iup_A: "\<forall>i. Iup (A i) = Y (i + k)" 85 proof 86 fix i :: nat 87 from Y le_add2 have "Y k \<sqsubseteq> Y (i + k)" by (rule chain_mono) 88 with k have "Y (i + k) \<noteq> Ibottom" by (cases "Y k") auto 89 then show "Iup (A i) = Y (i + k)" 90 by (cases "Y (i + k)", simp_all add: A_def) 91 qed 92 from Y have chain_A: "chain A" 93 by (simp add: chain_def Iup_below [symmetric] Iup_A) 94 then have "range A <<| (\<Squnion>i. A i)" 95 by (rule cpo_lubI) 96 then have "range (\<lambda>i. Iup (A i)) <<| Iup (\<Squnion>i. A i)" 97 by (rule is_lub_Iup) 98 then have "range (\<lambda>i. Y (i + k)) <<| Iup (\<Squnion>i. A i)" 99 by (simp only: Iup_A) 100 then have "range (\<lambda>i. Y i) <<| Iup (\<Squnion>i. A i)" 101 by (simp only: is_lub_range_shift [OF Y]) 102 with Iup_A chain_A show ?thesis .. 103next 104 case False 105 then have "\<forall>i. Y i = Ibottom" by simp 106 then show ?thesis .. 107qed 108 109instance u :: (cpo) cpo 110proof 111 fix S :: "nat \<Rightarrow> 'a u" 112 assume S: "chain S" 113 then show "\<exists>x. range (\<lambda>i. S i) <<| x" 114 proof (rule up_chain_lemma) 115 assume "\<forall>i. S i = Ibottom" 116 then have "range (\<lambda>i. S i) <<| Ibottom" 117 by (simp add: is_lub_const) 118 then show ?thesis .. 119 next 120 fix A :: "nat \<Rightarrow> 'a" 121 assume "range S <<| Iup (\<Squnion>i. A i)" 122 then show ?thesis .. 123 qed 124qed 125 126 127subsection \<open>Lifted cpo is pointed\<close> 128 129instance u :: (cpo) pcpo 130 by intro_classes fast 131 132text \<open>for compatibility with old HOLCF-Version\<close> 133lemma inst_up_pcpo: "\<bottom> = Ibottom" 134 by (rule minimal_up [THEN bottomI, symmetric]) 135 136 137subsection \<open>Continuity of \emph{Iup} and \emph{Ifup}\<close> 138 139text \<open>continuity for \<^term>\<open>Iup\<close>\<close> 140 141lemma cont_Iup: "cont Iup" 142 apply (rule contI) 143 apply (rule is_lub_Iup) 144 apply (erule cpo_lubI) 145 done 146 147text \<open>continuity for \<^term>\<open>Ifup\<close>\<close> 148 149lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)" 150 by (induct x) simp_all 151 152lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)" 153 apply (rule monofunI) 154 apply (case_tac x, simp) 155 apply (case_tac y, simp) 156 apply (simp add: monofun_cfun_arg) 157 done 158 159lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)" 160proof (rule contI2) 161 fix Y 162 assume Y: "chain Y" and Y': "chain (\<lambda>i. Ifup f (Y i))" 163 from Y show "Ifup f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. Ifup f (Y i))" 164 proof (rule up_chain_lemma) 165 fix A and k 166 assume A: "\<forall>i. Iup (A i) = Y (i + k)" 167 assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)" 168 then have "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))" 169 by (simp add: lub_eqI contlub_cfun_arg) 170 also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))" 171 by (simp add: A) 172 also have "\<dots> = (\<Squnion>i. Ifup f (Y i))" 173 using Y' by (rule lub_range_shift) 174 finally show ?thesis by simp 175 qed simp 176qed (rule monofun_Ifup2) 177 178 179subsection \<open>Continuous versions of constants\<close> 180 181definition up :: "'a \<rightarrow> 'a u" 182 where "up = (\<Lambda> x. Iup x)" 183 184definition fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" 185 where "fup = (\<Lambda> f p. Ifup f p)" 186 187translations 188 "case l of XCONST up\<cdot>x \<Rightarrow> t" \<rightleftharpoons> "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l" 189 "case l of (XCONST up :: 'a)\<cdot>x \<Rightarrow> t" \<rightharpoonup> "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l" 190 "\<Lambda>(XCONST up\<cdot>x). t" \<rightleftharpoons> "CONST fup\<cdot>(\<Lambda> x. t)" 191 192text \<open>continuous versions of lemmas for \<^typ>\<open>('a)u\<close>\<close> 193 194lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)" 195 by (induct z) (simp add: inst_up_pcpo, simp add: up_def cont_Iup) 196 197lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)" 198 by (simp add: up_def cont_Iup) 199 200lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y" 201 by simp 202 203lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>" 204 by (simp add: up_def cont_Iup inst_up_pcpo) 205 206lemma not_up_less_UU: "up\<cdot>x \<notsqsubseteq> \<bottom>" 207 by simp (* FIXME: remove? *) 208 209lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y" 210 by (simp add: up_def cont_Iup) 211 212lemma upE [case_names bottom up, cases type: u]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 213 by (cases p) (simp add: inst_up_pcpo, simp add: up_def cont_Iup) 214 215lemma up_induct [case_names bottom up, induct type: u]: "P \<bottom> \<Longrightarrow> (\<And>x. P (up\<cdot>x)) \<Longrightarrow> P x" 216 by (cases x) simp_all 217 218text \<open>lifting preserves chain-finiteness\<close> 219 220lemma up_chain_cases: 221 assumes Y: "chain Y" 222 obtains "\<forall>i. Y i = \<bottom>" 223 | A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)" 224 by (rule up_chain_lemma [OF Y]) (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI) 225 226lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)" 227 apply (rule compactI2) 228 apply (erule up_chain_cases) 229 apply simp 230 apply (drule (1) compactD2, simp) 231 apply (erule exE) 232 apply (drule_tac f="up" and x="x" in monofun_cfun_arg) 233 apply (simp, erule exI) 234 done 235 236lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x" 237 unfolding compact_def 238 by (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp) 239 240lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x" 241 by (safe elim!: compact_up compact_upD) 242 243instance u :: (chfin) chfin 244 apply intro_classes 245 apply (erule compact_imp_max_in_chain) 246 apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all) 247 done 248 249text \<open>properties of fup\<close> 250 251lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>" 252 by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM) 253 254lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x" 255 by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM) 256 257lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x" 258 by (cases x) simp_all 259 260end 261