923
|
1 |
(* Title: HOL/Sum.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1991 University of Cambridge
|
|
5 |
|
|
6 |
For Sum.thy. The disjoint sum of two types
|
|
7 |
*)
|
|
8 |
|
|
9 |
open Sum;
|
|
10 |
|
|
11 |
(** Inl_Rep and Inr_Rep: Representations of the constructors **)
|
|
12 |
|
|
13 |
(*This counts as a non-emptiness result for admitting 'a+'b as a type*)
|
|
14 |
goalw Sum.thy [Sum_def] "Inl_Rep(a) : Sum";
|
|
15 |
by (EVERY1 [rtac CollectI, rtac disjI1, rtac exI, rtac refl]);
|
|
16 |
qed "Inl_RepI";
|
|
17 |
|
|
18 |
goalw Sum.thy [Sum_def] "Inr_Rep(b) : Sum";
|
|
19 |
by (EVERY1 [rtac CollectI, rtac disjI2, rtac exI, rtac refl]);
|
|
20 |
qed "Inr_RepI";
|
|
21 |
|
|
22 |
goal Sum.thy "inj_onto Abs_Sum Sum";
|
|
23 |
by (rtac inj_onto_inverseI 1);
|
|
24 |
by (etac Abs_Sum_inverse 1);
|
|
25 |
qed "inj_onto_Abs_Sum";
|
|
26 |
|
|
27 |
(** Distinctness of Inl and Inr **)
|
|
28 |
|
|
29 |
goalw Sum.thy [Inl_Rep_def, Inr_Rep_def] "Inl_Rep(a) ~= Inr_Rep(b)";
|
|
30 |
by (EVERY1 [rtac notI,
|
|
31 |
etac (fun_cong RS fun_cong RS fun_cong RS iffE),
|
|
32 |
rtac (notE RS ccontr), etac (mp RS conjunct2),
|
|
33 |
REPEAT o (ares_tac [refl,conjI]) ]);
|
|
34 |
qed "Inl_Rep_not_Inr_Rep";
|
|
35 |
|
|
36 |
goalw Sum.thy [Inl_def,Inr_def] "Inl(a) ~= Inr(b)";
|
|
37 |
by (rtac (inj_onto_Abs_Sum RS inj_onto_contraD) 1);
|
|
38 |
by (rtac Inl_Rep_not_Inr_Rep 1);
|
|
39 |
by (rtac Inl_RepI 1);
|
|
40 |
by (rtac Inr_RepI 1);
|
|
41 |
qed "Inl_not_Inr";
|
|
42 |
|
|
43 |
bind_thm ("Inl_neq_Inr", (Inl_not_Inr RS notE));
|
|
44 |
val Inr_neq_Inl = sym RS Inl_neq_Inr;
|
|
45 |
|
|
46 |
goal Sum.thy "(Inl(a)=Inr(b)) = False";
|
|
47 |
by (simp_tac (HOL_ss addsimps [Inl_not_Inr]) 1);
|
|
48 |
qed "Inl_Inr_eq";
|
|
49 |
|
|
50 |
goal Sum.thy "(Inr(b)=Inl(a)) = False";
|
|
51 |
by (simp_tac (HOL_ss addsimps [Inl_not_Inr RS not_sym]) 1);
|
|
52 |
qed "Inr_Inl_eq";
|
|
53 |
|
|
54 |
|
|
55 |
(** Injectiveness of Inl and Inr **)
|
|
56 |
|
|
57 |
val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
|
|
58 |
by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
|
|
59 |
by (fast_tac HOL_cs 1);
|
|
60 |
qed "Inl_Rep_inject";
|
|
61 |
|
|
62 |
val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
|
|
63 |
by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
|
|
64 |
by (fast_tac HOL_cs 1);
|
|
65 |
qed "Inr_Rep_inject";
|
|
66 |
|
|
67 |
goalw Sum.thy [Inl_def] "inj(Inl)";
|
|
68 |
by (rtac injI 1);
|
|
69 |
by (etac (inj_onto_Abs_Sum RS inj_ontoD RS Inl_Rep_inject) 1);
|
|
70 |
by (rtac Inl_RepI 1);
|
|
71 |
by (rtac Inl_RepI 1);
|
|
72 |
qed "inj_Inl";
|
|
73 |
val Inl_inject = inj_Inl RS injD;
|
|
74 |
|
|
75 |
goalw Sum.thy [Inr_def] "inj(Inr)";
|
|
76 |
by (rtac injI 1);
|
|
77 |
by (etac (inj_onto_Abs_Sum RS inj_ontoD RS Inr_Rep_inject) 1);
|
|
78 |
by (rtac Inr_RepI 1);
|
|
79 |
by (rtac Inr_RepI 1);
|
|
80 |
qed "inj_Inr";
|
|
81 |
val Inr_inject = inj_Inr RS injD;
|
|
82 |
|
|
83 |
goal Sum.thy "(Inl(x)=Inl(y)) = (x=y)";
|
|
84 |
by (fast_tac (HOL_cs addSEs [Inl_inject]) 1);
|
|
85 |
qed "Inl_eq";
|
|
86 |
|
|
87 |
goal Sum.thy "(Inr(x)=Inr(y)) = (x=y)";
|
|
88 |
by (fast_tac (HOL_cs addSEs [Inr_inject]) 1);
|
|
89 |
qed "Inr_eq";
|
|
90 |
|
|
91 |
(*** Rules for the disjoint sum of two SETS ***)
|
|
92 |
|
|
93 |
(** Introduction rules for the injections **)
|
|
94 |
|
|
95 |
goalw Sum.thy [sum_def] "!!a A B. a : A ==> Inl(a) : A plus B";
|
|
96 |
by (REPEAT (ares_tac [UnI1,imageI] 1));
|
|
97 |
qed "InlI";
|
|
98 |
|
|
99 |
goalw Sum.thy [sum_def] "!!b A B. b : B ==> Inr(b) : A plus B";
|
|
100 |
by (REPEAT (ares_tac [UnI2,imageI] 1));
|
|
101 |
qed "InrI";
|
|
102 |
|
|
103 |
(** Elimination rules **)
|
|
104 |
|
|
105 |
val major::prems = goalw Sum.thy [sum_def]
|
|
106 |
"[| u: A plus B; \
|
|
107 |
\ !!x. [| x:A; u=Inl(x) |] ==> P; \
|
|
108 |
\ !!y. [| y:B; u=Inr(y) |] ==> P \
|
|
109 |
\ |] ==> P";
|
|
110 |
by (rtac (major RS UnE) 1);
|
|
111 |
by (REPEAT (rtac refl 1
|
|
112 |
ORELSE eresolve_tac (prems@[imageE,ssubst]) 1));
|
|
113 |
qed "plusE";
|
|
114 |
|
|
115 |
|
|
116 |
val sum_cs = set_cs addSIs [InlI, InrI]
|
|
117 |
addSEs [plusE, Inl_neq_Inr, Inr_neq_Inl]
|
|
118 |
addSDs [Inl_inject, Inr_inject];
|
|
119 |
|
|
120 |
|
|
121 |
(** sum_case -- the selection operator for sums **)
|
|
122 |
|
|
123 |
goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)";
|
|
124 |
by (fast_tac (sum_cs addIs [select_equality]) 1);
|
|
125 |
qed "sum_case_Inl";
|
|
126 |
|
|
127 |
goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
|
|
128 |
by (fast_tac (sum_cs addIs [select_equality]) 1);
|
|
129 |
qed "sum_case_Inr";
|
|
130 |
|
|
131 |
(** Exhaustion rule for sums -- a degenerate form of induction **)
|
|
132 |
|
|
133 |
val prems = goalw Sum.thy [Inl_def,Inr_def]
|
|
134 |
"[| !!x::'a. s = Inl(x) ==> P; !!y::'b. s = Inr(y) ==> P \
|
|
135 |
\ |] ==> P";
|
|
136 |
by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1);
|
|
137 |
by (REPEAT (eresolve_tac [disjE,exE] 1
|
|
138 |
ORELSE EVERY1 [resolve_tac prems,
|
|
139 |
etac subst,
|
|
140 |
rtac (Rep_Sum_inverse RS sym)]));
|
|
141 |
qed "sumE";
|
|
142 |
|
|
143 |
goal Sum.thy "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
|
|
144 |
by (EVERY1 [res_inst_tac [("s","s")] sumE,
|
|
145 |
etac ssubst, rtac sum_case_Inl,
|
|
146 |
etac ssubst, rtac sum_case_Inr]);
|
|
147 |
qed "surjective_sum";
|
|
148 |
|
|
149 |
goal Sum.thy "R(sum_case f g s) = \
|
|
150 |
\ ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
|
|
151 |
by (rtac sumE 1);
|
|
152 |
by (etac ssubst 1);
|
|
153 |
by (stac sum_case_Inl 1);
|
|
154 |
by (fast_tac (set_cs addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
|
|
155 |
by (etac ssubst 1);
|
|
156 |
by (stac sum_case_Inr 1);
|
|
157 |
by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
|
|
158 |
qed "expand_sum_case";
|
|
159 |
|
|
160 |
val sum_ss = prod_ss addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq,
|
|
161 |
sum_case_Inl, sum_case_Inr];
|
|
162 |
|
|
163 |
(*Prevents simplification of f and g: much faster*)
|
|
164 |
qed_goal "sum_case_weak_cong" Sum.thy
|
|
165 |
"s=t ==> sum_case f g s = sum_case f g t"
|
|
166 |
(fn [prem] => [rtac (prem RS arg_cong) 1]);
|
|
167 |
|
|
168 |
|
|
169 |
|
|
170 |
|
|
171 |
(** Rules for the Part primitive **)
|
|
172 |
|
|
173 |
goalw Sum.thy [Part_def]
|
|
174 |
"!!a b A h. [| a : A; a=h(b) |] ==> a : Part A h";
|
|
175 |
by (fast_tac set_cs 1);
|
|
176 |
qed "Part_eqI";
|
|
177 |
|
|
178 |
val PartI = refl RSN (2,Part_eqI);
|
|
179 |
|
|
180 |
val major::prems = goalw Sum.thy [Part_def]
|
|
181 |
"[| a : Part A h; !!z. [| a : A; a=h(z) |] ==> P \
|
|
182 |
\ |] ==> P";
|
|
183 |
by (rtac (major RS IntE) 1);
|
|
184 |
by (etac CollectE 1);
|
|
185 |
by (etac exE 1);
|
|
186 |
by (REPEAT (ares_tac prems 1));
|
|
187 |
qed "PartE";
|
|
188 |
|
|
189 |
goalw Sum.thy [Part_def] "Part A h <= A";
|
|
190 |
by (rtac Int_lower1 1);
|
|
191 |
qed "Part_subset";
|
|
192 |
|
|
193 |
goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
|
|
194 |
by (fast_tac (set_cs addSIs [PartI] addSEs [PartE]) 1);
|
|
195 |
qed "Part_mono";
|
|
196 |
|
|
197 |
goalw Sum.thy [Part_def] "!!a. a : Part A h ==> a : A";
|
|
198 |
by (etac IntD1 1);
|
|
199 |
qed "PartD1";
|
|
200 |
|
|
201 |
goal Sum.thy "Part A (%x.x) = A";
|
|
202 |
by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
|
|
203 |
qed "Part_id";
|
|
204 |
|