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