src/HOLCF/CompactBasis.thy
author huffman
Fri Jun 20 22:51:50 2008 +0200 (2008-06-20)
changeset 27309 c74270fd72a8
parent 27297 2c42b1505f25
child 27373 5794a0e3e26c
permissions -rw-r--r--
clean up and rename some profinite lemmas
huffman@25904
     1
(*  Title:      HOLCF/CompactBasis.thy
huffman@25904
     2
    ID:         $Id$
huffman@25904
     3
    Author:     Brian Huffman
huffman@25904
     4
*)
huffman@25904
     5
huffman@25904
     6
header {* Compact bases of domains *}
huffman@25904
     7
huffman@25904
     8
theory CompactBasis
huffman@27297
     9
imports Bifinite Cset
huffman@25904
    10
begin
huffman@25904
    11
huffman@25904
    12
subsection {* Ideals over a preorder *}
huffman@25904
    13
huffman@27268
    14
locale preorder =
huffman@27268
    15
  fixes r :: "'a::type \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
huffman@27268
    16
  assumes r_refl: "x \<preceq> x"
huffman@27268
    17
  assumes r_trans: "\<lbrakk>x \<preceq> y; y \<preceq> z\<rbrakk> \<Longrightarrow> x \<preceq> z"
huffman@25904
    18
begin
huffman@25904
    19
huffman@25904
    20
definition
huffman@25904
    21
  ideal :: "'a set \<Rightarrow> bool" where
huffman@27268
    22
  "ideal A = ((\<exists>x. x \<in> A) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<exists>z\<in>A. x \<preceq> z \<and> y \<preceq> z) \<and>
huffman@27268
    23
    (\<forall>x y. x \<preceq> y \<longrightarrow> y \<in> A \<longrightarrow> x \<in> A))"
huffman@25904
    24
huffman@25904
    25
lemma idealI:
huffman@25904
    26
  assumes "\<exists>x. x \<in> A"
huffman@27268
    27
  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. x \<preceq> z \<and> y \<preceq> z"
huffman@27268
    28
  assumes "\<And>x y. \<lbrakk>x \<preceq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
huffman@25904
    29
  shows "ideal A"
huffman@25904
    30
unfolding ideal_def using prems by fast
huffman@25904
    31
huffman@25904
    32
lemma idealD1:
huffman@25904
    33
  "ideal A \<Longrightarrow> \<exists>x. x \<in> A"
huffman@25904
    34
unfolding ideal_def by fast
huffman@25904
    35
huffman@25904
    36
lemma idealD2:
huffman@27268
    37
  "\<lbrakk>ideal A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. x \<preceq> z \<and> y \<preceq> z"
huffman@25904
    38
unfolding ideal_def by fast
huffman@25904
    39
huffman@25904
    40
lemma idealD3:
huffman@27268
    41
  "\<lbrakk>ideal A; x \<preceq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
huffman@25904
    42
unfolding ideal_def by fast
huffman@25904
    43
huffman@25904
    44
lemma ideal_directed_finite:
huffman@25904
    45
  assumes A: "ideal A"
huffman@27268
    46
  shows "\<lbrakk>finite U; U \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. \<forall>x\<in>U. x \<preceq> z"
huffman@25904
    47
apply (induct U set: finite)
huffman@25904
    48
apply (simp add: idealD1 [OF A])
huffman@25904
    49
apply (simp, clarify, rename_tac y)
huffman@25904
    50
apply (drule (1) idealD2 [OF A])
huffman@25904
    51
apply (clarify, erule_tac x=z in rev_bexI)
huffman@27268
    52
apply (fast intro: r_trans)
huffman@25904
    53
done
huffman@25904
    54
huffman@27268
    55
lemma ideal_principal: "ideal {x. x \<preceq> z}"
huffman@25904
    56
apply (rule idealI)
huffman@25904
    57
apply (rule_tac x=z in exI)
huffman@27268
    58
apply (fast intro: r_refl)
huffman@25904
    59
apply (rule_tac x=z in bexI, fast)
huffman@27268
    60
apply (fast intro: r_refl)
huffman@27268
    61
apply (fast intro: r_trans)
huffman@25904
    62
done
huffman@25904
    63
huffman@27268
    64
lemma ex_ideal: "\<exists>A. ideal A"
huffman@27268
    65
by (rule exI, rule ideal_principal)
huffman@27268
    66
huffman@25904
    67
lemma directed_image_ideal:
huffman@25904
    68
  assumes A: "ideal A"
huffman@27268
    69
  assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
huffman@25904
    70
  shows "directed (f ` A)"
huffman@25904
    71
apply (rule directedI)
huffman@25904
    72
apply (cut_tac idealD1 [OF A], fast)
huffman@25904
    73
apply (clarify, rename_tac a b)
huffman@25904
    74
apply (drule (1) idealD2 [OF A])
huffman@25904
    75
apply (clarify, rename_tac c)
huffman@25904
    76
apply (rule_tac x="f c" in rev_bexI)
huffman@25904
    77
apply (erule imageI)
huffman@25904
    78
apply (simp add: f)
huffman@25904
    79
done
huffman@25904
    80
huffman@27297
    81
lemma adm_ideal: "adm (\<lambda>A. ideal (Rep_cset A))"
huffman@25904
    82
unfolding ideal_def by (intro adm_lemmas adm_set_lemmas)
huffman@25904
    83
huffman@27297
    84
lemma cpodef_ideal_lemma:
huffman@27297
    85
  "(\<exists>x. x \<in> {S. ideal (Rep_cset S)}) \<and> adm (\<lambda>x. x \<in> {S. ideal (Rep_cset S)})"
