src/HOLCF/Bifinite.thy
author huffman
Thu Oct 07 13:54:43 2010 -0700 (2010-10-07)
changeset 39985 310f98585107
parent 39974 b525988432e9
child 39986 38677db30cad
permissions -rw-r--r--
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman@25903
     1
(*  Title:      HOLCF/Bifinite.thy
huffman@25903
     2
    Author:     Brian Huffman
huffman@25903
     3
*)
huffman@25903
     4
huffman@39985
     5
header {* Bifinite domains *}
huffman@25903
     6
huffman@25903
     7
theory Bifinite
huffman@39985
     8
imports Algebraic
huffman@25903
     9
begin
huffman@25903
    10
huffman@39985
    11
subsection {* Class of SFP domains *}
huffman@39985
    12
huffman@39985
    13
text {*
huffman@39985
    14
  We define a SFP domain as a pcpo that is isomorphic to some
huffman@39985
    15
  algebraic deflation over the universal domain.
huffman@39985
    16
*}
huffman@39985
    17
huffman@39985
    18
class sfp = pcpo +
huffman@39985
    19
  fixes emb :: "'a::pcpo \<rightarrow> udom"
huffman@39985
    20
  fixes prj :: "udom \<rightarrow> 'a::pcpo"
huffman@39985
    21
  fixes sfp :: "'a itself \<Rightarrow> sfp"
huffman@39985
    22
  assumes ep_pair_emb_prj: "ep_pair emb prj"
huffman@39985
    23
  assumes cast_SFP: "cast\<cdot>(sfp TYPE('a)) = emb oo prj"
huffman@31113
    24
huffman@39985
    25
syntax "_SFP" :: "type \<Rightarrow> sfp"  ("(1SFP/(1'(_')))")
huffman@39985
    26
translations "SFP('t)" \<rightleftharpoons> "CONST sfp TYPE('t)"
huffman@39985
    27
huffman@39985
    28
interpretation sfp:
huffman@39985
    29
  pcpo_ep_pair "emb :: 'a::sfp \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::sfp"
huffman@39985
    30
  unfolding pcpo_ep_pair_def
huffman@39985
    31
  by (rule ep_pair_emb_prj)
huffman@33504
    32
huffman@39985
    33
lemmas emb_inverse = sfp.e_inverse
huffman@39985
    34
lemmas emb_prj_below = sfp.e_p_below
huffman@39985
    35
lemmas emb_eq_iff = sfp.e_eq_iff
huffman@39985
    36
lemmas emb_strict = sfp.e_strict
huffman@39985
    37
lemmas prj_strict = sfp.p_strict
huffman@33504
    38
huffman@39985
    39
subsection {* SFP domains have a countable compact basis *}
huffman@33808
    40
huffman@39985
    41
text {*
huffman@39985
    42
  Eventually it should be possible to generalize this to an unpointed
huffman@39985
    43
  variant of the sfp class.
huffman@39985
    44
*}
huffman@33587
    45
huffman@39985
    46
interpretation compact_basis:
huffman@39985
    47
  ideal_completion below Rep_compact_basis "approximants::'a::sfp \<Rightarrow> _"
huffman@39985
    48
proof -
huffman@39985
    49
  obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
huffman@39985
    50
  and SFP: "SFP('a) = (\<Squnion>i. sfp_principal (Y i))"
huffman@39985
    51
    by (rule sfp.obtain_principal_chain)
