author | blanchet |
Wed, 06 Nov 2013 22:50:12 +0100 | |
changeset 54284 | 0b53378080d9 |
parent 46953 | 2b6e55924af3 |
child 58860 | fee7cfa69c50 |
permissions | -rw-r--r-- |
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 |