Theory Ssum

theory Ssum
imports Tr
(*  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"
  unfolding ssum_def by simp_all

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"
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 → '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)"
unfolding sscase_def by (simp add: cont_Rep_ssum)

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

lemma sscase2 [simp]: "x ≠ ⊥ ⟹ sscase⋅f⋅g⋅(sinl⋅x) = f⋅x"
unfolding beta_sscase by (simp add: Rep_ssum_sinl)

lemma sscase3 [simp]: "y ≠ ⊥ ⟹ sscase⋅f⋅g⋅(sinr⋅y) = g⋅y"
unfolding beta_sscase by (simp add: 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