src/HOL/HOLCF/Library/Sum_Cpo.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 55931 62156e694f3d
child 61169 4de9ff3ea29a
permissions -rw-r--r--
modernized header;
     1 (*  Title:      HOL/HOLCF/Library/Sum_Cpo.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 section {* The cpo of disjoint sums *}
     6 
     7 theory Sum_Cpo
     8 imports HOLCF
     9 begin
    10 
    11 subsection {* Ordering on sum type *}
    12 
    13 instantiation sum :: (below, below) below
    14 begin
    15 
    16 definition below_sum_def:
    17   "x \<sqsubseteq> y \<equiv> case x of
    18          Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b | Inr b \<Rightarrow> False) |
    19          Inr a \<Rightarrow> (case y of Inl b \<Rightarrow> False | Inr b \<Rightarrow> a \<sqsubseteq> b)"
    20 
    21 instance ..
    22 end
    23 
    24 lemma Inl_below_Inl [simp]: "Inl x \<sqsubseteq> Inl y \<longleftrightarrow> x \<sqsubseteq> y"
    25 unfolding below_sum_def by simp
    26 
    27 lemma Inr_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y \<longleftrightarrow> x \<sqsubseteq> y"
    28 unfolding below_sum_def by simp
    29 
    30 lemma Inl_below_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
    31 unfolding below_sum_def by simp
    32 
    33 lemma Inr_below_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
    34 unfolding below_sum_def by simp
    35 
    36 lemma Inl_mono: "x \<sqsubseteq> y \<Longrightarrow> Inl x \<sqsubseteq> Inl y"
    37 by simp
    38 
    39 lemma Inr_mono: "x \<sqsubseteq> y \<Longrightarrow> Inr x \<sqsubseteq> Inr y"
    40 by simp
    41 
    42 lemma Inl_belowE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
    43 by (cases x, simp_all)
    44 
    45 lemma Inr_belowE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
    46 by (cases x, simp_all)
    47 
    48 lemmas sum_below_elims = Inl_belowE Inr_belowE
    49 
    50 lemma sum_below_cases:
    51   "\<lbrakk>x \<sqsubseteq> y;
    52     \<And>a b. \<lbrakk>x = Inl a; y = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R;
    53     \<And>a b. \<lbrakk>x = Inr a; y = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk>
    54       \<Longrightarrow> R"
    55 by (cases x, safe elim!: sum_below_elims, auto)
    56 
    57 subsection {* Sum type is a complete partial order *}
    58 
    59 instance sum :: (po, po) po
    60 proof
    61   fix x :: "'a + 'b"
    62   show "x \<sqsubseteq> x"
    63     by (induct x, simp_all)
    64 next
    65   fix x y :: "'a + 'b"
    66   assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
    67     by (induct x, auto elim!: sum_below_elims intro: below_antisym)
    68 next
    69   fix x y z :: "'a + 'b"
    70   assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
    71     by (induct x, auto elim!: sum_below_elims intro: below_trans)
    72 qed
    73 
    74 lemma monofun_inv_Inl: "monofun (\<lambda>p. THE a. p = Inl a)"
    75 by (rule monofunI, erule sum_below_cases, simp_all)
    76 
    77 lemma monofun_inv_Inr: "monofun (\<lambda>p. THE b. p = Inr b)"
    78 by (rule monofunI, erule sum_below_cases, simp_all)
    79 
    80 lemma sum_chain_cases:
    81   assumes Y: "chain Y"
    82   assumes A: "\<And>A. \<lbrakk>chain A; Y = (\<lambda>i. Inl (A i))\<rbrakk> \<Longrightarrow> R"
    83   assumes B: "\<And>B. \<lbrakk>chain B; Y = (\<lambda>i. Inr (B i))\<rbrakk> \<Longrightarrow> R"
    84   shows "R"
    85  apply (cases "Y 0")
    86   apply (rule A)
    87    apply (rule ch2ch_monofun [OF monofun_inv_Inl Y])
    88   apply (rule ext)
    89   apply (cut_tac j=i in chain_mono [OF Y le0], simp)
    90   apply (erule Inl_belowE, simp)
    91  apply (rule B)
    92   apply (rule ch2ch_monofun [OF monofun_inv_Inr Y])
    93  apply (rule ext)
    94  apply (cut_tac j=i in chain_mono [OF Y le0], simp)
    95  apply (erule Inr_belowE, simp)
    96 done
    97 
    98 lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x"
    99  apply (rule is_lubI)
   100   apply (rule ub_rangeI)
   101   apply (simp add: is_lub_rangeD1)
   102  apply (frule ub_rangeD [where i=arbitrary])
   103  apply (erule Inl_belowE, simp)
   104  apply (erule is_lubD2)
   105  apply (rule ub_rangeI)
   106  apply (drule ub_rangeD, simp)
   107 done
   108 
   109 lemma is_lub_Inr: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inr (S i)) <<| Inr x"
   110  apply (rule is_lubI)
   111   apply (rule ub_rangeI)
   112   apply (simp add: is_lub_rangeD1)
   113  apply (frule ub_rangeD [where i=arbitrary])
   114  apply (erule Inr_belowE, simp)
   115  apply (erule is_lubD2)
   116  apply (rule ub_rangeI)
   117  apply (drule ub_rangeD, simp)
   118 done
   119 
   120 instance sum :: (cpo, cpo) cpo
   121  apply intro_classes
   122  apply (erule sum_chain_cases, safe)
   123   apply (rule exI)
   124   apply (rule is_lub_Inl)
   125   apply (erule cpo_lubI)
   126  apply (rule exI)
   127  apply (rule is_lub_Inr)
   128  apply (erule cpo_lubI)
   129 done
   130 
   131 subsection {* Continuity of \emph{Inl}, \emph{Inr}, and case function *}
   132 
   133 lemma cont_Inl: "cont Inl"
   134 by (intro contI is_lub_Inl cpo_lubI)
   135 
   136 lemma cont_Inr: "cont Inr"
   137 by (intro contI is_lub_Inr cpo_lubI)
   138 
   139 lemmas cont2cont_Inl [simp, cont2cont] = cont_compose [OF cont_Inl]
   140 lemmas cont2cont_Inr [simp, cont2cont] = cont_compose [OF cont_Inr]
   141 
   142 lemmas ch2ch_Inl [simp] = ch2ch_cont [OF cont_Inl]
   143 lemmas ch2ch_Inr [simp] = ch2ch_cont [OF cont_Inr]
   144 
   145 lemmas lub_Inl = cont2contlubE [OF cont_Inl, symmetric]
   146 lemmas lub_Inr = cont2contlubE [OF cont_Inr, symmetric]
   147 
   148 lemma cont_case_sum1:
   149   assumes f: "\<And>a. cont (\<lambda>x. f x a)"
   150   assumes g: "\<And>b. cont (\<lambda>x. g x b)"
   151   shows "cont (\<lambda>x. case y of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
   152 by (induct y, simp add: f, simp add: g)
   153 
   154 lemma cont_case_sum2: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (case_sum f g)"
   155 apply (rule contI)
   156 apply (erule sum_chain_cases)
   157 apply (simp add: cont2contlubE [OF cont_Inl, symmetric] contE)
   158 apply (simp add: cont2contlubE [OF cont_Inr, symmetric] contE)
   159 done
   160 
   161 lemma cont2cont_case_sum:
   162   assumes f1: "\<And>a. cont (\<lambda>x. f x a)" and f2: "\<And>x. cont (\<lambda>a. f x a)"
   163   assumes g1: "\<And>b. cont (\<lambda>x. g x b)" and g2: "\<And>x. cont (\<lambda>b. g x b)"
   164   assumes h: "cont (\<lambda>x. h x)"
   165   shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
   166 apply (rule cont_apply [OF h])
   167 apply (rule cont_case_sum2 [OF f2 g2])
   168 apply (rule cont_case_sum1 [OF f1 g1])
   169 done
   170 
   171 lemma cont2cont_case_sum' [simp, cont2cont]:
   172   assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
   173   assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
   174   assumes h: "cont (\<lambda>x. h x)"
   175   shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
   176 using assms by (simp add: cont2cont_case_sum prod_cont_iff)
   177 
   178 text {* Continuity of map function. *}
   179 
   180 lemma map_sum_eq: "map_sum f g = case_sum (\<lambda>a. Inl (f a)) (\<lambda>b. Inr (g b))"
   181 by (rule ext, case_tac x, simp_all)
   182 
   183 lemma cont2cont_map_sum [simp, cont2cont]:
   184   assumes f: "cont (\<lambda>(x, y). f x y)"
   185   assumes g: "cont (\<lambda>(x, y). g x y)"
   186   assumes h: "cont (\<lambda>x. h x)"
   187   shows "cont (\<lambda>x. map_sum (\<lambda>y. f x y) (\<lambda>y. g x y) (h x))"
   188 using assms by (simp add: map_sum_eq prod_cont_iff)
   189 
   190 subsection {* Compactness and chain-finiteness *}
   191 
   192 lemma compact_Inl: "compact a \<Longrightarrow> compact (Inl a)"
   193 apply (rule compactI2)
   194 apply (erule sum_chain_cases, safe)
   195 apply (simp add: lub_Inl)
   196 apply (erule (2) compactD2)
   197 apply (simp add: lub_Inr)
   198 done
   199 
   200 lemma compact_Inr: "compact a \<Longrightarrow> compact (Inr a)"
   201 apply (rule compactI2)
   202 apply (erule sum_chain_cases, safe)
   203 apply (simp add: lub_Inl)
   204 apply (simp add: lub_Inr)
   205 apply (erule (2) compactD2)
   206 done
   207 
   208 lemma compact_Inl_rev: "compact (Inl a) \<Longrightarrow> compact a"
   209 unfolding compact_def
   210 by (drule adm_subst [OF cont_Inl], simp)
   211 
   212 lemma compact_Inr_rev: "compact (Inr a) \<Longrightarrow> compact a"
   213 unfolding compact_def
   214 by (drule adm_subst [OF cont_Inr], simp)
   215 
   216 lemma compact_Inl_iff [simp]: "compact (Inl a) = compact a"
   217 by (safe elim!: compact_Inl compact_Inl_rev)
   218 
   219 lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a"
   220 by (safe elim!: compact_Inr compact_Inr_rev)
   221 
   222 instance sum :: (chfin, chfin) chfin
   223 apply intro_classes
   224 apply (erule compact_imp_max_in_chain)
   225 apply (case_tac "\<Squnion>i. Y i", simp_all)
   226 done
   227 
   228 instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo
   229 by intro_classes (simp add: below_sum_def split: sum.split)
   230 
   231 subsection {* Using sum types with fixrec *}
   232 
   233 definition
   234   "match_Inl = (\<Lambda> x k. case x of Inl a \<Rightarrow> k\<cdot>a | Inr b \<Rightarrow> Fixrec.fail)"
   235 
   236 definition
   237   "match_Inr = (\<Lambda> x k. case x of Inl a \<Rightarrow> Fixrec.fail | Inr b \<Rightarrow> k\<cdot>b)"
   238 
   239 lemma match_Inl_simps [simp]:
   240   "match_Inl\<cdot>(Inl a)\<cdot>k = k\<cdot>a"
   241   "match_Inl\<cdot>(Inr b)\<cdot>k = Fixrec.fail"
   242 unfolding match_Inl_def by simp_all
   243 
   244 lemma match_Inr_simps [simp]:
   245   "match_Inr\<cdot>(Inl a)\<cdot>k = Fixrec.fail"
   246   "match_Inr\<cdot>(Inr b)\<cdot>k = k\<cdot>b"
   247 unfolding match_Inr_def by simp_all
   248 
   249 setup {*
   250   Fixrec.add_matchers
   251     [ (@{const_name Inl}, @{const_name match_Inl}),
   252       (@{const_name Inr}, @{const_name match_Inr}) ]
   253 *}
   254 
   255 subsection {* Disjoint sum is a predomain *}
   256 
   257 definition
   258   "encode_sum_u =
   259     (\<Lambda>(up\<cdot>x). case x of Inl a \<Rightarrow> sinl\<cdot>(up\<cdot>a) | Inr b \<Rightarrow> sinr\<cdot>(up\<cdot>b))"
   260 
   261 definition
   262   "decode_sum_u = sscase\<cdot>(\<Lambda>(up\<cdot>a). up\<cdot>(Inl a))\<cdot>(\<Lambda>(up\<cdot>b). up\<cdot>(Inr b))"
   263 
   264 lemma decode_encode_sum_u [simp]: "decode_sum_u\<cdot>(encode_sum_u\<cdot>x) = x"
   265 unfolding decode_sum_u_def encode_sum_u_def
   266 by (case_tac x, simp, rename_tac y, case_tac y, simp_all)
   267 
   268 lemma encode_decode_sum_u [simp]: "encode_sum_u\<cdot>(decode_sum_u\<cdot>x) = x"
   269 unfolding decode_sum_u_def encode_sum_u_def
   270 apply (case_tac x, simp)
   271 apply (rename_tac a, case_tac a, simp, simp)
   272 apply (rename_tac b, case_tac b, simp, simp)
   273 done
   274 
   275 text {* A deflation combinator for making unpointed types *}
   276 
   277 definition udefl :: "udom defl \<rightarrow> udom u defl"
   278   where "udefl = defl_fun1 (strictify\<cdot>up) (fup\<cdot>ID) ID"
   279 
   280 lemma ep_pair_strictify_up:
   281   "ep_pair (strictify\<cdot>up) (fup\<cdot>ID)"
   282 apply (rule ep_pair.intro)
   283 apply (simp add: strictify_conv_if)
   284 apply (case_tac y, simp, simp add: strictify_conv_if)
   285 done
   286 
   287 lemma cast_udefl:
   288   "cast\<cdot>(udefl\<cdot>t) = strictify\<cdot>up oo cast\<cdot>t oo fup\<cdot>ID"
   289 unfolding udefl_def by (simp add: cast_defl_fun1 ep_pair_strictify_up)
   290 
   291 definition sum_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
   292   where "sum_liftdefl = (\<Lambda> a b. udefl\<cdot>(ssum_defl\<cdot>(u_liftdefl\<cdot>a)\<cdot>(u_liftdefl\<cdot>b)))"
   293 
   294 lemma u_emb_bottom: "u_emb\<cdot>\<bottom> = \<bottom>"
   295 by (rule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def, OF ep_pair_u])
   296 
   297 (*
   298 definition sum_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
   299   where "sum_liftdefl = defl_fun2 (u_map\<cdot>emb oo strictify\<cdot>up)
   300     (fup\<cdot>ID oo u_map\<cdot>prj) ssum_map"
   301 *)
   302 
   303 instantiation sum :: (predomain, predomain) predomain
   304 begin
   305 
   306 definition
   307   "liftemb = (strictify\<cdot>up oo ssum_emb) oo
   308     (ssum_map\<cdot>(u_emb oo liftemb)\<cdot>(u_emb oo liftemb) oo encode_sum_u)"
   309 
   310 definition
   311   "liftprj = (decode_sum_u oo ssum_map\<cdot>(liftprj oo u_prj)\<cdot>(liftprj oo u_prj))
   312     oo (ssum_prj oo fup\<cdot>ID)"
   313 
   314 definition
   315   "liftdefl (t::('a + 'b) itself) = sum_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
   316 
   317 instance proof
   318   show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a + 'b) u)"
   319     unfolding liftemb_sum_def liftprj_sum_def
   320     by (intro ep_pair_comp ep_pair_ssum_map ep_pair_u predomain_ep
   321       ep_pair_ssum ep_pair_strictify_up, simp add: ep_pair.intro)
   322   show "cast\<cdot>LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom u \<rightarrow> ('a + 'b) u)"
   323     unfolding liftemb_sum_def liftprj_sum_def liftdefl_sum_def
   324     by (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_liftdefl
   325       cast_liftdefl cfcomp1 ssum_map_map u_emb_bottom)
   326 qed
   327 
   328 end
   329 
   330 subsection {* Configuring domain package to work with sum type *}
   331 
   332 lemma liftdefl_sum [domain_defl_simps]:
   333   "LIFTDEFL('a::predomain + 'b::predomain) =
   334     sum_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
   335 by (rule liftdefl_sum_def)
   336 
   337 abbreviation map_sum'
   338   where "map_sum' f g \<equiv> Abs_cfun (map_sum (Rep_cfun f) (Rep_cfun g))"
   339 
   340 lemma map_sum_ID [domain_map_ID]: "map_sum' ID ID = ID"
   341 by (simp add: ID_def cfun_eq_iff map_sum.identity id_def)
   342 
   343 lemma deflation_map_sum [domain_deflation]:
   344   "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (map_sum' d1 d2)"
   345 apply default
   346 apply (induct_tac x, simp_all add: deflation.idem)
   347 apply (induct_tac x, simp_all add: deflation.below)
   348 done
   349 
   350 lemma encode_sum_u_map_sum:
   351   "encode_sum_u\<cdot>(u_map\<cdot>(map_sum' f g)\<cdot>(decode_sum_u\<cdot>x))
   352     = ssum_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>x"
   353 apply (induct x, simp add: decode_sum_u_def encode_sum_u_def)
   354 apply (case_tac x, simp, simp add: decode_sum_u_def encode_sum_u_def)
   355 apply (case_tac y, simp, simp add: decode_sum_u_def encode_sum_u_def)
   356 done
   357 
   358 lemma isodefl_sum [domain_isodefl]:
   359   fixes d :: "'a::predomain \<rightarrow> 'a"
   360   assumes "isodefl' d1 t1" and "isodefl' d2 t2"
   361   shows "isodefl' (map_sum' d1 d2) (sum_liftdefl\<cdot>t1\<cdot>t2)"
   362 using assms unfolding isodefl'_def liftemb_sum_def liftprj_sum_def
   363 apply (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_liftdefl)
   364 apply (simp add: cfcomp1 encode_sum_u_map_sum)
   365 apply (simp add: ssum_map_map u_emb_bottom)
   366 done
   367 
   368 setup {*
   369   Domain_Take_Proofs.add_rec_type (@{type_name "sum"}, [true, true])
   370 *}
   371 
   372 end