huffman@27297
    86
apply (simp add: adm_ideal)
huffman@27297
    87
apply (rule exI [where x="Abs_cset {x. x \<preceq> arbitrary}"])
huffman@27297
    88
apply (simp add: ideal_principal)
huffman@27297
    89
done
huffman@27297
    90
huffman@26420
    91
lemma lub_image_principal:
huffman@27268
    92
  assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
huffman@27268
    93
  shows "(\<Squnion>x\<in>{x. x \<preceq> y}. f x) = f y"
huffman@25904
    94
apply (rule thelubI)
huffman@25904
    95
apply (rule is_lub_maximal)
huffman@25904
    96
apply (rule ub_imageI)
huffman@25904
    97
apply (simp add: f)
huffman@25904
    98
apply (rule imageI)
huffman@27268
    99
apply (simp add: r_refl)
huffman@25904
   100
done
huffman@25904
   101
huffman@26420
   102
end
huffman@26420
   103
huffman@27268
   104
interpretation sq_le: preorder ["sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"]
huffman@27268
   105
apply unfold_locales
huffman@27268
   106
apply (rule refl_less)
huffman@27268
   107
apply (erule (1) trans_less)
huffman@27268
   108
done
huffman@27268
   109
huffman@26420
   110
subsection {* Defining functions in terms of basis elements *}
huffman@26420
   111
huffman@26034
   112
lemma finite_directed_contains_lub:
huffman@26034
   113
  "\<lbrakk>finite S; directed S\<rbrakk> \<Longrightarrow> \<exists>u\<in>S. S <<| u"
huffman@25904
   114
apply (drule (1) directed_finiteD, rule subset_refl)
huffman@25904
   115
apply (erule bexE)
huffman@26034
   116
apply (rule rev_bexI, assumption)
huffman@25904
   117
apply (erule (1) is_lub_maximal)
huffman@25904
   118
done
huffman@25904
   119
huffman@26034
   120
lemma lub_finite_directed_in_self:
huffman@26034
   121
  "\<lbrakk>finite S; directed S\<rbrakk> \<Longrightarrow> lub S \<in> S"
huffman@26034
   122
apply (drule (1) finite_directed_contains_lub, clarify)
huffman@26034
   123
apply (drule thelubI, simp)
huffman@26034
   124
done
huffman@26034
   125
huffman@26034
   126
lemma finite_directed_has_lub: "\<lbrakk>finite S; directed S\<rbrakk> \<Longrightarrow> \<exists>u. S <<| u"
huffman@26034
   127
by (drule (1) finite_directed_contains_lub, fast)
huffman@26034
   128
huffman@25904
   129
lemma is_ub_thelub0: "\<lbrakk>\<exists>u. S <<| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> lub S"
huffman@25904
   130
apply (erule exE, drule lubI)
huffman@25904
   131
apply (drule is_lubD1)
huffman@25904
   132
apply (erule (1) is_ubD)
huffman@25904
   133
done
huffman@25904
   134
huffman@25904
   135
lemma is_lub_thelub0: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x"
huffman@25904
   136
by (erule exE, drule lubI, erule is_lub_lub)
huffman@25904
   137
huffman@27268
   138
locale basis_take = preorder +
huffman@25904
   139
  fixes take :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'a"
huffman@27268
   140
  assumes take_less: "take n a \<preceq> a"
huffman@25904
   141
  assumes take_take: "take n (take n a) = take n a"
huffman@27268
   142
  assumes take_mono: "a \<preceq> b \<Longrightarrow> take n a \<preceq> take n b"
huffman@27268
   143
  assumes take_chain: "take n a \<preceq> take (Suc n) a"
huffman@25904
   144
  assumes finite_range_take: "finite (range (take n))"
huffman@25904
   145
  assumes take_covers: "\<exists>n. take n a = a"
huffman@27288
   146
begin
huffman@27288
   147
huffman@27288
   148
lemma take_chain_less: "m < n \<Longrightarrow> take m a \<preceq> take n a"
huffman@27288
   149
by (erule less_Suc_induct, rule take_chain, erule (1) r_trans)
huffman@27288
   150
huffman@27288
   151
lemma take_chain_le: "m \<le> n \<Longrightarrow> take m a \<preceq> take n a"
huffman@27288
   152
by (cases "m = n", simp add: r_refl, simp add: take_chain_less)
huffman@27288
   153
huffman@27288
   154
end
huffman@26420
   155
huffman@27268
   156
locale ideal_completion = basis_take +
huffman@26420
   157
  fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
huffman@26927
   158
  fixes rep :: "'b::cpo \<Rightarrow> 'a::type set"
huffman@26927
   159
  assumes ideal_rep: "\<And>x. preorder.ideal r (rep x)"
huffman@27297
   160
  assumes rep_contlub: "\<And>Y. chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
huffman@27268
   161
  assumes rep_principal: "\<And>a. rep (principal a) = {b. b \<preceq> a}"
huffman@26927
   162
  assumes subset_repD: "\<And>x y. rep x \<subseteq> rep y \<Longrightarrow> x \<sqsubseteq> y"
huffman@25904
   163
begin
huffman@25904
   164
huffman@26927
   165
lemma finite_take_rep: "finite (take n ` rep x)"
huffman@25904
   166
by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range_take])
huffman@25904
   167
huffman@25904
   168
lemma basis_fun_lemma0:
huffman@25904
   169
  fixes f :: "'a::type \<Rightarrow> 'c::cpo"
huffman@27268
   170
  assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
huffman@26927
   171
  shows "\<exists>u. f ` take i ` rep x <<| u"
