src/HOL/HOLCF/Library/Option_Cpo.thy
 changeset 41325 b27e5c9f5c10 parent 41292 2b7bc8d9fd6e child 41393 17bf4ddd0833
equal inserted replaced
41324:1383653efec3 41325:b27e5c9f5c10
`   147   assumes "cont (\<lambda>x. f x)"`
`   147   assumes "cont (\<lambda>x. f x)"`
`   148   assumes "\<And>a. cont (\<lambda>x. g x a)"`
`   148   assumes "\<And>a. cont (\<lambda>x. g x a)"`
`   149   shows "cont (\<lambda>x. case z of None \<Rightarrow> f x | Some a \<Rightarrow> g x a)"`
`   149   shows "cont (\<lambda>x. case z of None \<Rightarrow> f x | Some a \<Rightarrow> g x a)"`
`   150 using assms by (cases z) auto`
`   150 using assms by (cases z) auto`
`   151 `
`   151 `
`       `
`   152 text {* Continuity rule for map. *}`
`       `
`   153 `
`       `
`   154 lemma cont2cont_option_map [simp, cont2cont]:`
`       `
`   155   assumes f: "cont (\<lambda>(x, y). f x y)"`
`       `
`   156   assumes g: "cont (\<lambda>x. g x)"`
`       `
`   157   shows "cont (\<lambda>x. Option.map (\<lambda>y. f x y) (g x))"`
`       `
`   158 using assms by (simp add: prod_cont_iff Option.map_def)`
`       `
`   159 `
`   152 subsection {* Compactness and chain-finiteness *}`
`   160 subsection {* Compactness and chain-finiteness *}`
`   153 `
`   161 `
`   154 lemma compact_None [simp]: "compact None"`
`   162 lemma compact_None [simp]: "compact None"`
`   155 apply (rule compactI2)`
`   163 apply (rule compactI2)`
`   156 apply (erule option_chain_cases, safe)`
`   164 apply (erule option_chain_cases, safe)`
`   180 done`
`   188 done`
`   181 `
`   189 `
`   182 instance option :: (discrete_cpo) discrete_cpo`
`   190 instance option :: (discrete_cpo) discrete_cpo`
`   183 by intro_classes (simp add: below_option_def split: option.split)`
`   191 by intro_classes (simp add: below_option_def split: option.split)`
`   184 `
`   192 `
`   185 subsection {* Using option types with fixrec *}`
`   193 subsection {* Using option types with Fixrec *}`
`   186 `
`   194 `
`   187 definition`
`   195 definition`
`   188   "match_None = (\<Lambda> x k. case x of None \<Rightarrow> k | Some a \<Rightarrow> Fixrec.fail)"`
`   196   "match_None = (\<Lambda> x k. case x of None \<Rightarrow> k | Some a \<Rightarrow> Fixrec.fail)"`
`   189 `
`   197 `
`   190 definition`
`   198 definition`
`   245     by (simp add: cast_liftdefl cfcomp1 u_map_map ID_def [symmetric] u_map_ID)`
`   253     by (simp add: cast_liftdefl cfcomp1 u_map_map ID_def [symmetric] u_map_ID)`
`   246 qed`
`   254 qed`
`   247 `
`   255 `
`   248 end`
`   256 end`
`   249 `
`   257 `
`       `
`   258 subsection {* Configuring domain package to work with option type *}`
`       `
`   259 `
`       `
`   260 lemma liftdefl_option [domain_defl_simps]:`
`       `
`   261   "LIFTDEFL('a::predomain option) = LIFTDEFL(unit + 'a)"`
`       `
`   262 by (rule liftdefl_option_def)`
`       `
`   263 `
`       `
`   264 abbreviation option_map`
`       `
`   265   where "option_map f \<equiv> Abs_cfun (Option.map (Rep_cfun f))"`
`       `
`   266 `
`       `
`   267 lemma option_map_ID [domain_map_ID]: "option_map ID = ID"`
`       `
`   268 by (simp add: ID_def cfun_eq_iff Option.map.identity)`
`       `
`   269 `
`       `
`   270 lemma deflation_option_map [domain_deflation]:`
`       `
`   271   "deflation d \<Longrightarrow> deflation (option_map d)"`
`       `
`   272 apply default`
`       `
`   273 apply (induct_tac x, simp_all add: deflation.idem)`
`       `
`   274 apply (induct_tac x, simp_all add: deflation.below)`
`       `
`   275 done`
`       `
`   276 `
`       `
`   277 lemma encode_option_option_map:`
`       `
`   278   "encode_option\<cdot>(Option.map (\<lambda>x. f\<cdot>x) (decode_option\<cdot>x)) = sum_map' ID f\<cdot>x"`
`       `
`   279 by (induct x, simp_all add: decode_option_def encode_option_def)`
`       `
`   280 `
`       `
`   281 lemma isodefl_option [domain_isodefl]:`
`       `
`   282   assumes "isodefl' d t"`
`       `
`   283   shows "isodefl' (option_map d) (sum_liftdefl\<cdot>(pdefl\<cdot>DEFL(unit))\<cdot>t)"`
`       `
`   284 using isodefl_sum [OF isodefl_LIFTDEFL [where 'a=unit] assms]`
`       `
`   285 unfolding isodefl'_def liftemb_option_def liftprj_option_def liftdefl_eq`
`       `
`   286 by (simp add: cfcomp1 u_map_map encode_option_option_map)`
`       `
`   287 `
`       `
`   288 setup {*`
`       `
`   289   Domain_Take_Proofs.add_rec_type (@{type_name "option"}, [true])`
`       `
`   290 *}`
`       `
`   291 `
`   250 end`
`   292 end`