author  haftmann 
Fri, 04 Dec 2009 18:52:55 +0100  
changeset 33995  ebf231de0c5c 
parent 33962  abf9fa17452a 
child 36176  3fe7e97ccca8 
permissions  rwrr 
10213  1 
(* Title: HOL/Sum_Type.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
Copyright 1992 University of Cambridge 

4 
*) 

5 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

6 
header{*The Disjoint Sum of Two Types*} 
10213  7 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

8 
theory Sum_Type 
33961  9 
imports Typedef Inductive Fun 
15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

10 
begin 
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

11 

33962  12 
subsection {* Construction of the sum type and its basic abstract operations *} 
10213  13 

33962  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" 

10213  16 

33962  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" 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

19 

10213  20 
global 
21 

33962  22 
typedef (Sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}" 
15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

23 
by auto 
10213  24 

25 
local 

26 

33962  27 
lemma Inl_RepI: "Inl_Rep a \<in> Sum" 
28 
by (auto simp add: Sum_def) 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

29 

33962  30 
lemma Inr_RepI: "Inr_Rep b \<in> Sum" 
31 
by (auto simp add: Sum_def) 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

32 

33962  33 
lemma inj_on_Abs_Sum: "A \<subseteq> Sum \<Longrightarrow> inj_on Abs_Sum A" 
34 
by (rule inj_on_inverseI, rule Abs_Sum_inverse) auto 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

35 

33962  36 
lemma Inl_Rep_inject: "inj_on Inl_Rep A" 
37 
proof (rule inj_onI) 

38 
show "\<And>a c. Inl_Rep a = Inl_Rep c \<Longrightarrow> a = c" 

39 
by (auto simp add: Inl_Rep_def expand_fun_eq) 

40 
qed 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

41 

33962  42 
lemma Inr_Rep_inject: "inj_on Inr_Rep A" 
43 
proof (rule inj_onI) 

44 
show "\<And>b d. Inr_Rep b = Inr_Rep d \<Longrightarrow> b = d" 

45 
by (auto simp add: Inr_Rep_def expand_fun_eq) 

46 
qed 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

47 

33962  48 
lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a \<noteq> Inr_Rep b" 
49 
by (auto simp add: Inl_Rep_def Inr_Rep_def expand_fun_eq) 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

50 

33962  51 
definition Inl :: "'a \<Rightarrow> 'a + 'b" where 
33995  52 
"Inl = Abs_Sum \<circ> Inl_Rep" 
15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

53 

33962  54 
definition Inr :: "'b \<Rightarrow> 'a + 'b" where 
33995  55 
"Inr = Abs_Sum \<circ> Inr_Rep" 
15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

56 

29025
8c8859c0d734
move lemmas from Numeral_Type.thy to other theories
huffman
parents:
28524
diff
changeset

57 
lemma inj_Inl [simp]: "inj_on Inl A" 
33962  58 
by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_Sum Inl_RepI) 
29025
8c8859c0d734
move lemmas from Numeral_Type.thy to other theories
huffman
parents:
28524
diff
changeset

59 

33962  60 
lemma Inl_inject: "Inl x = Inl y \<Longrightarrow> x = y" 
61 
using inj_Inl by (rule injD) 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

62 

29025
8c8859c0d734
move lemmas from Numeral_Type.thy to other theories
huffman
parents:
28524
diff
changeset

63 
lemma inj_Inr [simp]: "inj_on Inr A" 
33962  64 
by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_Sum Inr_RepI) 
15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

65 

33962  66 
lemma Inr_inject: "Inr x = Inr y \<Longrightarrow> x = y" 
67 
using inj_Inr by (rule injD) 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

68 

33962  69 
lemma Inl_not_Inr: "Inl a \<noteq> Inr b" 
70 
proof  

71 
from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> Sum" by auto 

72 
with inj_on_Abs_Sum have "inj_on Abs_Sum {Inl_Rep a, Inr_Rep b}" . 

73 
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 

74 
then show ?thesis by (simp add: Inl_def Inr_def) 

75 
qed 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

76 

33962  77 
lemma Inr_not_Inl: "Inr b \<noteq> Inl a" 
78 
using Inl_not_Inr by (rule not_sym) 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

79 

797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

80 
lemma sumE: 
33962  81 
assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P" 
82 
and "\<And>y::'b. s = Inr y \<Longrightarrow> P" 

83 
shows P 

84 
proof (rule Abs_Sum_cases [of s]) 

85 
fix f 

86 
assume "s = Abs_Sum f" and "f \<in> Sum" 

