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