huffman@25904
   172
apply (rule finite_directed_has_lub)
huffman@25904
   173
apply (rule finite_imageI)
huffman@26927
   174
apply (rule finite_take_rep)
huffman@25904
   175
apply (subst image_image)
huffman@25904
   176
apply (rule directed_image_ideal)
huffman@26927
   177
apply (rule ideal_rep)
huffman@25904
   178
apply (rule f_mono)
huffman@25904
   179
apply (erule take_mono)
huffman@25904
   180
done
huffman@25904
   181
huffman@25904
   182
lemma basis_fun_lemma1:
huffman@25904
   183
  fixes f :: "'a::type \<Rightarrow> 'c::cpo"
huffman@27268
   184
  assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
huffman@26927
   185
  shows "chain (\<lambda>i. lub (f ` take i ` rep x))"
huffman@25904
   186
 apply (rule chainI)
huffman@25904
   187
 apply (rule is_lub_thelub0)
huffman@25904
   188
  apply (rule basis_fun_lemma0, erule f_mono)
huffman@25904
   189
 apply (rule is_ubI, clarsimp, rename_tac a)
huffman@26420
   190
 apply (rule sq_le.trans_less [OF f_mono [OF take_chain]])
huffman@25904
   191
 apply (rule is_ub_thelub0)
huffman@25904
   192
  apply (rule basis_fun_lemma0, erule f_mono)
huffman@25904
   193
 apply simp
huffman@25904
   194
done
huffman@25904
   195
huffman@25904
   196
lemma basis_fun_lemma2:
huffman@25904
   197
  fixes f :: "'a::type \<Rightarrow> 'c::cpo"
huffman@27268
   198
  assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
huffman@26927
   199
  shows "f ` rep x <<| (\<Squnion>i. lub (f ` take i ` rep x))"
huffman@25904
   200
 apply (rule is_lubI)
huffman@25904
   201
 apply (rule ub_imageI, rename_tac a)
huffman@25904
   202
  apply (cut_tac a=a in take_covers, erule exE, rename_tac i)
huffman@25904
   203
  apply (erule subst)
huffman@25904
   204
  apply (rule rev_trans_less)
huffman@25904
   205
   apply (rule_tac x=i in is_ub_thelub)
huffman@25904
   206
   apply (rule basis_fun_lemma1, erule f_mono)
huffman@25904
   207
  apply (rule is_ub_thelub0)
huffman@25904
   208
   apply (rule basis_fun_lemma0, erule f_mono)
huffman@25904
   209
  apply simp
huffman@25904
   210
 apply (rule is_lub_thelub [OF _ ub_rangeI])
huffman@25904
   211
  apply (rule basis_fun_lemma1, erule f_mono)
huffman@25904
   212
 apply (rule is_lub_thelub0)
huffman@25904
   213
  apply (rule basis_fun_lemma0, erule f_mono)
huffman@25904
   214
 apply (rule is_ubI, clarsimp, rename_tac a)
huffman@26420
   215
 apply (rule sq_le.trans_less [OF f_mono [OF take_less]])
huffman@25904
   216
 apply (erule (1) ub_imageD)
huffman@25904
   217
done
huffman@25904
   218
huffman@25904
   219
lemma basis_fun_lemma:
huffman@25904
   220
  fixes f :: "'a::type \<Rightarrow> 'c::cpo"
huffman@27268
   221
  assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
huffman@26927
   222
  shows "\<exists>u. f ` rep x <<| u"
huffman@25904
   223
by (rule exI, rule basis_fun_lemma2, erule f_mono)
huffman@25904
   224
huffman@26927
   225
lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y"
huffman@27297
   226
apply (frule bin_chain)
huffman@27297
   227
apply (drule rep_contlub)
huffman@27297
   228
apply (simp only: thelubI [OF lub_bin_chain])
huffman@27297
   229
apply (rule subsetI, rule UN_I [where a=0], simp_all)
huffman@25904
   230
done
huffman@25904
   231
huffman@26927
   232
lemma less_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y"
huffman@26927
   233
by (rule iffI [OF rep_mono subset_repD])
huffman@25904
   234
huffman@26927
   235
lemma rep_eq: "rep x = {a. principal a \<sqsubseteq> x}"
huffman@26927
   236
unfolding less_def rep_principal
huffman@25904
   237
apply safe
huffman@26927
   238
apply (erule (1) idealD3 [OF ideal_rep])
huffman@27268
   239
apply (erule subsetD, simp add: r_refl)
huffman@25904
   240
done
huffman@25904
   241
huffman@26927
   242
lemma mem_rep_iff_principal_less: "a \<in> rep x \<longleftrightarrow> principal a \<sqsubseteq> x"
huffman@26927
   243
by (simp add: rep_eq)
huffman@26927
   244
huffman@26927
   245
lemma principal_less_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x"
huffman@26927
   246
by (simp add: rep_eq)
huffman@25904
   247
huffman@27289
   248
lemma principal_less_iff [simp]: "principal a \<sqsubseteq> principal b \<longleftrightarrow> a \<preceq> b"
huffman@26927
   249
by (simp add: principal_less_iff_mem_rep rep_principal)
huffman@25904
   250
huffman@27268
   251
lemma principal_eq_iff: "principal a = principal b \<longleftrightarrow> a \<preceq> b \<and> b \<preceq> a"
huffman@26927
   252
unfolding po_eq_conv [where 'a='b] principal_less_iff ..
huffman@26927
   253
huffman@26927
   254
lemma repD: "a \<in> rep x \<Longrightarrow> principal a \<sqsubseteq> x"
huffman@26927
   255
