Quelle  Ssum.thy   Sprache: Isabelle

(*  Title:      HOL/HOLCF/Ssum.thy
    Author:     Franz Regensburger
    Author:     Brian Huffman
*)

section ‹The type of strict sums›

theory Ssum
  imports Tr
begin

subsection ‹Definition of strict sum type›

definition "ssum =
  {p :: tr × ('a::pcpo \ 'b::pcpo). p = ⊥ ∨
    (fst p = TT ∧ fst (snd p) ≠ ⊥ ∧ snd (snd p) = ⊥) ∨
    (fst p = FF ∧ fst (snd p) = ⊥ ∧ snd (snd p) ≠ ⊥)}"

pcpodef ('a::pcpo, 'b::pcpo) ssum  (‹(‹notation=‹infix strict sum››_ ⊕/ _)› [21, 20] 20) =
  "ssum :: (tr \ 'a \ 'b) set"
  by (simp_all add: ssum_def)

instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
  by (rule typedef_chfin [OF type_definition_ssum below_ssum_def])

type_notation (ASCII)
  ssum  (infixr ‹++› 10)


subsection ‹Definitions of constructors›

definition sinl :: "'a::pcpo \ ('a ++ 'b::pcpo)"
  where "sinl = (\ a. Abs_ssum (seq\a\TT, a, \))"

definition sinr :: "'b::pcpo \ ('a::pcpo ++ 'b)"
  where "sinr = (\ b. Abs_ssum (seq\b\FF, \, b))"

lemma sinl_ssum: "(seq\a\TT, a, \) \ ssum"
  by (simp add: ssum_def seq_conv_if)

lemma sinr_ssum: "(seq\b\FF, \, b) \ ssum"
  by (simp add: ssum_def seq_conv_if)

lemma Rep_ssum_sinl: "Rep_ssum (sinl\a) = (seq\a\TT, a, \)"
  by (simp add: sinl_def cont_Abs_ssum Abs_ssum_inverse sinl_ssum)

lemma Rep_ssum_sinr: "Rep_ssum (sinr\b) = (seq\b\FF, \, b)"
  by (simp add: sinr_def cont_Abs_ssum Abs_ssum_inverse sinr_ssum)

lemmas Rep_ssum_simps =
  Rep_ssum_inject [symmetric] below_ssum_def
  prod_eq_iff below_prod_def
  Rep_ssum_strict Rep_ssum_sinl Rep_ssum_sinr


subsection ‹Properties of \emph{sinl} and \emph{sinr}›

text ‹Ordering›

lemma sinl_below [simp]: "sinl\x \ sinl\y \ x \ y"
  by (simp add: Rep_ssum_simps seq_conv_if)

lemma sinr_below [simp]: "sinr\x \ sinr\y \ x \ y"
  by (simp add: Rep_ssum_simps seq_conv_if)

lemma sinl_below_sinr [simp]: "sinl\x \ sinr\y \ x = \"
  by (simp add: Rep_ssum_simps seq_conv_if)

lemma sinr_below_sinl [simp]: "sinr\x \ sinl\y \ x = \"
  by (simp add: Rep_ssum_simps seq_conv_if)

text ‹Equality›

lemma sinl_eq [simp]: "sinl\x = sinl\y \ x = y"
  by (simp add: po_eq_conv)

lemma sinr_eq [simp]: "sinr\x = sinr\y \ x = y"
  by (simp add: po_eq_conv)

lemma sinl_eq_sinr [simp]: "sinl\x = sinr\y \ x = \ \ y = \"
  by (subst po_eq_conv) simp

lemma sinr_eq_sinl [simp]: "sinr\x = sinl\y \ x = \ \ y = \"
  by (subst po_eq_conv) simp

lemma sinl_inject: "sinl\x = sinl\y \ x = y"
  by (rule sinl_eq [THEN iffD1])

lemma sinr_inject: "sinr\x = sinr\y \ x = y"
  by (rule sinr_eq [THEN iffD1])

text ‹Strictness›

lemma sinl_strict [simp]: "sinl\\ = \"
  by (simp add: Rep_ssum_simps)

lemma sinr_strict [simp]: "sinr\\ = \"
  by (simp add: Rep_ssum_simps)