87 
with assms show P by (auto simp add: Sum_def Inl_def Inr_def) 

88 
qed 

33961  89 

90 
rep_datatype (sum) Inl Inr 

91 
proof  

92 
fix P 

93 
fix s :: "'a + 'b" 

94 
assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)" 

95 
then show "P s" by (auto intro: sumE [of s]) 

33962  96 
qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr) 
97 

33961  98 

33962  99 
subsection {* Projections *} 
100 

101 
lemma sum_case_KK [simp]: "sum_case (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)" 

33961  102 
by (rule ext) (simp split: sum.split) 
103 

33962  104 
lemma surjective_sum: "sum_case (\<lambda>x::'a. f (Inl x)) (\<lambda>y::'b. f (Inr y)) = f" 
105 
proof 

106 
fix s :: "'a + 'b" 

107 
show "(case s of Inl (x\<Colon>'a) \<Rightarrow> f (Inl x)  Inr (y\<Colon>'b) \<Rightarrow> f (Inr y)) = f s" 

108 
by (cases s) simp_all 

109 
qed 

33961  110 

33962  111 
lemma sum_case_inject: 
112 
assumes a: "sum_case f1 f2 = sum_case g1 g2" 

113 
assumes r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P" 

114 
shows P 

115 
proof (rule r) 

116 
show "f1 = g1" proof 

117 
fix x :: 'a 

118 
from a have "sum_case f1 f2 (Inl x) = sum_case g1 g2 (Inl x)" by simp 

119 
then show "f1 x = g1 x" by simp 

120 
qed 

121 
show "f2 = g2" proof 

122 
fix y :: 'b 

123 
from a have "sum_case f1 f2 (Inr y) = sum_case g1 g2 (Inr y)" by simp 

124 
then show "f2 y = g2 y" by simp 

125 
qed 

126 
qed 

127 

128 
lemma sum_case_weak_cong: 

129 
"s = t \<Longrightarrow> sum_case f g s = sum_case f g t" 

33961  130 
 {* Prevents simplification of @{text f} and @{text g}: much faster. *} 
131 
by simp 

132 

33962  133 
primrec Projl :: "'a + 'b \<Rightarrow> 'a" where 
134 
Projl_Inl: "Projl (Inl x) = x" 

135 

136 
primrec Projr :: "'a + 'b \<Rightarrow> 'b" where 

137 
Projr_Inr: "Projr (Inr x) = x" 

138 

139 
primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where 

140 
"Suml f (Inl x) = f x" 

141 

142 
primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where 

143 
"Sumr f (Inr x) = f x" 

144 

145 
lemma Suml_inject: 

146 
assumes "Suml f = Suml g" shows "f = g" 

147 
proof 

148 
fix x :: 'a 

149 
let ?s = "Inl x \<Colon> 'a + 'b" 

150 
from assms have "Suml f ?s = Suml g ?s" by simp 

151 
then show "f x = g x" by simp 

33961  152 
qed 
153 

33962  154 
lemma Sumr_inject: 
155 
assumes "Sumr f = Sumr g" shows "f = g" 

156 
proof 

157 
fix x :: 'b 

158 
let ?s = "Inr x \<Colon> 'a + 'b" 

159 
from assms have "Sumr f ?s = Sumr g ?s" by simp 

160 
then show "f x = g x" by simp 

161 
qed 

33961  162 

33995  163 

33962  164 
subsection {* The Disjoint Sum of Sets *} 
33961  165 

33962  166 
definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) where 
167 
"A <+> B = Inl ` A \<union> Inr ` B" 

168 

169 
lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B" 

170 
by (simp add: Plus_def) 

33961  171 

33962  172 
lemma InrI [intro!]: "b \<in> B \<Longrightarrow> Inr b \<in> A <+> B" 
173 
by (simp add: Plus_def) 

33961  174 

33962  175 
text {* Exhaustion rule for sums, a degenerate form of induction *} 
176 

177 
lemma PlusE [elim!]: 

178 
"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" 

179 
by (auto simp add: Plus_def) 

33961  180 

33962  181 
lemma Plus_eq_empty_conv [simp]: "A <+> B = {} \<longleftrightarrow> A = {} \<and> B = {}" 
182 
by auto 

33961  183 

33962  184 
lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV" 
185 
proof (rule set_ext) 

186 
fix u :: "'a + 'b" 

187 
show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto 

188 
qed 

33961  189 

190 
hide (open) const Suml Sumr Projl Projr 

191 

10213  192 
end 