src/HOL/HOLCF/Bifinite.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 66453 cc19f7ca2ed6
child 67312 0d25e02759b7
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/Bifinite.thy
huffman@41286
     2
    Author:     Brian Huffman
huffman@41286
     3
*)
huffman@41286
     4
wenzelm@62175
     5
section \<open>Profinite and bifinite cpos\<close>
huffman@41286
     6
huffman@41286
     7
theory Bifinite
wenzelm@66453
     8
imports Map_Functions Cprod Sprod Sfun Up "HOL-Library.Countable"
huffman@41286
     9
begin
huffman@41286
    10
huffman@41286
    11
default_sort cpo
huffman@41286
    12
wenzelm@62175
    13
subsection \<open>Chains of finite deflations\<close>
huffman@41286
    14
huffman@41286
    15
locale approx_chain =
huffman@41286
    16
  fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
huffman@41286
    17
  assumes chain_approx [simp]: "chain (\<lambda>i. approx i)"
huffman@41286
    18
  assumes lub_approx [simp]: "(\<Squnion>i. approx i) = ID"
huffman@41286
    19
  assumes finite_deflation_approx [simp]: "\<And>i. finite_deflation (approx i)"
huffman@41286
    20
begin
huffman@41286
    21
huffman@41286
    22
lemma deflation_approx: "deflation (approx i)"
huffman@41286
    23
using finite_deflation_approx by (rule finite_deflation_imp_deflation)
huffman@41286
    24
huffman@41286
    25
lemma approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
huffman@41286
    26
using deflation_approx by (rule deflation.idem)
huffman@41286
    27
huffman@41286
    28
lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x"
huffman@41286
    29
using deflation_approx by (rule deflation.below)
huffman@41286
    30
huffman@41286
    31
lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))"
huffman@41286
    32
apply (rule finite_deflation.finite_range)
huffman@41286
    33
apply (rule finite_deflation_approx)
huffman@41286
    34
done
huffman@41286
    35
huffman@41370
    36
lemma compact_approx [simp]: "compact (approx n\<cdot>x)"
huffman@41286
    37
apply (rule finite_deflation.compact)
huffman@41286
    38
apply (rule finite_deflation_approx)
huffman@41286
    39
done
huffman@41286
    40
huffman@41286
    41
lemma compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
huffman@41286
    42
by (rule admD2, simp_all)
huffman@41286
    43
huffman@41286
    44
end
huffman@41286
    45
wenzelm@62175
    46
subsection \<open>Omega-profinite and bifinite domains\<close>
huffman@41286
    47
huffman@41286
    48
class bifinite = pcpo +
huffman@41286
    49
  assumes bifinite: "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a"
huffman@41286
    50
huffman@41286
    51
class profinite = cpo +
huffman@41286
    52
  assumes profinite: "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
huffman@41286
    53
wenzelm@62175
    54
subsection \<open>Building approx chains\<close>
huffman@41286
    55
huffman@41286
    56
lemma approx_chain_iso:
huffman@41286
    57
  assumes a: "approx_chain a"
huffman@41286
    58
  assumes [simp]: "\<And>x. f\<cdot>(g\<cdot>x) = x"
huffman@41286
    59
  assumes [simp]: "\<And>y. g\<cdot>(f\<cdot>y) = y"
huffman@41286
    60
  shows "approx_chain (\<lambda>i. f oo a i oo g)"
huffman@41286
    61
proof -
huffman@41286
    62
  have 1: "f oo g = ID" by (simp add: cfun_eqI)
huffman@41286
    63
  have 2: "ep_pair f g" by (simp add: ep_pair_def)
huffman@41286
    64
  from 1 2 show ?thesis
huffman@41286
    65
    using a unfolding approx_chain_def
huffman@41286
    66
    by (simp add: lub_APP ep_pair.finite_deflation_e_d_p)
huffman@41286
    67
qed
huffman@41286
    68
huffman@41286
    69
lemma approx_chain_u_map:
huffman@41286
    70
  assumes "approx_chain a"
huffman@41286
    71
  shows "approx_chain (\<lambda>i. u_map\<cdot>(a i))"
huffman@41286
    72
  using assms unfolding approx_chain_def
huffman@41286
    73
  by (simp add: lub_APP u_map_ID finite_deflation_u_map)
huffman@41286
    74
huffman@41286
    75
lemma approx_chain_sfun_map:
huffman@41286
    76
  assumes "approx_chain a" and "approx_chain b"
huffman@41286
    77
  shows "approx_chain (\<lambda>i. sfun_map\<cdot>(a i)\<cdot>(b i))"
huffman@41286
    78
  using assms unfolding approx_chain_def
huffman@41286
    79
  by (simp add: lub_APP sfun_map_ID finite_deflation_sfun_map)
huffman@41286
    80
