# Theory Ssum

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

section ‹The type of strict sums›

theory Ssum
imports Tr
begin

default_sort pcpo

subsection ‹Definition of strict sum type›

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

pcpodef ('a, 'b) ssum  ("(_ ⊕/ _)" [21, 20] 20) = "ssum :: (tr × 'a × 'b) set"

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 → ('a ++ 'b)"
where "sinl = (Λ a. Abs_ssum (seq⋅a⋅TT, a, ⊥))"

definition sinr :: "'b → ('a ++ 'b)"
where "sinr = (Λ b. Abs_ssum (seq⋅b⋅FF, ⊥, b))"

lemma sinl_ssum: "(seq⋅a⋅TT, a, ⊥) ∈ ssum"

lemma sinr_ssum: "(seq⋅b⋅FF, ⊥, b) ∈ ssum"

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"

lemma sinr_below [simp]: "sinr⋅x ⊑ sinr⋅y ⟷ x ⊑ y"

lemma sinl_below_sinr [simp]: "sinl⋅x ⊑ sinr⋅y ⟷ x = ⊥"

lemma sinr_below_sinl [simp]: "sinr⋅x ⊑ sinl⋅y ⟷ x = ⊥"

text ‹Equality›

lemma sinl_eq [simp]: "sinl⋅x = sinl⋅y ⟷ x = y"

lemma sinr_eq [simp]: "sinr⋅x = sinr⋅y ⟷ x = y"

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⋅⊥ = ⊥"

lemma sinr_strict [simp]: "sinr⋅⊥ = ⊥"

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 → 'c) → ('b → '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)"

lemma sscase1 [simp]: "sscase⋅f⋅g⋅⊥ = ⊥"

lemma sscase2 [simp]: "x ≠ ⊥ ⟹ sscase⋅f⋅g⋅(sinl⋅x) = f⋅x"

lemma sscase3 [simp]: "y ≠ ⊥ ⟹ sscase⋅f⋅g⋅(sinr⋅y) = g⋅y"

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