author | wenzelm |
Mon, 12 Apr 2021 14:14:47 +0200 | |
changeset 73563 | 55b66a45bc94 |
parent 67443 | 3abf6a722518 |
child 80932 | 261cd8722677 |
permissions | -rw-r--r-- |
10213 | 1 |
(* Title: HOL/Sum_Type.thy |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
Copyright 1992 University of Cambridge |
|
4 |
*) |
|
5 |
||
63575 | 6 |
section \<open>The Disjoint Sum of Two Types\<close> |
10213 | 7 |
|
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
8 |
theory Sum_Type |
63575 | 9 |
imports Typedef Inductive Fun |
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
10 |
begin |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
11 |
|
60758 | 12 |
subsection \<open>Construction of the sum type and its basic abstract operations\<close> |
10213 | 13 |
|
63400 | 14 |
definition Inl_Rep :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" |
15 |
where "Inl_Rep a x y p \<longleftrightarrow> x = a \<and> p" |
|
10213 | 16 |
|
63400 | 17 |
definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" |
18 |
where "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p" |
|
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
19 |
|
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45204
diff
changeset
|
20 |
definition "sum = {f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}" |
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45204
diff
changeset
|
21 |
|
63400 | 22 |
typedef ('a, 'b) sum (infixr "+" 10) = "sum :: ('a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool) set" |
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45204
diff
changeset
|
23 |
unfolding sum_def by auto |
10213 | 24 |
|
37388 | 25 |
lemma Inl_RepI: "Inl_Rep a \<in> sum" |
26 |
by (auto simp add: sum_def) |
|
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
27 |
|
37388 | 28 |
lemma Inr_RepI: "Inr_Rep b \<in> sum" |
29 |
by (auto simp add: sum_def) |
|
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
30 |
|
37388 | 31 |
lemma inj_on_Abs_sum: "A \<subseteq> sum \<Longrightarrow> inj_on Abs_sum A" |
32 |
by (rule inj_on_inverseI, rule Abs_sum_inverse) auto |
|
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
33 |
|
33962 | 34 |
lemma Inl_Rep_inject: "inj_on Inl_Rep A" |
35 |
proof (rule inj_onI) |
|
36 |
show "\<And>a c. Inl_Rep a = Inl_Rep c \<Longrightarrow> a = c" |
|
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
37 |
by (auto simp add: Inl_Rep_def fun_eq_iff) |
33962 | 38 |
qed |
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
39 |
|
33962 | 40 |
lemma Inr_Rep_inject: "inj_on Inr_Rep A" |
41 |
proof (rule inj_onI) |
|
42 |
show "\<And>b d. Inr_Rep b = Inr_Rep d \<Longrightarrow> b = d" |
|
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
43 |
by (auto simp add: Inr_Rep_def fun_eq_iff) |
33962 | 44 |
qed |
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
45 |
|
33962 | 46 |
lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a \<noteq> Inr_Rep b" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
47 |
by (auto simp add: Inl_Rep_def Inr_Rep_def fun_eq_iff) |
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
48 |
|
63400 | 49 |
definition Inl :: "'a \<Rightarrow> 'a + 'b" |
50 |
where "Inl = Abs_sum \<circ> Inl_Rep" |
|
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
51 |
|
63400 | 52 |
definition Inr :: "'b \<Rightarrow> 'a + 'b" |
53 |
where "Inr = Abs_sum \<circ> Inr_Rep" |
|
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
54 |
|
29025
8c8859c0d734
move lemmas from Numeral_Type.thy to other theories
huffman
parents:
28524
diff
changeset
|
55 |
lemma inj_Inl [simp]: "inj_on Inl A" |
63400 | 56 |
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
|
57 |
|
33962 | 58 |
lemma Inl_inject: "Inl x = Inl y \<Longrightarrow> x = y" |
63400 | 59 |
using inj_Inl by (rule injD) |
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
60 |
|
29025
8c8859c0d734
move lemmas from Numeral_Type.thy to other theories
huffman
parents:
28524
diff
changeset
|
61 |
lemma inj_Inr [simp]: "inj_on Inr A" |
63400 | 62 |
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 new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
63 |
|
33962 | 64 |
lemma Inr_inject: "Inr x = Inr y \<Longrightarrow> x = y" |
63400 | 65 |
using inj_Inr by (rule injD) |
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
66 |
|
33962 | 67 |
lemma Inl_not_Inr: "Inl a \<noteq> Inr b" |
68 |
proof - |
|
63400 | 69 |
have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum" |
70 |
using Inl_RepI [of a] Inr_RepI [of b] by auto |
|
37388 | 71 |
with inj_on_Abs_sum have "inj_on Abs_sum {Inl_Rep a, Inr_Rep b}" . |
63400 | 72 |
with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_sum (Inl_Rep a) \<noteq> Abs_sum (Inr_Rep b)" |
73 |
by auto |
|
74 |
then show ?thesis |
|
75 |
by (simp add: Inl_def Inr_def) |
|
33962 | 76 |
qed |
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
77 |
|
63400 | 78 |
lemma Inr_not_Inl: "Inr b \<noteq> Inl a" |
33962 | 79 |
using Inl_not_Inr by (rule not_sym) |
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
80 |
|
63400 | 81 |
lemma sumE: |
33962 | 82 |
assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P" |
83 |
and "\<And>y::'b. s = Inr y \<Longrightarrow> P" |
|
84 |
shows P |
|
37388 | 85 |
proof (rule Abs_sum_cases [of s]) |
63400 | 86 |
fix f |
37388 | 87 |
assume "s = Abs_sum f" and "f \<in> sum" |
63575 | 88 |
with assms show P |
89 |
by (auto simp add: sum_def Inl_def Inr_def) |
|
33962 | 90 |
qed |
33961 | 91 |
|
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset
|
92 |
free_constructors case_sum for |
63400 | 93 |
isl: Inl projl |
94 |
| Inr projr |
|
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
55931
diff
changeset
|
95 |
by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr) |
55393
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset
|
96 |
|
61799 | 97 |
text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close> |
55442 | 98 |
|
60758 | 99 |
setup \<open>Sign.mandatory_path "old"\<close> |
55393
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset
|
100 |
|
58306
117ba6cbe414
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
blanchet
parents:
58189
diff
changeset
|
101 |
old_rep_datatype Inl Inr |
33961 | 102 |
proof - |
103 |
fix P |
|
104 |
fix s :: "'a + 'b" |
|
61076 | 105 |
assume x: "\<And>x::'a. P (Inl x)" and y: "\<And>y::'b. P (Inr y)" |
33961 | 106 |
then show "P s" by (auto intro: sumE [of s]) |
33962 | 107 |
qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr) |
108 |
||
60758 | 109 |
setup \<open>Sign.parent_path\<close> |
55393
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset
|
110 |
|
61799 | 111 |
text \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close> |
55442 | 112 |
|
60758 | 113 |
setup \<open>Sign.mandatory_path "sum"\<close> |
55393
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset
|
114 |
|
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset
|
115 |
declare |
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset
|
116 |
old.sum.inject[iff del] |
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset
|
117 |
old.sum.distinct(1)[simp del, induct_simp del] |
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset
|
118 |
|
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset
|
119 |
lemmas induct = old.sum.induct |
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset
|
120 |
lemmas inducts = old.sum.inducts |
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55575
diff
changeset
|
121 |
lemmas rec = old.sum.rec |
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55575
diff
changeset
|
122 |
lemmas simps = sum.inject sum.distinct sum.case sum.rec |
55393
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset
|
123 |
|
60758 | 124 |
setup \<open>Sign.parent_path\<close> |
55393
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset
|
125 |
|
63400 | 126 |
primrec map_sum :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" |
63575 | 127 |
where |
128 |
"map_sum f1 f2 (Inl a) = Inl (f1 a)" |
|
129 |
| "map_sum f1 f2 (Inr a) = Inr (f2 a)" |
|
40610 | 130 |
|
63400 | 131 |
functor map_sum: map_sum |
132 |
proof - |
|
133 |
show "map_sum f g \<circ> map_sum h i = map_sum (f \<circ> h) (g \<circ> i)" for f g h i |
|
41372 | 134 |
proof |
63400 | 135 |
show "(map_sum f g \<circ> map_sum h i) s = map_sum (f \<circ> h) (g \<circ> i) s" for s |
41372 | 136 |
by (cases s) simp_all |
137 |
qed |
|
55931 | 138 |
show "map_sum id id = id" |
41372 | 139 |
proof |
63400 | 140 |
show "map_sum id id s = id s" for s |
41372 | 141 |
by (cases s) simp_all |
142 |
qed |
|
40610 | 143 |
qed |
144 |
||
53010 | 145 |
lemma split_sum_all: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))" |
146 |
by (auto intro: sum.induct) |
|
147 |
||
148 |
lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))" |
|
63400 | 149 |
using split_sum_all[of "\<lambda>x. \<not>P x"] by blast |
150 |
||
33961 | 151 |
|
60758 | 152 |
subsection \<open>Projections\<close> |
33962 | 153 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55403
diff
changeset
|
154 |
lemma case_sum_KK [simp]: "case_sum (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)" |
33961 | 155 |
by (rule ext) (simp split: sum.split) |
156 |
||
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55403
diff
changeset
|
157 |
lemma surjective_sum: "case_sum (\<lambda>x::'a. f (Inl x)) (\<lambda>y::'b. f (Inr y)) = f" |
33962 | 158 |
proof |
159 |
fix s :: "'a + 'b" |
|
61076 | 160 |
show "(case s of Inl (x::'a) \<Rightarrow> f (Inl x) | Inr (y::'b) \<Rightarrow> f (Inr y)) = f s" |
33962 | 161 |
by (cases s) simp_all |
162 |
qed |
|
33961 | 163 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55403
diff
changeset
|
164 |
lemma case_sum_inject: |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55403
diff
changeset
|
165 |
assumes a: "case_sum f1 f2 = case_sum g1 g2" |
63400 | 166 |
and r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P" |
33962 | 167 |
shows P |
168 |
proof (rule r) |
|
63400 | 169 |
show "f1 = g1" |
170 |
proof |
|
33962 | 171 |
fix x :: 'a |
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55403
diff
changeset
|
172 |
from a have "case_sum f1 f2 (Inl x) = case_sum g1 g2 (Inl x)" by simp |
33962 | 173 |
then show "f1 x = g1 x" by simp |
174 |
qed |
|
63400 | 175 |
show "f2 = g2" |
176 |
proof |
|
33962 | 177 |
fix y :: 'b |
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55403
diff
changeset
|
178 |
from a have "case_sum f1 f2 (Inr y) = case_sum g1 g2 (Inr y)" by simp |
33962 | 179 |
then show "f2 y = g2 y" by simp |
180 |
qed |
|
181 |
qed |
|
182 |
||
63400 | 183 |
primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" |
184 |
where "Suml f (Inl x) = f x" |
|
33962 | 185 |
|
63400 | 186 |
primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" |
187 |
where "Sumr f (Inr x) = f x" |
|
33962 | 188 |
|
189 |
lemma Suml_inject: |
|
63400 | 190 |
assumes "Suml f = Suml g" |
191 |
shows "f = g" |
|
33962 | 192 |
proof |
193 |
fix x :: 'a |
|
61076 | 194 |
let ?s = "Inl x :: 'a + 'b" |
33962 | 195 |
from assms have "Suml f ?s = Suml g ?s" by simp |
196 |
then show "f x = g x" by simp |
|
33961 | 197 |
qed |
198 |
||
33962 | 199 |
lemma Sumr_inject: |
63400 | 200 |
assumes "Sumr f = Sumr g" |
201 |
shows "f = g" |
|
33962 | 202 |
proof |
203 |
fix x :: 'b |
|
61076 | 204 |
let ?s = "Inr x :: 'a + 'b" |
33962 | 205 |
from assms have "Sumr f ?s = Sumr g ?s" by simp |
206 |
then show "f x = g x" by simp |
|
207 |
qed |
|
33961 | 208 |
|
33995 | 209 |
|
60758 | 210 |
subsection \<open>The Disjoint Sum of Sets\<close> |
33961 | 211 |
|
63400 | 212 |
definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) |
213 |
where "A <+> B = Inl ` A \<union> Inr ` B" |
|
33962 | 214 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63575
diff
changeset
|
215 |
hide_const (open) Plus \<comment> \<open>Valuable identifier\<close> |
40271 | 216 |
|
33962 | 217 |
lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B" |
63400 | 218 |
by (simp add: Plus_def) |
33961 | 219 |
|
33962 | 220 |
lemma InrI [intro!]: "b \<in> B \<Longrightarrow> Inr b \<in> A <+> B" |
63400 | 221 |
by (simp add: Plus_def) |
33961 | 222 |
|
60758 | 223 |
text \<open>Exhaustion rule for sums, a degenerate form of induction\<close> |
33962 | 224 |
|
63400 | 225 |
lemma PlusE [elim!]: |
33962 | 226 |
"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" |
63400 | 227 |
by (auto simp add: Plus_def) |
33961 | 228 |
|
33962 | 229 |
lemma Plus_eq_empty_conv [simp]: "A <+> B = {} \<longleftrightarrow> A = {} \<and> B = {}" |
63400 | 230 |
by auto |
33961 | 231 |
|
33962 | 232 |
lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
233 |
proof (rule set_eqI) |
33962 | 234 |
fix u :: "'a + 'b" |
235 |
show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto |
|
236 |
qed |
|
33961 | 237 |
|
63400 | 238 |
lemma UNIV_sum: "UNIV = Inl ` UNIV \<union> Inr ` UNIV" |
49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset
|
239 |
proof - |
63400 | 240 |
have "x \<in> range Inl" if "x \<notin> range Inr" for x :: "'a + 'b" |
241 |
using that by (cases x) simp_all |
|
242 |
then show ?thesis by auto |
|
49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset
|
243 |
qed |
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset
|
244 |
|
55393
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset
|
245 |
hide_const (open) Suml Sumr sum |
45204
5e4a1270c000
hide typedef-generated constants Product_Type.prod and Sum_Type.sum
huffman
parents:
41505
diff
changeset
|
246 |
|
10213 | 247 |
end |