src/HOL/Sum_Type.thy
 author wenzelm Mon Mar 22 20:58:52 2010 +0100 (2010-03-22) changeset 35898 c890a3835d15 parent 33995 ebf231de0c5c child 36176 3fe7e97ccca8 permissions -rw-r--r--
 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` paulson@15391 ` 6` ```header{*The Disjoint Sum of Two Types*} ``` nipkow@10213 ` 7` paulson@15391 ` 8` ```theory Sum_Type ``` haftmann@33961 ` 9` ```imports Typedef Inductive Fun ``` paulson@15391 ` 10` ```begin ``` paulson@15391 ` 11` haftmann@33962 ` 12` ```subsection {* Construction of the sum type and its basic abstract operations *} ``` nipkow@10213 ` 13` haftmann@33962 ` 14` ```definition Inl_Rep :: "'a \ 'a \ 'b \ bool \ bool" where ``` haftmann@33962 ` 15` ``` "Inl_Rep a x y p \ x = a \ p" ``` nipkow@10213 ` 16` haftmann@33962 ` 17` ```definition Inr_Rep :: "'b \ 'a \ 'b \ bool \ bool" where ``` haftmann@33962 ` 18` ``` "Inr_Rep b x y p \ y = b \ \ p" ``` paulson@15391 ` 19` nipkow@10213 ` 20` ```global ``` nipkow@10213 ` 21` haftmann@33962 ` 22` ```typedef (Sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\a. f = Inl_Rep (a::'a)) \ (\b. f = Inr_Rep (b::'b))}" ``` paulson@15391 ` 23` ``` by auto ``` nipkow@10213 ` 24` nipkow@10213 ` 25` ```local ``` nipkow@10213 ` 26` haftmann@33962 ` 27` ```lemma Inl_RepI: "Inl_Rep a \ Sum" ``` haftmann@33962 ` 28` ``` by (auto simp add: Sum_def) ``` paulson@15391 ` 29` haftmann@33962 ` 30` ```lemma Inr_RepI: "Inr_Rep b \ Sum" ``` haftmann@33962 ` 31` ``` by (auto simp add: Sum_def) ``` paulson@15391 ` 32` haftmann@33962 ` 33` ```lemma inj_on_Abs_Sum: "A \ Sum \ inj_on Abs_Sum A" ``` haftmann@33962 ` 34` ``` by (rule inj_on_inverseI, rule Abs_Sum_inverse) auto ``` paulson@15391 ` 35` haftmann@33962 ` 36` ```lemma Inl_Rep_inject: "inj_on Inl_Rep A" ``` haftmann@33962 ` 37` ```proof (rule inj_onI) ``` haftmann@33962 ` 38` ``` show "\a c. Inl_Rep a = Inl_Rep c \ a = c" ``` haftmann@33962 ` 39` ``` by (auto simp add: Inl_Rep_def expand_fun_eq) ``` haftmann@33962 ` 40` ```qed ``` paulson@15391 ` 41` haftmann@33962 ` 42` ```lemma Inr_Rep_inject: "inj_on Inr_Rep A" ``` haftmann@33962 ` 43` ```proof (rule inj_onI) ``` haftmann@33962 ` 44` ``` show "\b d. Inr_Rep b = Inr_Rep d \ b = d" ``` haftmann@33962 ` 45` ``` by (auto simp add: Inr_Rep_def expand_fun_eq) ``` haftmann@33962 ` 46` ```qed ``` paulson@15391 ` 47` haftmann@33962 ` 48` ```lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a \ Inr_Rep b" ``` haftmann@33962 ` 49` ``` by (auto simp add: Inl_Rep_def Inr_Rep_def expand_fun_eq) ``` paulson@15391 ` 50` haftmann@33962 ` 51` ```definition Inl :: "'a \ 'a + 'b" where ``` haftmann@33995 ` 52` ``` "Inl = Abs_Sum \ Inl_Rep" ``` paulson@15391 ` 53` haftmann@33962 ` 54` ```definition Inr :: "'b \ 'a + 'b" where ``` haftmann@33995 ` 55` ``` "Inr = Abs_Sum \ Inr_Rep" ``` paulson@15391 ` 56` huffman@29025 ` 57` ```lemma inj_Inl [simp]: "inj_on Inl A" ``` haftmann@33962 ` 58` ```by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_Sum Inl_RepI) ``` huffman@29025 ` 59` haftmann@33962 ` 60` ```lemma Inl_inject: "Inl x = Inl y \ x = y" ``` haftmann@33962 ` 61` ```using inj_Inl by (rule injD) ``` paulson@15391 ` 62` huffman@29025 ` 63` ```lemma inj_Inr [simp]: "inj_on Inr A" ``` haftmann@33962 ` 64` ```by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_Sum Inr_RepI) ``` paulson@15391 ` 65` haftmann@33962 ` 66` ```lemma Inr_inject: "Inr x = Inr y \ x = y" ``` haftmann@33962 ` 67` ```using inj_Inr by (rule injD) ``` paulson@15391 ` 68` haftmann@33962 ` 69` ```lemma Inl_not_Inr: "Inl a \ Inr b" ``` haftmann@33962 ` 70` ```proof - ``` haftmann@33962 ` 71` ``` from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \ Sum" by auto ``` haftmann@33962 ` 72` ``` with inj_on_Abs_Sum have "inj_on Abs_Sum {Inl_Rep a, Inr_Rep b}" . ``` haftmann@33962 ` 73` ``` 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 ``` haftmann@33962 ` 74` ``` then show ?thesis by (simp add: Inl_def Inr_def) ``` haftmann@33962 ` 75` ```qed ``` paulson@15391 ` 76` haftmann@33962 ` 77` ```lemma Inr_not_Inl: "Inr b \ Inl a" ``` haftmann@33962 ` 78` ``` using Inl_not_Inr by (rule not_sym) ``` paulson@15391 ` 79` paulson@15391 ` 80` ```lemma sumE: ``` haftmann@33962 ` 81` ``` assumes "\x::'a. s = Inl x \ P" ``` haftmann@33962 ` 82` ``` and "\y::'b. s = Inr y \ P" ``` haftmann@33962 ` 83` ``` shows P ``` haftmann@33962 ` 84` ```proof (rule Abs_Sum_cases [of s]) ``` haftmann@33962 ` 85` ``` fix f ``` haftmann@33962 ` 86` ``` assume "s = Abs_Sum f" and "f \ Sum" ``` haftmann@33962 ` 87` ``` with assms show P by (auto simp add: Sum_def Inl_def Inr_def) ``` haftmann@33962 ` 88` ```qed ``` haftmann@33961 ` 89` haftmann@33961 ` 90` ```rep_datatype (sum) Inl Inr ``` haftmann@33961 ` 91` ```proof - ``` haftmann@33961 ` 92` ``` fix P ``` haftmann@33961 ` 93` ``` fix s :: "'a + 'b" ``` haftmann@33961 ` 94` ``` assume x: "\x\'a. P (Inl x)" and y: "\y\'b. P (Inr y)" ``` haftmann@33961 ` 95` ``` then show "P s" by (auto intro: sumE [of s]) ``` haftmann@33962 ` 96` ```qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr) ``` haftmann@33962 ` 97` haftmann@33961 ` 98` haftmann@33962 ` 99` ```subsection {* Projections *} ``` haftmann@33962 ` 100` haftmann@33962 ` 101` ```lemma sum_case_KK [simp]: "sum_case (\x. a) (\x. a) = (\x. a)" ``` haftmann@33961 ` 102` ``` by (rule ext) (simp split: sum.split) ``` haftmann@33961 ` 103` haftmann@33962 ` 104` ```lemma surjective_sum: "sum_case (\x::'a. f (Inl x)) (\y::'b. f (Inr y)) = f" ``` haftmann@33962 ` 105` ```proof ``` haftmann@33962 ` 106` ``` fix s :: "'a + 'b" ``` haftmann@33962 ` 107` ``` show "(case s of Inl (x\'a) \ f (Inl x) | Inr (y\'b) \ f (Inr y)) = f s" ``` haftmann@33962 ` 108` ``` by (cases s) simp_all ``` haftmann@33962 ` 109` ```qed ``` haftmann@33961 ` 110` haftmann@33962 ` 111` ```lemma sum_case_inject: ``` haftmann@33962 ` 112` ``` assumes a: "sum_case f1 f2 = sum_case g1 g2" ``` haftmann@33962 ` 113` ``` assumes r: "f1 = g1 \ f2 = g2 \ P" ``` haftmann@33962 ` 114` ``` shows P ``` haftmann@33962 ` 115` ```proof (rule r) ``` haftmann@33962 ` 116` ``` show "f1 = g1" proof ``` haftmann@33962 ` 117` ``` fix x :: 'a ``` haftmann@33962 ` 118` ``` from a have "sum_case f1 f2 (Inl x) = sum_case g1 g2 (Inl x)" by simp ``` haftmann@33962 ` 119` ``` then show "f1 x = g1 x" by simp ``` haftmann@33962 ` 120` ``` qed ``` haftmann@33962 ` 121` ``` show "f2 = g2" proof ``` haftmann@33962 ` 122` ``` fix y :: 'b ``` haftmann@33962 ` 123` ``` from a have "sum_case f1 f2 (Inr y) = sum_case g1 g2 (Inr y)" by simp ``` haftmann@33962 ` 124` ``` then show "f2 y = g2 y" by simp ``` haftmann@33962 ` 125` ``` qed ``` haftmann@33962 ` 126` ```qed ``` haftmann@33962 ` 127` haftmann@33962 ` 128` ```lemma sum_case_weak_cong: ``` haftmann@33962 ` 129` ``` "s = t \ sum_case f g s = sum_case f g t" ``` haftmann@33961 ` 130` ``` -- {* Prevents simplification of @{text f} and @{text g}: much faster. *} ``` haftmann@33961 ` 131` ``` by simp ``` haftmann@33961 ` 132` haftmann@33962 ` 133` ```primrec Projl :: "'a + 'b \ 'a" where ``` haftmann@33962 ` 134` ``` Projl_Inl: "Projl (Inl x) = x" ``` haftmann@33962 ` 135` haftmann@33962 ` 136` ```primrec Projr :: "'a + 'b \ 'b" where ``` haftmann@33962 ` 137` ``` Projr_Inr: "Projr (Inr x) = x" ``` haftmann@33962 ` 138` haftmann@33962 ` 139` ```primrec Suml :: "('a \ 'c) \ 'a + 'b \ 'c" where ``` haftmann@33962 ` 140` ``` "Suml f (Inl x) = f x" ``` haftmann@33962 ` 141` haftmann@33962 ` 142` ```primrec Sumr :: "('b \ 'c) \ 'a + 'b \ 'c" where ``` haftmann@33962 ` 143` ``` "Sumr f (Inr x) = f x" ``` haftmann@33962 ` 144` haftmann@33962 ` 145` ```lemma Suml_inject: ``` haftmann@33962 ` 146` ``` assumes "Suml f = Suml g" shows "f = g" ``` haftmann@33962 ` 147` ```proof ``` haftmann@33962 ` 148` ``` fix x :: 'a ``` haftmann@33962 ` 149` ``` let ?s = "Inl x \ 'a + 'b" ``` haftmann@33962 ` 150` ``` from assms have "Suml f ?s = Suml g ?s" by simp ``` haftmann@33962 ` 151` ``` then show "f x = g x" by simp ``` haftmann@33961 ` 152` ```qed ``` haftmann@33961 ` 153` haftmann@33962 ` 154` ```lemma Sumr_inject: ``` haftmann@33962 ` 155` ``` assumes "Sumr f = Sumr g" shows "f = g" ``` haftmann@33962 ` 156` ```proof ``` haftmann@33962 ` 157` ``` fix x :: 'b ``` haftmann@33962 ` 158` ``` let ?s = "Inr x \ 'a + 'b" ``` haftmann@33962 ` 159` ``` from assms have "Sumr f ?s = Sumr g ?s" by simp ``` haftmann@33962 ` 160` ``` then show "f x = g x" by simp ``` haftmann@33962 ` 161` ```qed ``` haftmann@33961 ` 162` haftmann@33995 ` 163` haftmann@33962 ` 164` ```subsection {* The Disjoint Sum of Sets *} ``` haftmann@33961 ` 165` haftmann@33962 ` 166` ```definition Plus :: "'a set \ 'b set \ ('a + 'b) set" (infixr "<+>" 65) where ``` haftmann@33962 ` 167` ``` "A <+> B = Inl ` A \ Inr ` B" ``` haftmann@33962 ` 168` haftmann@33962 ` 169` ```lemma InlI [intro!]: "a \ A \ Inl a \ A <+> B" ``` haftmann@33962 ` 170` ```by (simp add: Plus_def) ``` haftmann@33961 ` 171` haftmann@33962 ` 172` ```lemma InrI [intro!]: "b \ B \ Inr b \ A <+> B" ``` haftmann@33962 ` 173` ```by (simp add: Plus_def) ``` haftmann@33961 ` 174` haftmann@33962 ` 175` ```text {* Exhaustion rule for sums, a degenerate form of induction *} ``` haftmann@33962 ` 176` haftmann@33962 ` 177` ```lemma PlusE [elim!]: ``` haftmann@33962 ` 178` ``` "u \ A <+> B \ (\x. x \ A \ u = Inl x \ P) \ (\y. y \ B \ u = Inr y \ P) \ P" ``` haftmann@33962 ` 179` ```by (auto simp add: Plus_def) ``` haftmann@33961 ` 180` haftmann@33962 ` 181` ```lemma Plus_eq_empty_conv [simp]: "A <+> B = {} \ A = {} \ B = {}" ``` haftmann@33962 ` 182` ```by auto ``` haftmann@33961 ` 183` haftmann@33962 ` 184` ```lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV" ``` haftmann@33962 ` 185` ```proof (rule set_ext) ``` haftmann@33962 ` 186` ``` fix u :: "'a + 'b" ``` haftmann@33962 ` 187` ``` show "u \ UNIV <+> UNIV \ u \ UNIV" by (cases u) auto ``` haftmann@33962 ` 188` ```qed ``` haftmann@33961 ` 189` haftmann@33961 ` 190` ```hide (open) const Suml Sumr Projl Projr ``` haftmann@33961 ` 191` nipkow@10213 ` 192` ```end ```