huffman@41286
    81
lemma approx_chain_sprod_map:
huffman@41286
    82
  assumes "approx_chain a" and "approx_chain b"
huffman@41286
    83
  shows "approx_chain (\<lambda>i. sprod_map\<cdot>(a i)\<cdot>(b i))"
huffman@41286
    84
  using assms unfolding approx_chain_def
huffman@41286
    85
  by (simp add: lub_APP sprod_map_ID finite_deflation_sprod_map)
huffman@41286
    86
huffman@41286
    87
lemma approx_chain_ssum_map:
huffman@41286
    88
  assumes "approx_chain a" and "approx_chain b"
huffman@41286
    89
  shows "approx_chain (\<lambda>i. ssum_map\<cdot>(a i)\<cdot>(b i))"
huffman@41286
    90
  using assms unfolding approx_chain_def
huffman@41286
    91
  by (simp add: lub_APP ssum_map_ID finite_deflation_ssum_map)
huffman@41286
    92
huffman@41286
    93
lemma approx_chain_cfun_map:
huffman@41286
    94
  assumes "approx_chain a" and "approx_chain b"
huffman@41286
    95
  shows "approx_chain (\<lambda>i. cfun_map\<cdot>(a i)\<cdot>(b i))"
huffman@41286
    96
  using assms unfolding approx_chain_def
huffman@41286
    97
  by (simp add: lub_APP cfun_map_ID finite_deflation_cfun_map)
huffman@41286
    98
huffman@41297
    99
lemma approx_chain_prod_map:
huffman@41286
   100
  assumes "approx_chain a" and "approx_chain b"
huffman@41297
   101
  shows "approx_chain (\<lambda>i. prod_map\<cdot>(a i)\<cdot>(b i))"
huffman@41286
   102
  using assms unfolding approx_chain_def
huffman@41297
   103
  by (simp add: lub_APP prod_map_ID finite_deflation_prod_map)
huffman@41286
   104
wenzelm@62175
   105
text \<open>Approx chains for countable discrete types.\<close>
huffman@41286
   106
huffman@41286
   107
definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"
huffman@41286
   108
  where "discr_approx = (\<lambda>i. \<Lambda>(up\<cdot>x). if to_nat (undiscr x) < i then up\<cdot>x else \<bottom>)"
huffman@41286
   109
huffman@41286
   110
lemma chain_discr_approx [simp]: "chain discr_approx"
huffman@41286
   111
unfolding discr_approx_def
huffman@41286
   112
by (rule chainI, simp add: monofun_cfun monofun_LAM)
huffman@41286
   113
huffman@41286
   114
lemma lub_discr_approx [simp]: "(\<Squnion>i. discr_approx i) = ID"
huffman@41286
   115
apply (rule cfun_eqI)
huffman@41286
   116
apply (simp add: contlub_cfun_fun)
huffman@41286
   117
apply (simp add: discr_approx_def)
huffman@41286
   118
apply (case_tac x, simp)
huffman@41286
   119
apply (rule lub_eqI)
huffman@41286
   120
apply (rule is_lubI)
huffman@41286
   121
apply (rule ub_rangeI, simp)
huffman@41286
   122
apply (drule ub_rangeD)
huffman@41286
   123
apply (erule rev_below_trans)
huffman@41286
   124
apply simp
huffman@41286
   125
apply (rule lessI)
huffman@41286
   126
done
huffman@41286
   127
huffman@41286
   128
lemma inj_on_undiscr [simp]: "inj_on undiscr A"
huffman@41286
   129
using Discr_undiscr by (rule inj_on_inverseI)
huffman@41286
   130
huffman@41286
   131
lemma finite_deflation_discr_approx: "finite_deflation (discr_approx i)"
huffman@41286
   132
proof
huffman@41286
   133
  fix x :: "'a discr u"
huffman@41286
   134
  show "discr_approx i\<cdot>x \<sqsubseteq> x"
huffman@41286
   135
    unfolding discr_approx_def
huffman@41286
   136
    by (cases x, simp, simp)
huffman@41286
   137
  show "discr_approx i\<cdot>(discr_approx i\<cdot>x) = discr_approx i\<cdot>x"
huffman@41286
   138
    unfolding discr_approx_def
huffman@41286
   139
    by (cases x, simp, simp)
huffman@41286
   140
  show "finite {x::'a discr u. discr_approx i\<cdot>x = x}"
huffman@41286
   141
  proof (rule finite_subset)
huffman@41286
   142
    let ?S = "insert (\<bottom>::'a discr u) ((\<lambda>x. up\<cdot>x) ` undiscr -` to_nat -` {..<i})"
huffman@41286
   143
    show "{x::'a discr u. discr_approx i\<cdot>x = x} \<subseteq> ?S"
huffman@41286
   144
      unfolding discr_approx_def
