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