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