# HG changeset patch
# User huffman
# Date 1292871421 28800
# Node ID b27e5c9f5c10ba732a68271d87f8576eb0cfe258
# Parent  1383653efec33cc11dd2094425601ca5148ef647
configure domain package to work with HOL option type

diff -r 1383653efec3 -r b27e5c9f5c10 src/HOL/HOLCF/Library/Option_Cpo.thy
--- a/src/HOL/HOLCF/Library/Option_Cpo.thy	Mon Dec 20 10:48:01 2010 -0800
+++ b/src/HOL/HOLCF/Library/Option_Cpo.thy	Mon Dec 20 10:57:01 2010 -0800
@@ -149,6 +149,14 @@
   shows "cont (\<lambda>x. case z of None \<Rightarrow> f x | Some a \<Rightarrow> g x a)"
 using assms by (cases z) auto
 
+text {* Continuity rule for map. *}
+
+lemma cont2cont_option_map [simp, cont2cont]:
+  assumes f: "cont (\<lambda>(x, y). f x y)"
+  assumes g: "cont (\<lambda>x. g x)"
+  shows "cont (\<lambda>x. Option.map (\<lambda>y. f x y) (g x))"
+using assms by (simp add: prod_cont_iff Option.map_def)
+
 subsection {* Compactness and chain-finiteness *}
 
 lemma compact_None [simp]: "compact None"
@@ -182,7 +190,7 @@
 instance option :: (discrete_cpo) discrete_cpo
 by intro_classes (simp add: below_option_def split: option.split)
 
-subsection {* Using option types with fixrec *}
+subsection {* Using option types with Fixrec *}
 
 definition
   "match_None = (\<Lambda> x k. case x of None \<Rightarrow> k | Some a \<Rightarrow> Fixrec.fail)"
@@ -247,4 +255,38 @@
 
 end
 
+subsection {* Configuring domain package to work with option type *}
+
+lemma liftdefl_option [domain_defl_simps]:
+  "LIFTDEFL('a::predomain option) = LIFTDEFL(unit + 'a)"
+by (rule liftdefl_option_def)
+
+abbreviation option_map
+  where "option_map f \<equiv> Abs_cfun (Option.map (Rep_cfun f))"
+
+lemma option_map_ID [domain_map_ID]: "option_map ID = ID"
+by (simp add: ID_def cfun_eq_iff Option.map.identity)
+
+lemma deflation_option_map [domain_deflation]:
+  "deflation d \<Longrightarrow> deflation (option_map d)"
+apply default
+apply (induct_tac x, simp_all add: deflation.idem)
+apply (induct_tac x, simp_all add: deflation.below)
+done
+
+lemma encode_option_option_map:
+  "encode_option\<cdot>(Option.map (\<lambda>x. f\<cdot>x) (decode_option\<cdot>x)) = sum_map' ID f\<cdot>x"
+by (induct x, simp_all add: decode_option_def encode_option_def)
+
+lemma isodefl_option [domain_isodefl]:
+  assumes "isodefl' d t"
+  shows "isodefl' (option_map d) (sum_liftdefl\<cdot>(pdefl\<cdot>DEFL(unit))\<cdot>t)"
+using isodefl_sum [OF isodefl_LIFTDEFL [where 'a=unit] assms]
+unfolding isodefl'_def liftemb_option_def liftprj_option_def liftdefl_eq
+by (simp add: cfcomp1 u_map_map encode_option_option_map)
+
+setup {*
+  Domain_Take_Proofs.add_rec_type (@{type_name "option"}, [true])
+*}
+
 end