lemma sinl_bottom_iff [simp]: "sinl\x = \ \ x = \"
  using sinl_eq [of "x" "\"] by simp

lemma sinr_bottom_iff [simp]: "sinr\x = \ \ x = \"
  using sinr_eq [of "x" "\"] by simp

lemma sinl_defined: "x \ \ \ sinl\x \ \"
  by simp

lemma sinr_defined: "x \ \ \ sinr\x \ \"
  by simp

text ‹Compactness›

lemma compact_sinl: "compact x \ compact (sinl\x)"
  by (rule compact_ssum) (simp add: Rep_ssum_sinl)

lemma compact_sinr: "compact x \ compact (sinr\x)"
  by (rule compact_ssum) (simp add: Rep_ssum_sinr)

lemma compact_sinlD: "compact (sinl\x) \ compact x"
  unfolding compact_def
  by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinl]], simp)

lemma compact_sinrD: "compact (sinr\x) \ compact x"
  unfolding compact_def
  by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinr]], simp)

lemma compact_sinl_iff [simp]: "compact (sinl\x) = compact x"
  by (safe elim!: compact_sinl compact_sinlD)

lemma compact_sinr_iff [simp]: "compact (sinr\x) = compact x"
  by (safe elim!: compact_sinr compact_sinrD)


subsection ‹Case analysis›

lemma ssumE [case_names bottom sinl sinr, cases type: ssum]:
  obtains "p = \"
  | x where "p = sinl\x" and "x \ \"
  | y where "p = sinr\y" and "y \ \"
  using Rep_ssum [of p] by (auto simp add: ssum_def Rep_ssum_simps)

lemma ssum_induct [case_names bottom sinl sinr, induct type: ssum]:
  "\P \;
   ∧x. x ≠ ⊥ ==> P (sinl⋅x);
   ∧y. y ≠ ⊥ ==> P (sinr⋅y)] ==> P x"
  by (cases x) simp_all

lemma ssumE2 [case_names sinl sinr]:
  "\\x. p = sinl\x \ Q; \y. p = sinr\y \ Q\ \ Q"
  by (cases p, simp only: sinl_strict [symmetric], simp, simp)

lemma below_sinlD: "p \ sinl\x \ \y. p = sinl\y \ y \ x"
  by (cases p, rule_tac x="\" in exI, simp_all)

lemma below_sinrD: "p \ sinr\x \ \y. p = sinr\y \ y \ x"
  by (cases p, rule_tac x="\" in exI, simp_all)


subsection ‹Case analysis combinator›

definition sscase :: "('a::pcpo \ 'c::pcpo) \ ('b::pcpo \ 'c) \ ('a ++ 'b) \ 'c"
  where "sscase = (\ f g s. (\(t, x, y). If t then f\x else g\y) (Rep_ssum s))"

translations
  "case s of XCONST sinl\x \ t1 | XCONST sinr\y \ t2" ⇌ "CONST sscase\(\ x. t1)\(\ y. t2)\s"
  "case s of (XCONST sinl :: 'a)\x \ t1 | XCONST sinr\y \ t2" ⇀ "CONST sscase\(\ x. t1)\(\ y. t2)\s"

translations
  "\(XCONST sinl\x). t" ⇌ "CONST sscase\(\ x. t)\\"
  "\(XCONST sinr\y). t" ⇌ "CONST sscase\\\(\ y. t)"

lemma beta_sscase: "sscase\f\g\s = (\(t, x, y). If t then f\x else g\y) (Rep_ssum s)"
  by (simp add: sscase_def cont_Rep_ssum)

lemma sscase1 [simp]: "sscase\f\g\\ = \"
  by (simp add: beta_sscase Rep_ssum_strict)

lemma sscase2 [simp]: "x \ \ \ sscase\f\g\(sinl\x) = f\x"
  by (simp add: beta_sscase Rep_ssum_sinl)

lemma sscase3 [simp]: "y \ \ \ sscase\f\g\(sinr\y) = g\y"
  by (simp add: beta_sscase Rep_ssum_sinr)

lemma sscase4 [simp]: "sscase\sinl\sinr\z = z"
  by (cases z) simp_all


subsection ‹Strict sum preserves flatness›

instance ssum :: (flat, flat) flat
  apply (intro_classes, clarify)
  apply (case_tac x, simp)
   apply (case_tac y, simp_all add: flat_below_iff)
  apply (case_tac y, simp_all add: flat_below_iff)
  done

end