Theory Ssum

(*  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