# Theory Sum_Type

Up to index of Isabelle/HOL-Proofs

theory Sum_Type
imports Typedef Inductive Fun
`(*  Title:      HOL/Sum_Type.thy    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory    Copyright   1992  University of Cambridge*)header{*The Disjoint Sum of Two Types*}theory Sum_Typeimports Typedef Inductive Funbeginsubsection {* 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 autolemma 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) autolemma 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)qedlemma 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)qedlemma 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 o Inl_Rep"definition Inr :: "'b => 'a + 'b" where  "Inr = Abs_sum o 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 -  from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} ⊆ sum" 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)qedlemma 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 Pproof (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)qedrep_datatype Inl Inrproof -  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)primrec sum_map :: "('a => 'c) => ('b => 'd) => 'a + 'b => 'c + 'd" where  "sum_map f1 f2 (Inl a) = Inl (f1 a)"| "sum_map f1 f2 (Inr a) = Inr (f2 a)"enriched_type sum_map: sum_map proof -  fix f g h i  show "sum_map f g o sum_map h i = sum_map (f o h) (g o i)"  proof    fix s    show "(sum_map f g o sum_map h i) s = sum_map (f o h) (g o i) s"      by (cases s) simp_all  qednext  fix s  show "sum_map id id = id"  proof    fix s    show "sum_map id id s = id s"       by (cases s) simp_all  qedqedsubsection {* Projections *}lemma sum_case_KK [simp]: "sum_case (λx. a) (λx. a) = (λx. a)"  by (rule ext) (simp split: sum.split)lemma surjective_sum: "sum_case (λ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_allqedlemma sum_case_inject:  assumes a: "sum_case f1 f2 = sum_case g1 g2"  assumes r: "f1 = g1 ==> f2 = g2 ==> P"  shows Pproof (rule r)  show "f1 = g1" proof    fix x :: 'a    from a have "sum_case f1 f2 (Inl x) = sum_case 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 "sum_case f1 f2 (Inr y) = sum_case g1 g2 (Inr y)" by simp    then show "f2 y = g2 y" by simp  qedqedlemma sum_case_weak_cong:  "s = t ==> sum_case f g s = sum_case f g t"  -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}  by simpprimrec Projl :: "'a + 'b => 'a" where  Projl_Inl: "Projl (Inl x) = x"primrec Projr :: "'a + 'b => 'b" where  Projr_Inr: "Projr (Inr x) = x"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 simpqedlemma 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 simpqedsubsection {* 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 autolemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV"proof (rule set_eqI)  fix u :: "'a + 'b"  show "u ∈ UNIV <+> UNIV <-> u ∈ UNIV" by (cases u) autoqedlemma UNIV_sum:  "UNIV = Inl ` UNIV ∪ Inr ` UNIV"proof -  { fix x :: "'a + 'b"    assume "x ∉ range Inr"    then have "x ∈ range Inl"    by (cases x) simp_all  } then show ?thesis by autoqedhide_const (open) Suml Sumr Projl Projrhide_const (open) sumend`