1(* Title: HOL/Sum_Type.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1992 University of Cambridge 4*) 5 6section \<open>The Disjoint Sum of Two Types\<close> 7 8theory Sum_Type 9 imports Typedef Inductive Fun 10begin 11 12subsection \<open>Construction of the sum type and its basic abstract operations\<close> 13 14definition Inl_Rep :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" 15 where "Inl_Rep a x y p \<longleftrightarrow> x = a \<and> p" 16 17definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" 18 where "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p" 19 20definition "sum = {f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}" 21 22typedef ('a, 'b) sum (infixr "+" 10) = "sum :: ('a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool) set" 23 unfolding sum_def by auto 24 25lemma Inl_RepI: "Inl_Rep a \<in> sum" 26 by (auto simp add: sum_def) 27 28lemma Inr_RepI: "Inr_Rep b \<in> sum" 29 by (auto simp add: sum_def) 30 31lemma inj_on_Abs_sum: "A \<subseteq> sum \<Longrightarrow> inj_on Abs_sum A" 32 by (rule inj_on_inverseI, rule Abs_sum_inverse) auto 33 34lemma Inl_Rep_inject: "inj_on Inl_Rep A" 35proof (rule inj_onI) 36 show "\<And>a c. Inl_Rep a = Inl_Rep c \<Longrightarrow> a = c" 37 by (auto simp add: Inl_Rep_def fun_eq_iff) 38qed 39 40lemma Inr_Rep_inject: "inj_on Inr_Rep A" 41proof (rule inj_onI) 42 show "\<And>b d. Inr_Rep b = Inr_Rep d \<Longrightarrow> b = d" 43 by (auto simp add: Inr_Rep_def fun_eq_iff) 44qed 45 46lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a \<noteq> Inr_Rep b" 47 by (auto simp add: Inl_Rep_def Inr_Rep_def fun_eq_iff) 48 49definition Inl :: "'a \<Rightarrow> 'a + 'b" 50 where "Inl = Abs_sum \<circ> Inl_Rep" 51 52definition Inr :: "'b \<Rightarrow> 'a + 'b" 53 where "Inr = Abs_sum \<circ> Inr_Rep" 54 55lemma inj_Inl [simp]: "inj_on Inl A" 56 by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_sum Inl_RepI) 57 58lemma Inl_inject: "Inl x = Inl y \<Longrightarrow> x = y" 59 using inj_Inl by (rule injD) 60 61lemma inj_Inr [simp]: "inj_on Inr A" 62 by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_sum Inr_RepI) 63 64lemma Inr_inject: "Inr x = Inr y \<Longrightarrow> x = y" 65 using inj_Inr by (rule injD) 66 67lemma Inl_not_Inr: "Inl a \<noteq> Inr b" 68proof - 69 have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum" 70 using Inl_RepI [of a] Inr_RepI [of b] by auto 71 with inj_on_Abs_sum have "inj_on Abs_sum {Inl_Rep a, Inr_Rep b}" . 72 with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_sum (Inl_Rep a) \<noteq> Abs_sum (Inr_Rep b)" 73 by auto 74 then show ?thesis 75 by (simp add: Inl_def Inr_def) 76qed 77 78lemma Inr_not_Inl: "Inr b \<noteq> Inl a" 79 using Inl_not_Inr by (rule not_sym) 80 81lemma sumE: 82 assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P" 83 and "\<And>y::'b. s = Inr y \<Longrightarrow> P" 84 shows P 85proof (rule Abs_sum_cases [of s]) 86 fix f 87 assume "s = Abs_sum f" and "f \<in> sum" 88 with assms show P 89 by (auto simp add: sum_def Inl_def Inr_def) 90qed 91 92free_constructors case_sum for 93 isl: Inl projl 94| Inr projr 95 by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr) 96 97text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close> 98 99setup \<open>Sign.mandatory_path "old"\<close> 100 101old_rep_datatype Inl Inr 102proof - 103 fix P 104 fix s :: "'a + 'b" 105 assume x: "\<And>x::'a. P (Inl x)" and y: "\<And>y::'b. P (Inr y)" 106 then show "P s" by (auto intro: sumE [of s]) 107qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr) 108 109setup \<open>Sign.parent_path\<close> 110 111text \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close> 112 113setup \<open>Sign.mandatory_path "sum"\<close> 114 115declare 116 old.sum.inject[iff del] 117 old.sum.distinct(1)[simp del, induct_simp del] 118 119lemmas induct = old.sum.induct 120lemmas inducts = old.sum.inducts 121lemmas rec = old.sum.rec 122lemmas simps = sum.inject sum.distinct sum.case sum.rec 123 124setup \<open>Sign.parent_path\<close> 125 126primrec map_sum :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" 127 where 128 "map_sum f1 f2 (Inl a) = Inl (f1 a)" 129 | "map_sum f1 f2 (Inr a) = Inr (f2 a)" 130 131functor map_sum: map_sum 132proof - 133 show "map_sum f g \<circ> map_sum h i = map_sum (f \<circ> h) (g \<circ> i)" for f g h i 134 proof 135 show "(map_sum f g \<circ> map_sum h i) s = map_sum (f \<circ> h) (g \<circ> i) s" for s 136 by (cases s) simp_all 137 qed 138 show "map_sum id id = id" 139 proof 140 show "map_sum id id s = id s" for s 141 by (cases s) simp_all 142 qed 143qed 144 145lemma split_sum_all: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))" 146 by (auto intro: sum.induct) 147 148lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))" 149 using split_sum_all[of "\<lambda>x. \<not>P x"] by blast 150 151 152subsection \<open>Projections\<close> 153 154lemma case_sum_KK [simp]: "case_sum (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)" 155 by (rule ext) (simp split: sum.split) 156 157lemma surjective_sum: "case_sum (\<lambda>x::'a. f (Inl x)) (\<lambda>y::'b. f (Inr y)) = f" 158proof 159 fix s :: "'a + 'b" 160 show "(case s of Inl (x::'a) \<Rightarrow> f (Inl x) | Inr (y::'b) \<Rightarrow> f (Inr y)) = f s" 161 by (cases s) simp_all 162qed 163 164lemma case_sum_inject: 165 assumes a: "case_sum f1 f2 = case_sum g1 g2" 166 and r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P" 167 shows P 168proof (rule r) 169 show "f1 = g1" 170 proof 171 fix x :: 'a 172 from a have "case_sum f1 f2 (Inl x) = case_sum g1 g2 (Inl x)" by simp 173 then show "f1 x = g1 x" by simp 174 qed 175 show "f2 = g2" 176 proof 177 fix y :: 'b 178 from a have "case_sum f1 f2 (Inr y) = case_sum g1 g2 (Inr y)" by simp 179 then show "f2 y = g2 y" by simp 180 qed 181qed 182 183primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" 184 where "Suml f (Inl x) = f x" 185 186primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" 187 where "Sumr f (Inr x) = f x" 188 189lemma Suml_inject: 190 assumes "Suml f = Suml g" 191 shows "f = g" 192proof 193 fix x :: 'a 194 let ?s = "Inl x :: 'a + 'b" 195 from assms have "Suml f ?s = Suml g ?s" by simp 196 then show "f x = g x" by simp 197qed 198 199lemma Sumr_inject: 200 assumes "Sumr f = Sumr g" 201 shows "f = g" 202proof 203 fix x :: 'b 204 let ?s = "Inr x :: 'a + 'b" 205 from assms have "Sumr f ?s = Sumr g ?s" by simp 206 then show "f x = g x" by simp 207qed 208 209 210subsection \<open>The Disjoint Sum of Sets\<close> 211 212definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) 213 where "A <+> B = Inl ` A \<union> Inr ` B" 214 215hide_const (open) Plus \<comment> \<open>Valuable identifier\<close> 216 217lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B" 218 by (simp add: Plus_def) 219 220lemma InrI [intro!]: "b \<in> B \<Longrightarrow> Inr b \<in> A <+> B" 221 by (simp add: Plus_def) 222 223text \<open>Exhaustion rule for sums, a degenerate form of induction\<close> 224 225lemma PlusE [elim!]: 226 "u \<in> A <+> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> u = Inl x \<Longrightarrow> P) \<Longrightarrow> (\<And>y. y \<in> B \<Longrightarrow> u = Inr y \<Longrightarrow> P) \<Longrightarrow> P" 227 by (auto simp add: Plus_def) 228 229lemma Plus_eq_empty_conv [simp]: "A <+> B = {} \<longleftrightarrow> A = {} \<and> B = {}" 230 by auto 231 232lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV" 233proof (rule set_eqI) 234 fix u :: "'a + 'b" 235 show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto 236qed 237 238lemma UNIV_sum: "UNIV = Inl ` UNIV \<union> Inr ` UNIV" 239proof - 240 have "x \<in> range Inl" if "x \<notin> range Inr" for x :: "'a + 'b" 241 using that by (cases x) simp_all 242 then show ?thesis by auto 243qed 244 245hide_const (open) Suml Sumr sum 246 247end 248