src/HOL/HOLCF/Representable.thy
author huffman
Sun Dec 19 17:37:19 2010 -0800 (2010-12-19)
changeset 41292 2b7bc8d9fd6e
parent 41290 e9c9577d88b5
child 41297 01b2de947cff
permissions -rw-r--r--
use deflations over type 'udom u' to represent predomains;
removed now-unnecessary class liftdomain;
huffman@41285
     1
(*  Title:      HOLCF/Representable.thy
huffman@25903
     2
    Author:     Brian Huffman
huffman@25903
     3
*)
huffman@25903
     4
huffman@41285
     5
header {* Representable domains *}
huffman@25903
     6
huffman@41285
     7
theory Representable
huffman@40502
     8
imports Algebraic Map_Functions Countable
huffman@25903
     9
begin
huffman@25903
    10
huffman@41292
    11
default_sort cpo
huffman@41292
    12
huffman@41285
    13
subsection {* Class of representable domains *}
huffman@39985
    14
huffman@39985
    15
text {*
huffman@40497
    16
  We define a ``domain'' as a pcpo that is isomorphic to some
huffman@40497
    17
  algebraic deflation over the universal domain; this is equivalent
huffman@40497
    18
  to being omega-bifinite.
huffman@40491
    19
huffman@40497
    20
  A predomain is a cpo that, when lifted, becomes a domain.
huffman@41292
    21
  Predomains are represented by deflations over a lifted universal
huffman@41292
    22
  domain type.
huffman@39985
    23
*}
huffman@39985
    24
huffman@41292
    25
class predomain_syn = cpo +
huffman@41292
    26
  fixes liftemb :: "'a\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
huffman@41292
    27
  fixes liftprj :: "udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>"
huffman@41292
    28
  fixes liftdefl :: "'a itself \<Rightarrow> udom u defl"
huffman@41292
    29
huffman@41292
    30
class predomain = predomain_syn +
huffman@40491
    31
  assumes predomain_ep: "ep_pair liftemb liftprj"
huffman@41292
    32
  assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a)) = liftemb oo liftprj"
huffman@40491
    33
huffman@40491
    34
syntax "_LIFTDEFL" :: "type \<Rightarrow> logic"  ("(1LIFTDEFL/(1'(_')))")
huffman@40491
    35
translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"
huffman@40491
    36
huffman@41292
    37
definition pdefl :: "udom defl \<rightarrow> udom u defl"
huffman@41292
    38
  where "pdefl = defl_fun1 ID ID u_map"
huffman@41292
    39
huffman@41292
    40
lemma cast_pdefl: "cast\<cdot>(pdefl\<cdot>t) = u_map\<cdot>(cast\<cdot>t)"
huffman@41292
    41
by (simp add: pdefl_def cast_defl_fun1 ep_pair_def finite_deflation_u_map)
huffman@41292
    42
huffman@41292
    43
class "domain" = predomain_syn + pcpo +
huffman@41292
    44
  fixes emb :: "'a \<rightarrow> udom"
huffman@41292
    45
  fixes prj :: "udom \<rightarrow> 'a"
huffman@41287
    46
  fixes defl :: "'a itself \<Rightarrow> udom defl"
huffman@39985
    47
  assumes ep_pair_emb_prj: "ep_pair emb prj"
huffman@39989
    48
  assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj"
huffman@41292
    49
  assumes liftemb_eq: "liftemb = u_map\<cdot>emb"
huffman@41292
    50
  assumes liftprj_eq: "liftprj = u_map\<cdot>prj"
huffman@41292
    51
  assumes liftdefl_eq: "liftdefl TYPE('a) = pdefl\<cdot>(defl TYPE('a))"
huffman@31113
    52
huffman@41287
    53
syntax "_DEFL" :: "type \<Rightarrow> logic"  ("(1DEFL/(1'(_')))")
huffman@39989
    54
translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
huffman@39985
    55
huffman@41292
    56
instance "domain" \<subseteq> predomain
huffman@41292
    57
proof
huffman@41292
    58
  show "ep_pair liftemb (liftprj::udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>)"
huffman@41292
    59
    unfolding liftemb_eq liftprj_eq
huffman@41292
    60
    by (intro ep_pair_u_map ep_pair_emb_prj)
huffman@41292
    61
  show "cast\<cdot>LIFTDEFL('a) = liftemb oo (liftprj::udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>)"
huffman@41292
    62
    unfolding liftemb_eq liftprj_eq liftdefl_eq
huffman@41292
    63
    by (simp add: cast_pdefl cast_DEFL u_map_oo)
huffman@41292
    64
qed
huffman@41292
    65
huffman@41292
    66
text {*
huffman@41292
    67
  Constants @{const liftemb} and @{const liftprj} imply class predomain.
huffman@41292
    68
*}
huffman@41292
    69
huffman@41292
    70