by (simp add: rep_eq)
huffman@25904
   256
huffman@27268
   257
lemma principal_mono: "a \<preceq> b \<Longrightarrow> principal a \<sqsubseteq> principal b"
huffman@27289
   258
by (simp only: principal_less_iff)
huffman@25904
   259
huffman@25904
   260
lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
huffman@26927
   261
unfolding principal_less_iff_mem_rep
berghofe@26806
   262
by (simp add: less_def subset_eq)
huffman@25904
   263
huffman@26927
   264
lemma lub_principal_rep: "principal ` rep x <<| x"
huffman@25904
   265
apply (rule is_lubI)
huffman@25904
   266
apply (rule ub_imageI)
huffman@26927
   267
apply (erule repD)
huffman@25904
   268
apply (subst less_def)
huffman@25904
   269
apply (rule subsetI)
huffman@25904
   270
apply (drule (1) ub_imageD)
huffman@26927
   271
apply (simp add: rep_eq)
huffman@25904
   272
done
huffman@25904
   273
huffman@25904
   274
definition
huffman@25904
   275
  basis_fun :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where
huffman@26927
   276
  "basis_fun = (\<lambda>f. (\<Lambda> x. lub (f ` rep x)))"
huffman@25904
   277
huffman@25904
   278
lemma basis_fun_beta:
huffman@25904
   279
  fixes f :: "'a::type \<Rightarrow> 'c::cpo"
huffman@27268
   280
  assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
huffman@26927
   281
  shows "basis_fun f\<cdot>x = lub (f ` rep x)"
huffman@25904
   282
unfolding basis_fun_def
huffman@25904
   283
proof (rule beta_cfun)
huffman@26927
   284
  have lub: "\<And>x. \<exists>u. f ` rep x <<| u"
huffman@25904
   285
    using f_mono by (rule basis_fun_lemma)
huffman@26927
   286
  show cont: "cont (\<lambda>x. lub (f ` rep x))"
huffman@25904
   287
    apply (rule contI2)
huffman@25904
   288
     apply (rule monofunI)
huffman@25904
   289
     apply (rule is_lub_thelub0 [OF lub ub_imageI])
huffman@25904
   290
     apply (rule is_ub_thelub0 [OF lub imageI])
huffman@26927
   291
     apply (erule (1) subsetD [OF rep_mono])
huffman@25904
   292
    apply (rule is_lub_thelub0 [OF lub ub_imageI])
huffman@26927
   293
    apply (simp add: rep_contlub, clarify)
huffman@25904
   294
    apply (erule rev_trans_less [OF is_ub_thelub])
huffman@25904
   295
    apply (erule is_ub_thelub0 [OF lub imageI])
huffman@25904
   296
    done
huffman@25904
   297
qed
huffman@25904
   298
huffman@25904
   299
lemma basis_fun_principal:
huffman@25904
   300
  fixes f :: "'a::type \<Rightarrow> 'c::cpo"
huffman@27268
   301
  assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
huffman@25904
   302
  shows "basis_fun f\<cdot>(principal a) = f a"
huffman@25904
   303
apply (subst basis_fun_beta, erule f_mono)
huffman@26927
   304
apply (subst rep_principal)
huffman@25904
   305
apply (rule lub_image_principal, erule f_mono)
huffman@25904
   306
done
huffman@25904
   307
huffman@25904
   308
lemma basis_fun_mono:
huffman@27268
   309
  assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
huffman@27268
   310
  assumes g_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> g a \<sqsubseteq> g b"
huffman@25904
   311
  assumes less: "\<And>a. f a \<sqsubseteq> g a"
huffman@25904
   312
  shows "basis_fun f \<sqsubseteq> basis_fun g"
huffman@25904
   313
 apply (rule less_cfun_ext)
huffman@25904
   314
 apply (simp only: basis_fun_beta f_mono g_mono)
huffman@25904
   315
 apply (rule is_lub_thelub0)
huffman@25904
   316
  apply (rule basis_fun_lemma, erule f_mono)
huffman@25904
   317
 apply (rule ub_imageI, rename_tac a)
huffman@26420
   318
 apply (rule sq_le.trans_less [OF less])
huffman@25904
   319
 apply (rule is_ub_thelub0)
huffman@25904
   320
  apply (rule basis_fun_lemma, erule g_mono)
huffman@25904
   321
 apply (erule imageI)
huffman@25904
   322
done
huffman@25904
   323
huffman@27289
   324
lemma compact_principal [simp]: "compact (principal a)"
huffman@26927
   325
by (rule compactI2, simp add: principal_less_iff_mem_rep rep_contlub)
huffman@26927
   326
huffman@26927
   327
definition
huffman@26927
   328
  completion_approx :: "nat \<Rightarrow> 'b \<rightarrow> 'b" where
huffman@26927
   329
  "completion_approx = (\<lambda>i. basis_fun (\<lambda>a. principal (take i a)))"
huffman@25904
   330
huffman@26927
   331
lemma completion_approx_beta:
huffman@26927
   332
  "completion_approx i\<cdot>x = (\<Squnion>a\<in>rep x. principal (take i a))"
huffman@26927
   333
unfolding completion_approx_def
huffman@26927
   334
by (simp add: basis_fun_beta principal_mono take_mono)
huffman@26927
   335
huffman@26927
   336
lemma completion_approx_principal:
huffman@26927
   337
  "completion_approx i\<cdot>(principal a) = principal (take i a)"
huffman@26927
   338
unfolding completion_approx_def
huffman@26927
   339
