src/HOLCF/Ssum.thy
 author huffman Tue Oct 12 06:20:05 2010 -0700 (2010-10-12) changeset 40006 116e94f9543b parent 40002 c5b5f7a3a3b1 child 40046 ba2e41c8b725 permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
     1 (*  Title:      HOLCF/Ssum.thy

     2     Author:     Franz Regensburger and Brian Huffman

     3 *)

     4

     5 header {* The type of strict sums *}

     6

     7 theory Ssum

     8 imports Tr

     9 begin

    10

    11 default_sort pcpo

    12

    13 subsection {* Definition of strict sum type *}

    14

    15 pcpodef (Ssum)  ('a, 'b) ssum (infixr "++" 10) =

    16   "{p :: tr \<times> ('a \<times> 'b).

    17     (fst p \<sqsubseteq> TT \<longleftrightarrow> snd (snd p) = \<bottom>) \<and>

    18     (fst p \<sqsubseteq> FF \<longleftrightarrow> fst (snd p) = \<bottom>)}"

    19 by simp_all

    20

    21 instance ssum :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po

    22 by (rule typedef_finite_po [OF type_definition_Ssum])

    23

    24 instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin

    25 by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])

    26

    27 type_notation (xsymbols)

    28   ssum  ("(_ \<oplus>/ _)" [21, 20] 20)

    29 type_notation (HTML output)

    30   ssum  ("(_ \<oplus>/ _)" [21, 20] 20)

    31

    32

    33 subsection {* Definitions of constructors *}

    34

    35 definition

    36   sinl :: "'a \<rightarrow> ('a ++ 'b)" where

    37   "sinl = (\<Lambda> a. Abs_Ssum (strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>))"

    38

    39 definition

    40   sinr :: "'b \<rightarrow> ('a ++ 'b)" where

    41   "sinr = (\<Lambda> b. Abs_Ssum (strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b))"

    42

    43 lemma sinl_Ssum: "(strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>) \<in> Ssum"

    44 by (simp add: Ssum_def strictify_conv_if)

    45

    46 lemma sinr_Ssum: "(strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b) \<in> Ssum"

    47 by (simp add: Ssum_def strictify_conv_if)

    48

    49 lemma sinl_Abs_Ssum: "sinl\<cdot>a = Abs_Ssum (strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>)"

    50 by (unfold sinl_def, simp add: cont_Abs_Ssum sinl_Ssum)

    51

    52 lemma sinr_Abs_Ssum: "sinr\<cdot>b = Abs_Ssum (strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b)"

    53 by (unfold sinr_def, simp add: cont_Abs_Ssum sinr_Ssum)

    54

    55 lemma Rep_Ssum_sinl: "Rep_Ssum (sinl\<cdot>a) = (strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>)"

    56 by (simp add: sinl_Abs_Ssum Abs_Ssum_inverse sinl_Ssum)

    57

    58 lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = (strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b)"

    59 by (simp add: sinr_Abs_Ssum Abs_Ssum_inverse sinr_Ssum)

    60

    61 subsection {* Properties of \emph{sinl} and \emph{sinr} *}

    62

    63 text {* Ordering *}

    64

    65 lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"

    66 by (simp add: below_Ssum_def Rep_Ssum_sinl strictify_conv_if)

    67

    68 lemma sinr_below [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"

    69 by (simp add: below_Ssum_def Rep_Ssum_sinr strictify_conv_if)

    70

    71 lemma sinl_below_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"

    72 by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if)

    73

    74 lemma sinr_below_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"

    75 by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if)

    76

    77 text {* Equality *}

    78

    79 lemma sinl_eq [simp]: "(sinl\<cdot>x = sinl\<cdot>y) = (x = y)"

    80 by (simp add: po_eq_conv)

    81

    82 lemma sinr_eq [simp]: "(sinr\<cdot>x = sinr\<cdot>y) = (x = y)"

    83 by (simp add: po_eq_conv)

    84

    85 lemma sinl_eq_sinr [simp]: "(sinl\<cdot>x = sinr\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"

    86 by (subst po_eq_conv, simp)

    87

    88 lemma sinr_eq_sinl [simp]: "(sinr\<cdot>x = sinl\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"

    89 by (subst po_eq_conv, simp)

    90

    91 lemma sinl_inject: "sinl\<cdot>x = sinl\<cdot>y \<Longrightarrow> x = y"

    92 by (rule sinl_eq [THEN iffD1])

    93

    94 lemma sinr_inject: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y"

    95 by (rule sinr_eq [THEN iffD1])

    96

    97 text {* Strictness *}

    98

    99 lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>"

   100 by (simp add: sinl_Abs_Ssum Abs_Ssum_strict)

   101

   102 lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"

   103 by (simp add: sinr_Abs_Ssum Abs_Ssum_strict)

   104

   105 lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"

   106 by (cut_tac sinl_eq [of "x" "\<bottom>"], simp)

   107

   108 lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"

   109 by (cut_tac sinr_eq [of "x" "\<bottom>"], simp)

   110

   111 lemma sinl_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"

   112 by simp

   113

   114 lemma sinr_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"

   115 by simp

   116

   117 text {* Compactness *}

   118

   119 lemma compact_sinl: "compact x \<Longrightarrow> compact (sinl\<cdot>x)"

   120 by (rule compact_Ssum, simp add: Rep_Ssum_sinl strictify_conv_if)

   121

   122 lemma compact_sinr: "compact x \<Longrightarrow> compact (sinr\<cdot>x)"

   123 by (rule compact_Ssum, simp add: Rep_Ssum_sinr strictify_conv_if)

   124

   125 lemma compact_sinlD: "compact (sinl\<cdot>x) \<Longrightarrow> compact x"

   126 unfolding compact_def

   127 by (drule adm_subst [OF cont_Rep_CFun2 [where f=sinl]], simp)

   128

   129 lemma compact_sinrD: "compact (sinr\<cdot>x) \<Longrightarrow> compact x"

   130 unfolding compact_def

   131 by (drule adm_subst [OF cont_Rep_CFun2 [where f=sinr]], simp)

   132

   133 lemma compact_sinl_iff [simp]: "compact (sinl\<cdot>x) = compact x"

   134 by (safe elim!: compact_sinl compact_sinlD)

   135

   136 lemma compact_sinr_iff [simp]: "compact (sinr\<cdot>x) = compact x"

   137 by (safe elim!: compact_sinr compact_sinrD)

   138

   139 subsection {* Case analysis *}

   140

   141 lemma Exh_Ssum:

   142   "z = \<bottom> \<or> (\<exists>a. z = sinl\<cdot>a \<and> a \<noteq> \<bottom>) \<or> (\<exists>b. z = sinr\<cdot>b \<and> b \<noteq> \<bottom>)"

   143 apply (induct z rule: Abs_Ssum_induct)

   144 apply (case_tac y, rename_tac t a b)

   145 apply (case_tac t rule: trE)

   146 apply (rule disjI1)

   147 apply (simp add: Ssum_def Abs_Ssum_strict)

   148 apply (rule disjI2, rule disjI1, rule_tac x=a in exI)

   149 apply (simp add: sinl_Abs_Ssum Ssum_def)

   150 apply (rule disjI2, rule disjI2, rule_tac x=b in exI)

   151 apply (simp add: sinr_Abs_Ssum Ssum_def)

   152 done

   153

   154 lemma ssumE [case_names bottom sinl sinr, cases type: ssum]:

   155   "\<lbrakk>p = \<bottom> \<Longrightarrow> Q;

   156    \<And>x. \<lbrakk>p = sinl\<cdot>x; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q;

   157    \<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"

   158 using Exh_Ssum [of p] by auto

   159

   160 lemma ssum_induct [case_names bottom sinl sinr, induct type: ssum]:

   161   "\<lbrakk>P \<bottom>;

   162    \<And>x. x \<noteq> \<bottom> \<Longrightarrow> P (sinl\<cdot>x);

   163    \<And>y. y \<noteq> \<bottom> \<Longrightarrow> P (sinr\<cdot>y)\<rbrakk> \<Longrightarrow> P x"

   164 by (cases x, simp_all)

   165

   166 lemma ssumE2 [case_names sinl sinr]:

   167   "\<lbrakk>\<And>x. p = sinl\<cdot>x \<Longrightarrow> Q; \<And>y. p = sinr\<cdot>y \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"

   168 by (cases p, simp only: sinl_strict [symmetric], simp, simp)

   169

   170 lemma below_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x"

   171 by (cases p, rule_tac x="\<bottom>" in exI, simp_all)

   172

   173 lemma below_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x"

   174 by (cases p, rule_tac x="\<bottom>" in exI, simp_all)

   175

   176 subsection {* Case analysis combinator *}

   177

   178 definition

   179   sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c" where

   180   "sscase = (\<Lambda> f g s. (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y fi) (Rep_Ssum s))"

   181

   182 translations

   183   "case s of XCONST sinl\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" == "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"

   184

   185 translations

   186   "\<Lambda>(XCONST sinl\<cdot>x). t" == "CONST sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"

   187   "\<Lambda>(XCONST sinr\<cdot>y). t" == "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"

   188

   189 lemma beta_sscase:

   190   "sscase\<cdot>f\<cdot>g\<cdot>s = (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y fi) (Rep_Ssum s)"

   191 unfolding sscase_def by (simp add: cont_Rep_Ssum [THEN cont_compose])

   192

   193 lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"

   194 unfolding beta_sscase by (simp add: Rep_Ssum_strict)

   195

   196 lemma sscase2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = f\<cdot>x"

   197 unfolding beta_sscase by (simp add: Rep_Ssum_sinl)

   198

   199 lemma sscase3 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>y) = g\<cdot>y"

   200 unfolding beta_sscase by (simp add: Rep_Ssum_sinr)

   201

   202 lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z"

   203 by (cases z, simp_all)

   204

   205 subsection {* Strict sum preserves flatness *}

   206

   207 instance ssum :: (flat, flat) flat

   208 apply (intro_classes, clarify)

   209 apply (case_tac x, simp)

   210 apply (case_tac y, simp_all add: flat_below_iff)

   211 apply (case_tac y, simp_all add: flat_below_iff)

   212 done

   213

   214 subsection {* Map function for strict sums *}

   215

   216 definition

   217   ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"

   218 where

   219   "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"

   220

   221 lemma ssum_map_strict [simp]: "ssum_map\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"

   222 unfolding ssum_map_def by simp

   223

   224 lemma ssum_map_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"

   225 unfolding ssum_map_def by simp

   226

   227 lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"

   228 unfolding ssum_map_def by simp

   229

   230 lemma ssum_map_sinl': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"

   231 by (cases "x = \<bottom>") simp_all

   232

   233 lemma ssum_map_sinr': "g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"

   234 by (cases "x = \<bottom>") simp_all

   235

   236 lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"

   237 unfolding ssum_map_def by (simp add: cfun_eq_iff eta_cfun)

   238

   239 lemma ssum_map_map:

   240   "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>

   241     ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =

   242      ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"

   243 apply (induct p, simp)

   244 apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp)

   245 apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp)

   246 done

   247

   248 lemma ep_pair_ssum_map:

   249   assumes "ep_pair e1 p1" and "ep_pair e2 p2"

   250   shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)"

   251 proof

   252   interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact

   253   interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact

   254   fix x show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x"

   255     by (induct x) simp_all

   256   fix y show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"

   257     apply (induct y, simp)

   258     apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below)

   259     apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below)

   260     done

   261 qed

   262

   263 lemma deflation_ssum_map:

   264   assumes "deflation d1" and "deflation d2"

   265   shows "deflation (ssum_map\<cdot>d1\<cdot>d2)"

   266 proof

   267   interpret d1: deflation d1 by fact

   268   interpret d2: deflation d2 by fact

   269   fix x

   270   show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x"

   271     apply (induct x, simp)

   272     apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.idem)

   273     apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.idem)

   274     done

   275   show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"

   276     apply (induct x, simp)

   277     apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.below)

   278     apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.below)

   279     done

   280 qed

   281

   282 lemma finite_deflation_ssum_map:

   283   assumes "finite_deflation d1" and "finite_deflation d2"

   284   shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)"

   285 proof (rule finite_deflation_intro)

   286   interpret d1: finite_deflation d1 by fact

   287   interpret d2: finite_deflation d2 by fact

   288   have "deflation d1" and "deflation d2" by fact+

   289   thus "deflation (ssum_map\<cdot>d1\<cdot>d2)" by (rule deflation_ssum_map)

   290   have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq>

   291         (\<lambda>x. sinl\<cdot>x)  {x. d1\<cdot>x = x} \<union>

   292         (\<lambda>x. sinr\<cdot>x)  {x. d2\<cdot>x = x} \<union> {\<bottom>}"

   293     by (rule subsetI, case_tac x, simp_all)

   294   thus "finite {x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x}"

   295     by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)

   296 qed

   297

   298 end