setup {*
huffman@41292
    71
  fold Sign.add_const_constraint
huffman@41292
    72
  [(@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom u"}),
huffman@41292
    73
   (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::predomain u"}),
huffman@41292
    74
   (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom u defl"})]
huffman@41292
    75
*}
huffman@41292
    76
huffman@41292
    77
interpretation predomain: pcpo_ep_pair liftemb liftprj
huffman@41292
    78
  unfolding pcpo_ep_pair_def by (rule predomain_ep)
huffman@41292
    79
huffman@40497
    80
interpretation "domain": pcpo_ep_pair emb prj
huffman@41292
    81
  unfolding pcpo_ep_pair_def by (rule ep_pair_emb_prj)
huffman@33504
    82
huffman@40497
    83
lemmas emb_inverse = domain.e_inverse
huffman@40497
    84
lemmas emb_prj_below = domain.e_p_below
huffman@40497
    85
lemmas emb_eq_iff = domain.e_eq_iff
huffman@40497
    86
lemmas emb_strict = domain.e_strict
huffman@40497
    87
lemmas prj_strict = domain.p_strict
huffman@33504
    88
huffman@41286
    89
subsection {* Domains are bifinite *}
huffman@33587
    90
huffman@41286
    91
lemma approx_chain_ep_cast:
huffman@41292
    92
  assumes ep: "ep_pair (e::'a::pcpo \<rightarrow> 'b::bifinite) (p::'b \<rightarrow> 'a)"
huffman@41286
    93
  assumes cast_t: "cast\<cdot>t = e oo p"
huffman@41287
    94
  shows "\<exists>(a::nat \<Rightarrow> 'a::pcpo \<rightarrow> 'a). approx_chain a"
huffman@39985
    95
proof -
huffman@41286
    96
  interpret ep_pair e p by fact
huffman@39985
    97
  obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
huffman@41286
    98
  and t: "t = (\<Squnion>i. defl_principal (Y i))"
huffman@39989
    99
    by (rule defl.obtain_principal_chain)
huffman@41286
   100
  def approx \<equiv> "\<lambda>i. (p oo cast\<cdot>(defl_principal (Y i)) oo e) :: 'a \<rightarrow> 'a"
huffman@41286
   101
  have "approx_chain approx"
huffman@39985
   102
  proof (rule approx_chain.intro)
huffman@39985
   103
    show "chain (\<lambda>i. approx i)"
huffman@39985
   104
      unfolding approx_def by (simp add: Y)
huffman@39985
   105
    show "(\<Squnion>i. approx i) = ID"
huffman@39985
   106
      unfolding approx_def
huffman@41286
   107
      by (simp add: lub_distribs Y t [symmetric] cast_t cfun_eq_iff)
huffman@39985
   108
    show "\<And>i. finite_deflation (approx i)"
huffman@39985
   109
      unfolding approx_def
huffman@41286
   110
      apply (rule finite_deflation_p_d_e)
huffman@39985
   111
      apply (rule finite_deflation_cast)
huffman@39989
   112
      apply (rule defl.compact_principal)
huffman@39985
   113
      apply (rule below_trans [OF monofun_cfun_fun])
huffman@39985
   114
      apply (rule is_ub_thelub, simp add: Y)
huffman@41286
   115
      apply (simp add: lub_distribs Y t [symmetric] cast_t)
huffman@39985
   116
      done
huffman@39985
   117
  qed
huffman@41286
   118
  thus "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a" by - (rule exI)
huffman@33504
   119
qed
huffman@33504
   120
huffman@41286
   121
instance "domain" \<subseteq> bifinite
huffman@41286
   122
by default (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL])
huffman@41286
   123
huffman@41286
   124
instance predomain \<subseteq> profinite
huffman@41286
   125
by default (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])
huffman@41286
   126
huffman@41290
   127
subsection {* Universal domain ep-pairs *}
huffman@40484
   128
huffman@41290
   129
definition "u_emb = udom_emb (\<lambda>i. u_map\<cdot>(udom_approx i))"
huffman@41290
   130
definition "u_prj = udom_prj (\<lambda>i. u_map\<cdot>(udom_approx i))"
huffman@40484
   131
huffman@41290
   132
definition "prod_emb = udom_emb (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
huffman@41290
   133
definition "prod_prj = udom_prj (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
huffman@40484
   134
huffman@41290
   135
definition "sprod_emb = udom_emb (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
huffman@41290
   136
definition "sprod_prj = udom_prj (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
huffman@40484
   137
huffman@41290
   138
definition "ssum_emb = udom_emb (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
huffman@41290
   139
definition "ssum_prj = udom_prj (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
huffman@41290
   140
huffman@41290
   141
definition "sfun_emb = udom_emb (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
huffman@41290
   142
definition "sfun_prj = udom_prj (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
huffman@40484
   143
huffman@41290
   144
lemma ep_pair_u: "ep_pair u_emb u_prj"
huffman@41290
   145
  unfolding u_emb_def u_prj_def
huffman@41290
   146
  by (simp add: ep_pair_udom approx_chain_u_map)
huffman@40484
   147
huffman@41290
   148
lemma ep_pair_prod: "ep_pair prod_emb prod_prj"
huffman@41290
   149
  unfolding prod_emb_def prod_prj_def
huffman@41290
   150
  by (simp add: ep_pair_udom approx_chain_cprod_map)
huffman@40484
   151
huffman@41290
   152
lemma ep_pair_sprod: "ep_pair sprod_emb sprod_prj"
huffman@41290
   153
  unfolding sprod_emb_def sprod_prj_def
huffman@41290
   154
  by (simp add: ep_pair_udom approx_chain_sprod_map)
huffman@40484
   155
huffman@41290
   156
lemma ep_pair_ssum: "ep_pair ssum_emb ssum_prj"
huffman@41290
   157
  unfolding ssum_emb_def ssum_prj_def
huffman@41290
   158
  by (simp add: ep_pair_udom approx_chain_ssum_map)
huffman@40484
   159
huffman@41290
   160
lemma ep_pair_sfun: "ep_pair sfun_emb sfun_prj"
huffman@41290
   161
  unfolding sfun_emb_def sfun_prj_def
huffman@41290
   162
  by (simp add: ep_pair_udom approx_chain_sfun_map)
huffman@40484
   163
huffman@39985
   164
subsection {* Type combinators *}
huffman@39985
   165
huffman@41292
   166
definition u_defl :: "udom u defl \<rightarrow> udom defl"
huffman@41292
   167
  where "u_defl = defl_fun1 u_emb u_prj ID"
huffman@39985
   168
huffman@41290
   169
definition prod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
huffman@41290
   170
  where "prod_defl = defl_fun2 prod_emb prod_prj cprod_map"
huffman@33504
   171
huffman@41290
   172
definition sprod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
huffman@41290
   173
  where "sprod_defl = defl_fun2 sprod_emb sprod_prj sprod_map"
huffman@33504
   174
huffman@41290
   175
definition ssum_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
huffman@41290
   176
where "ssum_defl = defl_fun2 ssum_emb ssum_prj ssum_map"
huffman@40484
   177
huffman@41287
   178
definition sfun_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
huffman@41290
   179
  where "sfun_defl = defl_fun2 sfun_emb sfun_prj sfun_map"
huffman@40484
   180
huffman@40484
   181
lemma cast_u_defl:
huffman@41292
   182
  "cast\<cdot>(u_defl\<cdot>A) = u_emb oo cast\<cdot>A oo u_prj"
huffman@41292
   183
unfolding u_defl_def by (simp add: cast_defl_fun1 ep_pair_u)
huffman@40484
   184
huffman@40484
   185
lemma cast_prod_defl:
huffman@41290
   186
  "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) =
huffman@41290
   187
    prod_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo prod_prj"
huffman@41290
   188
using ep_pair_prod finite_deflation_cprod_map
huffman@40484
   189
unfolding prod_defl_def by (rule cast_defl_fun2)
huffman@40484
   190
huffman@40484
   191
lemma cast_sprod_defl:
huffman@40484
   192
  "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) =
huffman@41290
   193
    sprod_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo sprod_prj"
huffman@41290
   194
using ep_pair_sprod finite_deflation_sprod_map
huffman@40484
   195
unfolding sprod_defl_def by (rule cast_defl_fun2)
huffman@40484
   196
huffman@40484
   197
lemma cast_ssum_defl:
huffman@40484
   198
  "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) =
huffman@41290
   199
    ssum_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo ssum_prj"
huffman@41290
   200
using ep_pair_ssum finite_deflation_ssum_map
huffman@40484
   201
unfolding ssum_defl_def by (rule cast_defl_fun2)
huffman@40484
   202
huffman@41290
   203
lemma cast_sfun_defl:
huffman@41290
   204
  "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) =
huffman@41290
   205
    sfun_emb oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo sfun_prj"
huffman@41290
   206
using ep_pair_sfun finite_deflation_sfun_map
huffman@41290
   207
unfolding sfun_defl_def by (rule cast_defl_fun2)
huffman@41290
   208
huffman@40506
   209
subsection {* Class instance proofs *}
huffman@40506
   210
huffman@40506
   211
subsubsection {* Universal domain *}
huffman@39985
   212
huffman@41292
   213
instantiation udom :: "domain"
huffman@39985
   214
begin
huffman@39985
   215
huffman@39985
   216
definition [simp]:
huffman@39985
   217
  "emb = (ID :: udom \<rightarrow> udom)"
huffman@39985
   218
huffman@39985
   219
definition [simp]:
huffman@39985
   220
  "prj = (ID :: udom \<rightarrow> udom)"
huffman@25903
   221
huffman@33504
   222
definition
huffman@39989
   223
  "defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))"
huffman@33808
   224
huffman@40491
   225
definition
huffman@41292
   226
  "(liftemb :: udom u \<rightarrow> udom u) = u_map\<cdot>emb"
huffman@40491
   227
huffman@40491
   228
definition
huffman@41292
   229
  "(liftprj :: udom u \<rightarrow> udom u) = u_map\<cdot>prj"
huffman@40491
   230
huffman@41292
   231
definition
huffman@41292
   232
  "liftdefl (t::udom itself) = pdefl\<cdot>DEFL(udom)"
huffman@41292
   233
huffman@41292
   234
instance proof
huffman@39985
   235
  show "ep_pair emb (prj :: udom \<rightarrow> udom)"
huffman@39985
   236
    by (simp add: ep_pair.intro)
huffman@39989
   237
  show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> udom)"
huffman@39989
   238
    unfolding defl_udom_def
huffman@39985
   239
    apply (subst contlub_cfun_arg)
huffman@39985
   240
    apply (rule chainI)
huffman@39989
   241
    apply (rule defl.principal_mono)
huffman@39985
   242
    apply (simp add: below_fin_defl_def)
huffman@39985
   243
    apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
huffman@39985
   244
    apply (rule chainE)
huffman@39985
   245
    apply (rule chain_udom_approx)
huffman@39989
   246
    apply (subst cast_defl_principal)
huffman@39985
   247
    apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
huffman@33504
   248
    done
huffman@41292
   249
qed (fact liftemb_udom_def liftprj_udom_def liftdefl_udom_def)+
huffman@33504
   250
huffman@39985
   251
end
huffman@39985
   252
huffman@40506
   253
subsubsection {* Lifted cpo *}
huffman@40491
   254
huffman@41292
   255
instantiation u :: (predomain) "domain"
huffman@40491
   256
begin
huffman@40491
   257
huffman@40491
   258
definition
huffman@41292
   259
  "emb = u_emb oo liftemb"
huffman@40491
   260
huffman@40491
   261
definition
huffman@41292
   262
  "prj = liftprj oo u_prj"
huffman@40491
   263
huffman@40491
   264
definition
huffman@41292
   265
  "defl (t::'a u itself) = u_defl\<cdot>LIFTDEFL('a)"
huffman@40491
   266
huffman@40491
   267
definition
huffman@41292
   268
  "(liftemb :: 'a u u \<rightarrow> udom u) = u_map\<cdot>emb"
huffman@40491
   269
huffman@40491
   270
definition
huffman@41292
   271
  "(liftprj :: udom u \<rightarrow> 'a u u) = u_map\<cdot>prj"
huffman@40491
   272
huffman@40491
   273
definition
huffman@41292
   274
  "liftdefl (t::'a u itself) = pdefl\<cdot>DEFL('a u)"
huffman@40491
   275
huffman@41292
   276
instance proof
huffman@40491
   277
  show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
huffman@40491
   278
    unfolding emb_u_def prj_u_def
huffman@41292
   279
    by (intro ep_pair_comp ep_pair_u predomain_ep)
huffman@40491
   280
  show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
huffman@40491
   281
    unfolding emb_u_def prj_u_def defl_u_def
huffman@41292
   282
    by (simp add: cast_u_defl cast_liftdefl assoc_oo)
huffman@41292
   283
qed (fact liftemb_u_def liftprj_u_def liftdefl_u_def)+
huffman@40491
   284
huffman@40491
   285
end
huffman@40491
   286
huffman@41292
   287
lemma DEFL_u: "DEFL('a::predomain u) = u_defl\<cdot>LIFTDEFL('a)"
huffman@40491
   288
by (rule defl_u_def)
huffman@40491
   289
huffman@40592
   290
subsubsection {* Strict function space *}
huffman@39985
   291
huffman@41292
   292
instantiation sfun :: ("domain", "domain") "domain"
huffman@39985
   293
begin
huffman@39985
   294
huffman@39985
   295
definition
huffman@41290
   296
  "emb = sfun_emb oo sfun_map\<cdot>prj\<cdot>emb"
huffman@40592
   297
huffman@40592
   298
definition
huffman@41290
   299
  "prj = sfun_map\<cdot>emb\<cdot>prj oo sfun_prj"
huffman@40592
   300
huffman@40592
   301
definition
huffman@40592
   302
  "defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
huffman@40592
   303
huffman@40592
   304
definition
huffman@41292
   305
  "(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
huffman@39985
   306
huffman@39985
   307
definition
huffman@41292
   308
  "(liftprj :: udom u \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj"
huffman@40592
   309
huffman@41292
   310
definition
huffman@41292
   311
  "liftdefl (t::('a \<rightarrow>! 'b) itself) = pdefl\<cdot>DEFL('a \<rightarrow>! 'b)"
huffman@41292
   312
huffman@41292
   313
instance proof
huffman@40592
   314
  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
huffman@40592
   315
    unfolding emb_sfun_def prj_sfun_def
huffman@41290
   316
    by (intro ep_pair_comp ep_pair_sfun ep_pair_sfun_map ep_pair_emb_prj)
huffman@40592
   317
  show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
huffman@40592
   318
    unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
huffman@40592
   319
    by (simp add: cast_DEFL oo_def sfun_eq_iff sfun_map_map)
huffman@41292
   320
qed (fact liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def)+
huffman@40592
   321
huffman@40592
   322
end
huffman@40592
   323
huffman@40592
   324
lemma DEFL_sfun:
huffman@40592
   325
  "DEFL('a::domain \<rightarrow>! 'b::domain) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
huffman@40592
   326
by (rule defl_sfun_def)
huffman@40592
   327
huffman@40592
   328
subsubsection {* Continuous function space *}
huffman@40592
   329
huffman@41292
   330
instantiation cfun :: (predomain, "domain") "domain"
huffman@40592
   331
begin
huffman@40592
   332
huffman@40592
   333
definition
huffman@40830
   334
  "emb = emb oo encode_cfun"
huffman@40592
   335
huffman@40592
   336
definition
huffman@40830
   337
  "prj = decode_cfun oo prj"
huffman@40592
   338
huffman@40592
   339
definition
huffman@40830
   340
  "defl (t::('a \<rightarrow> 'b) itself) = DEFL('a u \<rightarrow>! 'b)"
huffman@39985
   341
huffman@40491
   342
definition
huffman@41292
   343
  "(liftemb :: ('a \<rightarrow> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
huffman@40491
   344
huffman@40491
   345
definition
huffman@41292
   346
  "(liftprj :: udom u \<rightarrow> ('a \<rightarrow> 'b) u) = u_map\<cdot>prj"
huffman@40491
   347
huffman@41292
   348
definition
huffman@41292
   349
  "liftdefl (t::('a \<rightarrow> 'b) itself) = pdefl\<cdot>DEFL('a \<rightarrow> 'b)"
huffman@41292
   350
huffman@41292
   351
instance proof
huffman@40592
   352
  have "ep_pair encode_cfun decode_cfun"
huffman@40592
   353
    by (rule ep_pair.intro, simp_all)
huffman@40592
   354
  thus "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
huffman@39985
   355
    unfolding emb_cfun_def prj_cfun_def
huffman@40830
   356
    using ep_pair_emb_prj by (rule ep_pair_comp)
huffman@39989
   357
  show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
huffman@40830
   358
    unfolding emb_cfun_def prj_cfun_def defl_cfun_def
huffman@40830
   359
    by (simp add: cast_DEFL cfcomp1)
huffman@41292
   360
qed (fact liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def)+
huffman@25903
   361
huffman@39985
   362
end
huffman@33504
   363
huffman@39989
   364
lemma DEFL_cfun:
huffman@40830
   365
  "DEFL('a::predomain \<rightarrow> 'b::domain) = DEFL('a u \<rightarrow>! 'b)"
huffman@39989
   366
by (rule defl_cfun_def)
brianh@39972
   367
huffman@40506
   368
subsubsection {* Strict product *}
huffman@39987
   369
huffman@41292
   370
instantiation sprod :: ("domain", "domain") "domain"
huffman@39987
   371
begin
huffman@39987
   372
huffman@39987
   373
definition
huffman@41290
   374
  "emb = sprod_emb oo sprod_map\<cdot>emb\<cdot>emb"
huffman@39987
   375
huffman@39987
   376
definition
huffman@41290
   377
  "prj = sprod_map\<cdot>prj\<cdot>prj oo sprod_prj"
huffman@39987
   378
huffman@39987
   379
definition
huffman@39989
   380
  "defl (t::('a \<otimes> 'b) itself) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
huffman@39987
   381
huffman@40491
   382
definition
huffman@41292
   383
  "(liftemb :: ('a \<otimes> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
huffman@40491
   384
huffman@40491
   385
definition
huffman@41292
   386
  "(liftprj :: udom u \<rightarrow> ('a \<otimes> 'b) u) = u_map\<cdot>prj"
huffman@40491
   387
huffman@41292
   388
definition
huffman@41292
   389
  "liftdefl (t::('a \<otimes> 'b) itself) = pdefl\<cdot>DEFL('a \<otimes> 'b)"
huffman@41292
   390
huffman@41292
   391
instance proof
huffman@39987
   392
  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
huffman@39987
   393
    unfolding emb_sprod_def prj_sprod_def
huffman@41290
   394
    by (intro ep_pair_comp ep_pair_sprod ep_pair_sprod_map ep_pair_emb_prj)
huffman@39989
   395
  show "cast\<cdot>DEFL('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
huffman@39989
   396
    unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl
huffman@40002
   397
    by (simp add: cast_DEFL oo_def cfun_eq_iff sprod_map_map)
huffman@41292
   398
qed (fact liftemb_sprod_def liftprj_sprod_def liftdefl_sprod_def)+
huffman@39987
   399
huffman@39987
   400
end
huffman@39987
   401
huffman@39989
   402
lemma DEFL_sprod:
huffman@40497
   403
  "DEFL('a::domain \<otimes> 'b::domain) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
huffman@39989
   404
by (rule defl_sprod_def)
huffman@39987
   405
huffman@40830
   406
subsubsection {* Cartesian product *}
huffman@40830
   407
huffman@41292
   408
definition prod_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
huffman@41292
   409
  where "prod_liftdefl = defl_fun2 (u_map\<cdot>prod_emb oo decode_prod_u)
huffman@41292
   410
    (encode_prod_u oo u_map\<cdot>prod_prj) sprod_map"
huffman@41292
   411
huffman@41292
   412
lemma cast_prod_liftdefl:
huffman@41292
   413
  "cast\<cdot>(prod_liftdefl\<cdot>a\<cdot>b) =
huffman@41292
   414
    (u_map\<cdot>prod_emb oo decode_prod_u) oo sprod_map\<cdot>(cast\<cdot>a)\<cdot>(cast\<cdot>b) oo
huffman@41292
   415
      (encode_prod_u oo u_map\<cdot>prod_prj)"
huffman@41292
   416
unfolding prod_liftdefl_def
huffman@41292
   417
apply (rule cast_defl_fun2)
huffman@41292
   418
apply (intro ep_pair_comp ep_pair_u_map ep_pair_prod)
huffman@41292
   419
apply (simp add: ep_pair.intro)
huffman@41292
   420
apply (erule (1) finite_deflation_sprod_map)
huffman@41292
   421
done
huffman@41292
   422
huffman@40830
   423
instantiation prod :: (predomain, predomain) predomain
huffman@40830
   424
begin
huffman@40830
   425
huffman@40830
   426
definition
huffman@41292
   427
  "liftemb = (u_map\<cdot>prod_emb oo decode_prod_u) oo
huffman@41292
   428
    (sprod_map\<cdot>liftemb\<cdot>liftemb oo encode_prod_u)"
huffman@40830
   429
huffman@40830
   430
definition
huffman@41292
   431
  "liftprj = (decode_prod_u oo sprod_map\<cdot>liftprj\<cdot>liftprj) oo
huffman@41292
   432
    (encode_prod_u oo u_map\<cdot>prod_prj)"
huffman@40830
   433
huffman@40830
   434
definition
huffman@41292
   435
  "liftdefl (t::('a \<times> 'b) itself) = prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
huffman@40830
   436
huffman@40830
   437
instance proof
huffman@41292
   438
  show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a \<times> 'b) u)"
huffman@40830
   439
    unfolding liftemb_prod_def liftprj_prod_def
huffman@41292
   440
    by (intro ep_pair_comp ep_pair_sprod_map ep_pair_u_map
huffman@41292
   441
       ep_pair_prod predomain_ep, simp_all add: ep_pair.intro)
huffman@41292
   442
  show "cast\<cdot>LIFTDEFL('a \<times> 'b) = liftemb oo (liftprj :: udom u \<rightarrow> ('a \<times> 'b) u)"
huffman@40830
   443
    unfolding liftemb_prod_def liftprj_prod_def liftdefl_prod_def
huffman@41292
   444
    by (simp add: cast_prod_liftdefl cast_liftdefl cfcomp1 sprod_map_map)
huffman@40830
   445
qed
huffman@40830
   446
huffman@40830
   447
end
huffman@40830
   448
huffman@40830
   449
instantiation prod :: ("domain", "domain") "domain"
huffman@40830
   450
begin
huffman@40830
   451
huffman@40830
   452
definition
huffman@41290
   453
  "emb = prod_emb oo cprod_map\<cdot>emb\<cdot>emb"
huffman@40830
   454
huffman@40830
   455
definition
huffman@41290
   456
  "prj = cprod_map\<cdot>prj\<cdot>prj oo prod_prj"
huffman@40830
   457
huffman@40830
   458
definition
huffman@40830
   459
  "defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
huffman@40830
   460
huffman@40830
   461
instance proof
huffman@41292
   462
  show 1: "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
huffman@40830
   463
    unfolding emb_prod_def prj_prod_def
huffman@41290
   464
    by (intro ep_pair_comp ep_pair_prod ep_pair_cprod_map ep_pair_emb_prj)
huffman@41292
   465
  show 2: "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
huffman@40830
   466
    unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
huffman@40830
   467
    by (simp add: cast_DEFL oo_def cfun_eq_iff cprod_map_map)
huffman@41292
   468
  show 3: "liftemb = u_map\<cdot>(emb :: 'a \<times> 'b \<rightarrow> udom)"
huffman@41292
   469
    unfolding emb_prod_def liftemb_prod_def liftemb_eq
huffman@41292
   470
    unfolding encode_prod_u_def decode_prod_u_def
huffman@41292
   471
    by (rule cfun_eqI, case_tac x, simp, clarsimp)
huffman@41292
   472
  show 4: "liftprj = u_map\<cdot>(prj :: udom \<rightarrow> 'a \<times> 'b)"
huffman@41292
   473
    unfolding prj_prod_def liftprj_prod_def liftprj_eq
huffman@41292
   474
    unfolding encode_prod_u_def decode_prod_u_def
huffman@41292
   475
    apply (rule cfun_eqI, case_tac x, simp)
huffman@41292
   476
    apply (rename_tac y, case_tac "prod_prj\<cdot>y", simp)
huffman@41292
   477
    done
huffman@41292
   478
  show 5: "LIFTDEFL('a \<times> 'b) = pdefl\<cdot>DEFL('a \<times> 'b)"
huffman@41292
   479
    by (rule cast_eq_imp_eq)
huffman@41292
   480
      (simp add: cast_liftdefl cast_pdefl cast_DEFL 2 3 4 u_map_oo)
huffman@40830
   481
qed
huffman@40830
   482
huffman@40830
   483
end
huffman@40830
   484
huffman@40830
   485
lemma DEFL_prod:
huffman@40830
   486
  "DEFL('a::domain \<times> 'b::domain) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
huffman@40830
   487
by (rule defl_prod_def)
huffman@40830
   488
huffman@40830
   489
lemma LIFTDEFL_prod:
huffman@41292
   490
  "LIFTDEFL('a::predomain \<times> 'b::predomain) =
huffman@41292
   491
    prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
huffman@40830
   492
by (rule liftdefl_prod_def)
huffman@40830
   493
huffman@41034
   494
subsubsection {* Unit type *}
huffman@41034
   495
huffman@41292
   496
instantiation unit :: "domain"
huffman@41034
   497
begin
huffman@41034
   498
huffman@41034
   499
definition
huffman@41034
   500
  "emb = (\<bottom> :: unit \<rightarrow> udom)"
huffman@41034
   501
huffman@41034
   502
definition
huffman@41034
   503
  "prj = (\<bottom> :: udom \<rightarrow> unit)"
huffman@41034
   504
huffman@41034
   505
definition
huffman@41034
   506
  "defl (t::unit itself) = \<bottom>"
huffman@41034
   507
huffman@41034
   508
definition
huffman@41292
   509
  "(liftemb :: unit u \<rightarrow> udom u) = u_map\<cdot>emb"
huffman@41034
   510
huffman@41034
   511
definition
huffman@41292
   512
  "(liftprj :: udom u \<rightarrow> unit u) = u_map\<cdot>prj"
huffman@41034
   513
huffman@41292
   514
definition
huffman@41292
   515
  "liftdefl (t::unit itself) = pdefl\<cdot>DEFL(unit)"
huffman@41292
   516
huffman@41292
   517
instance proof
huffman@41034
   518
  show "ep_pair emb (prj :: udom \<rightarrow> unit)"
huffman@41034
   519
    unfolding emb_unit_def prj_unit_def
huffman@41034
   520
    by (simp add: ep_pair.intro)
huffman@41034
   521
  show "cast\<cdot>DEFL(unit) = emb oo (prj :: udom \<rightarrow> unit)"
huffman@41034
   522
    unfolding emb_unit_def prj_unit_def defl_unit_def by simp
huffman@41292
   523
qed (fact liftemb_unit_def liftprj_unit_def liftdefl_unit_def)+
huffman@41034
   524
huffman@41034
   525
end
huffman@41034
   526
huffman@40506
   527
subsubsection {* Discrete cpo *}
huffman@39987
   528
huffman@40491
   529
instantiation discr :: (countable) predomain
huffman@39987
   530
begin
huffman@39987
   531
huffman@39987
   532
definition
huffman@41292
   533
  "(liftemb :: 'a discr u \<rightarrow> udom u) = strictify\<cdot>up oo udom_emb discr_approx"
huffman@39987
   534
huffman@39987
   535
definition
huffman@41292
   536
  "(liftprj :: udom u \<rightarrow> 'a discr u) = udom_prj discr_approx oo fup\<cdot>ID"
huffman@39987
   537
huffman@39987
   538
definition
huffman@40491
   539
  "liftdefl (t::'a discr itself) =
huffman@41292
   540
    (\<Squnion>i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo (liftprj::udom u \<rightarrow> 'a discr u))))"
huffman@39987
   541
huffman@39987
   542
instance proof
huffman@41292
   543
  show 1: "ep_pair liftemb (liftprj :: udom u \<rightarrow> 'a discr u)"
huffman@40491
   544
    unfolding liftemb_discr_def liftprj_discr_def
huffman@41292
   545
    apply (intro ep_pair_comp ep_pair_udom [OF discr_approx])
huffman@41292
   546
    apply (rule ep_pair.intro)
huffman@41292
   547
    apply (simp add: strictify_conv_if)
huffman@41292
   548
    apply (case_tac y, simp, simp add: strictify_conv_if)
huffman@41292
   549
    done
huffman@41292
   550
  show "cast\<cdot>LIFTDEFL('a discr) = liftemb oo (liftprj :: udom u \<rightarrow> 'a discr u)"
huffman@41292
   551
    unfolding liftdefl_discr_def
huffman@39987
   552
    apply (subst contlub_cfun_arg)
huffman@39987
   553
    apply (rule chainI)
huffman@39989
   554
    apply (rule defl.principal_mono)
huffman@39987
   555
    apply (simp add: below_fin_defl_def)
huffman@40491
   556
    apply (simp add: Abs_fin_defl_inverse
huffman@41292
   557
        ep_pair.finite_deflation_e_d_p [OF 1]
huffman@40491
   558
        approx_chain.finite_deflation_approx [OF discr_approx])
huffman@39987
   559
    apply (intro monofun_cfun below_refl)
huffman@39987
   560
    apply (rule chainE)
huffman@40491
   561
    apply (rule chain_discr_approx)
huffman@39989
   562
    apply (subst cast_defl_principal)
huffman@40491
   563
    apply (simp add: Abs_fin_defl_inverse
huffman@41292
   564
        ep_pair.finite_deflation_e_d_p [OF 1]
huffman@40491
   565
        approx_chain.finite_deflation_approx [OF discr_approx])
huffman@40491
   566
    apply (simp add: lub_distribs)
huffman@39987
   567
    done
huffman@39987
   568
qed
huffman@39987
   569
huffman@39987
   570
end
huffman@39987
   571
huffman@40506
   572
subsubsection {* Strict sum *}
huffman@39987
   573
huffman@41292
   574
instantiation ssum :: ("domain", "domain") "domain"
huffman@39987
   575
begin
huffman@39987
   576
huffman@39987
   577
definition
huffman@41290
   578
  "emb = ssum_emb oo ssum_map\<cdot>emb\<cdot>emb"
huffman@39987
   579
huffman@39987
   580
definition
huffman@41290
   581
  "prj = ssum_map\<cdot>prj\<cdot>prj oo ssum_prj"
huffman@39987
   582
huffman@39987
   583
definition
huffman@39989
   584
  "defl (t::('a \<oplus> 'b) itself) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
huffman@39987
   585
huffman@40491
   586
definition
huffman@41292
   587
  "(liftemb :: ('a \<oplus> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
huffman@40491
   588
huffman@40491
   589
definition
huffman@41292
   590
  "(liftprj :: udom u \<rightarrow> ('a \<oplus> 'b) u) = u_map\<cdot>prj"
huffman@40491
   591
huffman@41292
   592
definition
huffman@41292
   593
  "liftdefl (t::('a \<oplus> 'b) itself) = pdefl\<cdot>DEFL('a \<oplus> 'b)"
huffman@41292
   594
huffman@41292
   595
instance proof
huffman@39987
   596
  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
huffman@39987
   597
    unfolding emb_ssum_def prj_ssum_def
huffman@41290
   598
    by (intro ep_pair_comp ep_pair_ssum ep_pair_ssum_map ep_pair_emb_prj)
huffman@39989
   599
  show "cast\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
huffman@39989
   600
    unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl
huffman@40002
   601
    by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map)
huffman@41292
   602
qed (fact liftemb_ssum_def liftprj_ssum_def liftdefl_ssum_def)+
huffman@39987
   603
huffman@39987
   604
end
huffman@39987
   605
huffman@39989
   606
lemma DEFL_ssum:
huffman@40497
   607
  "DEFL('a::domain \<oplus> 'b::domain) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
huffman@39989
   608
by (rule defl_ssum_def)
huffman@39987
   609
huffman@40506
   610
subsubsection {* Lifted HOL type *}
huffman@40491
   611
huffman@41292
   612
instantiation lift :: (countable) "domain"
huffman@40491
   613
begin
huffman@40491
   614
huffman@40491
   615
definition
huffman@40491
   616
  "emb = emb oo (\<Lambda> x. Rep_lift x)"
huffman@40491
   617
huffman@40491
   618
definition
huffman@40491
   619
  "prj = (\<Lambda> y. Abs_lift y) oo prj"
huffman@40491
   620
huffman@40491
   621
definition
huffman@40491
   622
  "defl (t::'a lift itself) = DEFL('a discr u)"
huffman@40491
   623
huffman@40491
   624
definition
huffman@41292
   625
  "(liftemb :: 'a lift u \<rightarrow> udom u) = u_map\<cdot>emb"
huffman@40491
   626
huffman@40491
   627
definition
huffman@41292
   628
  "(liftprj :: udom u \<rightarrow> 'a lift u) = u_map\<cdot>prj"
huffman@40491
   629
huffman@41292
   630
definition
huffman@41292
   631
  "liftdefl (t::'a lift itself) = pdefl\<cdot>DEFL('a lift)"
huffman@41292
   632
huffman@41292
   633
instance proof
huffman@40491
   634
  note [simp] = cont_Rep_lift cont_Abs_lift Rep_lift_inverse Abs_lift_inverse
huffman@40491
   635
  have "ep_pair (\<Lambda>(x::'a lift). Rep_lift x) (\<Lambda> y. Abs_lift y)"
huffman@40491
   636
    by (simp add: ep_pair_def)
huffman@40491
   637
  thus "ep_pair emb (prj :: udom \<rightarrow> 'a lift)"
huffman@40491
   638
    unfolding emb_lift_def prj_lift_def
huffman@40491
   639
    using ep_pair_emb_prj by (rule ep_pair_comp)
huffman@40491
   640
  show "cast\<cdot>DEFL('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
huffman@40491
   641
    unfolding emb_lift_def prj_lift_def defl_lift_def cast_DEFL
huffman@40491
   642
    by (simp add: cfcomp1)
huffman@41292
   643
qed (fact liftemb_lift_def liftprj_lift_def liftdefl_lift_def)+
huffman@40491
   644
huffman@39987
   645
end
huffman@40491
   646
huffman@40491
   647
end