by (simp add: basis_fun_principal principal_mono take_mono)
huffman@26927
   340
huffman@26927
   341
lemma chain_completion_approx: "chain completion_approx"
huffman@26927
   342
unfolding completion_approx_def
huffman@25904
   343
apply (rule chainI)
huffman@25904
   344
apply (rule basis_fun_mono)
huffman@25904
   345
apply (erule principal_mono [OF take_mono])
huffman@25904
   346
apply (erule principal_mono [OF take_mono])
huffman@25904
   347
apply (rule principal_mono [OF take_chain])
huffman@25904
   348
done
huffman@25904
   349
huffman@26927
   350
lemma lub_completion_approx: "(\<Squnion>i. completion_approx i\<cdot>x) = x"
huffman@26927
   351
unfolding completion_approx_beta
huffman@25904
   352
 apply (subst image_image [where f=principal, symmetric])
huffman@26927
   353
 apply (rule unique_lub [OF _ lub_principal_rep])
huffman@25904
   354
 apply (rule basis_fun_lemma2, erule principal_mono)
huffman@25904
   355
done
huffman@25904
   356
huffman@26927
   357
lemma completion_approx_eq_principal:
huffman@26927
   358
  "\<exists>a\<in>rep x. completion_approx i\<cdot>x = principal (take i a)"
huffman@26927
   359
unfolding completion_approx_beta
huffman@25904
   360
 apply (subst image_image [where f=principal, symmetric])
huffman@26927
   361
 apply (subgoal_tac "finite (principal ` take i ` rep x)")
huffman@26927
   362
  apply (subgoal_tac "directed (principal ` take i ` rep x)")
huffman@25904
   363
   apply (drule (1) lub_finite_directed_in_self, fast)
huffman@25904
   364
  apply (subst image_image)
huffman@25904
   365
  apply (rule directed_image_ideal)
huffman@26927
   366
   apply (rule ideal_rep)
huffman@25904
   367
  apply (erule principal_mono [OF take_mono])
huffman@25904
   368
 apply (rule finite_imageI)
huffman@26927
   369
 apply (rule finite_take_rep)
huffman@26927
   370
done
huffman@26927
   371
huffman@26927
   372
lemma completion_approx_idem:
huffman@26927
   373
  "completion_approx i\<cdot>(completion_approx i\<cdot>x) = completion_approx i\<cdot>x"
huffman@26927
   374
using completion_approx_eq_principal [where i=i and x=x]
huffman@26927
   375
by (auto simp add: completion_approx_principal take_take)
huffman@26927
   376
huffman@26927
   377
lemma finite_fixes_completion_approx:
huffman@26927
   378
  "finite {x. completion_approx i\<cdot>x = x}" (is "finite ?S")
huffman@26927
   379
apply (subgoal_tac "?S \<subseteq> principal ` range (take i)")
huffman@26927
   380
apply (erule finite_subset)
huffman@26927
   381
apply (rule finite_imageI)
huffman@26927
   382
apply (rule finite_range_take)
huffman@26927
   383
apply (clarify, erule subst)
huffman@26927
   384
apply (cut_tac x=x and i=i in completion_approx_eq_principal)
huffman@26927
   385
apply fast
huffman@25904
   386
done
huffman@25904
   387
huffman@25904
   388
lemma principal_induct:
huffman@25904
   389
  assumes adm: "adm P"
huffman@25904
   390
  assumes P: "\<And>a. P (principal a)"
huffman@25904
   391
  shows "P x"
huffman@26927
   392
 apply (subgoal_tac "P (\<Squnion>i. completion_approx i\<cdot>x)")
huffman@26927
   393
 apply (simp add: lub_completion_approx)
huffman@25925
   394
 apply (rule admD [OF adm])
huffman@26927
   395
  apply (simp add: chain_completion_approx)
huffman@26927
   396
 apply (cut_tac x=x and i=i in completion_approx_eq_principal)
huffman@25904
   397
 apply (clarify, simp add: P)
huffman@25904
   398
done
huffman@25904
   399
huffman@27289
   400
lemma principal_induct2:
huffman@27289
   401
  "\<lbrakk>\<And>y. adm (\<lambda>x. P x y); \<And>x. adm (\<lambda>y. P x y);
huffman@27289
   402
    \<And>a b. P (principal a) (principal b)\<rbrakk> \<Longrightarrow> P x y"
huffman@27289
   403
apply (rule_tac x=y in spec)
huffman@27289
   404
apply (rule_tac x=x in principal_induct, simp)
huffman@27289
   405
apply (rule allI, rename_tac y)
huffman@27289
   406
apply (rule_tac x=y in principal_induct, simp)
huffman@27289
   407
apply simp
huffman@27289
   408
done
huffman@27289
   409
huffman@27267
   410
lemma compact_imp_principal: "compact x \<Longrightarrow> \<exists>a. x = principal a"
huffman@27267
   411
apply (drule adm_compact_neq [OF _ cont_id])
huffman@27267
   412
apply (drule admD2 [where Y="\<lambda>n. completion_approx n\<cdot>x"])
huffman@27267
   413
apply (simp add: chain_completion_approx)
huffman@27267
   414
apply (simp add: lub_completion_approx)
huffman@27267
   415
apply (erule exE, erule ssubst)
huffman@27267
   416
apply (cut_tac i=i and x=x in completion_approx_eq_principal)
huffman@27267
   417
apply (clarify, erule exI)
huffman@27267
   418
done
huffman@27267
   419
huffman@25904
   420
end
huffman@25904
   421
huffman@25904
   422
huffman@25904
   423
subsection {* Compact bases of bifinite domains *}
huffman@25904
   424
