src/HOL/HOLCF/Library/Option_Cpo.thy
changeset 41325 b27e5c9f5c10
parent 41292 2b7bc8d9fd6e
child 41393 17bf4ddd0833
equal deleted 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