author | paulson <lp15@cam.ac.uk> |
Tue, 27 Sep 2022 17:46:52 +0100 | |
changeset 76215 | a642599ffdea |
parent 76214 | 0c18df79b1c8 |
child 76216 | 9fc34f76b4e8 |
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 |
||
60770 | 6 |
section\<open>Disjoint Sums\<close> |
13356 | 7 |
|
16417 | 8 |
theory Sum imports Bool equalities begin |
3923 | 9 |
|
60770 | 10 |
text\<open>And the "Part" primitive for simultaneous recursive type definitions\<close> |
13356 | 11 |
|
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
12 |
definition sum :: "[i,i]\<Rightarrow>i" (infixr \<open>+\<close> 65) where |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
13 |
"A+B \<equiv> {0}*A \<union> {1}*B" |
13240 | 14 |
|
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
15 |
definition Inl :: "i\<Rightarrow>i" where |
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
16 |
"Inl(a) \<equiv> \<langle>0,a\<rangle>" |
13240 | 17 |
|
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
18 |
definition Inr :: "i\<Rightarrow>i" where |
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
19 |
"Inr(b) \<equiv> \<langle>1,b\<rangle>" |
13240 | 20 |
|
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
21 |
definition "case" :: "[i\<Rightarrow>i, i\<Rightarrow>i, i]\<Rightarrow>i" where |
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
22 |
"case(c,d) \<equiv> (\<lambda>\<langle>y,z\<rangle>. cond(y, d(z), c(z)))" |
13240 | 23 |
|
24 |
(*operator for selecting out the various summands*) |
|
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
25 |
definition Part :: "[i,i\<Rightarrow>i] \<Rightarrow> i" where |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
26 |
"Part(A,h) \<equiv> {x \<in> A. \<exists>z. x = h(z)}" |
0 | 27 |
|
69593 | 28 |
subsection\<open>Rules for the \<^term>\<open>Part\<close> Primitive\<close> |
13240 | 29 |
|
46953 | 30 |
lemma Part_iff: |
76214 | 31 |
"a \<in> Part(A,h) \<longleftrightarrow> a \<in> A \<and> (\<exists>y. a=h(y))" |
13240 | 32 |
apply (unfold Part_def) |
33 |
apply (rule separation) |
|
34 |
done |
|
35 |
||
46953 | 36 |
lemma Part_eqI [intro]: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
37 |
"\<lbrakk>a \<in> A; a=h(b)\<rbrakk> \<Longrightarrow> 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!]: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
43 |
"\<lbrakk>a \<in> Part(A,h); \<And>z. \<lbrakk>a \<in> A; a=h(z)\<rbrakk> \<Longrightarrow> P |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
44 |
\<rbrakk> \<Longrightarrow> 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 |
||
60770 | 54 |
subsection\<open>Rules for Disjoint Sums\<close> |
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 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
63 |
lemma InlI [intro!,simp,TC]: "a \<in> A \<Longrightarrow> Inl(a) \<in> A+B" |
13255 | 64 |
by (unfold sum_defs, blast) |
13240 | 65 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
66 |
lemma InrI [intro!,simp,TC]: "b \<in> B \<Longrightarrow> Inr(b) \<in> A+B" |
13255 | 67 |
by (unfold sum_defs, blast) |
13240 | 68 |
|
69 |
(** Elimination rules **) |
|
70 |
||
71 |
lemma sumE [elim!]: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
72 |
"\<lbrakk>u \<in> A+B; |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
73 |
\<And>x. \<lbrakk>x \<in> A; u=Inl(x)\<rbrakk> \<Longrightarrow> P; |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
74 |
\<And>y. \<lbrakk>y \<in> B; u=Inr(y)\<rbrakk> \<Longrightarrow> P |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
75 |
\<rbrakk> \<Longrightarrow> 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 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
103 |
lemma InlD: "Inl(a): A+B \<Longrightarrow> a \<in> A" |
13255 | 104 |
by blast |
13240 | 105 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
106 |
lemma InrD: "Inr(b): A+B \<Longrightarrow> b \<in> B" |
13255 | 107 |
by blast |
13240 | 108 |
|
76214 | 109 |
lemma sum_iff: "u \<in> A+B \<longleftrightarrow> (\<exists>x. x \<in> A \<and> u=Inl(x)) | (\<exists>y. y \<in> B \<and> u=Inr(y))" |
13255 | 110 |
by blast |
111 |
||
58860 | 112 |
lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) \<longleftrightarrow> (x \<in> A)" |
13255 | 113 |
by auto |
114 |
||
58860 | 115 |
lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) \<longleftrightarrow> (y \<in> B)" |
13255 | 116 |
by auto |
13240 | 117 |
|
76214 | 118 |
lemma sum_subset_iff: "A+B \<subseteq> C+D \<longleftrightarrow> A<=C \<and> B<=D" |
13255 | 119 |
by blast |
13240 | 120 |
|
76214 | 121 |
lemma sum_equal_iff: "A+B = C+D \<longleftrightarrow> A=C \<and> 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 |
||
69593 | 128 |
subsection\<open>The Eliminator: \<^term>\<open>case\<close>\<close> |
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]: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
137 |
"\<lbrakk>u \<in> A+B; |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
138 |
\<And>x. x \<in> A \<Longrightarrow> c(x): C(Inl(x)); |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
139 |
\<And>y. y \<in> B \<Longrightarrow> d(y): C(Inr(y)) |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
140 |
\<rbrakk> \<Longrightarrow> case(c,d,u) \<in> C(u)" |
13255 | 141 |
by auto |
13240 | 142 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
143 |
lemma expand_case: "u \<in> A+B \<Longrightarrow> |
46953 | 144 |
R(case(c,d,u)) \<longleftrightarrow> |
76214 | 145 |
((\<forall>x\<in>A. u = Inl(x) \<longrightarrow> R(c(x))) \<and> |
46820 | 146 |
(\<forall>y\<in>B. u = Inr(y) \<longrightarrow> R(d(y))))" |
13240 | 147 |
by auto |
148 |
||
149 |
lemma case_cong: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
150 |
"\<lbrakk>z \<in> A+B; |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
151 |
\<And>x. x \<in> A \<Longrightarrow> c(x)=c'(x); |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
152 |
\<And>y. y \<in> B \<Longrightarrow> d(y)=d'(y) |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
153 |
\<rbrakk> \<Longrightarrow> case(c,d,z) = case(c',d',z)" |
46953 | 154 |
by auto |
13240 | 155 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
156 |
lemma case_case: "z \<in> A+B \<Longrightarrow> |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
157 |
case(c, d, case(\<lambda>x. Inl(c'(x)), \<lambda>y. Inr(d'(y)), z)) = |
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
158 |
case(\<lambda>x. c(c'(x)), \<lambda>y. d(d'(y)), z)" |
13240 | 159 |
by auto |
160 |
||
161 |
||
69593 | 162 |
subsection\<open>More Rules for \<^term>\<open>Part(A,h)\<close>\<close> |
13240 | 163 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
164 |
lemma Part_mono: "A<=B \<Longrightarrow> 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 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
179 |
lemma PartD1: "a \<in> Part(A,h) \<Longrightarrow> a \<in> A" |
13255 | 180 |
by (simp add: Part_def) |
13240 | 181 |
|
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
182 |
lemma Part_id: "Part(A,\<lambda>x. x) = A" |
13255 | 183 |
by blast |
13240 | 184 |
|
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
185 |
lemma Part_Inr2: "Part(A+B, \<lambda>x. Inr(h(x))) = {Inr(y). y \<in> Part(B,h)}" |
13255 | 186 |
by blast |
13240 | 187 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
188 |
lemma Part_sum_equality: "C \<subseteq> A+B \<Longrightarrow> Part(C,Inl) \<union> Part(C,Inr) = C" |
13255 | 189 |
by blast |
13240 | 190 |
|
0 | 191 |
end |