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