src/HOL/HOLCF/Powerdomains.thy
author wenzelm
Wed Jan 13 23:07:06 2016 +0100 (2016-01-13)
changeset 62175 8ffc4d0e652d
parent 58880 0baae4311a9f
child 69597 ff784d5a5bfb
permissions -rw-r--r--
isabelle update_cartouches -c -t;
     1 (*  Title:      HOL/HOLCF/Powerdomains.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 section \<open>Powerdomains\<close>
     6 
     7 theory Powerdomains
     8 imports ConvexPD Domain
     9 begin
    10 
    11 subsection \<open>Universal domain embeddings\<close>
    12 
    13 definition "upper_emb = udom_emb (\<lambda>i. upper_map\<cdot>(udom_approx i))"
    14 definition "upper_prj = udom_prj (\<lambda>i. upper_map\<cdot>(udom_approx i))"
    15 
    16 definition "lower_emb = udom_emb (\<lambda>i. lower_map\<cdot>(udom_approx i))"
    17 definition "lower_prj = udom_prj (\<lambda>i. lower_map\<cdot>(udom_approx i))"
    18 
    19 definition "convex_emb = udom_emb (\<lambda>i. convex_map\<cdot>(udom_approx i))"
    20 definition "convex_prj = udom_prj (\<lambda>i. convex_map\<cdot>(udom_approx i))"
    21 
    22 lemma ep_pair_upper: "ep_pair upper_emb upper_prj"
    23   unfolding upper_emb_def upper_prj_def
    24   by (simp add: ep_pair_udom approx_chain_upper_map)
    25 
    26 lemma ep_pair_lower: "ep_pair lower_emb lower_prj"
    27   unfolding lower_emb_def lower_prj_def
    28   by (simp add: ep_pair_udom approx_chain_lower_map)
    29 
    30 lemma ep_pair_convex: "ep_pair convex_emb convex_prj"
    31   unfolding convex_emb_def convex_prj_def
    32   by (simp add: ep_pair_udom approx_chain_convex_map)
    33 
    34 subsection \<open>Deflation combinators\<close>
    35 
    36 definition upper_defl :: "udom defl \<rightarrow> udom defl"
    37   where "upper_defl = defl_fun1 upper_emb upper_prj upper_map"
    38 
    39 definition lower_defl :: "udom defl \<rightarrow> udom defl"
    40   where "lower_defl = defl_fun1 lower_emb lower_prj lower_map"
    41 
    42 definition convex_defl :: "udom defl \<rightarrow> udom defl"
    43   where "convex_defl = defl_fun1 convex_emb convex_prj convex_map"
    44 
    45 lemma cast_upper_defl:
    46   "cast\<cdot>(upper_defl\<cdot>A) = upper_emb oo upper_map\<cdot>(cast\<cdot>A) oo upper_prj"
    47 using ep_pair_upper finite_deflation_upper_map
    48 unfolding upper_defl_def by (rule cast_defl_fun1)
    49 
    50 lemma cast_lower_defl:
    51   "cast\<cdot>(lower_defl\<cdot>A) = lower_emb oo lower_map\<cdot>(cast\<cdot>A) oo lower_prj"
    52 using ep_pair_lower finite_deflation_lower_map
    53 unfolding lower_defl_def by (rule cast_defl_fun1)
    54 
    55 lemma cast_convex_defl:
    56   "cast\<cdot>(convex_defl\<cdot>A) = convex_emb oo convex_map\<cdot>(cast\<cdot>A) oo convex_prj"
    57 using ep_pair_convex finite_deflation_convex_map
    58 unfolding convex_defl_def by (rule cast_defl_fun1)
    59 
    60 subsection \<open>Domain class instances\<close>
    61 
    62 instantiation upper_pd :: ("domain") "domain"
    63 begin
    64 
    65 definition
    66   "emb = upper_emb oo upper_map\<cdot>emb"
    67 
    68 definition
    69   "prj = upper_map\<cdot>prj oo upper_prj"
    70 
    71 definition
    72   "defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)"
    73 
    74 definition
    75   "(liftemb :: 'a upper_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
    76 
    77 definition
    78   "(liftprj :: udom u \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj"
    79 
    80 definition
    81   "liftdefl (t::'a upper_pd itself) = liftdefl_of\<cdot>DEFL('a upper_pd)"
    82 
    83 instance proof
    84   show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
    85     unfolding emb_upper_pd_def prj_upper_pd_def
    86     by (intro ep_pair_comp ep_pair_upper ep_pair_upper_map ep_pair_emb_prj)
    87 next
    88   show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
    89     unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
    90     by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map)
    91 qed (fact liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def)+
    92 
    93 end
    94 
    95 instantiation lower_pd :: ("domain") "domain"
    96 begin
    97 
    98 definition
    99   "emb = lower_emb oo lower_map\<cdot>emb"
   100 
   101 definition
   102   "prj = lower_map\<cdot>prj oo lower_prj"
   103 
   104 definition
   105   "defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)"
   106 
   107 definition
   108   "(liftemb :: 'a lower_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
   109 
   110 definition
   111   "(liftprj :: udom u \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj"
   112 
   113 definition
   114   "liftdefl (t::'a lower_pd itself) = liftdefl_of\<cdot>DEFL('a lower_pd)"
   115 
   116 instance proof
   117   show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
   118     unfolding emb_lower_pd_def prj_lower_pd_def
   119     by (intro ep_pair_comp ep_pair_lower ep_pair_lower_map ep_pair_emb_prj)
   120 next
   121   show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
   122     unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
   123     by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map)
   124 qed (fact liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def)+
   125 
   126 end
   127 
   128 instantiation convex_pd :: ("domain") "domain"
   129 begin
   130 
   131 definition
   132   "emb = convex_emb oo convex_map\<cdot>emb"
   133 
   134 definition
   135   "prj = convex_map\<cdot>prj oo convex_prj"
   136 
   137 definition
   138   "defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
   139 
   140 definition
   141   "(liftemb :: 'a convex_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
   142 
   143 definition
   144   "(liftprj :: udom u \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj"
   145 
   146 definition
   147   "liftdefl (t::'a convex_pd itself) = liftdefl_of\<cdot>DEFL('a convex_pd)"
   148 
   149 instance proof
   150   show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
   151     unfolding emb_convex_pd_def prj_convex_pd_def
   152     by (intro ep_pair_comp ep_pair_convex ep_pair_convex_map ep_pair_emb_prj)
   153 next
   154   show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
   155     unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
   156     by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map)
   157 qed (fact liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def)+
   158 
   159 end
   160 
   161 lemma DEFL_upper: "DEFL('a::domain upper_pd) = upper_defl\<cdot>DEFL('a)"
   162 by (rule defl_upper_pd_def)
   163 
   164 lemma DEFL_lower: "DEFL('a::domain lower_pd) = lower_defl\<cdot>DEFL('a)"
   165 by (rule defl_lower_pd_def)
   166 
   167 lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)"
   168 by (rule defl_convex_pd_def)
   169 
   170 subsection \<open>Isomorphic deflations\<close>
   171 
   172 lemma isodefl_upper:
   173   "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
   174 apply (rule isodeflI)
   175 apply (simp add: cast_upper_defl cast_isodefl)
   176 apply (simp add: emb_upper_pd_def prj_upper_pd_def)
   177 apply (simp add: upper_map_map)
   178 done
   179 
   180 lemma isodefl_lower:
   181   "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)"
   182 apply (rule isodeflI)
   183 apply (simp add: cast_lower_defl cast_isodefl)
   184 apply (simp add: emb_lower_pd_def prj_lower_pd_def)
   185 apply (simp add: lower_map_map)
   186 done
   187 
   188 lemma isodefl_convex:
   189   "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)"
   190 apply (rule isodeflI)
   191 apply (simp add: cast_convex_defl cast_isodefl)
   192 apply (simp add: emb_convex_pd_def prj_convex_pd_def)
   193 apply (simp add: convex_map_map)
   194 done
   195 
   196 subsection \<open>Domain package setup for powerdomains\<close>
   197 
   198 lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex
   199 lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID
   200 lemmas [domain_isodefl] = isodefl_upper isodefl_lower isodefl_convex
   201 
   202 lemmas [domain_deflation] =
   203   deflation_upper_map deflation_lower_map deflation_convex_map
   204 
   205 setup \<open>
   206   fold Domain_Take_Proofs.add_rec_type
   207     [(@{type_name "upper_pd"}, [true]),
   208      (@{type_name "lower_pd"}, [true]),
   209      (@{type_name "convex_pd"}, [true])]
   210 \<close>
   211 
   212 end