huffman@26407
   425
defaultsort profinite
huffman@25904
   426
huffman@26407
   427
typedef (open) 'a compact_basis = "{x::'a::profinite. compact x}"
huffman@25904
   428
by (fast intro: compact_approx)
huffman@25904
   429
huffman@27289
   430
lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)"
huffman@26927
   431
by (rule Rep_compact_basis [unfolded mem_Collect_eq])
huffman@25904
   432
huffman@26420
   433
instantiation compact_basis :: (profinite) sq_ord
huffman@26420
   434
begin
huffman@26420
   435
huffman@26420
   436
definition
huffman@26420
   437
  compact_le_def:
huffman@26420
   438
    "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)"
huffman@26420
   439
huffman@26420
   440
instance ..
huffman@26420
   441
huffman@26420
   442
end
huffman@26420
   443
huffman@26420
   444
instance compact_basis :: (profinite) po
huffman@26420
   445
by (rule typedef_po
huffman@26420
   446
    [OF type_definition_compact_basis compact_le_def])
huffman@25904
   447
huffman@27289
   448
text {* Take function for compact basis *}
huffman@25904
   449
huffman@25904
   450
definition
huffman@25904
   451
  compact_approx :: "nat \<Rightarrow> 'a compact_basis \<Rightarrow> 'a compact_basis" where
huffman@25904
   452
  "compact_approx = (\<lambda>n a. Abs_compact_basis (approx n\<cdot>(Rep_compact_basis a)))"
huffman@25904
   453
huffman@25904
   454
lemma Rep_compact_approx:
huffman@25904
   455
  "Rep_compact_basis (compact_approx n a) = approx n\<cdot>(Rep_compact_basis a)"
huffman@25904
   456
unfolding compact_approx_def
huffman@25904
   457
by (simp add: Abs_compact_basis_inverse)
huffman@25904
   458
huffman@25904
   459
lemmas approx_Rep_compact_basis = Rep_compact_approx [symmetric]
huffman@25904
   460
huffman@27289
   461
interpretation compact_basis:
huffman@27289
   462
  basis_take [sq_le compact_approx]
huffman@27289
   463
proof
huffman@27289
   464
  fix n :: nat and a :: "'a compact_basis"
huffman@27289
   465
  show "compact_approx n a \<sqsubseteq> a"
huffman@27289
   466
    unfolding compact_le_def
huffman@27289
   467
    by (simp add: Rep_compact_approx approx_less)
huffman@27289
   468
next
huffman@27289
   469
  fix n :: nat and a :: "'a compact_basis"
huffman@27289
   470
  show "compact_approx n (compact_approx n a) = compact_approx n a"
huffman@27289
   471
    by (simp add: Rep_compact_basis_inject [symmetric] Rep_compact_approx)
huffman@27289
   472
next
huffman@27289
   473
  fix n :: nat and a b :: "'a compact_basis"
huffman@27289
   474
  assume "a \<sqsubseteq> b" thus "compact_approx n a \<sqsubseteq> compact_approx n b"
huffman@27289
   475
    unfolding compact_le_def Rep_compact_approx
huffman@27289
   476
    by (rule monofun_cfun_arg)
huffman@27289
   477
next
huffman@27289
   478
  fix n :: nat and a :: "'a compact_basis"
huffman@27289
   479
  show "\<And>n a. compact_approx n a \<sqsubseteq> compact_approx (Suc n) a"
huffman@27289
   480
    unfolding compact_le_def Rep_compact_approx
huffman@27289
   481
    by (rule chainE, simp)
huffman@27289
   482
next
huffman@27289
   483
  fix n :: nat
huffman@27289
   484
  show "finite (range (compact_approx n))"
huffman@27289
   485
    apply (rule finite_imageD [where f="Rep_compact_basis"])
huffman@27289
   486
    apply (rule finite_subset [where B="range (\<lambda>x. approx n\<cdot>x)"])
huffman@27289
   487
    apply (clarsimp simp add: Rep_compact_approx)
huffman@27289
   488
    apply (rule finite_range_approx)
huffman@27289
   489
    apply (rule inj_onI, simp add: Rep_compact_basis_inject)
huffman@27289
   490
    done
huffman@27289
   491
next
huffman@27289
   492
  fix a :: "'a compact_basis"
huffman@27289
   493
  show "\<exists>n. compact_approx n a = a"
huffman@27289
   494
    apply (simp add: Rep_compact_basis_inject [symmetric])
huffman@27289
   495
    apply (simp add: Rep_compact_approx)
huffman@27309
   496
    apply (rule profinite_compact_eq_approx)
huffman@27289
   497
    apply (rule compact_Rep_compact_basis)
huffman@27289
   498
    done
huffman@27289
   499
qed
huffman@25904
   500
huffman@27289
   501
text {* Ideal completion *}
huffman@25904
   502
huffman@27289
   503
definition
huffman@27289
   504
  compacts :: "'a \<Rightarrow> 'a compact_basis set" where
huffman@27289
   505
  "compacts = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
huffman@25904
   506
huffman@25904
   507
interpretation compact_basis:
huffman@26927
   508
  ideal_completion [sq_le compact_approx Rep_compact_basis compacts]
huffman@27289
   509
proof
huffman@27289
   510
  fix w :: 'a
huffman@27289
   511
  show "preorder.ideal sq_le (compacts w)"
huffman@27289
   512
  proof (rule sq_le.idealI)
huffman@27289
   513
    show "\<exists>x. x \<in> compacts w"
huffman@27289
   514
      unfolding compacts_def
huffman@27289
   515
      apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