nipkow@62390
   145
      by (rule subsetI, case_tac x, simp, simp split: if_split_asm)
huffman@41286
   146
    show "finite ?S"
huffman@41286
   147
      by (simp add: finite_vimageI)
huffman@41286
   148
  qed
huffman@41286
   149
qed
huffman@41286
   150
huffman@41286
   151
lemma discr_approx: "approx_chain discr_approx"
huffman@41286
   152
using chain_discr_approx lub_discr_approx finite_deflation_discr_approx
huffman@41286
   153
by (rule approx_chain.intro)
huffman@41286
   154
wenzelm@62175
   155
subsection \<open>Class instance proofs\<close>
huffman@41286
   156
huffman@41286
   157
instance bifinite \<subseteq> profinite
huffman@41286
   158
proof
huffman@41286
   159
  show "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
huffman@41286
   160
    using bifinite [where 'a='a]
huffman@41286
   161
    by (fast intro!: approx_chain_u_map)
huffman@41286
   162
qed
huffman@41286
   163
huffman@41286
   164
instance u :: (profinite) bifinite
wenzelm@61169
   165
  by standard (rule profinite)
huffman@41286
   166
wenzelm@62175
   167
text \<open>
huffman@41286
   168
  Types @{typ "'a \<rightarrow> 'b"} and @{typ "'a u \<rightarrow>! 'b"} are isomorphic.
wenzelm@62175
   169
\<close>
huffman@41286
   170
huffman@41286
   171
definition "encode_cfun = (\<Lambda> f. sfun_abs\<cdot>(fup\<cdot>f))"
huffman@41286
   172
huffman@41286
   173
definition "decode_cfun = (\<Lambda> g x. sfun_rep\<cdot>g\<cdot>(up\<cdot>x))"
huffman@41286
   174
huffman@41286
   175
lemma decode_encode_cfun [simp]: "decode_cfun\<cdot>(encode_cfun\<cdot>x) = x"
huffman@41286
   176
unfolding encode_cfun_def decode_cfun_def
huffman@41286
   177
by (simp add: eta_cfun)
huffman@41286
   178
huffman@41286
   179
lemma encode_decode_cfun [simp]: "encode_cfun\<cdot>(decode_cfun\<cdot>y) = y"
huffman@41286
   180
unfolding encode_cfun_def decode_cfun_def
huffman@41286
   181
apply (simp add: sfun_eq_iff strictify_cancel)
huffman@41286
   182
apply (rule cfun_eqI, case_tac x, simp_all)
huffman@41286
   183
done
huffman@41286
   184
huffman@41286
   185
instance cfun :: (profinite, bifinite) bifinite
huffman@41286
   186
proof
huffman@41286
   187
  obtain a :: "nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" where a: "approx_chain a"
huffman@41286
   188
    using profinite ..
huffman@41286
   189
  obtain b :: "nat \<Rightarrow> 'b \<rightarrow> 'b" where b: "approx_chain b"
huffman@41286
   190
    using bifinite ..
huffman@41286
   191
  have "approx_chain (\<lambda>i. decode_cfun oo sfun_map\<cdot>(a i)\<cdot>(b i) oo encode_cfun)"
huffman@41286
   192
    using a b by (simp add: approx_chain_iso approx_chain_sfun_map)
huffman@41286
   193
  thus "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b)). approx_chain a"
huffman@41286
   194
    by - (rule exI)
huffman@41286
   195
qed
huffman@41286
   196
wenzelm@62175
   197
text \<open>
huffman@41286
   198
  Types @{typ "('a * 'b) u"} and @{typ "'a u \<otimes> 'b u"} are isomorphic.
wenzelm@62175
   199
\<close>
huffman@41286
   200
huffman@41286
   201
definition "encode_prod_u = (\<Lambda>(up\<cdot>(x, y)). (:up\<cdot>x, up\<cdot>y:))"
huffman@41286
   202
huffman@41286
   203
definition "decode_prod_u = (\<Lambda>(:up\<cdot>x, up\<cdot>y:). up\<cdot>(x, y))"
huffman@41286
   204
huffman@41286
   205
lemma decode_encode_prod_u [simp]: "decode_prod_u\<cdot>(encode_prod_u\<cdot>x) = x"
huffman@41286
   206
unfolding encode_prod_u_def decode_prod_u_def
huffman@41286
   207
by (case_tac x, simp, rename_tac y, case_tac y, simp)
huffman@41286
   208
huffman@41286
   209
lemma encode_decode_prod_u [simp]: "encode_prod_u\<cdot>(decode_prod_u\<cdot>y) = y"
huffman@41286
   210
unfolding encode_prod_u_def decode_prod_u_def
huffman@41286
   211
apply (case_tac y, simp, rename_tac a b)
huffman@41286
   212
