author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46953  2b6e55924af3 
child 58860  fee7cfa69c50 
permissions  rwrr 
41777  1 
(* Title: ZF/Sum.thy 
1478  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  3 
Copyright 1993 University of Cambridge 
4 
*) 

5 

13356  6 
header{*Disjoint Sums*} 
7 

16417  8 
theory Sum imports Bool equalities begin 
3923  9 

13356  10 
text{*And the "Part" primitive for simultaneous recursive type definitions*} 
11 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

12 
definition sum :: "[i,i]=>i" (infixr "+" 65) where 
46820  13 
"A+B == {0}*A \<union> {1}*B" 
13240  14 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

15 
definition Inl :: "i=>i" where 
13240  16 
"Inl(a) == <0,a>" 
17 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

18 
definition Inr :: "i=>i" where 
13240  19 
"Inr(b) == <1,b>" 
20 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

21 
definition "case" :: "[i=>i, i=>i, i]=>i" where 
13240  22 
"case(c,d) == (%<y,z>. cond(y, d(z), c(z)))" 
23 

24 
(*operator for selecting out the various summands*) 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

25 
definition Part :: "[i,i=>i] => i" where 
46953  26 
"Part(A,h) == {x \<in> A. \<exists>z. x = h(z)}" 
0  27 

13356  28 
subsection{*Rules for the @{term Part} Primitive*} 
13240  29 

46953  30 
lemma Part_iff: 
31 
"a \<in> Part(A,h) \<longleftrightarrow> a \<in> A & (\<exists>y. a=h(y))" 

13240  32 
apply (unfold Part_def) 
33 
apply (rule separation) 

34 
done 

35 

46953  36 
lemma Part_eqI [intro]: 
46820  37 
"[ a \<in> A; a=h(b) ] ==> a \<in> Part(A,h)" 
13255  38 
by (unfold Part_def, blast) 
13240  39 

40 
lemmas PartI = refl [THEN [2] Part_eqI] 

41 

46953  42 
lemma PartE [elim!]: 
43 
"[ a \<in> Part(A,h); !!z. [ a \<in> A; a=h(z) ] ==> P 

13240  44 
] ==> P" 
13255  45 
apply (unfold Part_def, blast) 
13240  46 
done 
47 

46820  48 
lemma Part_subset: "Part(A,h) \<subseteq> A" 
13240  49 
apply (unfold Part_def) 
50 
apply (rule Collect_subset) 

51 
done 

52 

53 

13356  54 
subsection{*Rules for Disjoint Sums*} 
13240  55 

56 
lemmas sum_defs = sum_def Inl_def Inr_def case_def 

57 

58 
lemma Sigma_bool: "Sigma(bool,C) = C(0) + C(1)" 

13255  59 
by (unfold bool_def sum_def, blast) 
13240  60 

61 
(** Introduction rules for the injections **) 

62 

46820  63 
lemma InlI [intro!,simp,TC]: "a \<in> A ==> Inl(a) \<in> A+B" 
13255  64 
by (unfold sum_defs, blast) 
13240  65 

46820  66 
lemma InrI [intro!,simp,TC]: "b \<in> B ==> Inr(b) \<in> A+B" 
13255  67 
by (unfold sum_defs, blast) 
13240  68 

69 
(** Elimination rules **) 

70 

71 
lemma sumE [elim!]: 

46953  72 
"[ u \<in> A+B; 
73 
!!x. [ x \<in> A; u=Inl(x) ] ==> P; 

74 
!!y. [ y \<in> B; u=Inr(y) ] ==> P 

13240  75 
] ==> P" 
46953  76 
by (unfold sum_defs, blast) 
13240  77 

78 
(** Injection and freeness equivalences, for rewriting **) 

79 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

80 
lemma Inl_iff [iff]: "Inl(a)=Inl(b) \<longleftrightarrow> a=b" 
13255  81 
by (simp add: sum_defs) 
13240  82 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

83 
lemma Inr_iff [iff]: "Inr(a)=Inr(b) \<longleftrightarrow> a=b" 
13255  84 
by (simp add: sum_defs) 
13240  85 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

86 
lemma Inl_Inr_iff [simp]: "Inl(a)=Inr(b) \<longleftrightarrow> False" 
13255  87 
by (simp add: sum_defs) 
13240  88 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

89 
lemma Inr_Inl_iff [simp]: "Inr(b)=Inl(a) \<longleftrightarrow> False" 
13255  90 
by (simp add: sum_defs) 
13240  91 

92 
lemma sum_empty [simp]: "0+0 = 0" 

13255  93 
by (simp add: sum_defs) 
13240  94 

95 
(*Injection and freeness rules*) 

96 

