src/HOL/HOLCF/Ssum.thy
 author wenzelm Sun Nov 02 17:16:01 2014 +0100 (2014-11-02) changeset 58880 0baae4311a9f parent 49759 ecf1d5d87e5e child 61378 3e04c9ca001a permissions -rw-r--r--
modernized header;
 wenzelm@42151  1 (* Title: HOL/HOLCF/Ssum.thy  huffman@40502  2  Author: Franz Regensburger  huffman@40502  3  Author: Brian Huffman  huffman@15576  4 *)  huffman@15576  5 wenzelm@58880  6 section {* The type of strict sums *}  huffman@15576  7 huffman@15577  8 theory Ssum  huffman@31115  9 imports Tr  huffman@15577  10 begin  huffman@15576  11 wenzelm@36452  12 default_sort pcpo  huffman@16083  13 huffman@15593  14 subsection {* Definition of strict sum type *}  huffman@15593  15 wenzelm@45695  16 definition  wenzelm@45695  17  "ssum =  wenzelm@45695  18  {p :: tr \ ('a \ 'b). p = \ \  wenzelm@45695  19  (fst p = TT \ fst (snd p) \ \ \ snd (snd p) = \) \  wenzelm@45695  20  (fst p = FF \ fst (snd p) = \ \ snd (snd p) \ \)}"  wenzelm@45695  21 huffman@49759  22 pcpodef ('a, 'b) ssum (infixr "++" 10) = "ssum :: (tr \ 'a \ 'b) set"  wenzelm@45695  23  unfolding ssum_def by simp_all  huffman@15576  24 huffman@35525  25 instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin  huffman@40098  26 by (rule typedef_chfin [OF type_definition_ssum below_ssum_def])  huffman@25827  27 wenzelm@35427  28 type_notation (xsymbols)  wenzelm@35547  29  ssum ("(_ \/ _)" [21, 20] 20)  wenzelm@35427  30 type_notation (HTML output)  wenzelm@35547  31  ssum ("(_ \/ _)" [21, 20] 20)  wenzelm@35547  32 huffman@15576  33 huffman@16060  34 subsection {* Definitions of constructors *}  huffman@15576  35 wenzelm@25131  36 definition  wenzelm@25131  37  sinl :: "'a \ ('a ++ 'b)" where  huffman@40767  38  "sinl = (\ a. Abs_ssum (seq\a\TT, a, \))"  huffman@16060  39 wenzelm@25131  40 definition  wenzelm@25131  41  sinr :: "'b \ ('a ++ 'b)" where  huffman@40767  42  "sinr = (\ b. Abs_ssum (seq\b\FF, \, b))"  huffman@25740  43 huffman@40767  44 lemma sinl_ssum: "(seq\a\TT, a, \) \ ssum"  huffman@40767  45 by (simp add: ssum_def seq_conv_if)  huffman@25740  46 huffman@40767  47 lemma sinr_ssum: "(seq\b\FF, \, b) \ ssum"  huffman@40767  48 by (simp add: ssum_def seq_conv_if)  huffman@25740  49 huffman@40767  50 lemma Rep_ssum_sinl: "Rep_ssum (sinl\a) = (seq\a\TT, a, \)"  huffman@40098  51 by (simp add: sinl_def cont_Abs_ssum Abs_ssum_inverse sinl_ssum)  huffman@25740  52 huffman@40767  53 lemma Rep_ssum_sinr: "Rep_ssum (sinr\b) = (seq\b\FF, \, b)"  huffman@40098  54 by (simp add: sinr_def cont_Abs_ssum Abs_ssum_inverse sinr_ssum)  huffman@40092  55 huffman@40098  56 lemmas Rep_ssum_simps =  huffman@40098  57  Rep_ssum_inject [symmetric] below_ssum_def  huffman@44066  58  prod_eq_iff below_prod_def  huffman@40098  59  Rep_ssum_strict Rep_ssum_sinl Rep_ssum_sinr  huffman@16060  60 huffman@35900  61 subsection {* Properties of \emph{sinl} and \emph{sinr} *}  huffman@16060  62 huffman@25740  63 text {* Ordering *}  huffman@25740  64 huffman@31076  65 lemma sinl_below [simp]: "(sinl\x \ sinl\y) = (x \ y)"  huffman@40767  66 by (simp add: Rep_ssum_simps seq_conv_if)  huffman@25740  67 huffman@31076  68 lemma sinr_below [simp]: "(sinr\x \ sinr\y) = (x \ y)"  huffman@40767  69 by (simp add: Rep_ssum_simps seq_conv_if)  huffman@25740  70 huffman@31076  71 lemma sinl_below_sinr [simp]: "(sinl\x \ sinr\y) = (x = \)"  huffman@40767  72 by (simp add: Rep_ssum_simps seq_conv_if)  huffman@25740  73 huffman@31076  74 lemma sinr_below_sinl [simp]: "(sinr\x \ sinl\y) = (x = \)"  huffman@40767  75 by (simp add: Rep_ssum_simps seq_conv_if)  huffman@25740  76 huffman@25740  77 text {* Equality *}  huffman@25740  78 huffman@25740  79 lemma sinl_eq [simp]: "(sinl\x = sinl\y) = (x = y)"  huffman@25740  80 by (simp add: po_eq_conv)  huffman@25740  81 huffman@25740  82 lemma sinr_eq [simp]: "(sinr\x = sinr\y) = (x = y)"  huffman@25740  83 by (simp add: po_eq_conv)  huffman@25740  84 huffman@25740  85 lemma sinl_eq_sinr [simp]: "(sinl\x = sinr\y) = (x = \ \ y = \)"  huffman@25740  86 by (subst po_eq_conv, simp)  huffman@25740  87 huffman@25740  88 lemma sinr_eq_sinl [simp]: "(sinr\x = sinl\y) = (x = \ \ y = \)"  huffman@25740  89 by (subst po_eq_conv, simp)  huffman@25740  90 huffman@25740  91 lemma sinl_inject: "sinl\x = sinl\y \ x = y"  huffman@25740  92 by (rule sinl_eq [THEN iffD1])  huffman@25740  93 huffman@25740  94 lemma sinr_inject: "sinr\x = sinr\y \ x = y"  huffman@25740  95 by (rule sinr_eq [THEN iffD1])  huffman@25740  96 huffman@25740  97 text {* Strictness *}  huffman@17837  98 huffman@16211  99 lemma sinl_strict [simp]: "sinl\\ = \"  huffman@40098  100 by (simp add: Rep_ssum_simps)  huffman@15576  101 huffman@16211  102 lemma sinr_strict [simp]: "sinr\\ = \"  huffman@40098  103 by (simp add: Rep_ssum_simps)  huffman@16060  104 huffman@40321  105 lemma sinl_bottom_iff [simp]: "(sinl\x = \) = (x = \)"  huffman@40080  106 using sinl_eq [of "x" "\"] by simp  huffman@15576  107 huffman@40321  108 lemma sinr_bottom_iff [simp]: "(sinr\x = \) = (x = \)"  huffman@40080  109 using sinr_eq [of "x" "\"] by simp  huffman@15576  110 huffman@40081  111 lemma sinl_defined: "x \ \ \ sinl\x \ \"  huffman@16752  112 by simp  huffman@16752  113 huffman@40081  114 lemma sinr_defined: "x \ \ \ sinr\x \ \"  huffman@16752  115 by simp  huffman@16752  116 huffman@25882  117 text {* Compactness *}  huffman@25882  118 huffman@25882  119 lemma compact_sinl: "compact x \ compact (sinl\x)"  huffman@40098  120 by (rule compact_ssum, simp add: Rep_ssum_sinl)  huffman@25882  121 huffman@25882  122 lemma compact_sinr: "compact x \ compact (sinr\x)"  huffman@40098  123 by (rule compact_ssum, simp add: Rep_ssum_sinr)  huffman@25882  124 huffman@25882  125 lemma compact_sinlD: "compact (sinl\x) \ compact x"  huffman@25882  126 unfolding compact_def  huffman@40327  127 by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinl]], simp)  huffman@25882  128 huffman@25882  129 lemma compact_sinrD: "compact (sinr\x) \ compact x"  huffman@25882  130 unfolding compact_def  huffman@40327  131 by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinr]], simp)  huffman@25882  132 huffman@25882  133 lemma compact_sinl_iff [simp]: "compact (sinl\x) = compact x"  huffman@25882  134 by (safe elim!: compact_sinl compact_sinlD)  huffman@25882  135 huffman@25882  136 lemma compact_sinr_iff [simp]: "compact (sinr\x) = compact x"  huffman@25882  137 by (safe elim!: compact_sinr compact_sinrD)  huffman@25882  138 huffman@16060  139 subsection {* Case analysis *}  huffman@16060  140 huffman@35783  141 lemma ssumE [case_names bottom sinl sinr, cases type: ssum]:  huffman@40080  142  obtains "p = \"  huffman@40080  143  | x where "p = sinl\x" and "x \ \"  huffman@40080  144  | y where "p = sinr\y" and "y \ \"  huffman@40098  145 using Rep_ssum [of p] by (auto simp add: ssum_def Rep_ssum_simps)  huffman@15576  146 huffman@35783  147 lemma ssum_induct [case_names bottom sinl sinr, induct type: ssum]:  huffman@25756  148  "\P \;  huffman@25756  149  \x. x \ \ \ P (sinl\x);  huffman@25756  150  \y. y \ \ \ P (sinr\y)\ \ P x"  huffman@25756  151 by (cases x, simp_all)  huffman@25756  152 huffman@35783  153 lemma ssumE2 [case_names sinl sinr]:  huffman@16060  154  "\\x. p = sinl\x \ Q; \y. p = sinr\y \ Q\ \ Q"  huffman@25740  155 by (cases p, simp only: sinl_strict [symmetric], simp, simp)  huffman@16060  156 huffman@31076  157 lemma below_sinlD: "p \ sinl\x \ \y. p = sinl\y \ y \ x"  huffman@25740  158 by (cases p, rule_tac x="\" in exI, simp_all)  huffman@15576  159 huffman@31076  160 lemma below_sinrD: "p \ sinr\x \ \y. p = sinr\y \ y \ x"  huffman@25740  161 by (cases p, rule_tac x="\" in exI, simp_all)  huffman@16060  162 huffman@25740  163 subsection {* Case analysis combinator *}  huffman@16060  164 wenzelm@25131  165 definition  wenzelm@25131  166  sscase :: "('a \ 'c) \ ('b \ 'c) \ ('a ++ 'b) \ 'c" where  huffman@40322  167  "sscase = (\ f g s. (\(t, x, y). If t then f\x else g\y) (Rep_ssum s))"  huffman@16060  168 huffman@16060  169 translations  huffman@26046  170  "case s of XCONST sinl\x \ t1 | XCONST sinr\y \ t2" == "CONST sscase\(\ x. t1)\(\ y. t2)\s"  wenzelm@46125  171  "case s of (XCONST sinl :: 'a)\x \ t1 | XCONST sinr\y \ t2" => "CONST sscase\(\ x. t1)\(\ y. t2)\s"  huffman@18078  172 huffman@18078  173 translations  huffman@26046  174  "\(XCONST sinl\x). t" == "CONST sscase\(\ x. t)\\"  huffman@26046  175  "\(XCONST sinr\y). t" == "CONST sscase\\\(\ y. t)"  huffman@16060  176 huffman@25740  177 lemma beta_sscase:  huffman@40322  178  "sscase\f\g\s = (\(t, x, y). If t then f\x else g\y) (Rep_ssum s)"  huffman@40834  179 unfolding sscase_def by (simp add: cont_Rep_ssum)  huffman@16060  180 huffman@16060  181 lemma sscase1 [simp]: "sscase\f\g\\ = \"  huffman@40098  182 unfolding beta_sscase by (simp add: Rep_ssum_strict)  huffman@15576  183 huffman@16060  184 lemma sscase2 [simp]: "x \ \ \ sscase\f\g\(sinl\x) = f\x"  huffman@40098  185 unfolding beta_sscase by (simp add: Rep_ssum_sinl)  huffman@15576  186 huffman@16060  187 lemma sscase3 [simp]: "y \ \ \ sscase\f\g\(sinr\y) = g\y"  huffman@40098  188 unfolding beta_sscase by (simp add: Rep_ssum_sinr)  huffman@15593  189 huffman@16060  190 lemma sscase4 [simp]: "sscase\sinl\sinr\z = z"  huffman@25756  191 by (cases z, simp_all)  huffman@15593  192 huffman@25827  193 subsection {* Strict sum preserves flatness *}  huffman@25827  194 huffman@35525  195 instance ssum :: (flat, flat) flat  huffman@25827  196 apply (intro_classes, clarify)  huffman@31115  197 apply (case_tac x, simp)  huffman@31115  198 apply (case_tac y, simp_all add: flat_below_iff)  huffman@31115  199 apply (case_tac y, simp_all add: flat_below_iff)  huffman@25827  200 done  huffman@25827  201 huffman@15576  202 end