apply (case_tac a, simp, case_tac b, simp, simp)
huffman@41286
   213
done
huffman@41286
   214
huffman@41286
   215
instance prod :: (profinite, profinite) profinite
huffman@41286
   216
proof
huffman@41286
   217
  obtain a :: "nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" where a: "approx_chain a"
huffman@41286
   218
    using profinite ..
huffman@41286
   219
  obtain b :: "nat \<Rightarrow> 'b\<^sub>\<bottom> \<rightarrow> 'b\<^sub>\<bottom>" where b: "approx_chain b"
huffman@41286
   220
    using profinite ..
huffman@41286
   221
  have "approx_chain (\<lambda>i. decode_prod_u oo sprod_map\<cdot>(a i)\<cdot>(b i) oo encode_prod_u)"
huffman@41286
   222
    using a b by (simp add: approx_chain_iso approx_chain_sprod_map)
huffman@41286
   223
  thus "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b)\<^sub>\<bottom> \<rightarrow> ('a \<times> 'b)\<^sub>\<bottom>). approx_chain a"
huffman@41286
   224
    by - (rule exI)
huffman@41286
   225
qed
huffman@41286
   226
huffman@41286
   227
instance prod :: (bifinite, bifinite) bifinite
huffman@41286
   228
proof
huffman@41286
   229
  show "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b) \<rightarrow> ('a \<times> 'b)). approx_chain a"
huffman@41286
   230
    using bifinite [where 'a='a] and bifinite [where 'a='b]
huffman@41297
   231
    by (fast intro!: approx_chain_prod_map)
huffman@41286
   232
qed
huffman@41286
   233
huffman@41286
   234
instance sfun :: (bifinite, bifinite) bifinite
huffman@41286
   235
proof
huffman@41286
   236
  show "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow>! 'b) \<rightarrow> ('a \<rightarrow>! 'b)). approx_chain a"
huffman@41286
   237
    using bifinite [where 'a='a] and bifinite [where 'a='b]
huffman@41286
   238
    by (fast intro!: approx_chain_sfun_map)
huffman@41286
   239
qed
huffman@41286
   240
huffman@41286
   241
instance sprod :: (bifinite, bifinite) bifinite
huffman@41286
   242
proof
huffman@41286
   243
  show "\<exists>(a::nat \<Rightarrow> ('a \<otimes> 'b) \<rightarrow> ('a \<otimes> 'b)). approx_chain a"
huffman@41286
   244
    using bifinite [where 'a='a] and bifinite [where 'a='b]
huffman@41286
   245
    by (fast intro!: approx_chain_sprod_map)
huffman@41286
   246
qed
huffman@41286
   247
huffman@41286
   248
instance ssum :: (bifinite, bifinite) bifinite
huffman@41286
   249
proof
huffman@41286
   250
  show "\<exists>(a::nat \<Rightarrow> ('a \<oplus> 'b) \<rightarrow> ('a \<oplus> 'b)). approx_chain a"
huffman@41286
   251
    using bifinite [where 'a='a] and bifinite [where 'a='b]
huffman@41286
   252
    by (fast intro!: approx_chain_ssum_map)
huffman@41286
   253
qed
huffman@41286
   254
huffman@41286
   255
lemma approx_chain_unit: "approx_chain (\<bottom> :: nat \<Rightarrow> unit \<rightarrow> unit)"
huffman@41430
   256
by (simp add: approx_chain_def cfun_eq_iff finite_deflation_bottom)
huffman@41286
   257
huffman@41286
   258
instance unit :: bifinite
wenzelm@61169
   259
  by standard (fast intro!: approx_chain_unit)
huffman@41286
   260
huffman@41286
   261
instance discr :: (countable) profinite
wenzelm@61169
   262
  by standard (fast intro!: discr_approx)
huffman@41286
   263
huffman@41286
   264
instance lift :: (countable) bifinite
huffman@41286
   265
proof
huffman@41286
   266
  note [simp] = cont_Abs_lift cont_Rep_lift Rep_lift_inverse Abs_lift_inverse
huffman@41286
   267
  obtain a :: "nat \<Rightarrow> ('a discr)\<^sub>\<bottom> \<rightarrow> ('a discr)\<^sub>\<bottom>" where a: "approx_chain a"
huffman@41286
   268
    using profinite ..
huffman@41286
   269
  hence "approx_chain (\<lambda>i. (\<Lambda> y. Abs_lift y) oo a i oo (\<Lambda> x. Rep_lift x))"
huffman@41286
   270
    by (rule approx_chain_iso) simp_all
huffman@41286
   271
  thus "\<exists>(a::nat \<Rightarrow> 'a lift \<rightarrow> 'a lift). approx_chain a"
huffman@41286
   272
    by - (rule exI)
huffman@41286
   273
qed
huffman@41286
   274
huffman@41286
   275
end