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