huffman@27289
   516
      apply (simp add: Abs_compact_basis_inverse approx_less)
huffman@27289
   517
      done
huffman@27289
   518
  next
huffman@27289
   519
    fix x y :: "'a compact_basis"
huffman@27289
   520
    assume "x \<in> compacts w" "y \<in> compacts w"
huffman@27289
   521
    thus "\<exists>z \<in> compacts w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
huffman@27289
   522
      unfolding compacts_def
huffman@27289
   523
      apply simp
huffman@27289
   524
      apply (cut_tac a=x in compact_Rep_compact_basis)
huffman@27289
   525
      apply (cut_tac a=y in compact_Rep_compact_basis)
huffman@27309
   526
      apply (drule profinite_compact_eq_approx)
huffman@27309
   527
      apply (drule profinite_compact_eq_approx)
huffman@27289
   528
      apply (clarify, rename_tac i j)
huffman@27289
   529
      apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
huffman@27289
   530
      apply (simp add: compact_le_def)
huffman@27289
   531
      apply (simp add: Abs_compact_basis_inverse approx_less)
huffman@27289
   532
      apply (erule subst, erule subst)
huffman@27289
   533
      apply (simp add: monofun_cfun chain_mono [OF chain_approx])
huffman@27289
   534
      done
huffman@27289
   535
  next
huffman@27289
   536
    fix x y :: "'a compact_basis"
huffman@27289
   537
    assume "x \<sqsubseteq> y" "y \<in> compacts w" thus "x \<in> compacts w"
huffman@27289
   538
      unfolding compacts_def
huffman@27289
   539
      apply simp
huffman@27289
   540
      apply (simp add: compact_le_def)
huffman@27289
   541
      apply (erule (1) trans_less)
huffman@27289
   542
      done
huffman@27289
   543
  qed
huffman@27289
   544
next
huffman@27297
   545
  fix Y :: "nat \<Rightarrow> 'a"
huffman@27297
   546
  assume Y: "chain Y"
huffman@27297
   547
  show "compacts (\<Squnion>i. Y i) = (\<Union>i. compacts (Y i))"
huffman@27289
   548
    unfolding compacts_def
huffman@27297
   549
    apply safe
huffman@27297
   550
    apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
huffman@27297
   551
    apply (erule trans_less, rule is_ub_thelub [OF Y])
huffman@27289
   552
    done
huffman@26420
   553
next
huffman@27289
   554
  fix a :: "'a compact_basis"
huffman@27289
   555
  show "compacts (Rep_compact_basis a) = {b. b \<sqsubseteq> a}"
huffman@27289
   556
    unfolding compacts_def compact_le_def ..
huffman@26420
   557
next
huffman@26420
   558
  fix x y :: "'a"
huffman@26420
   559
  assume "compacts x \<subseteq> compacts y" thus "x \<sqsubseteq> y"
huffman@27289
   560
    apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
huffman@27289
   561
    apply (rule admD, simp, simp)
huffman@27289
   562
    apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
huffman@27289
   563
    apply (simp add: compacts_def Abs_compact_basis_inverse approx_less)
huffman@27289
   564
    apply (simp add: compacts_def Abs_compact_basis_inverse)
huffman@27289
   565
    done
huffman@26420
   566
qed
huffman@25904
   567
huffman@27289
   568
text {* minimal compact element *}
huffman@27289
   569
huffman@27289
   570
definition
huffman@27289
   571
  compact_bot :: "'a::bifinite compact_basis" where
huffman@27289
   572
  "compact_bot = Abs_compact_basis \<bottom>"
huffman@27289
   573
huffman@27289
   574
lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \<bottom>"
huffman@27289
   575
unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse)
huffman@27289
   576
huffman@27289
   577
lemma compact_minimal [simp]: "compact_bot \<sqsubseteq> a"
huffman@27289
   578
unfolding compact_le_def Rep_compact_bot by simp
huffman@27289
   579
huffman@25904
   580
huffman@25904
   581
subsection {* A compact basis for powerdomains *}
huffman@25904
   582
huffman@25904
   583
typedef 'a pd_basis =
huffman@26407
   584
  "{S::'a::profinite compact_basis set. finite S \<and> S \<noteq> {}}"
huffman@25904
   585
by (rule_tac x="{arbitrary}" in exI, simp)
huffman@25904
   586
huffman@25904
   587
lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
huffman@25904
   588
by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
huffman@25904
   589
huffman@25904
   590
lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
huffman@25904
   591
by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
huffman@25904
   592
huffman@25904
   593
text {* unit and plus *}
huffman@25904
   594
huffman@25904
   595
definition
huffman@25904
   596
  PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
huffman@25904
   597
  "PDUnit = (\<lambda>x. Abs_pd_basis {x})"
huffman@25904
   598
huffman@25904
   599
definition
huffman@25904
   600
  PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
huffman@25904
   601
  "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)"
huffman@25904
   602
huffman@25904
   603
lemma Rep_PDUnit:
huffman@25904
   604
  "Rep_pd_basis (PDUnit x) = {x}"
huffman@25904
   605
unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
huffman@25904
   606
huffman@25904
   607
lemma Rep_PDPlus:
huffman@25904
   608
  "Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v"
huffman@25904
   609
unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
huffman@25904
   610
huffman@25904
   611
lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)"
huffman@25904
   612
unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp
huffman@25904
   613
huffman@25904
   614
lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)"
huffman@25904
   615
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc)
huffman@25904
   616
huffman@25904
   617
lemma PDPlus_commute: "PDPlus t u = PDPlus u t"
huffman@25904
   618
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute)
huffman@25904
   619