huffman@39985
    52
  def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(sfp_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a"
huffman@39985
    53
  interpret sfp_approx: approx_chain approx
huffman@39985
    54
  proof (rule approx_chain.intro)
huffman@39985
    55
    show "chain (\<lambda>i. approx i)"
huffman@39985
    56
      unfolding approx_def by (simp add: Y)
huffman@39985
    57
    show "(\<Squnion>i. approx i) = ID"
huffman@39985
    58
      unfolding approx_def
huffman@39985
    59
      by (simp add: lub_distribs Y SFP [symmetric] cast_SFP expand_cfun_eq)
huffman@39985
    60
    show "\<And>i. finite_deflation (approx i)"
huffman@39985
    61
      unfolding approx_def
huffman@39985
    62
      apply (rule sfp.finite_deflation_p_d_e)
huffman@39985
    63
      apply (rule finite_deflation_cast)
huffman@39985
    64
      apply (rule sfp.compact_principal)
huffman@39985
    65
      apply (rule below_trans [OF monofun_cfun_fun])
huffman@39985
    66
      apply (rule is_ub_thelub, simp add: Y)
huffman@39985
    67
      apply (simp add: lub_distribs Y SFP [symmetric] cast_SFP)
huffman@39985
    68
      done
huffman@39985
    69
  qed
huffman@39985
    70
  (* FIXME: why does show ?thesis fail here? *)
huffman@39985
    71
  show "ideal_completion below Rep_compact_basis (approximants::'a \<Rightarrow> _)" ..
huffman@33504
    72
qed
huffman@33504
    73
huffman@39985
    74
subsection {* Type combinators *}
huffman@39985
    75
huffman@39985
    76
definition
huffman@39985
    77
  sfp_fun1 ::
huffman@39985
    78
    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (sfp \<rightarrow> sfp)"
huffman@39985
    79
where
huffman@39985
    80
  "sfp_fun1 approx f =
huffman@39985
    81
    sfp.basis_fun (\<lambda>a.
huffman@39985
    82
      sfp_principal (Abs_fin_defl
huffman@39985
    83
        (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)))"
huffman@39985
    84
huffman@39985
    85
definition
huffman@39985
    86
  sfp_fun2 ::
huffman@39985
    87
    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
huffman@39985
    88
      \<Rightarrow> (sfp \<rightarrow> sfp \<rightarrow> sfp)"
huffman@39985
    89
where
huffman@39985
    90
  "sfp_fun2 approx f =
huffman@39985
    91
    sfp.basis_fun (\<lambda>a.
huffman@39985
    92
      sfp.basis_fun (\<lambda>b.
huffman@39985
    93
        sfp_principal (Abs_fin_defl
huffman@39985
    94
          (udom_emb approx oo
huffman@39985
    95
            f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx))))"
huffman@33504
    96
huffman@39985
    97
lemma cast_sfp_fun1:
huffman@39985
    98
  assumes approx: "approx_chain approx"
huffman@39985
    99
  assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
huffman@39985
   100
  shows "cast\<cdot>(sfp_fun1 approx f\<cdot>A) = udom_emb approx oo f\<cdot>(cast\<cdot>A) oo udom_prj approx"
huffman@39985
   101
proof -
huffman@39985
   102
  have 1: "\<And>a. finite_deflation
huffman@39985
   103
        (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)"
huffman@39985
   104
    apply (rule ep_pair.finite_deflation_e_d_p)
huffman@39985
   105
    apply (rule approx_chain.ep_pair_udom [OF approx])
huffman@39985
   106
    apply (rule f, rule finite_deflation_Rep_fin_defl)
huffman@39985
   107
    done
huffman@39985
   108
  show ?thesis
huffman@39985
   109
    by (induct A rule: sfp.principal_induct, simp)
huffman@39985
   110
       (simp only: sfp_fun1_def
huffman@39985
   111
                   sfp.basis_fun_principal
huffman@39985
   112
                   sfp.basis_fun_mono
huffman@39985
   113
                   sfp.principal_mono
huffman@39985
   114
                   Abs_fin_defl_mono [OF 1 1]
huffman@39985
   115
                   monofun_cfun below_refl
huffman@39985
   116
                   Rep_fin_defl_mono
huffman@39985
   117
                   cast_sfp_principal
huffman@39985
   118
                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
huffman@33504
   119
qed
huffman@33504
   120
huffman@39985
   121
lemma cast_sfp_fun2:
huffman@39985
   122
  assumes approx: "approx_chain approx"
huffman@39985
   123
  assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
huffman@39985
   124
                finite_deflation (f\<cdot>a\<cdot>b)"
huffman@39985
   125
  shows "cast\<cdot>(sfp_fun2 approx f\<cdot>A\<cdot>B) =
huffman@39985
   126
    udom_emb approx oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj approx"
huffman@39985
   127
proof -
huffman@39985
   128
  have 1: "\<And>a b. finite_deflation (udom_emb approx oo
huffman@39985
   129
      f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx)"
huffman@39985
   130
    apply (rule ep_pair.finite_deflation_e_d_p)
huffman@39985
   131
    apply (rule ep_pair_udom [OF approx])
huffman@39985
   132
    apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
huffman@39985
   133
    done
huffman@39985
   134
  show ?thesis
huffman@39985
   135
    by (induct A B rule: sfp.principal_induct2, simp, simp)
huffman@39985
   136
       (simp only: sfp_fun2_def
huffman@39985
   137
                   sfp.basis_fun_principal
huffman@39985
   138
                   sfp.basis_fun_mono
huffman@39985
   139
                   sfp.principal_mono
huffman@39985
   140
                   Abs_fin_defl_mono [OF 1 1]
huffman@39985
   141
                   monofun_cfun below_refl
huffman@39985
   142
                   Rep_fin_defl_mono
huffman@39985
   143
                   cast_sfp_principal
huffman@39985
   144
                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
huffman@39985
   145
qed
huffman@39985
   146
huffman@39985
   147
subsection {* Instance for universal domain type *}
huffman@39985
   148
huffman@39985
   149
instantiation udom :: sfp
huffman@39985
   150
begin
huffman@39985
   151
huffman@39985
   152
definition [simp]:
huffman@39985
   153
  "emb = (ID :: udom \<rightarrow> udom)"
huffman@39985
   154
huffman@39985
   155
definition [simp]:
huffman@39985
   156
  "prj = (ID :: udom \<rightarrow> udom)"
huffman@25903
   157
huffman@33504
   158
definition
huffman@39985
   159
  "sfp (t::udom itself) = (\<Squnion>i. sfp_principal (Abs_fin_defl (udom_approx i)))"
huffman@33808
   160
huffman@39985
   161
instance proof
huffman@39985
   162
  show "ep_pair emb (prj :: udom \<rightarrow> udom)"
huffman@39985
   163
    by (simp add: ep_pair.intro)
huffman@39985
   164
next
huffman@39985
   165
  show "cast\<cdot>SFP(udom) = emb oo (prj :: udom \<rightarrow> udom)"
huffman@39985
   166
    unfolding sfp_udom_def
huffman@39985
   167
    apply (subst contlub_cfun_arg)
huffman@39985
   168
    apply (rule chainI)
huffman@39985
   169
    apply (rule sfp.principal_mono)
huffman@39985
   170
    apply (simp add: below_fin_defl_def)
huffman@39985
   171
    apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
huffman@39985
   172
    apply (rule chainE)
huffman@39985
   173
    apply (rule chain_udom_approx)
huffman@39985
   174
    apply (subst cast_sfp_principal)
huffman@39985
   175
    apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
huffman@33504
   176
    done
huffman@33504
   177
qed
huffman@33504
   178
huffman@39985
   179
end
huffman@39985
   180
huffman@39985
   181
subsection {* Instance for continuous function space *}
huffman@39985
   182
huffman@39985
   183
definition
huffman@39985
   184
  cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
huffman@39985
   185
where
huffman@39985
   186
  "cfun_approx = (\<lambda>i. cfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
huffman@39985
   187
huffman@39985
   188
lemma cfun_approx: "approx_chain cfun_approx"
huffman@39985
   189
proof (rule approx_chain.intro)
huffman@39985
   190
  show "chain (\<lambda>i. cfun_approx i)"
huffman@39985
   191
    unfolding cfun_approx_def by simp
huffman@39985
   192
  show "(\<Squnion>i. cfun_approx i) = ID"
huffman@39985
   193
    unfolding cfun_approx_def
huffman@39985
   194
    by (simp add: lub_distribs cfun_map_ID)
huffman@39985
   195
  show "\<And>i. finite_deflation (cfun_approx i)"
huffman@39985
   196
    unfolding cfun_approx_def
huffman@39985
   197
    by (intro finite_deflation_cfun_map finite_deflation_udom_approx)
huffman@33504
   198
qed
huffman@33504
   199
huffman@39985
   200
definition cfun_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
huffman@39985
   201
where "cfun_sfp = sfp_fun2 cfun_approx cfun_map"
huffman@39985
   202
huffman@39985
   203
lemma cast_cfun_sfp:
huffman@39985
   204
  "cast\<cdot>(cfun_sfp\<cdot>A\<cdot>B) =
huffman@39985
   205
    udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
huffman@39985
   206
unfolding cfun_sfp_def
huffman@39985
   207
apply (rule cast_sfp_fun2 [OF cfun_approx])
huffman@39985
   208
apply (erule (1) finite_deflation_cfun_map)
huffman@39985
   209
done
huffman@39985
   210
huffman@39985
   211
instantiation cfun :: (sfp, sfp) sfp
huffman@39985
   212
begin
huffman@39985
   213
huffman@39985
   214
definition
huffman@39985
   215
  "emb = udom_emb cfun_approx oo cfun_map\<cdot>prj\<cdot>emb"
huffman@39985
   216
huffman@39985
   217
definition
huffman@39985
   218
  "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj cfun_approx"
huffman@39985
   219
huffman@39985
   220
definition
huffman@39985
   221
  "sfp (t::('a \<rightarrow> 'b) itself) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
huffman@39985
   222
huffman@39985
   223
instance proof
huffman@39985
   224
  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
huffman@39985
   225
    unfolding emb_cfun_def prj_cfun_def
huffman@39985
   226
    using ep_pair_udom [OF cfun_approx]
huffman@39985
   227
    by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj)
huffman@39985
   228
next
huffman@39985
   229
  show "cast\<cdot>SFP('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
huffman@39985
   230
    unfolding emb_cfun_def prj_cfun_def sfp_cfun_def cast_cfun_sfp
huffman@39985
   231
    by (simp add: cast_SFP oo_def expand_cfun_eq cfun_map_map)
huffman@27402
   232
qed
huffman@25903
   233
huffman@39985
   234
end
huffman@33504
   235
huffman@39985
   236
lemma SFP_cfun: "SFP('a::sfp \<rightarrow> 'b::sfp) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
huffman@39985
   237
by (rule sfp_cfun_def)
brianh@39972
   238
huffman@26962
   239
end