45602  97 
lemmas Inl_inject = Inl_iff [THEN iffD1] 
98 
lemmas Inr_inject = Inr_iff [THEN iffD1] 

13823  99 
lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE, elim!] 
100 
lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE, elim!] 

13240  101 

102 

46953  103 
lemma InlD: "Inl(a): A+B ==> a \<in> A" 
13255  104 
by blast 
13240  105 

46953  106 
lemma InrD: "Inr(b): A+B ==> b \<in> B" 
13255  107 
by blast 
13240  108 

46953  109 
lemma sum_iff: "u \<in> A+B \<longleftrightarrow> (\<exists>x. x \<in> A & u=Inl(x))  (\<exists>y. y \<in> B & u=Inr(y))" 
13255  110 
by blast 
111 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

112 
lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) \<longleftrightarrow> (x \<in> A)"; 
13255  113 
by auto 
114 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

115 
lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) \<longleftrightarrow> (y \<in> B)"; 
13255  116 
by auto 
13240  117 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

118 
lemma sum_subset_iff: "A+B \<subseteq> C+D \<longleftrightarrow> A<=C & B<=D" 
13255  119 
by blast 
13240  120 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

121 
lemma sum_equal_iff: "A+B = C+D \<longleftrightarrow> A=C & B=D" 
13255  122 
by (simp add: extension sum_subset_iff, blast) 
13240  123 

124 
lemma sum_eq_2_times: "A+A = 2*A" 

13255  125 
by (simp add: sum_def, blast) 
13240  126 

127 

13356  128 
subsection{*The Eliminator: @{term case}*} 
0  129 

13240  130 
lemma case_Inl [simp]: "case(c, d, Inl(a)) = c(a)" 
13255  131 
by (simp add: sum_defs) 
13240  132 

133 
lemma case_Inr [simp]: "case(c, d, Inr(b)) = d(b)" 

13255  134 
by (simp add: sum_defs) 
13240  135 

136 
lemma case_type [TC]: 

46953  137 
"[ u \<in> A+B; 
138 
!!x. x \<in> A ==> c(x): C(Inl(x)); 

139 
!!y. y \<in> B ==> d(y): C(Inr(y)) 

46820  140 
] ==> case(c,d,u) \<in> C(u)" 
13255  141 
by auto 
13240  142 

46953  143 
lemma expand_case: "u \<in> A+B ==> 
144 
R(case(c,d,u)) \<longleftrightarrow> 

145 
((\<forall>x\<in>A. u = Inl(x) \<longrightarrow> R(c(x))) & 

46820  146 
(\<forall>y\<in>B. u = Inr(y) \<longrightarrow> R(d(y))))" 
13240  147 
by auto 
148 

149 
lemma case_cong: 

46953  150 
"[ z \<in> A+B; 
151 
!!x. x \<in> A ==> c(x)=c'(x); 

152 
!!y. y \<in> B ==> d(y)=d'(y) 

13240  153 
] ==> case(c,d,z) = case(c',d',z)" 
46953  154 
by auto 
13240  155 

46953  156 
lemma case_case: "z \<in> A+B ==> 
157 
case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = 

13240  158 
case(%x. c(c'(x)), %y. d(d'(y)), z)" 
159 
by auto 

160 

161 

13356  162 
subsection{*More Rules for @{term "Part(A,h)"}*} 
13240  163 

164 
lemma Part_mono: "A<=B ==> Part(A,h)<=Part(B,h)" 

13255  165 
by blast 
13240  166 

167 
lemma Part_Collect: "Part(Collect(A,P), h) = Collect(Part(A,h), P)" 

13255  168 
by blast 
13240  169 

170 
lemmas Part_CollectE = 

45602  171 
Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE] 
13240  172 

46953  173 
lemma Part_Inl: "Part(A+B,Inl) = {Inl(x). x \<in> A}" 
13255  174 
by blast 
13240  175 

46953  176 
lemma Part_Inr: "Part(A+B,Inr) = {Inr(y). y \<in> B}" 
13255  177 
by blast 
13240  178 

46820  179 
lemma PartD1: "a \<in> Part(A,h) ==> a \<in> A" 
13255  180 
by (simp add: Part_def) 
13240  181 

182 
lemma Part_id: "Part(A,%x. x) = A" 

13255  183 
by blast 
13240  184 

46953  185 
lemma Part_Inr2: "Part(A+B, %x. Inr(h(x))) = {Inr(y). y \<in> Part(B,h)}" 
13255  186 
by blast 
13240  187 

46820  188 
lemma Part_sum_equality: "C \<subseteq> A+B ==> Part(C,Inl) \<union> Part(C,Inr) = C" 
13255  189 
by blast 
13240  190 

0  191 
end 