src/HOL/HOLCF/Domain.thy
author huffman
Tue Nov 30 15:56:19 2010 -0800 (2010-11-30)
changeset 40834 a1249aeff5b6
parent 40830 158d18502378
child 41285 efd23c1d9886
permissions -rw-r--r--
change cpodef-generated cont_Rep rules to cont2cont format
     1 (*  Title:      HOLCF/Domain.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* Domain package *}
     6 
     7 theory Domain
     8 imports Bifinite Domain_Aux
     9 uses
    10   ("Tools/domaindef.ML")
    11   ("Tools/Domain/domain_isomorphism.ML")
    12   ("Tools/Domain/domain_axioms.ML")
    13   ("Tools/Domain/domain.ML")
    14 begin
    15 
    16 default_sort "domain"
    17 
    18 subsection {* Representations of types *}
    19 
    20 lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>DEFL('a)\<cdot>x"
    21 by (simp add: cast_DEFL)
    22 
    23 lemma emb_prj_emb:
    24   fixes x :: "'a"
    25   assumes "DEFL('a) \<sqsubseteq> DEFL('b)"
    26   shows "emb\<cdot>(prj\<cdot>(emb\<cdot>x) :: 'b) = emb\<cdot>x"
    27 unfolding emb_prj
    28 apply (rule cast.belowD)
    29 apply (rule monofun_cfun_arg [OF assms])
    30 apply (simp add: cast_DEFL)
    31 done
    32 
    33 lemma prj_emb_prj:
    34   assumes "DEFL('a) \<sqsubseteq> DEFL('b)"
    35   shows "prj\<cdot>(emb\<cdot>(prj\<cdot>x :: 'b)) = (prj\<cdot>x :: 'a)"
    36  apply (rule emb_eq_iff [THEN iffD1])
    37  apply (simp only: emb_prj)
    38  apply (rule deflation_below_comp1)
    39    apply (rule deflation_cast)
    40   apply (rule deflation_cast)
    41  apply (rule monofun_cfun_arg [OF assms])
    42 done
    43 
    44 text {* Isomorphism lemmas used internally by the domain package: *}
    45 
    46 lemma domain_abs_iso:
    47   fixes abs and rep
    48   assumes DEFL: "DEFL('b) = DEFL('a)"
    49   assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
    50   assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
    51   shows "rep\<cdot>(abs\<cdot>x) = x"
    52 unfolding abs_def rep_def
    53 by (simp add: emb_prj_emb DEFL)
    54 
    55 lemma domain_rep_iso:
    56   fixes abs and rep
    57   assumes DEFL: "DEFL('b) = DEFL('a)"
    58   assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
    59   assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
    60   shows "abs\<cdot>(rep\<cdot>x) = x"
    61 unfolding abs_def rep_def
    62 by (simp add: emb_prj_emb DEFL)
    63 
    64 subsection {* Deflations as sets *}
    65 
    66 definition defl_set :: "defl \<Rightarrow> udom set"
    67 where "defl_set A = {x. cast\<cdot>A\<cdot>x = x}"
    68 
    69 lemma adm_defl_set: "adm (\<lambda>x. x \<in> defl_set A)"
    70 unfolding defl_set_def by simp
    71 
    72 lemma defl_set_bottom: "\<bottom> \<in> defl_set A"
    73 unfolding defl_set_def by simp
    74 
    75 lemma defl_set_cast [simp]: "cast\<cdot>A\<cdot>x \<in> defl_set A"
    76 unfolding defl_set_def by simp
    77 
    78 lemma defl_set_subset_iff: "defl_set A \<subseteq> defl_set B \<longleftrightarrow> A \<sqsubseteq> B"
    79 apply (simp add: defl_set_def subset_eq cast_below_cast [symmetric])
    80 apply (auto simp add: cast.belowI cast.belowD)
    81 done
    82 
    83 subsection {* Proving a subtype is representable *}
    84 
    85 text {* Temporarily relax type constraints. *}
    86 
    87 setup {*
    88   fold Sign.add_const_constraint
    89   [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
    90   , (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"})
    91   , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"})
    92   , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
    93   , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom"})
    94   , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
    95 *}
    96 
    97 lemma typedef_liftdomain_class:
    98   fixes Rep :: "'a::pcpo \<Rightarrow> udom"
    99   fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
   100   fixes t :: defl
   101   assumes type: "type_definition Rep Abs (defl_set t)"
   102   assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   103   assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
   104   assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
   105   assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)"
   106   assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
   107   assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
   108   assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> defl) \<equiv> (\<lambda>t. u_defl\<cdot>DEFL('a))"
   109   shows "OFCLASS('a, liftdomain_class)"
   110 using liftemb [THEN meta_eq_to_obj_eq]
   111 using liftprj [THEN meta_eq_to_obj_eq]
   112 proof (rule liftdomain_class_intro)
   113   have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
   114     unfolding emb
   115     apply (rule beta_cfun)
   116     apply (rule typedef_cont_Rep [OF type below adm_defl_set cont_id])
   117     done
   118   have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)"
   119     unfolding prj
   120     apply (rule beta_cfun)
   121     apply (rule typedef_cont_Abs [OF type below adm_defl_set])
   122     apply simp_all
   123     done
   124   have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
   125     using type_definition.Rep [OF type]
   126     unfolding prj_beta emb_beta defl_set_def
   127     by (simp add: type_definition.Rep_inverse [OF type])
   128   have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
   129     unfolding prj_beta emb_beta
   130     by (simp add: type_definition.Abs_inverse [OF type])
   131   show "ep_pair (emb :: 'a \<rightarrow> udom) prj"
   132     apply default
   133     apply (simp add: prj_emb)
   134     apply (simp add: emb_prj cast.below)
   135     done
   136   show "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
   137     by (rule cfun_eqI, simp add: defl emb_prj)
   138   show "LIFTDEFL('a) = u_defl\<cdot>DEFL('a)"
   139     unfolding liftdefl ..
   140 qed
   141 
   142 lemma typedef_DEFL:
   143   assumes "defl \<equiv> (\<lambda>a::'a::pcpo itself. t)"
   144   shows "DEFL('a::pcpo) = t"
   145 unfolding assms ..
   146 
   147 text {* Restore original typing constraints. *}
   148 
   149 setup {*
   150   fold Sign.add_const_constraint
   151   [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> defl"})
   152   , (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"})
   153   , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::domain"})
   154   , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> defl"})
   155   , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"})
   156   , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
   157 *}
   158 
   159 use "Tools/domaindef.ML"
   160 
   161 subsection {* Isomorphic deflations *}
   162 
   163 definition
   164   isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> defl \<Rightarrow> bool"
   165 where
   166   "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
   167 
   168 lemma isodeflI: "(\<And>x. cast\<cdot>t\<cdot>x = emb\<cdot>(d\<cdot>(prj\<cdot>x))) \<Longrightarrow> isodefl d t"
   169 unfolding isodefl_def by (simp add: cfun_eqI)
   170 
   171 lemma cast_isodefl: "isodefl d t \<Longrightarrow> cast\<cdot>t = (\<Lambda> x. emb\<cdot>(d\<cdot>(prj\<cdot>x)))"
   172 unfolding isodefl_def by (simp add: cfun_eqI)
   173 
   174 lemma isodefl_strict: "isodefl d t \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
   175 unfolding isodefl_def
   176 by (drule cfun_fun_cong [where x="\<bottom>"], simp)
   177 
   178 lemma isodefl_imp_deflation:
   179   fixes d :: "'a \<rightarrow> 'a"
   180   assumes "isodefl d t" shows "deflation d"
   181 proof
   182   note assms [unfolded isodefl_def, simp]
   183   fix x :: 'a
   184   show "d\<cdot>(d\<cdot>x) = d\<cdot>x"
   185     using cast.idem [of t "emb\<cdot>x"] by simp
   186   show "d\<cdot>x \<sqsubseteq> x"
   187     using cast.below [of t "emb\<cdot>x"] by simp
   188 qed
   189 
   190 lemma isodefl_ID_DEFL: "isodefl (ID :: 'a \<rightarrow> 'a) DEFL('a)"
   191 unfolding isodefl_def by (simp add: cast_DEFL)
   192 
   193 lemma isodefl_LIFTDEFL:
   194   "isodefl (u_map\<cdot>(ID :: 'a \<rightarrow> 'a)) LIFTDEFL('a::predomain)"
   195 unfolding u_map_ID DEFL_u [symmetric]
   196 by (rule isodefl_ID_DEFL)
   197 
   198 lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID"
   199 unfolding isodefl_def
   200 apply (simp add: cast_DEFL)
   201 apply (simp add: cfun_eq_iff)
   202 apply (rule allI)
   203 apply (drule_tac x="emb\<cdot>x" in spec)
   204 apply simp
   205 done
   206 
   207 lemma isodefl_bottom: "isodefl \<bottom> \<bottom>"
   208 unfolding isodefl_def by (simp add: cfun_eq_iff)
   209 
   210 lemma adm_isodefl:
   211   "cont f \<Longrightarrow> cont g \<Longrightarrow> adm (\<lambda>x. isodefl (f x) (g x))"
   212 unfolding isodefl_def by simp
   213 
   214 lemma isodefl_lub:
   215   assumes "chain d" and "chain t"
   216   assumes "\<And>i. isodefl (d i) (t i)"
   217   shows "isodefl (\<Squnion>i. d i) (\<Squnion>i. t i)"
   218 using prems unfolding isodefl_def
   219 by (simp add: contlub_cfun_arg contlub_cfun_fun)
   220 
   221 lemma isodefl_fix:
   222   assumes "\<And>d t. isodefl d t \<Longrightarrow> isodefl (f\<cdot>d) (g\<cdot>t)"
   223   shows "isodefl (fix\<cdot>f) (fix\<cdot>g)"
   224 unfolding fix_def2
   225 apply (rule isodefl_lub, simp, simp)
   226 apply (induct_tac i)
   227 apply (simp add: isodefl_bottom)
   228 apply (simp add: assms)
   229 done
   230 
   231 lemma isodefl_abs_rep:
   232   fixes abs and rep and d
   233   assumes DEFL: "DEFL('b) = DEFL('a)"
   234   assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
   235   assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
   236   shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
   237 unfolding isodefl_def
   238 by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb)
   239 
   240 lemma isodefl_sfun:
   241   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
   242     isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
   243 apply (rule isodeflI)
   244 apply (simp add: cast_sfun_defl cast_isodefl)
   245 apply (simp add: emb_sfun_def prj_sfun_def)
   246 apply (simp add: sfun_map_map isodefl_strict)
   247 done
   248 
   249 lemma isodefl_ssum:
   250   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
   251     isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)"
   252 apply (rule isodeflI)
   253 apply (simp add: cast_ssum_defl cast_isodefl)
   254 apply (simp add: emb_ssum_def prj_ssum_def)
   255 apply (simp add: ssum_map_map isodefl_strict)
   256 done
   257 
   258 lemma isodefl_sprod:
   259   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
   260     isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)"
   261 apply (rule isodeflI)
   262 apply (simp add: cast_sprod_defl cast_isodefl)
   263 apply (simp add: emb_sprod_def prj_sprod_def)
   264 apply (simp add: sprod_map_map isodefl_strict)
   265 done
   266 
   267 lemma isodefl_cprod:
   268   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
   269     isodefl (cprod_map\<cdot>d1\<cdot>d2) (prod_defl\<cdot>t1\<cdot>t2)"
   270 apply (rule isodeflI)
   271 apply (simp add: cast_prod_defl cast_isodefl)
   272 apply (simp add: emb_prod_def prj_prod_def)
   273 apply (simp add: cprod_map_map cfcomp1)
   274 done
   275 
   276 lemma isodefl_u:
   277   fixes d :: "'a::liftdomain \<rightarrow> 'a"
   278   shows "isodefl (d :: 'a \<rightarrow> 'a) t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
   279 apply (rule isodeflI)
   280 apply (simp add: cast_u_defl cast_isodefl)
   281 apply (simp add: emb_u_def prj_u_def liftemb_eq liftprj_eq)
   282 apply (simp add: u_map_map)
   283 done
   284 
   285 lemma encode_prod_u_map:
   286   "encode_prod_u\<cdot>(u_map\<cdot>(cprod_map\<cdot>f\<cdot>g)\<cdot>(decode_prod_u\<cdot>x))
   287     = sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>x"
   288 unfolding encode_prod_u_def decode_prod_u_def
   289 apply (case_tac x, simp, rename_tac a b)
   290 apply (case_tac a, simp, case_tac b, simp, simp)
   291 done
   292 
   293 lemma isodefl_cprod_u:
   294   assumes "isodefl (u_map\<cdot>d1) t1" and "isodefl (u_map\<cdot>d2) t2"
   295   shows "isodefl (u_map\<cdot>(cprod_map\<cdot>d1\<cdot>d2)) (sprod_defl\<cdot>t1\<cdot>t2)"
   296 using isodefl_sprod [OF assms] unfolding isodefl_def
   297 unfolding emb_u_def prj_u_def liftemb_prod_def liftprj_prod_def
   298 by (simp add: cfcomp1 encode_prod_u_map)
   299 
   300 lemma encode_cfun_map:
   301   "encode_cfun\<cdot>(cfun_map\<cdot>f\<cdot>g\<cdot>(decode_cfun\<cdot>x))
   302     = sfun_map\<cdot>(u_map\<cdot>f)\<cdot>g\<cdot>x"
   303 unfolding encode_cfun_def decode_cfun_def
   304 apply (simp add: sfun_eq_iff cfun_map_def sfun_map_def)
   305 apply (rule cfun_eqI, rename_tac y, case_tac y, simp_all)
   306 done
   307 
   308 lemma isodefl_cfun:
   309   assumes "isodefl (u_map\<cdot>d1) t1" and "isodefl d2 t2"
   310   shows "isodefl (cfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
   311 using isodefl_sfun [OF assms] unfolding isodefl_def
   312 by (simp add: emb_cfun_def prj_cfun_def cfcomp1 encode_cfun_map)
   313 
   314 subsection {* Setting up the domain package *}
   315 
   316 use "Tools/Domain/domain_isomorphism.ML"
   317 use "Tools/Domain/domain_axioms.ML"
   318 use "Tools/Domain/domain.ML"
   319 
   320 setup Domain_Isomorphism.setup
   321 
   322 lemmas [domain_defl_simps] =
   323   DEFL_cfun DEFL_sfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
   324   liftdefl_eq LIFTDEFL_prod
   325 
   326 lemmas [domain_map_ID] =
   327   cfun_map_ID sfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID
   328 
   329 lemmas [domain_isodefl] =
   330   isodefl_u isodefl_sfun isodefl_ssum isodefl_sprod
   331   isodefl_cfun isodefl_cprod isodefl_cprod_u
   332 
   333 lemmas [domain_deflation] =
   334   deflation_cfun_map deflation_sfun_map deflation_ssum_map
   335   deflation_sprod_map deflation_cprod_map deflation_u_map
   336 
   337 setup {*
   338   fold Domain_Take_Proofs.add_rec_type
   339     [(@{type_name cfun}, [true, true]),
   340      (@{type_name "sfun"}, [true, true]),
   341      (@{type_name ssum}, [true, true]),
   342      (@{type_name sprod}, [true, true]),
   343      (@{type_name prod}, [true, true]),
   344      (@{type_name "u"}, [true])]
   345 *}
   346 
   347 end