src/HOLCF/ConvexPD.thy
author huffman
Thu Jun 26 17:54:05 2008 +0200 (2008-06-26)
changeset 27373 5794a0e3e26c
parent 27310 d0229bc6c461
child 27405 785f5dbec8f4
permissions -rw-r--r--
remove cset theory; define ideal completions using typedef instead of cpodef
     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 typedef (open) 'a convex_pd =
   145   "{S::'a pd_basis set. convex_le.ideal S}"
   146 by (fast intro: convex_le.ideal_principal)
   147 
   148 instantiation convex_pd :: (profinite) sq_ord
   149 begin
   150 
   151 definition
   152   "x \<sqsubseteq> y \<longleftrightarrow> Rep_convex_pd x \<subseteq> Rep_convex_pd y"
   153 
   154 instance ..
   155 end
   156 
   157 instance convex_pd :: (profinite) po
   158 by (rule convex_le.typedef_ideal_po
   159     [OF type_definition_convex_pd sq_le_convex_pd_def])
   160 
   161 instance convex_pd :: (profinite) cpo
   162 by (rule convex_le.typedef_ideal_cpo
   163     [OF type_definition_convex_pd sq_le_convex_pd_def])
   164 
   165 lemma Rep_convex_pd_lub:
   166   "chain Y \<Longrightarrow> Rep_convex_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_convex_pd (Y i))"
   167 by (rule convex_le.typedef_ideal_rep_contlub
   168     [OF type_definition_convex_pd sq_le_convex_pd_def])
   169 
   170 lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)"
   171 by (rule Rep_convex_pd [unfolded mem_Collect_eq])
   172 
   173 definition
   174   convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where
   175   "convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}"
   176 
   177 lemma Rep_convex_principal:
   178   "Rep_convex_pd (convex_principal t) = {u. u \<le>\<natural> t}"
   179 unfolding convex_principal_def
   180 by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
   181 
   182 interpretation convex_pd:
   183   ideal_completion [convex_le approx_pd convex_principal Rep_convex_pd]
   184 apply unfold_locales
   185 apply (rule approx_pd_convex_le)
   186 apply (rule approx_pd_idem)
   187 apply (erule approx_pd_convex_mono)
   188 apply (rule approx_pd_convex_chain)
   189 apply (rule finite_range_approx_pd)
   190 apply (rule approx_pd_covers)
   191 apply (rule ideal_Rep_convex_pd)
   192 apply (erule Rep_convex_pd_lub)
   193 apply (rule Rep_convex_principal)
   194 apply (simp only: sq_le_convex_pd_def)
   195 done
   196 
   197 text {* Convex powerdomain is pointed *}
   198 
   199 lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys"
   200 by (induct ys rule: convex_pd.principal_induct, simp, simp)
   201 
   202 instance convex_pd :: (bifinite) pcpo
   203 by intro_classes (fast intro: convex_pd_minimal)
   204 
   205 lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
   206 by (rule convex_pd_minimal [THEN UU_I, symmetric])
   207 
   208 text {* Convex powerdomain is profinite *}
   209 
   210 instantiation convex_pd :: (profinite) profinite
   211 begin
   212 
   213 definition
   214   approx_convex_pd_def: "approx = convex_pd.completion_approx"
   215 
   216 instance
   217 apply (intro_classes, unfold approx_convex_pd_def)
   218 apply (rule convex_pd.chain_completion_approx)
   219 apply (rule convex_pd.lub_completion_approx)
   220 apply (rule convex_pd.completion_approx_idem)
   221 apply (rule convex_pd.finite_fixes_completion_approx)
   222 done
   223 
   224 end
   225 
   226 instance convex_pd :: (bifinite) bifinite ..
   227 
   228 lemma approx_convex_principal [simp]:
   229   "approx n\<cdot>(convex_principal t) = convex_principal (approx_pd n t)"
   230 unfolding approx_convex_pd_def
   231 by (rule convex_pd.completion_approx_principal)
   232 
   233 lemma approx_eq_convex_principal:
   234   "\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (approx_pd n t)"
   235 unfolding approx_convex_pd_def
   236 by (rule convex_pd.completion_approx_eq_principal)
   237 
   238 
   239 subsection {* Monadic unit and plus *}
   240 
   241 definition
   242   convex_unit :: "'a \<rightarrow> 'a convex_pd" where
   243   "convex_unit = compact_basis.basis_fun (\<lambda>a. convex_principal (PDUnit a))"
   244 
   245 definition
   246   convex_plus :: "'a convex_pd \<rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd" where
   247   "convex_plus = convex_pd.basis_fun (\<lambda>t. convex_pd.basis_fun (\<lambda>u.
   248       convex_principal (PDPlus t u)))"
   249 
   250 abbreviation
   251   convex_add :: "'a convex_pd \<Rightarrow> 'a convex_pd \<Rightarrow> 'a convex_pd"
   252     (infixl "+\<natural>" 65) where
   253   "xs +\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
   254 
   255 syntax
   256   "_convex_pd" :: "args \<Rightarrow> 'a convex_pd" ("{_}\<natural>")
   257 
   258 translations
   259   "{x,xs}\<natural>" == "{x}\<natural> +\<natural> {xs}\<natural>"
   260   "{x}\<natural>" == "CONST convex_unit\<cdot>x"
   261 
   262 lemma convex_unit_Rep_compact_basis [simp]:
   263   "{Rep_compact_basis a}\<natural> = convex_principal (PDUnit a)"
   264 unfolding convex_unit_def
   265 by (simp add: compact_basis.basis_fun_principal PDUnit_convex_mono)
   266 
   267 lemma convex_plus_principal [simp]:
   268   "convex_principal t +\<natural> convex_principal u = convex_principal (PDPlus t u)"
   269 unfolding convex_plus_def
   270 by (simp add: convex_pd.basis_fun_principal
   271     convex_pd.basis_fun_mono PDPlus_convex_mono)
   272 
   273 lemma approx_convex_unit [simp]:
   274   "approx n\<cdot>{x}\<natural> = {approx n\<cdot>x}\<natural>"
   275 apply (induct x rule: compact_basis.principal_induct, simp)
   276 apply (simp add: approx_Rep_compact_basis)
   277 done
   278 
   279 lemma approx_convex_plus [simp]:
   280   "approx n\<cdot>(xs +\<natural> ys) = approx n\<cdot>xs +\<natural> approx n\<cdot>ys"
   281 by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
   282 
   283 lemma convex_plus_assoc:
   284   "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)"
   285 apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp)
   286 apply (rule_tac x=zs in convex_pd.principal_induct, simp)
   287 apply (simp add: PDPlus_assoc)
   288 done
   289 
   290 lemma convex_plus_commute: "xs +\<natural> ys = ys +\<natural> xs"
   291 apply (induct xs ys rule: convex_pd.principal_induct2, simp, simp)
   292 apply (simp add: PDPlus_commute)
   293 done
   294 
   295 lemma convex_plus_absorb: "xs +\<natural> xs = xs"
   296 apply (induct xs rule: convex_pd.principal_induct, simp)
   297 apply (simp add: PDPlus_absorb)
   298 done
   299 
   300 interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"]
   301   by unfold_locales
   302     (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
   303 
   304 lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)"
   305 by (rule aci_convex_plus.mult_left_commute)
   306 
   307 lemma convex_plus_left_absorb: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> ys"
   308 by (rule aci_convex_plus.mult_left_idem)
   309 
   310 lemmas convex_plus_aci = aci_convex_plus.mult_ac_idem
   311 
   312 lemma convex_unit_less_plus_iff [simp]:
   313   "{x}\<natural> \<sqsubseteq> ys +\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs"
   314  apply (rule iffI)
   315   apply (subgoal_tac
   316     "adm (\<lambda>f. f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>ys \<and> f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>zs)")
   317    apply (drule admD, rule chain_approx)
   318     apply (drule_tac f="approx i" in monofun_cfun_arg)
   319     apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   320     apply (cut_tac x="approx i\<cdot>ys" in convex_pd.compact_imp_principal, simp)
   321     apply (cut_tac x="approx i\<cdot>zs" in convex_pd.compact_imp_principal, simp)
   322     apply (clarify, simp)
   323    apply simp
   324   apply simp
   325  apply (erule conjE)
   326  apply (subst convex_plus_absorb [of "{x}\<natural>", symmetric])
   327  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
   328 done
   329 
   330 lemma convex_plus_less_unit_iff [simp]:
   331   "xs +\<natural> ys \<sqsubseteq> {z}\<natural> \<longleftrightarrow> xs \<sqsubseteq> {z}\<natural> \<and> ys \<sqsubseteq> {z}\<natural>"
   332  apply (rule iffI)
   333   apply (subgoal_tac
   334     "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>{z}\<natural> \<and> f\<cdot>ys \<sqsubseteq> f\<cdot>{z}\<natural>)")
   335    apply (drule admD, rule chain_approx)
   336     apply (drule_tac f="approx i" in monofun_cfun_arg)
   337     apply (cut_tac x="approx i\<cdot>xs" in convex_pd.compact_imp_principal, simp)
   338     apply (cut_tac x="approx i\<cdot>ys" in convex_pd.compact_imp_principal, simp)
   339     apply (cut_tac x="approx i\<cdot>z" in compact_basis.compact_imp_principal, simp)
   340     apply (clarify, simp)
   341    apply simp
   342   apply simp
   343  apply (erule conjE)
   344  apply (subst convex_plus_absorb [of "{z}\<natural>", symmetric])
   345  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
   346 done
   347 
   348 lemma convex_unit_less_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y"
   349  apply (rule iffI)
   350   apply (rule profinite_less_ext)
   351   apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   352   apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   353   apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
   354   apply clarsimp
   355  apply (erule monofun_cfun_arg)
   356 done
   357 
   358 lemma convex_unit_eq_iff [simp]: "{x}\<natural> = {y}\<natural> \<longleftrightarrow> x = y"
   359 unfolding po_eq_conv by simp
   360 
   361 lemma convex_unit_strict [simp]: "{\<bottom>}\<natural> = \<bottom>"
   362 unfolding inst_convex_pd_pcpo Rep_compact_bot [symmetric] by simp
   363 
   364 lemma convex_unit_strict_iff [simp]: "{x}\<natural> = \<bottom> \<longleftrightarrow> x = \<bottom>"
   365 unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff)
   366 
   367 lemma compact_convex_unit_iff [simp]:
   368   "compact {x}\<natural> \<longleftrightarrow> compact x"
   369 unfolding profinite_compact_iff by simp
   370 
   371 lemma compact_convex_plus [simp]:
   372   "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<natural> ys)"
   373 by (auto dest!: convex_pd.compact_imp_principal)
   374 
   375 
   376 subsection {* Induction rules *}
   377 
   378 lemma convex_pd_induct1:
   379   assumes P: "adm P"
   380   assumes unit: "\<And>x. P {x}\<natural>"
   381   assumes insert: "\<And>x ys. \<lbrakk>P {x}\<natural>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<natural> +\<natural> ys)"
   382   shows "P (xs::'a convex_pd)"
   383 apply (induct xs rule: convex_pd.principal_induct, rule P)
   384 apply (induct_tac a rule: pd_basis_induct1)
   385 apply (simp only: convex_unit_Rep_compact_basis [symmetric])
   386 apply (rule unit)
   387 apply (simp only: convex_unit_Rep_compact_basis [symmetric]
   388                   convex_plus_principal [symmetric])
   389 apply (erule insert [OF unit])
   390 done
   391 
   392 lemma convex_pd_induct:
   393   assumes P: "adm P"
   394   assumes unit: "\<And>x. P {x}\<natural>"
   395   assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<natural> ys)"
   396   shows "P (xs::'a convex_pd)"
   397 apply (induct xs rule: convex_pd.principal_induct, rule P)
   398 apply (induct_tac a rule: pd_basis_induct)
   399 apply (simp only: convex_unit_Rep_compact_basis [symmetric] unit)
   400 apply (simp only: convex_plus_principal [symmetric] plus)
   401 done
   402 
   403 
   404 subsection {* Monadic bind *}
   405 
   406 definition
   407   convex_bind_basis ::
   408   "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
   409   "convex_bind_basis = fold_pd
   410     (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
   411     (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
   412 
   413 lemma ACI_convex_bind:
   414   "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
   415 apply unfold_locales
   416 apply (simp add: convex_plus_assoc)
   417 apply (simp add: convex_plus_commute)
   418 apply (simp add: convex_plus_absorb eta_cfun)
   419 done
   420 
   421 lemma convex_bind_basis_simps [simp]:
   422   "convex_bind_basis (PDUnit a) =
   423     (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   424   "convex_bind_basis (PDPlus t u) =
   425     (\<Lambda> f. convex_bind_basis t\<cdot>f +\<natural> convex_bind_basis u\<cdot>f)"
   426 unfolding convex_bind_basis_def
   427 apply -
   428 apply (rule fold_pd_PDUnit [OF ACI_convex_bind])
   429 apply (rule fold_pd_PDPlus [OF ACI_convex_bind])
   430 done
   431 
   432 lemma monofun_LAM:
   433   "\<lbrakk>cont f; cont g; \<And>x. f x \<sqsubseteq> g x\<rbrakk> \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)"
   434 by (simp add: expand_cfun_less)
   435 
   436 lemma convex_bind_basis_mono:
   437   "t \<le>\<natural> u \<Longrightarrow> convex_bind_basis t \<sqsubseteq> convex_bind_basis u"
   438 apply (erule convex_le_induct)
   439 apply (erule (1) trans_less)
   440 apply (simp add: monofun_LAM monofun_cfun)
   441 apply (simp add: monofun_LAM monofun_cfun)
   442 done
   443 
   444 definition
   445   convex_bind :: "'a convex_pd \<rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
   446   "convex_bind = convex_pd.basis_fun convex_bind_basis"
   447 
   448 lemma convex_bind_principal [simp]:
   449   "convex_bind\<cdot>(convex_principal t) = convex_bind_basis t"
   450 unfolding convex_bind_def
   451 apply (rule convex_pd.basis_fun_principal)
   452 apply (erule convex_bind_basis_mono)
   453 done
   454 
   455 lemma convex_bind_unit [simp]:
   456   "convex_bind\<cdot>{x}\<natural>\<cdot>f = f\<cdot>x"
   457 by (induct x rule: compact_basis.principal_induct, simp, simp)
   458 
   459 lemma convex_bind_plus [simp]:
   460   "convex_bind\<cdot>(xs +\<natural> ys)\<cdot>f = convex_bind\<cdot>xs\<cdot>f +\<natural> convex_bind\<cdot>ys\<cdot>f"
   461 by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
   462 
   463 lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   464 unfolding convex_unit_strict [symmetric] by (rule convex_bind_unit)
   465 
   466 
   467 subsection {* Map and join *}
   468 
   469 definition
   470   convex_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a convex_pd \<rightarrow> 'b convex_pd" where
   471   "convex_map = (\<Lambda> f xs. convex_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<natural>))"
   472 
   473 definition
   474   convex_join :: "'a convex_pd convex_pd \<rightarrow> 'a convex_pd" where
   475   "convex_join = (\<Lambda> xss. convex_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
   476 
   477 lemma convex_map_unit [simp]:
   478   "convex_map\<cdot>f\<cdot>(convex_unit\<cdot>x) = convex_unit\<cdot>(f\<cdot>x)"
   479 unfolding convex_map_def by simp
   480 
   481 lemma convex_map_plus [simp]:
   482   "convex_map\<cdot>f\<cdot>(xs +\<natural> ys) = convex_map\<cdot>f\<cdot>xs +\<natural> convex_map\<cdot>f\<cdot>ys"
   483 unfolding convex_map_def by simp
   484 
   485 lemma convex_join_unit [simp]:
   486   "convex_join\<cdot>{xs}\<natural> = xs"
   487 unfolding convex_join_def by simp
   488 
   489 lemma convex_join_plus [simp]:
   490   "convex_join\<cdot>(xss +\<natural> yss) = convex_join\<cdot>xss +\<natural> convex_join\<cdot>yss"
   491 unfolding convex_join_def by simp
   492 
   493 lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
   494 by (induct xs rule: convex_pd_induct, simp_all)
   495 
   496 lemma convex_map_map:
   497   "convex_map\<cdot>f\<cdot>(convex_map\<cdot>g\<cdot>xs) = convex_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
   498 by (induct xs rule: convex_pd_induct, simp_all)
   499 
   500 lemma convex_join_map_unit:
   501   "convex_join\<cdot>(convex_map\<cdot>convex_unit\<cdot>xs) = xs"
   502 by (induct xs rule: convex_pd_induct, simp_all)
   503 
   504 lemma convex_join_map_join:
   505   "convex_join\<cdot>(convex_map\<cdot>convex_join\<cdot>xsss) = convex_join\<cdot>(convex_join\<cdot>xsss)"
   506 by (induct xsss rule: convex_pd_induct, simp_all)
   507 
   508 lemma convex_join_map_map:
   509   "convex_join\<cdot>(convex_map\<cdot>(convex_map\<cdot>f)\<cdot>xss) =
   510    convex_map\<cdot>f\<cdot>(convex_join\<cdot>xss)"
   511 by (induct xss rule: convex_pd_induct, simp_all)
   512 
   513 lemma convex_map_approx: "convex_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs"
   514 by (induct xs rule: convex_pd_induct, simp_all)
   515 
   516 
   517 subsection {* Conversions to other powerdomains *}
   518 
   519 text {* Convex to upper *}
   520 
   521 lemma convex_le_imp_upper_le: "t \<le>\<natural> u \<Longrightarrow> t \<le>\<sharp> u"
   522 unfolding convex_le_def by simp
   523 
   524 definition
   525   convex_to_upper :: "'a convex_pd \<rightarrow> 'a upper_pd" where
   526   "convex_to_upper = convex_pd.basis_fun upper_principal"
   527 
   528 lemma convex_to_upper_principal [simp]:
   529   "convex_to_upper\<cdot>(convex_principal t) = upper_principal t"
   530 unfolding convex_to_upper_def
   531 apply (rule convex_pd.basis_fun_principal)
   532 apply (rule upper_pd.principal_mono)
   533 apply (erule convex_le_imp_upper_le)
   534 done
   535 
   536 lemma convex_to_upper_unit [simp]:
   537   "convex_to_upper\<cdot>{x}\<natural> = {x}\<sharp>"
   538 by (induct x rule: compact_basis.principal_induct, simp, simp)
   539 
   540 lemma convex_to_upper_plus [simp]:
   541   "convex_to_upper\<cdot>(xs +\<natural> ys) = convex_to_upper\<cdot>xs +\<sharp> convex_to_upper\<cdot>ys"
   542 by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
   543 
   544 lemma approx_convex_to_upper:
   545   "approx i\<cdot>(convex_to_upper\<cdot>xs) = convex_to_upper\<cdot>(approx i\<cdot>xs)"
   546 by (induct xs rule: convex_pd_induct, simp, simp, simp)
   547 
   548 lemma convex_to_upper_bind [simp]:
   549   "convex_to_upper\<cdot>(convex_bind\<cdot>xs\<cdot>f) =
   550     upper_bind\<cdot>(convex_to_upper\<cdot>xs)\<cdot>(convex_to_upper oo f)"
   551 by (induct xs rule: convex_pd_induct, simp, simp, simp)
   552 
   553 lemma convex_to_upper_map [simp]:
   554   "convex_to_upper\<cdot>(convex_map\<cdot>f\<cdot>xs) = upper_map\<cdot>f\<cdot>(convex_to_upper\<cdot>xs)"
   555 by (simp add: convex_map_def upper_map_def cfcomp_LAM)
   556 
   557 lemma convex_to_upper_join [simp]:
   558   "convex_to_upper\<cdot>(convex_join\<cdot>xss) =
   559     upper_bind\<cdot>(convex_to_upper\<cdot>xss)\<cdot>convex_to_upper"
   560 by (simp add: convex_join_def upper_join_def cfcomp_LAM eta_cfun)
   561 
   562 text {* Convex to lower *}
   563 
   564 lemma convex_le_imp_lower_le: "t \<le>\<natural> u \<Longrightarrow> t \<le>\<flat> u"
   565 unfolding convex_le_def by simp
   566 
   567 definition
   568   convex_to_lower :: "'a convex_pd \<rightarrow> 'a lower_pd" where
   569   "convex_to_lower = convex_pd.basis_fun lower_principal"
   570 
   571 lemma convex_to_lower_principal [simp]:
   572   "convex_to_lower\<cdot>(convex_principal t) = lower_principal t"
   573 unfolding convex_to_lower_def
   574 apply (rule convex_pd.basis_fun_principal)
   575 apply (rule lower_pd.principal_mono)
   576 apply (erule convex_le_imp_lower_le)
   577 done
   578 
   579 lemma convex_to_lower_unit [simp]:
   580   "convex_to_lower\<cdot>{x}\<natural> = {x}\<flat>"
   581 by (induct x rule: compact_basis.principal_induct, simp, simp)
   582 
   583 lemma convex_to_lower_plus [simp]:
   584   "convex_to_lower\<cdot>(xs +\<natural> ys) = convex_to_lower\<cdot>xs +\<flat> convex_to_lower\<cdot>ys"
   585 by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
   586 
   587 lemma approx_convex_to_lower:
   588   "approx i\<cdot>(convex_to_lower\<cdot>xs) = convex_to_lower\<cdot>(approx i\<cdot>xs)"
   589 by (induct xs rule: convex_pd_induct, simp, simp, simp)
   590 
   591 lemma convex_to_lower_bind [simp]:
   592   "convex_to_lower\<cdot>(convex_bind\<cdot>xs\<cdot>f) =
   593     lower_bind\<cdot>(convex_to_lower\<cdot>xs)\<cdot>(convex_to_lower oo f)"
   594 by (induct xs rule: convex_pd_induct, simp, simp, simp)
   595 
   596 lemma convex_to_lower_map [simp]:
   597   "convex_to_lower\<cdot>(convex_map\<cdot>f\<cdot>xs) = lower_map\<cdot>f\<cdot>(convex_to_lower\<cdot>xs)"
   598 by (simp add: convex_map_def lower_map_def cfcomp_LAM)
   599 
   600 lemma convex_to_lower_join [simp]:
   601   "convex_to_lower\<cdot>(convex_join\<cdot>xss) =
   602     lower_bind\<cdot>(convex_to_lower\<cdot>xss)\<cdot>convex_to_lower"
   603 by (simp add: convex_join_def lower_join_def cfcomp_LAM eta_cfun)
   604 
   605 text {* Ordering property *}
   606 
   607 lemma convex_pd_less_iff:
   608   "(xs \<sqsubseteq> ys) =
   609     (convex_to_upper\<cdot>xs \<sqsubseteq> convex_to_upper\<cdot>ys \<and>
   610      convex_to_lower\<cdot>xs \<sqsubseteq> convex_to_lower\<cdot>ys)"
   611  apply (safe elim!: monofun_cfun_arg)
   612  apply (rule profinite_less_ext)
   613  apply (drule_tac f="approx i" in monofun_cfun_arg)
   614  apply (drule_tac f="approx i" in monofun_cfun_arg)
   615  apply (cut_tac x="approx i\<cdot>xs" in convex_pd.compact_imp_principal, simp)
   616  apply (cut_tac x="approx i\<cdot>ys" in convex_pd.compact_imp_principal, simp)
   617  apply clarify
   618  apply (simp add: approx_convex_to_upper approx_convex_to_lower convex_le_def)
   619 done
   620 
   621 lemmas convex_plus_less_plus_iff =
   622   convex_pd_less_iff [where xs="xs +\<natural> ys" and ys="zs +\<natural> ws", standard]
   623 
   624 lemmas convex_pd_less_simps =
   625   convex_unit_less_plus_iff
   626   convex_plus_less_unit_iff
   627   convex_plus_less_plus_iff
   628   convex_unit_less_iff
   629   convex_to_upper_unit
   630   convex_to_upper_plus
   631   convex_to_lower_unit
   632   convex_to_lower_plus
   633   upper_pd_less_simps
   634   lower_pd_less_simps
   635 
   636 end