Theory Sum_Type

(*  Title:      HOL/Sum_Type.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge
*)

section ‹The Disjoint Sum of Two Types›

theory Sum_Type
  imports Typedef Inductive Fun
begin

subsection ‹Construction of the sum type and its basic abstract operations›

definition Inl_Rep :: "'a ⇒ 'a ⇒ 'b ⇒ bool ⇒ bool"
  where "Inl_Rep a x y p ⟷ x = a ∧ p"

definition Inr_Rep :: "'b ⇒ 'a ⇒ 'b ⇒ bool ⇒ bool"
  where "Inr_Rep b x y p ⟷ y = b ∧ ¬ p"

definition "sum = {f. (∃a. f = Inl_Rep (a::'a)) ∨ (∃b. f = Inr_Rep (b::'b))}"

typedef ('a, 'b) sum (infixr "+" 10) = "sum :: ('a ⇒ 'b ⇒ bool ⇒ bool) set"
  unfolding sum_def by auto

lemma Inl_RepI: "Inl_Rep a ∈ sum"
  by (auto simp add: sum_def)

lemma Inr_RepI: "Inr_Rep b ∈ sum"
  by (auto simp add: sum_def)

lemma inj_on_Abs_sum: "A ⊆ sum ⟹ inj_on Abs_sum A"
  by (rule inj_on_inverseI, rule Abs_sum_inverse) auto

lemma Inl_Rep_inject: "inj_on Inl_Rep A"
proof (rule inj_onI)
  show "⋀a c. Inl_Rep a = Inl_Rep c ⟹ a = c"
    by (auto simp add: Inl_Rep_def fun_eq_iff)
qed

lemma Inr_Rep_inject: "inj_on Inr_Rep A"
proof (rule inj_onI)
  show "⋀b d. Inr_Rep b = Inr_Rep d ⟹ b = d"
    by (auto simp add: Inr_Rep_def fun_eq_iff)
qed

lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a ≠ Inr_Rep b"
  by (auto simp add: Inl_Rep_def Inr_Rep_def fun_eq_iff)

definition Inl :: "'a ⇒ 'a + 'b"
  where "Inl = Abs_sum ∘ Inl_Rep"

definition Inr :: "'b ⇒ 'a + 'b"
  where "Inr = Abs_sum ∘ Inr_Rep"

lemma inj_Inl [simp]: "inj_on Inl A"
  by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_sum Inl_RepI)

lemma Inl_inject: "Inl x = Inl y ⟹ x = y"
  using inj_Inl by (rule injD)

lemma inj_Inr [simp]: "inj_on Inr A"
  by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_sum Inr_RepI)

lemma Inr_inject: "Inr x = Inr y ⟹ x = y"
  using inj_Inr by (rule injD)

lemma Inl_not_Inr: "Inl a ≠ Inr b"
proof -
  have "{Inl_Rep a, Inr_Rep b} ⊆ sum"
    using Inl_RepI [of a] Inr_RepI [of b] by auto
  with inj_on_Abs_sum have "inj_on Abs_sum {Inl_Rep a, Inr_Rep b}" .
  with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_sum (Inl_Rep a) ≠ Abs_sum (Inr_Rep b)"
    by auto
  then show ?thesis
    by (simp add: Inl_def Inr_def)
qed

lemma Inr_not_Inl: "Inr b ≠ Inl a"
  using Inl_not_Inr by (rule not_sym)

lemma sumE:
  assumes "⋀x::'a. s = Inl x ⟹ P"
    and "⋀y::'b. s = Inr y ⟹ P"
  shows P
proof (rule Abs_sum_cases [of s])
  fix f
  assume "s = Abs_sum f" and "f ∈ sum"
  with assms show P
    by (auto simp add: sum_def Inl_def Inr_def)
qed

free_constructors case_sum for
  isl: Inl projl
| Inr projr
  by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)

text ‹Avoid name clashes by prefixing the output of ‹old_rep_datatype› with ‹old›.›

setup ‹Sign.mandatory_path "old"›

old_rep_datatype Inl Inr
proof -
  fix P
  fix s :: "'a + 'b"
  assume x: "⋀x::'a. P (Inl x)" and y: "⋀y::'b. P (Inr y)"
  then show "P s" by (auto intro: sumE [of s])
qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)

setup ‹Sign.parent_path›

text ‹But erase the prefix for properties that are not generated by ‹free_constructors›.›

setup ‹Sign.mandatory_path "sum"›

declare
  old.sum.inject[iff del]
  old.sum.distinct(1)[simp del, induct_simp del]

lemmas induct = old.sum.induct
lemmas inducts = old.sum.inducts
lemmas rec = old.sum.rec
lemmas simps = sum.inject sum.distinct sum.case sum.rec

setup ‹Sign.parent_path›

