src/HOL/Sum_Type.thy
 author wenzelm Fri Dec 17 17:43:54 2010 +0100 (2010-12-17) changeset 41229 d797baa3d57c parent 40968 a6fcd305f7dc child 41372 551eb49a6e91 permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
1 (*  Title:      HOL/Sum_Type.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   1992  University of Cambridge
4 *)
6 header{*The Disjoint Sum of Two Types*}
8 theory Sum_Type
9 imports Typedef Inductive Fun
10 begin
12 subsection {* Construction of the sum type and its basic abstract operations *}
14 definition Inl_Rep :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
15   "Inl_Rep a x y p \<longleftrightarrow> x = a \<and> p"
17 definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
18   "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
20 typedef ('a, 'b) sum (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
21   by auto
23 lemma Inl_RepI: "Inl_Rep a \<in> sum"
24   by (auto simp add: sum_def)
26 lemma Inr_RepI: "Inr_Rep b \<in> sum"
27   by (auto simp add: sum_def)
29 lemma inj_on_Abs_sum: "A \<subseteq> sum \<Longrightarrow> inj_on Abs_sum A"
30   by (rule inj_on_inverseI, rule Abs_sum_inverse) auto
32 lemma Inl_Rep_inject: "inj_on Inl_Rep A"
33 proof (rule inj_onI)
34   show "\<And>a c. Inl_Rep a = Inl_Rep c \<Longrightarrow> a = c"
35     by (auto simp add: Inl_Rep_def fun_eq_iff)
36 qed
38 lemma Inr_Rep_inject: "inj_on Inr_Rep A"
39 proof (rule inj_onI)
40   show "\<And>b d. Inr_Rep b = Inr_Rep d \<Longrightarrow> b = d"
41     by (auto simp add: Inr_Rep_def fun_eq_iff)
42 qed
44 lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a \<noteq> Inr_Rep b"
45   by (auto simp add: Inl_Rep_def Inr_Rep_def fun_eq_iff)
47 definition Inl :: "'a \<Rightarrow> 'a + 'b" where
48   "Inl = Abs_sum \<circ> Inl_Rep"
50 definition Inr :: "'b \<Rightarrow> 'a + 'b" where
51   "Inr = Abs_sum \<circ> Inr_Rep"
53 lemma inj_Inl [simp]: "inj_on Inl A"
54 by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_sum Inl_RepI)
56 lemma Inl_inject: "Inl x = Inl y \<Longrightarrow> x = y"
57 using inj_Inl by (rule injD)
59 lemma inj_Inr [simp]: "inj_on Inr A"
60 by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_sum Inr_RepI)
62 lemma Inr_inject: "Inr x = Inr y \<Longrightarrow> x = y"
63 using inj_Inr by (rule injD)
65 lemma Inl_not_Inr: "Inl a \<noteq> Inr b"
66 proof -
67   from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum" by auto
68   with inj_on_Abs_sum have "inj_on Abs_sum {Inl_Rep a, Inr_Rep b}" .
69   with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_sum (Inl_Rep a) \<noteq> Abs_sum (Inr_Rep b)" by auto
70   then show ?thesis by (simp add: Inl_def Inr_def)
71 qed
73 lemma Inr_not_Inl: "Inr b \<noteq> Inl a"
74   using Inl_not_Inr by (rule not_sym)
76 lemma sumE:
77   assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P"
78     and "\<And>y::'b. s = Inr y \<Longrightarrow> P"
79   shows P
80 proof (rule Abs_sum_cases [of s])
81   fix f
82   assume "s = Abs_sum f" and "f \<in> sum"
83   with assms show P by (auto simp add: sum_def Inl_def Inr_def)
84 qed
86 rep_datatype Inl Inr
87 proof -
88   fix P
89   fix s :: "'a + 'b"
90   assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)"
91   then show "P s" by (auto intro: sumE [of s])
92 qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
94 primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
95   "sum_map f1 f2 (Inl a) = Inl (f1 a)"
96 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
98 type_lifting sum_map proof -
99   fix f g h i s
100   show "sum_map f g (sum_map h i s) = sum_map (\<lambda>x. f (h x)) (\<lambda>x. g (i x)) s"
101     by (cases s) simp_all
102 next
103   fix s
104   show "sum_map (\<lambda>x. x) (\<lambda>x. x) s = s"
105     by (cases s) simp_all
106 qed
109 subsection {* Projections *}
111 lemma sum_case_KK [simp]: "sum_case (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)"
112   by (rule ext) (simp split: sum.split)
114 lemma surjective_sum: "sum_case (\<lambda>x::'a. f (Inl x)) (\<lambda>y::'b. f (Inr y)) = f"
115 proof
116   fix s :: "'a + 'b"
117   show "(case s of Inl (x\<Colon>'a) \<Rightarrow> f (Inl x) | Inr (y\<Colon>'b) \<Rightarrow> f (Inr y)) = f s"
118     by (cases s) simp_all
119 qed
121 lemma sum_case_inject:
122   assumes a: "sum_case f1 f2 = sum_case g1 g2"
123   assumes r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P"
124   shows P
125 proof (rule r)
126   show "f1 = g1" proof
127     fix x :: 'a
128     from a have "sum_case f1 f2 (Inl x) = sum_case g1 g2 (Inl x)" by simp
129     then show "f1 x = g1 x" by simp
130   qed
131   show "f2 = g2" proof
132     fix y :: 'b
133     from a have "sum_case f1 f2 (Inr y) = sum_case g1 g2 (Inr y)" by simp
134     then show "f2 y = g2 y" by simp
135   qed
136 qed
138 lemma sum_case_weak_cong:
139   "s = t \<Longrightarrow> sum_case f g s = sum_case f g t"
140   -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
141   by simp
143 primrec Projl :: "'a + 'b \<Rightarrow> 'a" where
144   Projl_Inl: "Projl (Inl x) = x"
146 primrec Projr :: "'a + 'b \<Rightarrow> 'b" where
147   Projr_Inr: "Projr (Inr x) = x"
149 primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
150   "Suml f (Inl x) = f x"
152 primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
153   "Sumr f (Inr x) = f x"
155 lemma Suml_inject:
156   assumes "Suml f = Suml g" shows "f = g"
157 proof
158   fix x :: 'a
159   let ?s = "Inl x \<Colon> 'a + 'b"
160   from assms have "Suml f ?s = Suml g ?s" by simp
161   then show "f x = g x" by simp
162 qed
164 lemma Sumr_inject:
165   assumes "Sumr f = Sumr g" shows "f = g"
166 proof
167   fix x :: 'b
168   let ?s = "Inr x \<Colon> 'a + 'b"
169   from assms have "Sumr f ?s = Sumr g ?s" by simp
170   then show "f x = g x" by simp
171 qed
174 subsection {* The Disjoint Sum of Sets *}
176 definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) where
177   "A <+> B = Inl ` A \<union> Inr ` B"
179 hide_const (open) Plus --"Valuable identifier"
181 lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B"
184 lemma InrI [intro!]: "b \<in> B \<Longrightarrow> Inr b \<in> A <+> B"