src/HOLCF/Ssum.thy
changeset 40502 8e92772bc0e8
parent 40327 1dfdbd66093a
child 40767 a3e505b236e7
     1.1 --- a/src/HOLCF/Ssum.thy	Wed Nov 10 14:59:52 2010 -0800
     1.2 +++ b/src/HOLCF/Ssum.thy	Wed Nov 10 17:56:08 2010 -0800
     1.3 @@ -1,5 +1,6 @@
     1.4  (*  Title:      HOLCF/Ssum.thy
     1.5 -    Author:     Franz Regensburger and Brian Huffman
     1.6 +    Author:     Franz Regensburger
     1.7 +    Author:     Brian Huffman
     1.8  *)
     1.9  
    1.10  header {* The type of strict sums *}
    1.11 @@ -194,88 +195,4 @@
    1.12  apply (case_tac y, simp_all add: flat_below_iff)
    1.13  done
    1.14  
    1.15 -subsection {* Map function for strict sums *}
    1.16 -
    1.17 -definition
    1.18 -  ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
    1.19 -where
    1.20 -  "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"
    1.21 -
    1.22 -lemma ssum_map_strict [simp]: "ssum_map\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
    1.23 -unfolding ssum_map_def by simp
    1.24 -
    1.25 -lemma ssum_map_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
    1.26 -unfolding ssum_map_def by simp
    1.27 -
    1.28 -lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
    1.29 -unfolding ssum_map_def by simp
    1.30 -
    1.31 -lemma ssum_map_sinl': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
    1.32 -by (cases "x = \<bottom>") simp_all
    1.33 -
    1.34 -lemma ssum_map_sinr': "g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
    1.35 -by (cases "x = \<bottom>") simp_all
    1.36 -
    1.37 -lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
    1.38 -unfolding ssum_map_def by (simp add: cfun_eq_iff eta_cfun)
    1.39 -
    1.40 -lemma ssum_map_map:
    1.41 -  "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
    1.42 -    ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =
    1.43 -     ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    1.44 -apply (induct p, simp)
    1.45 -apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp)
    1.46 -apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp)
    1.47 -done
    1.48 -
    1.49 -lemma ep_pair_ssum_map:
    1.50 -  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    1.51 -  shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)"
    1.52 -proof
    1.53 -  interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
    1.54 -  interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
    1.55 -  fix x show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
    1.56 -    by (induct x) simp_all
    1.57 -  fix y show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
    1.58 -    apply (induct y, simp)
    1.59 -    apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below)
    1.60 -    apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below)
    1.61 -    done
    1.62 -qed
    1.63 -
    1.64 -lemma deflation_ssum_map:
    1.65 -  assumes "deflation d1" and "deflation d2"
    1.66 -  shows "deflation (ssum_map\<cdot>d1\<cdot>d2)"
    1.67 -proof
    1.68 -  interpret d1: deflation d1 by fact
    1.69 -  interpret d2: deflation d2 by fact
    1.70 -  fix x
    1.71 -  show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x"
    1.72 -    apply (induct x, simp)
    1.73 -    apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.idem)
    1.74 -    apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.idem)
    1.75 -    done
    1.76 -  show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
    1.77 -    apply (induct x, simp)
    1.78 -    apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.below)
    1.79 -    apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.below)
    1.80 -    done
    1.81 -qed
    1.82 -
    1.83 -lemma finite_deflation_ssum_map:
    1.84 -  assumes "finite_deflation d1" and "finite_deflation d2"
    1.85 -  shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)"
    1.86 -proof (rule finite_deflation_intro)
    1.87 -  interpret d1: finite_deflation d1 by fact
    1.88 -  interpret d2: finite_deflation d2 by fact
    1.89 -  have "deflation d1" and "deflation d2" by fact+
    1.90 -  thus "deflation (ssum_map\<cdot>d1\<cdot>d2)" by (rule deflation_ssum_map)
    1.91 -  have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq>
    1.92 -        (\<lambda>x. sinl\<cdot>x) ` {x. d1\<cdot>x = x} \<union>
    1.93 -        (\<lambda>x. sinr\<cdot>x) ` {x. d2\<cdot>x = x} \<union> {\<bottom>}"
    1.94 -    by (rule subsetI, case_tac x, simp_all)
    1.95 -  thus "finite {x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
    1.96 -    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    1.97 -qed
    1.98 -
    1.99  end