src/HOLCF/UpperPD.thy
author haftmann
Wed Feb 06 08:34:32 2008 +0100 (2008-02-06)
changeset 26041 c2e15e65165f
parent 25925 3dc4acca4388
child 26407 562a1d615336
permissions -rw-r--r--
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
     1 (*  Title:      HOLCF/UpperPD.thy
     2     ID:         $Id$
     3     Author:     Brian Huffman
     4 *)
     5 
     6 header {* Upper powerdomain *}
     7 
     8 theory UpperPD
     9 imports CompactBasis
    10 begin
    11 
    12 subsection {* Basis preorder *}
    13 
    14 definition
    15   upper_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<sharp>" 50) where
    16   "upper_le = (\<lambda>u v. \<forall>y\<in>Rep_pd_basis v. \<exists>x\<in>Rep_pd_basis u. compact_le x y)"
    17 
    18 lemma upper_le_refl [simp]: "t \<le>\<sharp> t"
    19 unfolding upper_le_def by (fast intro: compact_le_refl)
    20 
    21 lemma upper_le_trans: "\<lbrakk>t \<le>\<sharp> u; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> t \<le>\<sharp> v"
    22 unfolding upper_le_def
    23 apply (rule ballI)
    24 apply (drule (1) bspec, erule bexE)
    25 apply (drule (1) bspec, erule bexE)
    26 apply (erule rev_bexI)
    27 apply (erule (1) compact_le_trans)
    28 done
    29 
    30 interpretation upper_le: preorder [upper_le]
    31 by (rule preorder.intro, rule upper_le_refl, rule upper_le_trans)
    32 
    33 lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<sharp> t"
    34 unfolding upper_le_def Rep_PDUnit by simp
    35 
    36 lemma PDUnit_upper_mono: "compact_le x y \<Longrightarrow> PDUnit x \<le>\<sharp> PDUnit y"
    37 unfolding upper_le_def Rep_PDUnit by simp
    38 
    39 lemma PDPlus_upper_mono: "\<lbrakk>s \<le>\<sharp> t; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<sharp> PDPlus t v"
    40 unfolding upper_le_def Rep_PDPlus by fast
    41 
    42 lemma PDPlus_upper_less: "PDPlus t u \<le>\<sharp> t"
    43 unfolding upper_le_def Rep_PDPlus by (fast intro: compact_le_refl)
    44 
    45 lemma upper_le_PDUnit_PDUnit_iff [simp]:
    46   "(PDUnit a \<le>\<sharp> PDUnit b) = compact_le a b"
    47 unfolding upper_le_def Rep_PDUnit by fast
    48 
    49 lemma upper_le_PDPlus_PDUnit_iff:
    50   "(PDPlus t u \<le>\<sharp> PDUnit a) = (t \<le>\<sharp> PDUnit a \<or> u \<le>\<sharp> PDUnit a)"
    51 unfolding upper_le_def Rep_PDPlus Rep_PDUnit by fast
    52 
    53 lemma upper_le_PDPlus_iff: "(t \<le>\<sharp> PDPlus u v) = (t \<le>\<sharp> u \<and> t \<le>\<sharp> v)"
    54 unfolding upper_le_def Rep_PDPlus by fast
    55 
    56 lemma upper_le_induct [induct set: upper_le]:
    57   assumes le: "t \<le>\<sharp> u"
    58   assumes 1: "\<And>a b. compact_le a b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
    59   assumes 2: "\<And>t u a. P t (PDUnit a) \<Longrightarrow> P (PDPlus t u) (PDUnit a)"
    60   assumes 3: "\<And>t u v. \<lbrakk>P t u; P t v\<rbrakk> \<Longrightarrow> P t (PDPlus u v)"
    61   shows "P t u"
    62 using le apply (induct u arbitrary: t rule: pd_basis_induct)
    63 apply (erule rev_mp)
    64 apply (induct_tac t rule: pd_basis_induct)
    65 apply (simp add: 1)
    66 apply (simp add: upper_le_PDPlus_PDUnit_iff)
    67 apply (simp add: 2)
    68 apply (subst PDPlus_commute)
    69 apply (simp add: 2)
    70 apply (simp add: upper_le_PDPlus_iff 3)
    71 done
    72 
    73 lemma approx_pd_upper_mono1:
    74   "i \<le> j \<Longrightarrow> approx_pd i t \<le>\<sharp> approx_pd j t"
    75 apply (induct t rule: pd_basis_induct)
    76 apply (simp add: compact_approx_mono1)
    77 apply (simp add: PDPlus_upper_mono)
    78 done
    79 
    80 lemma approx_pd_upper_le: "approx_pd i t \<le>\<sharp> t"
    81 apply (induct t rule: pd_basis_induct)
    82 apply (simp add: compact_approx_le)
    83 apply (simp add: PDPlus_upper_mono)
    84 done
    85 
    86 lemma approx_pd_upper_mono:
    87   "t \<le>\<sharp> u \<Longrightarrow> approx_pd n t \<le>\<sharp> approx_pd n u"
    88 apply (erule upper_le_induct)
    89 apply (simp add: compact_approx_mono)
    90 apply (simp add: upper_le_PDPlus_PDUnit_iff)
    91 apply (simp add: upper_le_PDPlus_iff)
    92 done
    93 
    94 
    95 subsection {* Type definition *}
    96 
    97 cpodef (open) 'a upper_pd =
    98   "{S::'a::bifinite pd_basis set. upper_le.ideal S}"
    99 apply (simp add: upper_le.adm_ideal)
   100 apply (fast intro: upper_le.ideal_principal)
   101 done
   102 
   103 lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd x)"
   104 by (rule Rep_upper_pd [simplified])
   105 
   106 definition
   107   upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where
   108   "upper_principal t = Abs_upper_pd {u. u \<le>\<sharp> t}"
   109 
   110 lemma Rep_upper_principal:
   111   "Rep_upper_pd (upper_principal t) = {u. u \<le>\<sharp> t}"
   112 unfolding upper_principal_def
   113 apply (rule Abs_upper_pd_inverse [simplified])
   114 apply (rule upper_le.ideal_principal)
   115 done
   116 
   117 interpretation upper_pd:
   118   bifinite_basis [upper_le upper_principal Rep_upper_pd approx_pd]
   119 apply unfold_locales
   120 apply (rule ideal_Rep_upper_pd)
   121 apply (rule cont_Rep_upper_pd)
   122 apply (rule Rep_upper_principal)
   123 apply (simp only: less_upper_pd_def less_set_def)
   124 apply (rule approx_pd_upper_le)
   125 apply (rule approx_pd_idem)
   126 apply (erule approx_pd_upper_mono)
   127 apply (rule approx_pd_upper_mono1, simp)
   128 apply (rule finite_range_approx_pd)
   129 apply (rule ex_approx_pd_eq)
   130 done
   131 
   132 lemma upper_principal_less_iff [simp]:
   133   "(upper_principal t \<sqsubseteq> upper_principal u) = (t \<le>\<sharp> u)"
   134 unfolding less_upper_pd_def Rep_upper_principal less_set_def
   135 by (fast intro: upper_le_refl elim: upper_le_trans)
   136 
   137 lemma upper_principal_mono:
   138   "t \<le>\<sharp> u \<Longrightarrow> upper_principal t \<sqsubseteq> upper_principal u"
   139 by (rule upper_pd.principal_mono)
   140 
   141 lemma compact_upper_principal: "compact (upper_principal t)"
   142 by (rule upper_pd.compact_principal)
   143 
   144 lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys"
   145 by (induct ys rule: upper_pd.principal_induct, simp, simp)
   146 
   147 instance upper_pd :: (bifinite) pcpo
   148 by (intro_classes, fast intro: upper_pd_minimal)
   149 
   150 lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
   151 by (rule upper_pd_minimal [THEN UU_I, symmetric])
   152 
   153 
   154 subsection {* Approximation *}
   155 
   156 instance upper_pd :: (bifinite) approx ..
   157 
   158 defs (overloaded)
   159   approx_upper_pd_def:
   160     "approx \<equiv> (\<lambda>n. upper_pd.basis_fun (\<lambda>t. upper_principal (approx_pd n t)))"
   161 
   162 lemma approx_upper_principal [simp]:
   163   "approx n\<cdot>(upper_principal t) = upper_principal (approx_pd n t)"
   164 unfolding approx_upper_pd_def
   165 apply (rule upper_pd.basis_fun_principal)
   166 apply (erule upper_principal_mono [OF approx_pd_upper_mono])
   167 done
   168 
   169 lemma chain_approx_upper_pd:
   170   "chain (approx :: nat \<Rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd)"
   171 unfolding approx_upper_pd_def
   172 by (rule upper_pd.chain_basis_fun_take)
   173 
   174 lemma lub_approx_upper_pd:
   175   "(\<Squnion>i. approx i\<cdot>xs) = (xs::'a upper_pd)"
   176 unfolding approx_upper_pd_def
   177 by (rule upper_pd.lub_basis_fun_take)
   178 
   179 lemma approx_upper_pd_idem:
   180   "approx n\<cdot>(approx n\<cdot>xs) = approx n\<cdot>(xs::'a upper_pd)"
   181 apply (induct xs rule: upper_pd.principal_induct, simp)
   182 apply (simp add: approx_pd_idem)
   183 done
   184 
   185 lemma approx_eq_upper_principal:
   186   "\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (approx_pd n t)"
   187 unfolding approx_upper_pd_def
   188 by (rule upper_pd.basis_fun_take_eq_principal)
   189 
   190 lemma finite_fixes_approx_upper_pd:
   191   "finite {xs::'a upper_pd. approx n\<cdot>xs = xs}"
   192 unfolding approx_upper_pd_def
   193 by (rule upper_pd.finite_fixes_basis_fun_take)
   194 
   195 instance upper_pd :: (bifinite) bifinite
   196 apply intro_classes
   197 apply (simp add: chain_approx_upper_pd)
   198 apply (rule lub_approx_upper_pd)
   199 apply (rule approx_upper_pd_idem)
   200 apply (rule finite_fixes_approx_upper_pd)
   201 done
   202 
   203 lemma compact_imp_upper_principal:
   204   "compact xs \<Longrightarrow> \<exists>t. xs = upper_principal t"
   205 apply (drule bifinite_compact_eq_approx)
   206 apply (erule exE)
   207 apply (erule subst)
   208 apply (cut_tac n=i and xs=xs in approx_eq_upper_principal)
   209 apply fast
   210 done
   211 
   212 lemma upper_principal_induct:
   213   "\<lbrakk>adm P; \<And>t. P (upper_principal t)\<rbrakk> \<Longrightarrow> P xs"
   214 apply (erule approx_induct, rename_tac xs)
   215 apply (cut_tac n=n and xs=xs in approx_eq_upper_principal)
   216 apply (clarify, simp)
   217 done
   218 
   219 lemma upper_principal_induct2:
   220   "\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
   221     \<And>t u. P (upper_principal t) (upper_principal u)\<rbrakk> \<Longrightarrow> P xs ys"
   222 apply (rule_tac x=ys in spec)
   223 apply (rule_tac xs=xs in upper_principal_induct, simp)
   224 apply (rule allI, rename_tac ys)
   225 apply (rule_tac xs=ys in upper_principal_induct, simp)
   226 apply simp
   227 done
   228 
   229 
   230 subsection {* Monadic unit *}
   231 
   232 definition
   233   upper_unit :: "'a \<rightarrow> 'a upper_pd" where
   234   "upper_unit = compact_basis.basis_fun (\<lambda>a. upper_principal (PDUnit a))"
   235 
   236 lemma upper_unit_Rep_compact_basis [simp]:
   237   "upper_unit\<cdot>(Rep_compact_basis a) = upper_principal (PDUnit a)"
   238 unfolding upper_unit_def
   239 apply (rule compact_basis.basis_fun_principal)
   240 apply (rule upper_principal_mono)
   241 apply (erule PDUnit_upper_mono)
   242 done
   243 
   244 lemma upper_unit_strict [simp]: "upper_unit\<cdot>\<bottom> = \<bottom>"
   245 unfolding inst_upper_pd_pcpo Rep_compact_bot [symmetric] by simp
   246 
   247 lemma approx_upper_unit [simp]:
   248   "approx n\<cdot>(upper_unit\<cdot>x) = upper_unit\<cdot>(approx n\<cdot>x)"
   249 apply (induct x rule: compact_basis_induct, simp)
   250 apply (simp add: approx_Rep_compact_basis)
   251 done
   252 
   253 lemma upper_unit_less_iff [simp]:
   254   "(upper_unit\<cdot>x \<sqsubseteq> upper_unit\<cdot>y) = (x \<sqsubseteq> y)"
   255  apply (rule iffI)
   256   apply (rule bifinite_less_ext)
   257   apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   258   apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   259   apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
   260   apply (clarify, simp add: compact_le_def)
   261  apply (erule monofun_cfun_arg)
   262 done
   263 
   264 lemma upper_unit_eq_iff [simp]:
   265   "(upper_unit\<cdot>x = upper_unit\<cdot>y) = (x = y)"
   266 unfolding po_eq_conv by simp
   267 
   268 lemma upper_unit_strict_iff [simp]: "(upper_unit\<cdot>x = \<bottom>) = (x = \<bottom>)"
   269 unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
   270 
   271 lemma compact_upper_unit_iff [simp]:
   272   "compact (upper_unit\<cdot>x) = compact x"
   273 unfolding bifinite_compact_iff by simp
   274 
   275 
   276 subsection {* Monadic plus *}
   277 
   278 definition
   279   upper_plus :: "'a upper_pd \<rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd" where
   280   "upper_plus = upper_pd.basis_fun (\<lambda>t. upper_pd.basis_fun (\<lambda>u.
   281       upper_principal (PDPlus t u)))"
   282 
   283 abbreviation
   284   upper_add :: "'a upper_pd \<Rightarrow> 'a upper_pd \<Rightarrow> 'a upper_pd"
   285     (infixl "+\<sharp>" 65) where
   286   "xs +\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
   287 
   288 lemma upper_plus_principal [simp]:
   289   "upper_plus\<cdot>(upper_principal t)\<cdot>(upper_principal u) =
   290    upper_principal (PDPlus t u)"
   291 unfolding upper_plus_def
   292 by (simp add: upper_pd.basis_fun_principal
   293     upper_pd.basis_fun_mono PDPlus_upper_mono)
   294 
   295 lemma approx_upper_plus [simp]:
   296   "approx n\<cdot>(upper_plus\<cdot>xs\<cdot>ys) = upper_plus\<cdot>(approx n\<cdot>xs)\<cdot>(approx n\<cdot>ys)"
   297 by (induct xs ys rule: upper_principal_induct2, simp, simp, simp)
   298 
   299 lemma upper_plus_commute: "upper_plus\<cdot>xs\<cdot>ys = upper_plus\<cdot>ys\<cdot>xs"
   300 apply (induct xs ys rule: upper_principal_induct2, simp, simp)
   301 apply (simp add: PDPlus_commute)
   302 done
   303 
   304 lemma upper_plus_assoc:
   305   "upper_plus\<cdot>(upper_plus\<cdot>xs\<cdot>ys)\<cdot>zs = upper_plus\<cdot>xs\<cdot>(upper_plus\<cdot>ys\<cdot>zs)"
   306 apply (induct xs ys arbitrary: zs rule: upper_principal_induct2, simp, simp)
   307 apply (rule_tac xs=zs in upper_principal_induct, simp)
   308 apply (simp add: PDPlus_assoc)
   309 done
   310 
   311 lemma upper_plus_absorb: "upper_plus\<cdot>xs\<cdot>xs = xs"
   312 apply (induct xs rule: upper_principal_induct, simp)
   313 apply (simp add: PDPlus_absorb)
   314 done
   315 
   316 lemma upper_plus_less1: "upper_plus\<cdot>xs\<cdot>ys \<sqsubseteq> xs"
   317 apply (induct xs ys rule: upper_principal_induct2, simp, simp)
   318 apply (simp add: PDPlus_upper_less)
   319 done
   320 
   321 lemma upper_plus_less2: "upper_plus\<cdot>xs\<cdot>ys \<sqsubseteq> ys"
   322 by (subst upper_plus_commute, rule upper_plus_less1)
   323 
   324 lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> upper_plus\<cdot>ys\<cdot>zs"
   325 apply (subst upper_plus_absorb [of xs, symmetric])
   326 apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
   327 done
   328 
   329 lemma upper_less_plus_iff:
   330   "(xs \<sqsubseteq> upper_plus\<cdot>ys\<cdot>zs) = (xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs)"
   331 apply safe
   332 apply (erule trans_less [OF _ upper_plus_less1])
   333 apply (erule trans_less [OF _ upper_plus_less2])
   334 apply (erule (1) upper_plus_greatest)
   335 done
   336 
   337 lemma upper_plus_strict1 [simp]: "upper_plus\<cdot>\<bottom>\<cdot>ys = \<bottom>"
   338 by (rule UU_I, rule upper_plus_less1)
   339 
   340 lemma upper_plus_strict2 [simp]: "upper_plus\<cdot>xs\<cdot>\<bottom> = \<bottom>"
   341 by (rule UU_I, rule upper_plus_less2)
   342 
   343 lemma upper_plus_less_unit_iff:
   344   "(upper_plus\<cdot>xs\<cdot>ys \<sqsubseteq> upper_unit\<cdot>z) =
   345     (xs \<sqsubseteq> upper_unit\<cdot>z \<or> ys \<sqsubseteq> upper_unit\<cdot>z)"
   346  apply (rule iffI)
   347   apply (subgoal_tac
   348     "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z) \<or> f\<cdot>ys \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z))")
   349    apply (drule admD, rule chain_approx)
   350     apply (drule_tac f="approx i" in monofun_cfun_arg)
   351     apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_upper_principal, simp)
   352     apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_upper_principal, simp)
   353     apply (cut_tac x="approx i\<cdot>z" in compact_imp_Rep_compact_basis, simp)
   354     apply (clarify, simp add: upper_le_PDPlus_PDUnit_iff)
   355    apply simp
   356   apply simp
   357  apply (erule disjE)
   358   apply (erule trans_less [OF upper_plus_less1])
   359  apply (erule trans_less [OF upper_plus_less2])
   360 done
   361 
   362 lemmas upper_pd_less_simps =
   363   upper_unit_less_iff
   364   upper_less_plus_iff
   365   upper_plus_less_unit_iff
   366 
   367 
   368 subsection {* Induction rules *}
   369 
   370 lemma upper_pd_induct1:
   371   assumes P: "adm P"
   372   assumes unit: "\<And>x. P (upper_unit\<cdot>x)"
   373   assumes insert:
   374     "\<And>x ys. \<lbrakk>P (upper_unit\<cdot>x); P ys\<rbrakk> \<Longrightarrow> P (upper_plus\<cdot>(upper_unit\<cdot>x)\<cdot>ys)"
   375   shows "P (xs::'a upper_pd)"
   376 apply (induct xs rule: upper_principal_induct, rule P)
   377 apply (induct_tac t rule: pd_basis_induct1)
   378 apply (simp only: upper_unit_Rep_compact_basis [symmetric])
   379 apply (rule unit)
   380 apply (simp only: upper_unit_Rep_compact_basis [symmetric]
   381                   upper_plus_principal [symmetric])
   382 apply (erule insert [OF unit])
   383 done
   384 
   385 lemma upper_pd_induct:
   386   assumes P: "adm P"
   387   assumes unit: "\<And>x. P (upper_unit\<cdot>x)"
   388   assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (upper_plus\<cdot>xs\<cdot>ys)"
   389   shows "P (xs::'a upper_pd)"
   390 apply (induct xs rule: upper_principal_induct, rule P)
   391 apply (induct_tac t rule: pd_basis_induct)
   392 apply (simp only: upper_unit_Rep_compact_basis [symmetric] unit)
   393 apply (simp only: upper_plus_principal [symmetric] plus)
   394 done
   395 
   396 
   397 subsection {* Monadic bind *}
   398 
   399 definition
   400   upper_bind_basis ::
   401   "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where
   402   "upper_bind_basis = fold_pd
   403     (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
   404     (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
   405 
   406 lemma ACI_upper_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
   407 apply unfold_locales
   408 apply (simp add: upper_plus_assoc)
   409 apply (simp add: upper_plus_commute)
   410 apply (simp add: upper_plus_absorb eta_cfun)
   411 done
   412 
   413 lemma upper_bind_basis_simps [simp]:
   414   "upper_bind_basis (PDUnit a) =
   415     (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   416   "upper_bind_basis (PDPlus t u) =
   417     (\<Lambda> f. upper_plus\<cdot>(upper_bind_basis t\<cdot>f)\<cdot>(upper_bind_basis u\<cdot>f))"
   418 unfolding upper_bind_basis_def
   419 apply -
   420 apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_upper_bind])
   421 apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_upper_bind])
   422 done
   423 
   424 lemma upper_bind_basis_mono:
   425   "t \<le>\<sharp> u \<Longrightarrow> upper_bind_basis t \<sqsubseteq> upper_bind_basis u"
   426 unfolding expand_cfun_less
   427 apply (erule upper_le_induct, safe)
   428 apply (simp add: compact_le_def monofun_cfun)
   429 apply (simp add: trans_less [OF upper_plus_less1])
   430 apply (simp add: upper_less_plus_iff)
   431 done
   432 
   433 definition
   434   upper_bind :: "'a upper_pd \<rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where
   435   "upper_bind = upper_pd.basis_fun upper_bind_basis"
   436 
   437 lemma upper_bind_principal [simp]:
   438   "upper_bind\<cdot>(upper_principal t) = upper_bind_basis t"
   439 unfolding upper_bind_def
   440 apply (rule upper_pd.basis_fun_principal)
   441 apply (erule upper_bind_basis_mono)
   442 done
   443 
   444 lemma upper_bind_unit [simp]:
   445   "upper_bind\<cdot>(upper_unit\<cdot>x)\<cdot>f = f\<cdot>x"
   446 by (induct x rule: compact_basis_induct, simp, simp)
   447 
   448 lemma upper_bind_plus [simp]:
   449   "upper_bind\<cdot>(upper_plus\<cdot>xs\<cdot>ys)\<cdot>f =
   450    upper_plus\<cdot>(upper_bind\<cdot>xs\<cdot>f)\<cdot>(upper_bind\<cdot>ys\<cdot>f)"
   451 by (induct xs ys rule: upper_principal_induct2, simp, simp, simp)
   452 
   453 lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   454 unfolding upper_unit_strict [symmetric] by (rule upper_bind_unit)
   455 
   456 
   457 subsection {* Map and join *}
   458 
   459 definition
   460   upper_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a upper_pd \<rightarrow> 'b upper_pd" where
   461   "upper_map = (\<Lambda> f xs. upper_bind\<cdot>xs\<cdot>(\<Lambda> x. upper_unit\<cdot>(f\<cdot>x)))"
   462 
   463 definition
   464   upper_join :: "'a upper_pd upper_pd \<rightarrow> 'a upper_pd" where
   465   "upper_join = (\<Lambda> xss. upper_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
   466 
   467 lemma upper_map_unit [simp]:
   468   "upper_map\<cdot>f\<cdot>(upper_unit\<cdot>x) = upper_unit\<cdot>(f\<cdot>x)"
   469 unfolding upper_map_def by simp
   470 
   471 lemma upper_map_plus [simp]:
   472   "upper_map\<cdot>f\<cdot>(upper_plus\<cdot>xs\<cdot>ys) =
   473    upper_plus\<cdot>(upper_map\<cdot>f\<cdot>xs)\<cdot>(upper_map\<cdot>f\<cdot>ys)"
   474 unfolding upper_map_def by simp
   475 
   476 lemma upper_join_unit [simp]:
   477   "upper_join\<cdot>(upper_unit\<cdot>xs) = xs"
   478 unfolding upper_join_def by simp
   479 
   480 lemma upper_join_plus [simp]:
   481   "upper_join\<cdot>(upper_plus\<cdot>xss\<cdot>yss) =
   482    upper_plus\<cdot>(upper_join\<cdot>xss)\<cdot>(upper_join\<cdot>yss)"
   483 unfolding upper_join_def by simp
   484 
   485 lemma upper_map_ident: "upper_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
   486 by (induct xs rule: upper_pd_induct, simp_all)
   487 
   488 lemma upper_map_map:
   489   "upper_map\<cdot>f\<cdot>(upper_map\<cdot>g\<cdot>xs) = upper_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
   490 by (induct xs rule: upper_pd_induct, simp_all)
   491 
   492 lemma upper_join_map_unit:
   493   "upper_join\<cdot>(upper_map\<cdot>upper_unit\<cdot>xs) = xs"
   494 by (induct xs rule: upper_pd_induct, simp_all)
   495 
   496 lemma upper_join_map_join:
   497   "upper_join\<cdot>(upper_map\<cdot>upper_join\<cdot>xsss) = upper_join\<cdot>(upper_join\<cdot>xsss)"
   498 by (induct xsss rule: upper_pd_induct, simp_all)
   499 
   500 lemma upper_join_map_map:
   501   "upper_join\<cdot>(upper_map\<cdot>(upper_map\<cdot>f)\<cdot>xss) =
   502    upper_map\<cdot>f\<cdot>(upper_join\<cdot>xss)"
   503 by (induct xss rule: upper_pd_induct, simp_all)
   504 
   505 lemma upper_map_approx: "upper_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs"
   506 by (induct xs rule: upper_pd_induct, simp_all)
   507 
   508 end