src/HOLCF/ConvexPD.thy
author huffman
Fri Jun 20 22:51:50 2008 +0200 (2008-06-20)
changeset 27309 c74270fd72a8
parent 27297 2c42b1505f25
child 27310 d0229bc6c461
permissions -rw-r--r--
clean up and rename some profinite lemmas
     1 (*  Title:      HOLCF/ConvexPD.thy
     2     ID:         $Id$
     3     Author:     Brian Huffman
     4 *)
     5 
     6 header {* Convex powerdomain *}
     7 
     8 theory ConvexPD
     9 imports UpperPD LowerPD
    10 begin
    11 
    12 subsection {* Basis preorder *}
    13 
    14 definition
    15   convex_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<natural>" 50) where
    16   "convex_le = (\<lambda>u v. u \<le>\<sharp> v \<and> u \<le>\<flat> v)"
    17 
    18 lemma convex_le_refl [simp]: "t \<le>\<natural> t"
    19 unfolding convex_le_def by (fast intro: upper_le_refl lower_le_refl)
    20 
    21 lemma convex_le_trans: "\<lbrakk>t \<le>\<natural> u; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> t \<le>\<natural> v"
    22 unfolding convex_le_def by (fast intro: upper_le_trans lower_le_trans)
    23 
    24 interpretation convex_le: preorder [convex_le]
    25 by (rule preorder.intro, rule convex_le_refl, rule convex_le_trans)
    26 
    27 lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<natural> t"
    28 unfolding convex_le_def Rep_PDUnit by simp
    29 
    30 lemma PDUnit_convex_mono: "x \<sqsubseteq> y \<Longrightarrow> PDUnit x \<le>\<natural> PDUnit y"
    31 unfolding convex_le_def by (fast intro: PDUnit_upper_mono PDUnit_lower_mono)
    32 
    33 lemma PDPlus_convex_mono: "\<lbrakk>s \<le>\<natural> t; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<natural> PDPlus t v"
    34 unfolding convex_le_def by (fast intro: PDPlus_upper_mono PDPlus_lower_mono)
    35 
    36 lemma convex_le_PDUnit_PDUnit_iff [simp]:
    37   "(PDUnit a \<le>\<natural> PDUnit b) = a \<sqsubseteq> b"
    38 unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit by fast
    39 
    40 lemma convex_le_PDUnit_lemma1:
    41   "(PDUnit a \<le>\<natural> t) = (\<forall>b\<in>Rep_pd_basis t. a \<sqsubseteq> b)"
    42 unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit
    43 using Rep_pd_basis_nonempty [of t, folded ex_in_conv] by fast
    44 
    45 lemma convex_le_PDUnit_PDPlus_iff [simp]:
    46   "(PDUnit a \<le>\<natural> PDPlus t u) = (PDUnit a \<le>\<natural> t \<and> PDUnit a \<le>\<natural> u)"
    47 unfolding convex_le_PDUnit_lemma1 Rep_PDPlus by fast
    48 
    49 lemma convex_le_PDUnit_lemma2:
    50   "(t \<le>\<natural> PDUnit b) = (\<forall>a\<in>Rep_pd_basis t. a \<sqsubseteq> b)"
    51 unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit
    52 using Rep_pd_basis_nonempty [of t, folded ex_in_conv] by fast
    53 
    54 lemma convex_le_PDPlus_PDUnit_iff [simp]:
    55   "(PDPlus t u \<le>\<natural> PDUnit a) = (t \<le>\<natural> PDUnit a \<and> u \<le>\<natural> PDUnit a)"
    56 unfolding convex_le_PDUnit_lemma2 Rep_PDPlus by fast
    57 
    58 lemma convex_le_PDPlus_lemma:
    59   assumes z: "PDPlus t u \<le>\<natural> z"
    60   shows "\<exists>v w. z = PDPlus v w \<and> t \<le>\<natural> v \<and> u \<le>\<natural> w"
    61 proof (intro exI conjI)
    62   let ?A = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis t. a \<sqsubseteq> b}"
    63   let ?B = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis u. a \<sqsubseteq> b}"
    64   let ?v = "Abs_pd_basis ?A"
    65   let ?w = "Abs_pd_basis ?B"
    66   have Rep_v: "Rep_pd_basis ?v = ?A"
    67     apply (rule Abs_pd_basis_inverse)
    68     apply (rule Rep_pd_basis_nonempty [of t, folded ex_in_conv, THEN exE])
    69     apply (cut_tac z, simp only: convex_le_def lower_le_def, clarify)
    70     apply (drule_tac x=x in bspec, simp add: Rep_PDPlus, erule bexE)
    71     apply (simp add: pd_basis_def)
    72     apply fast
    73     done
    74   have Rep_w: "Rep_pd_basis ?w = ?B"
    75     apply (rule Abs_pd_basis_inverse)
    76     apply (rule Rep_pd_basis_nonempty [of u, folded ex_in_conv, THEN exE])
    77     apply (cut_tac z, simp only: convex_le_def lower_le_def, clarify)
    78     apply (drule_tac x=x in bspec, simp add: Rep_PDPlus, erule bexE)
    79     apply (simp add: pd_basis_def)
    80     apply fast
    81     done
    82   show "z = PDPlus ?v ?w"
    83     apply (insert z)
    84     apply (simp add: convex_le_def, erule conjE)
    85     apply (simp add: Rep_pd_basis_inject [symmetric] Rep_PDPlus)
    86     apply (simp add: Rep_v Rep_w)
    87     apply (rule equalityI)
    88      apply (rule subsetI)
    89      apply (simp only: upper_le_def)
    90      apply (drule (1) bspec, erule bexE)
    91      apply (simp add: Rep_PDPlus)
    92      apply fast
    93     apply fast
    94     done
    95   show "t \<le>\<natural> ?v" "u \<le>\<natural> ?w"
    96    apply (insert z)
    97    apply (simp_all add: convex_le_def upper_le_def lower_le_def Rep_PDPlus Rep_v Rep_w)
    98    apply fast+
    99    done
   100 qed
   101 
   102 lemma convex_le_induct [induct set: convex_le]:
   103   assumes le: "t \<le>\<natural> u"
   104   assumes 2: "\<And>t u v. \<lbrakk>P t u; P u v\<rbrakk> \<Longrightarrow> P t v"
   105   assumes 3: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
   106   assumes 4: "\<And>t u v w. \<lbrakk>P t v; P u w\<rbrakk> \<Longrightarrow> P (PDPlus t u) (PDPlus v w)"
   107   shows "P t u"
   108 using le apply (induct t arbitrary: u rule: pd_basis_induct)
   109 apply (erule rev_mp)
   110 apply (induct_tac u rule: pd_basis_induct1)
   111 apply (simp add: 3)
   112 apply (simp, clarify, rename_tac a b t)
   113 apply (subgoal_tac "P (PDPlus (PDUnit a) (PDUnit a)) (PDPlus (PDUnit b) t)")
   114 apply (simp add: PDPlus_absorb)
   115 apply (erule (1) 4 [OF 3])
   116 apply (drule convex_le_PDPlus_lemma, clarify)
   117 apply (simp add: 4)
   118 done
   119 
   120 lemma approx_pd_convex_chain:
   121   "approx_pd n t \<le>\<natural> approx_pd (Suc n) t"
   122 apply (induct t rule: pd_basis_induct)
   123 apply (simp add: compact_basis.take_chain)
   124 apply (simp add: PDPlus_convex_mono)
   125 done
   126 
   127 lemma approx_pd_convex_le: "approx_pd i t \<le>\<natural> t"
   128 apply (induct t rule: pd_basis_induct)
   129 apply (simp add: compact_basis.take_less)
   130 apply (simp add: PDPlus_convex_mono)
   131 done
   132 
   133 lemma approx_pd_convex_mono:
   134   "t \<le>\<natural> u \<Longrightarrow> approx_pd n t \<le>\<natural> approx_pd n u"
   135 apply (erule convex_le_induct)
   136 apply (erule (1) convex_le_trans)
   137 apply (simp add: compact_basis.take_mono)
   138 apply (simp add: PDPlus_convex_mono)
   139 done
   140 
   141 
   142 subsection {* Type definition *}
   143 
   144 cpodef (open) 'a convex_pd =
   145   "{S::'a pd_basis cset. convex_le.ideal (Rep_cset S)}"
   146 by (rule convex_le.cpodef_ideal_lemma)
   147 
   148 lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_cset (Rep_convex_pd xs))"
   149 by (rule Rep_convex_pd [unfolded mem_Collect_eq])
   150 
   151 definition
   152   convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where
   153   "convex_principal t = Abs_convex_pd (Abs_cset {u. u \<le>\<natural> t})"
   154 
   155 lemma Rep_convex_principal:
   156   "Rep_cset (Rep_convex_pd (convex_principal t)) = {u. u \<le>\<natural> t}"
   157 unfolding convex_principal_def
   158 by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
   159 
   160 interpretation convex_pd:
   161   ideal_completion
   162     [convex_le approx_pd convex_principal "\<lambda>x. Rep_cset (Rep_convex_pd x)"]
   163 apply unfold_locales
   164 apply (rule approx_pd_convex_le)
   165 apply (rule approx_pd_idem)
   166 apply (erule approx_pd_convex_mono)
   167 apply (rule approx_pd_convex_chain)
   168 apply (rule finite_range_approx_pd)
   169 apply (rule approx_pd_covers)
   170 apply (rule ideal_Rep_convex_pd)
   171 apply (simp add: cont2contlubE [OF cont_Rep_convex_pd] Rep_cset_lub)
   172 apply (rule Rep_convex_principal)
   173 apply (simp only: less_convex_pd_def sq_le_cset_def)
   174 done
   175 
   176 text {* Convex powerdomain is pointed *}
   177 
   178 lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys"
   179 by (induct ys rule: convex_pd.principal_induct, simp, simp)
   180 
   181 instance convex_pd :: (bifinite) pcpo
   182 by intro_classes (fast intro: convex_pd_minimal)
   183 
   184 lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
   185 by (rule convex_pd_minimal [THEN UU_I, symmetric])
   186 
   187 text {* Convex powerdomain is profinite *}
   188 
   189 instantiation convex_pd :: (profinite) profinite
   190 begin
   191 
   192 definition
   193   approx_convex_pd_def: "approx = convex_pd.completion_approx"
   194 
   195 instance
   196 apply (intro_classes, unfold approx_convex_pd_def)
   197 apply (simp add: convex_pd.chain_completion_approx)
   198 apply (rule convex_pd.lub_completion_approx)
   199 apply (rule convex_pd.completion_approx_idem)
   200 apply (rule convex_pd.finite_fixes_completion_approx)
   201 done
   202 
   203 end
   204 
   205 instance convex_pd :: (bifinite) bifinite ..
   206 
   207 lemma approx_convex_principal [simp]:
   208   "approx n\<cdot>(convex_principal t) = convex_principal (approx_pd n t)"
   209 unfolding approx_convex_pd_def
   210 by (rule convex_pd.completion_approx_principal)
   211 
   212 lemma approx_eq_convex_principal:
   213   "\<exists>t\<in>Rep_cset (Rep_convex_pd xs).
   214     approx n\<cdot>xs = convex_principal (approx_pd n t)"
   215 unfolding approx_convex_pd_def
   216 by (rule convex_pd.completion_approx_eq_principal)
   217 
   218 
   219 subsection {* Monadic unit and plus *}
   220 
   221 definition
   222   convex_unit :: "'a \<rightarrow> 'a convex_pd" where
   223   "convex_unit = compact_basis.basis_fun (\<lambda>a. convex_principal (PDUnit a))"
   224 
   225 definition
   226   convex_plus :: "'a convex_pd \<rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd" where
   227   "convex_plus = convex_pd.basis_fun (\<lambda>t. convex_pd.basis_fun (\<lambda>u.
   228       convex_principal (PDPlus t u)))"
   229 
   230 abbreviation
   231   convex_add :: "'a convex_pd \<Rightarrow> 'a convex_pd \<Rightarrow> 'a convex_pd"
   232     (infixl "+\<natural>" 65) where
   233   "xs +\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
   234 
   235 syntax
   236   "_convex_pd" :: "args \<Rightarrow> 'a convex_pd" ("{_}\<natural>")
   237 
   238 translations
   239   "{x,xs}\<natural>" == "{x}\<natural> +\<natural> {xs}\<natural>"
   240   "{x}\<natural>" == "CONST convex_unit\<cdot>x"
   241 
   242 lemma convex_unit_Rep_compact_basis [simp]:
   243   "{Rep_compact_basis a}\<natural> = convex_principal (PDUnit a)"
   244 unfolding convex_unit_def
   245 by (simp add: compact_basis.basis_fun_principal PDUnit_convex_mono)
   246 
   247 lemma convex_plus_principal [simp]:
   248   "convex_principal t +\<natural> convex_principal u = convex_principal (PDPlus t u)"
   249 unfolding convex_plus_def
   250 by (simp add: convex_pd.basis_fun_principal
   251     convex_pd.basis_fun_mono PDPlus_convex_mono)
   252 
   253 lemma approx_convex_unit [simp]:
   254   "approx n\<cdot>{x}\<natural> = {approx n\<cdot>x}\<natural>"
   255 apply (induct x rule: compact_basis.principal_induct, simp)
   256 apply (simp add: approx_Rep_compact_basis)
   257 done
   258 
   259 lemma approx_convex_plus [simp]:
   260   "approx n\<cdot>(xs +\<natural> ys) = approx n\<cdot>xs +\<natural> approx n\<cdot>ys"
   261 by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
   262 
   263 lemma convex_plus_assoc:
   264   "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)"
   265 apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp)
   266 apply (rule_tac x=zs in convex_pd.principal_induct, simp)
   267 apply (simp add: PDPlus_assoc)
   268 done
   269 
   270 lemma convex_plus_commute: "xs +\<natural> ys = ys +\<natural> xs"
   271 apply (induct xs ys rule: convex_pd.principal_induct2, simp, simp)
   272 apply (simp add: PDPlus_commute)
   273 done
   274 
   275 lemma convex_plus_absorb: "xs +\<natural> xs = xs"
   276 apply (induct xs rule: convex_pd.principal_induct, simp)
   277 apply (simp add: PDPlus_absorb)
   278 done
   279 
   280 interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"]
   281   by unfold_locales
   282     (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
   283 
   284 lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)"
   285 by (rule aci_convex_plus.mult_left_commute)
   286 
   287 lemma convex_plus_left_absorb: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> ys"
   288 by (rule aci_convex_plus.mult_left_idem)
   289 
   290 lemmas convex_plus_aci = aci_convex_plus.mult_ac_idem
   291 
   292 lemma convex_unit_less_plus_iff [simp]:
   293   "{x}\<natural> \<sqsubseteq> ys +\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs"
   294  apply (rule iffI)
   295   apply (subgoal_tac
   296     "adm (\<lambda>f. f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>ys \<and> f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>zs)")
   297    apply (drule admD, rule chain_approx)
   298     apply (drule_tac f="approx i" in monofun_cfun_arg)
   299     apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   300     apply (cut_tac x="approx i\<cdot>ys" in convex_pd.compact_imp_principal, simp)
   301     apply (cut_tac x="approx i\<cdot>zs" in convex_pd.compact_imp_principal, simp)
   302     apply (clarify, simp)
   303    apply simp
   304   apply simp
   305  apply (erule conjE)
   306  apply (subst convex_plus_absorb [of "{x}\<natural>", symmetric])
   307  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
   308 done
   309 
   310 lemma convex_plus_less_unit_iff [simp]:
   311   "xs +\<natural> ys \<sqsubseteq> {z}\<natural> \<longleftrightarrow> xs \<sqsubseteq> {z}\<natural> \<and> ys \<sqsubseteq> {z}\<natural>"
   312  apply (rule iffI)
   313   apply (subgoal_tac
   314     "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>{z}\<natural> \<and> f\<cdot>ys \<sqsubseteq> f\<cdot>{z}\<natural>)")
   315    apply (drule admD, rule chain_approx)
   316     apply (drule_tac f="approx i" in monofun_cfun_arg)
   317     apply (cut_tac x="approx i\<cdot>xs" in convex_pd.compact_imp_principal, simp)
   318     apply (cut_tac x="approx i\<cdot>ys" in convex_pd.compact_imp_principal, simp)
   319     apply (cut_tac x="approx i\<cdot>z" in compact_basis.compact_imp_principal, simp)
   320     apply (clarify, simp)
   321    apply simp
   322   apply simp
   323  apply (erule conjE)
   324  apply (subst convex_plus_absorb [of "{z}\<natural>", symmetric])
   325  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
   326 done
   327 
   328 lemma convex_unit_less_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y"
   329  apply (rule iffI)
   330   apply (rule profinite_less_ext)
   331   apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   332   apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   333   apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
   334   apply clarsimp
   335  apply (erule monofun_cfun_arg)
   336 done
   337 
   338 lemma convex_unit_eq_iff [simp]: "{x}\<natural> = {y}\<natural> \<longleftrightarrow> x = y"
   339 unfolding po_eq_conv by simp
   340 
   341 lemma convex_unit_strict [simp]: "{\<bottom>}\<natural> = \<bottom>"
   342 unfolding inst_convex_pd_pcpo Rep_compact_bot [symmetric] by simp
   343 
   344 lemma convex_unit_strict_iff [simp]: "{x}\<natural> = \<bottom> \<longleftrightarrow> x = \<bottom>"
   345 unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff)
   346 
   347 lemma compact_convex_unit_iff [simp]:
   348   "compact {x}\<natural> \<longleftrightarrow> compact x"
   349 unfolding profinite_compact_iff by simp
   350 
   351 lemma compact_convex_plus [simp]:
   352   "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<natural> ys)"
   353 by (auto dest!: convex_pd.compact_imp_principal)
   354 
   355 
   356 subsection {* Induction rules *}
   357 
   358 lemma convex_pd_induct1:
   359   assumes P: "adm P"
   360   assumes unit: "\<And>x. P {x}\<natural>"
   361   assumes insert: "\<And>x ys. \<lbrakk>P {x}\<natural>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<natural> +\<natural> ys)"
   362   shows "P (xs::'a convex_pd)"
   363 apply (induct xs rule: convex_pd.principal_induct, rule P)
   364 apply (induct_tac a rule: pd_basis_induct1)
   365 apply (simp only: convex_unit_Rep_compact_basis [symmetric])
   366 apply (rule unit)
   367 apply (simp only: convex_unit_Rep_compact_basis [symmetric]
   368                   convex_plus_principal [symmetric])
   369 apply (erule insert [OF unit])
   370 done
   371 
   372 lemma convex_pd_induct:
   373   assumes P: "adm P"
   374   assumes unit: "\<And>x. P {x}\<natural>"
   375   assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<natural> ys)"
   376   shows "P (xs::'a convex_pd)"
   377 apply (induct xs rule: convex_pd.principal_induct, rule P)
   378 apply (induct_tac a rule: pd_basis_induct)
   379 apply (simp only: convex_unit_Rep_compact_basis [symmetric] unit)
   380 apply (simp only: convex_plus_principal [symmetric] plus)
   381 done
   382 
   383 
   384 subsection {* Monadic bind *}
   385 
   386 definition
   387   convex_bind_basis ::
   388   "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
   389   "convex_bind_basis = fold_pd
   390     (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
   391     (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
   392 
   393 lemma ACI_convex_bind:
   394   "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
   395 apply unfold_locales
   396 apply (simp add: convex_plus_assoc)
   397 apply (simp add: convex_plus_commute)
   398 apply (simp add: convex_plus_absorb eta_cfun)
   399 done
   400 
   401 lemma convex_bind_basis_simps [simp]:
   402   "convex_bind_basis (PDUnit a) =
   403     (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   404   "convex_bind_basis (PDPlus t u) =
   405     (\<Lambda> f. convex_bind_basis t\<cdot>f +\<natural> convex_bind_basis u\<cdot>f)"
   406 unfolding convex_bind_basis_def
   407 apply -
   408 apply (rule fold_pd_PDUnit [OF ACI_convex_bind])
   409 apply (rule fold_pd_PDPlus [OF ACI_convex_bind])
   410 done
   411 
   412 lemma monofun_LAM:
   413   "\<lbrakk>cont f; cont g; \<And>x. f x \<sqsubseteq> g x\<rbrakk> \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)"
   414 by (simp add: expand_cfun_less)
   415 
   416 lemma convex_bind_basis_mono:
   417   "t \<le>\<natural> u \<Longrightarrow> convex_bind_basis t \<sqsubseteq> convex_bind_basis u"
   418 apply (erule convex_le_induct)
   419 apply (erule (1) trans_less)
   420 apply (simp add: monofun_LAM monofun_cfun)
   421 apply (simp add: monofun_LAM monofun_cfun)
   422 done
   423 
   424 definition
   425   convex_bind :: "'a convex_pd \<rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
   426   "convex_bind = convex_pd.basis_fun convex_bind_basis"
   427 
   428 lemma convex_bind_principal [simp]:
   429   "convex_bind\<cdot>(convex_principal t) = convex_bind_basis t"
   430 unfolding convex_bind_def
   431 apply (rule convex_pd.basis_fun_principal)
   432 apply (erule convex_bind_basis_mono)
   433 done
   434 
   435 lemma convex_bind_unit [simp]:
   436   "convex_bind\<cdot>{x}\<natural>\<cdot>f = f\<cdot>x"
   437 by (induct x rule: compact_basis.principal_induct, simp, simp)
   438 
   439 lemma convex_bind_plus [simp]:
   440   "convex_bind\<cdot>(xs +\<natural> ys)\<cdot>f = convex_bind\<cdot>xs\<cdot>f +\<natural> convex_bind\<cdot>ys\<cdot>f"
   441 by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
   442 
   443 lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   444 unfolding convex_unit_strict [symmetric] by (rule convex_bind_unit)
   445 
   446 
   447 subsection {* Map and join *}
   448 
   449 definition
   450   convex_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a convex_pd \<rightarrow> 'b convex_pd" where
   451   "convex_map = (\<Lambda> f xs. convex_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<natural>))"
   452 
   453 definition
   454   convex_join :: "'a convex_pd convex_pd \<rightarrow> 'a convex_pd" where
   455   "convex_join = (\<Lambda> xss. convex_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
   456 
   457 lemma convex_map_unit [simp]:
   458   "convex_map\<cdot>f\<cdot>(convex_unit\<cdot>x) = convex_unit\<cdot>(f\<cdot>x)"
   459 unfolding convex_map_def by simp
   460 
   461 lemma convex_map_plus [simp]:
   462   "convex_map\<cdot>f\<cdot>(xs +\<natural> ys) = convex_map\<cdot>f\<cdot>xs +\<natural> convex_map\<cdot>f\<cdot>ys"
   463 unfolding convex_map_def by simp
   464 
   465 lemma convex_join_unit [simp]:
   466   "convex_join\<cdot>{xs}\<natural> = xs"
   467 unfolding convex_join_def by simp
   468 
   469 lemma convex_join_plus [simp]:
   470   "convex_join\<cdot>(xss +\<natural> yss) = convex_join\<cdot>xss +\<natural> convex_join\<cdot>yss"
   471 unfolding convex_join_def by simp
   472 
   473 lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
   474 by (induct xs rule: convex_pd_induct, simp_all)
   475 
   476 lemma convex_map_map:
   477   "convex_map\<cdot>f\<cdot>(convex_map\<cdot>g\<cdot>xs) = convex_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
   478 by (induct xs rule: convex_pd_induct, simp_all)
   479 
   480 lemma convex_join_map_unit:
   481   "convex_join\<cdot>(convex_map\<cdot>convex_unit\<cdot>xs) = xs"
   482 by (induct xs rule: convex_pd_induct, simp_all)
   483 
   484 lemma convex_join_map_join:
   485   "convex_join\<cdot>(convex_map\<cdot>convex_join\<cdot>xsss) = convex_join\<cdot>(convex_join\<cdot>xsss)"
   486 by (induct xsss rule: convex_pd_induct, simp_all)
   487 
   488 lemma convex_join_map_map:
   489   "convex_join\<cdot>(convex_map\<cdot>(convex_map\<cdot>f)\<cdot>xss) =
   490    convex_map\<cdot>f\<cdot>(convex_join\<cdot>xss)"
   491 by (induct xss rule: convex_pd_induct, simp_all)
   492 
   493 lemma convex_map_approx: "convex_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs"
   494 by (induct xs rule: convex_pd_induct, simp_all)
   495 
   496 
   497 subsection {* Conversions to other powerdomains *}
   498 
   499 text {* Convex to upper *}
   500 
   501 lemma convex_le_imp_upper_le: "t \<le>\<natural> u \<Longrightarrow> t \<le>\<sharp> u"
   502 unfolding convex_le_def by simp
   503 
   504 definition
   505   convex_to_upper :: "'a convex_pd \<rightarrow> 'a upper_pd" where
   506   "convex_to_upper = convex_pd.basis_fun upper_principal"
   507 
   508 lemma convex_to_upper_principal [simp]:
   509   "convex_to_upper\<cdot>(convex_principal t) = upper_principal t"
   510 unfolding convex_to_upper_def
   511 apply (rule convex_pd.basis_fun_principal)
   512 apply (rule upper_pd.principal_mono)
   513 apply (erule convex_le_imp_upper_le)
   514 done
   515 
   516 lemma convex_to_upper_unit [simp]:
   517   "convex_to_upper\<cdot>{x}\<natural> = {x}\<sharp>"
   518 by (induct x rule: compact_basis.principal_induct, simp, simp)
   519 
   520 lemma convex_to_upper_plus [simp]:
   521   "convex_to_upper\<cdot>(xs +\<natural> ys) = convex_to_upper\<cdot>xs +\<sharp> convex_to_upper\<cdot>ys"
   522 by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
   523 
   524 lemma approx_convex_to_upper:
   525   "approx i\<cdot>(convex_to_upper\<cdot>xs) = convex_to_upper\<cdot>(approx i\<cdot>xs)"
   526 by (induct xs rule: convex_pd_induct, simp, simp, simp)
   527 
   528 lemma convex_to_upper_bind [simp]:
   529   "convex_to_upper\<cdot>(convex_bind\<cdot>xs\<cdot>f) =
   530     upper_bind\<cdot>(convex_to_upper\<cdot>xs)\<cdot>(convex_to_upper oo f)"
   531 by (induct xs rule: convex_pd_induct, simp, simp, simp)
   532 
   533 lemma convex_to_upper_map [simp]:
   534   "convex_to_upper\<cdot>(convex_map\<cdot>f\<cdot>xs) = upper_map\<cdot>f\<cdot>(convex_to_upper\<cdot>xs)"
   535 by (simp add: convex_map_def upper_map_def cfcomp_LAM)
   536 
   537 lemma convex_to_upper_join [simp]:
   538   "convex_to_upper\<cdot>(convex_join\<cdot>xss) =
   539     upper_bind\<cdot>(convex_to_upper\<cdot>xss)\<cdot>convex_to_upper"
   540 by (simp add: convex_join_def upper_join_def cfcomp_LAM eta_cfun)
   541 
   542 text {* Convex to lower *}
   543 
   544 lemma convex_le_imp_lower_le: "t \<le>\<natural> u \<Longrightarrow> t \<le>\<flat> u"
   545 unfolding convex_le_def by simp
   546 
   547 definition
   548   convex_to_lower :: "'a convex_pd \<rightarrow> 'a lower_pd" where
   549   "convex_to_lower = convex_pd.basis_fun lower_principal"
   550 
   551 lemma convex_to_lower_principal [simp]:
   552   "convex_to_lower\<cdot>(convex_principal t) = lower_principal t"
   553 unfolding convex_to_lower_def
   554 apply (rule convex_pd.basis_fun_principal)
   555 apply (rule lower_pd.principal_mono)
   556 apply (erule convex_le_imp_lower_le)
   557 done
   558 
   559 lemma convex_to_lower_unit [simp]:
   560   "convex_to_lower\<cdot>{x}\<natural> = {x}\<flat>"
   561 by (induct x rule: compact_basis.principal_induct, simp, simp)
   562 
   563 lemma convex_to_lower_plus [simp]:
   564   "convex_to_lower\<cdot>(xs +\<natural> ys) = convex_to_lower\<cdot>xs +\<flat> convex_to_lower\<cdot>ys"
   565 by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
   566 
   567 lemma approx_convex_to_lower:
   568   "approx i\<cdot>(convex_to_lower\<cdot>xs) = convex_to_lower\<cdot>(approx i\<cdot>xs)"
   569 by (induct xs rule: convex_pd_induct, simp, simp, simp)
   570 
   571 lemma convex_to_lower_bind [simp]:
   572   "convex_to_lower\<cdot>(convex_bind\<cdot>xs\<cdot>f) =
   573     lower_bind\<cdot>(convex_to_lower\<cdot>xs)\<cdot>(convex_to_lower oo f)"
   574 by (induct xs rule: convex_pd_induct, simp, simp, simp)
   575 
   576 lemma convex_to_lower_map [simp]:
   577   "convex_to_lower\<cdot>(convex_map\<cdot>f\<cdot>xs) = lower_map\<cdot>f\<cdot>(convex_to_lower\<cdot>xs)"
   578 by (simp add: convex_map_def lower_map_def cfcomp_LAM)
   579 
   580 lemma convex_to_lower_join [simp]:
   581   "convex_to_lower\<cdot>(convex_join\<cdot>xss) =
   582     lower_bind\<cdot>(convex_to_lower\<cdot>xss)\<cdot>convex_to_lower"
   583 by (simp add: convex_join_def lower_join_def cfcomp_LAM eta_cfun)
   584 
   585 text {* Ordering property *}
   586 
   587 lemma convex_pd_less_iff:
   588   "(xs \<sqsubseteq> ys) =
   589     (convex_to_upper\<cdot>xs \<sqsubseteq> convex_to_upper\<cdot>ys \<and>
   590      convex_to_lower\<cdot>xs \<sqsubseteq> convex_to_lower\<cdot>ys)"
   591  apply (safe elim!: monofun_cfun_arg)
   592  apply (rule profinite_less_ext)
   593  apply (drule_tac f="approx i" in monofun_cfun_arg)
   594  apply (drule_tac f="approx i" in monofun_cfun_arg)
   595  apply (cut_tac x="approx i\<cdot>xs" in convex_pd.compact_imp_principal, simp)
   596  apply (cut_tac x="approx i\<cdot>ys" in convex_pd.compact_imp_principal, simp)
   597  apply clarify
   598  apply (simp add: approx_convex_to_upper approx_convex_to_lower convex_le_def)
   599 done
   600 
   601 lemmas convex_plus_less_plus_iff =
   602   convex_pd_less_iff [where xs="xs +\<natural> ys" and ys="zs +\<natural> ws", standard]
   603 
   604 lemmas convex_pd_less_simps =
   605   convex_unit_less_plus_iff
   606   convex_plus_less_unit_iff
   607   convex_plus_less_plus_iff
   608   convex_unit_less_iff
   609   convex_to_upper_unit
   610   convex_to_upper_plus
   611   convex_to_lower_unit
   612   convex_to_lower_plus
   613   upper_pd_less_simps
   614   lower_pd_less_simps
   615 
   616 end