src/HOLCF/Representable.thy
author huffman
Tue Oct 12 06:20:05 2010 -0700 (2010-10-12)
changeset 40006 116e94f9543b
parent 40002 c5b5f7a3a3b1
child 40037 81e6b89d8f58
permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
     1 (*  Title:      HOLCF/Representable.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* Representable Types *}
     6 
     7 theory Representable
     8 imports Algebraic Bifinite Universal Ssum One Fixrec Domain_Aux
     9 uses
    10   ("Tools/repdef.ML")
    11   ("Tools/Domain/domain_isomorphism.ML")
    12 begin
    13 
    14 default_sort bifinite
    15 
    16 subsection {* Representations of types *}
    17 
    18 lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>DEFL('a)\<cdot>x"
    19 by (simp add: cast_DEFL)
    20 
    21 lemma in_DEFL_iff:
    22   "x ::: DEFL('a) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
    23 by (simp add: in_defl_def cast_DEFL)
    24 
    25 lemma prj_inverse:
    26   "x ::: DEFL('a) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
    27 by (simp only: in_DEFL_iff)
    28 
    29 lemma emb_in_DEFL [simp]:
    30   "emb\<cdot>(x::'a) ::: DEFL('a)"
    31 by (simp add: in_DEFL_iff)
    32 
    33 subsection {* Coerce operator *}
    34 
    35 definition coerce :: "'a \<rightarrow> 'b"
    36 where "coerce = prj oo emb"
    37 
    38 lemma beta_coerce: "coerce\<cdot>x = prj\<cdot>(emb\<cdot>x)"
    39 by (simp add: coerce_def)
    40 
    41 lemma prj_emb: "prj\<cdot>(emb\<cdot>x) = coerce\<cdot>x"
    42 by (simp add: coerce_def)
    43 
    44 lemma coerce_strict [simp]: "coerce\<cdot>\<bottom> = \<bottom>"
    45 by (simp add: coerce_def)
    46 
    47 lemma coerce_eq_ID [simp]: "(coerce :: 'a \<rightarrow> 'a) = ID"
    48 by (rule cfun_eqI, simp add: beta_coerce)
    49 
    50 lemma emb_coerce:
    51   "DEFL('a) \<sqsubseteq> DEFL('b)
    52    \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = emb\<cdot>x"
    53  apply (simp add: beta_coerce)
    54  apply (rule prj_inverse)
    55  apply (erule defl_belowD)
    56  apply (rule emb_in_DEFL)
    57 done
    58 
    59 lemma coerce_prj:
    60   "DEFL('a) \<sqsubseteq> DEFL('b)
    61    \<Longrightarrow> (coerce::'b \<rightarrow> 'a)\<cdot>(prj\<cdot>x) = prj\<cdot>x"
    62  apply (simp add: coerce_def)
    63  apply (rule emb_eq_iff [THEN iffD1])
    64  apply (simp only: emb_prj)
    65  apply (rule deflation_below_comp1)
    66    apply (rule deflation_cast)
    67   apply (rule deflation_cast)
    68  apply (erule monofun_cfun_arg)
    69 done
    70 
    71 lemma coerce_coerce [simp]:
    72   "DEFL('a) \<sqsubseteq> DEFL('b)
    73    \<Longrightarrow> coerce\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = coerce\<cdot>x"
    74 by (simp add: beta_coerce prj_inverse defl_belowD)
    75 
    76 lemma coerce_inverse:
    77   "emb\<cdot>(x::'a) ::: DEFL('b) \<Longrightarrow> coerce\<cdot>(coerce\<cdot>x :: 'b) = x"
    78 by (simp only: beta_coerce prj_inverse emb_inverse)
    79 
    80 lemma coerce_type:
    81   "DEFL('a) \<sqsubseteq> DEFL('b)
    82    \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) ::: DEFL('a)"
    83 by (simp add: beta_coerce prj_inverse defl_belowD)
    84 
    85 lemma ep_pair_coerce:
    86   "DEFL('a) \<sqsubseteq> DEFL('b)
    87    \<Longrightarrow> ep_pair (coerce::'a \<rightarrow> 'b) (coerce::'b \<rightarrow> 'a)"
    88  apply (rule ep_pair.intro)
    89   apply simp
    90  apply (simp only: beta_coerce)
    91  apply (rule below_trans)
    92   apply (rule monofun_cfun_arg)
    93   apply (rule emb_prj_below)
    94  apply simp
    95 done
    96 
    97 text {* Isomorphism lemmas used internally by the domain package: *}
    98 
    99 lemma domain_abs_iso:
   100   fixes abs and rep
   101   assumes DEFL: "DEFL('b) = DEFL('a)"
   102   assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
   103   assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
   104   shows "rep\<cdot>(abs\<cdot>x) = x"
   105 unfolding abs_def rep_def by (simp add: DEFL)
   106 
   107 lemma domain_rep_iso:
   108   fixes abs and rep
   109   assumes DEFL: "DEFL('b) = DEFL('a)"
   110   assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
   111   assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
   112   shows "abs\<cdot>(rep\<cdot>x) = x"
   113 unfolding abs_def rep_def by (simp add: DEFL [symmetric])
   114 
   115 
   116 subsection {* Proving a subtype is representable *}
   117 
   118 text {*
   119   Temporarily relax type constraints for @{term emb}, and @{term prj}.
   120 *}
   121 
   122 setup {* Sign.add_const_constraint
   123   (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"}) *}
   124 
   125 setup {* Sign.add_const_constraint
   126   (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"}) *}
   127 
   128 setup {* Sign.add_const_constraint
   129   (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"}) *}
   130 
   131 lemma typedef_rep_class:
   132   fixes Rep :: "'a::pcpo \<Rightarrow> udom"
   133   fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
   134   fixes t :: defl
   135   assumes type: "type_definition Rep Abs {x. x ::: t}"
   136   assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   137   assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
   138   assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
   139   assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)"
   140   shows "OFCLASS('a, bifinite_class)"
   141 proof
   142   have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})"
   143     by (simp add: adm_in_defl)
   144   have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
   145     unfolding emb
   146     apply (rule beta_cfun)
   147     apply (rule typedef_cont_Rep [OF type below adm])
   148     done
   149   have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)"
   150     unfolding prj
   151     apply (rule beta_cfun)
   152     apply (rule typedef_cont_Abs [OF type below adm])
   153     apply simp_all
   154     done
   155   have emb_in_defl: "\<And>x::'a. emb\<cdot>x ::: t"
   156     using type_definition.Rep [OF type]
   157     by (simp add: emb_beta)
   158   have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
   159     unfolding prj_beta
   160     apply (simp add: cast_fixed [OF emb_in_defl])
   161     apply (simp add: emb_beta type_definition.Rep_inverse [OF type])
   162     done
   163   have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
   164     unfolding prj_beta emb_beta
   165     by (simp add: type_definition.Abs_inverse [OF type])
   166   show "ep_pair (emb :: 'a \<rightarrow> udom) prj"
   167     apply default
   168     apply (simp add: prj_emb)
   169     apply (simp add: emb_prj cast.below)
   170     done
   171   show "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
   172     by (rule cfun_eqI, simp add: defl emb_prj)
   173 qed
   174 
   175 lemma typedef_DEFL:
   176   assumes "defl \<equiv> (\<lambda>a::'a::pcpo itself. t)"
   177   shows "DEFL('a::pcpo) = t"
   178 unfolding assms ..
   179 
   180 text {* Restore original typing constraints *}
   181 
   182 setup {* Sign.add_const_constraint
   183   (@{const_name defl}, SOME @{typ "'a::bifinite itself \<Rightarrow> defl"}) *}
   184 
   185 setup {* Sign.add_const_constraint
   186   (@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"}) *}
   187 
   188 setup {* Sign.add_const_constraint
   189   (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"}) *}
   190 
   191 lemma adm_mem_Collect_in_defl: "adm (\<lambda>x. x \<in> {x. x ::: A})"
   192 unfolding mem_Collect_eq by (rule adm_in_defl)
   193 
   194 use "Tools/repdef.ML"
   195 
   196 subsection {* Isomorphic deflations *}
   197 
   198 definition
   199   isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> defl \<Rightarrow> bool"
   200 where
   201   "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
   202 
   203 lemma isodeflI: "(\<And>x. cast\<cdot>t\<cdot>x = emb\<cdot>(d\<cdot>(prj\<cdot>x))) \<Longrightarrow> isodefl d t"
   204 unfolding isodefl_def by (simp add: cfun_eqI)
   205 
   206 lemma cast_isodefl: "isodefl d t \<Longrightarrow> cast\<cdot>t = (\<Lambda> x. emb\<cdot>(d\<cdot>(prj\<cdot>x)))"
   207 unfolding isodefl_def by (simp add: cfun_eqI)
   208 
   209 lemma isodefl_strict: "isodefl d t \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
   210 unfolding isodefl_def
   211 by (drule cfun_fun_cong [where x="\<bottom>"], simp)
   212 
   213 lemma isodefl_imp_deflation:
   214   fixes d :: "'a \<rightarrow> 'a"
   215   assumes "isodefl d t" shows "deflation d"
   216 proof
   217   note assms [unfolded isodefl_def, simp]
   218   fix x :: 'a
   219   show "d\<cdot>(d\<cdot>x) = d\<cdot>x"
   220     using cast.idem [of t "emb\<cdot>x"] by simp
   221   show "d\<cdot>x \<sqsubseteq> x"
   222     using cast.below [of t "emb\<cdot>x"] by simp
   223 qed
   224 
   225 lemma isodefl_ID_DEFL: "isodefl (ID :: 'a \<rightarrow> 'a) DEFL('a)"
   226 unfolding isodefl_def by (simp add: cast_DEFL)
   227 
   228 lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID"
   229 unfolding isodefl_def
   230 apply (simp add: cast_DEFL)
   231 apply (simp add: cfun_eq_iff)
   232 apply (rule allI)
   233 apply (drule_tac x="emb\<cdot>x" in spec)
   234 apply simp
   235 done
   236 
   237 lemma isodefl_bottom: "isodefl \<bottom> \<bottom>"
   238 unfolding isodefl_def by (simp add: cfun_eq_iff)
   239 
   240 lemma adm_isodefl:
   241   "cont f \<Longrightarrow> cont g \<Longrightarrow> adm (\<lambda>x. isodefl (f x) (g x))"
   242 unfolding isodefl_def by simp
   243 
   244 lemma isodefl_lub:
   245   assumes "chain d" and "chain t"
   246   assumes "\<And>i. isodefl (d i) (t i)"
   247   shows "isodefl (\<Squnion>i. d i) (\<Squnion>i. t i)"
   248 using prems unfolding isodefl_def
   249 by (simp add: contlub_cfun_arg contlub_cfun_fun)
   250 
   251 lemma isodefl_fix:
   252   assumes "\<And>d t. isodefl d t \<Longrightarrow> isodefl (f\<cdot>d) (g\<cdot>t)"
   253   shows "isodefl (fix\<cdot>f) (fix\<cdot>g)"
   254 unfolding fix_def2
   255 apply (rule isodefl_lub, simp, simp)
   256 apply (induct_tac i)
   257 apply (simp add: isodefl_bottom)
   258 apply (simp add: assms)
   259 done
   260 
   261 lemma isodefl_coerce:
   262   fixes d :: "'a \<rightarrow> 'a"
   263   assumes DEFL: "DEFL('b) = DEFL('a)"
   264   shows "isodefl d t \<Longrightarrow> isodefl (coerce oo d oo coerce :: 'b \<rightarrow> 'b) t"
   265 unfolding isodefl_def
   266 apply (simp add: cfun_eq_iff)
   267 apply (simp add: emb_coerce coerce_prj DEFL)
   268 done
   269 
   270 lemma isodefl_abs_rep:
   271   fixes abs and rep and d
   272   assumes DEFL: "DEFL('b) = DEFL('a)"
   273   assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
   274   assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
   275   shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
   276 unfolding abs_def rep_def using DEFL by (rule isodefl_coerce)
   277 
   278 lemma isodefl_cfun:
   279   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
   280     isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
   281 apply (rule isodeflI)
   282 apply (simp add: cast_cfun_defl cast_isodefl)
   283 apply (simp add: emb_cfun_def prj_cfun_def)
   284 apply (simp add: cfun_map_map cfcomp1)
   285 done
   286 
   287 lemma isodefl_ssum:
   288   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
   289     isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)"
   290 apply (rule isodeflI)
   291 apply (simp add: cast_ssum_defl cast_isodefl)
   292 apply (simp add: emb_ssum_def prj_ssum_def)
   293 apply (simp add: ssum_map_map isodefl_strict)
   294 done
   295 
   296 lemma isodefl_sprod:
   297   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
   298     isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)"
   299 apply (rule isodeflI)
   300 apply (simp add: cast_sprod_defl cast_isodefl)
   301 apply (simp add: emb_sprod_def prj_sprod_def)
   302 apply (simp add: sprod_map_map isodefl_strict)
   303 done
   304 
   305 lemma isodefl_cprod:
   306   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
   307     isodefl (cprod_map\<cdot>d1\<cdot>d2) (prod_defl\<cdot>t1\<cdot>t2)"
   308 apply (rule isodeflI)
   309 apply (simp add: cast_prod_defl cast_isodefl)
   310 apply (simp add: emb_prod_def prj_prod_def)
   311 apply (simp add: cprod_map_map cfcomp1)
   312 done
   313 
   314 lemma isodefl_u:
   315   "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
   316 apply (rule isodeflI)
   317 apply (simp add: cast_u_defl cast_isodefl)
   318 apply (simp add: emb_u_def prj_u_def)
   319 apply (simp add: u_map_map)
   320 done
   321 
   322 subsection {* Constructing Domain Isomorphisms *}
   323 
   324 use "Tools/Domain/domain_isomorphism.ML"
   325 
   326 setup {*
   327   fold Domain_Isomorphism.add_type_constructor
   328     [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm DEFL_cfun},
   329         @{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}),
   330 
   331      (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm DEFL_ssum},
   332         @{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}),
   333 
   334      (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm DEFL_sprod},
   335         @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
   336 
   337      (@{type_name prod}, @{term cprod_defl}, @{const_name cprod_map}, @{thm DEFL_prod},
   338         @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}),
   339 
   340      (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm DEFL_u},
   341         @{thm isodefl_u}, @{thm u_map_ID}, @{thm deflation_u_map})]
   342 *}
   343 
   344 end