src/HOLCF/UpperPD.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/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. x \<sqsubseteq> y)"
    17 
    18 lemma upper_le_refl [simp]: "t \<le>\<sharp> t"
    19 unfolding upper_le_def by fast
    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) trans_less)
    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: "x \<sqsubseteq> 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
    44 
    45 lemma upper_le_PDUnit_PDUnit_iff [simp]:
    46   "(PDUnit a \<le>\<sharp> PDUnit b) = a \<sqsubseteq> 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. a \<sqsubseteq> 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_chain:
    74   "approx_pd n t \<le>\<sharp> approx_pd (Suc n) t"
    75 apply (induct t rule: pd_basis_induct)
    76 apply (simp add: compact_basis.take_chain)
    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_basis.take_less)
    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_basis.take_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 pd_basis cset. upper_le.ideal (Rep_cset S)}"
    99 by (rule upper_le.cpodef_ideal_lemma)
   100 
   101 lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_cset (Rep_upper_pd xs))"
   102 by (rule Rep_upper_pd [unfolded mem_Collect_eq])
   103 
   104 definition
   105   upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where
   106   "upper_principal t = Abs_upper_pd (Abs_cset {u. u \<le>\<sharp> t})"
   107 
   108 lemma Rep_upper_principal:
   109   "Rep_cset (Rep_upper_pd (upper_principal t)) = {u. u \<le>\<sharp> t}"
   110 unfolding upper_principal_def
   111 by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
   112 
   113 interpretation upper_pd:
   114   ideal_completion
   115     [upper_le approx_pd upper_principal "\<lambda>x. Rep_cset (Rep_upper_pd x)"]
   116 apply unfold_locales
   117 apply (rule approx_pd_upper_le)
   118 apply (rule approx_pd_idem)
   119 apply (erule approx_pd_upper_mono)
   120 apply (rule approx_pd_upper_chain)
   121 apply (rule finite_range_approx_pd)
   122 apply (rule approx_pd_covers)
   123 apply (rule ideal_Rep_upper_pd)
   124 apply (simp add: cont2contlubE [OF cont_Rep_upper_pd] Rep_cset_lub)
   125 apply (rule Rep_upper_principal)
   126 apply (simp only: less_upper_pd_def sq_le_cset_def)
   127 done
   128 
   129 text {* Upper powerdomain is pointed *}
   130 
   131 lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys"
   132 by (induct ys rule: upper_pd.principal_induct, simp, simp)
   133 
   134 instance upper_pd :: (bifinite) pcpo
   135 by intro_classes (fast intro: upper_pd_minimal)
   136 
   137 lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
   138 by (rule upper_pd_minimal [THEN UU_I, symmetric])
   139 
   140 text {* Upper powerdomain is profinite *}
   141 
   142 instantiation upper_pd :: (profinite) profinite
   143 begin
   144 
   145 definition
   146   approx_upper_pd_def: "approx = upper_pd.completion_approx"
   147 
   148 instance
   149 apply (intro_classes, unfold approx_upper_pd_def)
   150 apply (simp add: upper_pd.chain_completion_approx)
   151 apply (rule upper_pd.lub_completion_approx)
   152 apply (rule upper_pd.completion_approx_idem)
   153 apply (rule upper_pd.finite_fixes_completion_approx)
   154 done
   155 
   156 end
   157 
   158 instance upper_pd :: (bifinite) bifinite ..
   159 
   160 lemma approx_upper_principal [simp]:
   161   "approx n\<cdot>(upper_principal t) = upper_principal (approx_pd n t)"
   162 unfolding approx_upper_pd_def
   163 by (rule upper_pd.completion_approx_principal)
   164 
   165 lemma approx_eq_upper_principal:
   166   "\<exists>t\<in>Rep_cset (Rep_upper_pd xs).
   167     approx n\<cdot>xs = upper_principal (approx_pd n t)"
   168 unfolding approx_upper_pd_def
   169 by (rule upper_pd.completion_approx_eq_principal)
   170 
   171 
   172 subsection {* Monadic unit and plus *}
   173 
   174 definition
   175   upper_unit :: "'a \<rightarrow> 'a upper_pd" where
   176   "upper_unit = compact_basis.basis_fun (\<lambda>a. upper_principal (PDUnit a))"
   177 
   178 definition
   179   upper_plus :: "'a upper_pd \<rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd" where
   180   "upper_plus = upper_pd.basis_fun (\<lambda>t. upper_pd.basis_fun (\<lambda>u.
   181       upper_principal (PDPlus t u)))"
   182 
   183 abbreviation
   184   upper_add :: "'a upper_pd \<Rightarrow> 'a upper_pd \<Rightarrow> 'a upper_pd"
   185     (infixl "+\<sharp>" 65) where
   186   "xs +\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
   187 
   188 syntax
   189   "_upper_pd" :: "args \<Rightarrow> 'a upper_pd" ("{_}\<sharp>")
   190 
   191 translations
   192   "{x,xs}\<sharp>" == "{x}\<sharp> +\<sharp> {xs}\<sharp>"
   193   "{x}\<sharp>" == "CONST upper_unit\<cdot>x"
   194 
   195 lemma upper_unit_Rep_compact_basis [simp]:
   196   "{Rep_compact_basis a}\<sharp> = upper_principal (PDUnit a)"
   197 unfolding upper_unit_def
   198 by (simp add: compact_basis.basis_fun_principal PDUnit_upper_mono)
   199 
   200 lemma upper_plus_principal [simp]:
   201   "upper_principal t +\<sharp> upper_principal u = upper_principal (PDPlus t u)"
   202 unfolding upper_plus_def
   203 by (simp add: upper_pd.basis_fun_principal
   204     upper_pd.basis_fun_mono PDPlus_upper_mono)
   205 
   206 lemma approx_upper_unit [simp]:
   207   "approx n\<cdot>{x}\<sharp> = {approx n\<cdot>x}\<sharp>"
   208 apply (induct x rule: compact_basis.principal_induct, simp)
   209 apply (simp add: approx_Rep_compact_basis)
   210 done
   211 
   212 lemma approx_upper_plus [simp]:
   213   "approx n\<cdot>(xs +\<sharp> ys) = (approx n\<cdot>xs) +\<sharp> (approx n\<cdot>ys)"
   214 by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp)
   215 
   216 lemma upper_plus_assoc: "(xs +\<sharp> ys) +\<sharp> zs = xs +\<sharp> (ys +\<sharp> zs)"
   217 apply (induct xs ys arbitrary: zs rule: upper_pd.principal_induct2, simp, simp)
   218 apply (rule_tac x=zs in upper_pd.principal_induct, simp)
   219 apply (simp add: PDPlus_assoc)
   220 done
   221 
   222 lemma upper_plus_commute: "xs +\<sharp> ys = ys +\<sharp> xs"
   223 apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
   224 apply (simp add: PDPlus_commute)
   225 done
   226 
   227 lemma upper_plus_absorb: "xs +\<sharp> xs = xs"
   228 apply (induct xs rule: upper_pd.principal_induct, simp)
   229 apply (simp add: PDPlus_absorb)
   230 done
   231 
   232 interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"]
   233   by unfold_locales
   234     (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
   235 
   236 lemma upper_plus_left_commute: "xs +\<sharp> (ys +\<sharp> zs) = ys +\<sharp> (xs +\<sharp> zs)"
   237 by (rule aci_upper_plus.mult_left_commute)
   238 
   239 lemma upper_plus_left_absorb: "xs +\<sharp> (xs +\<sharp> ys) = xs +\<sharp> ys"
   240 by (rule aci_upper_plus.mult_left_idem)
   241 
   242 lemmas upper_plus_aci = aci_upper_plus.mult_ac_idem
   243 
   244 lemma upper_plus_less1: "xs +\<sharp> ys \<sqsubseteq> xs"
   245 apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
   246 apply (simp add: PDPlus_upper_less)
   247 done
   248 
   249 lemma upper_plus_less2: "xs +\<sharp> ys \<sqsubseteq> ys"
   250 by (subst upper_plus_commute, rule upper_plus_less1)
   251 
   252 lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> ys +\<sharp> zs"
   253 apply (subst upper_plus_absorb [of xs, symmetric])
   254 apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
   255 done
   256 
   257 lemma upper_less_plus_iff:
   258   "xs \<sqsubseteq> ys +\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
   259 apply safe
   260 apply (erule trans_less [OF _ upper_plus_less1])
   261 apply (erule trans_less [OF _ upper_plus_less2])
   262 apply (erule (1) upper_plus_greatest)
   263 done
   264 
   265 lemma upper_plus_less_unit_iff:
   266   "xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
   267  apply (rule iffI)
   268   apply (subgoal_tac
   269     "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>{z}\<sharp> \<or> f\<cdot>ys \<sqsubseteq> f\<cdot>{z}\<sharp>)")
   270    apply (drule admD, rule chain_approx)
   271     apply (drule_tac f="approx i" in monofun_cfun_arg)
   272     apply (cut_tac x="approx i\<cdot>xs" in upper_pd.compact_imp_principal, simp)
   273     apply (cut_tac x="approx i\<cdot>ys" in upper_pd.compact_imp_principal, simp)
   274     apply (cut_tac x="approx i\<cdot>z" in compact_basis.compact_imp_principal, simp)
   275     apply (clarify, simp add: upper_le_PDPlus_PDUnit_iff)
   276    apply simp
   277   apply simp
   278  apply (erule disjE)
   279   apply (erule trans_less [OF upper_plus_less1])
   280  apply (erule trans_less [OF upper_plus_less2])
   281 done
   282 
   283 lemma upper_unit_less_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y"
   284  apply (rule iffI)
   285   apply (rule profinite_less_ext)
   286   apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   287   apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   288   apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
   289   apply clarsimp
   290  apply (erule monofun_cfun_arg)
   291 done
   292 
   293 lemmas upper_pd_less_simps =
   294   upper_unit_less_iff
   295   upper_less_plus_iff
   296   upper_plus_less_unit_iff
   297 
   298 lemma upper_unit_eq_iff [simp]: "{x}\<sharp> = {y}\<sharp> \<longleftrightarrow> x = y"
   299 unfolding po_eq_conv by simp
   300 
   301 lemma upper_unit_strict [simp]: "{\<bottom>}\<sharp> = \<bottom>"
   302 unfolding inst_upper_pd_pcpo Rep_compact_bot [symmetric] by simp
   303 
   304 lemma upper_plus_strict1 [simp]: "\<bottom> +\<sharp> ys = \<bottom>"
   305 by (rule UU_I, rule upper_plus_less1)
   306 
   307 lemma upper_plus_strict2 [simp]: "xs +\<sharp> \<bottom> = \<bottom>"
   308 by (rule UU_I, rule upper_plus_less2)
   309 
   310 lemma upper_unit_strict_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
   311 unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
   312 
   313 lemma upper_plus_strict_iff [simp]:
   314   "xs +\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>"
   315 apply (rule iffI)
   316 apply (erule rev_mp)
   317 apply (rule upper_pd.principal_induct2 [where x=xs and y=ys], simp, simp)
   318 apply (simp add: inst_upper_pd_pcpo upper_pd.principal_eq_iff
   319                  upper_le_PDPlus_PDUnit_iff)
   320 apply auto
   321 done
   322 
   323 lemma compact_upper_unit_iff [simp]: "compact {x}\<sharp> \<longleftrightarrow> compact x"
   324 unfolding profinite_compact_iff by simp
   325 
   326 lemma compact_upper_plus [simp]:
   327   "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<sharp> ys)"
   328 by (auto dest!: upper_pd.compact_imp_principal)
   329 
   330 
   331 subsection {* Induction rules *}
   332 
   333 lemma upper_pd_induct1:
   334   assumes P: "adm P"
   335   assumes unit: "\<And>x. P {x}\<sharp>"
   336   assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> +\<sharp> ys)"
   337   shows "P (xs::'a upper_pd)"
   338 apply (induct xs rule: upper_pd.principal_induct, rule P)
   339 apply (induct_tac a rule: pd_basis_induct1)
   340 apply (simp only: upper_unit_Rep_compact_basis [symmetric])
   341 apply (rule unit)
   342 apply (simp only: upper_unit_Rep_compact_basis [symmetric]
   343                   upper_plus_principal [symmetric])
   344 apply (erule insert [OF unit])
   345 done
   346 
   347 lemma upper_pd_induct:
   348   assumes P: "adm P"
   349   assumes unit: "\<And>x. P {x}\<sharp>"
   350   assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<sharp> ys)"
   351   shows "P (xs::'a upper_pd)"
   352 apply (induct xs rule: upper_pd.principal_induct, rule P)
   353 apply (induct_tac a rule: pd_basis_induct)
   354 apply (simp only: upper_unit_Rep_compact_basis [symmetric] unit)
   355 apply (simp only: upper_plus_principal [symmetric] plus)
   356 done
   357 
   358 
   359 subsection {* Monadic bind *}
   360 
   361 definition
   362   upper_bind_basis ::
   363   "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where
   364   "upper_bind_basis = fold_pd
   365     (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
   366     (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
   367 
   368 lemma ACI_upper_bind:
   369   "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
   370 apply unfold_locales
   371 apply (simp add: upper_plus_assoc)
   372 apply (simp add: upper_plus_commute)
   373 apply (simp add: upper_plus_absorb eta_cfun)
   374 done
   375 
   376 lemma upper_bind_basis_simps [simp]:
   377   "upper_bind_basis (PDUnit a) =
   378     (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   379   "upper_bind_basis (PDPlus t u) =
   380     (\<Lambda> f. upper_bind_basis t\<cdot>f +\<sharp> upper_bind_basis u\<cdot>f)"
   381 unfolding upper_bind_basis_def
   382 apply -
   383 apply (rule fold_pd_PDUnit [OF ACI_upper_bind])
   384 apply (rule fold_pd_PDPlus [OF ACI_upper_bind])
   385 done
   386 
   387 lemma upper_bind_basis_mono:
   388   "t \<le>\<sharp> u \<Longrightarrow> upper_bind_basis t \<sqsubseteq> upper_bind_basis u"
   389 unfolding expand_cfun_less
   390 apply (erule upper_le_induct, safe)
   391 apply (simp add: monofun_cfun)
   392 apply (simp add: trans_less [OF upper_plus_less1])
   393 apply (simp add: upper_less_plus_iff)
   394 done
   395 
   396 definition
   397   upper_bind :: "'a upper_pd \<rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where
   398   "upper_bind = upper_pd.basis_fun upper_bind_basis"
   399 
   400 lemma upper_bind_principal [simp]:
   401   "upper_bind\<cdot>(upper_principal t) = upper_bind_basis t"
   402 unfolding upper_bind_def
   403 apply (rule upper_pd.basis_fun_principal)
   404 apply (erule upper_bind_basis_mono)
   405 done
   406 
   407 lemma upper_bind_unit [simp]:
   408   "upper_bind\<cdot>{x}\<sharp>\<cdot>f = f\<cdot>x"
   409 by (induct x rule: compact_basis.principal_induct, simp, simp)
   410 
   411 lemma upper_bind_plus [simp]:
   412   "upper_bind\<cdot>(xs +\<sharp> ys)\<cdot>f = upper_bind\<cdot>xs\<cdot>f +\<sharp> upper_bind\<cdot>ys\<cdot>f"
   413 by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp)
   414 
   415 lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   416 unfolding upper_unit_strict [symmetric] by (rule upper_bind_unit)
   417 
   418 
   419 subsection {* Map and join *}
   420 
   421 definition
   422   upper_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a upper_pd \<rightarrow> 'b upper_pd" where
   423   "upper_map = (\<Lambda> f xs. upper_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<sharp>))"
   424 
   425 definition
   426   upper_join :: "'a upper_pd upper_pd \<rightarrow> 'a upper_pd" where
   427   "upper_join = (\<Lambda> xss. upper_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
   428 
   429 lemma upper_map_unit [simp]:
   430   "upper_map\<cdot>f\<cdot>{x}\<sharp> = {f\<cdot>x}\<sharp>"
   431 unfolding upper_map_def by simp
   432 
   433 lemma upper_map_plus [simp]:
   434   "upper_map\<cdot>f\<cdot>(xs +\<sharp> ys) = upper_map\<cdot>f\<cdot>xs +\<sharp> upper_map\<cdot>f\<cdot>ys"
   435 unfolding upper_map_def by simp
   436 
   437 lemma upper_join_unit [simp]:
   438   "upper_join\<cdot>{xs}\<sharp> = xs"
   439 unfolding upper_join_def by simp
   440 
   441 lemma upper_join_plus [simp]:
   442   "upper_join\<cdot>(xss +\<sharp> yss) = upper_join\<cdot>xss +\<sharp> upper_join\<cdot>yss"
   443 unfolding upper_join_def by simp
   444 
   445 lemma upper_map_ident: "upper_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
   446 by (induct xs rule: upper_pd_induct, simp_all)
   447 
   448 lemma upper_map_map:
   449   "upper_map\<cdot>f\<cdot>(upper_map\<cdot>g\<cdot>xs) = upper_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
   450 by (induct xs rule: upper_pd_induct, simp_all)
   451 
   452 lemma upper_join_map_unit:
   453   "upper_join\<cdot>(upper_map\<cdot>upper_unit\<cdot>xs) = xs"
   454 by (induct xs rule: upper_pd_induct, simp_all)
   455 
   456 lemma upper_join_map_join:
   457   "upper_join\<cdot>(upper_map\<cdot>upper_join\<cdot>xsss) = upper_join\<cdot>(upper_join\<cdot>xsss)"
   458 by (induct xsss rule: upper_pd_induct, simp_all)
   459 
   460 lemma upper_join_map_map:
   461   "upper_join\<cdot>(upper_map\<cdot>(upper_map\<cdot>f)\<cdot>xss) =
   462    upper_map\<cdot>f\<cdot>(upper_join\<cdot>xss)"
   463 by (induct xss rule: upper_pd_induct, simp_all)
   464 
   465 lemma upper_map_approx: "upper_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs"
   466 by (induct xs rule: upper_pd_induct, simp_all)
   467 
   468 end