primrec map_sum :: "('a ⇒ 'c) ⇒ ('b ⇒ 'd) ⇒ 'a + 'b ⇒ 'c + 'd"
  where
    "map_sum f1 f2 (Inl a) = Inl (f1 a)"
  | "map_sum f1 f2 (Inr a) = Inr (f2 a)"

functor map_sum: map_sum
proof -
  show "map_sum f g ∘ map_sum h i = map_sum (f ∘ h) (g ∘ i)" for f g h i
  proof
    show "(map_sum f g ∘ map_sum h i) s = map_sum (f ∘ h) (g ∘ i) s" for s
      by (cases s) simp_all
  qed
  show "map_sum id id = id"
  proof
    show "map_sum id id s = id s" for s
      by (cases s) simp_all
  qed
qed

lemma split_sum_all: "(∀x. P x) ⟷ (∀x. P (Inl x)) ∧ (∀x. P (Inr x))"
  by (auto intro: sum.induct)

lemma split_sum_ex: "(∃x. P x) ⟷ (∃x. P (Inl x)) ∨ (∃x. P (Inr x))"
  using split_sum_all[of "λx. ¬P x"] by blast


subsection ‹Projections›

lemma case_sum_KK [simp]: "case_sum (λx. a) (λx. a) = (λx. a)"
  by (rule ext) (simp split: sum.split)

lemma surjective_sum: "case_sum (λx::'a. f (Inl x)) (λy::'b. f (Inr y)) = f"
proof
  fix s :: "'a + 'b"
  show "(case s of Inl (x::'a) ⇒ f (Inl x) | Inr (y::'b) ⇒ f (Inr y)) = f s"
    by (cases s) simp_all
qed

lemma case_sum_inject:
  assumes a: "case_sum f1 f2 = case_sum g1 g2"
    and r: "f1 = g1 ⟹ f2 = g2 ⟹ P"
  shows P
proof (rule r)
  show "f1 = g1"
  proof
    fix x :: 'a
    from a have "case_sum f1 f2 (Inl x) = case_sum g1 g2 (Inl x)" by simp
    then show "f1 x = g1 x" by simp
  qed
  show "f2 = g2"
  proof
    fix y :: 'b
    from a have "case_sum f1 f2 (Inr y) = case_sum g1 g2 (Inr y)" by simp
    then show "f2 y = g2 y" by simp
  qed
qed

primrec Suml :: "('a ⇒ 'c) ⇒ 'a + 'b ⇒ 'c"
  where "Suml f (Inl x) = f x"

primrec Sumr :: "('b ⇒ 'c) ⇒ 'a + 'b ⇒ 'c"
  where "Sumr f (Inr x) = f x"

lemma Suml_inject:
  assumes "Suml f = Suml g"
  shows "f = g"
proof
  fix x :: 'a
  let ?s = "Inl x :: 'a + 'b"
  from assms have "Suml f ?s = Suml g ?s" by simp
  then show "f x = g x" by simp
qed

lemma Sumr_inject:
  assumes "Sumr f = Sumr g"
  shows "f = g"
proof
  fix x :: 'b
  let ?s = "Inr x :: 'a + 'b"
  from assms have "Sumr f ?s = Sumr g ?s" by simp
  then show "f x = g x" by simp
qed


subsection ‹The Disjoint Sum of Sets›

definition Plus :: "'a set ⇒ 'b set ⇒ ('a + 'b) set"  (infixr "<+>" 65)
  where "A <+> B = Inl ` A ∪ Inr ` B"

hide_const (open) Plus ― ‹Valuable identifier›

lemma InlI [intro!]: "a ∈ A ⟹ Inl a ∈ A <+> B"
  by (simp add: Plus_def)

lemma InrI [intro!]: "b ∈ B ⟹ Inr b ∈ A <+> B"
  by (simp add: Plus_def)

text ‹Exhaustion rule for sums, a degenerate form of induction›

lemma PlusE [elim!]:
  "u ∈ A <+> B ⟹ (⋀x. x ∈ A ⟹ u = Inl x ⟹ P) ⟹ (⋀y. y ∈ B ⟹ u = Inr y ⟹ P) ⟹ P"
  by (auto simp add: Plus_def)

lemma Plus_eq_empty_conv [simp]: "A <+> B = {} ⟷ A = {} ∧ B = {}"
  by auto

lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV"
proof (rule set_eqI)
  fix u :: "'a + 'b"
  show "u ∈ UNIV <+> UNIV ⟷ u ∈ UNIV" by (cases u) auto
qed

lemma UNIV_sum: "UNIV = Inl ` UNIV ∪ Inr ` UNIV"
proof -
  have "x ∈ range Inl" if "x ∉ range Inr" for x :: "'a + 'b"
    using that by (cases x) simp_all
  then show ?thesis by auto
qed

hide_const (open) Suml Sumr sum

end