huffman@25904
   620
lemma PDPlus_absorb: "PDPlus t t = t"
huffman@25904
   621
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
huffman@25904
   622
huffman@25904
   623
lemma pd_basis_induct1:
huffman@25904
   624
  assumes PDUnit: "\<And>a. P (PDUnit a)"
huffman@25904
   625
  assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
huffman@25904
   626
  shows "P x"
huffman@25904
   627
apply (induct x, unfold pd_basis_def, clarify)
huffman@25904
   628
apply (erule (1) finite_ne_induct)
huffman@25904
   629
apply (cut_tac a=x in PDUnit)
huffman@25904
   630
apply (simp add: PDUnit_def)
huffman@25904
   631
apply (drule_tac a=x in PDPlus)
huffman@25904
   632
apply (simp add: PDUnit_def PDPlus_def Abs_pd_basis_inverse [unfolded pd_basis_def])
huffman@25904
   633
done
huffman@25904
   634
huffman@25904
   635
lemma pd_basis_induct:
huffman@25904
   636
  assumes PDUnit: "\<And>a. P (PDUnit a)"
huffman@25904
   637
  assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
huffman@25904
   638
  shows "P x"
huffman@25904
   639
apply (induct x rule: pd_basis_induct1)
huffman@25904
   640
apply (rule PDUnit, erule PDPlus [OF PDUnit])
huffman@25904
   641
done
huffman@25904
   642
huffman@25904
   643
text {* fold-pd *}
huffman@25904
   644
huffman@25904
   645
definition
huffman@25904
   646
  fold_pd ::
huffman@25904
   647
    "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
huffman@25904
   648
  where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
huffman@25904
   649
huffman@26927
   650
lemma fold_pd_PDUnit:
huffman@26927
   651
  includes ab_semigroup_idem_mult f
huffman@26927
   652
  shows "fold_pd g f (PDUnit x) = g x"
huffman@25904
   653
unfolding fold_pd_def Rep_PDUnit by simp
huffman@25904
   654
huffman@26927
   655
lemma fold_pd_PDPlus:
huffman@26927
   656
  includes ab_semigroup_idem_mult f
huffman@26927
   657
  shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
huffman@25904
   658
unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
huffman@25904
   659
huffman@25904
   660
text {* approx-pd *}
huffman@25904
   661
huffman@25904
   662
definition
huffman@25904
   663
  approx_pd :: "nat \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
huffman@25904
   664
  "approx_pd n = (\<lambda>t. Abs_pd_basis (compact_approx n ` Rep_pd_basis t))"
huffman@25904
   665
huffman@25904
   666
lemma Rep_approx_pd:
huffman@25904
   667
  "Rep_pd_basis (approx_pd n t) = compact_approx n ` Rep_pd_basis t"
huffman@25904
   668
unfolding approx_pd_def
huffman@25904
   669
apply (rule Abs_pd_basis_inverse)
huffman@25904
   670
apply (simp add: pd_basis_def)
huffman@25904
   671
done
huffman@25904
   672
huffman@25904
   673
lemma approx_pd_simps [simp]:
huffman@25904
   674
  "approx_pd n (PDUnit a) = PDUnit (compact_approx n a)"
huffman@25904
   675
  "approx_pd n (PDPlus t u) = PDPlus (approx_pd n t) (approx_pd n u)"
huffman@25904
   676
apply (simp_all add: Rep_pd_basis_inject [symmetric])
huffman@25904
   677
apply (simp_all add: Rep_approx_pd Rep_PDUnit Rep_PDPlus image_Un)
huffman@25904
   678
done
huffman@25904
   679
huffman@25904
   680
lemma approx_pd_idem: "approx_pd n (approx_pd n t) = approx_pd n t"
huffman@25904
   681
apply (induct t rule: pd_basis_induct)
huffman@27289
   682
apply (simp add: compact_basis.take_take)
huffman@25904
   683
apply simp
huffman@25904
   684
done
huffman@25904
   685
huffman@25904
   686
lemma finite_range_approx_pd: "finite (range (approx_pd n))"
huffman@27289
   687
apply (rule finite_imageD [where f="Rep_pd_basis"])
huffman@27289
   688
apply (rule finite_subset [where B="Pow (range (compact_approx n))"])
huffman@27289
   689
apply (clarsimp simp add: Rep_approx_pd)
huffman@27289
   690
apply (simp add: compact_basis.finite_range_take)
huffman@25904
   691
apply (rule inj_onI, simp add: Rep_pd_basis_inject)
huffman@25904
   692
done
huffman@25904
   693
huffman@27289
   694
lemma approx_pd_covers: "\<exists>n. approx_pd n t = t"
huffman@25904
   695
apply (subgoal_tac "\<exists>n. \<forall>m\<ge>n. approx_pd m t = t", fast)
huffman@25904
   696
apply (induct t rule: pd_basis_induct)
huffman@27289
   697
apply (cut_tac a=a in compact_basis.take_covers)
huffman@25904
   698
apply (clarify, rule_tac x=n in exI)
huffman@25904
   699
apply (clarify, simp)
huffman@26420
   700
apply (rule antisym_less)
huffman@27289
   701
apply (rule compact_basis.take_less)
huffman@27289
   702
apply (drule_tac a=a in compact_basis.take_chain_le)
huffman@25904
   703
apply simp
huffman@25904
   704
apply (clarify, rename_tac i j)
huffman@25904
   705
apply (rule_tac x="max i j" in exI, simp)
huffman@25904
   706
done
huffman@25904
   707
huffman@25904
   708
end